From ec40683d2462ae15c1d0e68dbf8c6e14825b9cef Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 14:48:32 +0100
Subject: Implement tests for the symbolic interpreter

---
 src/Interpreter.ml           | 26 ++++++++------------------
 src/InterpreterStatements.ml |  2 +-
 src/main.ml                  |  7 +++++--
 3 files changed, 14 insertions(+), 21 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3