diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 11 | ||||
| -rw-r--r-- | src/SymbolicAstUtils.ml | 2 | ||||
| -rw-r--r-- | src/Values.ml | 10 |
3 files changed, 16 insertions, 7 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 6cf2c88f..f87d053c 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -314,8 +314,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) match nv.V.value with | V.Symbolic sv -> let abs = Option.get opt_abs in - (* Remember the given back value as a meta-value *) - let given_back_meta = nv in + (* Remember the given back value as a meta-value + * TODO: it is a bit annoying to have to deconstruct + * the value... Think about a more elegant way. *) + let given_back_meta = as_symbolic nv.value in (* The loan projector *) let given_back_loans_proj = mk_aproj_loans_value_from_symbolic_value abs.regions sv @@ -759,14 +761,14 @@ 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_given_back_value (abs_kind : V.abs_kind) - (av : V.typed_avalue) : V.typed_value = + (av : V.typed_avalue) : V.symbolic_value = let sv_kind = match abs_kind with | V.FunCall -> V.FunCallGivenBack | V.SynthRet -> V.SynthRetGivenBack | V.SynthInput -> V.SynthInputGivenBack in - mk_fresh_symbolic_typed_value sv_kind av.V.ty + mk_fresh_symbolic_value sv_kind av.V.ty (** End a borrow identified by its borrow id in a context. @@ -1168,6 +1170,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) let ended_borrow = V.ABorrow (V.AEndedMutBorrow (v, av)) in let ctx = update_aborrow ek_all bid ended_borrow ctx in (* Give the value back *) + let v = mk_typed_value_from_symbolic_value v in give_back_value config bid v ctx | V.ASharedBorrow bid -> (* Replace the shared borrow with bottom *) diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml index e74b381f..0f25e6b8 100644 --- a/src/SymbolicAstUtils.ml +++ b/src/SymbolicAstUtils.ml @@ -11,7 +11,7 @@ type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's type ended_loan = (V.mvalue, V.msymbolic_value list) ended -type ended_borrow = (V.mvalue, V.msymbolic_value) ended +type ended_borrow = (V.msymbolic_value, V.msymbolic_value) ended type ended_loan_or_borrow = | EndedLoan of ended_loan diff --git a/src/Values.ml b/src/Values.ml index 45bd5b6e..90250c63 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -195,12 +195,18 @@ type mvalue = typed_value [@@deriving show] Note that we never automatically visit the meta-values with the visitors: they really are meta information, and shouldn't be considered as part of the environment during a symbolic execution. + + TODO: we may want to create wrappers, to prevent mixing meta values + and regular values. *) type msymbolic_value = symbolic_value [@@deriving show] (** "Meta"-symbolic value. See the explanations for [mvalue] + + TODO: we may want to create wrappers, to prevent mixing meta values + and regular values. *) (** When giving shared borrows to functions (i.e., inserting shared borrows inside @@ -645,7 +651,7 @@ and aborrow_content = abstraction so that we can properly call the backward functions when generating the pure translation. *) - | AEndedMutBorrow of mvalue * typed_avalue + | AEndedMutBorrow of msymbolic_value * typed_avalue (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value that we gave back as a meta-value, to help with the synthesis. We also remember the child [avalue] because this structural information @@ -656,7 +662,7 @@ and aborrow_content = | AEndedIgnoredMutBorrow of { child : typed_avalue; given_back_loans_proj : typed_avalue; - given_back_meta : mvalue; + given_back_meta : msymbolic_value; (** [given_back_meta] is used to store the (symbolic) value we gave back upon ending the borrow. |