diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Interpreter.ml | 484 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 490 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 17 |
3 files changed, 508 insertions, 483 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 7dc37dff..d8256186 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -15,6 +15,7 @@ open Utils open InterpreterUtils open InterpreterProjectors open InterpreterBorrows +open InterpreterExpansion (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -366,168 +367,6 @@ 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. - - Also, if this function is called on an expansion for *shared references*, - the proj borrows should already have been expanded. - - TODO: the way this function is used is a bit complex, especially because of - the above condition. Maybe we should have: - 1. a generic function to expand the loan projectors - 2. a function to expand the borrow projectors for non-borrows - 3. specialized functions for mut borrows and shared borrows - Note that 2. and 3. may have a little bit of duplicated code, but hopefully - it would make things clearer. -*) -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 same_symbolic_id sv original_sv then - (* Apply the projector *) - let projected_value = - apply_proj_loans_on_symbolic_expansion proj_regions expansion - original_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 same_symbolic_id 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) *) - (* WARNING: we mustn't get there if the expansion is for a shared - * reference. *) - let expansion = - symbolic_expansion_non_shared_borrow_to_value 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 - -(** Auxiliary function. - - Simply replace the symbolic values (*not avalues*) in the context with - a given value. Will break invariants if not used properly. -*) -let replace_symbolic_values (at_most_once : bool) - (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) : - C.eval_ctx = - (* Count *) - let replaced = ref false in - let replace () = - if at_most_once then assert (not !replaced); - replaced := true; - nv - in - (* Visitor to apply the substitution *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic env spc = - if same_symbolic_id spc.V.svalue original_sv then replace () - else super#visit_Symbolic env spc - end - in - (* Apply the substitution *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check that we substituted *) - assert !replaced; - (* Return *) - 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 = - (* Apply the expansion to non-abstraction values *) - let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in - let at_most_once = false in - let ctx = replace_symbolic_values at_most_once original_sv nv.V.value 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) @@ -630,312 +469,6 @@ let expand_bottom_value_from_projection (config : C.config) | Ok ctx -> ctx | Error _ -> failwith "Unreachable" -(** Compute the expansion of an adt value. - - The function might return a list of contexts and values if the symbolic - value to expand is an enumeration. - - `expand_enumerations` controls the expansion of enumerations: if false, it - doesn't allow the expansion of enumerations *containing several variants*. - *) -let compute_expanded_symbolic_adt_value (expand_enumerations : bool) - (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id) - (regions : T.RegionId.id T.region list) (types : T.rty 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 = C.ctx_lookup_type_def ctx def_id in - assert (List.length regions = List.length def.T.region_params); - (* Retrieve, for every variant, the list of its instantiated field types *) - let variants_fields_types = - Subst.type_def_get_instantiated_variants_fields_rtypes def regions types - in - (* Check if there is strictly more than one variant *) - if List.length variants_fields_types > 1 && not expand_enumerations then - failwith "Not allowed to expand enumerations with several variants"; - (* 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 * 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 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 * symbolic_expansion = - (* Generate the field values *) - 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 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 * symbolic_expansion = - (* Introduce a fresh symbolic value *) - let ctx, boxed_value = - mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx - in - let see = SeAdt (None, [ boxed_value ]) in - (ctx, see) - -let expand_symbolic_value_shared_borrow (config : C.config) - (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t) - (ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx = - (* First, replace the projectors on borrows (AProjBorrow and proj_comp) - * The important point is that the symbolic value to expand may appear - * several times, if it has been copied. In this case, we need to introduce - * one fresh borrow id per instance. - *) - let borrows = ref V.BorrowId.Set.empty in - let borrow_counter = ref ctx.C.borrow_counter in - let fresh_borrow () = - let bid', cnt' = V.BorrowId.fresh !borrow_counter in - borrow_counter := cnt'; - borrows := V.BorrowId.Set.add bid' !borrows; - bid' - in - (* Small utility used on shared borrows in abstractions (regular borrow - * projector and asb). - * Returns `Some` if the symbolic value has been expanded to an asb list, - * `None` otherwise *) - let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) : - V.abstract_shared_borrows option = - if same_symbolic_id sv original_sv then - match proj_ty with - | T.Ref (r, ref_ty, T.Shared) -> - (* Projector over the shared value *) - let shared_asb = V.AsbProjReborrows (sv, ref_ty) in - (* Check if the region is in the set of projected regions *) - if region_in_set r proj_regions then - (* In the set: we need to reborrow *) - let bid = fresh_borrow () in - Some [ V.AsbBorrow bid; shared_asb ] - else (* Not in the set: ignore *) - Some [ shared_asb ] - | _ -> failwith "Unexpected" - else None - in - (* Visitor to replace the projectors on borrows *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic env sv = - if same_symbolic_id sv.V.svalue original_sv then - let bid = fresh_borrow () in - V.Borrow (V.SharedBorrow bid) - else super#visit_Symbolic env sv - - 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 - - method! visit_AProjSharedBorrow proj_regions asb = - let expand_asb (asb : V.abstract_shared_borrow) : - V.abstract_shared_borrows = - match asb with - | V.AsbBorrow _ -> [ asb ] - | V.AsbProjReborrows (sv, proj_ty) -> ( - match reborrow_ashared (Option.get proj_regions) sv proj_ty with - | None -> [ asb ] - | Some asb -> asb) - in - let asb = List.concat (List.map expand_asb asb) in - V.AProjSharedBorrow asb - - method! visit_ASymbolic proj_regions aproj = - match aproj with - | AProjLoans _ -> - (* Loans are handled later *) - super#visit_ASymbolic proj_regions aproj - | AProjBorrows (sv, proj_ty) -> ( - (* Check if we need to reborrow *) - match reborrow_ashared (Option.get proj_regions) sv proj_ty with - | None -> super#visit_ASymbolic proj_regions aproj - | Some asb -> V.ABorrow (V.AProjSharedBorrow asb)) - end - in - (* Call the visitor *) - let ctx = obj#visit_eval_ctx None ctx in - let ctx = { ctx with C.borrow_counter = !borrow_counter } in - (* Finally, replace the projectors on loans *) - let bids = !borrows in - assert (not (V.BorrowId.Set.is_empty bids)); - let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in - let see = SeSharedRef (bids, shared_sv) in - let allow_reborrows = true in - let ctx = - apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see - ctx - in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx - -let expand_symbolic_value_borrow (config : C.config) - (original_sv : V.symbolic_value) (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 = - (* Check that we are allowed to expand the reference *) - assert (not (region_in_set region ended_regions)); - (* Match on the reference kind *) - match rkind with - | T.Mut -> - (* Simple case: simply create a fresh symbolic value and a fresh - * borrow id *) - let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in - let ctx, bid = C.fresh_borrow_id ctx in - let see = SeMutRef (bid, sv) in - (* Expand the symbolic values - we simply perform a substitution (and - * check that we perform exactly one substitution) *) - let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in - let at_most_once = true in - let ctx = - replace_symbolic_values at_most_once original_sv nv.V.value ctx - in - (* Expand the symbolic avalues *) - let allow_reborrows = true in - let ctx = - apply_symbolic_expansion_to_avalues config allow_reborrows original_sv - see ctx - in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx - | T.Shared -> - expand_symbolic_value_shared_borrow config original_sv ended_regions - ref_ty ctx - -(** Expand a symbolic value which is not an enumeration with several variants - (i.e., in a situation where it doesn't lead to branching). - - This function is used when exploring paths. - *) -let expand_symbolic_value_no_branching (config : C.config) - (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : - C.eval_ctx = - (* Compute the expanded value - note that when doing so, we may introduce - * fresh symbolic values in the context (which thus gets updated) *) - let original_sv = sp.V.svalue in - let rty = original_sv.V.sv_ty in - let ended_regions = sp.V.rset_ended in - let ctx = - 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 regions types ctx - with - | [ (ctx, see) ] -> - (* Apply in the context *) - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx - in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx - | _ -> failwith "Unexpected") - (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> - assert (arity = List.length tys); - (* Generate the field values *) - let ctx, see = - compute_expanded_symbolic_tuple_value ended_regions tys ctx - in - (* Apply in the context *) - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx - in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx - (* Boxes *) - | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> - let ctx, see = - compute_expanded_symbolic_box_value ended_regions boxed_ty ctx - in - (* Apply in the context *) - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx - in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx - (* Borrows *) - | Deref, T.Ref (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config original_sv ended_regions region - ref_ty rkind ctx - | _ -> - failwith - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) - in - (* Sanity check: the symbolic value has disappeared *) - assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); - (* Return *) - ctx - -(** Expand a symbolic enumeration value. - - This might lead to branching. - *) -let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp) - (ctx : C.eval_ctx) : C.eval_ctx list = - (* Compute the expanded value - note that when doing so, we may introduce - * fresh symbolic values in the context (which thus gets updated) *) - let original_sv = sp.V.svalue in - let rty = original_sv.V.sv_ty in - let ended_regions = sp.V.rset_ended in - match rty with - (* The value should be a "regular" ADTs *) - | T.Adt (T.AdtId def_id, regions, types) -> - (* 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 = true in - let res = - compute_expanded_symbolic_adt_value expand_enumerations ended_regions - def_id regions types ctx - in - (* Update the synthesized program *) - let seel = List.map (fun (_, x) -> x) res in - S.synthesize_symbolic_expansion_enum_branching original_sv seel; - (* Apply in the context *) - let apply (ctx, see) : C.eval_ctx = - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx - in - (* Sanity check: the symbolic value has disappeared *) - assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); - (* Return *) - ctx - in - List.map apply res - | _ -> failwith "Unexpected" - (** Update the environment to be able to read a place. When reading a place, we may be stuck along the way because some value @@ -1209,21 +742,6 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) ctx with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx) -(** Return true if a type is "primitively copyable". - * - * "primitively copyable" means that copying instances of this type doesn't - * require calling dedicated functions defined through the Copy trait. It - * is the case for types like integers, shared borrows, etc. - *) -let rec type_is_primitively_copyable (ty : T.ety) : bool = - match ty with - | T.Adt ((T.AdtId _ | T.Assumed _), _, _) -> false - | T.Adt (T.Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys - | T.TypeVar _ | T.Never | T.Str | T.Array _ | T.Slice _ -> false - | T.Bool | T.Char | T.Integer _ -> true - | T.Ref (_, _, T.Mut) -> false - | T.Ref (_, _, T.Shared) -> true - (** Copy a value, and return the resulting value. Note that copying values might update the context. For instance, when diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml new file mode 100644 index 00000000..7b249717 --- /dev/null +++ b/src/InterpreterExpansion.ml @@ -0,0 +1,490 @@ +(* This module provides the functions which handle expansion of symbolic values. + * For now, this file doesn't handle expansion of ⊥ values because they need + * some path utilities for replacement. We might change that in the future (by + * using indices to identify the values for instance). *) + +module T = Types +module V = Values +open Scalars +module E = Expressions +open Errors +module C = Contexts +module Subst = Substitute +module A = CfimAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = Synthesis +open Utils +open InterpreterUtils +open InterpreterProjectors +open InterpreterBorrows + +(** 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. + + Also, if this function is called on an expansion for *shared references*, + the proj borrows should already have been expanded. + + TODO: the way this function is used is a bit complex, especially because of + the above condition. Maybe we should have: + 1. a generic function to expand the loan projectors + 2. a function to expand the borrow projectors for non-borrows + 3. specialized functions for mut borrows and shared borrows + Note that 2. and 3. may have a little bit of duplicated code, but hopefully + it would make things clearer. +*) +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 same_symbolic_id sv original_sv then + (* Apply the projector *) + let projected_value = + apply_proj_loans_on_symbolic_expansion proj_regions expansion + original_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 same_symbolic_id 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) *) + (* WARNING: we mustn't get there if the expansion is for a shared + * reference. *) + let expansion = + symbolic_expansion_non_shared_borrow_to_value 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 + +(** Auxiliary function. + + Simply replace the symbolic values (*not avalues*) in the context with + a given value. Will break invariants if not used properly. +*) +let replace_symbolic_values (at_most_once : bool) + (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) : + C.eval_ctx = + (* Count *) + let replaced = ref false in + let replace () = + if at_most_once then assert (not !replaced); + replaced := true; + nv + in + (* Visitor to apply the substitution *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Symbolic env spc = + if same_symbolic_id spc.V.svalue original_sv then replace () + else super#visit_Symbolic env spc + end + in + (* Apply the substitution *) + let ctx = obj#visit_eval_ctx None ctx in + (* Check that we substituted *) + assert !replaced; + (* Return *) + 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 = + (* Apply the expansion to non-abstraction values *) + let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in + let at_most_once = false in + let ctx = replace_symbolic_values at_most_once original_sv nv.V.value 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 the expansion of an adt value. + + The function might return a list of contexts and values if the symbolic + value to expand is an enumeration. + + `expand_enumerations` controls the expansion of enumerations: if false, it + doesn't allow the expansion of enumerations *containing several variants*. + *) +let compute_expanded_symbolic_adt_value (expand_enumerations : bool) + (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id) + (regions : T.RegionId.id T.region list) (types : T.rty 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 = C.ctx_lookup_type_def ctx def_id in + assert (List.length regions = List.length def.T.region_params); + (* Retrieve, for every variant, the list of its instantiated field types *) + let variants_fields_types = + Subst.type_def_get_instantiated_variants_fields_rtypes def regions types + in + (* Check if there is strictly more than one variant *) + if List.length variants_fields_types > 1 && not expand_enumerations then + failwith "Not allowed to expand enumerations with several variants"; + (* 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 * 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 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 * symbolic_expansion = + (* Generate the field values *) + 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 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 * symbolic_expansion = + (* Introduce a fresh symbolic value *) + let ctx, boxed_value = + mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx + in + let see = SeAdt (None, [ boxed_value ]) in + (ctx, see) + +let expand_symbolic_value_shared_borrow (config : C.config) + (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t) + (ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx = + (* First, replace the projectors on borrows (AProjBorrow and proj_comp) + * The important point is that the symbolic value to expand may appear + * several times, if it has been copied. In this case, we need to introduce + * one fresh borrow id per instance. + *) + let borrows = ref V.BorrowId.Set.empty in + let borrow_counter = ref ctx.C.borrow_counter in + let fresh_borrow () = + let bid', cnt' = V.BorrowId.fresh !borrow_counter in + borrow_counter := cnt'; + borrows := V.BorrowId.Set.add bid' !borrows; + bid' + in + (* Small utility used on shared borrows in abstractions (regular borrow + * projector and asb). + * Returns `Some` if the symbolic value has been expanded to an asb list, + * `None` otherwise *) + let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) : + V.abstract_shared_borrows option = + if same_symbolic_id sv original_sv then + match proj_ty with + | T.Ref (r, ref_ty, T.Shared) -> + (* Projector over the shared value *) + let shared_asb = V.AsbProjReborrows (sv, ref_ty) in + (* Check if the region is in the set of projected regions *) + if region_in_set r proj_regions then + (* In the set: we need to reborrow *) + let bid = fresh_borrow () in + Some [ V.AsbBorrow bid; shared_asb ] + else (* Not in the set: ignore *) + Some [ shared_asb ] + | _ -> failwith "Unexpected" + else None + in + (* Visitor to replace the projectors on borrows *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Symbolic env sv = + if same_symbolic_id sv.V.svalue original_sv then + let bid = fresh_borrow () in + V.Borrow (V.SharedBorrow bid) + else super#visit_Symbolic env sv + + 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 + + method! visit_AProjSharedBorrow proj_regions asb = + let expand_asb (asb : V.abstract_shared_borrow) : + V.abstract_shared_borrows = + match asb with + | V.AsbBorrow _ -> [ asb ] + | V.AsbProjReborrows (sv, proj_ty) -> ( + match reborrow_ashared (Option.get proj_regions) sv proj_ty with + | None -> [ asb ] + | Some asb -> asb) + in + let asb = List.concat (List.map expand_asb asb) in + V.AProjSharedBorrow asb + + method! visit_ASymbolic proj_regions aproj = + match aproj with + | AProjLoans _ -> + (* Loans are handled later *) + super#visit_ASymbolic proj_regions aproj + | AProjBorrows (sv, proj_ty) -> ( + (* Check if we need to reborrow *) + match reborrow_ashared (Option.get proj_regions) sv proj_ty with + | None -> super#visit_ASymbolic proj_regions aproj + | Some asb -> V.ABorrow (V.AProjSharedBorrow asb)) + end + in + (* Call the visitor *) + let ctx = obj#visit_eval_ctx None ctx in + let ctx = { ctx with C.borrow_counter = !borrow_counter } in + (* Finally, replace the projectors on loans *) + let bids = !borrows in + assert (not (V.BorrowId.Set.is_empty bids)); + let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in + let see = SeSharedRef (bids, shared_sv) in + let allow_reborrows = true in + let ctx = + apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see + ctx + in + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching original_sv see; + (* Return *) + ctx + +let expand_symbolic_value_borrow (config : C.config) + (original_sv : V.symbolic_value) (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 = + (* Check that we are allowed to expand the reference *) + assert (not (region_in_set region ended_regions)); + (* Match on the reference kind *) + match rkind with + | T.Mut -> + (* Simple case: simply create a fresh symbolic value and a fresh + * borrow id *) + let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in + let ctx, bid = C.fresh_borrow_id ctx in + let see = SeMutRef (bid, sv) in + (* Expand the symbolic values - we simply perform a substitution (and + * check that we perform exactly one substitution) *) + let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in + let at_most_once = true in + let ctx = + replace_symbolic_values at_most_once original_sv nv.V.value ctx + in + (* Expand the symbolic avalues *) + let allow_reborrows = true in + let ctx = + apply_symbolic_expansion_to_avalues config allow_reborrows original_sv + see ctx + in + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching original_sv see; + (* Return *) + ctx + | T.Shared -> + expand_symbolic_value_shared_borrow config original_sv ended_regions + ref_ty ctx + +(** Expand a symbolic value which is not an enumeration with several variants + (i.e., in a situation where it doesn't lead to branching). + + This function is used when exploring paths. + *) +let expand_symbolic_value_no_branching (config : C.config) + (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : + C.eval_ctx = + (* Compute the expanded value - note that when doing so, we may introduce + * fresh symbolic values in the context (which thus gets updated) *) + let original_sv = sp.V.svalue in + let rty = original_sv.V.sv_ty in + let ended_regions = sp.V.rset_ended in + let ctx = + 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 regions types ctx + with + | [ (ctx, see) ] -> + (* Apply in the context *) + let ctx = + apply_symbolic_expansion_non_borrow config original_sv see ctx + in + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching original_sv see; + (* Return *) + ctx + | _ -> failwith "Unexpected") + (* Tuples *) + | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> + assert (arity = List.length tys); + (* Generate the field values *) + let ctx, see = + compute_expanded_symbolic_tuple_value ended_regions tys ctx + in + (* Apply in the context *) + let ctx = + apply_symbolic_expansion_non_borrow config original_sv see ctx + in + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching original_sv see; + (* Return *) + ctx + (* Boxes *) + | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> + let ctx, see = + compute_expanded_symbolic_box_value ended_regions boxed_ty ctx + in + (* Apply in the context *) + let ctx = + apply_symbolic_expansion_non_borrow config original_sv see ctx + in + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching original_sv see; + (* Return *) + ctx + (* Borrows *) + | Deref, T.Ref (region, ref_ty, rkind) -> + expand_symbolic_value_borrow config original_sv ended_regions region + ref_ty rkind ctx + | _ -> + failwith + ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) + in + (* Sanity check: the symbolic value has disappeared *) + assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); + (* Return *) + ctx + +(** Expand a symbolic enumeration value. + + This might lead to branching. + *) +let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp) + (ctx : C.eval_ctx) : C.eval_ctx list = + (* Compute the expanded value - note that when doing so, we may introduce + * fresh symbolic values in the context (which thus gets updated) *) + let original_sv = sp.V.svalue in + let rty = original_sv.V.sv_ty in + let ended_regions = sp.V.rset_ended in + match rty with + (* The value should be a "regular" ADTs *) + | T.Adt (T.AdtId def_id, regions, types) -> + (* 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 = true in + let res = + compute_expanded_symbolic_adt_value expand_enumerations ended_regions + def_id regions types ctx + in + (* Update the synthesized program *) + let seel = List.map (fun (_, x) -> x) res in + S.synthesize_symbolic_expansion_enum_branching original_sv seel; + (* Apply in the context *) + let apply (ctx, see) : C.eval_ctx = + let ctx = + apply_symbolic_expansion_non_borrow config original_sv see ctx + in + (* Sanity check: the symbolic value has disappeared *) + assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); + (* Return *) + ctx + in + List.map apply res + | _ -> failwith "Unexpected" diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index c652a1d3..dc5a0477 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -1,3 +1,5 @@ +(* TODO: most of the definitions in this file need to be moved elsewhere *) + module T = Types module V = Values open Scalars @@ -792,3 +794,18 @@ type outer_borrows_or_abs = exception FoundOuter of outer_borrows_or_abs (** Utility exception *) + +(** Return true if a type is "primitively copyable". + * + * "primitively copyable" means that copying instances of this type doesn't + * require calling dedicated functions defined through the Copy trait. It + * is the case for types like integers, shared borrows, etc. + *) +let rec type_is_primitively_copyable (ty : T.ety) : bool = + match ty with + | T.Adt ((T.AdtId _ | T.Assumed _), _, _) -> false + | T.Adt (T.Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys + | T.TypeVar _ | T.Never | T.Str | T.Array _ | T.Slice _ -> false + | T.Bool | T.Char | T.Integer _ -> true + | T.Ref (_, _, T.Mut) -> false + | T.Ref (_, _, T.Shared) -> true |