Enum ConstantExprKind 

pub enum ConstantExprKind {
    Bool(bool),
    Integer(IntegerValue),
    Char(char),
    Float(FloatValue),
    Adt(Option<VariantId>, Vec<ConstantExpr>),
    Array(Vec<ConstantExpr>),
    Ref(ConstantExpr, Option<UnsizingMetadata>),
    Ptr(RefKind, ConstantExpr, Option<UnsizingMetadata>),
    Str(String),
    ByteStr(Vec<u8>),
    FnDef(FnPtr),
    FnPtr(FnPtr),
    PtrNoProvenance(u128),
    TypeId(Ty),
    RawMemory(Vec<Byte>),
    Var(ConstGenericDbVar),
    Global(GlobalDeclRef),
    Call(FnPtr, Vec<ConstantExpr>),
    TraitConst(TraitRef, AssocConstId),
    VTableRef(TraitRef),
    Discriminant(TypeDeclRef, VariantId),
    SizeOf(Ty),
    AlignOf(Ty),
    OffsetOf(TypeDeclRef, Option<VariantId>, FieldId),
    Opaque(String),
}

Variants

Bool(bool)

Boolean value.

Integer(IntegerValue)

Integer value.

Char(char)

Char value.

Float(FloatValue)

Float value.

Adt(Option<VariantId>, Vec<ConstantExpr>)

Value of an ADT (struct or enum).

This is eliminated inside functions if --raw-consts is off.

Array(Vec<ConstantExpr>)

Array value.

This is eliminated inside functions if --raw-consts is off.

Ref(ConstantExpr, Option<UnsizingMetadata>)

A shared reference to a constant value.

This is eliminated inside functions if --raw-consts is off.

Ptr(RefKind, ConstantExpr, Option<UnsizingMetadata>)

A pointer to a static.

This is eliminated inside functions if --raw-consts is off.

Str(String)

str value.

ByteStr(Vec<u8>)

Byte string value.

FnDef(FnPtr)

ZST constant corresponding to the unique value of the type of a function item.

FnPtr(FnPtr)

A function pointer value; this is a pointer (i.e. an address).

This is eliminated inside functions if --raw-consts is off.

PtrNoProvenance(u128)

A pointer with no provenance (e.g. 0 for the null pointer)

This is eliminated inside functions if --raw-consts is off.

TypeId(Ty)

The TypeId value for a type.

RawMemory(Vec<Byte>)

Raw memory value obtained from constant evaluation. Used when a more structured representation isn’t possible (e.g. for unions) or just isn’t implemented yet.

Var(ConstGenericDbVar)

A const generic var

Global(GlobalDeclRef)

The value of a constant/static.

This is eliminated inside functions if --raw-consts is off.

Call(FnPtr, Vec<ConstantExpr>)

A call to a const fn.

TraitConst(TraitRef, AssocConstId)

A trait associated constant.

E.g.:

impl Foo for Bar {
  const C : usize = 32; // <-
}

VTableRef(TraitRef)

A reference to the vtable static item for this trait ref. This can be normalized if we emitted a vtable item.

This is eliminated if --raw-consts is off.

Discriminant(TypeDeclRef, VariantId)

The integer discriminant value corresponding to this enum variant.

SizeOf(Ty)

The size of the given type.

AlignOf(Ty)

The alignment of the given type.

OffsetOf(TypeDeclRef, Option<VariantId>, FieldId)

The offset of the given field.

Opaque(String)

A constant expression that Charon doesn’t handle, along with the reason why.

Implementations

impl ConstantExprKind

pub fn variant_name(&self) -> &'static str

impl ConstantExprKind

pub fn is_bool(&self) -> bool

pub fn is_integer(&self) -> bool

pub fn is_char(&self) -> bool

pub fn is_float(&self) -> bool

pub fn is_adt(&self) -> bool

pub fn is_array(&self) -> bool

pub fn is_ref(&self) -> bool

pub fn is_ptr(&self) -> bool

pub fn is_str(&self) -> bool

pub fn is_byte_str(&self) -> bool

