Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

1 files changed, 23 insertions, 0 deletions

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 585fa828..34310ea1 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -831,6 +831,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
 
         (* Compose and apply *)
         comp cf_eval_rvalue cf_assign cf ctx
+    | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx
     | A.FakeRead p ->
         let expand_prim_copy = false in
         let cf_prepare cf =
@@ -908,6 +909,28 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
 
+and eval_global (config : C.config) (dest : V.VarId.id)
+    (gid : LA.GlobalDeclId.id) : st_cm_fun =
+ fun cf ctx ->
+  let global = C.ctx_lookup_global_decl ctx gid in
+  let place = { E.var_id = dest; projection = [] } in
+  match config.mode with
+  | ConcreteMode ->
+      (* Treat the evaluation of the global as a call to the global body (without arguments) *)
+      (eval_local_function_call_concrete config global.body_id [] [] [] place)
+        cf ctx
+  | SymbolicMode ->
+      (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
+       * defined as equal to the value of the global (see `S.synthesize_global_eval`). *)
+      let sval =
+        mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty)
+      in
+      let cc =
+        assign_to_place config (mk_typed_value_from_symbolic_value sval) place
+      in
+      let e = cc (cf Unit) ctx in
+      S.synthesize_global_eval gid sval e
+
 (** Evaluate a switch *)
 and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
     st_cm_fun =