Struct SmtModel 

pub(crate) struct SmtModel<'a, 'ctx, 'tcx> {
    tcx: TyCtxt<'tcx>,
    checkpoint: &'a Checkpoint<'tcx>,
    forward: &'a ForwardVisitResult<'tcx>,
    ctx: &'ctx Context,
    place_terms: HashMap<PlaceKey, Int<'ctx>>,
    local_terms: HashMap<usize, Int<'ctx>>,
    symbolic_align_terms: HashMap<String, Int<'ctx>>,
    symbolic_len_terms: HashMap<String, Int<'ctx>>,
    const_terms: HashMap<String, Int<'ctx>>,
    assumptions: Vec<SmtPredicate>,
    has_index_access_assumptions: bool,
}

Per-query SMT term builder over a forward visit result.

Fields

tcx: TyCtxt<'tcx>

checkpoint: &'a Checkpoint<'tcx>

forward: &'a ForwardVisitResult<'tcx>

ctx: &'ctx Context

place_terms: HashMap<PlaceKey, Int<'ctx>>

local_terms: HashMap<usize, Int<'ctx>>

Shared Z3 constants per MIR local — ensures every reference to the same local produces the exact same SMT term (e.g. mid used in both ptr.add and unchecked_sub).

symbolic_align_terms: HashMap<String, Int<'ctx>>

symbolic_len_terms: HashMap<String, Int<'ctx>>

const_terms: HashMap<String, Int<'ctx>>

assumptions: Vec<SmtPredicate>

has_index_access_assumptions: bool

Set to true when IndexAccess InBound assumptions were added from caller contract

Implementations

impl<'a, 'ctx, 'tcx> SmtModel<'a, 'ctx, 'tcx>

pub(crate) fn new( tcx: TyCtxt<'tcx>, checkpoint: &'a Checkpoint<'tcx>, forward: &'a ForwardVisitResult<'tcx>, ctx: &'ctx Context, ) -> Self

Create a fresh SMT model builder.

pub(crate) fn symbolic_align_term(&mut self, ty_name: &str) -> Int<'ctx>

Create or return a cached symbolic alignment constant for a type name.

fn symbolic_len_term(&mut self, len_key: &str) -> Int<'ctx>

fn has_equivalent_contract_fact( &mut self, place: &PlaceKey, _kind: PropertyKind, ) -> bool

Check whether a ContractFact in the forward facts targets the same (or Cast-equivalent) place with the given property kind.

Used by struct-invariant checkpoint checks to short-circuit when a caller #[rapx::requires] already establishes the property.

