summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml14
-rw-r--r--src/InterpreterStatements.ml13
-rw-r--r--src/InterpreterUtils.ml7
-rw-r--r--src/main.ml2
4 files changed, 23 insertions, 13 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 523957af..c8739394 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -162,7 +162,7 @@ module Test = struct
List.iter test_unit_fun unit_funs
(** Execute the symbolic interpreter on a function. *)
- let test_symbolic_function (type_context : C.type_context)
+ let test_function_symbolic (type_context : C.type_context)
(fun_defs : A.fun_def list) (fid : A.FunDefId.id) :
C.eval_ctx eval_result list =
(* Retrieve the function declaration *)
@@ -171,7 +171,7 @@ module Test = struct
(* Debug *)
L.log#ldebug
(lazy
- ("test_symbolic_function: " ^ Print.Types.name_to_string fdef.A.name));
+ ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name));
(* Create the evaluation context *)
let ctx = initialize_symbolic_context_for_fun type_context fun_defs fdef in
@@ -185,16 +185,18 @@ module Test = struct
TODO: for now we ignore the functions which contain loops, because
they are not supported by the symbolic interpreter.
*)
- let test_symbolic_functions (type_defs : T.type_def list)
+ let test_functions_symbolic (type_defs : T.type_def list)
(fun_defs : A.fun_def list) : unit =
let no_loop_funs =
List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) fun_defs
in
let test_fun (def : A.fun_def) : unit =
let type_ctx = { C.type_defs } in
- let res = test_symbolic_function type_ctx fun_defs def.A.def_id in
- if List.for_all Result.is_ok res then ()
- else failwith "Unit test failed (symbolic execution)"
+ (* Execute the function - note that as the symbolic interpreter explores
+ * all the path, some executions are expected to "panic": we thus don't
+ * check the return value *)
+ let _ = test_function_symbolic type_ctx fun_defs def.A.def_id in
+ ()
in
List.iter test_fun no_loop_funs
end
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 114f0daf..83d531a0 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -475,8 +475,9 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
(* Debugging *)
L.log#ldebug
(lazy
- ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate statement: "
- ^ statement_to_string ctx st ^ "\n"));
+ ("\n**About to evaluate statement**: [\n"
+ ^ statement_to_string_with_tab ctx st
+ ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
(* Sanity check *)
if config.C.check_invariants then Inv.check_invariants ctx;
(* Evaluate *)
@@ -504,7 +505,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
match v.value with
| Concrete (Bool b) ->
if b = assertion.expected then [ Ok (ctx, Unit) ] else [ Error Panic ]
- | _ -> failwith "Expected a boolean")
+ | _ -> failwith ("Expected a boolean, got: " ^ V.show_value v.value))
| A.Call call -> eval_function_call config ctx call
| A.Panic -> [ Error Panic ]
| A.Return -> [ Ok (ctx, Return) ]
@@ -611,9 +612,9 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets)
eval_statement config ctx st
in
(* Execute the two branches *)
- List.append
- (expand_and_execute see_true st1)
- (expand_and_execute see_false st2)
+ let ctxl_true = expand_and_execute see_true st1 in
+ let ctxl_false = expand_and_execute see_false st2 in
+ List.append ctxl_true ctxl_false
| _ -> failwith "Inconsistent state")
| A.SwitchInt (int_ty, tgts, otherwise) -> (
match op_v.value with
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index cc54cd24..9f6cf495 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -26,6 +26,9 @@ let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
let statement_to_string ctx =
Print.EvalCtxCfimAst.statement_to_string ctx "" " "
+let statement_to_string_with_tab ctx =
+ Print.EvalCtxCfimAst.statement_to_string ctx " " " "
+
let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
sv0.V.sv_id = sv1.V.sv_id
@@ -65,6 +68,10 @@ let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value =
let value = V.Symbolic sv in
{ V.value; ty }
+(** Create a typed value from a symbolic value.
+
+ Initializes the set of ended regions with `empty`.
+ *)
let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
V.typed_value =
let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
diff --git a/src/main.ml b/src/main.ml
index 63f15c85..e5c3c324 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -49,4 +49,4 @@ let () =
I.Test.test_unit_functions m.types m.functions;
(* Evaluate the symbolic interpreter on the functions *)
- I.Test.test_symbolic_functions m.types m.functions
+ I.Test.test_functions_symbolic m.types m.functions