summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterLoops.ml')
-rw-r--r--compiler/InterpreterLoops.ml521
1 files changed, 521 insertions, 0 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
new file mode 100644
index 00000000..702420cd
--- /dev/null
+++ b/compiler/InterpreterLoops.ml
@@ -0,0 +1,521 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module A = LlbcAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+module S = SynthesizeSymbolic
+module UF = UnionFind
+open Utils
+open Cps
+open InterpreterUtils
+open InterpreterBorrows
+open InterpreterProjectors
+open InterpreterExpansion
+open InterpreterPaths
+open InterpreterExpressions
+
+(** The local logger *)
+let log = L.loops_log
+
+type cnt_thresholds = {
+ aid : V.AbstractionId.id;
+ sid : V.SymbolicValueId.id;
+ bid : V.BorrowId.id;
+ did : C.DummyVarId.id;
+}
+
+(** Union Find *)
+module UnionFind = UF.Make (UF.StoreMap)
+
+(** A small utility *)
+type abs_borrows_loans_maps = {
+ abs_ids : V.AbstractionId.id list;
+ abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t;
+ abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
+ borrow_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
+ loan_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
+}
+
+(** Compute various maps linking the abstractions and the borrows/loans they contain.
+
+ The [explore] function is used to filter abstractions.
+ *)
+let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
+ abs_borrows_loans_maps =
+ let abs_ids = ref [] in
+ let abs_to_borrows = ref V.AbstractionId.Map.empty in
+ let abs_to_loans = ref V.AbstractionId.Map.empty in
+ let borrow_to_abs = ref V.BorrowId.Map.empty in
+ let loan_to_abs = ref V.BorrowId.Map.empty in
+
+ let register_borrow_id abs_id bid =
+ abs_to_borrows :=
+ V.AbstractionId.Map.update abs_id
+ (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
+ !abs_to_borrows;
+ assert (not (V.BorrowId.Map.mem bid !borrow_to_abs));
+ borrow_to_abs := V.BorrowId.Map.add bid abs_id !borrow_to_abs
+ in
+
+ let register_loan_id abs_id bid =
+ abs_to_loans :=
+ V.AbstractionId.Map.update abs_id
+ (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
+ !abs_to_loans;
+ assert (not (V.BorrowId.Map.mem bid !loan_to_abs));
+ loan_to_abs := V.BorrowId.Map.add bid abs_id !loan_to_abs
+ in
+
+ let explore_abs =
+ object (self : 'self)
+ inherit [_] V.iter_typed_avalue as super
+
+ (** Make sure we don't register the ignored ids *)
+ method! visit_aloan_content abs_id lc =
+ match lc with
+ | AMutLoan _ | ASharedLoan _ ->
+ (* Process those normally *)
+ super#visit_aloan_content abs_id lc
+ | AIgnoredMutLoan (_, child)
+ | AEndedIgnoredMutLoan { child; given_back = _; given_back_meta = _ }
+ | AIgnoredSharedLoan child ->
+ (* Ignore the id of the loan, if there is *)
+ self#visit_typed_avalue abs_id child
+ | AEndedMutLoan _ | AEndedSharedLoan _ -> raise (Failure "Unreachable")
+
+ (** Make sure we don't register the ignored ids *)
+ method! visit_aborrow_content abs_id bc =
+ match bc with
+ | AMutBorrow _ | ASharedBorrow _ | AProjSharedBorrow _ ->
+ (* Process those normally *)
+ super#visit_aborrow_content abs_id bc
+ | AIgnoredMutBorrow (_, child)
+ | AEndedIgnoredMutBorrow
+ { child; given_back_loans_proj = _; given_back_meta = _ } ->
+ (* Ignore the id of the borrow, if there is *)
+ self#visit_typed_avalue abs_id child
+ | AEndedMutBorrow _ | AEndedSharedBorrow ->
+ raise (Failure "Unreachable")
+
+ method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid
+ method! visit_loan_id abs_id lid = register_loan_id abs_id lid
+ end
+ in
+
+ List.iter
+ (fun (ee : C.env_elem) ->
+ match ee with
+ | Var _ | Frame -> ()
+ | Abs abs ->
+ let abs_id = abs.abs_id in
+ if explore abs then (
+ abs_to_borrows :=
+ V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty
+ !abs_to_borrows;
+ abs_to_loans :=
+ V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_loans;
+ abs_ids := abs.abs_id :: !abs_ids;
+ List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues)
+ else ())
+ env;
+
+ {
+ abs_ids = List.rev !abs_ids;
+ abs_to_borrows = !abs_to_borrows;
+ abs_to_loans = !abs_to_loans;
+ borrow_to_abs = !borrow_to_abs;
+ loan_to_abs = !loan_to_abs;
+ }
+
+(** Collapse an environment.
+
+ We do this to simplify an environment, for the purpose of finding a loop
+ fixed point.
+
+ We do the following:
+ - we look for all the *new* dummy values (we use id thresholds to decide
+ wether a value is new or not - the ids generated by our counters are
+ monotonic), and we convert to abstractions (if they contain loans or
+ borrows)
+ - whenever there is a new abstraction in the context, and some of its
+ its borrows are associated to loans in another new abstraction, we
+ merge them.
+ In effect, this allows us to merge newly introduced abstractions/borrows
+ with their parent abstractions.
+ *)
+let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+ (ctx0 : C.eval_ctx) : C.eval_ctx =
+ let abs_kind = V.Loop loop_id in
+ let can_end = true in
+ let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
+ V.AbstractionId.Ord.compare thresh.aid id >= 0
+ in
+ let is_fresh_did (id : C.DummyVarId.id) : bool =
+ C.DummyVarId.Ord.compare thresh.did id >= 0
+ in
+ (* Convert the dummy values to abstractions *)
+ (* Note that we preserve the order of the dummy values: we replace them with
+ abstractions in place - this makes matching easier *)
+ let env =
+ List.concat
+ (List.map
+ (fun ee ->
+ match ee with
+ | C.Abs _ | C.Frame | C.Var (VarBinder _, _) -> [ ee ]
+ | C.Var (DummyBinder id, v) ->
+ if is_fresh_did id then
+ let absl =
+ convert_value_to_abstractions abs_kind can_end ctx0 v
+ in
+ List.map (fun abs -> C.Abs abs) absl
+ else [ ee ])
+ ctx0.env)
+ in
+
+ (* Explore all the *new* abstractions, and compute various maps *)
+ let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
+ let ids_maps = compute_abs_borrows_loans_maps explore env in
+ let {
+ abs_ids;
+ abs_to_borrows;
+ abs_to_loans = _;
+ borrow_to_abs = _;
+ loan_to_abs;
+ } =
+ ids_maps
+ in
+
+ (* Use the maps to merge the abstractions together *)
+ let merged_abs : V.AbstractionId.id UF.elem V.AbstractionId.Map.t =
+ V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids)
+ in
+
+ let ctx = ref { ctx0 with C.env } in
+
+ (* Merge all the mergeable abs.
+
+ We iterate over the abstractions, then over the borrows in the abstractions.
+ We do this because we want to control the order in which abstractions
+ are merged (the ids are iterated in increasing order). Otherwise, we
+ could simply iterate over all the borrows in [borrow_to_abs]...
+ *)
+ List.iter
+ (fun abs_id0 ->
+ let bids = V.AbstractionId.Map.find abs_id0 abs_to_borrows in
+ let bids = V.BorrowId.Set.elements bids in
+ List.iter
+ (fun bid ->
+ match V.BorrowId.Map.find_opt bid loan_to_abs with
+ | None -> (* Nothing to do *) ()
+ | Some abs_id1 ->
+ (* We need to merge - unless we have already merged *)
+ (* First, find the representatives for the two abstractions (the
+ representative is the abstraction into which we merged) *)
+ let abs_ref0 =
+ UF.find (V.AbstractionId.Map.find abs_id0 merged_abs)
+ in
+ let abs_id0 = UF.get abs_ref0 in
+ let abs_ref1 =
+ UF.find (V.AbstractionId.Map.find abs_id1 merged_abs)
+ in
+ let abs_id1 = UF.get abs_ref1 in
+ (* If the two ids are the same, it means the abstractions were already merged *)
+ if abs_id0 = abs_id1 then ()
+ else
+ (* We actually need to merge the abstractions *)
+ (* Lookup the abstractions *)
+ let abs0 = C.ctx_lookup_abs !ctx abs_id0 in
+ let abs1 = C.ctx_lookup_abs !ctx abs_id1 in
+ (* Merge them - note that we take care to merge [abs0] into [abs1]
+ (the order is important).
+ *)
+ let nabs = merge_abstractions abs_kind can_end !ctx abs1 abs0 in
+ (* Update the environment *)
+ ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs);
+ ctx := fst (C.ctx_remove_abs !ctx abs_id0);
+ (* Update the union find *)
+ let abs_ref_merged = UF.union abs_ref0 abs_ref1 in
+ UF.set abs_ref_merged nabs.abs_id)
+ bids)
+ abs_ids;
+
+ (* Return the new context *)
+ !ctx
+
+(* TODO: document.
+ TODO: we might not use the bounds properly, use sets instead.
+*)
+type match_ctx = {
+ ctx : C.eval_ctx;
+ aids : V.AbstractionId.Set.t;
+ sids : V.SymbolicValueId.Set.t;
+ bids : V.BorrowId.Set.t;
+}
+
+let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
+ let aids = V.AbstractionId.Set.empty in
+ let sids = V.SymbolicValueId.Set.empty in
+ let bids = V.BorrowId.Set.empty in
+ { ctx; aids; sids; bids }
+
+type joined_ctx_or_update =
+ | EndAbs of V.AbstractionId.id
+ | EndBorrow of V.BorrowId.id
+ | JoinedCtx of match_ctx
+
+(** Merge a borrow with the abstraction containing the associated loan, where
+ the abstraction must be a *loop abstraction* (we don't synthesize code during
+ the operation).
+
+ For instance:
+ {[
+ abs'0 { mut_loan l0 }
+ x -> mut_borrow l0 sx
+
+ ~~>
+
+ abs'0 {}
+ x -> ⊥
+ ]}
+ *)
+let merge_borrow_with_parent_loop_abs (config : C.config) (bid : V.BorrowId.id)
+ (ctx : C.eval_ctx) : C.eval_ctx =
+ (* TODO: use the function from InterpreterBorrows *)
+ failwith "Unimplemented"
+(* (* Lookup the borrow *)
+ let ek =
+ { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
+ in
+ (* TODO: use [end_borrow_get_borrow]? *)
+ match lookup_borrow ek bid ctx with
+ | None -> ctx
+ | Some b -> failwith "Unimplemented"*)
+
+(** See {!merge_borrow_with_parent_loop_abs} *)
+let rec merge_borrows_with_parent_loop_abs (config : C.config)
+ (bids : V.BorrowId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
+ V.BorrowId.Set.fold
+ (fun id ctx -> merge_borrow_with_parent_loop_abs config id ctx)
+ bids ctx
+
+(* TODO: we probably don't need an [match_ctx], and actually we might not use
+ the bounds propertly.
+*)
+let match_ctx_with_target (config : C.config) (tgt_mctx : match_ctx) : cm_fun =
+ fun cf src_ctx ->
+ (* We first reorganize [ctx] so that we can match it with [tgt_mctx] *)
+ (* First, collect all the borrows and abstractions which are in [ctx]
+ and not in [tgt_mctx]: we need to end them *)
+ let src_bids, src_aids =
+ InterpreterBorrowsCore.compute_borrow_abs_ids_in_context src_ctx
+ in
+ let tgt_bids, tgt_aids =
+ InterpreterBorrowsCore.compute_borrow_abs_ids_in_context tgt_mctx.ctx
+ in
+ let bids = V.BorrowId.Set.diff src_bids tgt_bids in
+ let aids = V.AbstractionId.Set.diff src_aids tgt_aids in
+ (* End those borrows and abstractions *)
+ let cc = InterpreterBorrows.end_borrows config bids in
+ let cc = comp cc (InterpreterBorrows.end_abstractions config aids) in
+ (* In the target context, merge all the borrows introduced by the loop with
+ their parent abstractions
+ *)
+ let tgt_ctx =
+ merge_borrows_with_parent_loop_abs config
+ (V.BorrowId.Set.diff tgt_bids src_bids)
+ tgt_mctx.ctx
+ in
+ (* Replace the source context with the target context - TODO: explain
+ why this works *)
+ let cf_apply_match : cm_fun = fun cf _ -> cf tgt_ctx in
+ let cc = comp cc cf_apply_match in
+ (* Sanity check on the resulting context *)
+ let cc = comp_check_ctx cc Inv.check_invariants in
+ (* Apply and continue *)
+ cc cf src_ctx
+
+(** Join a context at the entry of a loop with a context upon reaching
+ a continue in this loop.
+ *)
+let loop_join_entry_ctx_with_continue_ctx (ctx0 : match_ctx) (ctx1 : C.eval_ctx)
+ : joined_ctx_or_update =
+ failwith "Unimplemented"
+
+(** See {!loop_join_entry_ctx_with_continue_ctx} *)
+let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : match_ctx)
+ (ctxs : C.eval_ctx list) : joined_ctx_or_update =
+ match ctxs with
+ | [] -> JoinedCtx ctx0
+ | ctx1 :: ctxs -> (
+ let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in
+ match res with
+ | EndAbs _ | EndBorrow _ -> res
+ | JoinedCtx ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
+
+let compute_loop_entry_fixed_point (config : C.config)
+ (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : match_ctx =
+ (* The continuation for when we exit the loop - we use it to register the
+ environments upon loop *reentry*
+ *)
+ let ctxs = ref [] in
+ let register_ctx ctx = ctxs := ctx :: !ctxs in
+ let cf_exit_loop_body (res : statement_eval_res) : m_fun =
+ fun ctx ->
+ match res with
+ | Return | Panic | Break _ -> None
+ | Unit ->
+ (* See the comment in {!eval_loop} *)
+ raise (Failure "Unreachable")
+ | Continue i ->
+ (* For now we don't support continues to outer loops *)
+ assert (i = 0);
+ register_ctx ctx;
+ None
+ | EndEnterLoop | EndContinue ->
+ (* We don't support nested loops for now *)
+ raise (Failure "Nested loops are not supported for now")
+ in
+ (* Join the contexts at the loop entry *)
+ (* TODO: return result:
+ * - end borrows in ctx0
+ * - ok: return joined env
+ * TODO: keep initial env somewhere?
+ * TODO: the returned env is an eval_ctx or smth else?
+ * Maybe simply keep track of existentially quantified variables?
+ *)
+ let join_ctxs (ctx0 : match_ctx) : joined_ctx_or_update =
+ let ctx1 = loop_join_entry_ctx_with_continue_ctxs ctx0 !ctxs in
+ ctxs := [];
+ ctx1
+ in
+ (* Check if two contexts are equivalent - modulo alpha conversion on the
+ existentially quantified borrows/abstractions/symbolic values *)
+ let equiv_ctxs (_ctx1 : match_ctx) (_ctx2 : match_ctx) : bool =
+ failwith "Unimplemented"
+ in
+ let max_num_iter = Config.loop_fixed_point_max_num_iters in
+ let rec compute_fixed_point (mctx : match_ctx) (i : int) : match_ctx =
+ if i = 0 then
+ raise
+ (Failure
+ ("Could not compute a loop fixed point in "
+ ^ string_of_int max_num_iter ^ " iterations"))
+ else
+ (* The join on the environments may fail if we need to end some borrows/abstractions
+ in the original context first: reorganize the original environment for as
+ long as we need to *)
+ let rec eval_iteration_then_join (mctx : match_ctx) =
+ (* Evaluate the loop body *)
+ let _ = eval_loop_body cf_exit_loop_body mctx.ctx in
+ (* Check if the join succeeded, or if we need to end abstractions/borrows
+ in the original environment first *)
+ match join_ctxs mctx with
+ | EndAbs id ->
+ let ctx1 =
+ InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx
+ in
+ eval_iteration_then_join { mctx with ctx = ctx1 }
+ | EndBorrow id ->
+ let ctx1 =
+ InterpreterBorrows.end_borrow_no_synth config id mctx.ctx
+ in
+ eval_iteration_then_join { mctx with ctx = ctx1 }
+ | JoinedCtx mctx1 ->
+ (* The join succeeded: check if we reached a fixed point, otherwise
+ iterate *)
+ if equiv_ctxs mctx mctx1 then mctx1
+ else compute_fixed_point mctx1 (i - 1)
+ in
+ eval_iteration_then_join mctx
+ in
+ compute_fixed_point (mk_match_ctx ctx0) max_num_iter
+
+(** Evaluate a loop in concrete mode *)
+let eval_loop_concrete (config : C.config) (eval_loop_body : st_cm_fun) :
+ st_cm_fun =
+ fun cf ctx ->
+ (* Continuation for after we evaluate the loop body: depending the result
+ of doing one loop iteration:
+ - redoes a loop iteration
+ - exits the loop
+ - other...
+
+ We need a specific function because of the {!Continue} case: in case we
+ continue, we might have to reevaluate the current loop body with the
+ new context (and repeat this an indefinite number of times).
+ *)
+ let rec reeval_loop_body (res : statement_eval_res) : m_fun =
+ match res with
+ | Return | Panic -> cf res
+ | Break i ->
+ (* Break out of the loop by calling the continuation *)
+ let res = if i = 0 then Unit else Break (i - 1) in
+ cf res
+ | Continue 0 ->
+ (* Re-evaluate the loop body *)
+ eval_loop_body reeval_loop_body
+ | Continue i ->
+ (* Continue to an outer loop *)
+ cf (Continue (i - 1))
+ | Unit ->
+ (* We can't get there.
+ * Note that if we decide not to fail here but rather do
+ * the same thing as for [Continue 0], we could make the
+ * code slightly simpler: calling {!reeval_loop_body} with
+ * {!Unit} would account for the first iteration of the loop.
+ * We prefer to write it this way for consistency and sanity,
+ * though. *)
+ raise (Failure "Unreachable")
+ | EndEnterLoop | EndContinue ->
+ (* We can't get there: this is only used in symbolic mode *)
+ raise (Failure "Unreachable")
+ in
+
+ (* Apply *)
+ eval_loop_body reeval_loop_body ctx
+
+(** Evaluate a loop in symbolic mode *)
+let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
+ st_cm_fun =
+ fun cf ctx ->
+ (* Compute the fixed point at the loop entrance *)
+ let mctx = compute_loop_entry_fixed_point config eval_loop_body ctx in
+ (* Synthesize the end of the function *)
+ let end_expr = match_ctx_with_target config mctx (cf EndEnterLoop) ctx in
+ (* Synthesize the loop body by evaluating it, with the continuation for
+ after the loop starting at the *fixed point*, but with a special
+ treatment for the [Break] and [Continue] cases *)
+ let cf_loop : st_m_fun =
+ fun res ctx ->
+ match res with
+ | Return | Panic -> cf res ctx
+ | Break i ->
+ (* Break out of the loop by calling the continuation *)
+ let res = if i = 0 then Unit else Break (i - 1) in
+ cf res ctx
+ | Continue i ->
+ (* We don't support nested loops for now *)
+ assert (i = 0);
+ match_ctx_with_target config mctx (cf EndContinue) ctx
+ | Unit | 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.
+ *)
+ raise (Failure "Unreachable")
+ in
+ let loop_expr = eval_loop_body cf_loop mctx.ctx in
+ (* Put together *)
+ S.synthesize_loop end_expr loop_expr
+
+(** Evaluate a loop *)
+let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
+ fun cf ctx ->
+ match config.C.mode with
+ | ConcreteMode -> eval_loop_concrete config eval_loop_body cf ctx
+ | SymbolicMode -> eval_loop_symbolic config eval_loop_body cf ctx
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-11 00:32:01 +0000