Module common 

Common SMT checking backend for the staged verifier.

The SMT layer consumes the abstract facts produced by verifying and exposes one property-oriented entry point. Safety properties do not call Z3 directly. Instead, each property-specific module lowers its requirement into one of the common SMT obligations below, and the common backend discharges that obligation against the path-local abstract facts.

Current common obligations:

• SmtObligation::Aligned: prove addr(place) % align == 0.
• SmtObligation::NonZero: prove addr(place) != 0.
• SmtObligation::Range: reserved for future bounds-style checks.

Current property lowering:

• Align(p, T) lowers to Aligned { place: p, align: align_of(T) }.
• NonNull(p) lowers to NonZero { place: p }.
• ValidPtr(p, T, n) is decomposed by valid_ptr.rs into primitive SMT checks that are implemented today, while unsupported primitives remain explicit Unknown notes.

Future SPs should add small lowering modules next to align.rs and reuse SmtModel, SmtQuery, and SmtCheckResult instead of constructing solver queries ad hoc.

Structs

PathCursorCutoff 🔒

PointerBounds 🔒

Recovered index and length terms for a first-cut in-bounds proof.

SmtCheckResult

Result of one SMT check.

SmtChecker

SMT backend for verifier properties.

SmtModel 🔒

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

SmtQuery

Solver query built from path facts plus one negated obligation.

Enums

SliceIndexKind 🔒

SmtObligation

General SMT obligation produced by an SP-specific lowering.

SmtPredicate

Common boolean predicate asserted or refuted by SMT queries.

SmtTerm

Common SMT term used by diagnostics and property-independent query building.

TypeSizeClass 🔒

Trivalent size classification for type-dependent composite SPs.

Functions

abstract_value_from_operand 🔒

abstract_value_from_rvalue 🔒

allocated_type_compatible 🔒

allocation_object_invalidated 🔒

array_elem_type 🔒

binop_label 🔒

Render a compact binary operator label.

call_has_pointer_add_effect 🔒

Return true when a call summary carries pointer-add semantics.

call_has_pointer_sub_effect 🔒

const_int_from_debug 🔒

Extract a small integer constant from rustc’s debug representation.

const_param_name_from_debug 🔒

Extract a const generic parameter name, e.g. Param(N) → "N".

contract_expr_from_place_key 🔒

failed_smt 🔒

infer_element_ty 🔒

init_type_compatible 🔒

initialized_element_ty_name 🔒

is_as_ptr_call 🔒

Return true when a call summary extracts a pointer from a slice-like object.

is_len_carrying_ty 🔒

is_pointer_add_call 🔒

Return true when a call summary is a typed pointer addition.

is_pointer_sub_call 🔒

Return true when a call summary is a typed pointer subtraction.

is_unsigned_integral_ty 🔒

normalize_init_ty_name 🔒

operand_place 🔒

Convert an operand into a place key when it names a MIR place.

place_label 🔒

Compact human-readable label for a MIR place key.

place_name 🔒

Stable SMT variable name for a place key.

pointee_stride_from_types 🔒

pointee_ty 🔒

Return the pointee type of raw pointers and references.

pointee_ty_str 🔒

Return a string label for the pointee type, for type-level alias checks.

pointer_range_negated_goal 🔒

ptr_metadata_origin 🔒

safe_type_layout 🔒

sanitize_smt_name 🔒

Stable SMT identifier for diagnostic-only symbolic terms.

short_func_name 🔒

Return the final path segment of a rustc debug function name.

smt_term_const_u64 🔒

smt_term_for_value 🔒

ty_has_param_const 🔒

value_for_place 🔒

Return the abstract value assigned to a place when it is tracked by local.

value_label 🔒

Compact human-readable label for an abstract value.

Type Aliases

TraceSeen 🔒

ValueCursor 🔒