rapx 0.7.32

A static analysis platform for Rust program analysis and verification
//! Symbolic memory model for the VM.

use rustc_middle::{
    mir::{Local, Place, ProjectionElem},
    ty::{PseudoCanonicalInput, Ty, TyKind, TypingEnv},
};
use z3::ast::{Ast, Int};

use super::state::{AllocId, Allocation, Provenance, VmState, VmValue, ValueInvariants};

impl<'ctx, 'tcx> VmState<'ctx, 'tcx> {
    pub fn address_of_place(&mut self, place: &Place<'tcx>) -> Option<VmValue<'ctx, 'tcx>> {
        self.ensure_local_allocation(place.local);

        let zero = Int::from_u64(self.ctx, 0);

        if place.projection.is_empty() {
            let base_addr = self.local_address(place.local);
            let ty = self.body.local_decls[place.local].ty;
            // Prefer the local's value provenance over the stack-allocation
            // provenance. For Box/Vec parameters, the value tracks the heap
            // allocation while local_alloc_ids tracks the stack location.
            let provenance = self.locals.get(&place.local)
                .and_then(|v| v.provenance.clone())
                .or_else(|| self.local_alloc_ids.get(&place.local).copied()
                    .map(|alloc_id| Provenance { alloc_id, offset: zero }));
            return Some(VmValue {
                term: base_addr,
                ty,
                provenance,
                invariants: ValueInvariants::default(),
            });
        }

        let mut term = self.local_address(place.local);
        let mut provenance: Option<Provenance<'ctx>> = self
            .local_alloc_ids
            .get(&place.local)
            .copied()
            .map(|alloc_id| Provenance {
                alloc_id,
                offset: zero.clone(),
            });
        let mut current_ty = self.body.local_decls[place.local].ty;

        for proj in place.projection.iter() {
            let mut handled = false;
            if let ProjectionElem::Index(local) = proj {
                if let Some(val) = self.locals.get(&local) {
                    if let Some(idx) = val.term.simplify().as_u64() {
                        let elem_sz = Int::from_u64(self.ctx, self.size_of_ty(current_ty));
                        let scaled = Int::mul(self.ctx, &[&Int::from_u64(self.ctx, idx), &elem_sz]);
                        term = Int::add(self.ctx, &[&term, &scaled]);
                        if let Some(ref mut prov) = provenance {
                            prov.offset = Int::add(self.ctx, &[&prov.offset, &scaled]);
                        }
                        handled = true;
                    }
                }
                if !handled {
                    let idx = self.fresh_int("idx");
                    let elem_size = self.size_of_ty(current_ty);
                    let elem_sz = Int::from_u64(self.ctx, elem_size);
                    let scaled = Int::mul(self.ctx, &[&idx, &elem_sz]);
                    term = Int::add(self.ctx, &[&term, &scaled]);
                    if let Some(ref mut prov) = provenance {
                        prov.offset = Int::add(self.ctx, &[&prov.offset, &scaled]);
                    }
                }
                continue;
            }
            match proj.kind() {
                ProjectionElem::Field(field_idx, _) => {
                    let field_offset = self.field_offset_in_bytes(current_ty, field_idx.as_usize());
                    let field_off = Int::from_u64(self.ctx, field_offset);
                    term = Int::add(self.ctx, &[&term, &field_off]);
                    if let Some(ref mut prov) = provenance {
                        prov.offset = Int::add(self.ctx, &[&prov.offset, &field_off]);
                    }
                }
                ProjectionElem::Deref => {
                    let pointed = self.locals.get(&place.local)?;
                    term = pointed.term.clone();
                    provenance = pointed.provenance.clone();
                    // For fat pointers (aggregates without provenance),
                    // use the first field's provenance (the data pointer).
                    if provenance.is_none()
                        && matches!(pointed.ty.kind(), TyKind::RawPtr(..))
                    {
                        if let Some(field0) = self.field_value(place.local, &[0]) {
                            provenance = field0.provenance.clone();
                        }
                    }
                    if let TyKind::Ref(_, deref_ty, _) = current_ty.kind() {
                        current_ty = *deref_ty;
                    }
                }
                _ => {
                    self.notes.push(format!("unsupported projection: {:?}", proj.kind()));
                    return None;
                }
            }
        }

        let ty = place.ty(self.body, self.tcx).ty;
        Some(VmValue {
            term,
            ty,
            provenance,
            invariants: ValueInvariants::default(),
        })
    }

