Crate hax_frontend_exporter Copy item path Source pub use crate::id_table ;pub use hax_frontend_exporter_options as options;pub use crate ::*;pub use crate::prelude ::*;pub use crate::state ::*;body 🔒 comments constant_utils 🔒 deterministic_hash 🔒 Stolen from https://github.com/Wassasin/deterministic-hash/blob/main/src/lib.rs id_table index_vec 🔒 mir_kinds Enumerates the kinds of Mir bodies. TODO: use const generics
instead of an open list of types. prelude 🔒 resolution Trait resolution: given a trait reference, we track which local clause caused it to be true.
This module is independent from the rest of hax, in particular it doesn’t use its
state-tracking machinery. rustc rustc_utils 🔒 sinto 🔒 state traits 🔒 types 🔒 utils 🔒 cfg_feature_rustc 🔒 schema_for Generates a RootSchema sinto_as_usize sinto_todo AdtExpr Reflects [thir::AdtExpr] Alias This type merges the information from
rustc_type_ir::AliasKind and ty::AliasTy Align Reflects [ty::Align], but directly stores the number of bytes as a u64. AnonConst Reflects [hir::AnonConst] Arm Reflects [thir::Arm] Ascription Reflects [thir::Ascription] AssocItem Reflects [ty::AssocItem] AttrItem Reflects [rustc_hir::AttrItem] BasicBlockData Binder Reflects [ty::Binder] BindingMode Reflects [rustc_ast::ast::BindingMode] Block Reflects [thir::Block] BoundRegion Reflects [ty::BoundRegion] BoundTy Reflects [ty::BoundTy] CORE_EXTRACTION_MODE Canonical Reflects [rustc_middle::infer::canonical::Canonical] CanonicalUserTypeAnnotation Reflects [ty::CanonicalUserTypeAnnotation] Clause Reflects [ty::Clause] and adds a hash-consed predicate identifier. ClosureArgs Reflects [ty::ClosureArgs] CoercePredicate Reflects [ty::CoercePredicate] ConstArg Reflects [hir::ConstArg] ConstOperand The contents of Operand::Const. ConstantFieldExpr CopyNonOverlapping Decorated Generic container for decorating items with a type, a span,
attributes and other meta-data. DefId Reflects rustc_hir::def_id::DefId DefIdContents DelimArgs Reflects [rustc_ast::ast::DelimArgs] Deprecation Reflects [rustc_hir::attrs::Deprecation] DisambiguatedDefPathItem Reflects [rustc_hir::definitions::DisambiguatedDefPathData] DiscriminantValue Reflects [ty::util::Discr] EarlyParamRegion Reflects [ty::EarlyParamRegion] ExistentialProjection Reflects [rustc_type_ir::ExistentialProjection] ExistentialTraitRef Reflects [rustc_type_ir::ExistentialTraitRef] FieldDef Reflects [ty::FieldDef] FieldExpr A field expression: a field name along with a value FieldPat A field pattern: a field name along with a pattern FnDecl Reflects [hir::FnDecl] FnDef Function definition FnHeader Reflects [hir::FnHeader] FnSig Reflects [hir::FnSig] ForeignItem Reflects [hir::ForeignItem] FruInfo Field Record Update (FRU) informations, this reflects [thir::FruInfo] FullDef Gathers a lot of definition information about a rustc_hir::def_id::DefId GenericParam Reflects [hir::GenericParam] GenericParamDef Reflects [ty::GenericParamDef] GenericPredicates Reflects [ty::GenericPredicates] Generics Reflects [hir::Generics] HashMap A hash map implemented with quadratic probing and SIMD lookup. HirFieldDef Reflects [hir::FieldDef] HirId Reflects [hir::hir_id::HirId] Impl Reflects [hir::Impl]. ImplAssocItem An associated item in a trait impl. This can be an item provided by the trait impl, or an item
that reuses the trait decl default value. ImplExpr An ImplExpr describes the full data of a trait implementation. Because of generics, this may
need to combine several concrete trait implementation items. For example, ((1u8, 2u8), "hello").clone() combines the generic implementation of Clone for (A, B) with the
concrete implementations for u8 and &str, represented as a tree. ImplInfos Meta-informations about an impl<GENERICS[: PREDICATES]> TRAIT for TYPE where PREDICATES {} ImplItem Reflects [hir::ImplItem] IndexVec Item Reflects [hir::Item] (and [hir::ItemId]) ItemAttributes ItemRef Reference to an item, with generics. Basically any mention of an item (function, type, etc)
uses this. ItemRefContents Contents of ItemRef. LateParamRegion Reflects [ty::LateParamRegion] Loc Reflects [rustc_span::Loc] LocalDecl LocalIdent Reflects [thir::LocalVarId] MacroDef Reflects [ast::MacroDef] MacroKinds MetaItemLit Reflects [rustc_ast::MetaItemLit] MirBody OutlivesPredicate Reflects [ty::OutlivesPredicate] as a named struct
instead of a tuple struct. This is because the script converting
JSONSchema types to OCaml doesn’t support tuple structs, and this
is the only tuple struct in the whole AST. Param Reflects [thir::Param] ParamConst Reflects [ty::ParamConst] ParamEnv The combination of type generics and related predicates. ParamTy Reflects [ty::ParamTy] PatRange Reflects [thir::PatRange] PathBuf An owned, mutable path (akin to String PathSegment Reflects [hir::PathSegment] Place Placeholder Reflects [ty::Placeholder] Predicate Reflects [ty::Predicate] and adds a hash-consed predicate identifier. PredicateId A PredicateId is a unique identifier for a clause or a
predicate. It is computed by hashing predicates and clause in a
uniform and deterministic way. PredicateSearcher Stores a set of predicates along with where they came from. ProjectionPredicate Expresses a constraints over an associated type. PromotedId The id of a promoted MIR constant. Rc A single-threaded reference-counting pointer. ‘Rc’ stands for ‘Reference
Counted’. Region Reflects [ty::Region] ReprFlags The representation flags without the ones irrelevant outside of rustc. ReprOptions Reflects [ty::ReprOptions] RustcVersion Reflects [rustc_hir::RustcVersion] ScalarInt Scope Reflects [rustc_middle::middle::region::Scope] SourceInfo SourceScopeData Span Reflects [rustc_span::Span] Spanned Reflects [rustc_span::source_map::Spanned] Statement Stmt Reflects [thir::Stmt] SubtypePredicate Reflects [ty::SubtypePredicate] Terminator TraitItem Reflects [hir::TraitItem] TraitPredicate Reflects [ty::TraitPredicate] Ty Reflects [rustc_middle::ty::Ty] TyFnSig Reflects [ty::FnSig] TyGenerics Reflects [ty::Generics] TypeAndMut Reflects [ty::TypeAndMut] TypeMap A map that maps types to values in a generic manner: we store for each type T a value of
type M::Value<T>. UsePath Reflects [hir::UsePath] UserArgs Reflects [ty::UserArgs] UserSelfTy Reflects [ty::UserSelfTy] Variant Reflects [hir::Variant] VariantDef Reflects [ty::VariantDef] VariantInformations Describe a variant VirtualTraitImpl Partial data for a trait impl, used for fake trait impls that we generate ourselves such as
FnOnce and Drop impls. RDefId A DefId identifies a particular definition , by combining a crate
index and a def index. RLocalDefId A LocalDefId is equivalent to a DefId with krate == LOCAL_CRATE. Since
we encode this information in the type, we can ensure at compile time that
no DefIds from upstream crates get thrown into the mix. There are quite a
few cases where we know that only DefIds from the local crate are expected;
a DefId from a different crate would signify a bug somewhere. This
is when LocalDefId comes in handy. ROwnerId AdtExprBase AdtFlags AdtKind Reflects [ty::AdtKind] AggregateKind AliasKind Reflects [ty::AliasKind] AliasRelationDirection Reflects [ty::AliasRelationDirection] AssertMessage AssignOp Reflects [rustc_middle::mir::AssignOp] AssocItemContainer AssocKind Reflects [ty::AssocKind] AssocTypeData Reflects [ty::AssocTypeData] AttrArgs Reflects [rustc_hir::AttrArgs] AttrStyle Reflects [rustc_ast::AttrStyle] Attribute Reflects [rustc_ast::Attribute] AttributeKind Reflects [rustc_hir::attrs::AttributeKind] BasicBlock BinOp Reflects [rustc_middle::mir::BinOp] BlockSafety Reflects [thir::BlockSafety] BorrowKind Reflects [rustc_middle::mir::BorrowKind] BoundRegionKind Reflects [ty::BoundRegionKind] BoundTyKind Reflects [ty::BoundTyKind] BoundVarIndexKind Reflects [ty::BoundVarIndexKind] BoundVariableKind Reflects [ty::BoundVariableKind] BuiltinTraitData ByRef Reflects [rustc_ast::ast::ByRef] CastKind ClauseKind Reflects [ty::ClauseKind] ClosureKind Reflects [ty::ClosureKind] CoercionSource CommentKind Reflects [rustc_ast::token::CommentKind] ConstArgKind Reflects [hir::ConstArgKind] ConstKind The kind of a constant item. ConstOperandKind ConstantExprKind The subset of Expr that corresponds to constants. ConstantInt ConstantLiteral Constness Reflects [hir::Constness] CoverageKind CtorKind Reflects [hir::def::CtorKind] CtorOf Reflects [hir::def::CtorOf] DefKind Reflects [rustc_hir::def::DefKind] DefPathItem Reflects [rustc_hir::definitions::DefPathData] Defaultness Reflects [hir::Defaultness] DelimSpan Delimiter Reflects [rustc_ast::token::Delimiter] DeprecatedSince Reflects [rustc_hir::attrs::DeprecatedSince] DestructData DiscriminantDefinition Reflects [ty::VariantDiscr] ErrorGuaranteed ExistentialPredicate A predicate without Self, for use in dyn Trait. ExprKind Reflects [thir::ExprKind] ExternAbi Reflects [rustc_abi::ExternAbi] FakeBorrowKind Reflects [rustc_middle::mir::FakeBorrowKind] FakeReadCause FieldIdx FileName Reflects [rustc_span::FileName] FloatTy Reflects [rustc_type_ir::FloatTy] FnRetTy Reflects [hir::FnRetTy] ForeignItemKind Reflects [hir::ForeignItemKind] FullDefKind Imbues [rustc_hir::def::DefKind] with a lot of extra information. FunOperand A value of type fn<...> A -> B that can be called. GenericArg Reflects both [ty::GenericArg] and [ty::GenericArgKind] GenericParamDefKind Reflects [ty::GenericParamDefKind] GenericParamKind Reflects [hir::GenericParamKind] HeaderSafety HirGenericArgs HostEffectPredicate ImplAssocItemValue ImplExprAtom The source of a particular trait implementation. Most often this is either Concrete for a
concrete impl Trait for Type {} item, or LocalBound for a context-bound where T: Trait. ImplExprPathChunk ImplItemKind Reflects [hir::ImplItemKind], inlining the body of the items. ImplPolarity Reflects [hir::ImplPolarity] ImplTraitInTraitData Reflects [ty::ImplTraitInTraitData] ImplicitSelfKind Reflects [hir::ImplicitSelfKind] InferTy Reflects partially [ty::InferTy] InlineAsm InlineAsmOperand InlineAsmOptions InlineAsmTemplatePiece InlineAttr Reflects [rustc_hir::attrs::InlineAttr] IntTy Reflects [rustc_type_ir::IntTy] InvisibleOrigin IsAsync Reflects [hir::IsAsync] IsAuto Reflects [hir::IsAuto] ItemKind Reflects [hir::ItemKind] LateParamRegionKind Reflects [ty::LateParamRegionKind] LifetimeParamKind Reflects [hir::LifetimeParamKind] LintLevel Reflects [thir::LintLevel] LitFloatType Reflects [ast::LitFloatType] LitIntType Reflects both [ty::GenericArg] and [ty::GenericArgKind] LitKind Reflects [rustc_ast::ast::LitKind] Local LogicalOp Reflects [thir::LogicalOp] MissingLifetimeKind Movability Reflects [hir::Movability] MutBorrowKind Reflects [rustc_middle::mir::MutBorrowKind] NonDivergingIntrinsic NonMacroAttrKind Reflects [hir::def::NonMacroAttrKind] NormalizesTo NullOp Operand OwnerId ParamName Reflects [hir::ParamName] PatKind Reflects [thir::PatKind] PatRangeBoundary Reflects [thir::PatRangeBoundary] PlaceKind PointerCoercion Reflects [ty::adjustment::PointerCoercion] PredicateKind Reflects [ty::PredicateKind] PrimTy Reflects [hir::PrimTy] ProjectionElem ProjectionElemFieldKind QPath RangeEnd Reflects [hir::RangeEnd] RawPtrKind RealFileName Reflects [rustc_span::RealFileName] RegionKind Reflects [ty::RegionKind] Res Reflects [hir::def::Res] RetagKind Rvalue Safety Reflects [hir::Safety] ScalarTy ScopeData Reflects [rustc_middle::middle::region::ScopeData] SourceScope StatementKind StmtKind Reflects [thir::StmtKind] StrStyle Reflects [rustc_ast::ast::StrStyle] SyntheticItem We create some extra DefIds to represent things that rustc doesn’t have a DefId for. This
makes the pipeline much easier to have “real” def_ids for them.
We generate fake struct-like items for each of: arrays, slices, and tuples. This makes it
easier to emit trait impls for these types, especially with monomorphization. This enum tracks
identifies these builtin types. Term Reflects [ty::Term] TerminatorKind TraitItemKind Reflects [hir::TraitItemKind] TyKind Reflects [ty::TyKind] UintTy Reflects [rustc_type_ir::UintTy] UnOp Reflects [rustc_middle::mir::UnOp] UnsizingMetadata The metadata to attach to the newly-unsized ptr. UnwindAction UnwindTerminateReason UseKind Reflects [hir::UseKind] UserType Reflects [ty::UserType]: this is currently
disabled, and everything is printed as debug in the
UserType::Todo UserTypeAnnotationIndex UserTypeProjection Variance Reflects [ty::Variance] VariantData Reflects [hir::VariantData] VariantKind Describe the kind of a variant Visibility Reflects [ty::Visibility] WhereEqPredicate WhereRegionPredicate Deserialize A data structure that can be deserialized from any data format supported
by Serde. ExprKindExt HasParamEnv HirIdExt IsBody IsMirKind JsonSchema A type which can be described as a JSON Schema document. SExpect SInto SafeTyCtxtBodies Serialize A data structure that can be serialized into any data format supported
by Serde. SubstBinder ToPolyTraitRef TypeMapper Defines a mapping from types to types. assoc_tys_for_trait Generates a list of <trait_ref>::Ty type aliases for each non-gat associated type of the
given trait and its parents, in a specific order. body_from_id closure_once_shim const_value_to_constant_expr def_id_as_synthetic Returns the SyntheticItemrustc DefId , if any. drop_glue_shim dyn_self_ty Generates a dyn Trait<Args.., Ty = <Self as Trait>::Ty..> type for the given trait ref. erase_and_norm erase_free_regions Erase free regions from the given value. Largely copied from tcx.erase_and_anonymize_regions, but also
erases bound regions that are bound outside value, so we can call this function inside a
Binder. eval_mir_constant Evaluate a mir::Const. eval_ty_constant Evaluate a ty::Const. get_closest_parent_type Gets the closest ancestor of id that is the id of a type. get_def_attrs Gets the attributes of the definition. get_def_visibility Gets the visibility (pub or not) of the definition. Returns None for defs that don’t have a
meaningful visibility. get_foreign_mod_children Gets the children of an extern block. Empty if the block is not defined in the current crate. get_method_sig The signature of a method impl may be a subtype of the one expected from the trait decl, as in
the example below. For correctness, we must be able to map from the method generics declared in
the trait to the actual method generics. Because this would require type inference, we instead
simply return the declared signature. This will cause issues if it is possible to use such a
more-specific implementation with its more-specific type, but we have a few other issues with
lifetime-generic function pointers anyway so this is unlikely to cause problems. get_mod_children Gets the children of a module. get_promoted_mir Retrieve the MIR for a promoted body. get_thir implied_predicates The predicates that can be deduced from the presence of this item in a signature. We only
consider predicates implied by traits here, not implied bounds such as &'a T implying T: 'a. E.g. inst_binder is_sized_related_trait Returns true whenever def_id is MetaSized, Sized or PointeeSized. make_fn_def normalize Normalize a value. override_queries_store_body Register overrides for rustc queries.
This will clone and store bodies for THIR and MIR (built) in an ad-hoc global cache. predicates_defined_on Returns a list of type predicates for the definition with ID def_id, including inferred
lifetime constraints. This is the basic list of predicates we use for essentially all items. required_predicates The predicates that must hold to mention this item. E.g. self_clause_for_item Retrieve the Self: Trait clause for a trait associated item. self_predicate The special “self” predicate on a trait. solve_item_implied_traits Solve the trait obligations for implementing a trait (or for trait associated type bounds) in
the current context. solve_item_required_traits Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.)
in the current context. Just like generic args include generics of parent items, this includes
impl exprs for parent items. solve_sized Solve the T: Sized predicate. solve_trait This is the entrypoint of the solving. substitute super_clause_to_clause_and_impl_expr Given a clause clause in the context of some impl block impl_did, susbts correctly Self
from clause and (1) derive a Clause and (2) resolve an ImplExpr. translate_constant_reference Attempts to translate a ty::UnevaluatedConst into a constant expression. This handles cases
of references to top-level or associated constants. Returns None if the input was not a named
constant. translate_item_ref Translate a reference to an item, resolving the appropriate trait clauses as needed. translate_span BasicBlocks BoundVar ByteSymbol CanonicalUserType Reflects [ty::CanonicalUserType] ConstantExpr Rustc has different representation for constants: one for MIR
([rustc_middle::mir::Const]), one for the type system
([rustc_middle::ty::ConstKind]). For simplicity hax maps those
two construct to one same ConstantExpr type. ConstantKind DebruijnIndex EnumDef Expr FirstStatementIndex GlobalIdent Ident Reflects [rustc_span::symbol::Ident] ItemLocalId Mutability Pat Path Pinnedness PlaceholderConst Reflects [ty::PlaceholderConst] PlaceholderRegion Reflects [ty::PlaceholderRegion] PlaceholderType Reflects [ty::PlaceholderType] PolyFnSig Reflects [ty::PolyFnSig] Predicates RegionOutlivesPredicate Reflects [ty::RegionOutlivesPredicate] RegionVid Symbol ThirBody TokenStream Reflects [rustc_ast::tokenstream::TokenStream] as a plain
string. If you need to reshape that into Rust tokens or construct,
please use, e.g., syn. TraitRef Reflects [ty::TraitRef]
Contains the def_id and arguments passed to the trait. The first type argument is the Self
type. The ImplExprs are the required predicate for this trait; currently they are always
empty because we consider all trait predicates as implied.
self.in_trait is always None because a trait can’t be associated to another one. TypeOutlivesPredicate Reflects [ty::TypeOutlivesPredicate] VariantIdx AdtInto AdtIntoSIntoA to
another ADT B when A and B shares a lot of structure.Deserialize JsonSchema Serialize TypeMappable