diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 364 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 18 | ||||
| -rw-r--r-- | src/Invariants.ml | 1 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 20 | ||||
| -rw-r--r-- | src/Values.ml | 7 |
8 files changed, 232 insertions, 189 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f38cb66e..d85c4bf8 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -77,7 +77,9 @@ module Test = struct (* Add the avalues to the abstractions and insert them in the context *) let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = (* Project over the values - we use *loan* projectors, as explained above *) - let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in + let avalues = + List.map (mk_aproj_loans_from_symbolic_value abs.regions) input_svs + in (* Insert the avalues in the abstraction *) let abs = { abs with avalues } in (* Insert the abstraction in the context *) diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index ebfd87c7..d8c2f3a8 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -316,9 +316,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) * and the given back value is thus a symbolic value *) match nv.V.value with | V.Symbolic sv -> + let abs = Option.get opt_abs in (* The loan projector *) let given_back_loans_proj = - mk_aproj_loans_from_symbolic_value sv + mk_aproj_loans_from_symbolic_value abs.regions sv in (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 18316610..ad8c8f53 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -18,8 +18,8 @@ type symbolic_expansion = (** Auxiliary function. Apply a proj_borrows on a shared borrow. - In the case of shared borrows, we return [abstract_shared_borrows], - not avalues. + Note that when projecting over shared values, we generate + [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) @@ -29,71 +29,74 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) * recursive call which is a bit overkill...) *) let ety = Subst.erase_regions ty in assert (ety = v.V.ty); - (* Project *) - match (v.V.value, ty) with - | V.Concrete _, (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 _, _ -> failwith "Unreachable" - | V.Symbolic s, _ -> - (* Check that the projection doesn't contain ended regions *) - assert (not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); - [ V.AsbProjReborrows (s, ty) ] - | _ -> failwith "Unreachable" + (* Project - if there are no regions from the abstraction in the type, return `_` *) + if not (ty_has_regions_in_set regions ty) then [] + else + match (v.V.value, ty) with + | V.Concrete _, (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 _, _ -> failwith "Unreachable" + | V.Symbolic s, _ -> + (* Check that the projection doesn't contain ended regions *) + assert ( + not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); + [ V.AsbProjReborrows (s, ty) ] + | _ -> failwith "Unreachable" (** Apply (and reduce) a projector over borrows to a value. @@ -135,114 +138,118 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) * recursive call which is a bit overkill...) *) let ety = Substitute.erase_regions ty in assert (ety = v.V.ty); - (* Match *) - let value : V.avalue = - match (v.V.value, ty) with - | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv - | 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 check_symbolic_no_ended ctx fresh_reborrow - regions ancestors_regions fv fty) - fields_types - in - V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } - | V.Bottom, _ -> failwith "Unreachable" - | V.Borrow bc, T.Ref (r, ref_ty, kind) -> - if - (* Check if the region is in the set of projected regions (note that - * we never project over static regions) *) - region_in_set r regions - then - (* In the set *) - let bc = - match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> - (* Apply the projection on the borrowed value *) - let bv = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions ancestors_regions bv ref_ty - in - V.AMutBorrow (bid, bv) - | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid - | V.InactivatedMutBorrow _, _ -> - failwith - "Can't apply a proj_borrow over an inactivated mutable borrow" - | _ -> failwith "Unreachable" + (* Project - if there are no regions from the abstraction in the type, return `_` *) + if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty } + else + let value : V.avalue = + match (v.V.value, ty) with + | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv + | 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 - V.ABorrow bc - else - (* Not in the set: ignore *) - let bc = - match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> - (* Apply the projection on the borrowed value *) - let bv = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions ancestors_regions bv ref_ty - in - (* If the borrow id is in the ancestor's regions, we still need - * to remember it *) - let opt_bid = - if region_in_set r ancestors_regions then Some bid else None - in - (* Return *) - V.AIgnoredMutBorrow (opt_bid, bv) - | 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 - V.AProjSharedBorrow asb - | V.InactivatedMutBorrow _, _ -> - failwith - "Can't apply a proj_borrow over an inactivated mutable borrow" - | _ -> failwith "Unreachable" + (* 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 check_symbolic_no_ended ctx fresh_reborrow + regions ancestors_regions fv fty) + fields_types in - V.ABorrow bc - | V.Loan _, _ -> failwith "Unreachable" - | V.Symbolic s, _ -> - (* Check that the projection doesn't contain already ended regions, - * if necessary *) - if check_symbolic_no_ended then ( - let ty1 = s.V.sv_ty in - let rset1 = ctx.ended_regions in - let ty2 = ty in - let rset2 = regions in - log#ldebug + V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } + | V.Bottom, _ -> failwith "Unreachable" + | V.Borrow bc, T.Ref (r, ref_ty, kind) -> + if + (* Check if the region is in the set of projected regions (note that + * we never project over static regions) *) + region_in_set r regions + then + (* In the set *) + let bc = + match (bc, kind) with + | V.MutBorrow (bid, bv), T.Mut -> + (* Apply the projection on the borrowed value *) + let bv = + apply_proj_borrows check_symbolic_no_ended ctx + fresh_reborrow regions ancestors_regions bv ref_ty + in + V.AMutBorrow (bid, bv) + | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid + | V.InactivatedMutBorrow _, _ -> + failwith + "Can't apply a proj_borrow over an inactivated mutable \ + borrow" + | _ -> failwith "Unreachable" + in + V.ABorrow bc + else + (* Not in the set: ignore *) + let bc = + match (bc, kind) with + | V.MutBorrow (bid, bv), T.Mut -> + (* Apply the projection on the borrowed value *) + let bv = + apply_proj_borrows check_symbolic_no_ended ctx + fresh_reborrow regions ancestors_regions bv ref_ty + in + (* If the borrow id is in the ancestor's regions, we still need + * to remember it *) + let opt_bid = + if region_in_set r ancestors_regions then Some bid else None + in + (* Return *) + V.AIgnoredMutBorrow (opt_bid, bv) + | 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 + V.AProjSharedBorrow asb + | V.InactivatedMutBorrow _, _ -> + failwith + "Can't apply a proj_borrow over an inactivated mutable \ + borrow" + | _ -> failwith "Unreachable" + in + V.ABorrow bc + | V.Loan _, _ -> failwith "Unreachable" + | V.Symbolic s, _ -> + (* Check that the projection doesn't contain already ended regions, + * if necessary *) + if check_symbolic_no_ended then ( + let ty1 = s.V.sv_ty in + let rset1 = ctx.ended_regions in + let ty2 = ty in + let rset2 = regions in + log#ldebug + (lazy + ("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1 + ^ "\n- rset1: " + ^ T.RegionId.set_to_string rset1 + ^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: " + ^ T.RegionId.set_to_string rset2 + ^ "\n")); + assert (not (projections_intersect ty1 rset1 ty2 rset2))); + V.ASymbolic (V.AProjBorrows (s, ty)) + | _ -> + log#lerror (lazy - ("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1 - ^ "\n- rset1: " - ^ T.RegionId.set_to_string rset1 - ^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: " - ^ T.RegionId.set_to_string rset2 - ^ "\n")); - assert (not (projections_intersect ty1 rset1 ty2 rset2))); - V.ASymbolic (V.AProjBorrows (s, ty)) - | _ -> - log#lerror - (lazy - ("apply_proj_borrows: unexpected inputs:\n- input value: " - ^ typed_value_to_string ctx v - ^ "\n- proj rty: " ^ rty_to_string ctx ty)); - failwith "Unreachable" - in - { V.value; V.ty } + ("apply_proj_borrows: unexpected inputs:\n- input value: " + ^ typed_value_to_string ctx v + ^ "\n- proj rty: " ^ rty_to_string ctx ty)); + failwith "Unreachable" + in + { V.value; V.ty } (** Convert a symbolic expansion *which is not a borrow* to a value *) let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) @@ -285,22 +292,25 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) *) let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue = + (* Sanity check: if we have a proj_loans over a symbolic value, it should + * contain regions which we will project *) + assert (ty_has_regions_in_set regions original_sv_ty); (* Match *) let (value, ty) : V.avalue * T.rty = match (see, original_sv_ty) with - | SeConcrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> - (V.AConcrete cv, original_sv_ty) + | SeConcrete _, (T.Bool | T.Char | T.Integer _ | T.Str) -> + (V.AIgnored, original_sv_ty) | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) -> (* Project over the field values *) let field_values = - List.map mk_aproj_loans_from_symbolic_value field_values + List.map (mk_aproj_loans_from_symbolic_value regions) field_values in (V.AAdt { V.variant_id; field_values }, original_sv_ty) | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_symbolic_value spc in + let child_av = mk_aproj_loans_from_symbolic_value regions spc in (* 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 @@ -313,7 +323,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_symbolic_value spc in + let child_av = mk_aproj_loans_from_symbolic_value regions spc in (* 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 diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index d172d1b7..3eb7322b 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -883,7 +883,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value ret_sv_ty in let ret_value = mk_typed_value_from_symbolic_value ret_spc in - let ret_av = mk_aproj_loans_from_symbolic_value ret_spc in + let ret_av regions = mk_aproj_loans_from_symbolic_value regions ret_spc in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in let args_with_rtypes = List.combine args inst_sg.A.inputs in @@ -908,7 +908,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) ctx args_with_rtypes in (* Group the input and output values *) - let avalues = List.append args_projs [ ret_av ] in + let avalues = List.append args_projs [ ret_av abs.regions ] in (* Add the avalues to the abstraction *) let abs = { abs with avalues } in (* Insert the abstraction in the context *) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 65502126..92c92807 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -67,12 +67,18 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : in av -(** Create a loans projector from a symbolic value. *) -let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) : - V.typed_avalue = - let av = V.ASymbolic (V.AProjLoans svalue) in - let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in - av +(** Create a loans projector from a symbolic value. + + Checks if the projector will actually project some regions. If not, + returns [AIgnored] (`_`). + *) +let mk_aproj_loans_from_symbolic_value (regions : T.RegionId.Set.t) + (svalue : V.symbolic_value) : V.typed_avalue = + if ty_has_regions_in_set regions svalue.sv_ty then + let av = V.ASymbolic (V.AProjLoans svalue) in + let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in + av + else { V.value = V.AIgnored; ty = svalue.V.sv_ty } (** TODO: move *) let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool diff --git a/src/Invariants.ml b/src/Invariants.ml index 23f7d456..24a02379 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -600,6 +600,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = let ty2 = Subst.erase_regions sv.V.sv_ty in assert (ty1 = ty2) | V.AEndedProjLoans | V.AEndedProjBorrows -> ()) + | V.AIgnored, _ -> () | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index 04a579bf..bda49608 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -109,6 +109,26 @@ let ty_has_regions (ty : ety) : bool = false with Found -> true +(** 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 = + object + inherit [_] iter_ty as super + + method! visit_Adt env type_id regions tys = + List.iter (fun r -> if region_in_set r rset then raise Found) regions; + super#visit_Adt env type_id regions tys + + method! visit_Ref env r ty rkind = + if region_in_set r rset then raise Found + else super#visit_Ref env r ty rkind + end + in + try + obj#visit_ty () ty; + false + with Found -> true + (** Return true if a type is "primitively copyable". * * "primitively copyable" means that copying instances of this type doesn't diff --git a/src/Values.ml b/src/Values.ml index 707986f8..9d25025e 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -236,7 +236,8 @@ class ['self] map_typed_avalue_base = *) type avalue = | AConcrete of constant_value - (** Note that this case is not used in the projections to keep track of the + (** TODO: remove + Note that this case is not used in the projections to keep track of the borrow graph (because there are no borrows in "concrete" values!) but to correctly instantiate the backward functions (we may give back some values at different moments: we need to remember what those values were @@ -250,7 +251,9 @@ type avalue = | ALoan of aloan_content | ABorrow of aborrow_content | ASymbolic of aproj - | AIgnored (** A value we don't own and thus ignore *) + | AIgnored + (** A value which doesn't contain borrows, or which borrows we + don't own and thus ignore *) and adt_avalue = { variant_id : (VariantId.id option[@opaque]); |