summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-13 21:24:58 +0100
committerSon Ho2022-01-13 21:24:58 +0100
commite9c3dfc34d7cac0d2449b4d11db5adf7218b25db (patch)
treeac838adf50a7051918a9d2169f139b03bde14173 /src
parent01cde7e6ddc047c2ea13365a67555ed1defbe1e4 (diff)
Introduce ended borrow/loan projectors over symbolic values
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml85
-rw-r--r--src/InterpreterExpansion.ml2
-rw-r--r--src/InterpreterUtils.ml4
-rw-r--r--src/Print.ml2
-rw-r--r--src/Values.ml2
5 files changed, 57 insertions, 38 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index c471faf7..067b867e 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -976,7 +976,7 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id)
super#visit_AEndedIgnoredMutLoan env given_back child
| V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
- method! visit_ASymbolic env sproj =
+ method! visit_ASymbolic _ sproj =
match sproj with
| V.AProjBorrows (_, _) -> ()
| V.AProjLoans sv -> raise (FoundSymbolicValue sv)
@@ -1007,6 +1007,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
(* Note that the abstraction mustn't contain any loans *)
(* We end the borrows, starting with the *inner* ones. This is important
when considering nested borrows which have the same lifetime.
+ TODO: is that really important?
For instance:
```
@@ -1057,6 +1058,12 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
| V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
(* Nothing to do for ignored borrows *)
()
+
+ method! visit_ASymbolic _ sproj =
+ match sproj with
+ | V.AProjLoans _ -> failwith "Unexpected"
+ | V.AProjBorrows (sv, proj_ty) ->
+ raise (FoundAProjBorrows (sv, proj_ty))
end
in
(* Lookup the abstraction *)
@@ -1067,42 +1074,44 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
(* No borrows: nothing to update *)
ctx
with
- (* There are borrows: end them, then reexplore *)
+ (* There are concrete borrows: end them, then reexplore *)
| FoundABorrowContent bc ->
- (* First, replace the borrow by ⊥ *)
- let bid =
- match bc with
- | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
- | V.AProjSharedBorrow asb -> (
- (* There should be at least one borrow identifier in the set, which we
- * can use to identify the whole set *)
- match
- List.find
- (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
- asb
- with
- | V.AsbBorrow bid -> bid
- | _ -> failwith "Unexpected")
- | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
- failwith "Unexpected"
- in
- let ctx = update_aborrow ek_all bid V.ABottom ctx in
- (* Then give back the value *)
- let ctx =
- match bc with
- | V.AMutBorrow (bid, av) ->
- (* First, convert the avalue to a (fresh symbolic) value *)
- let v = convert_avalue_to_value av in
- give_back_value config bid v ctx
- | V.ASharedBorrow bid -> give_back_shared config bid ctx
- | V.AProjSharedBorrow _ ->
- (* Nothing to do *)
- ctx
- | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
- failwith "Unexpected"
- in
- (* Reexplore *)
- end_abstraction_borrows config abs_id ctx
+ (* First, replace the borrow by ⊥ *)
+ let bid =
+ match bc with
+ | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
+ | V.AProjSharedBorrow asb -> (
+ (* There should be at least one borrow identifier in the set, which we
+ * can use to identify the whole set *)
+ match
+ List.find
+ (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
+ asb
+ with
+ | V.AsbBorrow bid -> bid
+ | _ -> failwith "Unexpected")
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+ failwith "Unexpected"
+ in
+ let ctx = update_aborrow ek_all bid V.ABottom ctx in
+ (* Then give back the value *)
+ let ctx =
+ match bc with
+ | V.AMutBorrow (bid, av) ->
+ (* First, convert the avalue to a (fresh symbolic) value *)
+ let v = convert_avalue_to_value av in
+ give_back_value config bid v ctx
+ | V.ASharedBorrow bid -> give_back_shared config bid ctx
+ | V.AProjSharedBorrow _ ->
+ (* Nothing to do *)
+ ctx
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+ failwith "Unexpected"
+ in
+ (* Reexplore *)
+ end_abstraction_borrows config abs_id ctx
+ (* There are symbolic borrows: end them, then reexplore *)
+ | FoundAProjBorrows (_sv, _proj_ty) -> raise Errors.Unimplemented
(** Remove an abstraction from the context, as well as all its references *)
and end_abstraction_remove_from_context (_config : C.config)
@@ -1133,8 +1142,8 @@ and end_abstraction_remove_from_context (_config : C.config)
intersecting proj_borrows, either in the concrete context or in an
abstraction
*)
-and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id)
- (regions : T.RegionId.set_t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
+and end_proj_loans_symbolic (_config : C.config) (_abs_id : V.AbstractionId.id)
+ (_regions : T.RegionId.set_t) (_sv : V.symbolic_value) (_ctx : C.eval_ctx) :
C.eval_ctx =
raise Errors.Unimplemented
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index e19f8bb4..18ec1ecc 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -75,6 +75,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
let proj_regions = current_abs.regions in
let ancestors_regions = current_abs.ancestors_regions in
match (aproj, proj_kind) with
+ | (V.AEndedProjLoans | V.AEndedProjBorrows), _ -> V.ASymbolic aproj
| V.AProjLoans sv, LoanProj ->
(* Check if this is the symbolic value we are looking for *)
if same_symbolic_id sv original_sv then
@@ -311,6 +312,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
match reborrow_ashared (Option.get proj_regions) sv proj_ty with
| None -> super#visit_ASymbolic proj_regions aproj
| Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
+ | AEndedProjLoans | AEndedProjBorrows -> V.ASymbolic aproj
end
in
(* Call the visitor *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index ce6bd0ce..9b272db8 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -133,6 +133,9 @@ exception FoundGLoanContent of g_loan_content
exception FoundSymbolicValue of V.symbolic_value
(** Utility exception *)
+exception FoundAProjBorrows of V.symbolic_value * T.rty
+(** Utility exception *)
+
let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
bool =
let obj =
@@ -146,6 +149,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
match aproj with
| AProjLoans sv | AProjBorrows (sv, _) ->
if sv.V.sv_id = sv_id then raise Found else ()
+ | AEndedProjLoans | AEndedProjBorrows -> ()
method! visit_abstract_shared_borrows _ asb =
let visit (asb : V.abstract_shared_borrow) : unit =
diff --git a/src/Print.ml b/src/Print.ml
index bc527acc..3869012a 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -315,6 +315,8 @@ module Values = struct
^ ")"
| AProjBorrows (sv, rty) ->
"proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
+ | AEndedProjLoans -> "ended_proj_loans"
+ | AEndedProjBorrows -> "ended_proj_borrows"
let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
string =
diff --git a/src/Values.ml b/src/Values.ml
index e8d4560e..41d8bd85 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -186,6 +186,8 @@ type aproj =
| AProjBorrows of symbolic_value * rty
(** Note that an AProjBorrows only operates on a value which is not below
a shared loan: under a shared loan, we use [abstract_shared_borrow]. *)
+ | AEndedProjLoans
+ | AEndedProjBorrows
[@@deriving show]
type region = RegionVarId.id Types.region [@@deriving show]