diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 31 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 47 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 8 |
3 files changed, 26 insertions, 60 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 3391a497..c4c090e3 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -454,8 +454,9 @@ let give_back_symbolic_value (_config : C.config) (sv : V.symbolic_value) end abstraction when ending this abstraction. When doing this, we need to convert the [avalue] to a [value] by introducing the proper symbolic values. *) -let give_back_avalue (_config : C.config) (bid : V.BorrowId.id) - (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx = +let give_back_avalue_to_same_abstraction (_config : C.config) + (bid : V.BorrowId.id) (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx + = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = @@ -490,8 +491,8 @@ let give_back_avalue (_config : C.config) (bid : V.BorrowId.id) let _, expected_ty, _ = ty_get_ref ty in if nv.V.ty <> expected_ty then ( log#serror - ("give_back_avalue: improper type:\n- expected: " - ^ rty_to_string ctx ty ^ "\n- received: " + ("give_back_avalue_to_same_abstraction: improper type:\n\ + - expected: " ^ rty_to_string ctx ty ^ "\n- received: " ^ rty_to_string ctx nv.V.ty); failwith "Value given back doesn't have the proper type"); (* This is the loan we are looking for: apply the projection to @@ -712,7 +713,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) (* Check that the corresponding loan is somewhere - purely a sanity check *) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) - give_back_avalue config l av ctx + give_back_avalue_to_same_abstraction config l av ctx | Abstract (V.ASharedBorrow l') -> (* Sanity check *) assert (l' = l); @@ -745,13 +746,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) a reference whose region has already ended). *) let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = - (* Convert the type *) - let ty = Subst.erase_regions av.V.ty in - (* Generate the fresh a symbolic value *) - let sv_id = C.fresh_symbolic_value_id () in - let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in - let value = V.Symbolic svalue in - { V.value; V.ty } + mk_fresh_symbolic_typed_value av.V.sv_ty (** End a borrow identified by its borrow id in a context @@ -1138,7 +1133,17 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) (* Reexplore *) end_abstraction_borrows config abs_id ctx (* There are symbolic borrows: end them, then reexplore *) - | FoundAProjBorrows (_sv, _proj_ty) -> raise Errors.Unimplemented + | FoundAProjBorrows (sv, proj_ty) -> + (* Replace the proj_borrows - there should be exactly one *) + let ctx = + update_intersecting_aproj_borrows_non_shared regions sv + V.AEndedProjBorrows ctx + in + (* Give back a fresh symbolic value *) + let nsv = mk_fresh_symbolic_typed_value proj_ty in + let ctx = give_back_symbolic_value config sv nsv ctx in + (* Reexplore *) + end_abstraction_borrows config abs_id ctx (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : C.config) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index e3789273..00d2cbb3 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -800,53 +800,6 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) update_intersecting_aproj_borrows can_update_shared update_shared update_non_shared regions sv ctx -(* -(** Updates the proj_loans intersecting some projection. - - Note that in practice, when we update a proj_loans, we always update exactly - one aproj_loans, in a specific abstraction. - - We make this function more general, by checking projection intersections - (rather than simply checking the abstraction and symbolic value ids) - for sanity checking: we check whether we need to update a loan based - on intersection criteria, but also check at the same time that we update - *exactly one* projector. - *) -let update_intersecting_aproj_loans (regions : T.RegionId.Set.t) - (sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = - (* Small helpers for sanity checks *) - let updated = ref false in - let update () : V.aproj = - assert (not !updated); - updated := true; - nv - in - (* The visitor *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_abs _ abs = super#visit_abs (Some abs) abs - - method! visit_aproj abs sproj = - match sproj with - | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows -> - super#visit_aproj abs sproj - | AProjLoans sv' -> - let abs = Option.get abs in - if proj_loans_intersect (regions, sv) (abs.regions, sv') then - update () - else super#visit_aproj (Some abs) sproj - end - in - (* Apply *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check that we updated the context at least once *) - assert !updated; - (* Return *) - ctx - *) - (** Substitute the proj_loans based an a symbolic id *) let substitute_aproj_loans_with_id (sv : V.symbolic_value) (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index e431aa30..2886f642 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -58,6 +58,14 @@ let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value = let svalue = { V.sv_id; V.sv_ty = ty } in svalue +(** Create a fresh symbolic value *) +let mk_fresh_symbolic_value (rty : T.rty) : V.symbolic_value = + let ty = Subst.erase_regions ty in + (* Generate the fresh a symbolic value *) + let value = mk_fresh_symbolic_value rty in + let value = V.Symbolic svalue in + { V.value; V.ty } + (** Create a typed value from a symbolic value. *) let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : V.typed_value = |