rapx/verify/property_checker/

typed.rs

//! Checkers for `Typed` and `Size`.
//!
//! `Typed` matches an allocation's `element_ty` (or a field at the provenance
//! offset) against the expected type; `Size` checks `sized`/`unsized`/exact
//! size assertions.

use crate::helpers::mir_scan::Checkpoint;
use crate::verify::contract::{ContractExpr, Property, PropertyArg};
use crate::verify::report::{CheckResult, UnknownReason};
use crate::verify::vm::state::VmState;
#[cfg(rapx_has_attr_ir)]
use rustc_attr_ir::LangItem;
#[cfg(all(not(rapx_has_attr_ir), not(rapx_ge_100)))]
use rustc_hir::LangItem;
#[cfg(all(not(rapx_has_attr_ir), rapx_ge_100))]
use rustc_hir::attrs::lang_items::LangItem;
use rustc_middle::ty::{Ty, TyKind};
use z3::ast::Ast;

use super::PropertyChecker;

impl PropertyChecker {
    pub(super) fn check_typed<'z3, 'tcx>(
        &self,
        vm_state: &VmState<'z3, 'tcx>,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> CheckResult {
        let Some(value) = self.target_value(vm_state, checkpoint, property) else {
            return CheckResult::Unknown(UnknownReason::Unimplemented);
        };
        let expected = Self::ty_arg(property, 1);
        if let Some(expected_ty) = expected {
            let expected_ty = self.instantiate_callsite_ty(vm_state, checkpoint, expected_ty);

            let value_elem_ty = match value.ty.kind() {
                TyKind::RawPtr(inner, _) | TyKind::Ref(_, inner, _) => *inner,
                _ => value.ty,
            };

            // `MaybeUninit<T>` (and slices/arrays of it) carries no validity
            // invariant: any byte pattern is a valid `MaybeUninit<T>`.  A byte
            // buffer reinterpreted as `[MaybeUninit<T>]` (e.g. the slice handed
            // to `Box::from_raw_in` by `RawVec::into_box`) is therefore always
            // "typed" — alignment/size are discharged by the separate
            // `Align`/`Allocated` facts.
            if Self::ty_is_maybe_uninit(expected_ty) {
                return CheckResult::ProvedByRule;
            }

            // Check provenance: does the allocation's element type match the expected type?
            if let Some(alloc_id) = value.provenance_alloc_id() {
                let alloc = vm_state.alloc(alloc_id);
                if let Some(mut elem_ty) = alloc.element_ty.as_ty() {
                    // Resolve generic type param to concrete callsite type.
                    elem_ty = self.resolve_ty_params(vm_state, checkpoint, elem_ty);
                    if matches!(elem_ty.kind(), TyKind::Param(_)) {
                        let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, elem_ty);
                        if resolved != elem_ty {
                            elem_ty = resolved;
                        }
                    }
                    if elem_ty == expected_ty {
                        return CheckResult::ProvedByRule;
                    }
                    // An allocation of `T` elements is also "typed" when
                    // accessed through a slice/array pointer `[T]`/`[T; N]`
                    // (a slice is just N contiguous `T` elements, e.g. a `u8`
                    // buffer reinterpreted as `[u8]` by `slice_from_raw_parts`).
                    let expected_elem = match expected_ty.kind() {
                        TyKind::Slice(e) | TyKind::Array(e, _) => *e,
                        _ => expected_ty,
                    };
                    if elem_ty == expected_elem {
                        return CheckResult::ProvedByRule;
                    }
                    // MaybeUninit<T> accessed via raw pointer from as_mut_ptr:
                    // treat as T for write ops where caller will initialize it.
                    if let TyKind::Adt(adt_def, substs) = elem_ty.kind() {
                        if crate::verify::api_classify::is_maybe_uninit_type(adt_def.did())
                            && matches!(value.ty.kind(), TyKind::RawPtr(..))
                        {
                            if let Some(inner) = substs.first().and_then(|s| s.as_type()) {
                                if inner == expected_ty {
                                    if crate::verify::api_classify::is_mem_copy_or_write(
                                        checkpoint.callee,
                                    ) {
                                        return CheckResult::ProvedByRule;
                                    }
                                }
                            }
                        }
                    }
                    // Struct/enum field: check if expected_ty matches a field at the provenance offset.
                    if let TyKind::Adt(adt_def, substs) = elem_ty.kind() {
                        if !adt_def.is_enum() {
                            let off_u64 = value
                                .provenance
                                .as_ref()
                                .and_then(|p| p.offset.simplify().as_u64());
                            let variant = adt_def.non_enum_variant();
                            let mut accum: u64 = 0;
                            for (i, field_def) in variant.fields.iter().enumerate() {
                                let field_off = vm_state.field_offset_in_bytes(elem_ty, i);
                                if i > 0 && field_off == 0 {
                                    accum = 0;
                                }
                                let field_ty: Ty<'tcx> = crate::helpers::mir_utils::field_ty(
                                    vm_state.tcx,
                                    field_def,
                                    substs,
                                );
                                if field_ty == expected_ty {
                                    if off_u64 == Some(accum) {
                                        if value.facts.init {
                                            return CheckResult::ProvedByRule;
                                        }
                                        return CheckResult::Failed;
                                    }
                                } else if off_u64 == Some(accum) {
                                    // Unwrap ManuallyDrop<T> → T for unions like MaybeUninit.
                                    if let TyKind::Adt(wrap_adt, wrap_substs) = field_ty.kind() {
                                        if !wrap_adt.is_enum() {
                                            if (vm_state.tcx.is_lang_item(
                                                wrap_adt.did(),
                                                LangItem::ManuallyDrop,
                                            ) || vm_state
                                                .tcx
                                                .is_lang_item(wrap_adt.did(), LangItem::UnsafeCell))
                                                && wrap_substs.first().and_then(|s| s.as_type())
                                                    == Some(expected_ty)
                                            {
                                                if vm_state.content(alloc_id).facts.initialized {
                                                    return CheckResult::ProvedByRule;
                                                }
                                                return CheckResult::Failed;
                                            }
                                        }
                                    }
                                }
                                accum += vm_state.size_of_ty(field_ty).max(1);
                            }
                        }
                    }
                    // ForEach (`buckets.iter()`): the allocation stores pointers
                    // (`*mut T`), but the invariant applies to the pointee (`T`).
                    // Unwrap *const/*mut to match.
                    if property.for_each().is_some() {
                        if let TyKind::RawPtr(inner, _) = elem_ty.kind() {
                            if *inner == expected_ty {
                                return CheckResult::ProvedByRule;
                            }
                        }
                    }
                    // A single pointer loaded from a container whose
                    // `Typed(container.iter(), T)` invariant established the
                    // element target type (`let cur = buckets[i]`). The fact comes
                    // from the invariant, so this does not bless dangling pointers
                    // in containers that carry no such invariant.
                    if let Some(target) = vm_state.alloc(alloc_id).facts.for_each.target_ty {
                        if target == expected_ty {
                            return CheckResult::ProvedByRule;
                        }
                    }
                    // Transmute to an all-bit-valid destination type
                    // (integers, floats, raw pointers): any byte pattern is
                    // a valid value, so a reinterpretation from a
                    // differently-typed allocation is sound (e.g. memchr
                    // reads `[u8]` as `usize`).  This is only sound when the
                    // pointer is also correctly aligned to the destination
                    // type: a raw `*const u8 as *const u32` cast over
                    // align-1 storage is misaligned and must stay UNSOUND.
                    if Self::all_bit_patterns_valid(expected_ty) {
                        let expected_align = vm_state.align_of_ty(expected_ty).max(1);
                        if Self::value_aligned_to(vm_state, &value, expected_align) {
                            return CheckResult::ProvedByRule;
                        }
                    }
                    // Non-ADT element type that doesn't match → Failed.
                    if !matches!(elem_ty.kind(), TyKind::Adt(..)) {
                        return CheckResult::Failed;
                    }
                    // ADT type with no matching field and no init → Failed.
                    if !value.facts.init {
                        return CheckResult::Failed;
                    }
                }
            }

            // No provenance: fall back to init and size checks.
            if value.facts.init {
                if vm_state.size_of_ty(value_elem_ty) > 0
                    && vm_state.size_of_ty(expected_ty) > 0
                    && vm_state.size_of_ty(value_elem_ty) == vm_state.size_of_ty(expected_ty)
                {
                    return CheckResult::ProvedByRule;
                }
            }

            // For ForEach (for_each) properties, the invariant applies to
            // individual elements loaded from a container. The VM may not track
            // provenance through memory loads from heap allocations. When sizes
            // match, trust the type.
            if property.for_each().is_some() {
                if vm_state.size_of_ty(value_elem_ty) > 0
                    && vm_state.size_of_ty(expected_ty) > 0
                    && vm_state.size_of_ty(value_elem_ty) == vm_state.size_of_ty(expected_ty)
                {
                    return CheckResult::ProvedByRule;
                }
            }

            // When we have provenance but the element type doesn't match and
            // sizes match, assume the type is correct. This handles pointers
            // loaded from container elements where individual provenance is lost.
            let vs = vm_state.size_of_ty(value_elem_ty);
            let es = vm_state.size_of_ty(expected_ty);
            if let Some(alloc_id) = value.provenance_alloc_id()
                && vs == es
            {
                if !vm_state.alloc(alloc_id).element_ty.is_generic() {
                    return CheckResult::ProvedByRule;
                }
            }

            if vs > 0 && es > 0 && vs != es {
                return CheckResult::Failed;
            }
        }
        CheckResult::Unknown(UnknownReason::Unimplemented)
    }

    pub(super) fn ty_is_maybe_uninit(ty: Ty<'_>) -> bool {
        crate::verify::api_classify::is_maybe_uninit_ty(ty)
    }

    pub(super) fn check_size<'z3, 'tcx>(
        &self,
        vm_state: &VmState<'z3, 'tcx>,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> CheckResult {
        let ty = match property.args().iter().find_map(|a| match a {
            PropertyArg::Ty(t) => Some(*t),
            _ => None,
        }) {
            Some(t) => t,
            None => return CheckResult::Unknown(UnknownReason::Unimplemented),
        };
        // Resolve a generic `T` to the call-site concrete type (e.g. `Box<i32>`
        // for `drop_in_place::<Box<i32>>`), so `Size(T, 0)` is decided rather
        // than left `Unknown` and dragged through `ValidPtr`'s `Size || Deref`.
        let resolved_ty = self.instantiate_callsite_ty(vm_state, checkpoint, ty);

        match property.args().last() {
            Some(PropertyArg::Ident(id)) if id == "sized" => {
                // For a generic type parameter (`T: Sized`) the concrete size is
                // unknown, but the `non-ZST` constraint is a caller obligation
                // (mirroring the `inject_layout_constraints` convention that a
                // generic `SizeOf(T)` term is `>= 1`).  Functions that panic on
                // ZST — `offset_from`, `size_of_val`, ... — are sound for every
                // `T`, so treating the constraint as satisfied is safe.
                if self.is_generic_ty(ty) {
                    return CheckResult::ProvedByRule;
                }
                if vm_state.size_of_ty(ty) == 0 {
                    CheckResult::Failed
                } else {
                    CheckResult::ProvedByRule
                }
            }
            Some(PropertyArg::Ident(id)) if id == "unsized" => match ty.kind() {
                TyKind::Slice(_) | TyKind::Str | TyKind::Dynamic(..) => CheckResult::ProvedByRule,
                _ => CheckResult::Unknown(UnknownReason::Unimplemented),
            },
            Some(PropertyArg::Expr(ContractExpr::Const(c))) => {
                let ty = resolved_ty;
                if self.is_generic_ty(ty) {
                    return CheckResult::Unknown(UnknownReason::Unimplemented);
                }
                if vm_state.size_of_ty(ty) as u128 == *c {
                    CheckResult::ProvedByRule
                } else {
                    CheckResult::Failed
                }
            }
            _ => CheckResult::Unknown(UnknownReason::Unimplemented),
        }
    }

    pub(super) fn check_no_padding<'z3, 'tcx>(
        &self,
        vm_state: &VmState<'z3, 'tcx>,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> CheckResult {
        let Some(ty) = property.args().iter().find_map(|a| match a {
            PropertyArg::Ty(t) => Some(*t),
            _ => None,
        }) else {
            return CheckResult::Unknown(UnknownReason::Unimplemented);
        };
        let ty = self.instantiate_callsite_ty(vm_state, checkpoint, ty);
        match self.type_has_no_padding(vm_state, ty) {
            Some(true) => CheckResult::ProvedByRule,
            Some(false) => CheckResult::Failed,
            None => CheckResult::Unknown(UnknownReason::Unimplemented),
        }
    }

    /// 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).
    fn type_has_no_padding<'tcx>(
        &self,
        vm_state: &VmState<'_, 'tcx>,
        ty: Ty<'tcx>,
    ) -> Option<bool> {
        let tcx = vm_state.tcx;
        if self.is_generic_ty(ty) {
            return None;
        }
        match ty.kind() {
            TyKind::Bool
            | TyKind::Char
            | TyKind::Int(_)
            | TyKind::Uint(_)
            | TyKind::Float(_)
            | TyKind::RawPtr(..)
            | TyKind::Ref(..)
            | TyKind::FnPtr(..)
            | TyKind::Never => Some(true),
            TyKind::Array(elem, _) => self.type_has_no_padding(vm_state, *elem),
            TyKind::Tuple(elems) => {
                let mut sum = 0u64;
                for elem in *elems {
                    match self.type_has_no_padding(vm_state, elem) {
                        Some(true) => sum += vm_state.size_of_ty(elem),
                        Some(false) => return Some(false),
                        None => return None,
                    }
                }
                Some(vm_state.size_of_ty(ty) == sum)
            }
            TyKind::Adt(adt_def, substs) if !adt_def.is_enum() && !adt_def.is_union() => {
                let variant = adt_def.non_enum_variant();
                let mut sum = 0u64;
                for field_def in variant.fields.iter() {
                    let field_ty: Ty<'tcx> =
                        crate::helpers::mir_utils::field_ty(tcx, field_def, substs);
                    match self.type_has_no_padding(vm_state, field_ty) {
                        Some(true) => sum += vm_state.size_of_ty(field_ty),
                        Some(false) => return Some(false),
                        None => return None,
                    }
                }
                Some(vm_state.size_of_ty(ty) == sum)
            }
            _ => None,
        }
    }
}