summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml12
-rw-r--r--compiler/Cps.ml10
-rw-r--r--compiler/Interpreter.ml174
-rw-r--r--compiler/InterpreterLoops.ml145
-rw-r--r--compiler/InterpreterStatements.ml39
-rw-r--r--compiler/InterpreterStatements.mli5
-rw-r--r--compiler/InterpreterUtils.ml1
-rw-r--r--compiler/SymbolicAst.ml10
-rw-r--r--compiler/SymbolicToPure.ml3
-rw-r--r--compiler/SynthesizeSymbolic.ml11
-rw-r--r--compiler/Values.ml5
-rw-r--r--compiler/ValuesUtils.ml7
12 files changed, 293 insertions, 129 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 55baa6a4..3d09b58a 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -405,16 +405,19 @@ let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in
ctx_push_vars ctx vars
-let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
+let env_find_abs (env : env) (pred : V.abs -> bool) : V.abs option =
let rec lookup env =
match env with
- | [] -> raise (Failure "Unexpected")
+ | [] -> None
| Var (_, _) :: env' -> lookup env'
- | Abs abs :: env' -> if abs.abs_id = abs_id then abs else lookup env'
+ | Abs abs :: env' -> if pred abs then Some abs else lookup env'
| Frame :: env' -> lookup env'
in
lookup env
+let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
+ Option.get (env_find_abs env (fun abs -> abs.abs_id = abs_id))
+
(** Remove an abstraction from the context, as well as all the references to
this abstraction (for instance, remove the abs id from all the parent sets
of all the other abstractions).
@@ -473,6 +476,9 @@ let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
env_lookup_abs ctx.env abs_id
+let ctx_find_abs (ctx : eval_ctx) (p : V.abs -> bool) : V.abs option =
+ env_find_abs ctx.env p
+
(** See the comments for {!env_remove_abs} *)
let ctx_remove_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) :
eval_ctx * V.abs option =
diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index dc51c614..a013003e 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -16,16 +16,22 @@ type statement_eval_res =
| Continue of int
| Return
| Panic
- | EndEnterLoop
+ | LoopReturn (** We reached a return statement *while inside a loop* *)
+ | EndEnterLoop of V.typed_value list
(** When we enter a loop, we delegate the end of the function is
synthesized with a call to the loop translation. We use this
evaluation result to transmit the fact that we end evaluation
because we entered a loop.
+
+ We provide the list of values for the translated loop function call.
*)
- | EndContinue
+ | EndContinue of V.typed_value list
(** For loop translations: we end with a continue (i.e., a recursive call
to the translation for the loop body).
+
+ We provide the list of values for the translated loop function call.
*)
+[@@deriving show]
type eval_result = SA.expression option
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 4b030088..7a85461e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -124,10 +124,16 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
reaching the [return] instruction when synthesizing a *backward* function:
this continuation takes care of doing the proper manipulations to finish
the synthesis (mostly by ending abstractions).
+
+ [entered_loop]: [true] if we reached the end of the function because we
+ (re-)entered a loop (results [EndEnterLoop] and [EndContinue]).
+
+ [inside_loop]: [true] if we are *inside* a loop (result [EndContinue]).
*)
let evaluate_function_symbolic_synthesize_backward_from_return
(config : C.config) (fdef : A.fun_decl) (inst_sg : A.inst_fun_sig)
- (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx) : SA.expression option =
+ (back_id : T.RegionGroupId.id) (entered_loop : bool) (inside_loop : bool)
+ (ctx : C.eval_ctx) : SA.expression option =
(* We need to instantiate the function signature - to retrieve
* the return type. Note that it is important to re-generate
* an instantiation of the signature, so that we use fresh
@@ -137,7 +143,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return
let ret_inst_sg = instantiate_fun_sig type_params sg in
let ret_rty = ret_inst_sg.output in
(* Move the return value out of the return variable *)
- let cf_pop_frame = pop_frame config in
+ let pop_return_value = not entered_loop in
+ let cf_pop_frame = pop_frame config pop_return_value in
(* We need to find the parents regions/abstractions of the region we
* will end - this will allow us to, first, mark the other return
@@ -156,30 +163,57 @@ let evaluate_function_symbolic_synthesize_backward_from_return
(* Insert the return value in the return abstractions (by applying
* borrow projections) *)
- let cf_consume_ret ret_value ctx =
- let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) :
- C.eval_ctx * V.typed_avalue list =
- let ctx, avalue =
- apply_proj_borrows_on_input_value config ctx abs.regions
- abs.ancestors_regions ret_value ret_rty
- in
- (ctx, [ avalue ])
+ let cf_consume_ret (ret_value : V.typed_value option) ctx =
+ let ctx =
+ if not entered_loop then (
+ let ret_value = Option.get ret_value in
+ let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) :
+ C.eval_ctx * V.typed_avalue list =
+ let ctx, avalue =
+ apply_proj_borrows_on_input_value config ctx abs.regions
+ abs.ancestors_regions ret_value ret_rty
+ in
+ (ctx, [ avalue ])
+ in
+
+ (* Initialize and insert the abstractions in the context.
+ *
+ * We take care of allowing to end only the regions which should end (note
+ * that this is important for soundness: this is part of the borrow checking).
+ * Also see the documentation of the [can_end] field of [abs] for more
+ * information. *)
+ let parent_and_current_rgs =
+ T.RegionGroupId.Set.add back_id parent_rgs
+ in
+ let region_can_end rid =
+ T.RegionGroupId.Set.mem rid parent_and_current_rgs
+ in
+ assert (region_can_end back_id);
+ let ctx =
+ create_push_abstractions_from_abs_region_groups
+ (fun rg_id -> V.SynthRet rg_id)
+ ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues
+ ctx
+ in
+ ctx)
+ else ctx
in
- (* Initialize and insert the abstractions in the context.
- *
- * We take care of disallowing ending the return regions which we
- * shouldn't end (see the documentation of the [can_end] field of [abs]
- * for more information. *)
- let parent_and_current_rgs = T.RegionGroupId.Set.add back_id parent_rgs in
- let region_can_end rid =
- T.RegionGroupId.Set.mem rid parent_and_current_rgs
- in
- assert (region_can_end back_id);
+ (* Set the proper loop abstractions as endable *)
let ctx =
- create_push_abstractions_from_abs_region_groups
- (fun rg_id -> V.SynthRet rg_id)
- ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
+ let visit_loop_abs =
+ object
+ inherit [_] C.map_eval_ctx
+
+ method! visit_abs _ abs =
+ match abs.kind with
+ | V.Loop (_, rg_id', _) ->
+ let rg_id' = Option.get rg_id' in
+ if rg_id' = back_id then { abs with can_end = true } else abs
+ | _ -> abs
+ end
+ in
+ visit_loop_abs#visit_eval_ctx () ctx
in
(* We now need to end the proper *input* abstractions - pay attention
@@ -190,9 +224,29 @@ let evaluate_function_symbolic_synthesize_backward_from_return
(* End the parent abstractions and the current abstraction - note that we
* end them in an order which follows the regions hierarchy: it should lead
* to generated code which has a better consistency between the parent
- * and children backward functions *)
+ * and children backward functions.
+ *
+ * Note that we don't end the same abstraction if we are *inside* a loop (i.e.,
+ * we are evaluating an [EndContinue]) or not.
+ *)
let current_abs_id =
- (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
+ if not inside_loop then
+ (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
+ else
+ let pred (abs : V.abs) =
+ match abs.kind with
+ | V.Loop (_, rg_id', kind) ->
+ let rg_id' = Option.get rg_id' in
+ let is_ret =
+ match kind with
+ | V.LoopSynthInput -> true
+ | V.LoopSynthRet -> false
+ in
+ rg_id' = back_id && is_ret
+ | _ -> false
+ in
+ let abs = Option.get (C.ctx_find_abs ctx pred) in
+ abs.abs_id
in
let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
let cf_end_target_abs cf =
@@ -231,8 +285,13 @@ let evaluate_function_symbolic (synthesize : bool)
(* Create the continuation to finish the evaluation *)
let config = C.mk_config C.SymbolicMode in
let cf_finish res ctx =
+ log#ldebug
+ (lazy
+ ("evaluate_function_symbolic: cf_finish: "
+ ^ Cps.show_statement_eval_res res));
+
match res with
- | Return ->
+ | Return | LoopReturn ->
if synthesize then
(* We have to "play different endings":
* - one execution for the forward function
@@ -248,10 +307,11 @@ let evaluate_function_symbolic (synthesize : bool)
(* Forward translation: retrieve the returned value *)
let fwd_e =
(* Pop the frame and retrieve the returned value at the same time*)
- let cf_pop = pop_frame config in
+ let pop_return_value = true in
+ let cf_pop = pop_frame config pop_return_value in
(* Generate the Return node *)
let cf_return ret_value : m_fun =
- fun ctx -> Some (SA.Return (ctx, Some ret_value))
+ fun ctx -> Some (SA.Return (ctx, ret_value))
in
(* Apply *)
cf_pop cf_return ctx
@@ -261,10 +321,59 @@ let evaluate_function_symbolic (synthesize : bool)
abstractions to consume the return value, then end all the
abstractions up to the one in which we are interested.
*)
+ let entered_loop = false in
+ let inside_loop =
+ match res with
+ | Return -> false
+ | LoopReturn -> true
+ | _ -> raise (Failure "Unreachable")
+ in
+ let finish_back_eval back_id =
+ Option.get
+ (evaluate_function_symbolic_synthesize_backward_from_return config
+ fdef inst_sg back_id entered_loop inside_loop ctx)
+ in
+ let back_el =
+ T.RegionGroupId.mapi
+ (fun gid _ -> (gid, finish_back_eval gid))
+ fdef.signature.regions_hierarchy
+ in
+ let back_el = T.RegionGroupId.Map.of_list back_el in
+ (* Put everything together *)
+ S.synthesize_forward_end None fwd_e back_el
+ else None
+ | EndEnterLoop loop_input_values | EndContinue loop_input_values ->
+ (* Similar to [Return]: we have to play different endings *)
+ if synthesize then
+ (* Forward translation *)
+ let fwd_e =
+ (* Pop the frame - there is no returned value to pop: in the
+ translation we will simply call the loop function *)
+ let pop_return_value = false in
+ let cf_pop = pop_frame config pop_return_value in
+ (* Generate the Return node *)
+ let cf_return _ret_value : m_fun =
+ fun ctx -> Some (SA.Return (ctx, None))
+ in
+ (* Apply *)
+ cf_pop cf_return ctx
+ in
+ let fwd_e = Option.get fwd_e in
+ (* Backward translation: introduce "return"
+ abstractions to consume the return value, then end all the
+ abstractions up to the one in which we are interested.
+ *)
+ let entered_loop = true in
+ let inside_loop =
+ match res with
+ | EndEnterLoop _ -> false
+ | EndContinue _ -> true
+ | _ -> raise (Failure "Unreachable")
+ in
let finish_back_eval back_id =
Option.get
(evaluate_function_symbolic_synthesize_backward_from_return config
- fdef inst_sg back_id ctx)
+ fdef inst_sg back_id entered_loop inside_loop ctx)
in
let back_el =
T.RegionGroupId.mapi
@@ -273,10 +382,8 @@ let evaluate_function_symbolic (synthesize : bool)
in
let back_el = T.RegionGroupId.Map.of_list back_el in
(* Put everything together *)
- S.synthesize_forward_end fwd_e back_el
+ S.synthesize_forward_end (Some loop_input_values) fwd_e back_el
else None
- | EndEnterLoop -> raise (Failure "Unimplemented")
- | EndContinue -> raise (Failure "Unimplemented")
| Panic ->
(* Note that as we explore all the execution branches, one of
* the executions can lead to a panic *)
@@ -329,7 +436,8 @@ module Test = struct
match res with
| Return ->
(* Ok: drop the local variables and finish *)
- pop_frame config (fun _ _ -> None) ctx
+ let pop_return_value = true in
+ pop_frame config pop_return_value (fun _ _ -> None) ctx
| _ ->
raise
(Failure
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index e68790d4..48292968 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -245,7 +245,7 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
(** Destructure all the new abstractions *)
let destructure_new_abs (loop_id : V.LoopId.id)
(old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
- let abs_kind = V.Loop (loop_id, None) in
+ let abs_kind = V.Loop (loop_id, None, V.LoopSynthInput) in
let can_end = false in
let destructure_shared_values = true in
let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
@@ -336,7 +336,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
- let abs_kind = V.Loop (loop_id, None) in
+ let abs_kind = V.Loop (loop_id, None, LoopSynthInput) in
let can_end = false in
let destructure_shared_values = true in
let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
@@ -966,7 +966,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
let abs =
{
V.abs_id = C.fresh_abstraction_id ();
- kind = V.Loop (S.loop_id, None);
+ kind = V.Loop (S.loop_id, None, LoopSynthInput);
can_end = false;
parents = V.AbstractionId.Set.empty;
original_parents = [];
@@ -1020,7 +1020,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
let abs =
{
V.abs_id = C.fresh_abstraction_id ();
- kind = V.Loop (S.loop_id, None);
+ kind = V.Loop (S.loop_id, None, LoopSynthInput);
can_end = false;
parents = V.AbstractionId.Set.empty;
original_parents = [];
@@ -1124,7 +1124,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
else raise (ValueMatchFailure (LoanInRight id)))
| None ->
(* Convert the value to an abstraction *)
- let abs_kind = V.Loop (S.loop_id, None) in
+ let abs_kind = V.Loop (S.loop_id, None, LoopSynthInput) in
let can_end = false in
let destructure_shared_values = true in
let absl =
@@ -1691,9 +1691,16 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
(* Return - the returned value is not used, so we can return whatever *)
v)
- let match_bottom_with_other (_left : bool) (_v : V.typed_value) :
- V.typed_value =
- raise Distinct
+ let match_bottom_with_other (left : bool) (v : V.typed_value) : V.typed_value
+ =
+ (* It can happen that some variables get initialized in some branches
+ and not in some others, which causes problems when matching. *)
+ (* TODO: the returned value is not used, while it should: in generality it
+ should be ok to match a fixed-point with the environment we get at
+ a continue, where the fixed point contains some bottom values. *)
+ if left && not (value_has_loans_or_borrows S.ctx v.V.value) then
+ mk_bottom v.V.ty
+ else raise Distinct
let match_distinct_aadts _ _ _ _ _ = raise Distinct
@@ -2131,7 +2138,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
assert (i = 0);
register_ctx ctx;
None
- | EndEnterLoop | EndContinue ->
+ | LoopReturn | EndEnterLoop _ | EndContinue _ ->
(* We don't support nested loops for now *)
raise (Failure "Nested loops are not supported for now")
in
@@ -2246,15 +2253,16 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
let list_loop_abstractions =
object
- inherit [_] C.map_eval_ctx as super
+ inherit [_] C.map_eval_ctx
- method! visit_abs env abs =
+ method! visit_abs _ abs =
match abs.kind with
- | Loop (loop_id', _) ->
+ | Loop (loop_id', _, kind) ->
assert (loop_id' = loop_id);
+ assert (kind = V.LoopSynthInput);
add_aid abs.abs_id;
{ abs with can_end = true }
- | _ -> super#visit_abs env abs
+ | _ -> abs
end
in
let fp = list_loop_abstractions#visit_eval_ctx () fp in
@@ -2285,7 +2293,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 | 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.
*)
@@ -2349,7 +2357,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
| id0 :: ids ->
let id0 = ref id0 in
(* Add the proper region group into the abstraction *)
- let abs_kind = V.Loop (loop_id, Some rg_id) in
+ let abs_kind = V.Loop (loop_id, Some rg_id, V.LoopSynthInput) in
let abs = C.ctx_lookup_abs !fp !id0 in
let abs = { abs with V.kind = abs_kind } in
let fp', _ = C.ctx_subst_abs !fp !id0 abs in
@@ -2372,17 +2380,19 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* Reset the loop abstracions as not endable *)
let list_loop_abstractions (remove_rg_id : bool) =
object
- inherit [_] C.map_eval_ctx as super
+ inherit [_] C.map_eval_ctx
- method! visit_abs env abs =
+ method! visit_abs _ abs =
match abs.kind with
- | Loop (loop_id', _) ->
+ | Loop (loop_id', _, kind) ->
assert (loop_id' = loop_id);
+ assert (kind = V.LoopSynthInput);
let kind =
- if remove_rg_id then V.Loop (loop_id, None) else abs.kind
+ if remove_rg_id then V.Loop (loop_id, None, V.LoopSynthInput)
+ else abs.kind
in
{ abs with can_end = false; kind }
- | _ -> super#visit_abs env abs
+ | _ -> abs
end
in
let update_kinds_can_end (remove_rg_id : bool) ctx =
@@ -2402,38 +2412,6 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* Return *)
(fp, fixed_ids)
-(*
-(** Introduce region groups in the loop abstractions.
-
- Initially, the new abstractions in the fixed-point have no region group.
- We want each one of them to have a unique region group (because we will
- translate each one of those abstractions to a pair forward
- function/backward function).
- *)
-let ctx_add_loop_region_groups (loop_id : V.LoopId.id) (fp : C.eval_ctx) :
- C.eval_ctx =
- let _, fresh_rid = T.RegionGroupId.fresh_stateful_generator () in
-
- let introduce_fresh_rids =
- object
- inherit [_] C.map_eval_ctx
-
- method! visit_abs _ abs =
- match abs.kind with
- | Loop (loop_id', rg_id) ->
- assert (loop_id' = loop_id);
- assert (rg_id = None);
- let rg_id = Some (fresh_rid ()) in
- let kind = V.Loop (loop_id, rg_id) in
- { abs with V.kind }
- | _ -> abs
- end
- in
- let fp_env = List.rev (introduce_fresh_rids#visit_env () (List.rev fp.env)) in
- let fp = { fp with env = fp_env } in
- fp
- *)
-
(** Split an environment between the fixed abstractions, values, etc. and
the new abstractions, values, etc.
@@ -2452,7 +2430,7 @@ let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : C.eval_ctx) :
let is_fresh (ee : C.env_elem) : bool =
match ee with
| C.Var (VarBinder _, _) | C.Frame -> false
- | C.Var (DummyBinder bv, _) -> not (is_fresh_did bv)
+ | C.Var (DummyBinder bv, _) -> is_fresh_did bv
| C.Abs abs -> is_fresh_abs_id abs.abs_id
in
let new_eel, filt_env = List.partition is_fresh ctx.env in
@@ -2785,6 +2763,11 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
values, if they contain borrows - above i points to [s@7], but it should
be a different symbolic value...).
+ Finally, we use the map from symbolic values to values to compute the list of
+ input values of the loop: we simply list the values, by order of increasing
+ symbolic value id. We *do* use the fixed values (though they are in the frame)
+ because they may be *read* inside the loop.
+
We can then proceed to finishing the symbolic execution and doing the
synthesis.
@@ -2799,8 +2782,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
(* Debug *)
log#ldebug
(lazy
- ("match_ctx_with_target:\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx
- ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx));
+ ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
+ ^ "\n\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
+ ^ eval_ctx_to_string tgt_ctx));
(* We first reorganize [src_ctx] so that we can match it with [tgt_ctx] *)
let rec cf_reorganize_src : cm_fun =
@@ -2810,6 +2794,14 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in
let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in
+ log#ldebug
+ (lazy
+ ("match_ctx_with_target:\n" ^ "\n- fixed_ids: "
+ ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx: "
+ ^ env_to_string src_ctx filt_src_env
+ ^ "\n- filt_tgt_ctx: "
+ ^ env_to_string tgt_ctx filt_tgt_env));
+
(* Remove the abstractions *)
let filter (ee : C.env_elem) : bool =
match ee with Var _ -> true | Abs _ | Frame -> false
@@ -3010,7 +3002,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
in
let visit_tgt =
object
- inherit [_] C.map_eval_ctx
+ inherit [_] C.map_eval_ctx as super
method! visit_borrow_id _ bid =
(* Lookup the id of the loan corresponding to this borrow *)
@@ -3032,6 +3024,17 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id ()
method! visit_abstraction_id _ _ = C.fresh_abstraction_id ()
method! visit_region_id _ id = get_rid id
+
+ (** We also need to change the abstraction kind *)
+ method! visit_abs env abs =
+ match abs.kind with
+ | V.Loop (loop_id', rg_id, kind) ->
+ assert (loop_id' = loop_id);
+ assert (kind = V.LoopSynthInput);
+ let kind = V.Loop (loop_id, rg_id, V.LoopSynthRet) in
+ let abs = { abs with kind } in
+ super#visit_abs env abs
+ | _ -> super#visit_abs env abs
end
in
let new_absl = List.map (visit_tgt#visit_abs ()) new_absl in
@@ -3058,8 +3061,19 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
in
let cc = InterpreterBorrows.end_borrows config new_borrows in
+ (* List the loop input values - when iterating over a map, we iterate
+ over the keys, in increasing order *)
+ let input_values =
+ List.map snd
+ (V.SymbolicValueId.Map.bindings tgt_to_src_maps.sid_to_value_map)
+ in
+
(* Continue *)
- cc (cf (if is_loop_entry then EndEnterLoop else EndContinue)) src_ctx
+ cc
+ (cf
+ (if is_loop_entry then EndEnterLoop input_values
+ else EndContinue input_values))
+ src_ctx
in
(* Compose and continue *)
@@ -3080,7 +3094,8 @@ 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 | Panic -> cf res
+ | Return -> cf LoopReturn
+ | Panic -> cf Panic
| Break i ->
(* Break out of the loop by calling the continuation *)
let res = if i = 0 then Unit else Break (i - 1) in
@@ -3100,7 +3115,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")
- | EndEnterLoop | EndContinue ->
+ | LoopReturn | EndEnterLoop _ | EndContinue _ ->
(* We can't get there: this is only used in symbolic mode *)
raise (Failure "Unreachable")
in
@@ -3155,12 +3170,12 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
| Continue i ->
(* We don't support nested loops for now *)
assert (i = 0);
- let fp_bl_corresp =
- compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx
+ let cc =
+ match_ctx_with_target config loop_id false fp_bl_corresp fixed_ids
+ fp_ctx
in
- match_ctx_with_target config loop_id false fp_bl_corresp fixed_ids
- fp_ctx cf ctx
- | Unit | EndEnterLoop | EndContinue ->
+ cc cf ctx
+ | 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.
*)
@@ -3169,7 +3184,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
let loop_expr = eval_loop_body cf_loop fp_ctx in
(* Put together *)
- S.synthesize_loop end_expr loop_expr
+ S.synthesize_loop loop_id end_expr loop_expr
(** Evaluate a loop *)
let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 63d10894..7e4722b8 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -317,14 +317,17 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id)
in
Subst.erase_regions_substitute_types tsubst sg.output
-let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
- =
+let move_return_value (config : C.config) (pop_return_value : bool)
+ (cf : V.typed_value option -> m_fun) : m_fun =
fun ctx ->
- let ret_vid = E.VarId.zero in
- let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
- cc cf ctx
-
-let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
+ if pop_return_value then
+ let ret_vid = E.VarId.zero in
+ let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
+ cc (fun v ctx -> cf (Some v) ctx) ctx
+ else cf None ctx
+
+let pop_frame (config : C.config) (pop_return_value : bool)
+ (cf : V.typed_value option -> m_fun) : m_fun =
fun ctx ->
(* Debug *)
log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx));
@@ -350,15 +353,18 @@ let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
^ "]"));
(* Move the return value out of the return variable *)
- let cc = move_return_value config in
+ let cc = move_return_value config pop_return_value in
(* Sanity check *)
let cc =
comp_check_value cc (fun ret_value ctx ->
- assert (not (bottom_in_value ctx.ended_regions ret_value)))
+ match ret_value with
+ | None -> ()
+ | Some ret_value ->
+ assert (not (bottom_in_value ctx.ended_regions ret_value)))
in
(* Drop the outer *loans* we find in the local variables *)
- let cf_drop_loans_in_locals cf (ret_value : V.typed_value) : m_fun =
+ let cf_drop_loans_in_locals cf (ret_value : V.typed_value option) : m_fun =
(* Drop the loans *)
let locals = List.rev locals in
let cf_drop =
@@ -392,7 +398,7 @@ let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
C.Var (C.DummyBinder vid, v) :: pop env
| C.Frame :: env -> (* Stop here *) env
in
- let cf_pop cf (ret_value : V.typed_value) : m_fun =
+ let cf_pop cf (ret_value : V.typed_value option) : m_fun =
fun ctx ->
let env = pop ctx.env in
let ctx = { ctx with env } in
@@ -403,9 +409,9 @@ let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
(** Pop the current frame and assign the returned value to its destination. *)
let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
- let cf_pop = pop_frame config in
+ let cf_pop = pop_frame config true in
let cf_assign cf ret_value : m_fun =
- assign_to_place config ret_value dest cf
+ assign_to_place config (Option.get ret_value) dest cf
in
comp cf_pop cf_assign
@@ -845,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 | EndEnterLoop | EndContinue
- ->
+ | Panic | Break _ | Continue _ | Return | LoopReturn | EndEnterLoop _
+ | EndContinue _ ->
cf res
in
(* Compose and apply *)
@@ -1094,7 +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 | EndEnterLoop | EndContinue ->
+ | Break _ | Continue _ | Unit | LoopReturn | EndEnterLoop _ | EndContinue _
+ ->
raise (Failure "Unreachable")
in
let cc = comp cc cf_finish in
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 46afa782..789804b1 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -18,8 +18,11 @@ open InterpreterExpressions
variable, move the return value out of the return variable, remove all the
local variables (but preserve the abstractions!), remove the {!C.Frame} indicator
delimiting the current frame and handle the return value to the continuation.
+
+ If the boolean is false, we don't move the return value, and call the
+ continuation with [None].
*)
-val pop_frame : C.config -> (V.typed_value -> m_fun) -> m_fun
+val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun
(** Instantiate a function signature, introducing **fresh** abstraction ids and
region ids. This is mostly used in preparation of function calls, when
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index dba2e7cd..ee8ea212 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -28,6 +28,7 @@ let operand_to_string = PA.operand_to_string
let statement_to_string ctx = PA.statement_to_string ctx "" " "
let statement_to_string_with_tab ctx = PA.statement_to_string ctx " " " "
let env_elem_to_string ctx = PA.env_elem_to_string ctx "" " "
+let env_to_string ctx env = eval_ctx_to_string { ctx with env }
let abs_to_string ctx = PA.abs_to_string ctx "" " "
let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 08253e77..60b45d99 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -100,7 +100,8 @@ type expression =
We use it to compute meaningful names for the variables we introduce,
to prettify the generated code.
*)
- | ForwardEnd of expression * expression T.RegionGroupId.Map.t
+ | ForwardEnd of
+ V.typed_value list option * expression * expression T.RegionGroupId.Map.t
(** We use this delimiter to indicate at which point we switch to the
generation of code specific to the backward function(s). This allows
us in particular to factor the work out: we don't need to replay the
@@ -110,11 +111,16 @@ type expression =
The first expression gives the end of the translation for the forward
function, the map from region group ids to expressions gives the end
of the translation for the backward functions.
+
+ The optional list of input values are input values for loops: upon
+ entering a loop, in the translation we call the loop translation
+ function, which takes care of the end of the execution.
*)
- | Loop of loop
+ | Loop of loop (** Loop *)
| Meta of meta * expression (** Meta information *)
and loop = {
+ loop_id : V.LoopId.id;
end_expr : expression;
(** The end of the function (upon the moment it enters the loop) *)
loop_expr : expression; (** The symbolically executed loop body *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6c956fe8..8db968f3 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1162,7 +1162,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
| Assertion (ectx, v, e) -> translate_assertion ectx v e ctx
| Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
| Meta (meta, e) -> translate_meta meta e ctx
- | ForwardEnd (e, back_e) ->
+ | ForwardEnd (loop_input_values, e, back_e) ->
+ assert (loop_input_values = None);
(* Update the current state with the additional state received by the backward
function, if needs be, and lookup the proper expression *)
let ctx, e =
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index a24b5690..a7f84f61 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -156,13 +156,14 @@ let synthesize_assertion (ctx : Contexts.eval_ctx) (v : V.typed_value)
(e : expression option) =
Option.map (fun e -> Assertion (ctx, v, e)) e
-let synthesize_forward_end (e : expression)
- (el : expression T.RegionGroupId.Map.t) =
- Some (ForwardEnd (e, el))
+let synthesize_forward_end (loop_input_values : V.typed_value list option)
+ (e : expression) (el : expression T.RegionGroupId.Map.t) =
+ Some (ForwardEnd (loop_input_values, e, el))
-let synthesize_loop (end_expr : expression option)
+let synthesize_loop (loop_id : V.LoopId.id) (end_expr : expression option)
(loop_expr : expression option) : expression option =
match (end_expr, loop_expr) with
| None, None -> None
- | Some end_expr, Some loop_expr -> Some (Loop { end_expr; loop_expr })
+ | Some end_expr, Some loop_expr ->
+ Some (Loop { loop_id; end_expr; loop_expr })
| _ -> raise (Failure "Unreachable")
diff --git a/compiler/Values.ml b/compiler/Values.ml
index e737103a..f9b4e423 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -893,6 +893,9 @@ and typed_avalue = { value : avalue; ty : rty }
concrete = true;
}]
+(** TODO: make those variants of [abs_kind] *)
+type loop_abs_kind = LoopSynthInput | LoopSynthRet [@@deriving show, ord]
+
(** The kind of an abstraction, which keeps track of its origin *)
type abs_kind =
| FunCall of (FunCallId.id * RegionGroupId.id)
@@ -920,7 +923,7 @@ type abs_kind =
See the explanations for [SynthInput].
*)
- | Loop of (LoopId.id * RegionGroupId.id option)
+ | Loop of (LoopId.id * RegionGroupId.id option * loop_abs_kind)
(** The abstraction corresponds to a loop.
The region group id is initially [None].
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 470f40ac..adeb105f 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -37,6 +37,13 @@ let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
| Borrow (MutBorrow (bid, bv)) -> (bid, bv)
| _ -> raise (Failure "Unexpected")
+let is_unit (v : typed_value) : bool =
+ ty_is_unit v.ty
+ &&
+ match v.value with
+ | Adt av -> av.variant_id = None && av.field_values = []
+ | _ -> false
+
(** Check if a value contains a *concrete* borrow (i.e., a [Borrow] value -
we don't check if there are borrows hidden in symbolic values).
*)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 03:38:13 +0000