Struct PropertyChecker 

pub(crate) struct PropertyChecker;

Implementations

impl PropertyChecker

pub(super) fn check_alias<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> CheckResult

pub(super) fn check_owning<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

impl PropertyChecker

pub(super) fn check_contain_no_type<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

ContainNoType(T, bad1, bad2, ...): T must not structurally contain any of the named negative types.

pub(super) fn check_no_raw_ptr<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

NoRawPtr(T): T must have no raw pointers.

pub(super) fn check_no_internal_mut<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, property: &Property<'tcx>, ) -> CheckResult

NoInternalMut(T): T must have no interior mutation through raw pointers.

pub(super) fn check_uni_internal_mut<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, property: &Property<'tcx>, ) -> CheckResult

UniInternalMut(T): T’s interior mutation must be unique (exclusive owner, no aliasing Clone).

pub(super) fn check_atomic_update<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

AtomicUpdate(T): T’s raw-pointer updates are guarded by a synchronization primitive (Mutex/RwLock) or performed atomically (Atomic*).

pub(super) fn check_ref_send<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

RefSend(T): every interior-mutability (UnsafeCell) / raw-pointer field of T must be guarded by a synchronization primitive.

impl PropertyChecker

pub(super) fn check_in_bound<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn count_is_offset_of<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, value: &VmValue<'z3, 'tcx>, ) -> bool

pub(super) fn resolve_index_access_args( property: &Property<'_>, ) -> (Option<usize>, Option<usize>)

pub(super) fn extract_place_arg_index(expr: &ContractExpr<'_>) -> Option<usize>

pub(super) fn check_in_bound_slice<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn extract_range_end<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, op: &Operand<'tcx>, ) -> Option<VmValue<'z3, 'tcx>>

pub(super) fn check_non_overlap<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn all_predicates_are_slice_size_invariant<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, predicates: &[NumericPredicate<'tcx>], ) -> bool

pub(super) fn predicate_is_slice_size_invariant<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, pred: &NumericPredicate<'tcx>, ) -> bool

pub(super) fn count_derives_from_slice_param<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, count_expr: &ContractExpr<'tcx>, elem_ty: Ty<'tcx>, ) -> bool

pub(super) fn is_slice_ref_with_elem<'z3, 'tcx>( &self, ty: Ty<'tcx>, elem_ty: Ty<'tcx>, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> bool

pub(super) fn same_erased_ty<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, a: Ty<'tcx>, b: Ty<'tcx>, ) -> bool

pub(super) fn is_caller_type_param<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, ty: Ty<'tcx>, ) -> bool

impl PropertyChecker

pub(super) fn check_valid_cstr<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn check_valid_cstr_from_known_nul<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, alloc_id: AllocId, start_offset: usize, ) -> Option<CheckResult>

Fast-path: check NUL termination using per-byte NUL/non-NUL knowledge. This handles constant byte strings like b"hello\0" and aggregate initializers where all element operands are constants. start_offset is the byte offset within the allocation where the C string begins (non-zero when pointer arithmetic like .add(n) is used).

fn check_valid_cstr_from_byte_values<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, alloc_id: AllocId, alloc_size: &Int<'z3>, ) -> Option<CheckResult>

Check NUL termination using per-byte symbolic values tracked in bytes. Uses the SMT solver to verify that a NUL-terminated byte sequence is possible.

fn check_valid_cstr_nul_store<'tcx>( vm_state: &VmState<'_, 'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> Option<CheckResult>

Scan MIR blocks for a single 0_u8 store into the target buffer. When exactly one nul-store exists among all constant stores, we can prove ValidCStr even without VM-level byte tracking. This mirrors the legacy nul_store_before_checkpoint logic.

fn check_valid_cstr_from_mir_constants<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> Option<CheckResult>

Fallback: scan the MIR body for constant byte assignments to the target pointer’s root local. Uses worklist-based analysis (handles as_ptr chains and branches), falling back to simple local chain for Aggregate cases.

impl PropertyChecker

pub(super) fn check_align<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn value_aligned_to<'z3, 'tcx>( vm_state: &VmState<'z3, 'tcx>, value: &VmValue<'z3, 'tcx>, align: u64, ) -> bool

pub(super) fn check_non_null<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn check_null<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn is_value_aligned<'z3, 'tcx>( vm_state: &VmState<'z3, 'tcx>, value: &VmValue<'z3, 'tcx>, ) -> bool

Whether value is known to be aligned: either align_n carries a concrete alignment, or the value sits at the base of an allocation whose align is not 1.

fn is_maybe_uninit_ptr<'z3, 'tcx>( vm_state: &VmState<'z3, 'tcx>, value: &VmValue<'z3, 'tcx>, alloc_id: AllocId, ) -> bool

Whether value is a MaybeUninit-typed pointer access into alloc_id.

assume_init_drop / as_mut_ptr (and friends) legitimately consume an initialized element from storage that may be going out of scope, so the Init/Allocated requirement concerns the write, not the allocation’s live/dead flag.

pub(super) fn check_allocated<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn allocation_covers_access<'z3, 'tcx>( vm_state: &VmState<'z3, 'tcx>, value: &VmValue<'z3, 'tcx>, access: &Int<'z3>, base: &Int<'z3>, size: &Int<'z3>, on_sat: CheckResult, elem_size: Option<&Int<'z3>>, ) -> CheckResult

Prove that value + access fits within [base, base + size).

on_sat is the result when the overflow is satisfiable: Failed for concrete sizes, Unknown for generic-element allocations whose byte layout cannot be resolved. elem_size, when present, is the generic element-size term: the check is then discharged by a case split on S = 0 (ZST) vs S ≥ 1 (non-ZST) rather than a single nonlinear query.

pub(super) fn check_init<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn trace_alloc_ids<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, local: Local, ) -> Vec<AllocId>

