rapx/verify/contract/
types.rs

1use rustc_middle::ty::Ty;
2
3use crate::verify::def_use::PlaceKey;
4
5#[derive(Clone, Debug, PartialEq)]
6pub enum PlaceBase {
7    Return,
8    Arg(usize),
9    Local(usize),
10}
11
12#[derive(Clone, Debug)]
13pub enum ContractProjection<'tcx> {
14    Field { index: usize, ty: Option<Ty<'tcx>> },
15    Downcast { variant_index: usize },
16    IterElements,
17}
18
19#[derive(Clone, Debug)]
20pub struct ContractPlace<'tcx> {
21    pub base: PlaceBase,
22    pub projections: Vec<ContractProjection<'tcx>>,
23}
24
25impl<'tcx> ContractPlace<'tcx> {
26    pub fn local(base: usize, fields: Vec<(usize, Ty<'tcx>)>) -> Self {
27        Self {
28            base: if base == 0 {
29                PlaceBase::Return
30            } else {
31                PlaceBase::Local(base)
32            },
33            projections: fields
34                .into_iter()
35                .map(|(index, ty)| ContractProjection::Field {
36                    index,
37                    ty: Some(ty),
38                })
39                .collect(),
40        }
41    }
42
43    pub fn arg(index: usize) -> Self {
44        Self {
45            base: PlaceBase::Arg(index),
46            projections: Vec::new(),
47        }
48    }
49
50    pub fn local_base(&self) -> Option<usize> {
51        match self.base {
52            PlaceBase::Return => Some(0),
53            PlaceBase::Local(local) => Some(local),
54            PlaceBase::Arg(_) => None,
55        }
56    }
57}
58
59#[derive(Clone, Copy, Debug)]
60pub enum NumericOp {
61    Add,
62    Sub,
63    Mul,
64    Div,
65    Rem,
66    BitAnd,
67    BitOr,
68    BitXor,
69}
70
71#[derive(Clone, Copy, Debug)]
72pub enum NumericUnaryOp {
73    Not,
74    Neg,
75}
76
77#[derive(Clone, Debug)]
78pub enum ContractExpr<'tcx> {
79    Place(ContractPlace<'tcx>),
80    Const(u128),
81    ConstParam {
82        index: u32,
83        name: String,
84    },
85    SizeOf(Ty<'tcx>),
86    AlignOf(Ty<'tcx>),
87    Len(Box<ContractExpr<'tcx>>),
88    IndexAccess {
89        slice: Box<ContractExpr<'tcx>>,
90        index: Box<ContractExpr<'tcx>>,
91    },
92    Binary {
93        op: NumericOp,
94        lhs: Box<ContractExpr<'tcx>>,
95        rhs: Box<ContractExpr<'tcx>>,
96    },
97    Unary {
98        op: NumericUnaryOp,
99        expr: Box<ContractExpr<'tcx>>,
100    },
101    Min {
102        a: Box<ContractExpr<'tcx>>,
103        b: Box<ContractExpr<'tcx>>,
104    },
105    Max {
106        a: Box<ContractExpr<'tcx>>,
107        b: Box<ContractExpr<'tcx>>,
108    },
109    If {
110        cond: Box<NumericPredicate<'tcx>>,
111        then_expr: Box<ContractExpr<'tcx>>,
112        else_expr: Box<ContractExpr<'tcx>>,
113    },
114    Unknown,
115}
116
117impl<'tcx> ContractExpr<'tcx> {
118    pub fn new_value(value: usize) -> Self {
119        Self::Const(value as u128)
120    }
121}
122
123#[derive(Clone, Copy, Debug)]
124pub enum RelOp {
125    Eq,
126    Ne,
127    Lt,
128    Le,
129    Gt,
130    Ge,
131}
132
133#[derive(Clone, Debug)]
134pub struct NumericPredicate<'tcx> {
135    pub lhs: ContractExpr<'tcx>,
136    pub op: RelOp,
137    pub rhs: ContractExpr<'tcx>,
138}
139
140impl<'tcx> NumericPredicate<'tcx> {
141    pub fn new(lhs: ContractExpr<'tcx>, op: RelOp, rhs: ContractExpr<'tcx>) -> Self {
142        Self { lhs, op, rhs }
143    }
144}
145
146#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
147pub enum PropertyKind {
148    Align,
149    Size,
150    NoPadding,
151    NonNull,
152    Allocated,
153    InBound,
154    NonOverlap,
155    ValidNum,
156    ValidString,
157    ValidCStr,
158    Init,
159    Unwrap,
160    Typed,
161    /// `ownership(*p) = none` — no live owner aliases the pointee, so the
162    /// callee may (re)claim ownership (psp IV.1 in primitive-sp.md).
163    Owning,
164    Alias,
165    Alive,
166    Pinned,
167    NonVolatile,
168    Opened,
169    Trait,
170    Unreachable,
171    ValidTransmute,
172    SplitTransmute,
173    Unknown,
174}
175
176#[derive(Clone, Debug)]
177pub enum PropertyArg<'tcx> {
178    Ty(Ty<'tcx>),
179    Expr(ContractExpr<'tcx>),
180    Predicates(Vec<NumericPredicate<'tcx>>),
181    Ident(String),
182}
183
184#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
185pub enum ContractKind {
186    Precond,
187    Hazard,
188    Option_,
189}
190
191/// A safety property: either a single predicate (`Leaf`) or a disjunction of
192/// alternative predicate groups (`Or`).
193///
194/// Conjunction (`And`) is deliberately *not* a variant: it is expressed by the
195/// surrounding collection — the caller's `requires` list is already a
196/// conjunction, and each `Or` group is a conjunction of its members (DNF).
197///
198/// Splitting `Leaf` from `Or` makes the mutually-exclusive payloads (`args`
199/// vs. `groups`) explicit in the type, so a leaf can never carry alternatives
200/// and an `Or` can never carry arguments.
201#[derive(Clone, Debug)]
202pub enum Property<'tcx> {
203    Leaf(LeafProperty<'tcx>),
204    Or(OrProperty<'tcx>),
205}
206
207#[derive(Clone, Debug)]
208pub struct LeafProperty<'tcx> {
209    pub kind: PropertyKind,
210    pub args: Vec<PropertyArg<'tcx>>,
211    pub contract_kind: ContractKind,
212    /// When set, this property came from an `any(Null(guard), ...)` expansion
213    /// and is vacuously true when `guard` is null.
214    pub null_guard: Option<PlaceKey>,
215    /// When set, this property must hold for every element of this
216    /// container (e.g. `Owning(buckets.iter())`).  The target place
217    /// in `args` is already stripped of the `IterElements` projection
218    /// and refers to a single element slot.
219    pub for_each: Option<ContractPlace<'tcx>>,
220    /// When set, the display name of the compound `def` this property expanded
221    /// from (e.g. `"Deref"`, `"ValidPtr"`), used for user-facing reports so a
222    /// macro-expanded contract keeps its original name.
223    pub origin_name: Option<String>,
224    /// The full call-site arguments of the compound `def` (rendered as source
225    /// text), used to display `name(args)` as a single entry.
226    pub origin_args: Option<Vec<String>>,
227    /// The human-readable meaning of the compound `def`, sourced from its `///`
228    /// doc comment.
229    pub origin_meaning: Option<String>,
230}
231
232#[derive(Clone, Debug)]
233pub struct OrProperty<'tcx> {
234    /// Alternative property groups.  Each inner `Vec` is a conjunction (all
235    /// must hold); at least one group must hold in a disjunction.
236    pub groups: Vec<Vec<Box<Property<'tcx>>>>,
237    pub contract_kind: ContractKind,
238    /// Display name of the compound `def` this property expanded from.
239    pub origin_name: Option<String>,
240    /// The full call-site arguments of the compound `def` (rendered source).
241    pub origin_args: Option<Vec<String>>,
242    /// The human-readable meaning of the compound `def`.
243    pub origin_meaning: Option<String>,
244}
245
246impl<'tcx> Property<'tcx> {
247    /// Build a single predicate leaf.
248    pub(crate) fn new_leaf(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self {
249        Self::Leaf(LeafProperty {
250            kind,
251            args,
252            contract_kind: ContractKind::Precond,
253            null_guard: None,
254            for_each: None,
255            origin_name: None,
256            origin_args: None,
257            origin_meaning: None,
258        })
259    }
260
261    /// Build a `Property::Or` disjunction from already-expanded DNF groups.
262    ///
263    /// Each inner `Vec` is one AND-group (all its members must hold); at least
264    /// one group must hold for the disjunction to be satisfied.  This is the
265    /// single place an `Or` property is constructed so that callers in the
266    /// `def`, JSON (`query`), and `any(...)` (`parser`) layers share identical
267    /// semantics.
268    pub(crate) fn new_or(groups: Vec<Vec<Box<Property<'tcx>>>>) -> Self {
269        Self::Or(OrProperty {
270            groups,
271            contract_kind: ContractKind::Precond,
272            origin_name: None,
273            origin_args: None,
274            origin_meaning: None,
275        })
276    }
277
278    /// The predicate kind of a leaf property (`None` for an `Or`, which has no
279    /// single kind).
280    pub fn kind(&self) -> Option<PropertyKind> {
281        match self {
282            Property::Leaf(l) => Some(l.kind),
283            Property::Or(_) => None,
284        }
285    }
286
287    /// The positional arguments of a leaf property (`Or` has none).
288    pub fn args(&self) -> &[PropertyArg<'tcx>] {
289        match self {
290            Property::Leaf(l) => &l.args,
291            Property::Or(_) => &[],
292        }
293    }
294
295    /// The alternative groups of an `Or` property (`Leaf` has none).
296    pub fn groups(&self) -> &[Vec<Box<Property<'tcx>>>] {
297        match self {
298            Property::Leaf(_) => &[],
299            Property::Or(o) => &o.groups,
300        }
301    }
302
303    pub fn contract_kind(&self) -> ContractKind {
304        match self {
305            Property::Leaf(l) => l.contract_kind,
306            Property::Or(o) => o.contract_kind,
307        }
308    }
309
310    pub fn null_guard(&self) -> Option<&PlaceKey> {
311        match self {
312            Property::Leaf(l) => l.null_guard.as_ref(),
313            Property::Or(_) => None,
314        }
315    }
316
317    pub fn for_each(&self) -> Option<&ContractPlace<'tcx>> {
318        match self {
319            Property::Leaf(l) => l.for_each.as_ref(),
320            Property::Or(_) => None,
321        }
322    }
323
324    pub fn origin_name(&self) -> Option<&str> {
325        match self {
326            Property::Leaf(l) => l.origin_name.as_deref(),
327            Property::Or(o) => o.origin_name.as_deref(),
328        }
329    }
330
331    /// The full call-site arguments of the compound `def` this property
332    /// expanded from (`None` for plain primitives).
333    pub fn origin_args(&self) -> Option<&[String]> {
334        match self {
335            Property::Leaf(l) => l.origin_args.as_deref(),
336            Property::Or(o) => o.origin_args.as_deref(),
337        }
338    }
339
340    /// The human-readable meaning of the compound `def`.
341    pub fn origin_meaning(&self) -> Option<&str> {
342        match self {
343            Property::Leaf(l) => l.origin_meaning.as_deref(),
344            Property::Or(o) => o.origin_meaning.as_deref(),
345        }
346    }
347
348    pub fn is_or(&self) -> bool {
349        matches!(self, Property::Or(_))
350    }
351
352    /// The first `Ty` argument.
353    pub fn ty_arg(&self) -> Option<Ty<'tcx>> {
354        self.args().iter().find_map(|a| match a {
355            PropertyArg::Ty(ty) => Some(*ty),
356            _ => None,
357        })
358    }
359
360    /// The first `Expr` argument, typically a count/length expression.
361    pub fn count_expr(&self) -> Option<&ContractExpr<'tcx>> {
362        self.args().iter().find_map(|a| match a {
363            PropertyArg::Expr(e) => Some(e),
364            _ => None,
365        })
366    }
367
368    /// Apply contract kind metadata from a JSON entry or attribute.
369    pub fn apply_kind(&mut self, kind: Option<&str>) {
370        let target = match self {
371            Property::Leaf(l) => &mut l.contract_kind,
372            Property::Or(o) => &mut o.contract_kind,
373        };
374        match kind {
375            Some("hazard") => *target = ContractKind::Hazard,
376            Some("option") => *target = ContractKind::Option_,
377            _ => {}
378        }
379    }
380
381    /// Tag a property (leaf or `Or`) with the display name, full call-site
382    /// arguments, and meaning of the compound `def` it expanded from.
383    pub(crate) fn set_origin(&mut self, name: String, args: Vec<String>, meaning: Option<String>) {
384        match self {
385            Property::Leaf(l) => {
386                l.origin_name = Some(name);
387                l.origin_args = Some(args);
388                l.origin_meaning = meaning;
389            }
390            Property::Or(o) => {
391                o.origin_name = Some(name);
392                o.origin_args = Some(args);
393                o.origin_meaning = meaning;
394            }
395        }
396    }
397
398    /// Attach a `for_each` container to a leaf property.
399    pub(crate) fn set_for_each(&mut self, place: Option<ContractPlace<'tcx>>) {
400        if let Property::Leaf(l) = self {
401            l.for_each = place;
402        }
403    }
404
405    /// Override the contract kind (e.g. `Alias` → `Hazard`).
406    pub(crate) fn set_contract_kind(&mut self, k: ContractKind) {
407        match self {
408            Property::Leaf(l) => l.contract_kind = k,
409            Property::Or(o) => o.contract_kind = k,
410        }
411    }
412}
rapx/verify/contract/types.rs

rapx/verify/contract/
types.rs
