Enum Fact

pub enum Fact {
    Range {
        bit_width: u16,
        min: u64,
        max: u64,
    },
    DynamicRange {
        bit_width: u16,
        min: Expr,
        max: Expr,
    },
    Mem {
        ty: MemoryType,
        min_offset: u64,
        max_offset: u64,
        nullable: bool,
    },
    DynamicMem {
        ty: MemoryType,
        min: Expr,
        max: Expr,
        nullable: bool,
    },
    Def {
        value: Value,
    },
    Compare {
        kind: IntCC,
        lhs: Expr,
        rhs: Expr,
    },
    Conflict,
}

A fact on a value.

Variants

Range

A bitslice of a value (up to a bitwidth) is within the given integer range.

The slicing behavior is needed because this fact can describe both an SSA Value, whose entire value is well-defined, and a VReg in VCode, whose bits beyond the type stored in that register are don’t-care (undefined).

Fields

bit_width: u16

The bitwidth of bits we care about, from the LSB upward.

min: u64

The minimum value that the bitslice can take (inclusive). The range is unsigned: the specified bits of the actual value will be greater than or equal to this value, as evaluated by an unsigned integer comparison.

max: u64

The maximum value that the bitslice can take (inclusive). The range is unsigned: the specified bits of the actual value will be less than or equal to this value, as evaluated by an unsigned integer comparison.

DynamicRange

A value bounded by a global value.

The range is in (min_GV + min_offset)..(max_GV + max_offset), inclusive on the lower and upper bound.

Fields

bit_width: u16

The bitwidth of bits we care about, from the LSB upward.

min: Expr

The lower bound, inclusive.

max: Expr

The upper bound, inclusive.

Mem

A pointer to a memory type.

Fields

ty: MemoryType

The memory type.

min_offset: u64

The minimum offset into the memory type, inclusive.

max_offset: u64

The maximum offset into the memory type, inclusive.

nullable: bool

This pointer can also be null.

DynamicMem

A pointer to a memory type, dynamically bounded. The pointer is within (GV_min+offset_min)..(GV_max+offset_max) (inclusive on both ends) in the memory type.

Fields

ty: MemoryType

The memory type.

min: Expr

The lower bound, inclusive.

max: Expr

The upper bound, inclusive.

nullable: bool

This pointer can also be null.

Def

A definition of a value to be used as a symbol in BaseExprs. There can only be one of these per value number.

Note that this differs from a DynamicRange specifying that some value in the program is the same as value. A def(v1) fact is propagated to machine code and serves as a source of truth: the value or location labeled with this fact defines what v1 is, and any dynamic_range(64, v1, v1)-labeled values elsewhere are claiming to be equal to this value.

This is necessary because we don’t propagate SSA value labels down to machine code otherwise; so when referring symbolically to addresses and expressions derived from addresses, we need to introduce the symbol first.

Fields

value: Value

The SSA value this value defines.

Compare

A comparison result between two dynamic values with a comparison of a certain kind.

Fields

kind: IntCC

The kind of comparison.

lhs: Expr

The left-hand side of the comparison.

rhs: Expr

The right-hand side of the comparison.

Conflict

A “conflict fact”: this fact results from merging two other facts, and it can never be satisfied – checking any value against this fact will fail.

Implementations

impl Fact

pub fn constant(bit_width: u16, value: u64) -> Self

Create a range fact that specifies a single known constant value.

pub fn dynamic_base_ptr(ty: MemoryType) -> Self

Create a dynamic range fact that points to the base of a dynamic memory.

pub fn value(bit_width: u16, value: Value) -> Self

Create a fact that specifies the value is exactly an SSA value.

Note that this differs from a def fact: it is not defining a symbol to have the value that this fact is attached to; rather it is claiming that this value is the same as whatever that symbol is. (In other words, the def should be elsewhere, and we are tying ourselves to it.)

pub fn value_offset(bit_width: u16, value: Value, offset: i64) -> Self

Create a fact that specifies the value is exactly an SSA value plus some offset.

pub fn global_value(bit_width: u16, gv: GlobalValue) -> Self

Create a fact that specifies the value is exactly the value of a GV.

pub fn global_value_offset(bit_width: u16, gv: GlobalValue, offset: i64) -> Self

Create a fact that specifies the value is exactly the value of a GV plus some offset.

pub const fn max_range_for_width(bit_width: u16) -> Self

Create a range fact that specifies the maximum range for a value of the given bit-width.

pub const fn max_range_for_width_extended( from_width: u16, to_width: u16, ) -> Self

Create a range fact that specifies the maximum range for a value of the given bit-width, zero-extended into a wider width.

pub fn infer_from_type(ty: Type) -> Option<&'static Self>

Try to infer a minimal fact for a value of the given IR type.

pub fn propagates(&self) -> bool

Does this fact “propagate” automatically, i.e., cause instructions that process it to infer their own output facts? Not all facts propagate automatically; otherwise, verification would be much slower.

pub fn as_const(&self, bits: u16) -> Option<u64>

Is this a constant value of the given bitwidth? Return it as a Some(value) if so.

pub fn as_symbol(&self) -> Option<&Expr>

Is this fact a single-value range with a symbolic Expr?

pub fn intersect(a: &Fact, b: &Fact) -> Fact

Merge two facts. We take the intersection: that is, we know both facts to be true, so we can intersect ranges. (This differs from the usual static analysis approach, where we are merging multiple possibilities into a generalized / widened fact. We want to narrow here.)

Trait Implementations

impl Clone for Fact

fn clone(&self) -> Fact

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Fact

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

Formats the value using the given formatter.

impl Display for Fact

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

Formats the value using the given formatter.

impl Hash for Fact

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 PartialEq for Fact

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Fact

impl StructuralPartialEq for Fact