pub(super) fn check_alive<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

impl PropertyChecker

pub(super) fn check_valid_num<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn range_end_of_lhs<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: Option<&Checkpoint<'tcx>>, expr: &ContractExpr<'tcx>, ) -> Option<Int<'z3>>

If expr is a SliceIndex range parameter (e.g. ..n), return its exclusive end term, so ValidNum(index < CAPACITY) compares n (not the opaque range value).

pub(super) fn eval_numeric_predicate<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: Option<&Checkpoint<'tcx>>, pred: &NumericPredicate<'tcx>, ) -> Option<CheckResult>

pub(super) fn inject_nia_axioms<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: Option<&Checkpoint<'tcx>>, expr: &ContractExpr<'tcx>, )

pub(super) fn inject_vm_div_axioms<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, expr: &ContractExpr<'tcx>, )

pub(super) fn inject_div_axioms_for_term<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, target: &Int<'z3>, depth: usize, )

pub(super) fn try_get_iter_len_term<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, expr: &ContractExpr<'tcx>, ) -> Option<Int<'z3>>

pub(super) fn try_iter_len_from_fields<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, expr: &ContractExpr<'tcx>, ) -> Option<Int<'z3>>

impl PropertyChecker

fn check_utf8_alloc<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, alloc_id: AllocId, ) -> CheckResult

Shared UTF-8 byte check: prove the tracked buffer bytes of alloc_id are not valid UTF-8 (i.e. disprove the DFA), reporting Failed when the solver proves they cannot be valid.

pub(super) fn check_valid_string<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

impl PropertyChecker