fn contract_predicate_to_smt( &mut self, predicate: &NumericPredicate<'tcx>, ) -> Option<SmtPredicate>

fn smt_term_from_contract_expr( &mut self, expr: &ContractExpr<'tcx>, ) -> Option<SmtTerm>

fn value_to_int(&mut self, value: &AbstractValue<'tcx>) -> Option<Int<'ctx>>

pub(crate) fn assert_forward_facts(&mut self, solver: &Solver<'ctx>)

Assert facts collected by the forward visitor.

pub(crate) fn assumptions(&self) -> &[SmtPredicate]

Return the path assumptions asserted by this model.

fn latest_cursor(&self) -> usize

fn call_definition_cursor(&self, call: &CallSummary<'tcx>) -> usize

pub(crate) fn pointer_bounds_for_place( &mut self, place: &PlaceKey, ) -> Option<PointerBounds<'ctx>>

Try to recover the slice index/length terms behind a pointer result.

Supported forms:

• slice.as_ptr().add(index) and wrappers summarized as ReturnPointerAdd
• plain slice.as_ptr() / slice.as_mut_ptr(), treated as index 0

fn field_projection_index( &mut self, place: &PlaceKey, origin_key: &str, len_term: &SmtTerm, ) -> (SmtTerm, Int<'ctx>)

Walk the value chain for place to determine if it is a field projection from an as_ptr_range/as_mut_ptr_range result (or an inlined equivalent). Returns (index_term, index_val). Field [0] (start) → offset 0; field [1] (end) → offset len.

fn compute_pointer_arith_index( &mut self, base: &AbstractValue<'tcx>, base_origin: &str, len_term: &SmtTerm, call: &CallSummary<'tcx>, call_cursor: usize, ) -> (SmtTerm, Int<'ctx>)

Compute the offset index for a pointer-arithmetic call result. result_offset = base_offset (+ or -) count

fn pointer_object_offset_for_place( &self, place: &PlaceKey, ) -> Option<(PlaceKey, SmtTerm)>

Recover the allocation object and element offset for a pointer-like place. This is intentionally small: it handles base pointers returned by as_ptr/as_mut_ptr and offsets produced by pointer arithmetic summaries.

fn pointer_object_offset_for_place_before( &self, place: &PlaceKey, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<(PlaceKey, SmtTerm)>

fn pointer_object_offset_for_value( &self, value: &AbstractValue<'tcx>, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<(PlaceKey, SmtTerm)>

fn allocated_object_for_place(&self, place: &PlaceKey) -> Option<PlaceKey>

pub(crate) fn assert_place_non_zero( &mut self, solver: &Solver<'ctx>, place: &PlaceKey, reason: &str, )

Assert that a place is known to denote a non-zero address.

fn assert_place_alignment(&mut self, solver: &Solver<'ctx>, place: &PlaceKey)

Assert known alignment for a place when its MIR type provides one.

fn assert_known_alignment( &mut self, solver: &Solver<'ctx>, place: &PlaceKey, align: u64, ty_name: &str, reason: &str, )

Assert an explicitly summarized alignment fact.

fn assert_known_const( &mut self, solver: &Solver<'ctx>, place: &PlaceKey, value: u64, reason: &str, )

Assert that a place is equal to a concrete layout/numeric constant.

fn assert_length_alias( &mut self, solver: &Solver<'ctx>, left: &PlaceKey, right: &PlaceKey, )

Assert equal slice lengths for two slice-like places that alias.

fn is_len_carrying_place(&self, place: &PlaceKey) -> bool

fn record_call_effect_assumptions(&mut self, call: &CallSummary<'tcx>)

Record call-effect definitions that the term builder understands.

pub(crate) fn term_for_place(&mut self, place: &PlaceKey) -> Option<Int<'ctx>>

Build an SMT term for a place.

fn term_for_place_before( &mut self, place: &PlaceKey, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<Int<'ctx>>

Build an SMT term for a place using only definitions before cursor.

fn projected_term_for_place( &mut self, place: &PlaceKey, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<Int<'ctx>>

Build terms for well-known aggregate projections.

Checked integer arithmetic is represented as (value, overflow) in MIR. For numeric reasoning we can use field 0 as the mathematical result. Field 1 remains a fresh value, so overflow assertions do not become accidental constraints on the result itself.

fn term_for_value( &mut self, value: &AbstractValue<'tcx>, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<Int<'ctx>>

Build an SMT term for an abstract value.

fn term_for_pointer_arith_call( &mut self, call: &CallSummary<'tcx>, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<Int<'ctx>>

Build an address expression for a call summarized as pointer arithmetic.

fn term_for_length_call( &mut self, call: &CallSummary<'tcx>, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<Int<'ctx>>

Build a stable len(origin) term for calls summarized as length reads.

fn const_param_symbol(&mut self, name_or_debug: &str) -> Int<'ctx>

Return a cached Z3 integer symbol for a const generic parameter, keyed by its plain name (e.g. N). Accepts either a plain name or a rustc debug string such as Ty(usize, N/#1) / Param(N), so that a const parameter referenced from a MIR operand, a contract, and an array length all resolve to the same const_<name> symbol.

fn term_for_value_at( &mut self, value: &AbstractValue<'tcx>, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<Int<'ctx>>

Build an SMT term for an abstract value at a program point.

fn term_for_smt_term(&mut self, term: &SmtTerm) -> Option<Int<'ctx>>

Build an SMT integer term from a property-independent diagnostic term.

fn bool_for_predicates( &mut self, predicates: &[SmtPredicate], ) -> Option<Bool<'ctx>>

Build a boolean term for a conjunction of shared predicates.

fn bool_for_predicate(&mut self, predicate: &SmtPredicate) -> Option<Bool<'ctx>>

Build a boolean term from a shared diagnostic/query predicate.

fn assert_unsigned_bounds_for_predicates( &mut self, solver: &Solver<'ctx>, predicates: &[SmtPredicate], )

Assert Rust unsigned integer lower bounds for terms that appear in a numeric obligation.

fn assert_unsigned_bounds_for_predicate( &mut self, solver: &Solver<'ctx>, predicate: &SmtPredicate, seen: &mut HashSet<PlaceKey>, )

fn assert_unsigned_bounds_for_term( &mut self, solver: &Solver<'ctx>, term: &SmtTerm, seen: &mut HashSet<PlaceKey>, )

fn term_for_binary( &self, op: BinOp, lhs: &Int<'ctx>, rhs: &Int<'ctx>, ) -> Option<Int<'ctx>>

Lower a binary MIR operation to an integer term.

fn call_destination_stride(&self, call: &CallSummary<'tcx>) -> Option<u64>

Return the byte stride for a typed pointer-add call destination.

fn place_ty(&self, place: &PlaceKey) -> Option<Ty<'tcx>>

Return the MIR type for a simple place key.

fn type_layout(&self, ty: Ty<'tcx>) -> Option<(u64, u64)>

fn guaranteed_alignment(&self, ty: Ty<'tcx>) -> Option<u64>

Return the alignment guaranteed by a concrete or generic type.

fn generic_candidate_alignments(&self, ty: Ty<'tcx>) -> Option<Vec<u64>>

fn pointer_add_call_for_place( &self, place: &PlaceKey, ) -> Option<CallSummary<'tcx>>

Return the pointer-add call/effect that produced a place after copies/casts.

fn resolved_value_for_place( &self, place: &PlaceKey, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<AbstractValue<'tcx>>

Resolve copy/cast chains for a MIR place into the value at their source.

fn resolved_value_for_place_before( &self, place: &PlaceKey, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<AbstractValue<'tcx>>

fn resolved_value( &self, value: &AbstractValue<'tcx>, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<AbstractValue<'tcx>>

Resolve copy/cast chains for an abstract value.

fn resolved_value_before( &self, value: &AbstractValue<'tcx>, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<AbstractValue<'tcx>>

fn path_value_definition_before( &self, place: &PlaceKey, cursor: usize, ) -> Option<AbstractValue<'tcx>>

Recover a local definition directly from the expanded MIR path.

Backward relevance keeps the proof slice intentionally small. When a pure call-argument temporary is not retained in the forward visit, SMT term construction can still recover its value by replaying assignments along the already-enumerated path up to the current cursor.

fn path_cursor_cutoff(&self, cursor: usize) -> PathCursorCutoff

fn origin_key_for_value( &self, value: &AbstractValue<'tcx>, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<String>

Return a stable origin key for matching as_ptr(source) and len(source).

fn origin_key_for_value_before( &self, value: &AbstractValue<'tcx>, cursor: usize, seen: &mut HashSet<(PlaceKey, usize)>, ) -> Option<String>

fn guarded_len_for_index( &self, base_origin: &str, index: &AbstractValue<'tcx>, ) -> Option<AbstractValue<'tcx>>

Recover a length value from a path guard that mentions index.

fn value_mentions( &self, haystack: &AbstractValue<'tcx>, needle: &AbstractValue<'tcx>, ) -> bool

Return true when haystack contains the same resolved value as needle.

fn value_mentions_inner( &self, haystack: &AbstractValue<'tcx>, needle: &AbstractValue<'tcx>, seen: &mut HashSet<(String, String)>, ) -> bool

fn len_matches_origin( &self, len: &AbstractValue<'tcx>, base_origin: &str, ) -> bool

Return true when a length-like value is the metadata/len of base_origin.

fn len_matches_origin_inner( &self, len: &AbstractValue<'tcx>, base_origin: &str, seen: &mut HashSet<String>, ) -> bool

fn source_from_points_to(&self, pointer: &PlaceKey) -> Option<PlaceKey>

Return the source place recorded by a PointsTo(pointer, source) fact.

fn init_target_terms(&mut self, place: &PlaceKey) -> Vec<Int<'ctx>>

Candidate address/value terms for an Init target.

Pointer targets use their value term. By-value MaybeUninit<T> targets may be moved into a temporary before assume_init; in that case the relevant initialized storage is the address of the original place.

fn init_source_terms(&mut self, place: &PlaceKey) -> Vec<Int<'ctx>>

Candidate address/value terms for a known initialized write.

fn storage_addr_for_place( &mut self, place: &PlaceKey, seen: &mut HashSet<PlaceKey>, ) -> Option<Int<'ctx>>

Return the address of the storage represented by place.

fn bounds_len_for_origin( &mut self, origin_key: &str, index: Option<&AbstractValue<'tcx>>, ) -> Option<(Int<'ctx>, SmtTerm)>

Find a retained len(source) call whose source matches origin_key.

fn is_slice_pointer_origin(&self, origin_key: &str) -> bool

Return true if origin_key is the source of an as_ptr-like call (suggesting it is a slice / reference whose internal pointer was extracted). For these origins a symbolic length term is safe because the length is naturally bounded by the reference type.

fn is_maybe_uninit_origin(&self, origin_key: &str) -> bool

Return true if the allocation for origin_key is a MaybeUninit wrapper (dynamic-length array). These have elements == 0 in KnownAllocated and should use a symbolic/sentinel length.

fn len_place_for_origin(&self, origin_key: &str) -> Option<PlaceKey>

fn allocated_len_for_origin(&self, origin_key: &str) -> Option<u64>

fn origin_is_initialized_for_ty( &self, origin_key: &str, required_ty_name: &str, ) -> bool

fn initialized_element_ty_for_place(&self, place: &PlaceKey) -> Option<String>