diff options
| -rw-r--r-- | src/Interpreter.ml | 316 |
1 files changed, 160 insertions, 156 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 9c806e8f..c871d530 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -69,12 +69,18 @@ let mk_box_value (v : V.typed_value) : V.typed_value = let box_v = V.Adt { variant_id = None; field_values = [ v ] } in mk_typed_value box_ty box_v -(** Create a fresh symbolic value (as a complementary projector) *) +(** Create a fresh symbolic proj comp *) let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp = let ctx, sv_id = C.fresh_symbolic_value_id ctx in let svalue = { V.sv_id; V.sv_ty = ty } in let sv = { V.svalue; rset_ended = ended_regions } in + (ctx, sv) + +(** Create a fresh symbolic value (as a complementary projector) *) +let mk_fresh_symbolic_proj_comp_value (ended_regions : T.RegionId.set_t) + (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ty ctx in let value : V.value = V.Symbolic sv in let ty : T.ety = Subst.erase_regions ty in let sv : V.typed_value = { V.value; ty } in @@ -2681,6 +2687,139 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) | Error _ -> failwith "Unreachable" | Ok ctx -> ctx +(** Projector kind *) +type proj_kind = LoanProj | BorrowProj + +(** Auxiliary function. + Apply a symbolic expansion to avalues in a context, targetting a specific + kind of projectors. + + [proj_kind] controls whether we apply the expansion to projectors + on loans or projectors on borrows. + + When dealing with reference expansion, it is necessary to first apply the + expansion on loan projectors, then on borrow projectors. The reason is + that reducing the borrow projectors might require to perform some reborrows, + in which case we need to lookup the corresponding loans in the context. + + [allow_reborrows] controls whether we allow reborrows or not. It is useful + only if we target borrow projectors. +*) +let apply_symbolic_expansion_to_target_avalues (config : C.config) + (allow_reborrows : bool) (proj_kind : proj_kind) + (original_sv : V.symbolic_value) (expansion : symbolic_expansion) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Symbolic values contained in the expansion might contain already ended regions *) + let check_symbolic_no_ended = false in + (* Prepare reborrows registration *) + let fresh_reborrow, apply_registered_reborrows = + prepare_reborrows config allow_reborrows ctx + in + (* Visitor to apply the expansion *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + 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, proj_kind) with + | V.AProjLoans sv, LoanProj -> + (* 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_on_symbolic_expansion ctx proj_regions + expansion sv.V.sv_ty + 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), BorrowProj -> + (* Check if this is the symbolic value we are looking for *) + if sv = original_sv then + (* Convert the symbolic expansion to a value on which we can + * apply a projector (if the expansion is a reference expansion, + * convert it to a borrow) *) + let expansion = + symbolic_expansion_to_value_with_borrows original_sv expansion + in + (* 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 + | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> + (* Nothing to do *) + super#visit_ASymbolic (Some proj_regions) aproj + end + in + (* Apply the expansion *) + let ctx = obj#visit_eval_ctx None ctx in + (* Apply the reborrows *) + apply_registered_reborrows ctx + +(** Auxiliary function. + Apply a symbolic expansion to avalues in a context. +*) +let apply_symbolic_expansion_to_avalues (config : C.config) + (allow_reborrows : bool) (original_sv : V.symbolic_value) + (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = + let apply_expansion proj_kind ctx = + apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind + original_sv expansion ctx + in + (* First target the loan projectors, then the borrow projectors *) + let ctx = apply_expansion LoanProj ctx in + let ctx = apply_expansion BorrowProj ctx in + ctx + +(** 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 : symbolic_expansion) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Convert the expansion to a value *) + let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in + (* Visitor to apply the expansion to *non-abstraction* values *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Symbolic env spc = + if spc.V.svalue = original_sv then nv.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). + *) + end + in + (* Apply the expansion to non-abstraction values *) + let ctx = obj#visit_eval_ctx None ctx in + (* Apply the expansion to abstraction values *) + let allow_reborrows = false in + apply_symbolic_expansion_to_avalues config allow_reborrows original_sv + expansion ctx + (** Compute an expanded ADT bottom value *) let compute_expanded_bottom_adt_value (tyctx : T.type_def list) (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) @@ -2795,7 +2934,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) (regions : T.RegionId.id T.region list) (types : T.rty list) - (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list = + (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list = (* Lookup the definition and check if it is an enumeration with several * variants *) let def = T.TypeDefId.nth ctx.type_context def_id in @@ -2810,42 +2949,40 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (* Initialize the expanded value for a given variant *) let initialize (ctx : C.eval_ctx) ((variant_id, field_types) : T.VariantId.id option * T.rty list) : - C.eval_ctx * V.typed_value = + C.eval_ctx * symbolic_expansion = let ctx, field_values = List.fold_left_map (fun ctx (ty : T.rty) -> mk_fresh_symbolic_proj_comp ended_regions ty ctx) ctx field_types in - let av = V.Adt { variant_id; field_values } in - let ty = T.Adt (T.AdtId def_id, regions, types) in - let ty = Subst.erase_regions ty in - (ctx, { V.value = av; V.ty }) + let see = SeAdt (variant_id, field_values) in + (ctx, see) in (* Initialize all the expanded values of all the variants *) List.map (initialize ctx) variants_fields_types let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) - (field_types : T.rty list) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (field_types : T.rty list) (ctx : C.eval_ctx) : + C.eval_ctx * symbolic_expansion = (* Generate the field values *) - let ctx, fields = + let ctx, field_values = List.fold_left_map (fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx) ctx field_types in - let v = V.Adt { variant_id = None; field_values = fields } in - let field_types = List.map Subst.erase_regions field_types in - let ty = T.Adt (T.Tuple, [], field_types) in - (ctx, { V.value = v; V.ty }) + let variant_id = None in + let see = SeAdt (variant_id, field_values) in + (ctx, see) let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t) - (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion = (* Introduce a fresh symbolic value *) let ctx, boxed_value = mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx in - let box_value = mk_box_value boxed_value in - (ctx, box_value) + let see = SeAdt (None, [ boxed_value ]) in + (ctx, see) 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) @@ -2862,139 +2999,6 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t) raise Unimplemented | T.Shared -> raise Unimplemented -(** Projector kind *) -type proj_kind = LoanProj | BorrowProj - -(** Auxiliary function. - Apply a symbolic expansion to avalues in a context, targetting a specific - kind of projectors. - - [proj_kind] controls whether we apply the expansion to projectors - on loans or projectors on borrows. - - When dealing with reference expansion, it is necessary to first apply the - expansion on loan projectors, then on borrow projectors. The reason is - that reducing the borrow projectors might require to perform some reborrows, - in which case we need to lookup the corresponding loans in the context. - - [allow_reborrows] controls whether we allow reborrows or not. It is useful - only if we target borrow projectors. -*) -let apply_symbolic_expansion_to_target_avalues (config : C.config) - (allow_reborrows : bool) (proj_kind : proj_kind) - (original_sv : V.symbolic_value) (expansion : symbolic_expansion) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Symbolic values contained in the expansion might contain already ended regions *) - let check_symbolic_no_ended = false in - (* Prepare reborrows registration *) - let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx - in - (* Visitor to apply the expansion *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - 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, proj_kind) with - | V.AProjLoans sv, LoanProj -> - (* 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_on_symbolic_expansion ctx proj_regions - expansion sv.V.sv_ty - 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), BorrowProj -> - (* Check if this is the symbolic value we are looking for *) - if sv = original_sv then - (* Convert the symbolic expansion to a value on which we can - * apply a projector (if the expansion is a reference expansion, - * convert it to a borrow) *) - let expansion = - symbolic_expansion_to_value_with_borrows original_sv expansion - in - (* 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 - | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> - (* Nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj - end - in - (* Apply the expansion *) - let ctx = obj#visit_eval_ctx None ctx in - (* Apply the reborrows *) - apply_registered_reborrows ctx - -(** Auxiliary function. - Apply a symbolic expansion to avalues in a context. -*) -let apply_symbolic_expansion_to_avalues (config : C.config) - (allow_reborrows : bool) (original_sv : V.symbolic_value) - (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = - let apply_expansion proj_kind ctx = - apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind - original_sv expansion ctx - in - (* First target the loan projectors, then the borrow projectors *) - let ctx = apply_expansion LoanProj ctx in - let ctx = apply_expansion BorrowProj ctx in - ctx - -(** 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 : symbolic_expansion) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Convert the expansion to a value *) - let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in - (* Visitor to apply the expansion to *non-abstraction* values *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic env spc = - if spc.V.svalue = original_sv then nv.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). - *) - end - in - (* Apply the expansion to non-abstraction values *) - let ctx = obj#visit_eval_ctx None ctx in - (* Apply the expansion to abstraction values *) - let allow_reborrows = false in - apply_symbolic_expansion_to_avalues config allow_reborrows original_sv - expansion ctx - (** Expand a symbolic value which is not an enumeration with several variants. This function is used when exploring a path. @@ -3030,12 +3034,6 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) 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 = @@ -3043,6 +3041,12 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) 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 | _ -> failwith ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) |