pub(super) fn check_valid_transmute<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn check_trait<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn check_split_transmute<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn is_simd_vector<'z3, 'tcx>( _vm_state: &VmState<'z3, 'tcx>, ty: Ty<'tcx>, ) -> bool

Return true if ty is a SIMD vector (a #[repr(simd)] ADT such as core::simd::Simd<T, N>).

fn ty_size<'z3, 'tcx>(vm_state: &VmState<'z3, 'tcx>, ty: Ty<'tcx>) -> u64

Compute type size, trying different typing environments.

pub(super) fn all_bit_patterns_valid(ty: Ty<'_>) -> bool

Returns true for integer and float types that accept all possible bit patterns as valid values. Types like bool, char, and enums have restricted validity. Tuples and arrays are all-bit-patterns-valid iff every component is, so a widening SplitTransmute such as [u8] -> [(usize, usize)] (used by memrchr) is recognised.

impl PropertyChecker

pub(super) fn check_typed<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn ty_is_maybe_uninit(ty: Ty<'_>) -> bool

pub(super) fn check_size<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

pub(super) fn check_no_padding<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn type_has_no_padding<'tcx>( &self, vm_state: &VmState<'_, 'tcx>, ty: Ty<'tcx>, ) -> Option<bool>

Conservative “no padding” test: Some(true) when the type definitely has no padding bytes, Some(false) when it definitely does, None when it cannot be determined (generic / enum / union / opaque).

impl PropertyChecker

pub(super) fn ty_arg<'tcx>( property: &Property<'tcx>, idx: usize, ) -> Option<Ty<'tcx>>

pub(super) fn target_value<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<VmValue<'z3, 'tcx>>

fn target_value_raw<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<VmValue<'z3, 'tcx>>

Resolve the target place to a VmValue, without pointer provenance penetration (see Self::resolve_pointer_provenance).

pub(super) fn resolve_pointer_provenance<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, value: VmValue<'z3, 'tcx>, ) -> VmValue<'z3, 'tcx>

Penetrate a reference/raw-pointer target down to the owned heap behind it. A target like &mut ManuallyDrop<Box<T>> or *mut Box<T> carries the stack provenance of the referent; the properties that matter (Allocated/Owning/ValidPtr) concern the heap object inside, so resolve through the referent local’s owned heap field.

pub(super) fn is_vacuously_true_for_nullable<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> bool

Implicit vacuous truth for projected targets.

A property over x.unwrap_some() / x.iter() talks about the contents of an Option/container; when that container resolves to no allocation (e.g. Option::None, an empty or unmodeled container) there is no element to check, so the property holds vacuously. The explicit counterpart is the Null(p) guard (Self::is_null), which the user writes via any(Null(p), …).

pub(super) fn is_null<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, place: &ContractPlace<'tcx>, ) -> bool

Whether place is null, in the vacuity sense of the Null(p) guard: true when the value provably equals 0, or carries no provenance and is not known non-null (e.g. an Option::None or an unmodeled value). The implicit counterpart is Self::is_vacuously_true_for_nullable, which handles unwrap_some() / iter() projections without an explicit guard.

pub(super) fn smt_check<'z3>( &self, solver: &Solver<'z3>, condition: &Bool<'z3>, ) -> CheckResult

pub(super) fn smt_check_size_split<'z3, 'tcx>( vm_state: &VmState<'z3, 'tcx>, elem_size: &Int<'z3>, goal_negated: &Bool<'z3>, on_sat: CheckResult, ) -> CheckResult

Prove goal_negated is unsatisfiable under a case split on a generic element size S: the ZST branch (S = 0) and the non-ZST branch (S ≥ 1, where the S factor cancels). Both branches must be UNSAT. on_sat is the result when either branch is satisfiable.

pub(super) fn resolve_arg_term<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, arg: &PropertyArg<'tcx>, ) -> Option<Int<'z3>>

pub(super) fn count_is_zero<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, count_arg: usize, ) -> bool

Whether the element-count argument (defaulting to args[2], the [Target, Ty, Expr] layout) evaluates to the constant 0, making any InBound/Allocated byte-range check trivially satisfied. count_arg overrides the index for two-argument forms like Init(self, n).

pub(super) fn access_bytes<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, property: &Property<'tcx>, ty_arg: usize, count_arg: usize, checkpoint: &Checkpoint<'tcx>, value: &VmValue<'z3, 'tcx>, ) -> Int<'z3>

pub(super) fn zst_guard<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> bool

pub(super) fn is_zst_type<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, ty: Option<Ty<'tcx>>, ) -> bool

pub(super) fn is_concrete_zst<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, ty: Ty<'tcx>, ) -> bool

pub(super) fn is_generic_ty<'tcx>(&self, ty: Ty<'tcx>) -> bool

pub(super) fn instantiate_callsite_ty<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, ty: Ty<'tcx>, ) -> Ty<'tcx>

pub(super) fn instantiate_callsite_const<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, index: u32, ) -> Option<u128>

pub(super) fn resolve_ty_params<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, ty: Ty<'tcx>, ) -> Ty<'tcx>

pub(super) fn eval_contract_expr<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: Option<&Checkpoint<'tcx>>, expr: &ContractExpr<'tcx>, ) -> Option<Int<'z3>>

pub(super) fn eval_contract_expr_to_value<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: Option<&Checkpoint<'tcx>>, expr: &ContractExpr<'tcx>, ) -> Option<VmValue<'z3, 'tcx>>

pub(super) fn eval_contract_place<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: Option<&Checkpoint<'tcx>>, cp: &ContractPlace<'tcx>, ) -> Option<Int<'z3>>

pub(super) fn eval_contract_operand<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, op: &Operand<'tcx>, ) -> Option<Int<'z3>>

pub(super) fn trace_value<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, op: &Operand<'tcx>, ) -> VmValue<'z3, 'tcx>

pub(super) fn alloc_elem_is_array_of<'tcx>( &self, alloc_elem_ty: Ty<'tcx>, required_ty: Ty<'tcx>, ) -> bool

impl PropertyChecker

pub(crate) fn check<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn check_inner<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn check_or<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn check_and<'z3, 'tcx>( &self, vm_state: &VmState<'z3, 'tcx>, solver: &Solver<'z3>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult