rapx/verify/contract/
types.rs

1//! The contract IR: places, expressions, predicates, and the property model.
2//!
3//! `Property` is a DNF form (only `Atom` and `Or`; conjunction is a list), with
4//! a `PropertyKind` vocabulary of safety tags. All contract front-ends
5//! (attributes, JSON, compound-property macros, pest DSL) produce this IR.
6
7use rustc_middle::mir::Local;
8use rustc_middle::ty::{Region, Ty};
9
10/// The root of a contract place: a function's return value, an argument, or a
11/// raw MIR local.  `Return` ⇔ `Local(0)`; `Arg(n)` ⇔ `Local(n + 1)`.
12#[derive(Clone, Debug, PartialEq)]
13pub(crate) enum PlaceBase {
14    /// The function's return value.
15    Return,
16    /// The n-th parameter (0-indexed).
17    Arg(usize),
18    /// A MIR local (`0` is the return place, `1..` are the parameters).
19    Local(usize),
20}
21
22impl PlaceBase {
23    /// The MIR local this base denotes (`Return` ⇔ `Local(0)`, `Arg(n)` ⇔ `Local(n + 1)`).
24    pub(crate) fn to_local(&self) -> Local {
25        match self {
26            PlaceBase::Return => Local::from_usize(0),
27            PlaceBase::Arg(n) => Local::from_usize(*n + 1),
28            PlaceBase::Local(n) => Local::from_usize(*n),
29        }
30    }
31
32    /// Like [`to_local`](Self::to_local), but `None` for `Return`.  Callers that
33    /// need a concrete `Arg`/`Local` index (e.g. resolving a container's local)
34    /// use this instead of hand-copying the `Arg`/`Local` arm plus an `_ => None`.
35    pub(crate) fn try_to_local(&self) -> Option<Local> {
36        match self {
37            PlaceBase::Return => None,
38            PlaceBase::Arg(n) => Some(Local::from_usize(*n + 1)),
39            PlaceBase::Local(n) => Some(Local::from_usize(*n)),
40        }
41    }
42}
43
44/// A step into a place, from the base down to the value a contract talks
45/// about (written as `.field`, `.unwrap_some()`, or `.iter()` in the DSL).
46#[derive(Clone, Debug)]
47pub(crate) enum ContractProjection<'tcx> {
48    /// Select a struct/tuple field.
49    Field { index: usize, ty: Option<Ty<'tcx>> },
50    /// Unwrap the `Some` variant of an enum.
51    Downcast { variant_index: usize },
52    /// Iterate over the elements of a container.
53    ForEach,
54}
55
56/// A place a contract refers to: a [`PlaceBase`] root plus a sequence of
57/// [`ContractProjection`] steps into it (e.g. `self.next.value`, `head.iter()`).
58#[derive(Clone, Debug)]
59pub(crate) struct ContractPlace<'tcx> {
60    /// The root: return value, an argument, or a MIR local.
61    pub base: PlaceBase,
62    /// Field / `Some`-unwrap / element steps from the base down.
63    pub projections: Vec<ContractProjection<'tcx>>,
64}
65
66impl<'tcx> ContractPlace<'tcx> {
67    pub(crate) fn local(base: usize, fields: Vec<(usize, Ty<'tcx>)>) -> Self {
68        Self {
69            base: if base == 0 {
70                PlaceBase::Return
71            } else {
72                PlaceBase::Local(base)
73            },
74            projections: fields
75                .into_iter()
76                .map(|(index, ty)| ContractProjection::Field {
77                    index,
78                    ty: Some(ty),
79                })
80                .collect(),
81        }
82    }
83
84    pub(crate) fn arg(index: usize) -> Self {
85        Self {
86            base: PlaceBase::Arg(index),
87            projections: Vec::new(),
88        }
89    }
90
91    pub(crate) fn local_base(&self) -> Option<usize> {
92        match self.base {
93            PlaceBase::Return => Some(0),
94            PlaceBase::Local(local) => Some(local),
95            PlaceBase::Arg(_) => None,
96        }
97    }
98
99    /// The field indices when this place is a pure `Field` chain (no `Downcast`
100    /// / `ForEach` steps), otherwise `None`.  Shared by the exec- and
101    /// checker-side `Len` evaluators.
102    pub(crate) fn plain_field_path(&self) -> Option<Vec<usize>> {
103        let mut path = Vec::new();
104        for proj in &self.projections {
105            match proj {
106                ContractProjection::Field { index, .. } => path.push(*index),
107                _ => return None,
108            }
109        }
110        Some(path)
111    }
112}
113
114#[derive(Clone, Copy, Debug)]
115pub(crate) enum NumericBinOp {
116    Add,
117    Sub,
118    Mul,
119    Div,
120    Rem,
121    Min,
122    Max,
123    BitAnd,
124    BitOr,
125    BitXor,
126}
127
128#[derive(Clone, Copy, Debug)]
129pub(crate) enum NumericUnaryOp {
130    Not,
131    Neg,
132}
133
134#[derive(Clone, Debug)]
135pub(crate) enum ContractExpr<'tcx> {
136    Place(ContractPlace<'tcx>),
137    Const(u128),
138    ConstParam {
139        index: u32,
140        name: String,
141    },
142    SizeOf(Ty<'tcx>),
143    AlignOf(Ty<'tcx>),
144    Len(Box<ContractExpr<'tcx>>),
145    IndexAccess {
146        slice: Box<ContractExpr<'tcx>>,
147        index: Box<ContractExpr<'tcx>>,
148    },
149    Binary {
150        op: NumericBinOp,
151        lhs: Box<ContractExpr<'tcx>>,
152        rhs: Box<ContractExpr<'tcx>>,
153    },
154    Unary {
155        op: NumericUnaryOp,
156        expr: Box<ContractExpr<'tcx>>,
157    },
158    If {
159        cond: Box<NumericPredicate<'tcx>>,
160        then_expr: Box<ContractExpr<'tcx>>,
161        else_expr: Box<ContractExpr<'tcx>>,
162    },
163    Unknown,
164}
165
166impl<'tcx> ContractExpr<'tcx> {
167    pub(crate) fn new_value(value: usize) -> Self {
168        Self::Const(value as u128)
169    }
170}
171
172#[derive(Clone, Copy, Debug)]
173pub(crate) enum RelOp {
174    Eq,
175    Ne,
176    Lt,
177    Le,
178    Gt,
179    Ge,
180}
181
182#[derive(Clone, Debug)]
183pub(crate) struct NumericPredicate<'tcx> {
184    pub lhs: ContractExpr<'tcx>,
185    pub op: RelOp,
186    pub rhs: ContractExpr<'tcx>,
187}
188
189impl<'tcx> NumericPredicate<'tcx> {
190    pub(crate) fn new(lhs: ContractExpr<'tcx>, op: RelOp, rhs: ContractExpr<'tcx>) -> Self {
191        Self { lhs, op, rhs }
192    }
193}
194
195/// The vocabulary of safety predicates a contract can assert.
196///
197/// Each kind's meaning, accepted argument shapes, and assembly strategy are
198/// declared in `spec::SPECS` (the single source of truth); this enum only
199/// names the kinds.  A few kinds carry extra semantics: `Null` is the guard
200/// branch of `any(Null(p), …)` (proved when `p` is null), and `Owning` asserts
201/// `ownership(*p) = none` (psp IV.1 in primitive-sp.md).  The kinds `Unwrap`,
202/// `Pinned`, `Opened` and `Unreachable` are declared but not yet verified (the
203/// checker returns `Unknown`), and `NonVolatile` is assumed satisfied (the VM
204/// does not model volatile access).
205#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
206pub(crate) enum PropertyKind {
207    Align,
208    Size,
209    NoPadding,
210    NonNull,
211    Allocated,
212    InBound,
213    NonOverlap,
214    ValidNum,
215    ValidString,
216    ValidCStr,
217    Init,
218    Unwrap,
219    Typed,
220    Owning,
221    Alias,
222    Alive,
223    Pinned,
224    NonVolatile,
225    Opened,
226    Null,
227    Trait,
228    Unreachable,
229    ValidTransmute,
230    SplitTransmute,
231    ContainNoType,
232    NoRawPtr,
233    NoInternalMut,
234    UniInternalMut,
235    AtomicUpdate,
236    RefSend,
237    Unknown,
238}
239
240/// One argument of a predicate call — what the property is applied to.
241#[derive(Clone, Debug)]
242pub(crate) enum PropertyArg<'tcx> {
243    /// A type (e.g. `T` in `Align(ptr, T)`).
244    Ty(Ty<'tcx>),
245    /// A value expression (e.g. `buf`, `n`).
246    Expr(ContractExpr<'tcx>),
247    /// An interval of comparisons, used by `ValidNum`.
248    Predicates(Vec<NumericPredicate<'tcx>>),
249    /// A name: lifetime, allocator, trait (e.g. `Copy`), or `sized`/`unsized`.
250    Ident(String),
251    /// A resolved lifetime region (e.g. `'a` in `Alive(p, 'a)`), bound against
252    /// the item that declares the lifetime (a struct for its invariants).
253    Region(Region<'tcx>),
254}
255
256#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
257pub(crate) enum ContractKind {
258    Precond,
259    Hazard,
260    Option_,
261}
262
263/// Display metadata for a property expanded from a compound property
264/// (`pred!`-style macro).  Purely presentational: it lets reports render a
265/// macro-expanded contract as a single `name(args)` entry with its doc-derived
266/// meaning, instead of the underlying primitives it expanded into.
267#[derive(Clone, Debug)]
268pub(crate) struct ContractOrigin {
269    pub name: String,
270    pub args: Vec<String>,
271    pub meaning: Option<String>,
272}
273
274/// A safety property: a boolean formula over atomic predicates.
275///
276/// The formula is a tree of three node kinds — `Atom` (a single predicate),
277/// `And` (conjunction: all members hold), and `Or` (disjunction: at least one
278/// member holds).  `Box` breaks the recursion; the top level of a contract is
279/// simply a `Vec<Property>` (an implicit conjunction of requirements).
280#[derive(Clone, Debug)]
281pub(crate) enum Property<'tcx> {
282    Atom(AtomProperty<'tcx>),
283    And(AndProperty<'tcx>),
284    Or(OrProperty<'tcx>),
285}
286
287#[derive(Clone, Debug)]
288pub(crate) struct AtomProperty<'tcx> {
289    pub kind: PropertyKind,
290    pub args: Vec<PropertyArg<'tcx>>,
291    pub contract_kind: ContractKind,
292    /// When set, this property must hold for every element of this
293    /// container (e.g. `Owning(buckets.iter())`).  The target place
294    /// in `args` is already stripped of the `ForEach` projection
295    /// and refers to a single element slot.
296    pub for_each: Option<ContractPlace<'tcx>>,
297    /// Display metadata when this property was expanded from a compound property.
298    pub origin: Option<ContractOrigin>,
299}
300
301/// A conjunction: every [`conjuncts`](Self::conjuncts) member must hold.
302#[derive(Clone, Debug)]
303pub(crate) struct AndProperty<'tcx> {
304    pub conjuncts: Vec<Box<Property<'tcx>>>,
305    pub contract_kind: ContractKind,
306    /// Display metadata when this property was expanded from a compound property.
307    pub origin: Option<ContractOrigin>,
308}
309
310/// A disjunction: at least one [`disjuncts`](Self::disjuncts) member must hold.
311#[derive(Clone, Debug)]
312pub(crate) struct OrProperty<'tcx> {
313    pub disjuncts: Vec<Box<Property<'tcx>>>,
314    pub contract_kind: ContractKind,
315    /// Display metadata when this property was expanded from a compound property.
316    pub origin: Option<ContractOrigin>,
317}
318
319impl<'tcx> Property<'tcx> {
320    /// Build a single atomic predicate.
321    pub(crate) fn new_atom(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self {
322        Self::Atom(AtomProperty {
323            kind,
324            args,
325            contract_kind: ContractKind::Precond,
326            for_each: None,
327            origin: None,
328        })
329    }
330
331    /// Build a conjunction (`And`) of already-expanded conjuncts.
332    pub(crate) fn new_and(conjuncts: Vec<Property<'tcx>>) -> Self {
333        Self::And(AndProperty {
334            conjuncts: conjuncts.into_iter().map(Box::new).collect(),
335            contract_kind: ContractKind::Precond,
336            origin: None,
337        })
338    }
339
340    /// Build a disjunction (`Or`) of already-expanded disjuncts.
341    pub(crate) fn new_or(disjuncts: Vec<Property<'tcx>>) -> Self {
342        Self::Or(OrProperty {
343            disjuncts: disjuncts.into_iter().map(Box::new).collect(),
344            contract_kind: ContractKind::Precond,
345            origin: None,
346        })
347    }
348
349    /// Normalize a list of conjuncts into a single `Property`: a singleton is
350    /// returned as-is, otherwise the list is wrapped in an `And` node.
351    pub(crate) fn conjunction(conjuncts: Vec<Property<'tcx>>) -> Self {
352        if conjuncts.len() == 1 {
353            conjuncts.into_iter().next().unwrap()
354        } else {
355            Self::new_and(conjuncts)
356        }
357    }
358
359    /// The predicate kind of an atom (`None` for `And`/`Or`, which have no
360    /// single kind).
361    pub(crate) fn kind(&self) -> Option<PropertyKind> {
362        match self {
363            Property::Atom(a) => Some(a.kind),
364            Property::And(_) | Property::Or(_) => None,
365        }
366    }
367
368    /// The positional arguments of an atom (`And`/`Or` have none).
369    pub(crate) fn args(&self) -> &[PropertyArg<'tcx>] {
370        match self {
371            Property::Atom(a) => &a.args,
372            Property::And(_) | Property::Or(_) => &[],
373        }
374    }
375
376    /// The `ContractPlace` this atom's first argument refers to, when the
377    /// first argument is a place (or an index access over one, e.g. `slice[i]`).
378    pub(crate) fn target_place(&self) -> Option<&ContractPlace<'tcx>> {
379        match self.args().first()? {
380            PropertyArg::Expr(ContractExpr::Place(cp)) => Some(cp),
381            PropertyArg::Expr(ContractExpr::IndexAccess { slice, .. }) => match slice.as_ref() {
382                ContractExpr::Place(cp) => Some(cp),
383                _ => None,
384            },
385            _ => None,
386        }
387    }
388
389    /// The conjuncts of an `And` property (`Atom`/`Or` have none).
390    pub(crate) fn conjuncts(&self) -> &[Box<Property<'tcx>>] {
391        match self {
392            Property::And(a) => &a.conjuncts,
393            Property::Atom(_) | Property::Or(_) => &[],
394        }
395    }
396
397    /// The disjuncts of an `Or` property (`Atom`/`And` have none).
398    pub(crate) fn disjuncts(&self) -> &[Box<Property<'tcx>>] {
399        match self {
400            Property::Or(o) => &o.disjuncts,
401            Property::Atom(_) | Property::And(_) => &[],
402        }
403    }
404
405    pub(crate) fn contract_kind(&self) -> ContractKind {
406        match self {
407            Property::Atom(a) => a.contract_kind,
408            Property::And(a) => a.contract_kind,
409            Property::Or(o) => o.contract_kind,
410        }
411    }
412
413    pub(crate) fn for_each(&self) -> Option<&ContractPlace<'tcx>> {
414        match self {
415            Property::Atom(a) => a.for_each.as_ref(),
416            Property::And(_) | Property::Or(_) => None,
417        }
418    }
419
420    /// Display metadata when this property was expanded from a compound property.
421    pub(crate) fn origin(&self) -> Option<&ContractOrigin> {
422        match self {
423            Property::Atom(a) => a.origin.as_ref(),
424            Property::And(a) => a.origin.as_ref(),
425            Property::Or(o) => o.origin.as_ref(),
426        }
427    }
428
429    pub(crate) fn is_or(&self) -> bool {
430        matches!(self, Property::Or(_))
431    }
432
433    pub(crate) fn is_and(&self) -> bool {
434        matches!(self, Property::And(_))
435    }
436
437    /// Apply contract kind metadata from a JSON entry or attribute.
438    pub(crate) fn apply_kind(&mut self, kind: Option<&str>) {
439        let target = match self {
440            Property::Atom(a) => &mut a.contract_kind,
441            Property::And(a) => &mut a.contract_kind,
442            Property::Or(o) => &mut o.contract_kind,
443        };
444        match kind {
445            Some("hazard") => *target = ContractKind::Hazard,
446            Some("option") => *target = ContractKind::Option_,
447            _ => {}
448        }
449    }
450
451    /// Tag a property (atom, `And`, or `Or`) with the display name, full
452    /// call-site arguments, and meaning of the compound property it expanded from.
453    pub(crate) fn set_origin(&mut self, name: String, args: Vec<String>, meaning: Option<String>) {
454        let origin = ContractOrigin {
455            name,
456            args,
457            meaning,
458        };
459        match self {
460            Property::Atom(a) => a.origin = Some(origin),
461            Property::And(a) => a.origin = Some(origin),
462            Property::Or(o) => o.origin = Some(origin),
463        }
464    }
465
466    /// Remove the compound-origin display metadata from this property.
467    pub(crate) fn clear_origin(&mut self) {
468        match self {
469            Property::Atom(a) => a.origin = None,
470            Property::And(a) => a.origin = None,
471            Property::Or(o) => o.origin = None,
472        }
473    }
474
475    /// Attach a `for_each` container to an atom.
476    pub(crate) fn set_for_each(&mut self, place: Option<ContractPlace<'tcx>>) {
477        if let Property::Atom(a) = self {
478            a.for_each = place;
479        }
480    }
481
482    /// Override the contract kind (e.g. `Alias` → `Hazard`).
483    pub(crate) fn set_contract_kind(&mut self, k: ContractKind) {
484        match self {
485            Property::Atom(a) => a.contract_kind = k,
486            Property::And(a) => a.contract_kind = k,
487            Property::Or(o) => o.contract_kind = k,
488        }
489    }
490}
rapx/verify/contract/types.rs

rapx/verify/contract/
types.rs
