diff options
Diffstat (limited to 'compiler/InterpreterExpansion.ml')
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 147 |
1 files changed, 74 insertions, 73 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index e489ddc3..0a5a289e 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -13,6 +13,7 @@ open ValuesUtils open InterpreterUtils open InterpreterProjectors open Print.EvalCtx +open Errors module S = SynthesizeSymbolic (** The local logger *) @@ -47,7 +48,7 @@ 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) +let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : config) (allow_reborrows : bool) (proj_kind : proj_kind) (original_sv : symbolic_value) (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx = @@ -65,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) method! visit_abs current_abs abs = - assert (Option.is_none current_abs); + cassert (Option.is_none current_abs) meta "T"; let current_abs = Some abs in super#visit_abs current_abs abs @@ -77,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) method! visit_aproj current_abs aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> - assert (not (same_symbolic_id sv original_sv)) + cassert (not (same_symbolic_id sv original_sv)) meta "T" | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj current_abs aproj @@ -97,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then ( (* There mustn't be any given back values *) - assert (given_back = []); + cassert (given_back = []) meta "T"; (* Apply the projector *) let projected_value = apply_proj_loans_on_symbolic_expansion proj_regions @@ -145,11 +146,11 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (** Auxiliary function. Apply a symbolic expansion to avalues in a context. *) -let apply_symbolic_expansion_to_avalues (config : config) +let apply_symbolic_expansion_to_avalues (meta : Meta.meta) (config : config) (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 allow_reborrows proj_kind + apply_symbolic_expansion_to_target_avalues meta config allow_reborrows proj_kind original_sv expansion ctx in (* First target the loan projectors, then the borrow projectors *) @@ -162,12 +163,12 @@ let apply_symbolic_expansion_to_avalues (config : config) 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 : symbolic_value) +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 () = - if at_most_once then assert (not !replaced); + if at_most_once then cassert (not !replaced) meta "T"; replaced := true; nv in @@ -186,16 +187,16 @@ let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value) (* Return *) ctx -let apply_symbolic_expansion_non_borrow (config : config) +let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config) (original_sv : symbolic_value) (expansion : symbolic_expansion) (ctx : eval_ctx) : 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.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 allow_reborrows original_sv + apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv expansion ctx (** Compute the expansion of a non-assumed (i.e.: not [Box], etc.) @@ -208,13 +209,13 @@ let apply_symbolic_expansion_non_borrow (config : config) [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 (expand_enumerations : bool) +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 - assert (List.length generics.regions = List.length def.generics.regions); + cassert (List.length generics.regions = List.length def.generics.regions) meta "T"; (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def @@ -222,7 +223,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool) in (* Check if there is strictly more than one variant *) if List.length variants_fields_types > 1 && not expand_enumerations then - raise (Failure "Not allowed to expand enumerations with several variants"); + craise meta "Not allowed to expand enumerations with several variants"; (* Initialize the expanded value for a given variant *) let initialize ((variant_id, field_types) : VariantId.id option * rty list) : symbolic_expansion = @@ -260,21 +261,21 @@ let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion = [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) +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 expand_enumerations def_id + compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id generics ctx | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ] | TAssumed TBox, [], [ boxed_ty ] -> [ compute_expanded_symbolic_box_value boxed_ty ] | _ -> - raise - (Failure "compute_expanded_symbolic_adt_value: unexpected combination") + craise + meta "compute_expanded_symbolic_adt_value: unexpected combination" -let expand_symbolic_value_shared_borrow (config : config) +let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (ref_ty : rty) : cm_fun = fun cf ctx -> @@ -307,7 +308,7 @@ let expand_symbolic_value_shared_borrow (config : config) Some [ AsbBorrow bid; shared_asb ] else (* Not in the set: ignore *) Some [ shared_asb ] - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" else None in (* The fresh symbolic value for the shared value *) @@ -324,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config) else super#visit_VSymbolic env sv method! visit_EAbs proj_regions abs = - assert (Option.is_none proj_regions); + cassert (Option.is_none proj_regions) meta "T"; let proj_regions = Some abs.regions in super#visit_EAbs proj_regions abs @@ -349,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config) method! visit_aproj proj_regions aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> - assert (not (same_symbolic_id sv original_sv)) + cassert (not (same_symbolic_id sv original_sv)) meta "T" | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj proj_regions aproj @@ -375,27 +376,27 @@ let expand_symbolic_value_shared_borrow (config : config) let ctx = obj#visit_eval_ctx None ctx in (* Finally, replace the projectors on loans *) let bids = !borrows in - assert (not (BorrowId.Set.is_empty bids)); + cassert (not (BorrowId.Set.is_empty bids)) meta "T"; 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 + apply_symbolic_expansion_to_avalues meta config 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 original_sv original_sv_place see + 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) +let expand_symbolic_value_borrow (meta : Meta.meta) (config : config) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun = fun cf ctx -> - assert (region <> RErased); + cassert (region <> RErased) meta "T"; (* Check that we are allowed to expand the reference *) - assert (not (region_in_set region ctx.ended_regions)); + cassert (not (region_in_set region ctx.ended_regions)) meta "T"; (* Match on the reference kind *) match rkind with | RMut -> @@ -408,20 +409,20 @@ let expand_symbolic_value_borrow (config : config) * 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.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 allow_reborrows original_sv + apply_symbolic_expansion_to_avalues meta config 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 original_sv original_sv_place + S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see expr | RShared -> - expand_symbolic_value_shared_borrow config original_sv original_sv_place + expand_symbolic_value_shared_borrow meta config original_sv original_sv_place ref_ty cf ctx (** A small helper. @@ -440,12 +441,12 @@ let expand_symbolic_value_borrow (config : config) 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) +let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config : config) (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 -> - assert (see_cf_l <> []); + cassert (see_cf_l <> []) meta "T"; (* Apply the symbolic expansion in the context and call the continuation *) let resl = List.map @@ -456,7 +457,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) let ctx = match see_opt with | None -> ctx - | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx + | Some see -> apply_symbolic_expansion_non_borrow meta config sv see ctx in (* Debug *) log#ldebug @@ -475,15 +476,15 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) match resl with | Some _ :: _ -> Some (List.map Option.get resl) | None :: _ -> - List.iter (fun res -> assert (res = None)) resl; + List.iter (fun res -> cassert (res = None) meta "T") resl; None - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in (* Synthesize and return *) let seel = List.map fst see_cf_l in - S.synthesize_symbolic_expansion sv sv_place seel subterms + S.synthesize_symbolic_expansion meta sv sv_place seel subterms -let expand_symbolic_bool (config : config) (sv : symbolic_value) +let expand_symbolic_bool (meta : Meta.meta) (config : config) (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 -> @@ -491,16 +492,16 @@ let expand_symbolic_bool (config : config) (sv : symbolic_value) let original_sv = sv in let original_sv_place = sv_place in let rty = original_sv.sv_ty in - assert (rty = TLiteral TBool); + cassert (rty = TLiteral TBool) meta "T"; (* Expand the symbolic value to true or false and continue execution *) let see_true = SeLiteral (VBool true) in let see_false = SeLiteral (VBool false) in let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) - apply_branching_symbolic_expansions_non_borrow config original_sv + apply_branching_symbolic_expansions_non_borrow meta config original_sv original_sv_place seel cf_after_join ctx -let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value) +let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv : symbolic_value) (sv_place : SA.mplace option) : cm_fun = fun cf ctx -> (* Debug *) @@ -522,29 +523,29 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value) (* Compute the expanded value *) let allow_branching = false in let seel = - compute_expanded_symbolic_adt_value allow_branching adt_id generics + 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 (* Apply in the context *) let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx + apply_symbolic_expansion_non_borrow meta config original_sv see ctx in (* Call the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv + S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see expr (* Borrows *) | TRef (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config original_sv original_sv_place region + expand_symbolic_value_borrow meta config original_sv original_sv_place region ref_ty rkind cf ctx | _ -> - raise - (Failure + craise + meta ("expand_symbolic_value_no_branching: unexpected type: " - ^ show_rty rty)) + ^ show_rty rty) in (* Debug *) let cc = @@ -556,12 +557,12 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value) ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) - assert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx))) + cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "T") in (* Continue *) cc cf ctx -let expand_symbolic_adt (config : config) (sv : symbolic_value) +let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_value) (sv_place : SA.mplace option) (cf_branches : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = fun ctx -> @@ -579,21 +580,21 @@ let expand_symbolic_adt (config : config) (sv : symbolic_value) let allow_branching = true in (* Compute the expanded value *) let seel = - compute_expanded_symbolic_adt_value 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 original_sv + apply_branching_symbolic_expansions_non_borrow meta config original_sv original_sv_place seel cf_after_join ctx | _ -> - raise (Failure ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)) + craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) -let expand_symbolic_int (config : config) (sv : symbolic_value) +let expand_symbolic_int (meta : Meta.meta) (config : config) (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 *) - assert (sv.sv_ty = TLiteral (TInteger int_type)); + cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "T"; (* For all the branches of the switch, we expand the symbolic value * to the value given by the branch and execute the branch statement. * For the otherwise branch, we leave the symbolic value as it is @@ -608,7 +609,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value) in let seel = List.append seel [ (None, otherwise) ] in (* Then expand and evaluate - this generates the proper symbolic AST *) - apply_branching_symbolic_expansions_non_borrow config sv sv_place seel + apply_branching_symbolic_expansions_non_borrow meta config sv sv_place seel cf_after_join (** Expand all the symbolic values which contain borrows. @@ -619,7 +620,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value) 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) : cm_fun = +let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) : cm_fun = fun cf ctx -> (* The visitor object, to look for symbolic values in the concrete environment *) let obj = @@ -660,33 +661,33 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun = (match def.kind with | Struct _ | Enum ([] | [ _ ]) -> () | Enum (_ :: _) -> - raise - (Failure + 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)) + ^ name_to_string ctx def.name) | Opaque -> - raise (Failure "Attempted to greedily expand an opaque type")); + 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 - raise - (Failure + 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 sv None + ^ name_to_string ctx def.name) + else expand_symbolic_value_no_branching meta config sv None | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) - expand_symbolic_value_no_branching config sv None + expand_symbolic_value_no_branching meta config sv None | TAdt (TAssumed (TArray | TSlice | TStr), _) -> (* We can't expand those *) - raise - (Failure - "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 _ -> - raise (Failure "Unreachable") + craise meta "Unreachable" in (* Compose and continue *) comp cc expand cf ctx @@ -694,9 +695,9 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun = (* Apply *) expand cf ctx -let greedy_expand_symbolic_values (config : config) : cm_fun = +let greedy_expand_symbolic_values (meta : Meta.meta) (config : config) : cm_fun = fun cf ctx -> if Config.greedy_expand_symbolics_with_borrows then ( log#ldebug (lazy "greedy_expand_symbolic_values"); - greedy_expand_symbolics_with_borrows config cf ctx) + greedy_expand_symbolics_with_borrows meta config cf ctx) else cf ctx |