Enum Proposition 

#[non_exhaustive]
pub enum Proposition {
    FunctionReturns(FunctionId),
    UnboundedStackReader(FunctionId),
    FrameEscapingCaller(FunctionId),
    ArgsDisjointFromCallerFrame(FunctionId),
    LoadedPointerDisjointFromSlot(FunctionId),
    CopyBuffersDisjoint(FunctionId),
    ImmutableMemory {
        addr: u64,
        size: u8,
    },
    ExecutableMemory {
        start: u64,
        end: u64,
    },
    WindowsTeb {
        bitness: u8,
    },
    AssumeCallingConvention,
    ExternalArgmemConfinement(FunctionId, FunctionId),
}

A positive statement about the program whose truth a pass may assume or prove. Used as the key of the truth map on the Context.

#[non_exhaustive] so adding future propositions does not break exhaustive matches in downstream crates.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

FunctionReturns(FunctionId)

Function returns normally to the fall-through after a call to it (false = noreturn: exit/abort, infinite loops, no Return in body).

UnboundedStackReader(FunctionId)

Function performs an unresolved/dynamic stack read, or forwards a stack pointer into one, so callers must keep their frame in memory.

FrameEscapingCaller(FunctionId)

Function hands a pointer into its own frame to an unbounded-reading callee, so its own frame must stay in memory.

ArgsDisjointFromCallerFrame(FunctionId)

Every incoming pointer parameter of this function (and any address offset from one) is disjoint from the function’s own caller-frame region — the @SP + k (k ≥ 0) slots holding the return address and incoming stack arguments. This lets the frame-freshness alias rule forward a load of a caller-frame slot across a store through an incoming pointer (the spilled-pointer reload idiom). Unlike own-frame freshness it is not statically sound on its own — a caller could pass the address of one of its outgoing-argument slots — so a pass records it Assumed and a verifier (verify_args_disjoint_caller_frame) keeps it standing by default, refuting it (→ replay) only when a direct caller provably passes a pointer argument whose access interval overlaps the callee’s argument slots.

LoadedPointerDisjointFromSlot(FunctionId)

Within this function, a pointer loaded from a slot does not alias that slot: a store through load(X) + … cannot clobber X itself — the buffer a pointer addresses does not overlap the storage of the pointer. This lets the alias rule (see AliasResult::provably_disjoint) forward a spilled buffer pointer’s in-loop reload across the very store that writes through it, which argpromote needs to region-promote a dynamic-index buffer loop. Like ArgsDisjointFromCallerFrame it is not statically sound on its own — it fails only for a self-referential pointer (*pp == &pp), which real code does not build — so a pass records it Assumed; v1 has no verifier (nothing currently proves the negation), the checkpoint+replay net catching any future refutation.

CopyBuffersDisjoint(FunctionId)

The source and destination buffers of a recognized copy/transform loop in this function do not overlap — the C strcpy/memcpy contract, where overlapping buffers are undefined behaviour (that is memmove’s job).

A copy-until-terminator (while (*src) *dst++ = *src++;) loop pipelines its loaded byte through a loop-carried register, and re-deriving that byte as load(src - step) — the move that removes the carry and exposes the map(body, take_while(src)) shape — re-reads memory that the body also writes through dst. That re-read is value-preserving only when the two buffers are disjoint. Like ArgsDisjointFromCallerFrame it is not statically sound on its own — a caller may pass overlapping pointers — so a pass records it Assumed; v1 has no verifier (the checkpoint+replay net catches any future refutation).

ImmutableMemory

The size bytes at virtual address addr (a jump-table entry the jump-table resolver read out of read-only data) are assumed never written at runtime; a write would invalidate the resolved jump target.

Fields

addr: u64

size: u8

ExecutableMemory

The mapped region [start, end) is executable code. The lifter assumes this for any readable byte (default r/x) until the optional memory_protections pass establishes the binary’s real protections; a target in a region the pass marks non-executable contradicts it. Keyed by the whole containing segment (not per byte) so the truth map stays small.

Fields

start: u64

end: u64

WindowsTeb

The binary is a Windows target of the given bitness (32 or 64), so the segment-base register (FS on x86, GS on x64) points at the Thread Information Block. Recorded Assumed by the TEB-seeding pass to justify retyping that base as PtrTo<TEB>; it is an analyst aid and override hook, with no verifier in v1 (nothing currently proves the negation).

Fields

bitness: u8

AssumeCallingConvention

Whole-program, opt-in hypothesis: every indirect (CallInd) and unresolved-direct call obeys the module’s calling convention, so instead of clobbering the entire register file it reads only the convention’s argument registers and writes only its caller-saved set (the effect is cached as an AssumedCallEffect on the context). A deliberate, controllable unsoundness — an indirect callee may violate the ABI — off by default, recorded by the assume_calling_convention pass when the user opts in, and surfaced in the assumptions panel.

It is a downstream refinement only: it sharpens how the mem2reg / alias register classifier (classify_call_reg_effect) clobbers around such calls, and does not feed back into the argpromote effect-summary fixpoint (which keeps modelling CallInd as Some(empty)). No verifier in v1 (it is never proven, so it is not discharged and the checkpoint+replay net never acts on it).

ExternalArgmemConfinement(FunctionId, FunctionId)

The external function (second field), reached from the caller (first field), has a prototype-derived argmem footprint that it honours. Two halves, both assumed:

(a) it writes and reads only within the objects addressed by its pointer arguments — e.g. memset(dst, c, n) touches only [dst, dst+n), never spilling past the object we hand it; and

(b) the caller’s subsequent same-base reads of such an object observe the external’s writes — a read of local after memset(&local, …) sees the bytes memset wrote, i.e. the read does not exceed the written extent (it never reads past [dst, dst+n) into stale frame bytes the external left untouched).

argpromote’s RAM effect lattice mints whole-object entries for such externals and rebases them onto the caller’s bases (Frame/Param/ Global); the memset(&local) fold — a write-only external landing on an own-frame local, contained and dead at return — rests on (a), and the summary scan’s read-after-external licensing (a load(local) in a block dominated by the memset call reading as a captured own write rather than refuting frame freshness) rests on (b).

Like LoadedPointerDisjointFromSlot it is not statically sound on its own: the prototype could be lying (an OutPtr that secretly reads, a callback hidden behind a plain pointer) or the length could run out of bounds (memset(dst, c, huge_n)), either of which would touch memory outside the addressed object. A pass records it Assumed at the point a promotion is committed that relied on the containment (the promoted function’s summary flag-set names every external it transitively folded through); v1 has no verifier, the checkpoint+replay net catching any future refutation. A cheap future refuter is available where the caller passes a constant length whose value exceeds the frame-layout distance from the landing slot to the next live slot — a provable overflow.

The first field is the invalidation target (the promoted caller whose IR must be discarded on refutation); the second is the trust anchor (the external whose prototype is being believed).

Trait Implementations

impl Clone for Proposition

fn clone(&self) -> Proposition

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for Proposition

impl Debug for Proposition

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Proposition

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for Proposition

impl Hash for Proposition

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 Proposition

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for Proposition

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Proposition