diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 5 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 8 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 8 | ||||
| -rw-r--r-- | src/Translate.ml | 6 | ||||
| -rw-r--r-- | tests/misc/Constants.fst | 10 |
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 |