rapx/verify/property_checker/
transmute.rs

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

rapx/verify/property_checker/
transmute.rs
