diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Interpreter.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 86 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 11 |
3 files changed, 63 insertions, 38 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 4c1bc047..ec1b6260 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -270,8 +270,8 @@ let evaluate_function_symbolic (synthesize : bool) (* Put everything together *) S.synthesize_forward_end fwd_e back_el else None - | EndEnterLoop -> failwith "Unimplemented" - | EndContinue -> failwith "Unimplemented" + | 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 *) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index b8dc510f..53005bf3 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -1491,7 +1491,7 @@ module type MatchCheckEquivState = sig val rid_map : T.RegionId.InjSubst.t ref (** Substitution for the loan and borrow ids - used only if [check_equiv] is true *) - val bid_map : V.BorrowId.InjSubst.t ref + val blid_map : V.BorrowId.InjSubst.t ref (** Substitution for the borrow ids - used only if [check_equiv] is false *) val borrow_id_map : V.BorrowId.InjSubst.t ref @@ -1551,34 +1551,34 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct module GetSetBid = MkGetSetM (V.BorrowId) - let get_bid = GetSetBid.get S.bid_map - let match_bid = GetSetBid.match_e S.bid_map - let match_bidl = GetSetBid.match_el S.bid_map - let match_bids = GetSetBid.match_es S.bid_map + let get_blid = GetSetBid.get S.blid_map + let match_blid = GetSetBid.match_e S.blid_map + let match_blidl = GetSetBid.match_el S.blid_map + let match_blids = GetSetBid.match_es S.blid_map let get_borrow_id = - if S.check_equiv then get_bid else GetSetBid.get S.borrow_id_map + if S.check_equiv then get_blid else GetSetBid.get S.borrow_id_map let match_borrow_id = - if S.check_equiv then match_bid else GetSetBid.match_e S.borrow_id_map + if S.check_equiv then match_blid else GetSetBid.match_e S.borrow_id_map let match_borrow_idl = - if S.check_equiv then match_bidl else GetSetBid.match_el S.borrow_id_map + if S.check_equiv then match_blidl else GetSetBid.match_el S.borrow_id_map let match_borrow_ids = - if S.check_equiv then match_bids else GetSetBid.match_es S.borrow_id_map + if S.check_equiv then match_blids else GetSetBid.match_es S.borrow_id_map let get_loan_id = - if S.check_equiv then get_bid else GetSetBid.get S.loan_id_map + if S.check_equiv then get_blid else GetSetBid.get S.loan_id_map let match_loan_id = - if S.check_equiv then match_bid else GetSetBid.match_e S.loan_id_map + if S.check_equiv then match_blid else GetSetBid.match_e S.loan_id_map let match_loan_idl = - if S.check_equiv then match_bidl else GetSetBid.match_el S.loan_id_map + if S.check_equiv then match_blidl else GetSetBid.match_el S.loan_id_map let match_loan_ids = - if S.check_equiv then match_bids else GetSetBid.match_es S.loan_id_map + if S.check_equiv then match_blids else GetSetBid.match_es S.loan_id_map module GetSetSid = MkGetSetM (V.SymbolicValueId) @@ -1719,7 +1719,7 @@ end (** See {!match_ctxs} *) type ids_maps = { aid_map : V.AbstractionId.InjSubst.t; - bid_map : V.BorrowId.InjSubst.t; + blid_map : V.BorrowId.InjSubst.t; (** Substitution for the loan and borrow ids *) borrow_id_map : V.BorrowId.InjSubst.t; (** Substitution for the borrow ids *) loan_id_map : V.BorrowId.InjSubst.t; (** Substitution for the loan ids *) @@ -1765,9 +1765,9 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) let module IdMap = IdMap (T.RegionId) in IdMap.mk_map_ref fixed_ids.rids in - let bid_map = + let blid_map = let module IdMap = IdMap (V.BorrowId) in - IdMap.mk_map_ref fixed_ids.bids + IdMap.mk_map_ref fixed_ids.blids in let borrow_id_map = let module IdMap = IdMap (V.BorrowId) in @@ -1797,7 +1797,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) let check_equiv = check_equiv let ctx = ctx0 let rid_map = rid_map - let bid_map = bid_map + let blid_map = blid_map let borrow_id_map = borrow_id_map let loan_id_map = loan_id_map let sid_map = sid_map @@ -1811,7 +1811,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) (* Small utility: check that ids are fixed/mapped to themselves *) let ids_are_fixed (ids : ids_sets) : bool = - let { aids; bids = _; borrow_ids; loan_ids; dids; rids; sids } = ids in + let { aids; blids = _; borrow_ids; loan_ids; dids; rids; sids } = ids in V.AbstractionId.Set.subset aids fixed_ids.aids && V.BorrowId.Set.subset borrow_ids fixed_ids.borrow_ids && V.BorrowId.Set.subset loan_ids fixed_ids.loan_ids @@ -1879,8 +1879,8 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) ("ctxs_are_equivalent: match_envs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- rid_map: " ^ T.RegionId.InjSubst.show_t !rid_map - ^ "\n- bid_map: " - ^ V.BorrowId.InjSubst.show_t !bid_map + ^ "\n- blid_map: " + ^ V.BorrowId.InjSubst.show_t !blid_map ^ "\n- sid_map: " ^ V.SymbolicValueId.InjSubst.show_t !sid_map ^ "\n- aid_map: " @@ -1956,7 +1956,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) let maps = { aid_map = !aid_map; - bid_map = !bid_map; + blid_map = !blid_map; borrow_id_map = !borrow_id_map; loan_id_map = !loan_id_map; rid_map = !rid_map; @@ -2133,24 +2133,26 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) | None -> let old_ids = compute_context_ids ctx0 in let new_ids = compute_contexts_ids !ctxs in - let bids = V.BorrowId.Set.diff old_ids.bids new_ids.bids in + let blids = V.BorrowId.Set.diff old_ids.blids new_ids.blids in let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in (* End those borrows and abstractions *) - let end_borrows_abs bids aids ctx = - let ctx = InterpreterBorrows.end_borrows_no_synth config bids ctx in + let end_borrows_abs blids aids ctx = + let ctx = + InterpreterBorrows.end_borrows_no_synth config blids ctx + in let ctx = InterpreterBorrows.end_abstractions_no_synth config aids ctx in ctx in (* End the borrows/abs in [ctx0] *) - let ctx0 = end_borrows_abs bids aids ctx0 in + let ctx0 = end_borrows_abs blids aids ctx0 in (* We can also do the same in the contexts [ctxs]: if there are several contexts, maybe one of them ended some borrows and some others didn't. As we need to end those borrows anyway (the join will detect them and ask to end them) we do it preemptively. *) - ctxs := List.map (end_borrows_abs bids aids) !ctxs; + ctxs := List.map (end_borrows_abs blids aids) !ctxs; fixed_ids := Some (compute_context_ids ctx0); ctx0 in @@ -2171,14 +2173,14 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) intersection of ids between the original environment and [ctx1] and [ctx2] *) let fixed_ids = compute_context_ids (Option.get !ctx_upon_entry) in - let { aids; bids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in + let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in let fixed_ids1 = compute_context_ids ctx1 in let fixed_ids2 = compute_context_ids ctx2 in let sids = V.SymbolicValueId.Set.inter sids (V.SymbolicValueId.Set.inter fixed_ids1.sids fixed_ids2.sids) in - let fixed_ids = { aids; bids; borrow_ids; loan_ids; dids; rids; sids } in + 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) : bool = @@ -2213,6 +2215,30 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) in let fp = compute_fixed_point ctx0 max_num_iter in let fixed_ids = compute_fixed_ids (Option.get !ctx_upon_entry) fp in + (* For now, all the new abstractions in the fixed-point have the same region + group (of id 0): 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 region_map = ref T.RegionId.Map.empty in + let get_rid (rid : T.RegionId.id) : T.RegionId.id = + if T.RegionId.Set.mem rid fixed_ids.rids then rid + else + match T.RegionId.Map.find_opt rid !region_map with + | Some rid -> rid + | None -> + let nrid = C.fresh_region_id () in + region_map := T.RegionId.Map.add rid nrid !region_map; + nrid + in + let introduce_fresh_rids = + object + inherit [_] C.map_eval_ctx + method! visit_region_id _ rid = get_rid rid + 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, fixed_ids) (** Split an environment between the fixed abstractions, values, etc. and @@ -2261,14 +2287,14 @@ type borrow_loan_corresp = { } let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = - let { aids; bids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } = + let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } = ids in let empty = V.BorrowId.Set.empty in let ids = { aids; - bids = empty; + blids = empty; borrow_ids = empty; loan_ids = empty; dids; diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index f5932d47..dba2e7cd 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -269,8 +269,7 @@ let value_has_loans_or_borrows (ctx : C.eval_ctx) (v : V.value) : bool = (** See {!compute_typed_value_ids}, {!compute_context_ids}, etc. *) type ids_sets = { aids : V.AbstractionId.Set.t; - bids : V.BorrowId.Set.t; - (** All the borrow/loan ids. TODO: rename to [blids] *) + blids : V.BorrowId.Set.t; (** All the borrow/loan ids *) borrow_ids : V.BorrowId.Set.t; (** Only the borrow ids *) loan_ids : V.BorrowId.Set.t; (** Only the loan ids *) dids : C.DummyVarId.Set.t; @@ -280,7 +279,7 @@ type ids_sets = { [@@deriving show] let compute_ids () = - let bids = ref V.BorrowId.Set.empty in + let blids = ref V.BorrowId.Set.empty in let borrow_ids = ref V.BorrowId.Set.empty in let loan_ids = ref V.BorrowId.Set.empty in let aids = ref V.AbstractionId.Set.empty in @@ -291,7 +290,7 @@ let compute_ids () = let get_ids () = { aids = !aids; - bids = !bids; + blids = !blids; borrow_ids = !borrow_ids; loan_ids = !loan_ids; dids = !dids; @@ -305,11 +304,11 @@ let compute_ids () = method! visit_dummy_var_id _ did = dids := C.DummyVarId.Set.add did !dids method! visit_borrow_id _ id = - bids := V.BorrowId.Set.add id !bids; + blids := V.BorrowId.Set.add id !blids; borrow_ids := V.BorrowId.Set.add id !borrow_ids method! visit_loan_id _ id = - bids := V.BorrowId.Set.add id !bids; + blids := V.BorrowId.Set.add id !blids; loan_ids := V.BorrowId.Set.add id !loan_ids method! visit_abstraction_id _ id = |