From cd754eabe3af025ca3465c5fc6d8cb48da66a1ae Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 10 Aug 2022 18:56:25 +0200 Subject: Corrected translation without using functions, remaining bug in hashmap translation --- src/ExtractToFStar.ml | 2 +- src/InterpreterBorrows.ml | 2 +- src/InterpreterStatements.ml | 17 ++++------------- src/InterpreterUtils.ml | 4 ++-- src/SymbolicAst.ml | 2 ++ src/SymbolicToPure.ml | 21 ++++++++++++++------- src/SynthesizeSymbolic.ml | 6 ++++++ src/Values.ml | 1 + 8 files changed, 31 insertions(+), 24 deletions(-) (limited to 'src') 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` *) 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 = { -- cgit v1.2.3