diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 44 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 51 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 16 |
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 |