Corrected translation without using functions, remaining bug in hashmap translation

8 files changed, 31 insertions, 24 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index c915aede..f2c481c0 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1363,7 +1363,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
     unit =
-  assert (def.is_global_body);
+  assert (not def.is_global_body);
   (* Retrieve the function name *)
   let def_name = ctx_get_local_function def.def_id def.back_id ctx in
   (* (* Add the type parameters - note that we need those bindings only for the
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index a13ac786..6b920a51 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -436,7 +436,7 @@ let give_back_symbolic_value (_config : C.config)
   assert (sv.sv_id <> nsv.sv_id);
   (match nsv.sv_kind with
   | V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
-  | V.FunCallRet | V.SynthInput -> failwith "Unrechable");
+  | V.FunCallRet | V.SynthInput | V.Global -> failwith "Unrechable");
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 31c3aabb..48620439 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -920,19 +920,10 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i
     (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx
   | SymbolicMode ->
     (* Treat the global as a fresh symbolic value *)
-    
-    (*
-    let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in
-    (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx
-    
-    failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value";
-    *)
-
-    let rty = ety_no_regions_to_rty global.ty in
-    let sval = mk_fresh_symbolic_value V.FunCallRet rty in
-    let sval = mk_typed_value_from_symbolic_value sval in
-    (assign_to_place config sval place) (cf Unit) ctx
-    
+    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) :
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 47323cc2..6ef66f1d 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -238,8 +238,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack ->
-            ()
+        | V.SynthRetGivenBack -> ()
+        | V.Global -> ()
     end
   in
   (* We use exceptions *)
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 9cab092d..fd490e43 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -65,6 +65,8 @@ type expression =
   | Panic
   | FunCall of call * expression
   | EndAbstraction of V.abs * expression
+  | EvalGlobal of A.GlobalDeclId.id * V.symbolic_value * expression
+      (** A fresh symbolic value for the global *)
   | Expansion of mplace option * V.symbolic_value * expansion
       (** Expansion of a symbolic value.
     
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 16e48aef..81af6a8b 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -687,13 +687,7 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) :
   List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars
 
 let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
-  try (V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var) with
-    Not_found ->
-      print_endline ("Missing " ^ Print.V.show_symbolic_value sv);
-      V.SymbolicValueId.Map.iter (fun id (v : var) ->
-          print_endline (" -- " ^ (Option.value v.basename ~default:""))
-        ) ctx.sv_to_var;
-      raise Not_found
+  V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var
 
 (** Peel boxes as long as the value is of the form `Box<T>` *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
@@ -1080,6 +1074,7 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
   | Panic -> translate_panic ctx
   | FunCall (call, e) -> translate_function_call config call e ctx
   | EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx
+  | EvalGlobal (gid, sv, e) -> translate_global_eval config gid sv e ctx
   | Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx
   | Meta (meta, e) -> translate_meta config meta e ctx
 
@@ -1466,6 +1461,18 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
           mk_let monadic given_back (mk_texpression_from_var input_var) e)
         given_back_inputs next_e
 
+and translate_global_eval (config : config) (gid : A.GlobalDeclId.id)
+  (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx)
+    : texpression =
+  let (ctx, var) = fresh_var_for_symbolic_value sval ctx in
+  let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
+  let global_expr = { id = Global gid; type_args = [] } in
+  (* We use translate_fwd_ty to translate the global type *)
+  let ty = ctx_translate_fwd_ty ctx decl.ty in
+  let gval = { e = Qualif global_expr; ty } in
+  let e = translate_expression config e ctx in
+  mk_let false (mk_typed_pattern_from_var var None) gval e
+
 and translate_expansion (config : config) (p : S.mplace option)
     (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression =
   (* Translate the scrutinee *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 95da38e6..fa244649 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -114,6 +114,12 @@ let synthesize_function_call (call_id : call_id)
       in
       Some (FunCall (call, expr))
 
+let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) (expr : expression option)
+    : expression option =
+  match expr with
+  | None   -> None
+  | Some e -> Some (EvalGlobal (gid, dest, e))
+
 let synthesize_regular_function_call (fun_id : A.fun_id)
     (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
     (type_params : T.ety list) (args : V.typed_value list)
diff --git a/src/Values.ml b/src/Values.ml
index 4585b443..13cd2580 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -65,6 +65,7 @@ type sv_kind =
        *)
   | SynthInputGivenBack
       (** The value was given back upon ending one of the input abstractions *)
+  | Global (** The value is a global *)
 [@@deriving show]
 
 type symbolic_value = {