Register global names, one error remaining

5 files changed, 33 insertions, 4 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a2b15ece..c915aede 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -794,6 +794,11 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
   (* Return *)
   ctx
 
+(** Simply add the global name to the context. *)
+let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl)
+    : extraction_ctx =
+  ctx_add_global_decl def ctx
+
 (** The following function factorizes the extraction of ADT values.
 
     Note that patterns can introduce new variables: we thus return an extraction
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index ffc47741..31c3aabb 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -919,16 +919,20 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i
     (* Treat the global as a function without arguments to call *)
     (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";
-    (* Treat the global as a fresh 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
+    
 
 (** Evaluate a switch *)
 and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 83cce3e9..16e48aef 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -687,7 +687,13 @@ 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 =
-  V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_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
 
 (** 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 =
diff --git a/src/Translate.ml b/src/Translate.ml
index a936d626..fdd6d05f 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -655,7 +655,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
             m.declarations))
   in
 
-  (* Register unique names for all the top-level types and functions.
+  (* Register unique names for all the top-level types, functions and globals.
    * Note that the order in which we generate the names doesn't matter:
    * we just need to generate a mapping from identifier to name, and make
    * sure there are no name clashes. *)
@@ -677,6 +677,10 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       ctx trans_funs
   in
 
+  let ctx = List.fold_left
+    ExtractToFStar.extract_global_decl_register_names ctx m.globals
+  in
+
   (* Open the output file *)
   (* First compute the filename by replacing the extension and converting the
    * case (rust module names are snake case) *)
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index e1a942a0..f5bd41cb 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -4,3 +4,13 @@ module Constants
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [constants::X0] *)
+let x0_body : result u32 = Return 0
+let x0_c : u32 = eval_global x0_body
+
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
+(** [constants::X1] *)
\ No newline at end of file