summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-06 14:48:32 +0100
committerSon Ho2022-01-06 14:48:32 +0100
commitec40683d2462ae15c1d0e68dbf8c6e14825b9cef (patch)
tree1ca6e6bc22eb003b20e605f69b53e5e35ebdb9ec
parentf2fb0dc39cfa9aef2b16963d3f8a270ec45bae5e (diff)
Implement tests for the symbolic interpreter
-rw-r--r--src/Interpreter.ml26
-rw-r--r--src/InterpreterStatements.ml2
-rw-r--r--src/main.ml7
3 files changed, 14 insertions, 21 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index cb42abf2..6b27b180 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -93,6 +93,7 @@ module Test = struct
(* Return *)
ctx
in
+ let ctx = List.fold_left create_abs ctx inst_sg.regions_hierarchy in
(* Split the variables between return var, inputs and remaining locals *)
let ret_var = List.hd fdef.locals in
let input_vars, local_vars =
@@ -162,8 +163,8 @@ module Test = struct
(** Execute the symbolic interpreter on a function. *)
let test_symbolic_function (type_context : C.type_context)
- (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result list
- =
+ (fun_defs : A.fun_def list) (fid : A.FunDefId.id) :
+ C.eval_ctx eval_result list =
(* Retrieve the function declaration *)
let fdef = A.FunDefId.nth fun_defs fid in
@@ -178,22 +179,11 @@ module Test = struct
assert (fdef.A.arg_count = 0);
(* Create the evaluation context *)
- let ctx = initialize_context type_context fun_defs in
-
- (* Initialize the inputs as symbolic values *)
- raise Unimplemented
+ let ctx = initialize_symbolic_context_for_fun type_context fun_defs fdef in
- (* (* Initialize the remaining local variables as Bottom *)
- let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
-
- (* Evaluate the function *)
- let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in
- match eval_function_body config ctx fdef.A.body with
- | [ Ok _ ] -> Ok ()
- | [ Error err ] -> Error err
- | _ ->
- (* We execute the concrete interpreter: there shouldn't be any branching *)
- failwith "Unreachable"*)
+ (* Evaluate the function *)
+ let config = { C.mode = C.SymbolicMode; C.check_invariants = true } in
+ eval_function_body config ctx fdef.A.body
(** Execute the symbolic interpreter on a list of functions.
@@ -209,5 +199,5 @@ module Test = struct
if List.for_all Result.is_ok res then ()
else failwith "Unit test failed (symbolic execution)"
in
- List.iter test_fun fun_defs
+ List.iter test_fun no_loop_funs
end
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 6b06a27f..114f0daf 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -906,7 +906,7 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
(** Evaluate a statement seen as a function body (auxiliary helper for
[eval_statement]) *)
and eval_function_body (config : C.config) (ctx : C.eval_ctx)
- (body : A.statement) : (C.eval_ctx, eval_error) result list =
+ (body : A.statement) : C.eval_ctx eval_result list =
let res = eval_statement config ctx body in
let finish res =
match res with
diff --git a/src/main.ml b/src/main.ml
index b4537c3a..63f15c85 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -45,5 +45,8 @@ let () =
(* Print the module *)
log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
- (* Test the unit functions *)
- I.Test.test_unit_functions m.types m.functions
+ (* Test the unit functions with the concrete interpreter *)
+ 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