pub fn is_fn_def(&self) -> bool

pub fn is_fn_ptr(&self) -> bool

pub fn is_ptr_no_provenance(&self) -> bool

pub fn is_type_id(&self) -> bool

pub fn is_raw_memory(&self) -> bool

pub fn is_var(&self) -> bool

pub fn is_global(&self) -> bool

pub fn is_call(&self) -> bool

pub fn is_trait_const(&self) -> bool

pub fn is_vtable_ref(&self) -> bool

pub fn is_discriminant(&self) -> bool

pub fn is_size_of(&self) -> bool

pub fn is_align_of(&self) -> bool

pub fn is_offset_of(&self) -> bool

pub fn is_opaque(&self) -> bool

impl ConstantExprKind

pub fn as_bool(&self) -> Option<&bool>

pub fn as_integer(&self) -> Option<&IntegerValue>

pub fn as_char(&self) -> Option<&char>

pub fn as_float(&self) -> Option<&FloatValue>

pub fn as_adt(&self) -> Option<(&Option<VariantId>, &Vec<ConstantExpr>)>

pub fn as_array(&self) -> Option<&Vec<ConstantExpr>>

pub fn as_ref(&self) -> Option<(&ConstantExpr, &Option<UnsizingMetadata>)>

pub fn as_ptr( &self, ) -> Option<(&RefKind, &ConstantExpr, &Option<UnsizingMetadata>)>

pub fn as_str(&self) -> Option<&String>

pub fn as_byte_str(&self) -> Option<&Vec<u8>>

pub fn as_fn_def(&self) -> Option<&FnPtr>

pub fn as_fn_ptr(&self) -> Option<&FnPtr>

pub fn as_ptr_no_provenance(&self) -> Option<&u128>

pub fn as_type_id(&self) -> Option<&Ty>

pub fn as_raw_memory(&self) -> Option<&Vec<Byte>>

pub fn as_var(&self) -> Option<&ConstGenericDbVar>

pub fn as_global(&self) -> Option<&GlobalDeclRef>

pub fn as_call(&self) -> Option<(&FnPtr, &Vec<ConstantExpr>)>

pub fn as_trait_const(&self) -> Option<(&TraitRef, &AssocConstId)>

pub fn as_vtable_ref(&self) -> Option<&TraitRef>

pub fn as_discriminant(&self) -> Option<(&TypeDeclRef, &VariantId)>

pub fn as_size_of(&self) -> Option<&Ty>

pub fn as_align_of(&self) -> Option<&Ty>

pub fn as_offset_of( &self, ) -> Option<(&TypeDeclRef, &Option<VariantId>, &FieldId)>

pub fn as_opaque(&self) -> Option<&String>

impl ConstantExprKind

pub fn as_bool_mut(&mut self) -> Option<&mut bool>

pub fn as_integer_mut(&mut self) -> Option<&mut IntegerValue>

pub fn as_char_mut(&mut self) -> Option<&mut char>

pub fn as_float_mut(&mut self) -> Option<&mut FloatValue>

pub fn as_adt_mut( &mut self, ) -> Option<(&mut Option<VariantId>, &mut Vec<ConstantExpr>)>

pub fn as_array_mut(&mut self) -> Option<&mut Vec<ConstantExpr>>

pub fn as_ref_mut( &mut self, ) -> Option<(&mut ConstantExpr, &mut Option<UnsizingMetadata>)>

pub fn as_ptr_mut( &mut self, ) -> Option<(&mut RefKind, &mut ConstantExpr, &mut Option<UnsizingMetadata>)>

pub fn as_str_mut(&mut self) -> Option<&mut String>

pub fn as_byte_str_mut(&mut self) -> Option<&mut Vec<u8>>

pub fn as_fn_def_mut(&mut self) -> Option<&mut FnPtr>

pub fn as_fn_ptr_mut(&mut self) -> Option<&mut FnPtr>

pub fn as_ptr_no_provenance_mut(&mut self) -> Option<&mut u128>

pub fn as_type_id_mut(&mut self) -> Option<&mut Ty>

