diff options
Diffstat (limited to 'compiler/InterpreterExpansion.ml')
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 180 |
1 files changed, 97 insertions, 83 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index a2550e88..3e1aeef2 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -48,8 +48,8 @@ type proj_kind = LoanProj | BorrowProj 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 : config) (meta : Meta.meta) - (allow_reborrows : bool) (proj_kind : proj_kind) +let apply_symbolic_expansion_to_target_avalues (config : config) + (meta : Meta.meta) (allow_reborrows : bool) (proj_kind : proj_kind) (original_sv : symbolic_value) (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx = (* Symbolic values contained in the expansion might contain already ended regions *) @@ -123,8 +123,9 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me in (* Apply the projector *) let projected_value = - apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow - proj_regions ancestors_regions expansion proj_ty + apply_proj_borrows meta check_symbolic_no_ended ctx + fresh_reborrow proj_regions ancestors_regions expansion + proj_ty in (* Replace *) projected_value.value @@ -150,8 +151,8 @@ let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta) (allow_reborrows : bool) (original_sv : symbolic_value) (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx = let apply_expansion proj_kind ctx = - apply_symbolic_expansion_to_target_avalues config meta allow_reborrows proj_kind - original_sv expansion ctx + apply_symbolic_expansion_to_target_avalues config meta 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 @@ -163,8 +164,8 @@ let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta) 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 (meta : Meta.meta) (at_most_once : bool) (original_sv : symbolic_value) - (nv : value) (ctx : eval_ctx) : eval_ctx = +let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) + (original_sv : symbolic_value) (nv : value) (ctx : eval_ctx) : eval_ctx = (* Count *) let replaced = ref false in let replace () = @@ -193,7 +194,9 @@ let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta) (* Apply the expansion to non-abstraction values *) let nv = symbolic_expansion_non_borrow_to_value meta original_sv expansion in let at_most_once = false in - let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in + let ctx = + replace_symbolic_values meta at_most_once original_sv nv.value ctx + in (* Apply the expansion to abstraction values *) let allow_reborrows = false in apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv @@ -209,13 +212,15 @@ let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta) [expand_enumerations] controls the expansion of enumerations: if false, it doesn't allow the expansion of enumerations *containing several variants*. *) -let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_enumerations : bool) - (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) : - symbolic_expansion list = +let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) + (expand_enumerations : bool) (def_id : TypeDeclId.id) + (generics : generic_args) (ctx : eval_ctx) : symbolic_expansion list = (* Lookup the definition and check if it is an enumeration with several * variants *) let def = ctx_lookup_type_decl ctx def_id in - sanity_check (List.length generics.regions = List.length def.generics.regions) meta; + sanity_check + (List.length generics.regions = List.length def.generics.regions) + meta; (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes meta ctx def @@ -236,8 +241,8 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e (* Initialize all the expanded values of all the variants *) List.map initialize variants_fields_types -let compute_expanded_symbolic_tuple_value (meta : Meta.meta) (field_types : rty list) : - symbolic_expansion = +let compute_expanded_symbolic_tuple_value (meta : Meta.meta) + (field_types : rty list) : symbolic_expansion = (* Generate the field values *) let field_values = List.map (fun sv_ty -> mk_fresh_symbolic_value meta sv_ty) field_types @@ -246,7 +251,8 @@ let compute_expanded_symbolic_tuple_value (meta : Meta.meta) (field_types : rty let see = SeAdt (variant_id, field_values) in see -let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : symbolic_expansion = +let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : + symbolic_expansion = (* Introduce a fresh symbolic value *) let boxed_value = mk_fresh_symbolic_value meta boxed_ty in let see = SeAdt (None, [ boxed_value ]) in @@ -261,19 +267,19 @@ let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : sy [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 (meta : Meta.meta) (expand_enumerations : bool) - (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) : - symbolic_expansion list = +let compute_expanded_symbolic_adt_value (meta : Meta.meta) + (expand_enumerations : bool) (adt_id : type_id) (generics : generic_args) + (ctx : eval_ctx) : symbolic_expansion list = match (adt_id, generics.regions, generics.types) with | TAdtId def_id, _, _ -> - compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id - generics ctx - | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value meta generics.types ] + compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations + def_id generics ctx + | TTuple, [], _ -> + [ compute_expanded_symbolic_tuple_value meta generics.types ] | TAssumed TBox, [], [ boxed_ty ] -> [ compute_expanded_symbolic_box_value meta boxed_ty ] | _ -> - craise - meta "compute_expanded_symbolic_adt_value: unexpected combination" + craise meta "compute_expanded_symbolic_adt_value: unexpected combination" let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) @@ -380,14 +386,14 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) let see = SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = - apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv see - ctx + apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv + see ctx in (* Call the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see - expr + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see expr (** TODO: simplify and merge with the other expansion function *) let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) @@ -407,23 +413,27 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) 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 meta original_sv see in + let nv = + symbolic_expansion_non_shared_borrow_to_value meta original_sv see + in let at_most_once = true in - let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in + let ctx = + replace_symbolic_values meta at_most_once original_sv nv.value ctx + in (* Expand the symbolic avalues *) let allow_reborrows = true in let ctx = - apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv - see ctx + apply_symbolic_expansion_to_avalues config meta allow_reborrows + original_sv see ctx in (* Apply the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place - see expr + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see expr | RShared -> - expand_symbolic_value_shared_borrow config meta original_sv original_sv_place - ref_ty cf ctx + expand_symbolic_value_shared_borrow config meta original_sv + original_sv_place ref_ty cf ctx (** A small helper. @@ -441,8 +451,8 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) We need this continuation separately (i.e., we can't compose it with the continuations in [see_cf_l]) because we perform a join *before* calling it. *) -let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Meta.meta) - (sv : symbolic_value) (sv_place : SA.mplace option) +let apply_branching_symbolic_expansions_non_borrow (config : config) + (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) (see_cf_l : (symbolic_expansion option * st_cm_fun) list) (cf_after_join : st_m_fun) : m_fun = fun ctx -> @@ -457,15 +467,19 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met let ctx = match see_opt with | None -> ctx - | Some see -> apply_symbolic_expansion_non_borrow config meta sv see ctx + | Some see -> + apply_symbolic_expansion_non_borrow config meta sv see ctx in (* Debug *) log#ldebug (lazy ("apply_branching_symbolic_expansions_non_borrow: " ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); + ^ "\n\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n")); (* Continuation *) cf_br cf_after_join ctx) see_cf_l @@ -484,9 +498,9 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met let seel = List.map fst see_cf_l in S.synthesize_symbolic_expansion meta sv sv_place seel subterms -let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_value) - (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun) - (cf_after_join : st_m_fun) : m_fun = +let expand_symbolic_bool (config : config) (meta : Meta.meta) + (sv : symbolic_value) (sv_place : SA.mplace option) (cf_true : st_cm_fun) + (cf_false : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = fun ctx -> (* Compute the expanded value *) let original_sv = sv in @@ -501,8 +515,8 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_val apply_branching_symbolic_expansions_non_borrow config meta original_sv original_sv_place seel cf_after_join ctx -let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv : symbolic_value) - (sv_place : SA.mplace option) : cm_fun = +let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) + (sv : symbolic_value) (sv_place : SA.mplace option) : cm_fun = fun cf ctx -> (* Debug *) log#ldebug @@ -523,8 +537,8 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv (* Compute the expanded value *) let allow_branching = false in let seel = - compute_expanded_symbolic_adt_value meta allow_branching adt_id generics - ctx + compute_expanded_symbolic_adt_value meta allow_branching adt_id + generics ctx in (* There should be exacly one branch *) let see = Collections.List.to_cons_nil seel in @@ -539,13 +553,12 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv original_sv_place see expr (* Borrows *) | TRef (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config meta original_sv original_sv_place region - ref_ty rkind cf ctx + expand_symbolic_value_borrow config meta original_sv original_sv_place + region ref_ty rkind cf ctx | _ -> - craise - meta - ("expand_symbolic_value_no_branching: unexpected type: " - ^ show_rty rty) + craise meta + ("expand_symbolic_value_no_branching: unexpected type: " + ^ show_rty rty) in (* Debug *) let cc = @@ -554,17 +567,20 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv (lazy ("expand_symbolic_value_no_branching: " ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); + ^ "\n\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n")); (* Sanity check: the symbolic value has disappeared *) sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta) in (* Continue *) cc cf ctx -let expand_symbolic_adt (config : config) (meta : Meta.meta) (sv : symbolic_value) - (sv_place : SA.mplace option) (cf_branches : st_cm_fun) - (cf_after_join : st_m_fun) : m_fun = +let expand_symbolic_adt (config : config) (meta : Meta.meta) + (sv : symbolic_value) (sv_place : SA.mplace option) + (cf_branches : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv)); @@ -580,19 +596,19 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta) (sv : symbolic_valu let allow_branching = true in (* Compute the expanded value *) let seel = - compute_expanded_symbolic_adt_value meta allow_branching adt_id generics ctx + compute_expanded_symbolic_adt_value meta allow_branching adt_id generics + ctx in (* Apply *) let seel = List.map (fun see -> (Some see, cf_branches)) seel in apply_branching_symbolic_expansions_non_borrow config meta original_sv original_sv_place seel cf_after_join ctx - | _ -> - craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) + | _ -> craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) -let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value) - (sv_place : SA.mplace option) (int_type : integer_type) - (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun) - (cf_after_join : st_m_fun) : m_fun = +let expand_symbolic_int (config : config) (meta : Meta.meta) + (sv : symbolic_value) (sv_place : SA.mplace option) + (int_type : integer_type) (tgts : (scalar_value * st_cm_fun) list) + (otherwise : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = (* Sanity check *) sanity_check (sv.sv_ty = TLiteral (TInteger int_type)) meta; (* For all the branches of the switch, we expand the symbolic value @@ -620,7 +636,8 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_valu an enumeration with strictly more than one variant, a slice, etc.) or if we need to expand a recursive type (because this leads to looping). *) -let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : cm_fun = +let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : + cm_fun = fun cf ctx -> (* The visitor object, to look for symbolic values in the concrete environment *) let obj = @@ -661,31 +678,27 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : (match def.kind with | Struct _ | Enum ([] | [ _ ]) -> () | Enum (_ :: _) -> - craise - meta - ("Attempted to greedily expand a symbolic enumeration \ - with > 1 variants (option \ - [greedy_expand_symbolics_with_borrows] of [config]): " - ^ name_to_string ctx def.name) + craise meta + ("Attempted to greedily expand a symbolic enumeration with > \ + 1 variants (option [greedy_expand_symbolics_with_borrows] \ + of [config]): " + ^ name_to_string ctx def.name) | Opaque -> craise meta "Attempted to greedily expand an opaque type"); (* Also, we need to check if the definition is recursive *) if ctx_type_decl_is_rec ctx def_id then - craise - meta - ("Attempted to greedily expand a recursive definition \ - (option [greedy_expand_symbolics_with_borrows] of \ - [config]): " - ^ name_to_string ctx def.name) + craise meta + ("Attempted to greedily expand a recursive definition (option \ + [greedy_expand_symbolics_with_borrows] of [config]): " + ^ name_to_string ctx def.name) else expand_symbolic_value_no_branching config meta sv None | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) expand_symbolic_value_no_branching config meta sv None | TAdt (TAssumed (TArray | TSlice | TStr), _) -> (* We can't expand those *) - craise - meta - "Attempted to greedily expand an ADT which can't be expanded " + craise meta + "Attempted to greedily expand an ADT which can't be expanded " | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> craise meta "Unreachable" in @@ -695,7 +708,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : (* Apply *) expand cf ctx -let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun = +let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun + = fun cf ctx -> if Config.greedy_expand_symbolics_with_borrows then ( log#ldebug (lazy "greedy_expand_symbolic_values"); |