rapx/verify/
contract.rs

1use rustc_hir::def_id::DefId;
2use rustc_middle::mir::BinOp as MirBinOp;
3use rustc_middle::ty::{GenericParamDefKind, Ty, TyCtxt};
4use safety_parser::syn::{
5    BinOp as SynBinOp, Expr, GenericArgument, Lit, PathArguments, Type, UnOp,
6};
7
8use super::helpers::{
9    access_ident_recursive, match_ty_with_ident, parse_expr_into_local_and_ty,
10    parse_expr_into_number,
11};
12
13#[derive(Clone, Debug)]
14pub enum PlaceBase {
15    Return,
16    Arg(usize),
17    Local(usize),
18}
19
20#[derive(Clone, Debug)]
21pub enum ContractProjection<'tcx> {
22    Field { index: usize, ty: Option<Ty<'tcx>> },
23}
24
25#[derive(Clone, Debug)]
26pub struct ContractPlace<'tcx> {
27    pub base: PlaceBase,
28    pub projections: Vec<ContractProjection<'tcx>>,
29}
30
31impl<'tcx> ContractPlace<'tcx> {
32    pub fn local(base: usize, fields: Vec<(usize, Ty<'tcx>)>) -> Self {
33        Self {
34            base: if base == 0 {
35                PlaceBase::Return
36            } else {
37                PlaceBase::Local(base)
38            },
39            projections: fields
40                .into_iter()
41                .map(|(index, ty)| ContractProjection::Field {
42                    index,
43                    ty: Some(ty),
44                })
45                .collect(),
46        }
47    }
48
49    pub fn arg(index: usize) -> Self {
50        Self {
51            base: PlaceBase::Arg(index),
52            projections: Vec::new(),
53        }
54    }
55
56    pub fn local_base(&self) -> Option<usize> {
57        match self.base {
58            PlaceBase::Return => Some(0),
59            PlaceBase::Local(local) => Some(local),
60            PlaceBase::Arg(_) => None,
61        }
62    }
63
64    pub fn field_indices(&self) -> Vec<usize> {
65        self.projections
66            .iter()
67            .map(|projection| match projection {
68                ContractProjection::Field { index, .. } => *index,
69            })
70            .collect()
71    }
72}
73
74#[derive(Clone, Copy, Debug)]
75pub enum NumericOp {
76    Add,
77    Sub,
78    Mul,
79    Div,
80    Rem,
81    BitAnd,
82    BitOr,
83    BitXor,
84}
85
86impl NumericOp {
87    fn from_syn(op: &SynBinOp) -> Option<Self> {
88        match op {
89            SynBinOp::Add(_) => Some(Self::Add),
90            SynBinOp::Sub(_) => Some(Self::Sub),
91            SynBinOp::Mul(_) => Some(Self::Mul),
92            SynBinOp::Div(_) => Some(Self::Div),
93            SynBinOp::Rem(_) => Some(Self::Rem),
94            SynBinOp::BitAnd(_) => Some(Self::BitAnd),
95            SynBinOp::BitOr(_) => Some(Self::BitOr),
96            SynBinOp::BitXor(_) => Some(Self::BitXor),
97            _ => None,
98        }
99    }
100}
101
102#[derive(Clone, Copy, Debug)]
103pub enum NumericUnaryOp {
104    Not,
105    Neg,
106}
107
108impl NumericUnaryOp {
109    fn from_syn(op: &UnOp) -> Option<Self> {
110        match op {
111            UnOp::Not(_) => Some(Self::Not),
112            UnOp::Neg(_) => Some(Self::Neg),
113            _ => None,
114        }
115    }
116}
117
118#[derive(Clone, Debug)]
119pub enum ContractExpr<'tcx> {
120    Place(ContractPlace<'tcx>),
121    Const(u128),
122    ConstParam {
123        index: u32,
124        name: String,
125    },
126    SizeOf(Ty<'tcx>),
127    AlignOf(Ty<'tcx>),
128    Len(Box<ContractExpr<'tcx>>),
129    IndexAccess {
130        slice: Box<ContractExpr<'tcx>>,
131        index: Box<ContractExpr<'tcx>>,
132    },
133    Binary {
134        op: NumericOp,
135        lhs: Box<ContractExpr<'tcx>>,
136        rhs: Box<ContractExpr<'tcx>>,
137    },
138    Unary {
139        op: NumericUnaryOp,
140        expr: Box<ContractExpr<'tcx>>,
141    },
142    Unknown,
143}
144
145impl<'tcx> ContractExpr<'tcx> {
146    pub fn new_var(base: usize) -> Self {
147        Self::Place(ContractPlace::local(base, Vec::new()))
148    }
149
150    pub fn new_value(value: usize) -> Self {
151        Self::Const(value as u128)
152    }
153
154    pub fn new_unknown() -> Self {
155        Self::Unknown
156    }
157
158    pub fn get_var_base(&self) -> Option<usize> {
159        match self {
160            Self::Place(place) => place.local_base(),
161            _ => None,
162        }
163    }
164}
165
166#[derive(Clone, Copy, Debug)]
167pub enum RelOp {
168    Eq,
169    Ne,
170    Lt,
171    Le,
172    Gt,
173    Ge,
174}
175
176impl RelOp {
177    pub fn from_mir(op: MirBinOp) -> Option<Self> {
178        match op {
179            MirBinOp::Eq => Some(Self::Eq),
180            MirBinOp::Ne => Some(Self::Ne),
181            MirBinOp::Lt => Some(Self::Lt),
182            MirBinOp::Le => Some(Self::Le),
183            MirBinOp::Gt => Some(Self::Gt),
184            MirBinOp::Ge => Some(Self::Ge),
185            _ => None,
186        }
187    }
188
189    fn from_syn(op: &SynBinOp) -> Option<Self> {
190        match op {
191            SynBinOp::Eq(_) => Some(Self::Eq),
192            SynBinOp::Ne(_) => Some(Self::Ne),
193            SynBinOp::Lt(_) => Some(Self::Lt),
194            SynBinOp::Le(_) => Some(Self::Le),
195            SynBinOp::Gt(_) => Some(Self::Gt),
196            SynBinOp::Ge(_) => Some(Self::Ge),
197            _ => None,
198        }
199    }
200
201    pub fn reversed(self) -> Self {
202        match self {
203            Self::Eq => Self::Eq,
204            Self::Ne => Self::Ne,
205            Self::Lt => Self::Gt,
206            Self::Le => Self::Ge,
207            Self::Gt => Self::Lt,
208            Self::Ge => Self::Le,
209        }
210    }
211}
212
213#[derive(Clone, Debug)]
214pub struct NumericPredicate<'tcx> {
215    pub lhs: ContractExpr<'tcx>,
216    pub op: RelOp,
217    pub rhs: ContractExpr<'tcx>,
218}
219
220impl<'tcx> NumericPredicate<'tcx> {
221    pub fn new(lhs: ContractExpr<'tcx>, op: RelOp, rhs: ContractExpr<'tcx>) -> Self {
222        Self { lhs, op, rhs }
223    }
224
225    pub fn from_mir_locals(lhs: usize, rhs: usize, op: MirBinOp) -> Option<Self> {
226        RelOp::from_mir(op)
227            .map(|rel| Self::new(ContractExpr::new_var(lhs), rel, ContractExpr::new_var(rhs)))
228    }
229}
230
231#[derive(Clone, Debug, PartialEq)]
232pub enum PropertyKind {
233    Align,
234    Size,
235    NoPadding,
236    NonNull,
237    Allocated,
238    InBound,
239    NonOverlap,
240    ValidNum,
241    ValidString,
242    ValidCStr,
243    Init,
244    Unwrap,
245    Typed,
246    Owning,
247    Alias,
248    Alive,
249    Pinned,
250    NonVolatile,
251    Opened,
252    Trait,
253    Unreachable,
254    ValidPtr,
255    ValidSlice,
256    Deref,
257    Ptr2Ref,
258    Layout,
259    ValidTransmute,
260    NonSize,
261    Nullable,
262    Unknown,
263}
264
265#[derive(Clone, Debug)]
266pub enum PropertyArg<'tcx> {
267    Place(ContractPlace<'tcx>),
268    Ty(Ty<'tcx>),
269    Expr(ContractExpr<'tcx>),
270    Predicates(Vec<NumericPredicate<'tcx>>),
271    Ident(String),
272}
273
274#[derive(Clone, Debug)]
275pub struct Property<'tcx> {
276    pub kind: PropertyKind,
277    pub args: Vec<PropertyArg<'tcx>>,
278}
279
280impl<'tcx> Property<'tcx> {
281    pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr]) -> Self {
282        match name {
283            "Align" => {
284                if !Self::check_arg_length(exprs.len(), 2, "Align") {
285                    return Self::new_simple(PropertyKind::Unknown);
286                }
287                let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
288                let Some(ty) = Self::parse_type(tcx, def_id, &exprs[1], "Align") else {
289                    return Self::new_simple(PropertyKind::Unknown);
290                };
291                Self::new_with_args(PropertyKind::Align, vec![target, PropertyArg::Ty(ty)])
292            }
293            "Size" => Self::new_with_target(PropertyKind::Size, tcx, def_id, exprs),
294            "NoPadding" => Self::new_with_target(PropertyKind::NoPadding, tcx, def_id, exprs),
295            "NonNull" => Self::new_with_target(PropertyKind::NonNull, tcx, def_id, exprs),
296            "Allocated" => match exprs {
297                [target] => Self::new_with_args(
298                    PropertyKind::Allocated,
299                    vec![Self::parse_target_arg(tcx, def_id, target)],
300                ),
301                [target_expr, ty_expr, len_expr] => {
302                    let target = Self::parse_target_arg(tcx, def_id, target_expr);
303                    let Some(ty) = Self::parse_type(tcx, def_id, ty_expr, "Allocated") else {
304                        return Self::new_simple(PropertyKind::Unknown);
305                    };
306                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "Allocated");
307                    Self::new_with_args(
308                        PropertyKind::Allocated,
309                        vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
310                    )
311                }
312                _ => {
313                    Self::check_arg_length(exprs.len(), 3, "Allocated");
314                    Self::new_simple(PropertyKind::Unknown)
315                }
316            },
317            "InBound" | "InBounded" => match exprs {
318                [expr] => {
319                    let expr = Self::parse_contract_expr(tcx, def_id, expr, "InBound");
320                    if matches!(expr, ContractExpr::IndexAccess { .. }) {
321                        Self::new_with_args(PropertyKind::InBound, vec![PropertyArg::Expr(expr)])
322                    } else {
323                        Self::new_simple(PropertyKind::Unknown)
324                    }
325                }
326                [_target, ty_expr, len_expr] => {
327                    let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
328                    let Some(ty) = Self::parse_type(tcx, def_id, ty_expr, "InBound") else {
329                        return Self::new_simple(PropertyKind::Unknown);
330                    };
331                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "InBound");
332                    Self::new_with_args(
333                        PropertyKind::InBound,
334                        vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
335                    )
336                }
337                [target, len_expr] => {
338                    let Some(ty) = Self::parse_target_type(tcx, def_id, target) else {
339                        return Self::new_simple(PropertyKind::Unknown);
340                    };
341                    let target = Self::parse_target_arg(tcx, def_id, target);
342                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "InBound");
343                    Self::new_with_args(
344                        PropertyKind::InBound,
345                        vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
346                    )
347                }
348                _ => {
349                    Self::check_arg_length(exprs.len(), 3, "InBound");
350                    Self::new_simple(PropertyKind::Unknown)
351                }
352            },
353            "NonOverlap" => match exprs {
354                [indices] => {
355                    let target = Self::parse_target_arg(tcx, def_id, indices);
356                    Self::new_with_args(PropertyKind::NonOverlap, vec![target])
357                }
358                _ => Self::new_with_targets(PropertyKind::NonOverlap, tcx, def_id, exprs),
359            },
360            "ValidNum" => {
361                let predicates = Self::parse_valid_num(tcx, def_id, exprs);
362                if predicates.is_empty() {
363                    Self::new_simple(PropertyKind::Unknown)
364                } else {
365                    Self::new_with_args(
366                        PropertyKind::ValidNum,
367                        vec![PropertyArg::Predicates(predicates)],
368                    )
369                }
370            }
371            "ValidString" => Self::new_with_target(PropertyKind::ValidString, tcx, def_id, exprs),
372            "ValidCStr" => Self::new_with_target(PropertyKind::ValidCStr, tcx, def_id, exprs),
373            "Init" => {
374                if !Self::check_arg_length(exprs.len(), 3, "Init") {
375                    return Self::new_simple(PropertyKind::Unknown);
376                }
377                let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
378                let Some(ty) = Self::parse_type(tcx, def_id, &exprs[1], "Init") else {
379                    return Self::new_simple(PropertyKind::Unknown);
380                };
381                let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "Init");
382                Self::new_with_args(
383                    PropertyKind::Init,
384                    vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
385                )
386            }
387            "Unwrap" => Self::new_with_target(PropertyKind::Unwrap, tcx, def_id, exprs),
388            "Typed" => {
389                if !Self::check_arg_length(exprs.len(), 2, "Typed") {
390                    return Self::new_simple(PropertyKind::Unknown);
391                }
392                let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
393                let Some(ty) = Self::parse_type(tcx, def_id, &exprs[1], "Typed") else {
394                    return Self::new_simple(PropertyKind::Unknown);
395                };
396                Self::new_with_args(PropertyKind::Typed, vec![target, PropertyArg::Ty(ty)])
397            }
398            "Owning" => Self::new_with_target(PropertyKind::Owning, tcx, def_id, exprs),
399            "Alias" => Self::new_with_target(PropertyKind::Alias, tcx, def_id, exprs),
400            "Alive" => Self::new_with_target(PropertyKind::Alive, tcx, def_id, exprs),
401            "Pinned" => Self::new_with_target(PropertyKind::Pinned, tcx, def_id, exprs),
402            "NonVolatile" => Self::new_with_target(PropertyKind::NonVolatile, tcx, def_id, exprs),
403            "Opened" => Self::new_with_target(PropertyKind::Opened, tcx, def_id, exprs),
404            "Trait" => Self::new_with_target(PropertyKind::Trait, tcx, def_id, exprs),
405            "Unreachable" => Self::new_with_target(PropertyKind::Unreachable, tcx, def_id, exprs),
406            "ValidPtr" => {
407                if !Self::check_arg_length(exprs.len(), 3, "ValidPtr") {
408                    return Self::new_simple(PropertyKind::Unknown);
409                }
410                let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
411                let Some(ty) = Self::parse_type(tcx, def_id, &exprs[1], "ValidPtr") else {
412                    return Self::new_simple(PropertyKind::Unknown);
413                };
414                let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "ValidPtr");
415                Self::new_with_args(
416                    PropertyKind::ValidPtr,
417                    vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
418                )
419            }
420            "ValidSlice" => match exprs {
421                [target_expr, ty_expr] => {
422                    let target = Self::parse_target_arg(tcx, def_id, target_expr);
423                    let Some(ty) = Self::parse_type(tcx, def_id, ty_expr, "ValidSlice") else {
424                        return Self::new_simple(PropertyKind::Unknown);
425                    };
426                    Self::new_with_args(PropertyKind::ValidSlice, vec![target, PropertyArg::Ty(ty)])
427                }
428                [target_expr] => {
429                    let Some(ty) = Self::parse_target_type(tcx, def_id, target_expr) else {
430                        return Self::new_simple(PropertyKind::Unknown);
431                    };
432                    let target = Self::parse_target_arg(tcx, def_id, target_expr);
433                    Self::new_with_args(PropertyKind::ValidSlice, vec![target, PropertyArg::Ty(ty)])
434                }
435                _ => {
436                    Self::check_arg_length(exprs.len(), 2, "ValidSlice");
437                    Self::new_simple(PropertyKind::Unknown)
438                }
439            },
440            "Deref" => match exprs {
441                [_target, ty_expr, len_expr] => {
442                    let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
443                    let Some(ty) = Self::parse_type(tcx, def_id, ty_expr, "Deref") else {
444                        return Self::new_simple(PropertyKind::Unknown);
445                    };
446                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "Deref");
447                    Self::new_with_args(
448                        PropertyKind::Deref,
449                        vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
450                    )
451                }
452                [target, len_expr] => {
453                    let Some(ty) = Self::parse_target_type(tcx, def_id, target) else {
454                        return Self::new_simple(PropertyKind::Unknown);
455                    };
456                    let target = Self::parse_target_arg(tcx, def_id, target);
457                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "Deref");
458                    Self::new_with_args(
459                        PropertyKind::Deref,
460                        vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
461                    )
462                }
463                _ => Self::new_with_target(PropertyKind::Deref, tcx, def_id, exprs),
464            },
465            "Ptr2Ref" | "ValidPtr2Ref" => {
466                Self::new_with_target(PropertyKind::Ptr2Ref, tcx, def_id, exprs)
467            }
468            "Layout" => Self::new_with_target(PropertyKind::Layout, tcx, def_id, exprs),
469            "ValidTransmute" => {
470                if !Self::check_arg_length(exprs.len(), 2, "ValidTransmute") {
471                    return Self::new_simple(PropertyKind::Unknown);
472                }
473                let Some(src_ty) = Self::parse_type(tcx, def_id, &exprs[0], "ValidTransmute") else {
474                    return Self::new_simple(PropertyKind::Unknown);
475                };
476                let Some(dst_ty) = Self::parse_type(tcx, def_id, &exprs[1], "ValidTransmute") else {
477                    return Self::new_simple(PropertyKind::Unknown);
478                };
479                Self::new_with_args(
480                    PropertyKind::ValidTransmute,
481                    vec![PropertyArg::Ty(src_ty), PropertyArg::Ty(dst_ty)],
482                )
483            }
484            "NonSize" => Self::new_simple(PropertyKind::NonSize),
485            "Null" => Self::new_with_target(PropertyKind::Nullable, tcx, def_id, exprs),
486            _ => Self::new_simple(PropertyKind::Unknown),
487        }
488    }
489
490    pub fn new_partial_order(lhs: usize, rhs: usize, op: MirBinOp) -> Self {
491        if let Some(predicate) = NumericPredicate::from_mir_locals(lhs, rhs, op) {
492            Self::new_with_args(
493                PropertyKind::ValidNum,
494                vec![PropertyArg::Predicates(vec![predicate])],
495            )
496        } else {
497            Self::new_simple(PropertyKind::Unknown)
498        }
499    }
500
501    pub fn new_obj_boundary(ty: Ty<'tcx>, len: ContractExpr<'tcx>) -> Self {
502        Self::new_with_args(
503            PropertyKind::InBound,
504            vec![
505                PropertyArg::Expr(ContractExpr::Unknown),
506                PropertyArg::Ty(ty),
507                PropertyArg::Expr(len),
508            ],
509        )
510    }
511
512    fn new_simple(kind: PropertyKind) -> Self {
513        Self {
514            kind,
515            args: Vec::new(),
516        }
517    }
518
519    fn new_with_args(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self {
520        Self { kind, args }
521    }
522
523    fn new_with_target(
524        kind: PropertyKind,
525        tcx: TyCtxt<'tcx>,
526        def_id: DefId,
527        exprs: &[Expr],
528    ) -> Self {
529        let args = exprs
530            .first()
531            .map(|expr| Self::parse_target_arg(tcx, def_id, expr))
532            .into_iter()
533            .collect();
534        Self { kind, args }
535    }
536
537    fn new_with_targets(
538        kind: PropertyKind,
539        tcx: TyCtxt<'tcx>,
540        def_id: DefId,
541        exprs: &[Expr],
542    ) -> Self {
543        let args = exprs
544            .iter()
545            .map(|expr| Self::parse_target_arg(tcx, def_id, expr))
546            .collect();
547        Self { kind, args }
548    }
549
550    fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool {
551        if expr_len != required_len {
552            rap_error!(
553                "Wrong args length for {:?} Tag! expected {required_len}, got {expr_len}",
554                sp
555            );
556            return false;
557        }
558        true
559    }
560
561    fn parse_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str) -> Option<Ty<'tcx>> {
562        let ty_ident_full = access_ident_recursive(expr);
563        if ty_ident_full.is_none() {
564            rap_debug!("Incorrect expression for the type of {:?} Tag!", sp);
565            return None;
566        }
567        let ty_ident = ty_ident_full.unwrap().0;
568        let ty = match_ty_with_ident(tcx, def_id, ty_ident);
569        if ty.is_none() {
570            rap_debug!("Cannot get type in {:?} Tag!", sp);
571        }
572        ty
573    }
574
575    fn parse_target_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr) -> Option<Ty<'tcx>> {
576        parse_expr_into_local_and_ty(tcx, def_id, expr).map(|(_, _, ty)| ty)
577    }
578
579    fn parse_target_arg(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr) -> PropertyArg<'tcx> {
580        Self::parse_contract_place(tcx, def_id, expr)
581            .map(PropertyArg::Place)
582            .unwrap_or_else(|| {
583                PropertyArg::Expr(Self::parse_contract_expr(tcx, def_id, expr, "target"))
584            })
585    }
586
587    fn parse_contract_expr(
588        tcx: TyCtxt<'tcx>,
589        def_id: DefId,
590        expr: &Expr,
591        sp: &str,
592    ) -> ContractExpr<'tcx> {
593        match expr {
594            Expr::Paren(paren) => Self::parse_contract_expr(tcx, def_id, &paren.expr, sp),
595            Expr::Group(group) => Self::parse_contract_expr(tcx, def_id, &group.expr, sp),
596            Expr::Lit(expr_lit) => match &expr_lit.lit {
597                Lit::Int(lit_int) => lit_int
598                    .base10_parse::<u128>()
599                    .map(ContractExpr::Const)
600                    .unwrap_or(ContractExpr::Unknown),
601                _ => ContractExpr::Unknown,
602            },
603            Expr::Call(expr_call) => {
604                if let Some(expr) = Self::parse_index_access_expr(tcx, def_id, expr_call) {
605                    return expr;
606                }
607                if let Some(expr) = Self::parse_len_expr(tcx, def_id, expr_call) {
608                    return expr;
609                }
610                if let Some(expr) = Self::parse_layout_expr(tcx, def_id, expr_call) {
611                    return expr;
612                }
613                ContractExpr::Unknown
614            }
615            // Treat `x.len` (field-access sugar) as the slice length `len(x)`.
616            Expr::Field(expr_field)
617                if matches!(&expr_field.member, safety_parser::syn::Member::Named(ident) if ident == "len") =>
618            {
619                ContractExpr::Len(Box::new(Self::parse_contract_expr(
620                    tcx,
621                    def_id,
622                    &expr_field.base,
623                    sp,
624                )))
625            }
626            Expr::Unary(expr_unary) => {
627                let Some(op) = NumericUnaryOp::from_syn(&expr_unary.op) else {
628                    return ContractExpr::Unknown;
629                };
630                ContractExpr::Unary {
631                    op,
632                    expr: Box::new(Self::parse_contract_expr(tcx, def_id, &expr_unary.expr, sp)),
633                }
634            }
635            Expr::Binary(expr_binary) => {
636                let Some(op) = NumericOp::from_syn(&expr_binary.op) else {
637                    return ContractExpr::Unknown;
638                };
639                ContractExpr::Binary {
640                    op,
641                    lhs: Box::new(Self::parse_contract_expr(
642                        tcx,
643                        def_id,
644                        &expr_binary.left,
645                        sp,
646                    )),
647                    rhs: Box::new(Self::parse_contract_expr(
648                        tcx,
649                        def_id,
650                        &expr_binary.right,
651                        sp,
652                    )),
653                }
654            }
655            _ => {
656                if let Some(place) = Self::parse_contract_place(tcx, def_id, expr) {
657                    ContractExpr::Place(place)
658                } else if let Some(expr) = Self::parse_const_param(tcx, def_id, expr) {
659                    expr
660                } else if let Some(value) = Self::parse_builtin_const(tcx, expr) {
661                    ContractExpr::Const(value)
662                } else if let Some(value) = parse_expr_into_number(expr) {
663                    ContractExpr::new_value(value)
664                } else {
665                    rap_debug!(
666                        "Numeric expression in {:?} could not be resolved: {:?}",
667                        sp,
668                        expr
669                    );
670                    ContractExpr::Unknown
671                }
672            }
673        }
674    }
675
676    fn parse_index_access_expr(
677        tcx: TyCtxt<'tcx>,
678        def_id: DefId,
679        expr_call: &safety_parser::syn::ExprCall,
680    ) -> Option<ContractExpr<'tcx>> {
681        let Expr::Path(func_path) = expr_call.func.as_ref() else {
682            return None;
683        };
684        let name = func_path.path.segments.last()?.ident.to_string();
685        if name != "index_access" || expr_call.args.len() != 2 {
686            return None;
687        }
688
689        let mut args = expr_call.args.iter();
690        let slice = args.next()?;
691        let index = args.next()?;
692        Some(ContractExpr::IndexAccess {
693            slice: Box::new(Self::parse_contract_expr(
694                tcx,
695                def_id,
696                slice,
697                "index_access",
698            )),
699            index: Box::new(Self::parse_contract_expr(
700                tcx,
701                def_id,
702                index,
703                "index_access",
704            )),
705        })
706    }
707
708    fn parse_len_expr(
709        tcx: TyCtxt<'tcx>,
710        def_id: DefId,
711        expr_call: &safety_parser::syn::ExprCall,
712    ) -> Option<ContractExpr<'tcx>> {
713        let Expr::Path(func_path) = expr_call.func.as_ref() else {
714            return None;
715        };
716        let name = func_path.path.segments.last()?.ident.to_string();
717        if name != "len" || expr_call.args.len() != 1 {
718            return None;
719        }
720        let target = expr_call.args.first()?;
721        Some(ContractExpr::Len(Box::new(Self::parse_contract_expr(
722            tcx, def_id, target, "len",
723        ))))
724    }
725
726    fn parse_layout_expr(
727        tcx: TyCtxt<'tcx>,
728        def_id: DefId,
729        expr_call: &safety_parser::syn::ExprCall,
730    ) -> Option<ContractExpr<'tcx>> {
731        let Expr::Path(func_path) = expr_call.func.as_ref() else {
732            return None;
733        };
734        let last = func_path.path.segments.last()?;
735        let name = last.ident.to_string();
736        if name != "size_of" && name != "align_of" {
737            return None;
738        }
739
740        let ty = if let Some(arg) = expr_call.args.first() {
741            Self::parse_type_opt(tcx, def_id, arg)
742        } else {
743            Self::parse_turbofish_type(tcx, def_id, &last.arguments, "ValidNum")
744        }?;
745
746        Some(match name.as_str() {
747            "size_of" => ContractExpr::SizeOf(ty),
748            "align_of" => ContractExpr::AlignOf(ty),
749            _ => return None,
750        })
751    }
752
753    fn parse_turbofish_type(
754        tcx: TyCtxt<'tcx>,
755        def_id: DefId,
756        arguments: &PathArguments,
757        sp: &str,
758    ) -> Option<Ty<'tcx>> {
759        let PathArguments::AngleBracketed(args) = arguments else {
760            return None;
761        };
762        args.args.iter().find_map(|arg| match arg {
763            GenericArgument::Type(ty) => Self::parse_syn_type(tcx, def_id, ty, sp),
764            _ => None,
765        })
766    }
767
768    fn parse_type_opt(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr) -> Option<Ty<'tcx>> {
769        if let Expr::Path(expr_path) = expr
770            && let Some(segment) = expr_path.path.segments.last()
771        {
772            return match_ty_with_ident(tcx, def_id, segment.ident.to_string());
773        }
774        let ty_ident = access_ident_recursive(expr)?.0;
775        match_ty_with_ident(tcx, def_id, ty_ident)
776    }
777
778    fn parse_syn_type(tcx: TyCtxt<'tcx>, def_id: DefId, ty: &Type, sp: &str) -> Option<Ty<'tcx>> {
779        let Type::Path(type_path) = ty else {
780            return None;
781        };
782        let ident = type_path.path.segments.last()?.ident.to_string();
783        match_ty_with_ident(tcx, def_id, ident).or_else(|| {
784            rap_debug!("Cannot get type in {:?} Tag from {:?}", sp, type_path);
785            None
786        })
787    }
788
789    fn parse_builtin_const(tcx: TyCtxt<'tcx>, expr: &Expr) -> Option<u128> {
790        let Expr::Path(expr_path) = expr else {
791            return None;
792        };
793        let mut segments = expr_path.path.segments.iter();
794        let first = segments.next()?.ident.to_string();
795        let second = segments.next()?.ident.to_string();
796        if segments.next().is_some() || second != "MAX" {
797            return None;
798        }
799
800        let pointer_bits = tcx.data_layout.pointer_size().bits();
801        match first.as_str() {
802            "isize" => Some((1_u128 << (pointer_bits - 1)) - 1),
803            "usize" => Some((1_u128 << pointer_bits) - 1),
804            _ => None,
805        }
806    }
807
808    fn parse_const_param(
809        tcx: TyCtxt<'tcx>,
810        def_id: DefId,
811        expr: &Expr,
812    ) -> Option<ContractExpr<'tcx>> {
813        let Expr::Path(expr_path) = expr else {
814            return None;
815        };
816        let ident = expr_path.path.get_ident()?.to_string();
817        let mut generics = Some(tcx.generics_of(def_id));
818        while let Some(current) = generics {
819            if let Some(param) = current.own_params.iter().find(|param| {
820                matches!(param.kind, GenericParamDefKind::Const { .. })
821                    && param.name.as_str() == ident
822            }) {
823                return Some(ContractExpr::ConstParam {
824                    index: param.index,
825                    name: ident,
826                });
827            }
828            generics = current.parent.map(|parent| tcx.generics_of(parent));
829        }
830        None
831    }
832
833    fn parse_contract_place(
834        tcx: TyCtxt<'tcx>,
835        def_id: DefId,
836        expr: &Expr,
837    ) -> Option<ContractPlace<'tcx>> {
838        if let Some((base, fields, _ty)) = parse_expr_into_local_and_ty(tcx, def_id, expr) {
839            return Some(ContractPlace::local(base, fields));
840        }
841        Self::parse_named_place(expr)
842    }
843
844    fn parse_named_place(expr: &Expr) -> Option<ContractPlace<'tcx>> {
845        if let Expr::Path(expr_path) = expr {
846            if let Some(ident) = expr_path.path.get_ident() {
847                let s = ident.to_string();
848                if let Some(num_str) = s.strip_prefix("Arg_") {
849                    if let Ok(idx) = num_str.parse::<usize>() {
850                        return Some(ContractPlace::arg(idx));
851                    }
852                }
853                if s == "return" {
854                    return Some(ContractPlace {
855                        base: PlaceBase::Return,
856                        projections: Vec::new(),
857                    });
858                }
859            }
860        }
861        None
862    }
863
864    fn parse_valid_num(
865        tcx: TyCtxt<'tcx>,
866        def_id: DefId,
867        exprs: &[Expr],
868    ) -> Vec<NumericPredicate<'tcx>> {
869        match exprs {
870            [] => Vec::new(),
871            [expr] => Self::parse_numeric_predicate(tcx, def_id, expr)
872                .into_iter()
873                .collect(),
874            [value, range, ..] => {
875                if let Some(predicates) = Self::parse_interval_predicates(tcx, def_id, value, range)
876                {
877                    predicates
878                } else {
879                    Self::parse_numeric_predicate(tcx, def_id, value)
880                        .into_iter()
881                        .collect()
882                }
883            }
884        }
885    }
886
887    fn parse_numeric_predicate(
888        tcx: TyCtxt<'tcx>,
889        def_id: DefId,
890        expr: &Expr,
891    ) -> Option<NumericPredicate<'tcx>> {
892        if let Expr::Binary(expr_binary) = expr {
893            if let Some(op) = RelOp::from_syn(&expr_binary.op) {
894                return Some(NumericPredicate::new(
895                    Self::parse_contract_expr(tcx, def_id, &expr_binary.left, "ValidNum"),
896                    op,
897                    Self::parse_contract_expr(tcx, def_id, &expr_binary.right, "ValidNum"),
898                ));
899            }
900        }
901
902        Some(NumericPredicate::new(
903            Self::parse_contract_expr(tcx, def_id, expr, "ValidNum"),
904            RelOp::Ne,
905            ContractExpr::Const(0),
906        ))
907    }
908
909    fn parse_interval_predicates(
910        tcx: TyCtxt<'tcx>,
911        def_id: DefId,
912        value: &Expr,
913        range: &Expr,
914    ) -> Option<Vec<NumericPredicate<'tcx>>> {
915        match range {
916            Expr::Array(array) if array.elems.len() == 2 => {
917                let mut elems = array.elems.iter();
918                let lower = elems.next().unwrap();
919                let upper = elems.next().unwrap();
920                Some(Self::build_interval_predicates(
921                    tcx, def_id, value, lower, true, upper, true,
922                ))
923            }
924            Expr::Lit(expr_lit) => {
925                let Lit::Str(range_lit) = &expr_lit.lit else {
926                    return None;
927                };
928                Self::parse_string_interval(tcx, def_id, value, &range_lit.value())
929            }
930            _ => None,
931        }
932    }
933
934    fn parse_string_interval(
935        tcx: TyCtxt<'tcx>,
936        def_id: DefId,
937        value: &Expr,
938        raw_range: &str,
939    ) -> Option<Vec<NumericPredicate<'tcx>>> {
940        let trimmed = raw_range.trim();
941        if trimmed.len() < 5 {
942            return None;
943        }
944
945        let lower_inclusive = trimmed.starts_with('[');
946        let upper_inclusive = trimmed.ends_with(']');
947        if !(lower_inclusive || trimmed.starts_with('('))
948            || !(upper_inclusive || trimmed.ends_with(')'))
949        {
950            return None;
951        }
952
953        let body = &trimmed[1..trimmed.len() - 1];
954        let (lower_raw, upper_raw) = body.split_once(',')?;
955        let lower = safety_parser::syn::parse_str::<Expr>(lower_raw.trim()).ok()?;
956        let upper = safety_parser::syn::parse_str::<Expr>(upper_raw.trim()).ok()?;
957
958        Some(Self::build_interval_predicates(
959            tcx,
960            def_id,
961            value,
962            &lower,
963            lower_inclusive,
964            &upper,
965            upper_inclusive,
966        ))
967    }
968
969    fn build_interval_predicates(
970        tcx: TyCtxt<'tcx>,
971        def_id: DefId,
972        value: &Expr,
973        lower: &Expr,
974        lower_inclusive: bool,
975        upper: &Expr,
976        upper_inclusive: bool,
977    ) -> Vec<NumericPredicate<'tcx>> {
978        let value_expr = Self::parse_contract_expr(tcx, def_id, value, "ValidNum");
979        let lower_expr = Self::parse_contract_expr(tcx, def_id, lower, "ValidNum");
980        let upper_expr = Self::parse_contract_expr(tcx, def_id, upper, "ValidNum");
981        vec![
982            NumericPredicate::new(
983                lower_expr,
984                if lower_inclusive {
985                    RelOp::Le
986                } else {
987                    RelOp::Lt
988                },
989                value_expr.clone(),
990            ),
991            NumericPredicate::new(
992                value_expr,
993                if upper_inclusive {
994                    RelOp::Le
995                } else {
996                    RelOp::Lt
997                },
998                upper_expr,
999            ),
1000        ]
1001    }
1002}
rapx/verify/contract.rs

rapx/verify/
contract.rs