pub fn as_raw_memory_mut(&mut self) -> Option<&mut Vec<Byte>>

pub fn as_var_mut(&mut self) -> Option<&mut ConstGenericDbVar>

pub fn as_global_mut(&mut self) -> Option<&mut GlobalDeclRef>

pub fn as_call_mut(&mut self) -> Option<(&mut FnPtr, &mut Vec<ConstantExpr>)>

pub fn as_trait_const_mut( &mut self, ) -> Option<(&mut TraitRef, &mut AssocConstId)>

pub fn as_vtable_ref_mut(&mut self) -> Option<&mut TraitRef>

pub fn as_discriminant_mut( &mut self, ) -> Option<(&mut TypeDeclRef, &mut VariantId)>

pub fn as_size_of_mut(&mut self) -> Option<&mut Ty>

pub fn as_align_of_mut(&mut self) -> Option<&mut Ty>

pub fn as_offset_of_mut( &mut self, ) -> Option<(&mut TypeDeclRef, &mut Option<VariantId>, &mut FieldId)>

pub fn as_opaque_mut(&mut self) -> Option<&mut String>

impl ConstantExprKind

pub fn from_bits(scalar_ty: &ScalarTy, bits: u128) -> Option<Self>

Trait Implementations

impl AstVisitable for ConstantExprKind

