summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoopsCore.ml44
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml51
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml16
3 files changed, 63 insertions, 48 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index cd609ab0..8d6caac4 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -429,3 +429,47 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
}
in
ids
+
+(* Small utility: Add a projection marker to a typed avalue.
+ This can be used in combination with List.map to add markers to an entire abstraction
+*)
+let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker)
+ (av : typed_avalue) : typed_avalue =
+ let obj =
+ object
+ inherit [_] map_typed_avalue as super
+
+ method! visit_borrow_content _ _ =
+ craise __FILE__ __LINE__ span "Unexpected borrow"
+
+ method! visit_loan_content _ _ =
+ craise __FILE__ __LINE__ span "Unexpected loan"
+
+ method! visit_symbolic_value _ sv =
+ sanity_check __FILE__ __LINE__
+ (not (symbolic_value_has_borrows ctx sv))
+ span;
+ sv
+
+ method! visit_aloan_content env lc =
+ match lc with
+ | AMutLoan (pm0, bid, av) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aloan_content env (AMutLoan (pm, bid, av))
+ | ASharedLoan (pm0, bids, av, child) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aloan_content env (ASharedLoan (pm, bids, av, child))
+ | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
+
+ method! visit_aborrow_content env bc =
+ match bc with
+ | AMutBorrow (pm0, bid, av) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aborrow_content env (AMutBorrow (pm, bid, av))
+ | ASharedBorrow (pm0, bid) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aborrow_content env (ASharedBorrow (pm, bid))
+ | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
+ end
+ in
+ obj#visit_typed_avalue () av
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 1e099d96..2f2dba41 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -664,58 +664,15 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
craise __FILE__ __LINE__ span "Unreachable"
in
- (* Add a projection marker to a typed avalue *)
- let add_marker_avalue (pm : proj_marker) (av : typed_avalue) : typed_avalue
- =
- let obj =
- object
- inherit [_] map_typed_avalue as super
-
- method! visit_borrow_content _ _ =
- craise __FILE__ __LINE__ span "Unexpected borrow"
-
- method! visit_loan_content _ _ =
- craise __FILE__ __LINE__ span "Unexpected loan"
-
- method! visit_symbolic_value _ sv =
- (* While ctx0 and ctx1 are different, we assume that the type info context is
- the same in both. Hence, we can use ctx0's types wlog *)
- sanity_check __FILE__ __LINE__
- (not (symbolic_value_has_borrows ctx0 sv))
- span;
- sv
-
- method! visit_aloan_content env lc =
- match lc with
- | AMutLoan (pm0, bid, av) ->
- sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
- super#visit_aloan_content env (AMutLoan (pm, bid, av))
- | ASharedLoan (pm0, bids, av, child) ->
- sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
- super#visit_aloan_content env
- (ASharedLoan (pm, bids, av, child))
- | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
-
- method! visit_aborrow_content env bc =
- match bc with
- | AMutBorrow (pm0, bid, av) ->
- sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
- super#visit_aborrow_content env (AMutBorrow (pm, bid, av))
- | ASharedBorrow (pm0, bid) ->
- sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
- super#visit_aborrow_content env (ASharedBorrow (pm, bid))
- | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
- end
- in
- obj#visit_typed_avalue () av
- in
-
(* Add projection marker to all abstractions in the left and right environments *)
let add_marker (pm : proj_marker) (ee : env_elem) : env_elem =
match ee with
| EAbs abs ->
EAbs
- { abs with avalues = List.map (add_marker_avalue pm) abs.avalues }
+ {
+ abs with
+ avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
+ }
| x -> x
in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 9b1d3dd0..713f462b 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -516,7 +516,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
(* Generate the avalues for the abstraction *)
- let mk_aborrow (pm: proj_marker) (bid : borrow_id) : typed_avalue =
+ let mk_aborrow (pm : proj_marker) (bid : borrow_id) : typed_avalue =
let value = ABorrow (ASharedBorrow (pm, bid)) in
{ value; ty = borrow_ty }
in
@@ -832,6 +832,20 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
convert_value_to_abstractions span abs_kind can_end
destructure_shared_values ctx v
in
+ (* Add a marker to the abstraction indicating the provenance of the value *)
+ let absl =
+ List.map
+ (fun abs ->
+ {
+ abs with
+ avalues =
+ List.map
+ (add_marker_avalue span ctx0
+ (if value_is_left then PLeft else PRight))
+ abs.avalues;
+ })
+ absl
+ in
push_absl absl;
(* Return [Bottom] *)
mk_bottom span v.ty