Struct SmtChecker 

pub struct SmtChecker<'tcx> {
    pub(crate) tcx: TyCtxt<'tcx>,
}

SMT backend for verifier properties.

Fields

tcx: TyCtxt<'tcx>

Implementations

impl<'tcx> SmtChecker<'tcx>

pub fn new(tcx: TyCtxt<'tcx>) -> Self

Create an SMT checker for the current compiler type context.

pub fn check( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, forward: &ForwardVisitResult<'tcx>, ) -> SmtCheckResult

Try to prove one property using SMT.

pub fn check_for_checkpoint( &self, caller: DefId, property: &Property<'tcx>, forward: &ForwardVisitResult<'tcx>, ) -> SmtCheckResult

Try to prove one property at a return checkpoint (struct invariant).

Unlike [check], this does not use callee-to-caller argument mapping because struct invariant properties are already resolved in the caller’s local namespace.

pub(crate) fn prove_obligation( &self, checkpoint: &Checkpoint<'tcx>, forward: &ForwardVisitResult<'tcx>, obligation: SmtObligation, ) -> SmtCheckResult

Prove one already-lowered common SMT obligation.

pub(crate) fn prove_obligation_for_checkpoint( &self, caller: DefId, forward: &ForwardVisitResult<'tcx>, obligation: SmtObligation, ) -> SmtCheckResult

Prove one lowered obligation at a return checkpoint (struct invariant).

Wraps prove_obligation with a minimal dummy checkpoint that only carries the caller DefId. No callee-to-caller argument mapping is needed.

pub(crate) fn property_target( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<PlaceKey>

Resolve the target place of a property at a concrete checkpoint.

pub(crate) fn property_place_arg( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, index: usize, ) -> Option<PlaceKey>

Resolve the index-th property argument as a concrete checkpoint place.

pub(crate) fn property_target_direct( &self, property: &Property<'tcx>, ) -> Option<PlaceKey>

Resolve the target place of a property directly from a contract place without going through callee argument mapping.

fn resolve_contract_place(&self, place: &ContractPlace<'tcx>) -> PlaceKey

Convert a contract place to a PlaceKey, resolving Arg(n) to Local(n+1).

pub(crate) fn property_required_ty( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<Ty<'tcx>>

Resolve the type argument used by an alignment property.

pub(crate) fn property_required_ty_direct( &self, property: &Property<'tcx>, ) -> Option<Ty<'tcx>>

Resolve the type argument of a property directly without callee generic instantiation.

pub(crate) fn property_len_expr_direct( &self, property: &Property<'tcx>, ) -> Option<ContractExpr<'tcx>>

Resolve the trailing length expression directly (without checkpoint binding).

For checkpoint checks this extracts the last argument as an expression using the function’s own parameter space.

pub(crate) fn property_len_expr( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<ContractExpr<'tcx>>

Resolve the trailing length expression at a concrete checkpoint.

This keeps constants unchanged and rewrites callee argument places, such as Arg_2 from std-contract JSON, to the concrete MIR place passed by the caller at this checkpoint. Composite numeric expressions are rebound recursively.

pub(crate) fn contract_expr_to_smt_term( &self, caller: DefId, expr: &ContractExpr<'tcx>, ) -> Option<SmtTerm>

Lower a rebound contract arithmetic expression into the common SMT term model.

pub(crate) fn property_numeric_predicates( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<Vec<NumericPredicate<'tcx>>>

Resolve a ValidNum predicate list at a concrete checkpoint.

pub(crate) fn numeric_predicate_to_smt_predicate( &self, caller: DefId, predicate: &NumericPredicate<'tcx>, ) -> Option<SmtPredicate>

Convert a rebound contract predicate into the shared SMT predicate model.

pub(crate) fn property_numeric_smt_predicates( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<Vec<SmtPredicate>>

Resolve and lower ValidNum predicates, expanding non-scalar helpers.

pub(crate) fn property_index_access_in_bound_predicates( &self, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Option<Vec<SmtPredicate>>

Resolve an InBound(index_access(slice, index)) property to range predicates.

fn expand_index_access_predicate( &self, checkpoint: &Checkpoint<'tcx>, predicate: &NumericPredicate<'tcx>, ) -> Option<Option<Vec<SmtPredicate>>>

fn index_access_in_bound_predicates( &self, checkpoint: &Checkpoint<'tcx>, expr: &ContractExpr<'tcx>, ) -> Option<Vec<SmtPredicate>>

fn slice_index_bounds( &self, caller: DefId, index: &ContractExpr<'tcx>, len: SmtTerm, ) -> Option<(SmtTerm, SmtTerm)>

fn slice_index_kind( &self, caller: DefId, index: &ContractExpr<'tcx>, ) -> Option<SliceIndexKind>

fn contract_expr_field_term( &self, caller: DefId, expr: &ContractExpr<'tcx>, field: usize, ) -> Option<SmtTerm>

fn contract_expr_place(&self, expr: &ContractExpr<'tcx>) -> Option<PlaceKey>

fn contract_expr_label(&self, expr: &ContractExpr<'tcx>) -> Option<String>

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

pub(crate) fn infer_pointee_ty( &self, caller: DefId, place: &PlaceKey, ) -> Option<Ty<'tcx>>

pub(crate) fn is_len_carrying_place_for_caller( &self, caller: DefId, place: &PlaceKey, ) -> bool

Return true if a place is a safe reference/slice/string carrying object length.

fn bind_contract_expr_to_callsite( &self, checkpoint: &Checkpoint<'tcx>, expr: &ContractExpr<'tcx>, ) -> Option<ContractExpr<'tcx>>

fn contract_place_to_callsite_expr( &self, checkpoint: &Checkpoint<'tcx>, place: &ContractPlace<'tcx>, ) -> Option<ContractExpr<'tcx>>

fn callsite_arg_expr( &self, checkpoint: &Checkpoint<'tcx>, index: usize, fields: &[usize], ) -> Option<ContractExpr<'tcx>>

pub(crate) fn contract_place_to_callsite_place( &self, checkpoint: &Checkpoint<'tcx>, place: &ContractPlace<'tcx>, ) -> Option<PlaceKey>

Convert a contract place into a concrete MIR place when possible.

pub(crate) fn callsite_arg_place( &self, checkpoint: &Checkpoint<'tcx>, index: usize, ) -> Option<PlaceKey>

Return the concrete MIR place used as the index-th call argument.

pub(crate) fn callsite_arg_smt_term( &self, checkpoint: &Checkpoint<'tcx>, index: usize, ) -> Option<SmtTerm>

Return the index-th call argument as a common SMT term.

pub(crate) fn place_pointee_size( &self, caller: DefId, place: &PlaceKey, ) -> Option<u64>

Return the pointee size for a concrete pointer place.

pub(crate) fn callsite_arg_place_with_fields( &self, checkpoint: &Checkpoint<'tcx>, index: usize, fields: &[usize], ) -> Option<PlaceKey>

Return the index-th call argument with contract projections appended.

pub(crate) fn instantiate_callsite_ty( &self, checkpoint: &Checkpoint<'tcx>, ty: Ty<'tcx>, ) -> Ty<'tcx>

Replace a callee generic parameter with its concrete checkpoint type.

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

Replace a callee const generic parameter with its concrete checkpoint value.

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

Return ABI alignment and size for a type.

pub(crate) fn required_alignment( &self, caller: DefId, ty: Ty<'tcx>, ) -> Option<u64>

Return the alignment required by a property type.

For concrete types this is the ABI alignment. For generic parameters with finite representative candidates, the requirement must hold for every candidate, so we use the maximum candidate alignment.

pub(crate) fn required_size(&self, caller: DefId, ty: Ty<'tcx>) -> Option<u64>

Return a conservative byte size for a concrete or bounded generic type.

For a generic parameter with representative candidates, every candidate must satisfy a numeric precondition. We therefore use the maximum candidate size for upper-bound formulas such as size_of(T) * len <= isize::MAX.

pub(crate) fn type_size_class( &self, caller: DefId, ty: Ty<'tcx>, ) -> TypeSizeClass

Classify whether a type is definitely zero-sized, definitely non-zero, or still layout-ambiguous under the current generic bounds.

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

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