diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 37 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 6 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 22 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 8 | ||||
| -rw-r--r-- | src/Values.ml | 4 |
5 files changed, 68 insertions, 9 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 9331d9f3..034d566a 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -432,14 +432,39 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) let give_back_symbolic_value (_config : C.config) (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value) (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = - let subst (abs : V.abs) abs_proj_ty = - (* TODO: check that we can consume this symbolic value - this is not - * a precondition, purely a sanity check *) - raise Errors.Unimplemented; + let subst (_abs : V.abs) _abs_proj_ty = + (* Compute the projection over the given back value *) let child_proj = + (* If it is the same symbolic value, it means it was left unchanged: + * we don't have to project it *) if sv.sv_id = nsv.sv_id then None - else - Some (mk_aproj_borrows_from_symbolic_value abs.regions nsv abs_proj_ty) + else ( + (* Not the same symbolic value: it was updated (because given to a + * function or returned) *) + (* For now, we can only have the following case *) + assert (nsv.sv_kind = V.SynthGivenBack); + match nsv.sv_kind with + | V.SynthGivenBack -> + (* The given back value comes from the return value of the function + * we are currently synthesizing (as it is given back, it means + * we ended one of the regions appearing in the signature: we are + * currently synthesizing one of the backward functions *) + (* As we don't allow borrow overwrites on returned value, we can + * (and MUST) forget the borrows *) + None + | V.FunCallGivenBack -> + (* The value was fed as input to a function, and was given back *) + (* For now, we don't allow borrow overwrites on returned values, + * meaning the given back value can't have borrows below mutable + * borrows. *) + let has_borrow_below_mut = + ty_has_borrow_below_mut ctx.type_context.type_infos nsv.sv_ty + in + assert (not has_borrow_below_mut); + (* We don't allow overwrites: we must thus not project over the + * given back value *) + None + | _ -> failwith "Unreachable") in V.AEndedProjLoans child_proj in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 74886bf9..67a4bac5 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -905,7 +905,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) * be fed to functions (i.e., symbolic values output from function return * values and which contain borrows of borrows can't be used as function * inputs *) - raise Errors.Unimplemented; + assert ( + List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args); (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) let empty_absl = create_empty_abstractions_from_abs_region_groups V.FunCall diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index ca437593..be899c08 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -224,3 +224,25 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) : obj#visit_typed_value () v; false with Found -> true + +let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx) + (v : V.typed_value) : bool = + let obj = + object + inherit [_] V.iter_typed_value + + method! visit_symbolic_value _ s = + match s.sv_kind with + | V.FunCallRet -> + if ty_has_borrow_below_mut ctx.type_context.type_infos s.sv_ty then + raise Found + else () + | V.SynthInput -> () + | V.FunCallGivenBack | V.SynthGivenBack -> failwith "Unreachable" + end + in + (* We use exceptions *) + try + obj#visit_typed_value () v; + false + with Found -> true diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index ef260830..e34add63 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -92,7 +92,7 @@ let rec ety_no_regions_to_rty (ty : ety) : rty = "Can't convert a ref with erased regions to a ref with non-erased \ regions" -(** Retuns true if a type contains borrows. +(** Retuns true if the type contains borrows. Note that we can't simply explore the type and look for regions: sometimes we erase the lists of regions (by replacing them with `[]` when using `ety`, @@ -102,7 +102,7 @@ let ty_has_borrows (infos : TA.type_infos) (ty : 'r ty) : bool = let info = TA.analyze_ty infos ty in info.TA.contains_borrow -(** Retuns true if a type contains nested borrows. +(** Retuns true if the type contains nested borrows. Note that we can't simply explore the type and look for regions: sometimes we erase the lists of regions (by replacing them with `[]` when using `ety`, @@ -112,6 +112,10 @@ let ty_has_nested_borrows (infos : TA.type_infos) (ty : 'r ty) : bool = let info = TA.analyze_ty infos ty in info.TA.contains_nested_borrows +(** Retuns true if the type contains a borrow below a mutable borrow *) +let ty_has_borrow_below_mut (infos : TA.type_infos) (ty : 'r ty) : bool = + raise Errors.Unimplemented + (** Check if a [ty] contains regions from a given set *) let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool = let obj = diff --git a/src/Values.ml b/src/Values.ml index a64d4467..6386f8db 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -232,6 +232,10 @@ type aproj = (** When ending a proj_loans over a symbolic value, we may need to insert (and keep track of) a proj_borrows over the given back value, if the symbolic value was consumed by an abstraction then updated. + + Rk.: for now this is useless, because we forbid borrow overwrites on + returned values. A consequence is that when a proj_loans over a symbolic + value ends, we don't project the given back value. *) | AEndedProjBorrows (* TODO: remove AEndedProjBorrows? We might need it for synthesis, to contain |