diff options
| -rw-r--r-- | compiler/Cps.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 97 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 8 | ||||
| -rw-r--r-- | compiler/Logging.ml | 4 | ||||
| -rw-r--r-- | compiler/Print.ml | 8 | ||||
| -rw-r--r-- | compiler/Pure.ml | 38 | ||||
| -rw-r--r-- | compiler/SCC.ml | 9 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 93 |
8 files changed, 175 insertions, 85 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml index 8763ff78..c0dd0ae2 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -16,7 +16,8 @@ type statement_eval_res = | Continue of int | Return | Panic - | LoopReturn (** We reached a return statement *while inside a loop* *) + | LoopReturn of V.loop_id + (** We reached a return statement *while inside a loop* *) | EndEnterLoop of V.loop_id * V.typed_value V.SymbolicValueId.Map.t (** When we enter a loop, we delegate the end of the function is synthesized with a call to the loop translation. We use this diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 82a9011c..7a72f8e3 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -1521,6 +1521,8 @@ end - to compute a mapping between the borrows and the symbolic values in a target context to the values and borrows in a source context (see {!match_ctx_with_target}). + + TODO: rename *) module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct module MkGetSetM (Id : Identifiers.Id) = struct @@ -1599,7 +1601,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct if S.check_equiv then GetSetSid.match_e S.sid_map else fun _ -> raise (Failure "Unexpected") - let match_value_with_sid (v : V.typed_value) (id : V.SymbolicValueId.id) : + let match_sid_with_value (id : V.SymbolicValueId.id) (v : V.typed_value) : unit = (* Even when we don't use it, the sids map contains the fixed ids: check that we are not trying to map a fixed id. *) @@ -1611,9 +1613,6 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct (* Add the mapping *) S.sid_to_value_map := V.SymbolicValueId.Map.add id v !S.sid_to_value_map - (* let match_sidl = GetSetSid.match_el S.sid_map *) - (* let match_sids = GetSetSid.match_es S.sid_map *) - module GetSetAid = MkGetSetM (V.AbstractionId) let match_aid = GetSetAid.match_e S.aid_map @@ -1666,9 +1665,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : V.symbolic_value = + let id0 = sv0.sv_id in let id1 = sv1.sv_id in if S.check_equiv then - let id0 = sv0.sv_id in let sv_id = match_sid id0 id1 in let sv_ty = match_rtys sv0.V.sv_ty sv1.V.sv_ty in let sv_kind = @@ -1677,7 +1676,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct { V.sv_id; sv_ty; sv_kind } else ( (* Update the binding for the target symbolic value *) - match_value_with_sid (mk_typed_value_from_symbolic_value sv0) id1; + match_sid_with_value id0 (mk_typed_value_from_symbolic_value sv1); (* Return - the returned value is not used, so we can return whatever *) sv1) @@ -1685,9 +1684,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct (v : V.typed_value) : V.typed_value = if S.check_equiv then raise Distinct else ( - assert (not left); + assert left; (* Update the binding for the target symbolic value *) - match_value_with_sid v sv.sv_id; + match_sid_with_value sv.sv_id v; (* Return - the returned value is not used, so we can return whatever *) v) @@ -2122,8 +2121,7 @@ let loop_join_origin_with_continue_ctxs (config : C.config) the values which are read or modified (some symbolic values may be ignored). *) let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) - (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : - C.eval_ctx * ids_sets * V.symbolic_value list = + (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : C.eval_ctx * ids_sets = (* The continuation for when we exit the loop - we register the environments upon loop *reentry*, and synthesize nothing by returning [None] @@ -2143,7 +2141,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) assert (i = 0); register_ctx ctx; None - | LoopReturn | EndEnterLoop _ | EndContinue _ -> + | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* We don't support nested loops for now *) raise (Failure "Nested loops are not supported for now") in @@ -2216,30 +2214,14 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; rids; sids } in fixed_ids in - let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : - V.symbolic_value list option = + let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool = let fixed_ids = compute_fixed_ids ctx1 ctx2 in let check_equivalent = true in - match match_ctxs check_equivalent fixed_ids ctx1 ctx2 with - | None -> None - | Some maps -> - (* Compute the list of symbolic value ids *) - let sidl = - List.map fst (V.SymbolicValueId.Map.bindings maps.sid_to_value_map) - in - (* Lookup the symbolic value themselves *) - let _, ids_to_values = compute_context_ids ctx1 in - let svl = - List.map - (fun sid -> - V.SymbolicValueId.Map.find sid ids_to_values.sids_to_values) - sidl - in - Some svl + Option.is_some (match_ctxs check_equivalent fixed_ids ctx1 ctx2) in let max_num_iter = Config.loop_fixed_point_max_num_iters in let rec compute_fixed_point (ctx : C.eval_ctx) (i0 : int) (i : int) : - C.eval_ctx * V.symbolic_value list = + C.eval_ctx = if i = 0 then raise (Failure @@ -2262,11 +2244,9 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) ^ "\n\n")); (* Check if we reached a fixed point: if not, iterate *) - match equiv_ctxs ctx ctx1 with - | Some svl -> (ctx1, svl) - | None -> compute_fixed_point ctx1 i0 (i - 1) + if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 i0 (i - 1) in - let fp, fp_svl = compute_fixed_point ctx0 max_num_iter max_num_iter in + let fp = compute_fixed_point ctx0 max_num_iter max_num_iter in (* Make sure we have exactly one loop abstraction per function region (merge abstractions accordingly). @@ -2323,7 +2303,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) | Break _ -> (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *) raise (Failure "Unreachable") - | Unit | LoopReturn | EndEnterLoop _ | EndContinue _ -> + | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. *) @@ -2434,22 +2414,13 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) while allowing exactly one iteration to see if it fails *) let _ = compute_fixed_point (update_kinds_can_end true fp) 1 1 in - (* Sanity check: the set of symbolic value ids is still valid *) - let _ = - let all_ids, _ = compute_context_ids fp in - let fp_sids = - V.SymbolicValueId.Set.of_list (List.map (fun sv -> sv.V.sv_id) fp_svl) - in - assert (V.SymbolicValueId.Set.subset fp_sids all_ids.sids) - in - (* Return *) fp in let fixed_ids = compute_fixed_ids (Option.get !ctx_upon_entry) fp in (* Return *) - (fp, fixed_ids, fp_svl) + (fp, fixed_ids) (** Split an environment between the fixed abstractions, values, etc. and the new abstractions, values, etc. @@ -3117,6 +3088,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) (** Evaluate a loop in concrete mode *) let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> + (* We need a loop id for the [LoopReturn]. In practice it won't be used + (it is useful only for the symbolic execution *) + let loop_id = C.fresh_loop_id () in (* Continuation for after we evaluate the loop body: depending the result of doing one loop iteration: - redoes a loop iteration @@ -3129,7 +3103,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = *) let rec reeval_loop_body (res : statement_eval_res) : m_fun = match res with - | Return -> cf LoopReturn + | Return -> cf (LoopReturn loop_id) | Panic -> cf Panic | Break i -> (* Break out of the loop by calling the continuation *) @@ -3150,7 +3124,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = * We prefer to write it this way for consistency and sanity, * though. *) raise (Failure "Unreachable") - | LoopReturn | EndEnterLoop _ | EndContinue _ -> + | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* We can't get there: this is only used in symbolic mode *) raise (Failure "Unreachable") in @@ -3169,7 +3143,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : (* Compute a fresh loop id *) let loop_id = C.fresh_loop_id () in (* Compute the fixed point at the loop entrance *) - let fp_ctx, fixed_ids, input_svalues = + let fp_ctx, fixed_ids = compute_loop_entry_fixed_point config loop_id eval_loop_body ctx in @@ -3210,7 +3184,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : fp_ctx in cc cf ctx - | Unit | LoopReturn | EndEnterLoop _ | EndContinue _ -> + | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. *) @@ -3219,14 +3193,29 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : let loop_expr = eval_loop_body cf_loop fp_ctx in (* Compute the list of fresh symbolic values *) - let fresh_sids = - let input_sids = - V.SymbolicValueId.Set.of_list - (List.map (fun sv -> sv.V.sv_id) input_svalues) + let fresh_sids, input_svalues = + let old_ids, _ = compute_context_ids ctx in + let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in + let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in + (* The value ids should be listed in increasing order *) + let input_svalues = + List.map + (fun sid -> V.SymbolicValueId.Map.find sid fp_ids_maps.sids_to_values) + (V.SymbolicValueId.Set.elements fresh_sids) in - V.SymbolicValueId.Set.diff input_sids fixed_ids.sids + (fresh_sids, input_svalues) in + log#ldebug + (lazy + ("eval_loop_symbolic: result:" ^ "\n- src context:\n" + ^ eval_ctx_to_string ctx ^ "\n- fixed point:\n" ^ eval_ctx_to_string fp_ctx + ^ "\n- fixed_sids: " + ^ V.SymbolicValueId.Set.show fixed_ids.sids + ^ "\n- input_svalues: " + ^ V.SymbolicValueId.Set.show fresh_sids + ^ "\n\n")); + (* Put together *) S.synthesize_loop loop_id input_svalues fresh_sids end_expr loop_expr diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 7e4722b8..fe508f6b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -851,8 +851,8 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Evaluation successful: evaluate the second statement *) | Unit -> eval_statement config st2 cf (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Panic | Break _ | Continue _ | Return | LoopReturn | EndEnterLoop _ - | EndContinue _ -> + | Panic | Break _ | Continue _ | Return | LoopReturn _ + | EndEnterLoop _ | EndContinue _ -> cf res in (* Compose and apply *) @@ -1100,8 +1100,8 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (* Pop the stack frame, retrieve the return value, move it to * its destination and continue *) pop_frame_assign config dest (cf Unit) - | Break _ | Continue _ | Unit | LoopReturn | EndEnterLoop _ | EndContinue _ - -> + | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ + | EndContinue _ -> raise (Failure "Unreachable") in let cc = comp cc cf_finish in diff --git a/compiler/Logging.ml b/compiler/Logging.ml index 71f72471..706ea5cb 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -49,7 +49,7 @@ let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows" let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants" (** Logger for SCC *) -let scc_log = L.get_logger "MainLogger.SCC" +let scc_log = L.get_logger "MainLogger.Graph.SCC" (** Logger for ReorderDecls *) -let reorder_decls_log = L.get_logger "MainLogger.ReorderDecls" +let reorder_decls_log = L.get_logger "MainLogger.Graph.ReorderDecls" diff --git a/compiler/Print.ml b/compiler/Print.ml index 82c5dac5..e2bc3777 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -486,8 +486,8 @@ module Contexts = struct let frames = split_aux [] [] env in frames - let eval_ctx_to_string_gen (filter : bool) (ctx : C.eval_ctx) : string = - let fmt = eval_ctx_to_ctx_formatter ctx in + let fmt_eval_ctx_to_string_gen (fmt : ctx_formatter) (filter : bool) + (ctx : C.eval_ctx) : string = let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in let frames = split_env_according_to_frames ctx.env in let num_frames = List.length frames in @@ -515,6 +515,10 @@ module Contexts = struct "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames + let eval_ctx_to_string_gen (filter : bool) (ctx : C.eval_ctx) : string = + let fmt = eval_ctx_to_ctx_formatter ctx in + fmt_eval_ctx_to_string_gen fmt filter ctx + let eval_ctx_to_string (ctx : C.eval_ctx) : string = eval_ctx_to_string_gen true ctx diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 10ce876f..6fb20b22 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -567,6 +567,7 @@ type fun_effect_info = { is_rec : bool; (** [true] if the function is recursive (or in a mutually recursive group) *) } +[@@deriving show] (** Meta information about a function signature *) type fun_sig_info = { @@ -585,6 +586,7 @@ type fun_sig_info = { with the state (if there is one) *) effect_info : fun_effect_info; } +[@@deriving show] (** A function signature. @@ -600,7 +602,7 @@ type fun_sig_info = { [in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state -> result (state & (back_out0 & ... & back_outp))] (* state-error *) - Note that a stateful backward function takes two states as inputs: the + Note that a stateful backward function may take two states as inputs: the state received by the associated forward function, and the state at which the backward is called. This leads to code of the following shape: @@ -611,7 +613,7 @@ type fun_sig_info = { ]} The function's type should be given by [mk_arrows sig.inputs sig.output]. - We provide additional meta-information: + We provide additional meta-information with {!fun_sig.info}: - we divide between forward inputs and backward inputs (i.e., inputs specific to the forward functions, and additional inputs necessary if the signature is for a backward function) @@ -622,7 +624,32 @@ type fun_sig_info = { type fun_sig = { type_params : type_var list; inputs : ty list; + (** The input types. + + Note that those input types take into account the [fuel] parameter, + if the function uses fuel for termination, and the [state] parameter, + if the function is stateful. + + For instance, if we have the following Rust function: + {[ + fn f(x : int); + ]} + + If we translate it to a stateful function which uses fuel we get: + {[ + val f : nat -> int -> state -> result (state * unit); + ]} + + In particular, the list of input types is: [[nat; int; state]]. + *) output : ty; + (** The output type. + + Note that this type contains the "effect" of the function (i.e., it is + not just a purification of the Rust return type). For instance, it will + be a tuple with a [state] if the function is stateful, and will be wrapped + in a [result] if the function can fail. + *) doutputs : ty list; (** The "decomposed" list of outputs. @@ -641,9 +668,13 @@ type fun_sig = { - forward function: [[T]] - backward function: [[T; T]] (for "x" and "y") + Non-decomposed ouputs (if the function can fail, but is not stateful): + - [result T] + - [[result (T * T)] *) info : fun_sig_info; (** Additional information *) } +[@@deriving show] (** An instantiated function signature. See {!fun_sig} *) type inst_fun_sig = { @@ -652,6 +683,7 @@ type inst_fun_sig = { doutputs : ty list; info : fun_sig_info; } +[@@deriving show] type fun_body = { inputs : var list; @@ -660,6 +692,7 @@ type fun_body = { to replace unused variables by [_] *) body : texpression; } +[@@deriving show] type fun_decl = { def_id : FunDeclId.id; @@ -681,3 +714,4 @@ type fun_decl = { is_global_decl_body : bool; body : fun_body option; } +[@@deriving show] diff --git a/compiler/SCC.ml b/compiler/SCC.ml index 2095c350..d9a4cd3e 100644 --- a/compiler/SCC.ml +++ b/compiler/SCC.ml @@ -94,15 +94,6 @@ module Make (Id : OrderedType) = struct *) let reorder_sccs (id_deps : Id.t list IdMap.t) (ids : Id.t list) (sccs : Id.t list list) : sccs = - log#ldebug - (lazy - ("reorder_sccs:" ^ "\n- id_deps: " - ^ IdMap.show (Print.list_to_string Id.show_t) id_deps - ^ "\n- ids: " - ^ Print.list_to_string Id.show_t ids - ^ "\n- sccs: " - ^ Print.list_to_string (Print.list_to_string Id.show_t) sccs)); - (* Map the identifiers to the SCC indices *) let id_to_scc = IdMap.of_list diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 006fdda7..f06e6542 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -9,6 +9,7 @@ module TA = TypesAnalysis module L = Logging module PP = PrintPure module FA = FunsAnalysis +module IU = InterpreterUtils (** The local logger *) let log = L.symbolic_to_pure_log @@ -23,6 +24,7 @@ type type_context = { *) types_infos : TA.type_infos; (* TODO: rename to type_infos *) } +[@@deriving show] type fun_sig_named_outputs = { sg : fun_sig; (** A function signature *) @@ -37,14 +39,17 @@ type fun_sig_named_outputs = { which case we use those names). *) } +[@@deriving show] type fun_context = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *) fun_infos : FA.fun_info A.FunDeclId.Map.t; } +[@@deriving show] type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t } +[@@deriving show] (** Whenever we translate a function call or an ended abstraction, we store the related information (this is useful when translating ended @@ -64,6 +69,7 @@ type call_info = { TODO: remove? it is also in the bs_ctx ("abstractions" field) *) } +[@@deriving show] (** Contains information about a loop we entered. @@ -101,9 +107,10 @@ type loop_info = { type_args : ty list; forward_inputs : texpression list option; (** The forward inputs are initialized at [None] *) - forward_output_no_state : var option; + forward_output_no_state_no_result : var option; (** The forward outputs are initialized at [None] *) } +[@@deriving show] (** Body synthesis context *) type bs_ctx = { @@ -179,6 +186,7 @@ type bs_ctx = { AST in a single function. *) } +[@@deriving show] let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit = let env = VarId.Map.empty in @@ -209,6 +217,22 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter = ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls ctx.fun_decl +let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter = + let rvar_to_string = Print.Types.region_var_id_to_string in + let r_to_string = Print.Types.region_id_to_string in + let type_var_id_to_string = Print.Types.type_var_id_to_string in + let var_id_to_string = Print.Expressions.var_id_to_string in + let ast_fmt = bs_ctx_to_ast_formatter ctx in + { + Print.Values.rvar_to_string; + r_to_string; + type_var_id_to_string; + type_decl_id_to_string = ast_fmt.type_decl_id_to_string; + adt_variant_to_string = ast_fmt.adt_variant_to_string; + var_id_to_string; + adt_field_names = ast_fmt.adt_field_names; + } + let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = let type_params = ctx.fun_decl.signature.type_params in let type_decls = ctx.type_context.llbc_type_decls in @@ -216,6 +240,11 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = let global_decls = ctx.global_context.llbc_global_decls in PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params +let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = + let fmt = bs_ctx_to_ctx_formatter ctx in + let fmt = Print.PC.ctx_to_rtype_formatter fmt in + Print.PV.symbolic_value_to_string fmt sv + let ty_to_string (ctx : bs_ctx) (ty : ty) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in let fmt = PrintPure.ast_to_type_formatter fmt in @@ -843,7 +872,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 + match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with + | Some v -> v + | None -> + raise + (Failure + ("Could not find var for symbolic value: " + ^ V.SymbolicValueId.to_string sv.sv_id)) (** 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 = @@ -1319,7 +1354,8 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) match ctx.bid with | None -> (* Forward *) - mk_texpression_from_var (Option.get loop_info.forward_output_no_state) + mk_texpression_from_var + (Option.get loop_info.forward_output_no_state_no_result) | Some bid -> (* Backward *) (* Group the variables in which we stored the values we need to give back. @@ -1478,12 +1514,17 @@ and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs) | V.FunCall (call_id, rg_id) -> translate_end_abstraction_fun_call ectx abs e ctx call_id rg_id | V.SynthRet rg_id -> translate_end_abstraction_synth_ret ectx abs e ctx rg_id - | Loop (loop_id, rg_id, abs_kind) -> + | V.Loop (loop_id, rg_id, abs_kind) -> translate_end_abstraction_loop ectx abs e ctx loop_id rg_id abs_kind and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = + log#ldebug + (lazy + ("translate_end_abstraction_synth_input:" ^ "\n- eval_ctx:\n" + ^ IU.eval_ctx_to_string ectx ^ "\n- abs:\n" ^ IU.abs_to_string ectx abs + ^ "\n")); (* When we end an input abstraction, this input abstraction gets back * the borrows which it introduced in the context through the input * values: by listing those values, we get the values which are given @@ -1763,7 +1804,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) ([ back_state ], ctx, Some nstate) else ([], ctx, None) in - (* Concatenate all the inpus *) + (* Concatenate all the inputs *) let inputs = List.concat [ fwd_inputs; back_inputs; back_state ] in (* Retrieve the values given back by this function *) let ctx, outputs = abs_to_given_back None abs ctx in @@ -2057,12 +2098,11 @@ and translate_forward_end (ectx : C.eval_ctx) translate_expression e ctx in - (* If we entered/are entering a loop, we need to introduce a call to the + (* If we are (re-)entering a loop, we need to introduce a call to the forward translation of the loop. *) match loop_input_values with | None -> - (* "Regular" case: not a loop *) - assert (ctx.loop_id = None); + (* "Regular" case: we reached a return *) translate_end ctx | Some loop_input_values -> (* Loop *) @@ -2089,7 +2129,7 @@ and translate_forward_end (ectx : C.eval_ctx) (* Introduce a fresh output value for the forward function *) let ctx, output_var = - let output_ty = ctx.sg.output in + let output_ty = mk_simpl_tuple_ty ctx.sg.doutputs in fresh_var None output_ty ctx in let args, ctx, out_pats = @@ -2116,7 +2156,7 @@ and translate_forward_end (ectx : C.eval_ctx) { loop_info with forward_inputs = Some args; - forward_output_no_state = Some output_var; + forward_output_no_state_no_result = Some output_var; } in let ctx = @@ -2145,6 +2185,33 @@ and translate_forward_end (ectx : C.eval_ctx) and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in + (* Translate the loop inputs - some inputs are symbolic values already + in the context, some inputs are introduced by the loop fixed point: + we need to introduce fresh variables for those. *) + (* First introduce fresh variables for the new inputs *) + let ctx = + (* We have to filter the list of symbolic values, to remove the not fresh ones *) + let svl = + List.filter + (fun (sv : V.symbolic_value) -> + V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues) + loop.input_svalues + in + log#ldebug + (lazy + ("translate_loop:" ^ "\n- filtered svl: " + ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl)); + let ctx, _ = fresh_vars_for_symbolic_values svl ctx in + ctx + in + + (* Sanity check: all the non-fresh symbolic values are in the context *) + assert ( + List.for_all + (fun (sv : V.symbolic_value) -> + V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var) + loop.input_svalues); + (* Translate the loop inputs *) let inputs = List.map @@ -2172,7 +2239,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = input_svl = loop.input_svalues; type_args; forward_inputs = None; - forward_output_no_state = None; + forward_output_no_state_no_result = None; } in let loops = LoopId.Map.add loop_id loop_info ctx.loops in @@ -2196,6 +2263,10 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues) loop.input_svalues in + log#ldebug + (lazy + ("translate_loop:" ^ "\n- filtered svl: " + ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl)); let ctx_loop, _ = fresh_vars_for_symbolic_values svl ctx_loop in ctx_loop in |