summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2022-12-07 14:28:21 +0100
committerSon HO2023-02-03 11:21:46 +0100
commitc86ecc916f9493bf312aa3f156e07da3bc415e77 (patch)
tree30696c3cb425bcaeed7d304fa15f44b40d5b3465 /compiler
parent7e42a6a6a5c0e8bb1638ea4dbdd75e8f89d0b7d6 (diff)
Make minor modifications
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Interpreter.ml4
-rw-r--r--compiler/InterpreterLoops.ml86
-rw-r--r--compiler/InterpreterUtils.ml11
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 =