    /// Lazily create a stack allocation for a MIR local if one doesn't exist.
    pub(crate) fn ensure_local_allocation(&mut self, local: Local) {
        if self.local_alloc_ids.contains_key(&local) {
            return;
        }
        let ty = self.body.local_decls[local].ty;
        let size = self.size_of_ty(ty) as u64;
        let align = self.align_of_ty(ty);
        let size_term = Int::from_u64(self.ctx, size.max(1));
        let base = self.local_address(local);
        let id = AllocId(self.next_alloc_id);
        self.next_alloc_id += 1;
        // For arrays, track the element type (not the array type) so that
        // len() computes `size / elem_size` correctly.
        let element_ty = match ty.kind() {
            TyKind::Array(elem, _) => Some(*elem),
            _ => Some(ty),
        };
        let alloc = Allocation {
            id,
            base,
            size: size_term,
            align,
            element_ty,
            is_external: false,
        };
        self.allocations.push(alloc);
        self.local_alloc_ids.insert(local, id);
    }

    pub(crate) fn field_offset_in_bytes(&self, ty: Ty<'tcx>, field_idx: usize) -> u64 {
        let Some(layout) = self.compute_layout(ty) else { return 0 };
        match layout.fields {
            rustc_abi::FieldsShape::Arbitrary { ref offsets, .. } => {
                let idx = rustc_abi::FieldIdx::from_usize(field_idx);
                if idx.as_usize() < offsets.len() { return offsets[idx].bytes(); }
            }
            _ => {}
        }
        0
    }

    pub fn size_of_ty(&self, ty: Ty<'tcx>) -> u64 {
        self.compute_layout(ty).map(|l| l.size.bytes()).unwrap_or(0)
    }

    pub fn align_of_ty(&self, ty: Ty<'tcx>) -> u64 {
        self.compute_layout(ty).map(|l| l.align.abi.bytes()).unwrap_or(1)
    }

    fn compute_layout(&self, ty: Ty<'tcx>) -> Option<rustc_abi::TyAndLayout<'tcx, Ty<'tcx>>> {
        let typing_env = TypingEnv::post_analysis(self.tcx, self.caller_def_id);
        let input = PseudoCanonicalInput { typing_env, value: ty };
        crate::helpers::mir_utils::catch_panic(|| self.tcx.layout_of(input))
            .ok()
            .and_then(|r| r.ok())
    }

    pub fn alloc_for_local(&self, local: Local) -> Option<AllocId> {
        self.local_alloc_ids.get(&local).copied()
    }

    pub fn allocation_size(&self, alloc_id: AllocId) -> Option<&Int<'ctx>> {
        self.allocations.iter().find(|a| a.id == alloc_id).map(|a| &a.size)
    }

    pub fn allocation_base(&self, alloc_id: AllocId) -> Option<&Int<'ctx>> {
        self.allocations.iter().find(|a| a.id == alloc_id).map(|a| &a.base)
    }

    /// Get the element size (in bytes) for a pointer type, peeling
    /// through `*const T`, `*mut T`, `&T`, and `&[T]` to find `size_of(T)`.
    pub fn pointee_elem_size(&self, ty: Ty<'tcx>) -> u64 {
        let inner = match ty.kind() {
            TyKind::RawPtr(inner_ty, _) | TyKind::Ref(_, inner_ty, _) => *inner_ty,
            _ => ty,
        };
        match inner.kind() {
            TyKind::Slice(elem) => self.size_of_ty(*elem),
            _ => self.size_of_ty(inner),
        }
    }
}