rapx/verify/property_checker/
util.rs

1use rustc_middle::mir::{Local, Operand, Rvalue, StatementKind, TerminatorKind};
2use rustc_middle::ty::{GenericArg, GenericArgKind, Ty, TyKind};
3#[cfg(not(rapx_has_skip_norm_wip))]
4use crate::compat::SkipNormWip;
5use z3::{SatResult, Solver, ast::{Ast, Bool, Int}};
6use crate::verify::contract::{ContractExpr, ContractProjection, NumericOp, PlaceBase, Property, PropertyArg, RelOp};
7use crate::verify::report::CheckResult;
8use crate::helpers::mir_scan::Checkpoint;
9use crate::verify::vm::state::{VmState, VmValue};
10
11use super::PropertyChecker;
12
13impl PropertyChecker {
14    pub(super) fn target_value<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
15        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> Option<VmValue<'ctx, 'tcx>>
16    {
17        let cp = match property.args().first()? {
18            PropertyArg::Expr(ContractExpr::Const(n)) => {
19                let idx = usize::try_from(*n).ok()?;
20                crate::verify::contract::ContractPlace {
21                    base: PlaceBase::Arg(idx),
22                    projections: vec![],
23                }
24            }
25            PropertyArg::Predicates(_) | PropertyArg::Ty(_) | PropertyArg::Ident(_) => return None,
26            PropertyArg::Expr(ContractExpr::Place(cp)) => cp.clone(),
27            PropertyArg::Expr(ContractExpr::IndexAccess { slice, .. }) => {
28                match slice.as_ref() {
29                    ContractExpr::Place(cp) => cp.clone(),
30                    _ => return None,
31                }
32            }
33            _ => return None,
34        };
35        if cp.projections.is_empty() {
36            return match cp.base {
37                PlaceBase::Return => vm_state.local_value(Local::from_usize(0)).cloned(),
38                PlaceBase::Arg(n) => {
39                    let operand = checkpoint.args.get(n)?;
40                    Some(vm_state.value_of_operand(operand))
41                }
42                PlaceBase::Local(n) => vm_state.local_value(Local::from_usize(n)).cloned(),
43            };
44        }
45        let base_local = match cp.base {
46            PlaceBase::Return => Local::from_usize(0),
47            PlaceBase::Arg(n) => {
48                let operand = checkpoint.args.get(n)?;
49                match operand {
50                    Operand::Copy(place) | Operand::Move(place) => place.local,
51                    _ => return None,
52                }
53            }
54            PlaceBase::Local(n) => Local::from_usize(n),
55        };
56        let mut field_path: Vec<usize> = Vec::new();
57        let mut last_field_ty: Option<Ty<'tcx>> = None;
58
59        for proj in &cp.projections {
60            match proj {
61                ContractProjection::Field { index, ty } => {
62                    field_path.push(*index);
63                    last_field_ty = *ty;
64                }
65                ContractProjection::Downcast { variant_index } => {
66                    let base_val = vm_state.field_value(base_local, &field_path)
67                        .cloned()
68                        .or_else(|| vm_state.local_value(base_local).cloned());
69                    let Some(base_val) = base_val else { return None };
70
71                    let enum_ty = last_field_ty.unwrap_or(base_val.ty);
72                    let inner_ty = match enum_ty.kind() {
73                        TyKind::Adt(adt_def, substs) => {
74                            if adt_def.is_enum() {
75                                let variant = &adt_def.variants()[rustc_abi::VariantIdx::from_usize(*variant_index)];
76                                if !variant.fields.is_empty() {
77                                    Some(variant.fields[rustc_abi::FieldIdx::from_usize(0)].ty(vm_state.tcx, substs).skip_norm_wip())
78                                } else {
79                                    None
80                                }
81                            } else {
82                                None
83                            }
84                        }
85                        _ => None,
86                    };
87                    let inner_ty = inner_ty.unwrap_or(base_val.ty);
88
89                    return Some(VmValue {
90                        term: base_val.term.clone(),
91                        ty: inner_ty,
92                        provenance: base_val.provenance.clone(),
93                        invariants: base_val.invariants,
94                    });
95                }
96                ContractProjection::IterElements => {
97                    // iter() projections: try to resolve the base field and
98                    // return the base value (iterator elements handled elsewhere).
99                    if let Some(val) = vm_state.field_value(base_local, &field_path) {
100                        return Some(val.clone());
101                    }
102                    if let Some(base_val) = vm_state.local_value(base_local) {
103                        if base_val.provenance.is_some() {
104                            return Some(VmValue {
105                                term: base_val.term.clone(),
106                                ty: base_val.ty,
107                                provenance: base_val.provenance.clone(),
108                                invariants: base_val.invariants,
109                            });
110                        }
111                    }
112                    return None;
113                }
114            }
115        }
116
117        // All projections were Field (or no projections)
118        if let Some(val) = vm_state.field_value(base_local, &field_path) {
119            return Some(val.clone());
120        }
121        // Fallback: if the field value is not set (e.g. constructor return
122        // value _0 whose Aggregate was not executed), resolve from MIR.
123        if !field_path.is_empty() && base_local == Local::from_usize(0) {
124            for bb in vm_state.body.basic_blocks.iter() {
125                for stmt in &bb.statements {
126                    match &stmt.kind {
127                        rustc_middle::mir::StatementKind::Assign(assign) => {
128                            let (ref place, ref rval) = **assign;
129                            if let rustc_middle::mir::Rvalue::Aggregate(_, operands) = rval {
130                                if place.local == base_local {
131                                    if let Some(operand) = operands.get(rustc_abi::FieldIdx::from_usize(field_path[0])) {
132                                        let val = vm_state.value_of_operand(operand);
133                                        if field_path.len() == 1 {
134                                            return Some(val);
135                                        }
136                                    }
137                                }
138                            }
139                        }
140                        _ => {}
141                    }
142                }
143            }
144        }
145        if let Some(base_val) = vm_state.local_value(base_local) {
146            if let Some(ref prov) = base_val.provenance {
147                return Some(VmValue {
148                    term: base_val.term.clone(),
149                    ty: base_val.ty,
150                    provenance: Some(prov.clone()),
151                    invariants: base_val.invariants,
152                });
153            }
154        }
155        None
156    }
157
158    pub(super) fn is_vacuously_true_for_nullable<'ctx, 'tcx>(
159        &self,
160        vm_state: &VmState<'ctx, 'tcx>,
161        checkpoint: &Checkpoint<'tcx>,
162        property: &Property<'tcx>,
163    ) -> bool {
164        let cp = match property.args().first() {
165            Some(PropertyArg::Expr(crate::verify::contract::ContractExpr::Place(cp))) => cp,
166            _ => return false,
167        };
168        let has_nullable_proj = cp.projections.iter().any(|p| {
169            matches!(p, ContractProjection::Downcast { .. } | ContractProjection::IterElements)
170        });
171        if !has_nullable_proj {
172            return false;
173        }
174        match self.target_value(vm_state, checkpoint, property) {
175            Some(val) => val.provenance.is_none(),
176            None => true,
177        }
178    }
179
180    pub(super) fn is_guard_null<'ctx, 'tcx>(
181        &self,
182        vm_state: &VmState<'ctx, 'tcx>,
183        checkpoint: &Checkpoint<'tcx>,
184        guard_key: &crate::verify::def_use::PlaceKey,
185    ) -> bool {
186        use crate::verify::def_use::PlaceBaseKey;
187        let local = match guard_key.base {
188            PlaceBaseKey::Local(n) => Local::from_usize(n),
189            PlaceBaseKey::Arg(n) => {
190                checkpoint.args.get(n)
191                    .and_then(|op| match op {
192                        Operand::Copy(place) | Operand::Move(place) => Some(place.local),
193                        _ => None,
194                    })
195                    .unwrap_or(Local::from_usize(n + 1))
196            }
197            PlaceBaseKey::Return => Local::from_usize(0),
198        };
199        let val = if guard_key.fields.is_empty() {
200            vm_state.local_value(local).cloned()
201        } else {
202            vm_state.field_value(local, &guard_key.fields).cloned()
203        };
204        match val {
205            Some(v) => {
206                if v.provenance.is_none() && !v.invariants.non_null {
207                    return true;
208                }
209                if let Some(term_zero) = v.term.simplify().as_u64() {
210                    if term_zero == 0 {
211                        return true;
212                    }
213                }
214                false
215            }
216            None => true,
217        }
218    }
219
220    pub(super) fn smt_check<'ctx>(&self, solver: &Solver<'ctx>, condition: &Bool<'ctx>) -> CheckResult {
221        solver.push();
222        solver.assert(condition);
223        let r = match solver.check() { SatResult::Unsat => CheckResult::Proved, SatResult::Sat => CheckResult::Failed, SatResult::Unknown => CheckResult::Unknown };
224        solver.pop(1);
225        r
226    }
227
228    pub(super) fn resolve_arg_term<'ctx, 'tcx>(
229        &self,
230        vm_state: &VmState<'ctx, 'tcx>,
231        checkpoint: &Checkpoint<'tcx>,
232        arg: &PropertyArg<'tcx>,
233    ) -> Option<Int<'ctx>> {
234        match arg {
235            PropertyArg::Expr(ContractExpr::Const(n)) if *n <= u64::MAX as u128 => {
236                Some(Int::from_u64(vm_state.ctx, *n as u64))
237            }
238            PropertyArg::Expr(ContractExpr::Place(cp)) => {
239                match cp.base {
240                    PlaceBase::Arg(n) => {
241                        let op = checkpoint.args.get(n)?;
242                        Some(vm_state.value_of_operand(op).term)
243                    }
244                    PlaceBase::Local(n) => {
245                        // The Local(N) refers to the callee's parameter.
246                        // Map to the callsite's corresponding Arg(N-1).
247                        let arg_idx = n.saturating_sub(1);
248                        if arg_idx < checkpoint.args.len() {
249                            let op = &checkpoint.args[arg_idx];
250                            Some(vm_state.value_of_operand(op).term)
251                        } else {
252                            vm_state.local_value(Local::from_usize(n)).map(|v| v.term.clone())
253                        }
254                    }
255                    PlaceBase::Return => None,
256                }
257            }
258            PropertyArg::Expr(expr) => self.eval_contract_expr(vm_state, Some(checkpoint), expr),
259            _ => None,
260        }
261    }
262
263    pub(super) fn access_bytes<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
264        property: &Property<'tcx>, ty_arg: usize, count_arg: usize,
265        checkpoint: &Checkpoint<'tcx>, _value: &VmValue<'ctx, 'tcx>) -> Int<'ctx>
266    {
267        let elem_size = property.args().get(ty_arg)
268            .and_then(|a| if let PropertyArg::Ty(ty) = a { Some(vm_state.size_of_ty(*ty)) } else { None })
269            .unwrap_or(0);
270        // When the contract uses a generic T (size_of returns 0), infer the
271        // concrete element type from the checkpoint's target argument's pointee.
272        let elem_size = if elem_size == 0 {
273            checkpoint.args.first()
274                .map(|op| {
275                    let arg_val = vm_state.value_of_operand(op);
276                    vm_state.pointee_elem_size(arg_val.ty)
277                })
278                .unwrap_or(0)
279        } else {
280            elem_size
281        };
282        let elem_size_term = Int::from_u64(vm_state.ctx, (elem_size as u64).max(1));
283
284        let count_term = property.args().get(count_arg)
285            .and_then(|a| self.resolve_arg_term(vm_state, checkpoint, a))
286            .unwrap_or_else(|| Int::from_u64(vm_state.ctx, 1));
287        // Simplify the multiplication for concrete count and elem_size
288        if let (Some(elem), Some(count)) = (Some(elem_size), count_term.simplify().as_u64()) {
289            return Int::from_u64(vm_state.ctx, (elem as u64).max(1) * count.max(1));
290        }
291        Int::mul(vm_state.ctx, &[&elem_size_term, &count_term])
292    }
293
294    pub(super) fn zst_guard<'ctx, 'tcx>(
295        &self,
296        vm_state: &VmState<'ctx, 'tcx>,
297        checkpoint: &Checkpoint<'tcx>,
298        property: &Property<'tcx>,
299    ) -> bool {
300        let required_ty = property.args().get(1)
301            .and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
302        self.is_zst_type(vm_state, checkpoint, required_ty)
303    }
304
305    pub(super) fn is_zst_type<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, checkpoint: &Checkpoint<'tcx>,
306        ty: Option<Ty<'tcx>>) -> bool
307    {
308        let ty = match ty {
309            Some(t) => t,
310            None => return false,
311        };
312        if self.is_concrete_zst(vm_state, ty) { return true; }
313        let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, ty);
314        if resolved != ty {
315            return self.is_concrete_zst(vm_state, resolved);
316        }
317        false
318    }
319
320    pub(super) fn is_concrete_zst<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, ty: Ty<'tcx>) -> bool {
321        match ty.kind() {
322            TyKind::Param(_) | TyKind::Alias(..) | TyKind::Error(_) => false,
323            _ => vm_state.size_of_ty(ty) == 0,
324        }
325    }
326
327    pub(super) fn is_generic_ty<'tcx>(&self, ty: Ty<'tcx>) -> bool {
328        matches!(ty.kind(), TyKind::Param(_) | TyKind::Alias(..) | TyKind::Error(_))
329    }
330
331    pub(super) fn instantiate_callsite_ty<'ctx, 'tcx>(
332        &self,
333        vm_state: &VmState<'ctx, 'tcx>,
334        checkpoint: &Checkpoint<'tcx>,
335        ty: Ty<'tcx>,
336    ) -> Ty<'tcx> {
337        let TyKind::Param(param) = ty.kind() else {
338            return ty;
339        };
340
341        let body = vm_state.body;
342        let terminator = body.basic_blocks[checkpoint.block].terminator();
343        let TerminatorKind::Call { func, .. } = &terminator.kind else {
344            return ty;
345        };
346        let Operand::Constant(func_constant) = func else {
347            return ty;
348        };
349        let TyKind::FnDef(_, args) = func_constant.const_.ty().kind() else {
350            return ty;
351        };
352        let Some(arg) = crate::compat::args_get(args, param.index as usize) else {
353            return ty;
354        };
355        match arg.kind() {
356            GenericArgKind::Type(actual_ty) => actual_ty,
357            _ => ty,
358        }
359    }
360
361    pub(super) fn instantiate_callsite_const<'ctx, 'tcx>(
362        &self,
363        vm_state: &VmState<'ctx, 'tcx>,
364        checkpoint: &Checkpoint<'tcx>,
365        index: u32,
366    ) -> Option<u128> {
367        let body = vm_state.body;
368        let terminator = body.basic_blocks[checkpoint.block].terminator();
369        let TerminatorKind::Call { func, .. } = &terminator.kind else {
370            return None;
371        };
372        let Operand::Constant(func_constant) = func else {
373            return None;
374        };
375        let TyKind::FnDef(_, args) = func_constant.const_.ty().kind() else {
376            return None;
377        };
378        let arg = crate::compat::args_get(args, index as usize)?;
379        match arg.kind() {
380            GenericArgKind::Const(actual_const) => actual_const
381                .try_to_target_usize(vm_state.tcx)
382                .map(|value| value as u128)
383                .or_else(|| crate::helpers::mir_utils::const_int_from_debug(
384                    &format!("{actual_const:?}")
385                ).map(|v| v as u128)),
386            _ => None,
387        }
388    }
389
390    pub(super) fn resolve_ty_params<'ctx, 'tcx>(
391        &self,
392        vm_state: &VmState<'ctx, 'tcx>,
393        checkpoint: &Checkpoint<'tcx>,
394        ty: Ty<'tcx>,
395    ) -> Ty<'tcx> {
396        match ty.kind() {
397            TyKind::Param(_) => self.instantiate_callsite_ty(vm_state, checkpoint, ty),
398            TyKind::Adt(adt_def, substs) => {
399                let mut changed = false;
400                let resolved_substs: Vec<_> = substs.iter().map(|arg| {
401                    match arg.kind() {
402                        GenericArgKind::Type(t) => {
403                            let resolved = self.resolve_ty_params(vm_state, checkpoint, t);
404                            if resolved != t {
405                                changed = true;
406                                GenericArg::from(resolved)
407                            } else {
408                                arg.clone()
409                            }
410                        }
411                        _ => arg.clone(),
412                    }
413                }).collect();
414                if changed {
415                    Ty::new_adt(vm_state.tcx, *adt_def, vm_state.tcx.mk_args(&resolved_substs))
416                } else {
417                    ty
418                }
419            }
420            _ => ty,
421        }
422    }
423
424    pub(super) fn eval_contract_expr<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
425        checkpoint: Option<&Checkpoint<'tcx>>,
426        expr: &ContractExpr<'tcx>) -> Option<Int<'ctx>>
427    {
428        match expr {
429            ContractExpr::Const(n) => Some(Int::from_u64(vm_state.ctx, *n as u64)),
430            ContractExpr::SizeOf(ty) => {
431                let mut size = vm_state.size_of_ty(*ty);
432                if size == 0 && matches!(ty.kind(), rustc_middle::ty::TyKind::Param(_)) {
433                    size = crate::helpers::mir_utils::size_of_generic_param(vm_state.tcx, vm_state.caller_def_id, *ty);
434                    if size == 0 {
435                        if let Some(ck) = checkpoint {
436                            if let Some(_callee) = ck.callee {
437                                if !self.is_caller_type_param(vm_state, *ty) {
438                                    let resolved = self.instantiate_callsite_ty(vm_state, ck, *ty);
439                                    if resolved != *ty {
440                                        size = vm_state.size_of_ty(resolved);
441                                    }
442                                }
443                            }
444                        }
445                    }
446                }
447                if size > 0 {
448                    Some(Int::from_u64(vm_state.ctx, size as u64))
449                } else {
450                    Some(Int::from_u64(vm_state.ctx, 0))
451                }
452            }
453            ContractExpr::AlignOf(ty) => {
454                let align = vm_state.align_of_ty(*ty) as u64;
455                if align > 0 {
456                    Some(Int::from_u64(vm_state.ctx, align.max(1)))
457                } else {
458                    Some(Int::from_u64(vm_state.ctx, 0))
459                }
460            }
461            ContractExpr::Place(cp) => self.eval_contract_place(vm_state, checkpoint, cp),
462            ContractExpr::Binary { op, lhs, rhs } => {
463                let l = self.eval_contract_expr(vm_state, checkpoint, lhs)?;
464                let r = self.eval_contract_expr(vm_state, checkpoint, rhs)?;
465                match op {
466                    NumericOp::Add => Some(Int::add(vm_state.ctx, &[&l, &r])),
467                    NumericOp::Sub => Some(Int::sub(vm_state.ctx, &[&l, &r])),
468                    NumericOp::Mul => Some(Int::mul(vm_state.ctx, &[&l, &r])),
469                    NumericOp::Div | NumericOp::Rem => {
470                        // Z3 division by zero yields unconstrained results,
471                        // leading to unsound proofs downstream. When the
472                        // divisor is zero (e.g. size_of::<T>() for generic
473                        // or ZST params), return zero so that subsequent
474                        // access_bytes computes 0 * elem_size == 0.
475                        if r.as_u64() == Some(0) {
476                            Some(Int::from_u64(vm_state.ctx, 0))
477                        } else if matches!(op, NumericOp::Div) {
478                            Some(l.div(&r))
479                        } else {
480                            let q = l.div(&r);
481                            Some(Int::sub(vm_state.ctx, &[&l, &Int::mul(vm_state.ctx, &[&q, &r])]))
482                        }
483                    }
484                    _ => None,
485                }
486            }
487            ContractExpr::Unary { op, expr: inner } => {
488                let v = self.eval_contract_expr(vm_state, checkpoint, inner)?;
489                match op {
490                    crate::verify::contract::NumericUnaryOp::Not => {
491                        Some(v._eq(&Int::from_u64(vm_state.ctx, 0))
492                            .ite(&Int::from_u64(vm_state.ctx, 1), &Int::from_u64(vm_state.ctx, 0)))
493                    }
494                    crate::verify::contract::NumericUnaryOp::Neg => {
495                        let zero = Int::from_u64(vm_state.ctx, 0);
496                        Some(Int::sub(vm_state.ctx, &[&zero, &v]))
497                    }
498                }
499            }
500            ContractExpr::Min { a, b } => {
501                let a_val = self.eval_contract_expr(vm_state, checkpoint, a)?;
502                let b_val = self.eval_contract_expr(vm_state, checkpoint, b)?;
503                Some(a_val.le(&b_val).ite(&a_val, &b_val))
504            }
505            ContractExpr::Max { a, b } => {
506                let a_val = self.eval_contract_expr(vm_state, checkpoint, a)?;
507                let b_val = self.eval_contract_expr(vm_state, checkpoint, b)?;
508                Some(a_val.ge(&b_val).ite(&a_val, &b_val))
509            }
510            ContractExpr::Len(inner) => {
511                if let Some(ck) = checkpoint {
512                    if let Some(term) = self.try_iter_len_from_fields(vm_state, ck, inner) {
513                        return Some(term);
514                    }
515                }
516                let val = self.eval_contract_expr_to_value(vm_state, checkpoint, inner)?;
517                let alloc_id = val.provenance_alloc_id()?;
518                let alloc = vm_state.alloc(alloc_id);
519                let elem_ty = alloc.element_ty?;
520                let elem_size = vm_state.size_of_ty(elem_ty).max(1) as u64;
521                if elem_size == 1 {
522                    return Some(alloc.size.clone());
523                }
524                let elem_term = Int::from_u64(vm_state.ctx, elem_size);
525                Some(alloc.size.div(&elem_term))
526            }
527            ContractExpr::ConstParam { index, name: _ } => {
528                self.instantiate_callsite_const(vm_state, checkpoint?, *index)
529                    .and_then(|v| u64::try_from(v).ok())
530                    .map(|v| Int::from_u64(vm_state.ctx, v))
531            }
532            ContractExpr::If {
533                cond,
534                then_expr,
535                else_expr,
536            } => {
537                let l = self.eval_contract_expr(vm_state, checkpoint, &cond.lhs)?;
538                let r = self.eval_contract_expr(vm_state, checkpoint, &cond.rhs)?;
539                let cond_bool = match cond.op {
540                    RelOp::Eq => l._eq(&r),
541                    RelOp::Ne => l._eq(&r).not(),
542                    RelOp::Le => l.le(&r),
543                    RelOp::Lt => l.lt(&r),
544                    RelOp::Ge => l.ge(&r),
545                    RelOp::Gt => l.gt(&r),
546                };
547                // When the condition is concretely true/false, short-circuit to
548                // the taken branch so the result is a concrete term (otherwise an
549                // `ite(true, a, b)` stays symbolic and downstream `as_u64()`
550                // checks fail, e.g. the `count == 0` fast-path in check_in_bound).
551                match cond_bool.simplify().as_bool() {
552                    Some(true) => self.eval_contract_expr(vm_state, checkpoint, then_expr),
553                    Some(false) => self.eval_contract_expr(vm_state, checkpoint, else_expr),
554                    _ => {
555                        let t = self.eval_contract_expr(vm_state, checkpoint, then_expr)?;
556                        let e = self.eval_contract_expr(vm_state, checkpoint, else_expr)?;
557                        Some(cond_bool.ite(&t, &e))
558                    }
559                }
560            }
561            _ => None,
562        }
563    }
564
565    pub(super) fn eval_contract_expr_to_value<'ctx, 'tcx>(&self,
566        vm_state: &VmState<'ctx, 'tcx>,
567        checkpoint: Option<&Checkpoint<'tcx>>,
568        expr: &ContractExpr<'tcx>) -> Option<VmValue<'ctx, 'tcx>>
569    {
570        match expr {
571            ContractExpr::Place(cp) => {
572                match cp.base {
573                    PlaceBase::Arg(n) => {
574                        checkpoint?.args.get(n).map(|op| vm_state.value_of_operand(op))
575                    }
576                    PlaceBase::Local(n) => {
577                        let ck = checkpoint?;
578                        if let Some(callee) = ck.callee {
579                            if let Some(idx) = crate::helpers::mir_utils::callee_param_index_for_local(
580                                vm_state.tcx, callee, n)
581                            {
582                                if let Some(op) = ck.args.get(idx) {
583                                    return Some(vm_state.value_of_operand(op));
584                                }
585                            }
586                        }
587                        vm_state.local_value(Local::from_usize(n)).cloned()
588                    }
589                    _ => None,
590                }
591            }
592            _ => None,
593        }
594    }
595
596    pub(super) fn eval_contract_place<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
597        checkpoint: Option<&Checkpoint<'tcx>>,
598        cp: &crate::verify::contract::ContractPlace<'tcx>) -> Option<Int<'ctx>>
599    {
600        // Collect numeric field projections.  Any non-field projection (e.g. a
601        // `Downcast` or `IterElements`) cannot be resolved to a scalar, so the
602        // place does not evaluate.
603        let mut field_path: Vec<usize> = Vec::new();
604        for proj in &cp.projections {
605            match proj {
606                ContractProjection::Field { index, .. } => field_path.push(*index),
607                _ => return None,
608            }
609        }
610
611        let base_local: Option<Local> = match cp.base {
612            PlaceBase::Return => Some(Local::from_usize(0)),
613            PlaceBase::Arg(n) => {
614                if field_path.is_empty() {
615                    return checkpoint.and_then(|ck| {
616                        let op = ck.args.get(n)?;
617                        self.eval_contract_operand(vm_state, op)
618                    });
619                }
620                // A field projection of an argument: resolve the argument
621                // operand to its underlying local so the field can be read.
622                checkpoint.and_then(|ck| ck.args.get(n)).and_then(|op| match op {
623                    Operand::Copy(p) | Operand::Move(p) => Some(p.local),
624                    _ => None,
625                })
626            }
627            PlaceBase::Local(n) => {
628                if field_path.is_empty() {
629                    if let Some(ck) = checkpoint {
630                        if let Some(callee) = ck.callee {
631                            if let Some(idx) =
632                                crate::helpers::mir_utils::callee_param_index_for_local(
633                                    vm_state.tcx, callee, n)
634                            {
635                                if let Some(op) = ck.args.get(idx) {
636                                    if let Some(v) = self.eval_contract_operand(vm_state, op) {
637                                        return Some(v);
638                                    }
639                                }
640                            }
641                        }
642                    }
643                }
644                Some(Local::from_usize(n))
645            }
646        };
647
648        let local = base_local?;
649        if field_path.is_empty() {
650            vm_state.local_value(local).map(|v| v.term.clone())
651        } else {
652            vm_state.field_value(local, &field_path).map(|v| v.term.clone())
653        }
654    }
655
656    pub(super) fn eval_contract_operand<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
657        op: &Operand<'tcx>) -> Option<Int<'ctx>>
658    {
659        match op {
660            Operand::Constant(c) => {
661                let const_text = format!("{:?}", c.const_);
662                let typing_env = rustc_middle::ty::TypingEnv::fully_monomorphized();
663                if let Ok(val) = c.const_.eval(vm_state.tcx, typing_env, rustc_span::DUMMY_SP) {
664                    if let Some(scalar) = val.try_to_scalar_int() {
665                        let v = scalar.to_bits(scalar.size()) as u64;
666                        if v == 0 && (const_text.contains("AlignOf") || const_text.contains("SizeOf") || const_text.contains("min_align_of") || const_text.contains("min_size_of")) {
667                            // Generic AlignOf/SizeOf may evaluate to 0 but
668                            // are always >= 1 for non-ZST types. Fall through
669                            // to the debug text path below.
670                        } else {
671                            return Some(Int::from_u64(vm_state.ctx, v));
672                        }
673                    }
674                }
675                crate::helpers::mir_utils::const_int_from_debug(&const_text)
676                    .map(|v| Int::from_u64(vm_state.ctx, v))
677            }
678            Operand::Copy(p) | Operand::Move(p)
679                if p.projection.is_empty()
680            => {
681                vm_state.local_value(p.local).map(|v| v.term.clone())
682            }
683            _ => None,
684        }
685    }
686
687    pub(super) fn trace_value<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
688        op: &Operand<'tcx>) -> VmValue<'ctx, 'tcx>
689    {
690        let place = match op {
691            Operand::Copy(p) | Operand::Move(p) => p,
692            _ => return vm_state.value_of_operand(op),
693        };
694        if !place.projection.is_empty() { return vm_state.value_of_operand(op); }
695        let local = place.local;
696        // If this local is a parameter (arg), use it directly
697        if local.as_usize() <= vm_state.body.arg_count {
698            return vm_state.value_of_operand(op);
699        }
700        // Trace through simple Use assignments
701        for block in vm_state.body.basic_blocks.iter() {
702            for stmt in &block.statements {
703                if let StatementKind::Assign(assign) = &stmt.kind {
704                    let (dest, rvalue) = &**assign;
705                    if dest.local == local && dest.projection.is_empty() {
706                        #[cfg(rapx_rvalue_use_with_retag)]
707                        if let Rvalue::Use(src_op, _) = rvalue {
708                            return self.trace_value(vm_state, src_op);
709                        }
710                        #[cfg(not(rapx_rvalue_use_with_retag))]
711                        if let Rvalue::Use(src_op) = rvalue {
712                            return self.trace_value(vm_state, src_op);
713                        }
714                    }
715                }
716            }
717        }
718        vm_state.value_of_operand(op)
719    }
720
721    pub(super) fn alloc_elem_is_array_of<'tcx>(&self, alloc_elem_ty: Ty<'tcx>, required_ty: Ty<'tcx>) -> bool {
722        match alloc_elem_ty.kind() {
723            TyKind::Array(inner_ty, _) => {
724                *inner_ty == required_ty
725                || matches!((inner_ty.kind(), required_ty.kind()),
726                    (TyKind::Param(_), TyKind::Param(_)))
727            },
728            _ => false,
729        }
730    }
731
732    pub(super) fn has_iter_elements<'tcx>(&self, property: &Property<'tcx>) -> bool {
733        property.for_each().is_some()
734    }
735}
rapx/verify/property_checker/util.rs

rapx/verify/property_checker/
util.rs
