diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 583 |
1 files changed, 331 insertions, 252 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 3fa550cc..0c30f44c 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -5,6 +5,7 @@ open PureUtils open InterpreterUtils open FunsAnalysis open TypesAnalysis +open Errors module T = Types module V = Values module C = Contexts @@ -143,6 +144,7 @@ type loop_info = { (** Body synthesis context *) type bs_ctx = { (* TODO: there are a lot of duplications with the various decls ctx *) + meta : Meta.meta; (** The meta information about the current declaration *) decls_ctx : C.decls_ctx; type_ctx : type_ctx; fun_ctx : fun_ctx; @@ -324,7 +326,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string = let env = bs_ctx_to_fmt_env ctx in - Print.Values.typed_value_to_string env v + Print.Values.typed_value_to_string ~meta:(Some ctx.meta) env v let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string = let env = bs_ctx_to_pure_fmt_env ctx in @@ -348,7 +350,7 @@ let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = let texpression_to_string (ctx : bs_ctx) (e : texpression) : string = let env = bs_ctx_to_pure_fmt_env ctx in - PrintPure.texpression_to_string env false "" " " e + PrintPure.texpression_to_string ~metadata:(Some ctx.meta) env false "" " " e let fun_id_to_string (ctx : bs_ctx) (id : A.fun_id) : string = let env = bs_ctx_to_fmt_env ctx in @@ -364,7 +366,7 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string = let env = bs_ctx_to_pure_fmt_env ctx in - PrintPure.typed_pattern_to_string env p + PrintPure.typed_pattern_to_string ~meta:(Some ctx.meta) env p let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) : fun_effect_info = @@ -383,7 +385,8 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let verbose = false in let indent = "" in let indent_incr = " " in - Print.Values.abs_to_string env verbose indent indent_incr abs + Print.Values.abs_to_string ~meta:(Some ctx.meta) env verbose indent + indent_incr abs let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = @@ -395,40 +398,44 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : (* Some generic translation functions (we need to translate different "flavours" of types: forward types, backward types, etc.) *) -let rec translate_generic_args (translate_ty : T.ty -> ty) +let rec translate_generic_args (meta : Meta.meta) (translate_ty : T.ty -> ty) (generics : T.generic_args) : generic_args = (* We ignore the regions: if they didn't cause trouble for the symbolic execution, then everything's fine *) let types = List.map translate_ty generics.types in let const_generics = generics.const_generics in let trait_refs = - List.map (translate_trait_ref translate_ty) generics.trait_refs + List.map (translate_trait_ref meta translate_ty) generics.trait_refs in { types; const_generics; trait_refs } -and translate_trait_ref (translate_ty : T.ty -> ty) (tr : T.trait_ref) : - trait_ref = - let trait_id = translate_trait_instance_id translate_ty tr.trait_id in - let generics = translate_generic_args translate_ty tr.generics in +and translate_trait_ref (meta : Meta.meta) (translate_ty : T.ty -> ty) + (tr : T.trait_ref) : trait_ref = + let trait_id = translate_trait_instance_id meta translate_ty tr.trait_id in + let generics = translate_generic_args meta translate_ty tr.generics in let trait_decl_ref = - translate_trait_decl_ref translate_ty tr.trait_decl_ref + translate_trait_decl_ref meta translate_ty tr.trait_decl_ref in { trait_id; generics; trait_decl_ref } -and translate_trait_decl_ref (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref) - : trait_decl_ref = - let decl_generics = translate_generic_args translate_ty tr.decl_generics in +and translate_trait_decl_ref (meta : Meta.meta) (translate_ty : T.ty -> ty) + (tr : T.trait_decl_ref) : trait_decl_ref = + let decl_generics = + translate_generic_args meta translate_ty tr.decl_generics + in { trait_decl_id = tr.trait_decl_id; decl_generics } -and translate_trait_instance_id (translate_ty : T.ty -> ty) +and translate_trait_instance_id (meta : Meta.meta) (translate_ty : T.ty -> ty) (id : T.trait_instance_id) : trait_instance_id = - let translate_trait_instance_id = translate_trait_instance_id translate_ty in + let translate_trait_instance_id = + translate_trait_instance_id meta translate_ty + in match id with | T.Self -> Self | TraitImpl id -> TraitImpl id | BuiltinOrAuto _ -> (* We should have eliminated those in the prepasses *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | Clause id -> Clause id | ParentClause (inst_id, decl_id, clause_id) -> let inst_id = translate_trait_instance_id inst_id in @@ -436,20 +443,21 @@ and translate_trait_instance_id (translate_ty : T.ty -> ty) | ItemClause (inst_id, decl_id, item_name, clause_id) -> let inst_id = translate_trait_instance_id inst_id in ItemClause (inst_id, decl_id, item_name, clause_id) - | TraitRef tr -> TraitRef (translate_trait_ref translate_ty tr) - | FnPointer _ | Closure _ -> raise (Failure "Closures are not supported yet") - | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s)) + | TraitRef tr -> TraitRef (translate_trait_ref meta translate_ty tr) + | FnPointer _ | Closure _ -> + craise __FILE__ __LINE__ meta "Closures are not supported yet" + | UnknownTrait s -> craise __FILE__ __LINE__ meta ("Unknown trait found: " ^ s) (** Translate a signature type - TODO: factor out the different translation functions *) -let rec translate_sty (ty : T.ty) : ty = +let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty = let translate = translate_sty in match ty with | T.TAdt (type_id, generics) -> ( - let generics = translate_sgeneric_args generics in + let generics = translate_sgeneric_args meta generics in match type_id with | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics) | T.TTuple -> - assert (generics.const_generics = []); + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; mk_simpl_tuple_ty generics.types | T.TAssumed aty -> ( match aty with @@ -458,81 +466,87 @@ let rec translate_sty (ty : T.ty) : ty = match generics.types with | [ ty ] -> ty | _ -> - raise - (Failure - "Box/vec/option type with incorrect number of arguments") - ) + craise __FILE__ __LINE__ meta + "Box/vec/option type with incorrect number of arguments") | T.TArray -> TAdt (TAssumed TArray, generics) | T.TSlice -> TAdt (TAssumed TSlice, generics) | T.TStr -> TAdt (TAssumed TStr, generics))) | TVar vid -> TVar vid | TLiteral ty -> TLiteral ty - | TNever -> raise (Failure "Unreachable") - | TRef (_, rty, _) -> translate rty + | TNever -> craise __FILE__ __LINE__ meta "Unreachable" + | TRef (_, rty, _) -> translate meta rty | TRawPtr (ty, rkind) -> let mut = match rkind with RMut -> Mut | RShared -> Const in - let ty = translate ty in + let ty = translate meta ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) | TTraitType (trait_ref, type_name) -> - let trait_ref = translate_strait_ref trait_ref in + let trait_ref = translate_strait_ref meta trait_ref in TTraitType (trait_ref, type_name) - | TArrow _ -> raise (Failure "TODO") + | TArrow _ -> + craise __FILE__ __LINE__ meta "Arrow types are not supported yet" -and translate_sgeneric_args (generics : T.generic_args) : generic_args = - translate_generic_args translate_sty generics +and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) : + generic_args = + translate_generic_args meta (translate_sty meta) generics -and translate_strait_ref (tr : T.trait_ref) : trait_ref = - translate_trait_ref translate_sty tr +and translate_strait_ref (meta : Meta.meta) (tr : T.trait_ref) : trait_ref = + translate_trait_ref meta (translate_sty meta) tr -and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id - = - translate_trait_instance_id translate_sty id +and translate_strait_instance_id (meta : Meta.meta) (id : T.trait_instance_id) : + trait_instance_id = + translate_trait_instance_id meta (translate_sty meta) id -let translate_trait_clause (clause : T.trait_clause) : trait_clause = +let translate_trait_clause (meta : Meta.meta) (clause : T.trait_clause) : + trait_clause = let { T.clause_id; meta = _; trait_id; clause_generics } = clause in - let generics = translate_sgeneric_args clause_generics in + let generics = translate_sgeneric_args meta clause_generics in { clause_id; trait_id; generics } -let translate_strait_type_constraint (ttc : T.trait_type_constraint) : - trait_type_constraint = +let translate_strait_type_constraint (meta : Meta.meta) + (ttc : T.trait_type_constraint) : trait_type_constraint = let { T.trait_ref; type_name; ty } = ttc in - let trait_ref = translate_strait_ref trait_ref in - let ty = translate_sty ty in + let trait_ref = translate_strait_ref meta trait_ref in + let ty = translate_sty meta ty in { trait_ref; type_name; ty } -let translate_predicates (preds : T.predicates) : predicates = +let translate_predicates (meta : Meta.meta) (preds : T.predicates) : predicates + = let trait_type_constraints = - List.map translate_strait_type_constraint preds.trait_type_constraints + List.map + (translate_strait_type_constraint meta) + preds.trait_type_constraints in { trait_type_constraints } -let translate_generic_params (generics : T.generic_params) : generic_params = +let translate_generic_params (meta : Meta.meta) (generics : T.generic_params) : + generic_params = let { T.regions = _; types; const_generics; trait_clauses } = generics in - let trait_clauses = List.map translate_trait_clause trait_clauses in + let trait_clauses = List.map (translate_trait_clause meta) trait_clauses in { types; const_generics; trait_clauses } -let translate_field (f : T.field) : field = +let translate_field (meta : Meta.meta) (f : T.field) : field = let field_name = f.field_name in - let field_ty = translate_sty f.field_ty in + let field_ty = translate_sty meta f.field_ty in { field_name; field_ty } -let translate_fields (fl : T.field list) : field list = - List.map translate_field fl +let translate_fields (meta : Meta.meta) (fl : T.field list) : field list = + List.map (translate_field meta) fl -let translate_variant (v : T.variant) : variant = +let translate_variant (meta : Meta.meta) (v : T.variant) : variant = let variant_name = v.variant_name in - let fields = translate_fields v.fields in + let fields = translate_fields meta v.fields in { variant_name; fields } -let translate_variants (vl : T.variant list) : variant list = - List.map translate_variant vl +let translate_variants (meta : Meta.meta) (vl : T.variant list) : variant list = + List.map (translate_variant meta) vl (** Translate a type def kind from LLBC *) -let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind = +let translate_type_decl_kind (meta : Meta.meta) (kind : T.type_decl_kind) : + type_decl_kind = match kind with - | T.Struct fields -> Struct (translate_fields fields) - | T.Enum variants -> Enum (translate_variants variants) + | T.Struct fields -> Struct (translate_fields meta fields) + | T.Enum variants -> Enum (translate_variants meta variants) | T.Opaque -> Opaque (** Translate a type definition from LLBC @@ -554,11 +568,14 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let name = Print.Types.name_to_string env def.name in let { T.regions; types; const_generics; trait_clauses } = def.generics in (* Can't translate types with regions for now *) - assert (regions = []); - let trait_clauses = List.map translate_trait_clause trait_clauses in + cassert __FILE__ __LINE__ (regions = []) def.meta + "ADTs containing borrows are not supported yet"; + let trait_clauses = + List.map (translate_trait_clause def.meta) trait_clauses + in let generics = { types; const_generics; trait_clauses } in - let kind = translate_type_decl_kind def.T.kind in - let preds = translate_predicates def.preds in + let kind = translate_type_decl_kind def.meta def.T.kind in + let preds = translate_predicates def.meta def.preds in let is_local = def.is_local in let meta = def.meta in { @@ -573,7 +590,7 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : preds; } -let translate_type_id (id : T.type_id) : type_id = +let translate_type_id (meta : Meta.meta) (id : T.type_id) : type_id = match id with | TAdtId adt_id -> TAdtId adt_id | TAssumed aty -> @@ -585,7 +602,7 @@ let translate_type_id (id : T.type_id) : type_id = | T.TBox -> (* Boxes have to be eliminated: this type id shouldn't be translated *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in TAssumed aty | TTuple -> TTuple @@ -598,15 +615,16 @@ let translate_type_id (id : T.type_id) : type_id = TODO: factor out the various translation functions. *) -let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = - let translate = translate_fwd_ty type_infos in +let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) + (ty : T.ty) : ty = + let translate = translate_fwd_ty meta type_infos in match ty with | T.TAdt (type_id, generics) -> ( - let t_generics = translate_fwd_generic_args type_infos generics in + let t_generics = translate_fwd_generic_args meta type_infos generics in (* Eliminate boxes and simplify tuples *) match type_id with | TAdtId _ | TAssumed (TArray | TSlice | TStr) -> - let type_id = translate_type_id type_id in + let type_id = translate_type_id meta type_id in TAdt (type_id, t_generics) | TTuple -> (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the @@ -615,20 +633,20 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = | TAssumed TBox -> ( (* We eliminate boxes *) (* No general parametricity for now *) - assert ( - not - (List.exists - (TypesUtils.ty_has_borrows type_infos) - generics.types)); + cassert __FILE__ __LINE__ + (not + (List.exists + (TypesUtils.ty_has_borrows type_infos) + generics.types)) + meta "ADTs containing borrows are not supported yet"; match t_generics.types with | [ bty ] -> bty | _ -> - raise - (Failure - "Unreachable: box/vec/option receives exactly one type \ - parameter"))) + craise __FILE__ __LINE__ meta + "Unreachable: box/vec/option receives exactly one type \ + parameter")) | TVar vid -> TVar vid - | TNever -> raise (Failure "Unreachable") + | TNever -> craise __FILE__ __LINE__ meta "Unreachable" | TLiteral lty -> TLiteral lty | TRef (_, rty, _) -> translate rty | TRawPtr (ty, rkind) -> @@ -637,32 +655,33 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) | TTraitType (trait_ref, type_name) -> - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in TTraitType (trait_ref, type_name) - | TArrow _ -> raise (Failure "TODO") + | TArrow _ -> + craise __FILE__ __LINE__ meta "Arrow types are not supported yet" -and translate_fwd_generic_args (type_infos : type_infos) +and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos) (generics : T.generic_args) : generic_args = - translate_generic_args (translate_fwd_ty type_infos) generics + translate_generic_args meta (translate_fwd_ty meta type_infos) generics -and translate_fwd_trait_ref (type_infos : type_infos) (tr : T.trait_ref) : - trait_ref = - translate_trait_ref (translate_fwd_ty type_infos) tr +and translate_fwd_trait_ref (meta : Meta.meta) (type_infos : type_infos) + (tr : T.trait_ref) : trait_ref = + translate_trait_ref meta (translate_fwd_ty meta type_infos) tr -and translate_fwd_trait_instance_id (type_infos : type_infos) +and translate_fwd_trait_instance_id (meta : Meta.meta) (type_infos : type_infos) (id : T.trait_instance_id) : trait_instance_id = - translate_trait_instance_id (translate_fwd_ty type_infos) id + translate_trait_instance_id meta (translate_fwd_ty meta type_infos) id (** Simply calls [translate_fwd_ty] *) let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty = let type_infos = ctx.type_ctx.type_infos in - translate_fwd_ty type_infos ty + translate_fwd_ty ctx.meta type_infos ty (** Simply calls [translate_fwd_generic_args] *) let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) : generic_args = let type_infos = ctx.type_ctx.type_infos in - translate_fwd_generic_args type_infos generics + translate_fwd_generic_args ctx.meta type_infos generics (** Translate a type, when some regions may have ended. @@ -670,21 +689,23 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) : [inside_mut]: are we inside a mutable borrow? *) -let rec translate_back_ty (type_infos : type_infos) +let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos) (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option = - let translate = translate_back_ty type_infos keep_region inside_mut in + let translate = translate_back_ty meta type_infos keep_region inside_mut in (* A small helper for "leave" types *) let wrap ty = if inside_mut then Some ty else None in match ty with | T.TAdt (type_id, generics) -> ( match type_id with | TAdtId _ | TAssumed (TArray | TSlice | TStr) -> - let type_id = translate_type_id type_id in + let type_id = translate_type_id meta type_id in if inside_mut then (* We do not want to filter anything, so we translate the generics as "forward" types *) - let generics = translate_fwd_generic_args type_infos generics in + let generics = + translate_fwd_generic_args meta type_infos generics + in Some (TAdt (type_id, generics)) else (* If not inside a mutable reference: check if at least one @@ -695,19 +716,22 @@ let rec translate_back_ty (type_infos : type_infos) *) let types = List.filter_map translate generics.types in if types <> [] then - let generics = translate_fwd_generic_args type_infos generics in + let generics = + translate_fwd_generic_args meta type_infos generics + in Some (TAdt (type_id, generics)) else None | TAssumed TBox -> ( (* Don't accept ADTs (which are not tuples) with borrows for now *) - assert (not (TypesUtils.ty_has_borrows type_infos ty)); + cassert __FILE__ __LINE__ + (not (TypesUtils.ty_has_borrows type_infos ty)) + meta "ADTs containing borrows are not supported yet"; (* Eliminate the box *) match generics.types with | [ bty ] -> translate bty | _ -> - raise - (Failure "Unreachable: boxes receive exactly one type parameter") - ) + craise __FILE__ __LINE__ meta + "Unreachable: boxes receive exactly one type parameter") | TTuple -> ( (* Tuples can contain borrows (which we eliminate) *) let tys_t = List.filter_map translate generics.types in @@ -718,7 +742,7 @@ let rec translate_back_ty (type_infos : type_infos) * is the identity *) Some (mk_simpl_tuple_ty tys_t))) | TVar vid -> wrap (TVar vid) - | TNever -> raise (Failure "Unreachable") + | TNever -> craise __FILE__ __LINE__ meta "Unreachable" | TLiteral lty -> wrap (TLiteral lty) | TRef (r, rty, rkind) -> ( match rkind with @@ -729,7 +753,7 @@ let rec translate_back_ty (type_infos : type_infos) (* Dive in, remembering the fact that we are inside a mutable borrow *) let inside_mut = true in if keep_region r then - translate_back_ty type_infos keep_region inside_mut rty + translate_back_ty meta type_infos keep_region inside_mut rty else None) | TRawPtr _ -> (* TODO: not sure what to do here *) @@ -740,16 +764,17 @@ let rec translate_back_ty (type_infos : type_infos) if inside_mut then (* Translate the trait ref as a "forward" trait ref - we do not want to filter any type *) - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in Some (TTraitType (trait_ref, type_name)) else None - | TArrow _ -> raise (Failure "TODO") + | TArrow _ -> + craise __FILE__ __LINE__ meta "Arrow types are not supported yet" (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) (inside_mut : bool) (ty : T.ty) : ty option = let type_infos = ctx.type_ctx.type_infos in - translate_back_ty type_infos keep_region inside_mut ty + translate_back_ty ctx.meta type_infos keep_region inside_mut ty let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = let const_generics = @@ -768,14 +793,16 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = } let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit = + let meta = ctx.meta in let ctx = mk_type_check_ctx ctx in - let _ = PureTypeCheck.check_typed_pattern ctx v in + let _ = PureTypeCheck.check_typed_pattern meta ctx v in () let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = if !Config.type_check_pure_code then + let meta = ctx.meta in let ctx = mk_type_check_ctx ctx in - PureTypeCheck.check_texpression ctx e + PureTypeCheck.check_texpression meta ctx e let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref = @@ -783,7 +810,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) | FunId fun_id -> FunId fun_id | TraitMethod (trait_ref, method_name, fun_decl_id) -> let type_infos = ctx.type_ctx.type_infos in - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in TraitMethod (trait_ref, method_name, fun_decl_id) let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) @@ -791,7 +818,9 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) (back_funs : texpression option RegionGroupId.Map.t option) (ctx : bs_ctx) : bs_ctx = let calls = ctx.calls in - assert (not (V.FunCallId.Map.mem call_id calls)); + sanity_check __FILE__ __LINE__ + (not (V.FunCallId.Map.mem call_id calls)) + ctx.meta; let info = { forward; forward_inputs = args; back_funs } in let calls = V.FunCallId.Map.add call_id info calls in { ctx with calls } @@ -813,7 +842,9 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id) let calls = V.FunCallId.Map.add call_id info ctx.calls in (* Insert the abstraction in the abstractions map *) let abstractions = ctx.abstractions in - assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions)); + sanity_check __FILE__ __LINE__ + (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) + ctx.meta; let abstractions = V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions in @@ -875,7 +906,8 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) : if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else [] (** Small utility. *) -let compute_raw_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t) +let compute_raw_fun_effect_info (meta : Meta.meta) + (fun_infos : fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with @@ -893,7 +925,7 @@ let compute_raw_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t) is_rec = info.is_rec || Option.is_some lid; } | FunId (FAssumed aid) -> - assert (lid = None); + sanity_check __FILE__ __LINE__ (lid = None) meta; { can_fail = Assumed.assumed_fun_can_fail aid; stateful_group = false; @@ -918,19 +950,20 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) in { info with is_rec = info.is_rec || Option.is_some lid } | FunId (FAssumed _) -> - compute_raw_fun_effect_info ctx.fun_ctx.fun_infos fun_id lid gid) + compute_raw_fun_effect_info ctx.meta ctx.fun_ctx.fun_infos fun_id lid + gid) | Some lid -> ( (* This is necessarily for the current function *) match fun_id with | FunId (FRegular fid) -> ( - assert (fid = ctx.fun_decl.def_id); + sanity_check __FILE__ __LINE__ (fid = ctx.fun_decl.def_id) ctx.meta; (* Lookup the loop *) let lid = V.LoopId.Map.find lid ctx.loop_ids_map in let loop_info = LoopId.Map.find lid ctx.loops in match gid with | None -> loop_info.fwd_effect_info | Some gid -> RegionGroupId.Map.find gid loop_info.back_effect_infos) - | _ -> raise (Failure "Unreachable")) + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") (** Translate a function signature to a decomposed function signature. @@ -943,7 +976,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) We use [bid] ("backward function id") only if we split the forward and the backward functions. *) -let translate_fun_sig_with_regions_hierarchy_to_decomposed +let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) (decls_ctx : C.decls_ctx) (fun_id : A.fun_id_or_trait_method_ref) (regions_hierarchy : T.region_var_groups) (sg : A.fun_sig) (input_names : string option list) : decomposed_fun_sig = @@ -959,18 +992,18 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed List.map (fun (g : T.region_var_group) -> g.id) regions_hierarchy in let ctx = - InterpreterUtils.initialize_eval_ctx decls_ctx region_groups + InterpreterUtils.initialize_eval_ctx meta decls_ctx region_groups sg.generics.types sg.generics.const_generics in (* Compute the normalization map for the *sty* types and add it to the context *) - AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx + AssociatedTypes.ctx_add_norm_trait_types_from_preds meta ctx sg.preds.trait_type_constraints in (* Normalize the signature *) let sg = let ({ A.inputs; output; _ } : A.fun_sig) = sg in - let norm = AssociatedTypes.ctx_normalize_ty ctx in + let norm = AssociatedTypes.ctx_normalize_ty meta ctx in let inputs = List.map norm inputs in let output = norm output in { sg with A.inputs; output } @@ -978,12 +1011,12 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (* Is the forward function stateful, and can it fail? *) let fwd_effect_info = - compute_raw_fun_effect_info fun_infos fun_id None None + compute_raw_fun_effect_info meta fun_infos fun_id None None in (* Compute the forward inputs *) let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in let fwd_inputs_no_fuel_no_state = - List.map (translate_fwd_ty type_infos) sg.inputs + List.map (translate_fwd_ty meta type_infos) sg.inputs in (* State input for the forward function *) let fwd_state_ty = @@ -995,7 +1028,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed List.concat [ fwd_fuel; fwd_inputs_no_fuel_no_state; fwd_state_ty ] in (* Compute the backward output, without the effect information *) - let fwd_output = translate_fwd_ty type_infos sg.output in + let fwd_output = translate_fwd_ty meta type_infos sg.output in (* Compute the type information for the backward function *) (* Small helper to translate types for backward functions *) @@ -1017,18 +1050,20 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let keep_region r = match r with | T.RStatic -> raise Unimplemented - | RErased -> raise (Failure "Unexpected erased region") - | RBVar _ -> raise (Failure "Unexpected bound region") + | RErased -> craise __FILE__ __LINE__ meta "Unexpected erased region" + | RBVar _ -> craise __FILE__ __LINE__ meta "Unexpected bound region" | RFVar rid -> T.RegionId.Set.mem rid gr_regions in let inside_mut = false in - translate_back_ty type_infos keep_region inside_mut ty + translate_back_ty meta type_infos keep_region inside_mut ty in let translate_back_inputs_for_gid (gid : T.RegionGroupId.id) : ty list = (* For now we don't supported nested borrows, so we check that there aren't parent regions *) let parents = list_ancestor_region_groups regions_hierarchy gid in - assert (T.RegionGroupId.Set.is_empty parents); + cassert __FILE__ __LINE__ + (T.RegionGroupId.Set.is_empty parents) + meta "Nested borrows are not supported yet"; (* For now, we don't allow nested borrows, so the additional inputs to the backward function can only come from borrows that were returned like in (for the backward function we introduce for 'a): @@ -1096,7 +1131,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed RegionGroupId.id * back_sg_info = let gid = rg.id in let back_effect_info = - compute_raw_fun_effect_info fun_infos fun_id None (Some gid) + compute_raw_fun_effect_info meta fun_infos fun_id None (Some gid) in let inputs_no_state = translate_back_inputs_for_gid gid in let inputs_no_state = @@ -1185,15 +1220,15 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed else false in let info = { fwd_info; effect_info = fwd_effect_info; ignore_output } in - assert (fun_sig_info_is_wf info); + sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf info) meta; info in (* Generic parameters *) - let generics = translate_generic_params sg.generics in + let generics = translate_generic_params meta sg.generics in (* Return *) - let preds = translate_predicates sg.preds in + let preds = translate_predicates meta sg.preds in { generics; llbc_generics = sg.generics; @@ -1211,7 +1246,8 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) let regions_hierarchy = FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies in - translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx + let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).meta in + translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx (FunId (FRegular fun_id)) regions_hierarchy sg input_names let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx) @@ -1473,18 +1509,18 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with | Some v -> v | None -> - raise - (Failure - ("Could not find var for symbolic value: " - ^ V.SymbolicValueId.to_string sv.sv_id)) + craise __FILE__ __LINE__ ctx.meta + ("Could not find var for symbolic value: " + ^ V.SymbolicValueId.to_string sv.sv_id) (** Peel boxes as long as the value is of the form [Box<T>] *) -let rec unbox_typed_value (v : V.typed_value) : V.typed_value = +let rec unbox_typed_value (meta : Meta.meta) (v : V.typed_value) : V.typed_value + = match (v.value, v.ty) with | V.VAdt av, T.TAdt (T.TAssumed T.TBox, _) -> ( match av.field_values with - | [ bv ] -> unbox_typed_value bv - | _ -> raise (Failure "Unreachable")) + | [ bv ] -> unbox_typed_value meta bv + | _ -> craise __FILE__ __LINE__ meta "Unreachable") | _ -> v (** Translate a symbolic value. @@ -1523,7 +1559,7 @@ let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) : let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (v : V.typed_value) : texpression = (* We need to ignore boxes *) - let v = unbox_typed_value v in + let v = unbox_typed_value ctx.meta v in let translate = typed_value_to_texpression ctx ectx in (* Translate the type *) let ty = ctx_translate_fwd_ty ctx v.ty in @@ -1537,12 +1573,12 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (* Eliminate the tuple wrapper if it is a tuple with exactly one field *) match v.ty with | TAdt (TTuple, _) -> - assert (variant_id = None); - mk_simpl_tuple_texpression field_values + sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta; + mk_simpl_tuple_texpression ctx.meta field_values | _ -> (* Retrieve the type and the translated generics from the translated type (simpler this way) *) - let adt_id, generics = ty_as_adt ty in + let adt_id, generics = ty_as_adt ctx.meta ty in (* Create the constructor *) let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in let qualif = { id = qualif_id; generics } in @@ -1553,23 +1589,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) let cons_ty = mk_arrows field_tys ty in let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) - mk_apps cons field_values) - | VBottom -> raise (Failure "Unreachable") + mk_apps ctx.meta cons field_values) + | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | VLoan lc -> ( match lc with | VSharedLoan (_, v) -> translate v - | VMutLoan _ -> raise (Failure "Unreachable")) + | VMutLoan _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") | VBorrow bc -> ( match bc with | VSharedBorrow bid -> (* Lookup the shared value in the context, and continue *) - let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in + let sv = + InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid + in translate sv | VReservedMutBorrow bid -> (* Same as for shared borrows. However, note that we use reserved borrows * only in *meta-data*: a value *actually used* in the translation can't come * from an unpromoted reserved borrow *) - let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in + let sv = + InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid + in translate sv | VMutBorrow (_, v) -> (* Borrows are the identity in the extraction *) @@ -1615,7 +1655,8 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) -> - assert (field_values = []); + cassert __FILE__ __LINE__ (field_values = []) ctx.meta + "ADTs containing borrows are not supported yet"; None | TTuple -> (* Return *) @@ -1623,9 +1664,9 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) else (* Note that if there is exactly one field value, * [mk_simpl_tuple_rvalue] is the identity *) - let rv = mk_simpl_tuple_texpression field_values in + let rv = mk_simpl_tuple_texpression ctx.meta field_values in Some rv) - | ABottom -> raise (Failure "Unreachable") + | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | ALoan lc -> aloan_content_to_consumed ctx ectx lc | ABorrow bc -> aborrow_content_to_consumed ctx bc | ASymbolic aproj -> aproj_to_consumed ctx aproj @@ -1642,7 +1683,8 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (lc : V.aloan_content) : texpression option = match lc with - | AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable") + | AMutLoan (_, _) | ASharedLoan (_, _, _) -> + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta } -> (* Return the meta-value *) Some (typed_value_to_texpression ctx ectx given_back_meta) @@ -1654,7 +1696,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) None | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -1666,7 +1708,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : texpression option = match bc with | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> - raise (Failure "Unreachable") + craise __FILE__ __LINE__ _ctx.meta "Unreachable" | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) None @@ -1683,7 +1725,9 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = (* The symbolic value was left unchanged *) Some (symbolic_value_to_texpression ctx msv) | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> - assert (child_aproj = AIgnoredProjBorrows); + sanity_check __FILE__ __LINE__ + (child_aproj = AIgnoredProjBorrows) + ctx.meta; (* The symbolic value was updated *) Some (symbolic_value_to_texpression ctx mnv) | V.AEndedProjLoans (_, _) -> @@ -1692,7 +1736,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = raise Unimplemented | AEndedProjBorrows _ -> (* We consider consumed values *) None | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" (** Convert the abstraction values in an abstraction to consumed values. @@ -1758,19 +1802,20 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) -> - assert (field_values = []); + cassert __FILE__ __LINE__ (field_values = []) ctx.meta + "ADTs with borrows are not supported yet"; (ctx, None) | TTuple -> (* Return *) let variant_id = adt_v.variant_id in - assert (variant_id = None); + sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta; if field_values = [] then (ctx, None) else (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern] * is the identity *) let lv = mk_simpl_tuple_pattern field_values in (ctx, Some lv)) - | ABottom -> raise (Failure "Unreachable") + | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | ALoan lc -> aloan_content_to_given_back mp lc ctx | ABorrow bc -> aborrow_content_to_given_back mp bc ctx | ASymbolic aproj -> aproj_to_given_back mp aproj ctx @@ -1785,14 +1830,15 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match lc with - | AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable") + | AMutLoan (_, _) | ASharedLoan (_, _, _) -> + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } | AEndedSharedLoan (_, _) -> (* We consider given back values, and thus ignore those *) (ctx, None) | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -1804,7 +1850,7 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match bc with | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) let ctx, var = fresh_var_for_symbolic_value msv ctx in @@ -1822,17 +1868,18 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : | V.AEndedProjLoans (_, child_projs) -> (* There may be children borrow projections in case of nested borrows, * in which case we need to dive in - we disallow nested borrows for now *) - assert ( - List.for_all - (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) - child_projs); + cassert __FILE__ __LINE__ + (List.for_all + (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) + child_projs) + ctx.meta "Nested borrows are not supported yet"; (ctx, None) | AEndedProjBorrows mv -> (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" (** Convert the abstraction values in an abstraction to given back values. @@ -1956,10 +2003,13 @@ and translate_panic (ctx : bs_ctx) : texpression = (* Create the [Fail] value *) let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in let ret_v = - mk_result_fail_texpression_with_error_id error_failure_id ret_ty + mk_result_fail_texpression_with_error_id ctx.meta error_failure_id + ret_ty in ret_v - else mk_result_fail_texpression_with_error_id error_failure_id output_ty + else + mk_result_fail_texpression_with_error_id ctx.meta error_failure_id + output_ty in if ctx.inside_loop && Option.is_some ctx.bid then (* We are synthesizing the backward function of a loop body *) @@ -2015,12 +2065,12 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) | Some _ -> (* Backward function *) (* Sanity check *) - assert (opt_v = None); + sanity_check __FILE__ __LINE__ (opt_v = None) ctx.meta; (* Group the variables in which we stored the values we need to give back. See the explanations for the [SynthInput] case in [translate_end_abstraction] *) let backward_outputs = Option.get ctx.backward_outputs in let field_values = List.map mk_texpression_from_var backward_outputs in - mk_simpl_tuple_texpression field_values + mk_simpl_tuple_texpression ctx.meta field_values in (* We may need to return a state * - error-monad: Return x @@ -2030,17 +2080,17 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) let output = if effect_info.stateful then let state_rvalue = mk_state_texpression ctx.state_var in - mk_simpl_tuple_texpression [ state_rvalue; output ] + mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ] else output in (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *) - mk_result_return_texpression output + mk_result_return_texpression ctx.meta output and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (ctx : bs_ctx) : texpression = - assert (is_continue = ctx.inside_loop); + sanity_check __FILE__ __LINE__ (is_continue = ctx.inside_loop) ctx.meta; let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in - assert (loop_id = Option.get ctx.loop_id); + sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta; (* Lookup the loop information *) let loop_id = Option.get ctx.loop_id in @@ -2064,7 +2114,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) match ctx.backward_outputs with Some outputs -> outputs | None -> [] in let field_values = List.map mk_texpression_from_var backward_outputs in - mk_simpl_tuple_texpression field_values + mk_simpl_tuple_texpression ctx.meta field_values in (* We may need to return a state @@ -2078,11 +2128,12 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) let output = if effect_info.stateful then let state_rvalue = mk_state_texpression ctx.state_var in - mk_simpl_tuple_texpression [ state_rvalue; output ] + mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ] else output in (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *) - mk_emeta (Tag "return_with_loop") (mk_result_return_texpression output) + mk_emeta (Tag "return_with_loop") + (mk_result_return_texpression ctx.meta output) and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : texpression = @@ -2133,8 +2184,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let sg = Option.get call.sg in let decls_ctx = ctx.decls_ctx in let dsg = - translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx fid - call.regions_hierarchy sg + translate_fun_sig_with_regions_hierarchy_to_decomposed ctx.meta + decls_ctx fid call.regions_hierarchy sg (List.map (fun _ -> None) sg.inputs) in log#ldebug @@ -2147,8 +2198,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : ctx_translate_fwd_generic_args ctx all_generics in let tr_self = - translate_fwd_trait_instance_id ctx.type_ctx.type_infos - tr_self + translate_fwd_trait_instance_id ctx.meta + ctx.type_ctx.type_infos tr_self in (tr_self, all_generics) in @@ -2179,7 +2230,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | PeIdent (s, _) -> s | PeImpl _ -> (* We shouldn't get there *) - raise (Failure "Unexpected")) + craise __FILE__ __LINE__ decl.meta "Unexpected") in name ^ "_back" in @@ -2268,7 +2319,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | S.Unop E.Neg -> ( match args with | [ arg ] -> - let int_ty = ty_as_integer arg.ty in + let int_ty = ty_as_integer ctx.meta arg.ty in (* Note that negation can lead to an overflow and thus fail (it * is thus monadic) *) let effect_info = @@ -2283,7 +2334,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Neg int_ty), effect_info, args, dest) - | _ -> raise (Failure "Unreachable")) + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") | S.Unop (E.Cast cast_kind) -> ( match cast_kind with | CastScalar (src_ty, tgt_ty) -> @@ -2300,16 +2351,17 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest) - | CastFnPtr _ -> raise (Failure "TODO: function casts")) + | CastFnPtr _ -> + craise __FILE__ __LINE__ ctx.meta "TODO: function casts") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> - let int_ty0 = ty_as_integer arg0.ty in - let int_ty1 = ty_as_integer arg1.ty in + let int_ty0 = ty_as_integer ctx.meta arg0.ty in + let int_ty1 = ty_as_integer ctx.meta arg1.ty in (match binop with (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *) | E.Shl | E.Shr -> () - | _ -> assert (int_ty0 = int_ty1)); + | _ -> sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) ctx.meta); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; @@ -2322,7 +2374,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Binop (binop, int_ty0), effect_info, args, dest) - | _ -> raise (Failure "Unreachable")) + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") in let func = { id = FunOrOp fun_id; generics } in let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in @@ -2331,7 +2383,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : in let func_ty = mk_arrows input_tys ret_ty in let func = { e = Qualif func; ty = func_ty } in - let call = mk_apps func args in + let call = mk_apps ctx.meta func args in (* Translate the next expression *) let next_e = translate_expression e ctx in (* Put together *) @@ -2364,8 +2416,9 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) ^ T.RegionGroupId.to_string rg_id ^ "\n- loop_id: " ^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id - ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ectx ^ "\n- abs:\n" - ^ abs_to_string ctx abs ^ "\n")); + ^ "\n- eval_ctx:\n" + ^ eval_ctx_to_string ~meta:(Some ctx.meta) ectx + ^ "\n- abs:\n" ^ abs_to_string ctx abs ^ "\n")); (* When we end an input abstraction, this input abstraction gets back the borrows which it introduced in the context through the input @@ -2378,7 +2431,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) for a parent backward function. *) let bid = Option.get ctx.bid in - assert (rg_id = bid); + sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.meta; (* First, introduce the given back variables. @@ -2425,7 +2478,10 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) (* TODO: normalize the types *) if !Config.type_check_pure_code then List.iter - (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty)) + (fun (var, v) -> + sanity_check __FILE__ __LINE__ + ((var : var).ty = (v : texpression).ty) + ctx.meta) variables_values; (* Translate the next expression *) let next_e = translate_expression e ctx in @@ -2446,7 +2502,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) | S.Fun (fun_id, _) -> fun_id | Unop _ | Binop _ -> (* Those don't have backward functions *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" in let effect_info = get_fun_effect_info ctx fun_id None (Some rg_id) in (* Retrieve the values consumed upon ending the loans inside this @@ -2508,7 +2564,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) ^ "\nfunc type: " ^ pure_ty_to_string ctx func.ty ^ "\n\nargs:\n" ^ String.concat "\n" args)); - let call = mk_apps func args in + let call = mk_apps ctx.meta func args in mk_let effect_info.can_fail output call next_e and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) @@ -2519,8 +2575,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) (* We can do this simply by checking that it consumes and gives back nothing *) let inputs = abs_to_consumed ctx ectx abs in let ctx, outputs = abs_to_given_back None abs ctx in - assert (inputs = []); - assert (outputs = []); + sanity_check __FILE__ __LINE__ (inputs = []) ctx.meta; + sanity_check __FILE__ __LINE__ (outputs = []) ctx.meta; (* Translate the next expression *) translate_expression e ctx @@ -2562,7 +2618,8 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (* Retrieve the values consumed upon ending the loans inside this * abstraction: as there are no nested borrows, there should be none. *) let consumed = abs_to_consumed ctx ectx abs in - assert (consumed = []); + cassert __FILE__ __LINE__ (consumed = []) ctx.meta + "Nested borrows are not supported yet"; (* Retrieve the values given back upon ending this abstraction - note that * we don't provide meta-place information, because those assignments will * be inlined anyway... *) @@ -2580,7 +2637,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) ^ pure_ty_to_string ctx given_back.ty ^ "\n- sig input ty: " ^ pure_ty_to_string ctx input.ty)); - assert (given_back.ty = input.ty)) + sanity_check __FILE__ __LINE__ (given_back.ty = input.ty) ctx.meta) given_back_inputs; (* Translate the next expression *) let next_e = translate_expression e ctx in @@ -2597,7 +2654,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) texpression = let vloop_id = loop_id in let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in - assert (loop_id = Option.get ctx.loop_id); + sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta; let rg_id = Option.get rg_id in (* There are two cases depending on the [abs_kind] (whether this is a synth input or a regular loop call) *) @@ -2667,7 +2724,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) match func with | None -> next_e | Some func -> - let call = mk_apps func args in + let call = mk_apps ctx.meta func args in (* Add meta-information - this is slightly hacky: we look at the values consumed by the abstraction (note that those come from *before* we applied the fixed-point context) and use them to @@ -2724,7 +2781,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value) in let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in let func = { e = Qualif func; ty = func_ty } in - let assertion = mk_apps func args in + let assertion = mk_apps ctx.meta func args in mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) @@ -2739,7 +2796,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) | V.SeLiteral _ -> (* We do not *register* symbolic expansions to literal values in the symbolic ADT *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ ctx.meta "Unreachable" | SeMutRef (_, nsv) | SeSharedRef (_, nsv) -> (* The (mut/shared) borrow type is extracted to identity: we thus simply introduce an reassignment *) @@ -2752,11 +2809,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) next_e | SeAdt _ -> (* Should be in the [ExpandAdt] case *) - raise (Failure "Unreachable")) + craise __FILE__ __LINE__ ctx.meta "Unreachable") | ExpandAdt branches -> ( (* We don't do the same thing if there is a branching or not *) match branches with - | [] -> raise (Failure "Unreachable") + | [] -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | [ (variant_id, svl, branch) ] when not (TypesUtils.ty_is_custom_adt sv.V.sv_ty @@ -2795,7 +2852,9 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) let branch = List.hd branches in let ty = branch.branch.ty in (* Sanity check *) - assert (List.for_all (fun br -> br.branch.ty = ty) branches); + sanity_check __FILE__ __LINE__ + (List.for_all (fun br -> br.branch.ty = ty) branches) + ctx.meta; (* Return *) { e; ty }) | ExpandBool (true_e, false_e) -> @@ -2815,7 +2874,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) ^ pure_ty_to_string ctx true_e.ty ^ "\n\nfalse_e.ty: " ^ pure_ty_to_string ctx false_e.ty)); - if !Config.fail_hard then assert (ty = false_e.ty); + sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.meta; { e; ty } | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : @@ -2840,8 +2899,9 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) Match all_branches ) in let ty = otherwise.branch.ty in - assert ( - List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches); + sanity_check __FILE__ __LINE__ + (List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) + ctx.meta; { e; ty } (* Translate and [ExpandAdt] when there is no branching (i.e., one branch). @@ -2916,14 +2976,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) * field. * We use the [dest] variable in order not to have to recompute * the type of the result of the projection... *) - let adt_id, generics = ty_as_adt scrutinee.ty in + let adt_id, generics = ty_as_adt ctx.meta scrutinee.ty in let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression = let proj_kind = { adt_id; field_id } in let qualif = { id = Proj proj_kind; generics } in let proj_e = Qualif qualif in let proj_ty = mk_arrow scrutinee.ty dest.ty in let proj = { e = proj_e; ty = proj_ty } in - mk_app proj scrutinee + mk_app ctx.meta proj scrutinee in let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in let monadic = false in @@ -2942,7 +3002,9 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) | TAssumed TBox -> (* There should be exactly one variable *) let var = - match vars with [ v ] -> v | _ -> raise (Failure "Unreachable") + match vars with + | [ v ] -> v + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable" in (* We simply introduce an assignment - the box type is the * identity when extracted ([box a = a]) *) @@ -2956,7 +3018,8 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) * through the functions provided by the API (note that we don't * know how to expand values like vectors or arrays, because they have a variable number * of fields!) *) - raise (Failure "Attempt to expand a non-expandable value") + craise __FILE__ __LINE__ ctx.meta + "Attempt to expand a non-expandable value" and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression) @@ -2993,7 +3056,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } | VaTraitConstValue (trait_ref, const_name) -> let type_infos = ctx.type_ctx.type_infos in - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in let qualif_id = TraitConst (trait_ref, const_name) in let qualif = { id = qualif_id; generics = empty_generic_args } in { e = Qualif qualif; ty = var.ty } @@ -3134,7 +3197,7 @@ and translate_forward_end (ectx : C.eval_ctx) else pure_fwd_var :: back_vars in let vars = List.map mk_texpression_from_var vars in - let ret = mk_simpl_tuple_texpression vars in + let ret = mk_simpl_tuple_texpression ctx.meta vars in (* Introduce a fresh input state variable for the forward expression *) let _ctx, state_var, state_pat = @@ -3145,8 +3208,8 @@ and translate_forward_end (ectx : C.eval_ctx) in let state_var = List.map mk_texpression_from_var state_var in - let ret = mk_simpl_tuple_texpression (state_var @ [ ret ]) in - let ret = mk_result_return_texpression ret in + let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in + let ret = mk_result_return_texpression ctx.meta ret in (* Introduce all the let-bindings *) @@ -3319,7 +3382,7 @@ and translate_forward_end (ectx : C.eval_ctx) in let func_ty = mk_arrows input_tys ret_ty in let func = { e = Qualif func; ty = func_ty } in - let call = mk_apps func args in + let call = mk_apps ctx.meta func args in call in @@ -3373,11 +3436,12 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = in (* Sanity check: all the non-fresh symbolic values are in the context *) - assert ( - List.for_all - (fun (sv : V.symbolic_value) -> - V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var) - loop.input_svalues); + sanity_check __FILE__ __LINE__ + (List.for_all + (fun (sv : V.symbolic_value) -> + V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var) + loop.input_svalues) + ctx.meta; (* Translate the loop inputs *) let inputs = @@ -3397,7 +3461,9 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* The types shouldn't contain borrows - we can translate them as forward types *) List.map (fun ty -> - assert (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty)); + cassert __FILE__ __LINE__ + (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty)) + !ctx.meta "The types shouldn't contain borrows"; ctx_translate_fwd_ty !ctx ty) tys) loop.rg_to_given_back_tys @@ -3476,7 +3542,9 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Add the loop information in the context *) let ctx = - assert (not (LoopId.Map.mem loop_id ctx.loops)); + sanity_check __FILE__ __LINE__ + (not (LoopId.Map.mem loop_id ctx.loops)) + ctx.meta; (* Note that we will retrieve the input values later in the [ForwardEnd] (and will introduce the outputs at that moment, together with the actual @@ -3585,14 +3653,14 @@ and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) : | None -> next_e (** Wrap a function body in a match over the fuel to control termination. *) -let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) - : texpression = +let wrap_in_match_fuel (meta : Meta.meta) (fuel0 : VarId.id) (fuel : VarId.id) + (body : texpression) : texpression = let fuel0_var : var = mk_fuel_var fuel0 in let fuel0 = mk_texpression_from_var fuel0_var in let nfuel_var : var = mk_fuel_var fuel in let nfuel_pat = mk_typed_pattern_from_var nfuel_var None in let fail_branch = - mk_result_fail_texpression_with_error_id error_out_of_fuel_id body.ty + mk_result_fail_texpression_with_error_id meta error_out_of_fuel_id body.ty in match !Config.backend with | FStar -> @@ -3614,7 +3682,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) in let func_ty = mk_arrow mk_fuel_ty mk_bool_ty in let func = { e = Qualif func; ty = func_ty } in - mk_app func fuel0 + mk_app meta func fuel0 in (* Create the expression: [decrease fuel0] *) let decrease_fuel = @@ -3626,7 +3694,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) in let func_ty = mk_arrow mk_fuel_ty mk_fuel_ty in let func = { e = Qualif func; ty = func_ty } in - mk_app func fuel0 + mk_app meta func fuel0 in (* Create the success branch *) @@ -3691,7 +3759,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* Add a match over the fuel, if necessary *) let body = if function_decreases_fuel effect_info then - wrap_in_match_fuel ctx.fuel0 ctx.fuel body + wrap_in_match_fuel def.meta ctx.fuel0 ctx.fuel body else body in (* Sanity check *) @@ -3732,10 +3800,11 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (List.map (pure_ty_to_string ctx) signature.inputs))); (* TODO: we need to normalize the types *) if !Config.type_check_pure_code then - assert ( - List.for_all - (fun (var, ty) -> (var : var).ty = ty) - (List.combine inputs signature.inputs)); + sanity_check __FILE__ __LINE__ + (List.for_all + (fun (var, ty) -> (var : var).ty = ty) + (List.combine inputs signature.inputs)) + def.meta; Some { inputs; inputs_lvs; body } in @@ -3797,20 +3866,23 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params llbc_generics in - let preds = translate_predicates preds in - let parent_clauses = List.map translate_trait_clause llbc_parent_clauses in + let generics = translate_generic_params trait_decl.meta llbc_generics in + let preds = translate_predicates trait_decl.meta preds in + let parent_clauses = + List.map (translate_trait_clause trait_decl.meta) llbc_parent_clauses + in let consts = List.map - (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id))) + (fun (name, (ty, id)) -> + (name, (translate_fwd_ty trait_decl.meta type_infos ty, id))) consts in let types = List.map (fun (name, (trait_clauses, ty)) -> ( name, - ( List.map translate_trait_clause trait_clauses, - Option.map (translate_fwd_ty type_infos) ty ) )) + ( List.map (translate_trait_clause trait_decl.meta) trait_clauses, + Option.map (translate_fwd_ty trait_decl.meta type_infos) ty ) )) types in { @@ -3850,27 +3922,34 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) in let type_infos = ctx.type_ctx.type_infos in let impl_trait = - translate_trait_decl_ref (translate_fwd_ty type_infos) llbc_impl_trait + translate_trait_decl_ref trait_impl.meta + (translate_fwd_ty trait_impl.meta type_infos) + llbc_impl_trait in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params llbc_generics in - let preds = translate_predicates preds in - let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in + let generics = translate_generic_params trait_impl.meta llbc_generics in + let preds = translate_predicates trait_impl.meta preds in + let parent_trait_refs = + List.map (translate_strait_ref trait_impl.meta) parent_trait_refs + in let consts = List.map - (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id))) + (fun (name, (ty, id)) -> + (name, (translate_fwd_ty trait_impl.meta type_infos ty, id))) consts in let types = List.map (fun (name, (trait_refs, ty)) -> ( name, - ( List.map (translate_fwd_trait_ref type_infos) trait_refs, - translate_fwd_ty type_infos ty ) )) + ( List.map + (translate_fwd_trait_ref trait_impl.meta type_infos) + trait_refs, + translate_fwd_ty trait_impl.meta type_infos ty ) )) types in { @@ -3911,9 +3990,9 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params llbc_generics in - let preds = translate_predicates preds in - let ty = translate_fwd_ty ctx.type_ctx.type_infos ty in + let generics = translate_generic_params decl.meta llbc_generics in + let preds = translate_predicates decl.meta preds in + let ty = translate_fwd_ty decl.meta ctx.type_ctx.type_infos ty in { meta; def_id; |