diff options
| -rw-r--r-- | src/Interpreter.ml | 14 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 13 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 7 | ||||
| -rw-r--r-- | src/main.ml | 2 |
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 |