Struct PropertyChecker 

pub struct PropertyChecker;

Implementations

impl PropertyChecker

pub(super) fn check_alias<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

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

impl PropertyChecker

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

pub(super) fn count_is_offset_of<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, value: &VmValue<'ctx, '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<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

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

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

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

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

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

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

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

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

impl PropertyChecker

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

fn check_valid_cstr_from_known_nul<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, '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<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>, alloc_id: AllocId, alloc_size: &Int<'ctx>, ) -> 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<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, checkpoint: &Checkpoint<'tcx>, _property: &Property<'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<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

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

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

fn is_maybe_uninit_ptr<'ctx, 'tcx>( vm_state: &VmState<'ctx, 'tcx>, value: &VmValue<'ctx, '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<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

fn allocation_covers_access<'ctx, 'tcx>( vm_state: &VmState<'ctx, 'tcx>, value: &VmValue<'ctx, 'tcx>, access: &Int<'ctx>, base: &Int<'ctx>, size: &Int<'ctx>, on_sat: CheckResult, ) -> 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.

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

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

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

impl PropertyChecker

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

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

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

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

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

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

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

impl PropertyChecker

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

impl PropertyChecker

pub(super) fn check_valid_transmute<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>, _checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

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

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

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

Return true if ty is core::simd::Simd<T, N>.

fn ty_size<'ctx, 'tcx>(vm_state: &VmState<'ctx, '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<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> CheckResult

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

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

impl PropertyChecker

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

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

pub(super) fn is_guard_null<'ctx, 'tcx>( &self, vm_state: &VmState<'ctx, 'tcx>, checkpoint: &Checkpoint<'tcx>, guard_key: &PlaceKey, ) -> bool

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pub(super) fn has_iter_elements<'tcx>(&self, property: &Property<'tcx>) -> bool

impl PropertyChecker

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

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

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