rapx/check/senryx/
contract.rs

1//! Contract and abstract-state data types used by the Senryx verifier.
2//!
3//! This module owns the contract representation parsed from RAPx safety
4//! annotations. Numeric obligations use a small expression AST so contracts can
5//! describe relationships such as `region.size >= 0`, `offset + len <= cap`,
6//! and future layout-sensitive formulas without inventing new ad-hoc range
7//! types for every property.
8
9use crate::analysis::utils::fn_info::{
10    access_ident_recursive, match_ty_with_ident, parse_expr_into_local_and_ty,
11    parse_expr_into_number,
12};
13use rustc_hir::def_id::DefId;
14use rustc_middle::mir::BinOp as MirBinOp;
15use rustc_middle::ty::Ty;
16use rustc_middle::ty::TyCtxt;
17use safety_parser::syn::{BinOp as SynBinOp, Expr, Lit, UnOp};
18
19/// The root of a contract expression place.
20#[derive(Clone, Debug)]
21pub enum PlaceBase {
22    /// MIR return local `_0`.
23    Return,
24    /// A function argument index in contract-spec coordinates.
25    Arg(usize),
26    /// A concrete MIR local id in the analyzed caller/body.
27    Local(usize),
28}
29
30/// A projection from a contract place root.
31#[derive(Clone, Debug)]
32pub enum ContractProjection<'tcx> {
33    /// A struct/tuple field projection with optional resolved field type.
34    Field { index: usize, ty: Option<Ty<'tcx>> },
35}
36
37/// A place expression referenced by a contract.
38#[derive(Clone, Debug)]
39pub struct ContractPlace<'tcx> {
40    pub base: PlaceBase,
41    pub projections: Vec<ContractProjection<'tcx>>,
42}
43
44impl<'tcx> ContractPlace<'tcx> {
45    /// Build a place from a concrete MIR local id and field sequence.
46    pub fn local(base: usize, fields: Vec<(usize, Ty<'tcx>)>) -> Self {
47        Self {
48            base: if base == 0 {
49                PlaceBase::Return
50            } else {
51                PlaceBase::Local(base)
52            },
53            projections: fields
54                .into_iter()
55                .map(|(index, ty)| ContractProjection::Field {
56                    index,
57                    ty: Some(ty),
58                })
59                .collect(),
60        }
61    }
62
63    /// Build a place from a contract argument reference such as `Arg_1`.
64    pub fn arg(index: usize) -> Self {
65        Self {
66            base: PlaceBase::Arg(index),
67            projections: Vec::new(),
68        }
69    }
70
71    /// Return the concrete MIR local base when this place is already resolved.
72    pub fn local_base(&self) -> Option<usize> {
73        match self.base {
74            PlaceBase::Return => Some(0),
75            PlaceBase::Local(local) => Some(local),
76            PlaceBase::Arg(_) => None,
77        }
78    }
79
80    /// Return field projection indices, dropping type metadata.
81    pub fn field_indices(&self) -> Vec<usize> {
82        self.projections
83            .iter()
84            .map(|projection| match projection {
85                ContractProjection::Field { index, .. } => *index,
86            })
87            .collect()
88    }
89}
90
91/// Arithmetic operators supported by contract expressions.
92#[derive(Clone, Copy, Debug)]
93pub enum NumericOp {
94    Add,
95    Sub,
96    Mul,
97    Div,
98    Rem,
99    BitAnd,
100    BitOr,
101    BitXor,
102}
103
104impl NumericOp {
105    /// Convert a `syn` binary operator into a numeric operator when possible.
106    fn from_syn(op: &SynBinOp) -> Option<Self> {
107        match op {
108            SynBinOp::Add(_) => Some(Self::Add),
109            SynBinOp::Sub(_) => Some(Self::Sub),
110            SynBinOp::Mul(_) => Some(Self::Mul),
111            SynBinOp::Div(_) => Some(Self::Div),
112            SynBinOp::Rem(_) => Some(Self::Rem),
113            SynBinOp::BitAnd(_) => Some(Self::BitAnd),
114            SynBinOp::BitOr(_) => Some(Self::BitOr),
115            SynBinOp::BitXor(_) => Some(Self::BitXor),
116            _ => None,
117        }
118    }
119}
120
121/// Unary operators supported by contract expressions.
122#[derive(Clone, Copy, Debug)]
123pub enum NumericUnaryOp {
124    Not,
125    Neg,
126}
127
128impl NumericUnaryOp {
129    /// Convert a `syn` unary operator into a contract expression operator.
130    fn from_syn(op: &UnOp) -> Option<Self> {
131        match op {
132            UnOp::Not(_) => Some(Self::Not),
133            UnOp::Neg(_) => Some(Self::Neg),
134            _ => None,
135        }
136    }
137}
138
139/// Numeric expression AST used by length and `ValidNum` contracts.
140#[derive(Clone, Debug)]
141pub enum ContractExpr<'tcx> {
142    /// A MIR/argument place, optionally with field projections.
143    Place(ContractPlace<'tcx>),
144    /// A literal integer value.
145    Const(u128),
146    /// `size_of::<T>()` style layout expression reserved for future parsing.
147    SizeOf(Ty<'tcx>),
148    /// `align_of::<T>()` style layout expression reserved for future parsing.
149    AlignOf(Ty<'tcx>),
150    /// A binary arithmetic expression.
151    Binary {
152        op: NumericOp,
153        lhs: Box<ContractExpr<'tcx>>,
154        rhs: Box<ContractExpr<'tcx>>,
155    },
156    /// A unary arithmetic/bitwise expression.
157    Unary {
158        op: NumericUnaryOp,
159        expr: Box<ContractExpr<'tcx>>,
160    },
161    /// An expression the parser could not currently resolve.
162    Unknown,
163}
164
165impl<'tcx> ContractExpr<'tcx> {
166    /// Build an expression from a resolved MIR local.
167    pub fn new_var(base: usize) -> Self {
168        Self::Place(ContractPlace::local(base, Vec::new()))
169    }
170
171    /// Build an expression from a literal integer.
172    pub fn new_value(value: usize) -> Self {
173        Self::Const(value as u128)
174    }
175
176    /// Build an unresolved expression placeholder.
177    pub fn new_unknown() -> Self {
178        Self::Unknown
179    }
180
181    /// Return the resolved MIR local base when this expression is a concrete place.
182    pub fn get_var_base(&self) -> Option<usize> {
183        match self {
184            Self::Place(place) => place.local_base(),
185            _ => None,
186        }
187    }
188}
189
190/// Relational operators used by numeric predicates.
191#[derive(Clone, Copy, Debug)]
192pub enum RelOp {
193    Eq,
194    Ne,
195    Lt,
196    Le,
197    Gt,
198    Ge,
199}
200
201impl RelOp {
202    /// Convert a MIR binary operator into a relational operator.
203    pub fn from_mir(op: MirBinOp) -> Option<Self> {
204        match op {
205            MirBinOp::Eq => Some(Self::Eq),
206            MirBinOp::Ne => Some(Self::Ne),
207            MirBinOp::Lt => Some(Self::Lt),
208            MirBinOp::Le => Some(Self::Le),
209            MirBinOp::Gt => Some(Self::Gt),
210            MirBinOp::Ge => Some(Self::Ge),
211            _ => None,
212        }
213    }
214
215    /// Convert a `syn` binary operator into a relational operator.
216    fn from_syn(op: &SynBinOp) -> Option<Self> {
217        match op {
218            SynBinOp::Eq(_) => Some(Self::Eq),
219            SynBinOp::Ne(_) => Some(Self::Ne),
220            SynBinOp::Lt(_) => Some(Self::Lt),
221            SynBinOp::Le(_) => Some(Self::Le),
222            SynBinOp::Gt(_) => Some(Self::Gt),
223            SynBinOp::Ge(_) => Some(Self::Ge),
224            _ => None,
225        }
226    }
227
228    /// Return the inverse relation with left/right operands swapped.
229    pub fn reversed(self) -> Self {
230        match self {
231            Self::Eq => Self::Eq,
232            Self::Ne => Self::Ne,
233            Self::Lt => Self::Gt,
234            Self::Le => Self::Ge,
235            Self::Gt => Self::Lt,
236            Self::Ge => Self::Le,
237        }
238    }
239}
240
241/// A complete numeric predicate with explicit left and right expressions.
242#[derive(Clone, Debug)]
243pub struct NumericPredicate<'tcx> {
244    pub lhs: ContractExpr<'tcx>,
245    pub op: RelOp,
246    pub rhs: ContractExpr<'tcx>,
247}
248
249impl<'tcx> NumericPredicate<'tcx> {
250    /// Create a new numeric predicate.
251    pub fn new(lhs: ContractExpr<'tcx>, op: RelOp, rhs: ContractExpr<'tcx>) -> Self {
252        Self { lhs, op, rhs }
253    }
254
255    /// Create a predicate between two resolved MIR locals from a MIR relation.
256    pub fn from_mir_locals(lhs: usize, rhs: usize, op: MirBinOp) -> Option<Self> {
257        RelOp::from_mir(op)
258            .map(|rel| Self::new(ContractExpr::new_var(lhs), rel, ContractExpr::new_var(rhs)))
259    }
260}
261
262/// A parsed safety-property contract.
263///
264/// The variants correspond to the primitive safety-property tags used by the
265/// annotation DSL and the built-in standard-library contract database.
266#[derive(Clone, Debug)]
267pub enum PropertyContract<'tcx> {
268    /// Alignment requirement for a pointer interpreted as `Ty`.
269    Align(Ty<'tcx>),
270    /// Size requirement placeholder.
271    Size(),
272    /// No-padding layout requirement placeholder.
273    NoPadding,
274    /// Non-null pointer requirement.
275    NonNull,
276    /// Allocation provenance requirement for `Ty` and `length`.
277    Allocated(Ty<'tcx>, ContractExpr<'tcx>),
278    /// Object-boundary requirement for `Ty` and `length`.
279    InBound(Ty<'tcx>, ContractExpr<'tcx>),
280    /// Non-overlapping memory range requirement placeholder.
281    NonOverlap,
282    /// Numeric relationship requirements.
283    ValidNum(Vec<NumericPredicate<'tcx>>),
284    /// UTF-8 string validity requirement placeholder.
285    ValidString,
286    /// NUL-terminated C string validity requirement placeholder.
287    ValidCStr,
288    /// Initialization requirement for `Ty` and `length`.
289    Init(Ty<'tcx>, ContractExpr<'tcx>),
290    /// `Option`/`Result` unwrap safety requirement placeholder.
291    Unwrap,
292    /// Dynamic type compatibility requirement.
293    Typed(Ty<'tcx>),
294    /// Ownership requirement placeholder.
295    Owning,
296    /// Aliasing requirement placeholder.
297    Alias,
298    /// Liveness requirement placeholder.
299    Alive,
300    /// Pinning requirement placeholder.
301    Pinned,
302    /// Non-volatile access requirement placeholder.
303    NonVolatile,
304    /// Resource-open state requirement placeholder.
305    Opened,
306    /// Trait invariant requirement placeholder.
307    Trait,
308    /// Unreachable-code contract placeholder.
309    Unreachable,
310    /// Composite valid-pointer requirement.
311    ValidPtr(Ty<'tcx>, ContractExpr<'tcx>),
312    /// Dereferenceability requirement placeholder.
313    Deref,
314    /// Pointer-to-reference conversion requirement placeholder.
315    Ptr2Ref,
316    /// Layout compatibility requirement placeholder.
317    Layout,
318    /// Unknown or currently unsupported safety-property tag.
319    Unknown,
320}
321
322impl<'tcx> PropertyContract<'tcx> {
323    /// Parse one safety-property tag from the annotation DSL.
324    pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &Vec<Expr>) -> Self {
325        match name {
326            "Align" => {
327                Self::check_arg_length(exprs.len(), 2, "Align");
328                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Align");
329                Self::Align(ty)
330            }
331            "Size" => Self::Size(),
332            "NoPadding" => Self::NoPadding,
333            "NonNull" => Self::NonNull,
334            "Allocated" => {
335                Self::check_arg_length(exprs.len(), 3, "Allocated");
336                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Allocated");
337                let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "Allocated");
338                Self::Allocated(ty, length)
339            }
340            "InBound" | "InBounded" => match exprs.as_slice() {
341                [_target, ty_expr, len_expr] => {
342                    let ty = Self::parse_type(tcx, def_id, ty_expr, "InBound");
343                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "InBound");
344                    Self::InBound(ty, length)
345                }
346                [target, len_expr] => {
347                    let Some(ty) = Self::parse_target_type(tcx, def_id, target) else {
348                        return Self::Unknown;
349                    };
350                    let length = Self::parse_contract_expr(tcx, def_id, len_expr, "InBound");
351                    Self::InBound(ty, length)
352                }
353                _ => {
354                    Self::check_arg_length(exprs.len(), 3, "InBound");
355                    Self::Unknown
356                }
357            },
358            "NonOverlap" => Self::NonOverlap,
359            "ValidNum" => {
360                let predicates = Self::parse_valid_num(tcx, def_id, exprs);
361                if predicates.is_empty() {
362                    Self::Unknown
363                } else {
364                    Self::ValidNum(predicates)
365                }
366            }
367            "ValidString" => Self::ValidString,
368            "ValidCStr" => Self::ValidCStr,
369            "Init" => {
370                Self::check_arg_length(exprs.len(), 3, "Init");
371                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Init");
372                let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "Init");
373                Self::Init(ty, length)
374            }
375            "Unwrap" => Self::Unwrap,
376            "Typed" => {
377                Self::check_arg_length(exprs.len(), 2, "Typed");
378                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Typed");
379                Self::Typed(ty)
380            }
381            "Owning" => Self::Owning,
382            "Alias" => Self::Alias,
383            "Alive" => Self::Alive,
384            "Pinned" => Self::Pinned,
385            "NonVolatile" => Self::NonVolatile,
386            "Opened" => Self::Opened,
387            "Trait" => Self::Trait,
388            "Unreachable" => Self::Unreachable,
389            "ValidPtr" => {
390                Self::check_arg_length(exprs.len(), 3, "ValidPtr");
391                let ty = Self::parse_type(tcx, def_id, &exprs[1], "ValidPtr");
392                let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "ValidPtr");
393                Self::ValidPtr(ty, length)
394            }
395            "Deref" => Self::Deref,
396            "Ptr2Ref" | "ValidPtr2Ref" => Self::Ptr2Ref,
397            "Layout" => Self::Layout,
398            _ => Self::Unknown,
399        }
400    }
401
402    /// Create a numeric partial-order contract between two MIR locals.
403    pub fn new_partial_order(lhs: usize, rhs: usize, op: MirBinOp) -> Self {
404        if let Some(predicate) = NumericPredicate::from_mir_locals(lhs, rhs, op) {
405            Self::ValidNum(vec![predicate])
406        } else {
407            Self::Unknown
408        }
409    }
410
411    /// Create the default object-boundary contract for a newly modeled object.
412    pub fn new_obj_boundary(ty: Ty<'tcx>, len: ContractExpr<'tcx>) -> Self {
413        Self::InBound(ty, len)
414    }
415
416    /// Validate the number of parsed annotation arguments.
417    fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool {
418        if expr_len != required_len {
419            panic!("Wrong args length for {:?} Tag!", sp);
420        }
421        true
422    }
423
424    /// Parse a type argument from a contract expression.
425    fn parse_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str) -> Ty<'tcx> {
426        let ty_ident_full = access_ident_recursive(expr);
427        if ty_ident_full.is_none() {
428            rap_error!("Incorrect expression for the type of {:?} Tag!", sp);
429        }
430        let ty_ident = ty_ident_full.unwrap().0;
431        let ty = match_ty_with_ident(tcx, def_id, ty_ident);
432        if ty.is_none() {
433            rap_error!("Cannot get type in {:?} Tag!", sp);
434        }
435        ty.unwrap()
436    }
437
438    /// Parse the current type of a target place used by a two-argument contract form.
439    fn parse_target_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr) -> Option<Ty<'tcx>> {
440        parse_expr_into_local_and_ty(tcx, def_id, expr).map(|(_, _, ty)| ty)
441    }
442
443    /// Parse any numeric expression used by a contract.
444    fn parse_contract_expr(
445        tcx: TyCtxt<'tcx>,
446        def_id: DefId,
447        expr: &Expr,
448        sp: &str,
449    ) -> ContractExpr<'tcx> {
450        match expr {
451            Expr::Paren(paren) => Self::parse_contract_expr(tcx, def_id, &paren.expr, sp),
452            Expr::Group(group) => Self::parse_contract_expr(tcx, def_id, &group.expr, sp),
453            Expr::Lit(expr_lit) => match &expr_lit.lit {
454                Lit::Int(lit_int) => lit_int
455                    .base10_parse::<u128>()
456                    .map(ContractExpr::Const)
457                    .unwrap_or(ContractExpr::Unknown),
458                _ => ContractExpr::Unknown,
459            },
460            Expr::Unary(expr_unary) => {
461                let Some(op) = NumericUnaryOp::from_syn(&expr_unary.op) else {
462                    return ContractExpr::Unknown;
463                };
464                ContractExpr::Unary {
465                    op,
466                    expr: Box::new(Self::parse_contract_expr(tcx, def_id, &expr_unary.expr, sp)),
467                }
468            }
469            Expr::Binary(expr_binary) => {
470                let Some(op) = NumericOp::from_syn(&expr_binary.op) else {
471                    return ContractExpr::Unknown;
472                };
473                ContractExpr::Binary {
474                    op,
475                    lhs: Box::new(Self::parse_contract_expr(
476                        tcx,
477                        def_id,
478                        &expr_binary.left,
479                        sp,
480                    )),
481                    rhs: Box::new(Self::parse_contract_expr(
482                        tcx,
483                        def_id,
484                        &expr_binary.right,
485                        sp,
486                    )),
487                }
488            }
489            _ => {
490                if let Some(place) = Self::parse_contract_place(tcx, def_id, expr) {
491                    ContractExpr::Place(place)
492                } else if let Some(value) = parse_expr_into_number(expr) {
493                    ContractExpr::new_value(value)
494                } else {
495                    rap_debug!(
496                        "Numeric expression in {:?} could not be resolved: {:?}",
497                        sp,
498                        expr
499                    );
500                    ContractExpr::Unknown
501                }
502            }
503        }
504    }
505
506    /// Parse a place expression from an annotation expression.
507    fn parse_contract_place(
508        tcx: TyCtxt<'tcx>,
509        def_id: DefId,
510        expr: &Expr,
511    ) -> Option<ContractPlace<'tcx>> {
512        if let Some((base, fields, _ty)) = parse_expr_into_local_and_ty(tcx, def_id, expr) {
513            return Some(ContractPlace::local(base, fields));
514        }
515        Self::parse_arg_place(expr)
516    }
517
518    /// Parse contract argument references such as `Arg_1`.
519    fn parse_arg_place(expr: &Expr) -> Option<ContractPlace<'tcx>> {
520        if let Expr::Path(expr_path) = expr {
521            if let Some(ident) = expr_path.path.get_ident() {
522                let s = ident.to_string();
523
524                if let Some(num_str) = s.strip_prefix("Arg_") {
525                    if let Ok(idx) = num_str.parse::<usize>() {
526                        return Some(ContractPlace::arg(idx));
527                    }
528                }
529            }
530        }
531        None
532    }
533
534    /// Parse `ValidNum` into one or more numeric predicates.
535    fn parse_valid_num(
536        tcx: TyCtxt<'tcx>,
537        def_id: DefId,
538        exprs: &Vec<Expr>,
539    ) -> Vec<NumericPredicate<'tcx>> {
540        match exprs.as_slice() {
541            [] => Vec::new(),
542            [expr] => Self::parse_numeric_predicate(tcx, def_id, expr)
543                .into_iter()
544                .collect(),
545            [value, range, ..] => {
546                if let Some(predicates) = Self::parse_interval_predicates(tcx, def_id, value, range)
547                {
548                    predicates
549                } else {
550                    Self::parse_numeric_predicate(tcx, def_id, value)
551                        .into_iter()
552                        .collect()
553                }
554            }
555        }
556    }
557
558    /// Parse a single comparison predicate, falling back to `expr != 0`.
559    fn parse_numeric_predicate(
560        tcx: TyCtxt<'tcx>,
561        def_id: DefId,
562        expr: &Expr,
563    ) -> Option<NumericPredicate<'tcx>> {
564        if let Expr::Binary(expr_binary) = expr {
565            if let Some(op) = RelOp::from_syn(&expr_binary.op) {
566                return Some(NumericPredicate::new(
567                    Self::parse_contract_expr(tcx, def_id, &expr_binary.left, "ValidNum"),
568                    op,
569                    Self::parse_contract_expr(tcx, def_id, &expr_binary.right, "ValidNum"),
570                ));
571            }
572        }
573
574        Some(NumericPredicate::new(
575            Self::parse_contract_expr(tcx, def_id, expr, "ValidNum"),
576            RelOp::Ne,
577            ContractExpr::Const(0),
578        ))
579    }
580
581    /// Parse interval-style `ValidNum(value, [lower, upper])` predicates.
582    fn parse_interval_predicates(
583        tcx: TyCtxt<'tcx>,
584        def_id: DefId,
585        value: &Expr,
586        range: &Expr,
587    ) -> Option<Vec<NumericPredicate<'tcx>>> {
588        match range {
589            Expr::Array(array) if array.elems.len() == 2 => {
590                let mut elems = array.elems.iter();
591                let lower = elems.next().unwrap();
592                let upper = elems.next().unwrap();
593                Some(Self::build_interval_predicates(
594                    tcx, def_id, value, lower, true, upper, true,
595                ))
596            }
597            Expr::Lit(expr_lit) => {
598                let Lit::Str(range_lit) = &expr_lit.lit else {
599                    return None;
600                };
601                Self::parse_string_interval(tcx, def_id, value, &range_lit.value())
602            }
603            _ => None,
604        }
605    }
606
607    /// Parse string interval notation such as `"[0,self.len)"`.
608    fn parse_string_interval(
609        tcx: TyCtxt<'tcx>,
610        def_id: DefId,
611        value: &Expr,
612        raw_range: &str,
613    ) -> Option<Vec<NumericPredicate<'tcx>>> {
614        let trimmed = raw_range.trim();
615        if trimmed.len() < 5 {
616            return None;
617        }
618
619        let lower_inclusive = trimmed.starts_with('[');
620        let upper_inclusive = trimmed.ends_with(']');
621        if !(lower_inclusive || trimmed.starts_with('('))
622            || !(upper_inclusive || trimmed.ends_with(')'))
623        {
624            return None;
625        }
626
627        let body = &trimmed[1..trimmed.len() - 1];
628        let (lower_raw, upper_raw) = body.split_once(',')?;
629        let lower = safety_parser::syn::parse_str::<Expr>(lower_raw.trim()).ok()?;
630        let upper = safety_parser::syn::parse_str::<Expr>(upper_raw.trim()).ok()?;
631
632        Some(Self::build_interval_predicates(
633            tcx,
634            def_id,
635            value,
636            &lower,
637            lower_inclusive,
638            &upper,
639            upper_inclusive,
640        ))
641    }
642
643    /// Build lower/upper bound predicates for an interval contract.
644    fn build_interval_predicates(
645        tcx: TyCtxt<'tcx>,
646        def_id: DefId,
647        value: &Expr,
648        lower: &Expr,
649        lower_inclusive: bool,
650        upper: &Expr,
651        upper_inclusive: bool,
652    ) -> Vec<NumericPredicate<'tcx>> {
653        let value_expr = Self::parse_contract_expr(tcx, def_id, value, "ValidNum");
654        let lower_expr = Self::parse_contract_expr(tcx, def_id, lower, "ValidNum");
655        let upper_expr = Self::parse_contract_expr(tcx, def_id, upper, "ValidNum");
656        vec![
657            NumericPredicate::new(
658                lower_expr,
659                if lower_inclusive {
660                    RelOp::Le
661                } else {
662                    RelOp::Lt
663                },
664                value_expr.clone(),
665            ),
666            NumericPredicate::new(
667                value_expr,
668                if upper_inclusive {
669                    RelOp::Le
670                } else {
671                    RelOp::Lt
672                },
673                upper_expr,
674            ),
675        ]
676    }
677}
678
679/// The set of contract facts known to hold for one graph node.
680#[derive(Debug, Clone)]
681pub struct ContractFactSet<'tcx> {
682    pub contracts: Vec<PropertyContract<'tcx>>,
683    pub predicates: Vec<NumericPredicate<'tcx>>,
684}
685
686impl<'tcx> ContractFactSet<'tcx> {
687    /// Create an empty contract fact set.
688    pub fn new_default() -> Self {
689        Self {
690            contracts: Vec::new(),
691            predicates: Vec::new(),
692        }
693    }
694
695    /// Add one contract assumption to the fact set.
696    pub fn add_contract(&mut self, contract: PropertyContract<'tcx>) {
697        if let PropertyContract::ValidNum(predicates) = &contract {
698            self.predicates.extend(predicates.iter().cloned());
699        }
700        self.contracts.push(contract);
701    }
702
703    /// Add one numeric predicate to the fact set.
704    pub fn add_predicate(&mut self, predicate: NumericPredicate<'tcx>) {
705        self.predicates.push(predicate.clone());
706        self.contracts
707            .push(PropertyContract::ValidNum(vec![predicate]));
708    }
709
710    /// Return the number of contract entries stored in the fact set.
711    pub fn get_contracts_length(&self) -> usize {
712        self.contracts.len()
713    }
714}
715
716/// Tracks pointer alignment status in the abstract domain.
717#[derive(Debug, Clone, PartialEq, Eq)]
718pub enum AlignState<'tcx> {
719    /// The pointer is known aligned for values of this type.
720    Aligned(Ty<'tcx>),
721    /// The pointer is known unaligned for values of this type.
722    Unaligned(Ty<'tcx>),
723    /// No usable alignment fact is available.
724    Unknown,
725}
726
727impl<'tcx> AlignState<'tcx> {
728    /// Merge two alignment states conservatively at a control-flow join.
729    pub fn merge(&self, other: &Self) -> Self {
730        if self == other {
731            return other.clone();
732        }
733        match (self, other) {
734            (AlignState::Aligned(t1), AlignState::Aligned(t2)) => {
735                if t1 == t2 {
736                    AlignState::Aligned(*t1)
737                } else {
738                    AlignState::Unknown
739                }
740            }
741            (AlignState::Unaligned(_), AlignState::Unaligned(_)) => AlignState::Unknown,
742            _ => AlignState::Unknown,
743        }
744    }
745}
rapx/check/senryx/contract.rs

rapx/check/senryx/
contract.rs
