summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/Cps.ml3
-rw-r--r--compiler/InterpreterLoops.ml97
-rw-r--r--compiler/InterpreterStatements.ml8
-rw-r--r--compiler/Logging.ml4
-rw-r--r--compiler/Print.ml8
-rw-r--r--compiler/Pure.ml38
-rw-r--r--compiler/SCC.ml9
-rw-r--r--compiler/SymbolicToPure.ml93
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