Implement test_unit_function

2 files changed, 36 insertions, 0 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 824fd8ad..8072b316 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -16,6 +16,8 @@ module type Id = sig
 
   val zero : id
 
+  val generator_zero : generator
+
   val fresh : generator -> id * generator
 
   val to_string : id -> string
@@ -85,6 +87,8 @@ module IdGen () : Id = struct
 
   let zero = 0
 
+  let generator_zero = 0
+
   let incr x =
     (* Identifiers should never overflow (because max_int is a really big
      * value - but we really want to make sure we detect overflows if
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 308a443b..66eb7d87 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2307,3 +2307,35 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) :
               | None -> eval_expression config ctx1 otherwise
               | Some (_, tgt) -> eval_expression config ctx1 tgt)
           | _ -> failwith "Inconsistent state"))
+
+(** Test a unit function (taking no arguments) by evaluating it in an empty
+    environment
+ *)
+let test_unit_function (type_decls : T.type_def T.TypeDefId.vector)
+    (fun_decls : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) :
+    unit eval_result =
+  (* Retrieve the function declaration *)
+  let fdef = A.FunDefId.nth fun_decls fid in
+
+  (* Sanity check - *)
+  assert (T.RegionVarId.length fdef.A.signature.region_params = 0);
+  assert (T.TypeVarId.length fdef.A.signature.type_params = 0);
+  assert (fdef.A.arg_count = 0);
+
+  (* Create the evaluation context *)
+  let ctx =
+    {
+      C.type_context = type_decls;
+      C.fun_context = fun_decls;
+      C.type_vars = T.TypeVarId.empty_vector;
+      C.env = [];
+      C.symbolic_counter = V.SymbolicValueId.generator_zero;
+      C.borrow_counter = V.BorrowId.generator_zero;
+    }
+  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
+  | Error err -> Error err
+  | Ok _ -> Ok ()