rapx/verify/property_checker/
transmute.rs

1//! Transmute / trait / size property checking for the symbolic VM.
2
3use rustc_middle::ty::{GenericArgKind, Ty, TyKind};
4use z3::Solver;
5
6use crate::verify::{
7    contract::{Property, PropertyArg},
8    report::CheckResult,
9};
10use crate::helpers::mir_scan::Checkpoint;
11use crate::verify::vm::state::VmState;
12
13use super::PropertyChecker;
14
15impl PropertyChecker {
16    // ── check_valid_transmute ──────────────────────────────────
17
18    pub(super) fn check_valid_transmute<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
19        _checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
20    {
21        let src = property.args().get(0).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
22        let dst = property.args().get(1).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
23        match (src, dst) {
24            (Some(s), Some(d)) if vm_state.size_of_ty(s) == vm_state.size_of_ty(d) => CheckResult::Proved,
25            (Some(s), Some(d)) => {
26                let ss = vm_state.size_of_ty(s);
27                let ds = vm_state.size_of_ty(d);
28                if ss == 0 || ds == 0 {
29                    // One or both types are generic; sizes are opaque.
30                    // Trust the type system: the call compiles, so
31                    // the transmute is compatible.
32                    CheckResult::Proved
33                } else if ss == ds {
34                    CheckResult::Proved
35                } else {
36                    CheckResult::Failed
37                }
38            }
39            _ => CheckResult::Proved,
40        }
41    }
42
43    // ── check_trait ────────────────────────────────────────────
44
45    pub(super) fn check_trait<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
46        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
47    {
48        let ty = match property.args().first() {
49            Some(PropertyArg::Ty(ty)) => *ty,
50            _ => return CheckResult::Unknown,
51        };
52        let trait_name = match property.args().get(1) {
53            Some(PropertyArg::Ident(name)) => name.as_str(),
54            _ => return CheckResult::Unknown,
55        };
56
57        let tcx = vm_state.tcx;
58
59        if trait_name == "Copy" {
60            let typing_env = rustc_middle::ty::TypingEnv::post_analysis(tcx, checkpoint.caller);
61            if tcx.type_is_copy_modulo_regions(typing_env, ty) {
62                return CheckResult::Proved;
63            }
64            // Resolve generic param to concrete type via FnDef args
65            let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, ty);
66            if resolved != ty && tcx.type_is_copy_modulo_regions(typing_env, resolved) {
67                return CheckResult::Proved;
68            }
69        }
70
71        if trait_name == "Sized" {
72            if !ty.is_sized(tcx, rustc_middle::ty::TypingEnv::post_analysis(tcx, checkpoint.caller)) {
73                return CheckResult::Failed;
74            }
75            return CheckResult::Proved;
76        }
77
78        let predicates = crate::compat::predicates_of(tcx, checkpoint.caller);
79        #[cfg(not(rapx_ge_100))]
80        let pred_iter = predicates.predicates.iter();
81        #[cfg(rapx_ge_100)]
82        let pred_iter = predicates.clauses.iter();
83        for (predicate, _span) in pred_iter {
84            if let rustc_middle::ty::ClauseKind::Trait(trait_ref) = predicate.kind().skip_binder() {
85                if trait_ref.self_ty() == ty {
86                    let def_path = tcx.def_path_str(trait_ref.def_id());
87                    let short_name = def_path.rsplit("::").next().unwrap_or(&def_path);
88                    if short_name == trait_name {
89                        return CheckResult::Proved;
90                    }
91                }
92            }
93        }
94
95        CheckResult::Unknown
96    }
97
98    // ── check_split_transmute ──────────────────────────────────
99
100    pub(super) fn check_split_transmute<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
101        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
102    {
103        if vm_state.contract_flags.split_transmute_asserted {
104            return CheckResult::Proved;
105        }
106        let src = property.args().get(0).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
107        let dst = property.args().get(1).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
108        let src = src.map(|ty| self.instantiate_callsite_ty(vm_state, checkpoint, ty));
109        let dst = dst.map(|ty| self.instantiate_callsite_ty(vm_state, checkpoint, ty));
110        match (src, dst) {
111            (Some(mut s), Some(mut d)) => {
112                // If the type is a slice (e.g. `[T]` from contract parsing), unwrap
113                // to the element type.  `unwrap_array_expr` strips the array expr
114                // in the parser, but some paths (e.g. `parse_type` fallback) may
115                // keep the slice wrapper.
116                if let TyKind::Slice(elem) = s.kind() {
117                    s = *elem;
118                }
119                if let TyKind::Slice(elem) = d.kind() {
120                    d = *elem;
121                }
122
123                // If the source and destination element types are the same,
124                // transmute is trivially valid.
125                if s == d {
126                    return CheckResult::Proved;
127                }
128
129                // If the destination is a SIMD vector with a matching lane type,
130                // the transmute is valid by the standard library contract.
131                if Self::is_simd_vector(vm_state, d) {
132                    if let TyKind::Adt(_, args) = d.kind() {
133                        if args.iter().any(|a| matches!(a.kind(), GenericArgKind::Type(t) if t == s)) {
134                            return CheckResult::Proved;
135                        }
136                    }
137                }
138
139                let src_sz = Self::ty_size(vm_state, s);
140                let dst_sz = Self::ty_size(vm_state, d);
141                if src_sz == 0 || dst_sz == 0 { return CheckResult::Failed; }
142                // A split transmute is sound whenever the destination element
143                // type accepts all bit patterns (integers, floats, raw pointers):
144                // any contiguous `size_of::<U>()`-byte chunk of the source is
145                // then a valid destination value. This holds for both narrowing
146                // (`[usize]` -> `[u8]`, src_sz >= dst_sz) and widening
147                // (`[u8]` -> `[usize]`, src_sz < dst_sz) transmutes.
148                if Self::all_bit_patterns_valid(d) {
149                    return CheckResult::Proved;
150                }
151                CheckResult::Failed
152            }
153            _ => CheckResult::Failed,
154        }
155    }
156
157    /// Return true if `ty` is `core::simd::Simd<T, N>`.
158    fn is_simd_vector<'ctx, 'tcx>(vm_state: &VmState<'ctx, 'tcx>, ty: Ty<'tcx>) -> bool {
159        if let TyKind::Adt(adt_def, _) = ty.kind() {
160            let name = vm_state.tcx.item_name(adt_def.did());
161            if name.as_str() == "Simd" {
162                let path = vm_state.tcx.def_path_str(adt_def.did());
163                return path.contains("::simd::");
164            }
165        }
166        false
167    }
168
169    /// Compute type size, trying different typing environments.
170    fn ty_size<'ctx, 'tcx>(vm_state: &VmState<'ctx, 'tcx>, ty: Ty<'tcx>) -> u64 {
171        let sz = vm_state.size_of_ty(ty);
172        if sz > 0 { return sz; }
173        // Fallback 1: try with the monomorphized environment.
174        let typing_env = rustc_middle::ty::TypingEnv::post_analysis(
175            vm_state.tcx, vm_state.caller_def_id);
176        let sz = crate::helpers::mir_utils::catch_panic(|| {
177            vm_state.tcx.layout_of(
178                rustc_middle::ty::PseudoCanonicalInput { typing_env, value: ty }
179            )
180        }).ok().and_then(|r| r.ok()).map(|l| l.size.bytes()).unwrap_or(0);
181        if sz > 0 { return sz; }
182        // Fallback 2: for generic type params, enumerate impl sizes.
183        let generic_sz = crate::helpers::mir_utils::size_of_generic_param(vm_state.tcx, vm_state.caller_def_id, ty);
184        if generic_sz > 0 { return generic_sz; }
185        0
186    }
187
188    /// Returns true for integer and float types that accept all possible bit patterns
189    /// as valid values.  Types like bool, char, and enums have restricted validity.
190    /// Tuples and arrays are all-bit-patterns-valid iff every component is, so a
191    /// widening `SplitTransmute` such as `[u8] -> [(usize, usize)]` (used by
192    /// `memrchr`) is recognised.
193    pub(super) fn all_bit_patterns_valid(ty: Ty<'_>) -> bool {
194        match ty.kind() {
195            rustc_middle::ty::TyKind::Uint(_) => true,
196            rustc_middle::ty::TyKind::Int(_) => true,
197            rustc_middle::ty::TyKind::Float(_) => true,
198            rustc_middle::ty::TyKind::RawPtr(..) => true,
199            rustc_middle::ty::TyKind::Tuple(elems) => {
200                elems.iter().all(|e| Self::all_bit_patterns_valid(e))
201            }
202            rustc_middle::ty::TyKind::Array(elem, _) => Self::all_bit_patterns_valid(*elem),
203            _ => false,
204        }
205    }
206}
rapx/verify/property_checker/transmute.rs

rapx/verify/property_checker/
transmute.rs
