diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 19 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 25 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 6 | ||||
| -rw-r--r-- | src/Print.ml | 2 |
4 files changed, 46 insertions, 6 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 26374bf7..a13ac786 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1442,12 +1442,22 @@ let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = - it mustn't contain [Bottom] - it mustn't contain inactivated borrows TODO: this kind of checks should be put in an auxiliary helper, because - they are redundant + they are redundant. + + The loan to update mustn't be a borrowed value. *) let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> - (* Lookup the shared loan *) + (* Debug *) + log#ldebug + (lazy + ("promote_shared_loan_to_mut_loan:\n- loan: " ^ V.BorrowId.to_string l + ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); + (* Lookup the shared loan - note that we can't promote a shared loan + * in a shared value, but we can do it in a mutably borrowed value. + * This is important because we can do: `let y = &two-phase ( *x );` + *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in @@ -1548,7 +1558,10 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) the borrow we want to promote *) let bids = V.BorrowId.Set.remove l bids in let cc = end_outer_borrows config bids in - (* Promote the loan *) + (* Promote the loan - TODO: this will fail if the value contains + * any loans. In practice, it shouldn't, but we could also + * look for loans inside the value and end them before promoting + * the borrow. *) let cc = comp cc (promote_shared_loan_to_mut_loan l) in (* Promote the borrow - the value should have been checked by [promote_shared_loan_to_mut_loan] diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index bdcadf3a..6bb2baf0 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -48,11 +48,20 @@ let expand_primitively_copyable_at_place (config : C.config) (* Apply *) expand cf ctx -(** Read a place (CPS-style function *) +(** Read a place (CPS-style function). + + We also check that the value *doesn't contain bottoms or inactivated + borrows. + *) let read_place (config : C.config) (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> let v = read_place_unwrap config access p ctx in + (* Check that there are no bottoms in the value *) + assert (not (bottom_in_value ctx.ended_regions v)); + (* Check that there are no inactivated borrows in the value *) + assert (not (inactivated_in_value v)); + (* Call the continuation *) cf v ctx (** Small utility. @@ -60,6 +69,14 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) Prepare the access to a place in a right-value (typically an operand) by reorganizing the environment. + We reorganize the environment so that: + - we can access the place (we prepare *along* the path) + - the value at the place itself doesn't contain loans (the `access_kind` + controls whether we only end mutable loans, or also shared loans). + + We also check, after the reorganization, that the value at the place + *doesn't contain any bottom nor inactivated borrows*. + [expand_prim_copy]: if true, expand the symbolic values which are primitively copyable and contain borrows. *) @@ -67,14 +84,20 @@ let access_rplace_reorganize_and_read (config : C.config) (expand_prim_copy : bool) (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> + (* Make sure we can evaluate the path *) let cc = update_ctx_along_read_place config access p in + (* End the proper loans at the place itself *) let cc = comp cc (end_loans_at_place config access p) in + (* Expand the copyable values which contain borrows (which are necessarily shared + * borrows) *) let cc = if expand_prim_copy then comp cc (expand_primitively_copyable_at_place config access p) else cc in + (* Read the place - note that this checks that the value doesn't contain bottoms *) let read_place = read_place config access p in + (* Compose *) comp cc read_place cf ctx let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 52742703..edd27138 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -304,7 +304,11 @@ let access_kind_to_projection_access (access : access_kind) : projection_access lookup_shared_borrows = false; } -(** Read the value at a given place *) +(** Read the value at a given place. + + Note that we only access the value at the place, and do not check that + the value is "well-formed" (for instance that it doesn't contain bottoms). + *) let read_place (config : C.config) (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : V.typed_value path_access_result = let access = access_kind_to_projection_access access in diff --git a/src/Print.ml b/src/Print.ml index 8e29bc67..af6fc982 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -948,7 +948,7 @@ module LlbcAst = struct match st with | A.Assign (p, rv) -> indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv - | A.FakeRead p -> "fake_read " ^ place_to_string fmt p + | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p | A.SetDiscriminant (p, variant_id) -> (* TODO: improve this to lookup the variant name by using the def id *) indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", " |