diff options
| -rw-r--r-- | src/Interpreter.ml | 152 | ||||
| -rw-r--r-- | src/Substitute.ml | 21 |
2 files changed, 148 insertions, 25 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 416ba44b..0ce4ff99 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -93,6 +93,9 @@ type exploration_kind = { functions behave, by restraining the kind of therms they can enter. *) +let ek_all : exploration_kind = + { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } + (** We sometimes need to return a value whose type may vary depending on whether we find it in a "concrete" value or an abstraction (ex.: loan contents when we perform environment lookups by using borrow ids) *) @@ -235,6 +238,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.AEndedIgnoredMutLoan { given_back; child } -> super#visit_AEndedIgnoredMutLoan env given_back child | V.AProjSharedLoan asb -> + (* TODO: is it correct to do this? *) (* Check the set of borrow ids *) if borrow_in_asb l asb then raise (FoundGLoanContent (Abstract lc)) else () @@ -662,6 +666,87 @@ let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) || projections_intersect ty1 rset1 ty2 rset2 | _ -> failwith "Unreachable" +(** Auxiliary function. + + Apply a proj_borrows on a shared borrow. + In the case of shared borrows, we return [abstract_shared_borrows], + not avalues. +*) +let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) + (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) + (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : + V.abstract_shared_borrows = + (* Sanity check - TODO: move this elsewhere (here we perform the check at every + * recursive call which is a bit overkill...) *) + let ety = Substitute.erase_regions ty in + assert (ety = v.V.ty); + (* Project *) + match (v.V.value, ty) with + | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> [] + | V.Adt adt, T.Adt (id, region_params, tys) -> + (* Retrieve the types of the fields *) + let field_types = + Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id + region_params tys + in + (* Project over the field values *) + let fields_types = List.combine adt.V.field_values field_types in + let proj_fields = + List.map + (fun (fv, fty) -> + apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv + fty) + fields_types + in + List.concat proj_fields + | V.Bottom, _ -> failwith "Unreachable" + | V.Borrow bc, T.Ref (r, ref_ty, kind) -> + (* Retrieve the bid of the borrow and the asb of the projected borrowed value *) + let bid, asb = + (* Not in the set: dive *) + match (bc, kind) with + | V.MutBorrow (bid, bv), T.Mut -> + (* Apply the projection on the borrowed value *) + let asb = + apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv + ref_ty + in + (bid, asb) + | V.SharedBorrow bid, T.Shared -> + (* Lookup the shared value *) + let ek = ek_all in + let sv = lookup_loan ek bid ctx in + let asb = + match sv with + | _, Concrete (V.SharedLoan (_, sv)) + | _, Abstract (V.ASharedLoan (_, sv, _)) -> + apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions + sv ref_ty + | _ -> failwith "Unexpected" + in + (bid, asb) + | V.InactivatedMutBorrow _, _ -> + failwith + "Can't apply a proj_borrow over an inactivated mutable borrow" + | _ -> failwith "Unreachable" + in + let asb = + (* Check if the region is in the set of projected regions (note that + * we never project over static regions) *) + if region_in_set r regions then + let bid' = fresh_reborrow bid in + V.AsbBorrow bid' :: asb + else asb + in + asb + | V.Loan lc, _ -> failwith "Unreachable" + | V.Symbolic s, _ -> + (* Check that the symbolic value doesn't contain already ended regions *) + assert ( + not (projections_intersect s.V.svalue.V.sv_ty s.V.rset_ended ty regions)); + [ V.AsbProjReborrows (s.V.svalue, ty) ] + | _ -> failwith "Unreachable" + (** Apply (and reduce) a projector over borrows to a value. - [regions]: the regions we project @@ -675,10 +760,9 @@ let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) the projection on borrows, we can't update the context immediately. Instead, we remember the list of borrows we have to insert in the context *afterwards*. - TODO: implement this. *) let rec apply_proj_borrows (ctx : C.eval_ctx) - (reborrows : (V.BorrowId.id * V.BorrowId.id) list ref) + (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : V.typed_avalue = (* Sanity check - TODO: move this elsewhere (here we perform the check at every @@ -692,26 +776,15 @@ let rec apply_proj_borrows (ctx : C.eval_ctx) | V.Adt adt, T.Adt (id, region_params, tys) -> (* Retrieve the types of the fields *) let field_types = - match id with - | T.AdtId id -> - (* Retrieve the types of the fields *) - Subst.ctx_adt_get_instantiated_field_rtypes ctx id - adt.V.variant_id region_params tys - | T.Tuple -> - assert (List.length region_params = 0); - tys - | T.Assumed aty -> ( - match aty with - | T.Box -> - assert (List.length region_params = 0); - assert (List.length tys = 1); - tys) + Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id + region_params tys in (* Project over the field values *) let fields_types = List.combine adt.V.field_values field_types in let proj_fields = List.map - (fun (fv, fty) -> apply_proj_borrows ctx reborrows regions fv fty) + (fun (fv, fty) -> + apply_proj_borrows ctx fresh_reborrow regions fv fty) fields_types in V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } @@ -727,7 +800,9 @@ let rec apply_proj_borrows (ctx : C.eval_ctx) match (bc, kind) with | V.MutBorrow (bid, bv), T.Mut -> (* Apply the projection on the borrowed value *) - let bv = apply_proj_borrows ctx reborrows regions bv ref_ty in + let bv = + apply_proj_borrows ctx fresh_reborrow regions bv ref_ty + in V.AMutBorrow (bid, bv) | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid | V.InactivatedMutBorrow _, _ -> @@ -742,11 +817,23 @@ let rec apply_proj_borrows (ctx : C.eval_ctx) match (bc, kind) with | V.MutBorrow (bid, bv), T.Mut -> (* Apply the projection on the borrowed value *) - let bv = apply_proj_borrows ctx reborrows regions bv ref_ty in + let bv = + apply_proj_borrows ctx fresh_reborrow regions bv ref_ty + in V.AIgnoredMutBorrow bv | V.SharedBorrow bid, T.Shared -> - (* TODO: we need the context to lookup the value *) - raise Unimplemented + (* Lookup the shared value *) + let ek = ek_all in + let sv = lookup_loan ek bid ctx in + let asb = + match sv with + | _, Concrete (V.SharedLoan (_, sv)) + | _, Abstract (V.ASharedLoan (_, sv, _)) -> + apply_proj_borrows_on_shared_borrow ctx fresh_reborrow + regions sv ref_ty + | _ -> failwith "Unexpected" + in + V.AProjSharedBorrow asb | V.InactivatedMutBorrow _, _ -> failwith "Can't apply a proj_borrow over an inactivated mutable borrow" @@ -1129,7 +1216,13 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) in (* We sometimes need to reborrow values while giving a value back due *) let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in - + let borrow_counter = ref ctx.C.borrow_counter in + let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id = + let bid', cnt' = V.BorrowId.fresh ctx.borrow_counter in + borrow_counter := cnt'; + reborrows := (bid, bid') :: !reborrows; + bid' + in let obj = object (self) inherit [_] C.map_eval_ctx as super @@ -1176,7 +1269,9 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* Register the insertion *) set_replaced (); (* Apply the projection *) - let given_back = apply_proj_borrows ctx reborrows regions nv ty in + let given_back = + apply_proj_borrows ctx fresh_reborrow regions nv ty + in (* Return the new value *) V.ALoan (V.AEndedMutLoan { given_back; child })) else @@ -1199,7 +1294,9 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) * mut loan. Also, this is not the loan we are looking for *per se*: * we don't register the fact that we inserted the value somewhere * (i.e., we don't call [set_replaced]) *) - let given_back = apply_proj_borrows ctx reborrows regions nv ty in + let given_back = + apply_proj_borrows ctx fresh_reborrow regions nv ty + in V.ALoan (V.AEndedIgnoredMutLoan { given_back; child }) else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) | V.AEndedIgnoredMutLoan { given_back; child } -> @@ -1229,9 +1326,14 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) match config.C.mode with | C.ConcreteMode -> (* Reborrows are introduced when applying projections in symbolic mode *) + assert (!borrow_counter = ctx.C.borrow_counter); assert (!reborrows = []); ctx - | C.SymbolicMode -> apply_reborrows !reborrows ctx + | C.SymbolicMode -> + (* Update the borrow counter *) + let ctx = { ctx with C.borrow_counter = !borrow_counter } in + (* Apply the reborrows *) + apply_reborrows !reborrows ctx in (* Return *) ctx diff --git a/src/Substitute.ml b/src/Substitute.ml index 42372c25..35304c29 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -92,6 +92,27 @@ let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx) let def = C.ctx_lookup_type_def ctx def_id in type_def_get_instantiated_field_rtypes def opt_variant_id regions types +(** Return the types of the properly instantiated ADT value (note that + here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *) +let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx) + (adt : V.adt_value) (id : T.type_id) + (region_params : T.RegionId.id T.region list) (type_params : T.rty list) : + T.rty list = + match id with + | T.AdtId id -> + (* Retrieve the types of the fields *) + ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id + region_params type_params + | T.Tuple -> + assert (List.length region_params = 0); + type_params + | T.Assumed aty -> ( + match aty with + | T.Box -> + assert (List.length region_params = 0); + assert (List.length type_params = 1); + type_params) + (** Instantiate the type variables in an ADT definition, and return the list of types of the fields for the chosen variant *) let type_def_get_instantiated_field_etypes (def : T.type_def) |