rapx/verify/contract/
builder.rs

1//! Assemble a safety tag into a [`Property`] via the declarative spec table.
2//!
3//! `Property::new` looks up `spec::SPECS`, dispatches on the tag's `BuildKind`,
4//! and resolves arguments positionally. `Property::parse_list` is the shared
5//! entry point for all front-ends, including the `any(...)` combinator.
6
7use rustc_hir::def_id::DefId;
8use rustc_middle::ty::TyCtxt;
9use syn::Expr;
10
11use crate::helpers::name::access_ident_recursive;
12
13use super::spec;
14use super::types::*;
15
16impl<'tcx> Property<'tcx> {
17    /// Parse a property from the declaration table, dispatching on the tag's
18    /// assembly strategy.
19    fn parse_from_spec(
20        tcx: TyCtxt<'tcx>,
21        def_id: DefId,
22        spec: &spec::PropertySpec,
23        exprs: &[Expr],
24    ) -> Self {
25        let mut prop = match spec.build {
26            spec::BuildKind::Uniform => Self::build_uniform(tcx, def_id, spec, exprs),
27            spec::BuildKind::Size => Self::build_size(tcx, def_id, exprs),
28            spec::BuildKind::Allocated => Self::build_allocated(tcx, def_id, exprs),
29            spec::BuildKind::InBound => Self::build_inbound(tcx, def_id, exprs),
30            spec::BuildKind::NonOverlap => Self::build_nonoverlap(tcx, def_id, exprs),
31            spec::BuildKind::ValidNum => Self::build_validnum(tcx, def_id, exprs),
32            spec::BuildKind::Pinned => Self::build_pinned(tcx, def_id, exprs),
33            spec::BuildKind::SplitTransmute => Self::build_split_transmute(tcx, def_id, exprs),
34            spec::BuildKind::Targets => Self::build_targets(spec, tcx, def_id, exprs),
35            spec::BuildKind::ContainNoType => Self::build_contain_no_type(tcx, def_id, exprs),
36            spec::BuildKind::TobeSpecified => Self::new_simple(PropertyKind::Unknown),
37        };
38        // Apply the spec-declared `ContractKind` centrally, so `Hazard` /
39        // `Option_` tags keep their kind regardless of build strategy (not just
40        // for `BuildKind::Targets`).
41        prop.set_contract_kind(spec.contract_kind);
42        prop
43    }
44
45    /// Resolve a single positional argument according to its declared role.
46    ///
47    /// Returns `None` when a `Ty` argument cannot be resolved, so the caller
48    /// degrades the whole property to `Unknown` instead of silently
49    /// substituting the `never` type (which would make `Align`/`Typed` trivially
50    /// provable).
51    fn resolve_arg(
52        tcx: TyCtxt<'tcx>,
53        def_id: DefId,
54        tag: &str,
55        arg_kind: spec::ArgKind,
56        expr: &Expr,
57    ) -> Option<PropertyArg<'tcx>> {
58        match arg_kind {
59            spec::ArgKind::Target => Some(super::resolve::parse_target_arg(tcx, def_id, expr)),
60            spec::ArgKind::Ty => {
61                super::resolve::parse_type(tcx, def_id, expr, tag).map(PropertyArg::Ty)
62            }
63            spec::ArgKind::Expr => Some(PropertyArg::Expr(super::resolve::expr_to_pest(
64                tcx, def_id, expr,
65            ))),
66            spec::ArgKind::Ident => {
67                let s = access_ident_recursive(expr).map(|(name, _)| name)?;
68                Some(PropertyArg::Ident(s))
69            }
70        }
71    }
72
73    /// Positional resolution over one of the spec's accepted forms.
74    fn build_uniform(
75        tcx: TyCtxt<'tcx>,
76        def_id: DefId,
77        spec: &spec::PropertySpec,
78        exprs: &[Expr],
79    ) -> Self {
80        let Some(form) = spec.forms.iter().find(|f| f.len() == exprs.len()) else {
81            let expected: Vec<usize> = spec.forms.iter().map(|f| f.len()).collect();
82            rap_error!(
83                "Wrong args length for {:?} Tag! expected one of {expected:?}, got {}",
84                spec.tag,
85                exprs.len()
86            );
87            return Self::new_simple(PropertyKind::Unknown);
88        };
89        let mut args: Vec<PropertyArg<'tcx>> = Vec::with_capacity(exprs.len());
90        for (expr, &arg_kind) in exprs.iter().zip(form.iter()) {
91            let Some(arg) = Self::resolve_arg(tcx, def_id, spec.tag, arg_kind, expr) else {
92                return Self::new_simple(PropertyKind::Unknown);
93            };
94            args.push(arg);
95        }
96        Self::new_atom(spec.kind, args)
97    }
98
99    pub(crate) fn new(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr]) -> Self {
100        match spec::find_spec(name) {
101            Some(spec) => Self::parse_from_spec(tcx, def_id, spec, exprs),
102            None => Self::new_simple(PropertyKind::Unknown),
103        }
104    }
105
106    // ── Special-build constructors ───────────────────────────────
107
108    fn build_size(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
109        match exprs {
110            [ty_expr, const_expr] => {
111                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "Size") else {
112                    return Self::new_simple(PropertyKind::Unknown);
113                };
114                if let Some((ident, _)) = access_ident_recursive(const_expr) {
115                    if ident == "sized" || ident == "unsized" {
116                        return Self::new_atom(
117                            PropertyKind::Size,
118                            vec![PropertyArg::Ty(ty), PropertyArg::Ident(ident)],
119                        );
120                    }
121                }
122                let c = super::resolve::expr_to_pest(tcx, def_id, const_expr);
123                Self::new_atom(
124                    PropertyKind::Size,
125                    vec![PropertyArg::Ty(ty), PropertyArg::Expr(c)],
126                )
127            }
128            _ => {
129                rap_error!(
130                    "Wrong args length for Size Tag! expected 2, got {}",
131                    exprs.len()
132                );
133                Self::new_simple(PropertyKind::Unknown)
134            }
135        }
136    }
137
138    fn build_allocated(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
139        match exprs {
140            [target] => Self::new_atom(
141                PropertyKind::Allocated,
142                vec![super::resolve::parse_target_arg(tcx, def_id, target)],
143            ),
144            [target_expr, ty_expr, len_expr] => {
145                let target = super::resolve::parse_target_arg(tcx, def_id, target_expr);
146                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "Allocated") else {
147                    return Self::new_simple(PropertyKind::Unknown);
148                };
149                let length = super::resolve::expr_to_pest(tcx, def_id, len_expr);
150                Self::new_atom(
151                    PropertyKind::Allocated,
152                    vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
153                )
154            }
155            [target_expr, ty_expr, len_expr, allocator_expr] => {
156                let target = super::resolve::parse_target_arg(tcx, def_id, target_expr);
157                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "Allocated") else {
158                    return Self::new_simple(PropertyKind::Unknown);
159                };
160                let length = super::resolve::expr_to_pest(tcx, def_id, len_expr);
161                let allocator = access_ident_recursive(allocator_expr)
162                    .map(|(name, _)| name)
163                    .unwrap_or_else(|| "global".to_string());
164                Self::new_atom(
165                    PropertyKind::Allocated,
166                    vec![
167                        target,
168                        PropertyArg::Ty(ty),
169                        PropertyArg::Expr(length),
170                        PropertyArg::Ident(allocator),
171                    ],
172                )
173            }
174            _ => {
175                rap_error!(
176                    "Wrong args length for Allocated Tag! expected 1, 3 or 4, got {}",
177                    exprs.len()
178                );
179                Self::new_simple(PropertyKind::Unknown)
180            }
181        }
182    }
183
184    fn build_inbound(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
185        match exprs {
186            [_target, ty_expr, len_expr] => {
187                let target = super::resolve::parse_target_arg(tcx, def_id, &exprs[0]);
188                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "InBound") else {
189                    return Self::new_simple(PropertyKind::Unknown);
190                };
191                let length = super::resolve::expr_to_pest(tcx, def_id, len_expr);
192                Self::new_atom(
193                    PropertyKind::InBound,
194                    vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
195                )
196            }
197            [target, index_expr] => {
198                let slice = super::resolve::expr_to_pest(tcx, def_id, target);
199                let index = super::resolve::expr_to_pest(tcx, def_id, index_expr);
200                if matches!(slice, ContractExpr::Unknown) || matches!(index, ContractExpr::Unknown)
201                {
202                    return Self::new_simple(PropertyKind::Unknown);
203                }
204                // Auto-detect array index for for_each
205                let for_each = super::place::detect_array_for_each(tcx, def_id, index_expr);
206                let mut prop = Self::new_atom(
207                    PropertyKind::InBound,
208                    vec![PropertyArg::Expr(ContractExpr::IndexAccess {
209                        slice: Box::new(slice),
210                        index: Box::new(index),
211                    })],
212                );
213                prop.set_for_each(for_each);
214                prop
215            }
216            _ => {
217                rap_error!(
218                    "Wrong args length for InBound Tag! expected 2 or 3, got {}",
219                    exprs.len()
220                );
221                Self::new_simple(PropertyKind::Unknown)
222            }
223        }
224    }
225
226    fn build_nonoverlap(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
227        match exprs {
228            [indices] => {
229                let target = super::resolve::parse_target_arg(tcx, def_id, indices);
230                Self::new_atom(PropertyKind::NonOverlap, vec![target])
231            }
232            [a, b, ty_expr, count_expr] => {
233                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "NonOverlap")
234                else {
235                    return Self::new_simple(PropertyKind::Unknown);
236                };
237                let left = super::resolve::parse_target_arg(tcx, def_id, a);
238                let right = super::resolve::parse_target_arg(tcx, def_id, b);
239                let count = super::resolve::expr_to_pest(tcx, def_id, count_expr);
240                Self::new_atom(
241                    PropertyKind::NonOverlap,
242                    vec![left, right, PropertyArg::Ty(ty), PropertyArg::Expr(count)],
243                )
244            }
245            _ => {
246                rap_error!(
247                    "Wrong args length for NonOverlap Tag! expected 1 or 4, got {}",
248                    exprs.len()
249                );
250                Self::new_simple(PropertyKind::Unknown)
251            }
252        }
253    }
254
255    fn build_validnum(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
256        let predicates = super::resolve::parse_valid_num(tcx, def_id, exprs);
257        if predicates.is_empty() {
258            Self::new_simple(PropertyKind::Unknown)
259        } else {
260            Self::new_atom(
261                PropertyKind::ValidNum,
262                vec![PropertyArg::Predicates(predicates)],
263            )
264        }
265    }
266
267    fn build_targets(
268        spec: &spec::PropertySpec,
269        tcx: TyCtxt<'tcx>,
270        def_id: DefId,
271        exprs: &[Expr],
272    ) -> Self {
273        let args = exprs
274            .iter()
275            .map(|expr| super::resolve::parse_target_arg(tcx, def_id, expr))
276            .collect();
277        Self::new_atom(spec.kind, args)
278    }
279
280    fn build_pinned(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
281        match exprs {
282            [ptr_expr, lifetime_expr] => {
283                let target = super::resolve::parse_target_arg(tcx, def_id, ptr_expr);
284                let Some((lifetime, _)) = access_ident_recursive(lifetime_expr) else {
285                    return Self::new_simple(PropertyKind::Unknown);
286                };
287                Self::new_atom(
288                    PropertyKind::Pinned,
289                    vec![target, PropertyArg::Ident(lifetime)],
290                )
291            }
292            _ => {
293                rap_error!(
294                    "Wrong args length for Pinned Tag! expected 2, got {}",
295                    exprs.len()
296                );
297                Self::new_simple(PropertyKind::Unknown)
298            }
299        }
300    }
301
302    fn build_split_transmute(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
303        if !Self::check_arg_length(exprs.len(), 2, "SplitTransmute") {
304            return Self::new_simple(PropertyKind::Unknown);
305        }
306        let src_elem = super::resolve::unwrap_array_expr(tcx, def_id, &exprs[0]);
307        let dst_elem = super::resolve::unwrap_array_expr(tcx, def_id, &exprs[1]);
308        let (Some(src_elem), Some(dst_elem)) = (src_elem, dst_elem) else {
309            return Self::new_simple(PropertyKind::Unknown);
310        };
311        Self::new_atom(
312            PropertyKind::SplitTransmute,
313            vec![PropertyArg::Ty(src_elem), PropertyArg::Ty(dst_elem)],
314        )
315    }
316
317    fn build_contain_no_type(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
318        if exprs.len() < 2 {
319            rap_error!(
320                "Wrong args length for ContainNoType Tag! expected at least 2 (ty, ident...), got {}",
321                exprs.len()
322            );
323            return Self::new_simple(PropertyKind::Unknown);
324        }
325        let Some(ty) = super::resolve::parse_type(tcx, def_id, &exprs[0], "ContainNoType") else {
326            return Self::new_simple(PropertyKind::Unknown);
327        };
328        let mut args = vec![PropertyArg::Ty(ty)];
329        for expr in &exprs[1..] {
330            let Some((name, _)) = access_ident_recursive(expr) else {
331                return Self::new_simple(PropertyKind::Unknown);
332            };
333            args.push(PropertyArg::Ident(name));
334        }
335        Self::new_atom(PropertyKind::ContainNoType, args)
336    }
337
338    fn new_simple(kind: PropertyKind) -> Self {
339        Self::new_atom(kind, Vec::new())
340    }
341
342    /// Parse one annotation entry into the properties it denotes.
343    ///
344    /// Plain entries (`Align(p, T)`, `Owning(p)`, ...) yield one property.
345    /// The `any(...)` combinator may expand to several: see [`Self::parse_any`].
346    pub(crate) fn parse_list(
347        tcx: TyCtxt<'tcx>,
348        def_id: DefId,
349        name: &str,
350        exprs: &[Expr],
351    ) -> Vec<Self> {
352        // User-defined / compound property macro expansion takes precedence, so
353        // `#[rapx::requires(MyTag(...))]` can reference DSL-defined contracts.
354        if let Some(props) = super::compound::expand_compound(tcx, def_id, name, exprs) {
355            return props;
356        }
357        let mut props = if name == "any" {
358            Self::parse_any(tcx, def_id, exprs)
359        } else {
360            vec![Self::new(tcx, def_id, name, exprs)]
361        };
362        for prop in &mut props {
363            if let Property::Atom(atom) = prop {
364                if atom.for_each.is_none() {
365                    for arg in &mut atom.args {
366                        atom.for_each = super::place::strip_for_each(arg);
367                        if atom.for_each.is_some() {
368                            break;
369                        }
370                    }
371                }
372            }
373        }
374        props
375    }
376
377    /// Parse the disjunctive combinator `any(D1, D2, ...)` written in DNF:
378    /// `any` means logical OR between disjuncts, and commas inside a
379    /// parenthesised disjunct mean logical AND:
380    ///
381    /// ```text
382    /// any(Null(p), (P1(p, ...), P2(p, ...), ...))
383    /// any(Trait(T, Copy), Trait(T, TrivialClone), ...)
384    /// ```
385    ///
386    /// A disjunct is either a single property application `P(...)` or a
387    /// parenthesised conjunction `(P1(...), ..., Pn(...))`.  Any number (≥ 2)
388    /// of disjuncts is accepted; each is expanded into its constituent
389    /// properties, producing a single `Property::Or` whose disjuncts are atoms
390    /// or `And` nodes.
391    fn parse_any(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Vec<Self> {
392        if exprs.len() < 2 {
393            rap_error!(
394                "any(...) requires at least 2 disjuncts, got {}",
395                exprs.len()
396            );
397            return vec![Self::new_simple(PropertyKind::Unknown)];
398        }
399
400        let mut disjuncts: Vec<Vec<(String, Vec<Expr>)>> = Vec::with_capacity(exprs.len());
401        for expr in exprs {
402            let Some(parts) = Self::disjunct_parts(expr) else {
403                rap_error!(
404                    "any(...) disjuncts must be property applications or (P1, P2, ...) groups"
405                );
406                return vec![Self::new_simple(PropertyKind::Unknown)];
407            };
408            disjuncts.push(parts);
409        }
410
411        let mut or_disjuncts: Vec<Self> = Vec::with_capacity(disjuncts.len());
412        for parts in disjuncts {
413            let mut conjuncts: Vec<Self> = Vec::new();
414            for (name, args) in parts {
415                conjuncts.extend(Self::parse_list(tcx, def_id, &name, &args));
416            }
417            or_disjuncts.push(Self::conjunction(conjuncts));
418        }
419        vec![Self::new_or(or_disjuncts)]
420    }
421
422    /// Split one disjunct into its conjunct calls: a `(P1, P2, ...)` tuple, a
423    /// parenthesised single property `(P)`, or a bare property application.
424    fn disjunct_parts(expr: &Expr) -> Option<Vec<(String, Vec<Expr>)>> {
425        match expr {
426            Expr::Tuple(tuple) => tuple.elems.iter().map(Self::call_parts).collect(),
427            Expr::Paren(paren) => Self::call_parts(&paren.expr).map(|parts| vec![parts]),
428            _ => Self::call_parts(expr).map(|parts| vec![parts]),
429        }
430    }
431
432    /// Split a `Name(arg, ...)` call expression into its name and arguments.
433    fn call_parts(expr: &Expr) -> Option<(String, Vec<Expr>)> {
434        let Expr::Call(call) = expr else {
435            return None;
436        };
437        let Expr::Path(path) = call.func.as_ref() else {
438            return None;
439        };
440        let name = path.path.get_ident()?.to_string();
441        Some((name, call.args.iter().cloned().collect()))
442    }
443
444    fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool {
445        if expr_len != required_len {
446            rap_error!(
447                "Wrong args length for {:?} Tag! expected {required_len}, got {expr_len}",
448                sp
449            );
450            return false;
451        }
452        true
453    }
454}
rapx/verify/contract/builder.rs

rapx/verify/contract/
builder.rs