fn drive<V: VisitAst>(&self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_mut<V: VisitAstMut>(&mut self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_two<V: ZipAst>(&self, other: &Self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn name(&self) -> &'static str

The name of the type, used for debug logging.

fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

impl Clone for ConstantExprKind

fn clone(&self) -> ConstantExprKind

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ConstantExprKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de, __State: ?Sized> DeserializeState<'de, __State> for ConstantExprKind

where bool: DeserializeState<'de, __State>, IntegerValue: Deserialize<'de>, char: DeserializeState<'de, __State>, FloatValue: Deserialize<'de>, Option<VariantId>: DeserializeState<'de, __State>, Vec<ConstantExpr>: DeserializeState<'de, __State>, ConstantExpr: DeserializeState<'de, __State>, Option<UnsizingMetadata>: DeserializeState<'de, __State>, RefKind: DeserializeState<'de, __State>, String: DeserializeState<'de, __State>, Vec<u8>: DeserializeState<'de, __State>, FnPtr: DeserializeState<'de, __State>, u128: DeserializeState<'de, __State>, Ty: DeserializeState<'de, __State>, Vec<Byte>: DeserializeState<'de, __State>, ConstGenericDbVar: DeserializeState<'de, __State>, GlobalDeclRef: DeserializeState<'de, __State>, TraitRef: DeserializeState<'de, __State>, AssocConstId: DeserializeState<'de, __State>, TypeDeclRef: DeserializeState<'de, __State>, VariantId: DeserializeState<'de, __State>, FieldId: DeserializeState<'de, __State>,

fn deserialize_state<__D>( __state: &__State, __deserializer: __D, ) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

impl<'s, V> Drive<'s, V> for ConstantExprKind

where V: Visitor + Visit<'s, bool> + Visit<'s, IntegerValue> + Visit<'s, char> + Visit<'s, FloatValue> + Visit<'s, Option<VariantId>> + Visit<'s, Vec<ConstantExpr>> + Visit<'s, ConstantExpr> + Visit<'s, Option<UnsizingMetadata>> + Visit<'s, RefKind> + Visit<'s, String> + Visit<'s, Vec<u8>> + Visit<'s, FnPtr> + Visit<'s, u128> + Visit<'s, Ty> + Visit<'s, Vec<Byte>> + Visit<'s, ConstGenericDbVar> + Visit<'s, GlobalDeclRef> + Visit<'s, TraitRef> + Visit<'s, AssocConstId> + Visit<'s, TypeDeclRef> + Visit<'s, VariantId> + Visit<'s, FieldId>,

fn drive_inner(&'s self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveMut<'s, V> for ConstantExprKind

where V: Visitor + VisitMut<'s, bool> + VisitMut<'s, IntegerValue> + VisitMut<'s, char> + VisitMut<'s, FloatValue> + VisitMut<'s, Option<VariantId>> + VisitMut<'s, Vec<ConstantExpr>> + VisitMut<'s, ConstantExpr> + VisitMut<'s, Option<UnsizingMetadata>> + VisitMut<'s, RefKind> + VisitMut<'s, String> + VisitMut<'s, Vec<u8>> + VisitMut<'s, FnPtr> + VisitMut<'s, u128> + VisitMut<'s, Ty> + VisitMut<'s, Vec<Byte>> + VisitMut<'s, ConstGenericDbVar> + VisitMut<'s, GlobalDeclRef> + VisitMut<'s, TraitRef> + VisitMut<'s, AssocConstId> + VisitMut<'s, TypeDeclRef> + VisitMut<'s, VariantId> + VisitMut<'s, FieldId>,

fn drive_inner_mut(&'s mut self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveTwo<'s, V> for ConstantExprKind

where V: Visitor<Break: Default> + VisitTwo<'s, bool> + VisitTwo<'s, IntegerValue> + VisitTwo<'s, char> + VisitTwo<'s, FloatValue> + VisitTwo<'s, Option<VariantId>> + VisitTwo<'s, Vec<ConstantExpr>> + VisitTwo<'s, ConstantExpr> + VisitTwo<'s, Option<UnsizingMetadata>> + VisitTwo<'s, RefKind> + VisitTwo<'s, String> + VisitTwo<'s, Vec<u8>> + VisitTwo<'s, FnPtr> + VisitTwo<'s, u128> + VisitTwo<'s, Ty> + VisitTwo<'s, Vec<Byte>> + VisitTwo<'s, ConstGenericDbVar> + VisitTwo<'s, GlobalDeclRef> + VisitTwo<'s, TraitRef> + VisitTwo<'s, AssocConstId> + VisitTwo<'s, TypeDeclRef> + VisitTwo<'s, VariantId> + VisitTwo<'s, FieldId>,

fn drive_two_inner( &'s self, other: &'s Self, visitor: &mut V, ) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self and other, if they correspond. If the values don’t match up, this returns Break(Default::default()).

impl Eq for ConstantExprKind

impl From<DeBruijnVar<ConstGenericVarId>> for ConstantExprKind

fn from(x: ConstGenericDbVar) -> Self

Converts to this type from the input type.

impl Hash for ConstantExprKind

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for ConstantExprKind

fn cmp(&self, other: &ConstantExprKind) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for ConstantExprKind

fn eq(&self, other: &ConstantExprKind) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl PartialOrd for ConstantExprKind

fn partial_cmp(&self, other: &ConstantExprKind) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<__State: ?Sized> SerializeState<__State> for ConstantExprKind

where bool: SerializeState<__State>, IntegerValue: Serialize, char: SerializeState<__State>, FloatValue: Serialize, Option<VariantId>: SerializeState<__State>, Vec<ConstantExpr>: SerializeState<__State>, ConstantExpr: SerializeState<__State>, Option<UnsizingMetadata>: SerializeState<__State>, RefKind: SerializeState<__State>, String: SerializeState<__State>, Vec<u8>: SerializeState<__State>, FnPtr: SerializeState<__State>, u128: SerializeState<__State>, Ty: SerializeState<__State>, Vec<Byte>: SerializeState<__State>, ConstGenericDbVar: SerializeState<__State>, GlobalDeclRef: SerializeState<__State>, TraitRef: SerializeState<__State>, AssocConstId: SerializeState<__State>, TypeDeclRef: SerializeState<__State>, VariantId: SerializeState<__State>, FieldId: SerializeState<__State>,

fn serialize_state<__S>( &self, __state: &__State, __serializer: __S, ) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

impl StructuralPartialEq for ConstantExprKind

impl TryFrom<ConstantExprKind> for ConstGenericDbVar

type Error = ()

The type returned in the event of a conversion error.

fn try_from(e: ConstantExprKind) -> Result<Self, Self::Error>

Performs the conversion.