diff options
| -rw-r--r-- | compiler/InterpreterLoops.ml | 6 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 119 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 12 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 2 |
4 files changed, 137 insertions, 2 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 1d774e0e..afbe0501 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -261,6 +261,10 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : match config.mode with | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx | SymbolicMode -> + (* Simplify the context by ending the unnecessary borrows/loans and getting + rid of the useless symbolic values (which are in anonymous variables) *) + let cc = cleanup_fresh_values_and_abs config empty_ids_set in + (* We want to make sure the loop will *not* manipulate shared avalues containing themselves shared loans (i.e., nested shared loans in the abstractions), because it complexifies the matches between values @@ -279,5 +283,5 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : introduce *fixed* abstractions, and again later to introduce *non-fixed* abstractions. *) - let cc = prepare_ashared_loans None in + let cc = comp cc (prepare_ashared_loans None) in comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 39a17c25..66c97cde 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -6,6 +6,8 @@ open ValuesUtils module S = SynthesizeSymbolic open Cps open InterpreterUtils +open InterpreterBorrowsCore +open InterpreterBorrows open InterpreterLoopsCore open InterpreterLoopsMatchCtxs open InterpreterLoopsJoinCtxs @@ -13,6 +15,119 @@ open InterpreterLoopsJoinCtxs (** The local logger *) let log = Logging.loops_fixed_point_log +exception FoundBorrowId of BorrowId.id +exception FoundAbsId of AbstractionId.id + +(* Repeat until we can't simplify the context anymore: + - end the borrows which appear in fresh anonymous values and don't contain loans + - end the fresh region abstractions which can be ended (no loans) +*) +let rec end_useless_fresh_borrows_and_abs (config : config) + (fixed_ids : ids_sets) : cm_fun = + fun cf ctx -> + let rec explore_env (env : env) : unit = + match env with + | [] -> () (* Done *) + | EBinding (BDummy vid, v) :: env + when not (DummyVarId.Set.mem vid fixed_ids.dids) -> + (* Explore the anonymous value - raises an exception if it finds + a borrow to end *) + let visitor = + object + inherit [_] iter_typed_value + method! visit_VLoan _ _ = () (* Don't enter inside loans *) + + method! visit_VBorrow _ bc = + (* Check if we can end the borrow, do not enter inside if we can't *) + match bc with + | VSharedBorrow bid | VReservedMutBorrow bid -> + raise (FoundBorrowId bid) + | VMutBorrow (bid, v) -> + if not (value_has_loans v.value) then + raise (FoundBorrowId bid) + else (* Stop there *) + () + end + in + visitor#visit_typed_value () v; + (* No exception was raised: continue *) + explore_env env + | EAbs abs :: env when not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids) + -> ( + (* Check if it is possible to end the abstraction: if yes, raise an exception *) + let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in + match opt_loan with + | None -> + (* No remaining loans: we can end the abstraction *) + raise (FoundAbsId abs.abs_id) + | Some _ -> + (* There are remaining loans: we can't end the abstraction *) + explore_env env) + | _ :: env -> explore_env env + in + let rec_call = end_useless_fresh_borrows_and_abs config fixed_ids in + try + (* Explore the environment *) + explore_env ctx.env; + (* No exception raised: call the continuation *) + cf ctx + with + | FoundAbsId abs_id -> + let cc = end_abstraction config abs_id in + comp cc rec_call cf ctx + | FoundBorrowId bid -> + let cc = end_borrow config bid in + comp cc rec_call cf ctx + +(* Explore the fresh anonymous values and replace all the values which are not + borrows/loans with ⊥ *) +let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun = + fun cf ctx -> + let rec explore_env (env : env) : env = + match env with + | [] -> [] (* Done *) + | EBinding (BDummy vid, v) :: env + when not (DummyVarId.Set.mem vid fixed_ids.dids) -> + let env = explore_env env in + (* Eliminate the value altogether if it doesn't contain loans/borrows *) + if not (value_has_loans_or_borrows ctx v.value) then env + else + (* Explore the anonymous value - raises an exception if it finds + a borrow to end *) + let visitor = + object + inherit [_] map_typed_value as super + method! visit_VLoan _ v = VLoan v (* Don't enter inside loans *) + + method! visit_VBorrow _ v = + VBorrow v (* Don't enter inside borrows *) + + method! visit_value _ v = + if not (value_has_loans_or_borrows ctx v) then VBottom + else super#visit_value () v + end + in + let v = visitor#visit_typed_value () v in + EBinding (BDummy vid, v) :: env + | x :: env -> x :: explore_env env + in + let ctx = { ctx with env = explore_env ctx.env } in + cf ctx + +(* Repeat until we can't simplify the context anymore: + - explore the fresh anonymous values and replace all the values which are not + borrows/loans with ⊥ + - also end the borrows which appear in fresh anonymous values and don't contain loans + - end the fresh region abstractions which can be ended (no loans) +*) +let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) : + cm_fun = + fun cf ctx -> + comp + (end_useless_fresh_borrows_and_abs config fixed_ids) + (cleanup_fresh_values fixed_ids) + cf ctx + (** Reorder the loans and borrows in the fresh abstractions. We do this in order to enforce some structure in the environments: this @@ -370,7 +485,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) (* The fixed ids. They are the ids of the original ctx, after we ended the borrows/loans which end during the first loop iteration (we do - one loop iteration, then set it to [Some]. + one loop iteration, then set it to [Some]). *) let fixed_ids : ids_sets option ref = ref None in @@ -425,6 +540,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) in let fixed_ids = Option.get !fixed_ids in + + (* Join the context with the context at the loop entry *) let (_, _), ctx2 = loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs in diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index c0e5dca5..7c3f6199 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -3,6 +3,18 @@ open Contexts open InterpreterUtils open InterpreterLoopsCore +(** Repeat until we can't simplify the context anymore: + - explore the fresh anonymous values and replace all the values which are not + borrows/loans with ⊥ + - also end the borrows which appear in fresh anonymous values and don't contain loans + - end the fresh region abstractions which can be ended (no loans) + + Inputs: + - config + - fixed ids (the fixeds ids are the ids we consider as non-fresh) + *) +val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun + (** Prepare the shared loans in the abstractions by moving them to fresh abstractions. diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 0817b111..667c5080 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -420,6 +420,8 @@ let compute_ctxs_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values = let compute_ctx_ids (ctx : eval_ctx) : ids_sets * ids_to_values = compute_ctxs_ids [ ctx ] +let empty_ids_set = fst (compute_ctxs_ids []) + (** **WARNING**: this function doesn't compute the normalized types (for the trait type aliases). This should be computed afterwards. *) |