diff options
| -rw-r--r-- | src/Interpreter.ml | 167 |
1 files changed, 131 insertions, 36 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 79a06384..129b856b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -859,9 +859,14 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) - [regions]: the regions we project - [v]: the value over which we project - - [ty]: the type with regions which we use for the projection (to - map borrows to regions - or to interpret the borrows as belonging - to some regions...) + - [ty]: the projection type (is used to map borrows to regions, or to + interpret the borrows as belonging to some regions...). Remember that + `v` doesn't contain region information. + For instance, if we have: + `v <: ty` where: + - `v = mut_borrow l ...` + - `ty = Ref (r, ...)` + then we interpret the borrow `l` as belonging to region `r` Also, when applying projections on shared values, we need to apply reborrows. This is a bit annoying because, with the way we compute @@ -976,6 +981,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in { V.value; V.ty } +(** Apply (and reduce) a projector over loans to a value. + + TODO: detailed comments. See [apply_proj_borrows] +*) +let rec apply_proj_loans (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) + (regions : T.RegionId.set_t) (v : V.typed_value) : V.typed_avalue = + raise Unimplemented + (** Auxiliary function to end borrows: lookup a borrow in the environment, update it (by returning an updated environment where the borrow has been replaced by [Bottom])) if we can end the borrow (for instance, it is not @@ -2730,9 +2743,9 @@ let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t) let box_value = mk_box_value boxed_value in (ctx, box_value) -let compute_expanded_symbolic_ref_value (ended_regions : T.RegionId.set_t) +let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t) (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (ctx : C.eval_ctx) : C.eval_ctx = (* Check that we are allowed to expand the reference *) assert (not (region_in_set region ended_regions)); (* Match on the reference kind *) @@ -2745,6 +2758,80 @@ let compute_expanded_symbolic_ref_value (ended_regions : T.RegionId.set_t) raise Unimplemented | T.Shared -> raise Unimplemented +(** Apply a symbolic expansion to a context, by replacing the original + symbolic value with its expanded value. Is valid only if the expansion + is not a borrow (i.e., an adt...). +*) +let apply_symbolic_expansion_non_borrow (config : C.config) + (original_sv : V.symbolic_value) (expansion : V.typed_value) + (ctx : C.eval_ctx) : C.eval_ctx = + (* [apply_proj_borrows] needs a [fresh_reborrow] function, to generate + fresh identifiers and register reborrows, whenever needed. As we don't + expand borrows, we shouldn't have to apply reborrows. *) + let fresh_reborrow (_ : V.BorrowId.id) : V.BorrowId.id = + failwith "Unexpected reborrow" + in + (* For the projectors: it might happen that the expansion contains symbolic + variables with already ended regions. + *) + let check_symbolic_no_ended = false in + (* Visitor to apply the expansion *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Symbolic env spc = + if spc.V.svalue = original_sv then expansion.V.value + else super#visit_Symbolic env spc + (** Replace a symbolic value with its expansion. + Note that there may be several references to the same symbolic value + in the context, if the value has been copied. Expansion is then a bit + subtle in the case we expand shared borrows, in which case we need to + introduce a unique borrow identifier for every borrow (this is not + the case here: this function should NOT be used to expand borrows). + *) + + method! visit_abs proj_regions abs = + assert (Option.is_none proj_regions); + let proj_regions = Some abs.V.regions in + super#visit_abs proj_regions abs + (** When visiting an abstraction, we remember the regions it owns to be + able to properly reduce projectors when expanding symbolic values *) + + method! visit_ASymbolic proj_regions aproj = + let proj_regions = Option.get proj_regions in + match aproj with + | V.AProjLoans sv -> + (* Check if this is the symbolic value we are looking for *) + if sv = original_sv then + (* Apply the projector *) + let projected_value = + apply_proj_loans check_symbolic_no_ended ctx proj_regions + expansion + in + (* Replace *) + projected_value.V.value + else + (* Not the searched symbolic value: nothing to do *) + super#visit_ASymbolic (Some proj_regions) aproj + | V.AProjBorrows (sv, proj_ty) -> + (* Check if this is the symbolic value we are looking for *) + if sv = original_sv then + (* Apply the projector *) + let projected_value = + apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow + proj_regions expansion proj_ty + in + (* Replace *) + projected_value.V.value + else + (* Not the searched symbolic value: nothing to do *) + super#visit_ASymbolic (Some proj_regions) aproj + end + in + (* Apply the expansion *) + obj#visit_eval_ctx None ctx + (** Expand a symbolic value which is not an enumeration with several variants. This function is used when exploring a path. @@ -2755,39 +2842,47 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) * fresh symbolic values in the context (which thus gets updated) *) let rty = sp.V.svalue.V.sv_ty in let ended_regions = sp.V.rset_ended in - let ctx, nv = - match (pe, rty) with - (* "Regular" ADTs *) - | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> ( - assert (def_id = def_id'); - (* Compute the expanded value - there should be exactly one because we - * don't allow to expand enumerations with strictly more than one variant *) - let expand_enumerations = false in - match - compute_expanded_symbolic_adt_value expand_enumerations ended_regions - def_id opt_variant_id regions types ctx - with - | [ (ctx, nv) ] -> (ctx, nv) - | _ -> failwith "Unexpected") - (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> - assert (arity = List.length tys); - (* Generate the field values *) + match (pe, rty) with + (* "Regular" ADTs *) + | ( Field (ProjAdt (def_id, opt_variant_id), _), + T.Adt (T.AdtId def_id', regions, types) ) -> ( + assert (def_id = def_id'); + (* Compute the expanded value - there should be exactly one because we + * don't allow to expand enumerations with strictly more than one variant *) + let expand_enumerations = false in + match + compute_expanded_symbolic_adt_value expand_enumerations ended_regions + def_id opt_variant_id regions types ctx + with + | [ (ctx, nv) ] -> + (* Apply in the context *) + apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx + | _ -> failwith "Unexpected") + (* Tuples *) + | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> + assert (arity = List.length tys); + (* Generate the field values *) + let ctx, nv = compute_expanded_symbolic_tuple_value ended_regions tys ctx - (* Borrows *) - | Deref, T.Ref (region, ref_ty, rkind) -> - compute_expanded_symbolic_ref_value ended_regions region ref_ty rkind - ctx - (* Boxes *) - | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> + in + (* Apply in the context *) + apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx + (* Borrows *) + | Deref, T.Ref (region, ref_ty, rkind) -> + let _ = + expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx + in + raise Unimplemented + (* Boxes *) + | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> + let ctx, nv = compute_expanded_symbolic_box_value ended_regions boxed_ty ctx - | _ -> - failwith - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) - in - (* Update the context *) - raise Unimplemented + in + (* Apply in the context *) + apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx + | _ -> + failwith + ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) (** Update the environment to be able to read a place. |