rapx/verify/contract/
builder.rs

1use rustc_hir::def_id::DefId;
2use rustc_middle::ty::TyCtxt;
3use quote::ToTokens;
4use safety_parser::syn::Expr;
5
6use crate::helpers::name::access_ident_recursive;
7
8use super::types::*;
9use super::spec;
10
11impl<'tcx> Property<'tcx> {
12    /// Parse a property from the declaration table, dispatching on the tag's
13    /// assembly strategy.
14    fn parse_from_spec(
15        tcx: TyCtxt<'tcx>,
16        def_id: DefId,
17        spec: &spec::PropertySpec,
18        exprs: &[Expr],
19    ) -> Self {
20        match spec.build {
21            spec::BuildKind::Uniform => Self::build_uniform(tcx, def_id, spec, exprs),
22            spec::BuildKind::Size => Self::build_size(tcx, def_id, exprs),
23            spec::BuildKind::Allocated => Self::build_allocated(tcx, def_id, exprs),
24            spec::BuildKind::InBound => Self::build_inbound(tcx, def_id, exprs),
25            spec::BuildKind::NonOverlap => Self::build_nonoverlap(tcx, def_id, exprs),
26            spec::BuildKind::ValidNum => Self::build_validnum(tcx, def_id, exprs),
27            spec::BuildKind::Pinned => Self::build_pinned(tcx, def_id, exprs),
28            spec::BuildKind::SplitTransmute => Self::build_split_transmute(tcx, def_id, exprs),
29            spec::BuildKind::Targets => Self::build_targets(spec, tcx, def_id, exprs),
30            spec::BuildKind::TobeSpecified => Self::new_simple(PropertyKind::Unknown),
31        }
32    }
33
34    /// Resolve a single positional argument according to its declared role.
35    fn resolve_arg(
36        tcx: TyCtxt<'tcx>,
37        def_id: DefId,
38        tag: &str,
39        arg_kind: spec::ArgKind,
40        expr: &Expr,
41    ) -> PropertyArg<'tcx> {
42        match arg_kind {
43            spec::ArgKind::Target => super::resolve::parse_target_arg(tcx, def_id, expr),
44            spec::ArgKind::Ty => {
45                let ty = super::resolve::parse_type(tcx, def_id, expr, tag)
46                    .unwrap_or_else(|| tcx.types.never);
47                PropertyArg::Ty(ty)
48            }
49            spec::ArgKind::Expr => {
50                let text = expr.to_token_stream().to_string();
51                PropertyArg::Expr(super::pest_conv::parse_expr_pest(tcx, def_id, &text))
52            }
53            spec::ArgKind::Ident => {
54                let s = access_ident_recursive(expr)
55                    .map(|(name, _)| name)
56                    .unwrap_or_default();
57                PropertyArg::Ident(s)
58            }
59        }
60    }
61
62    /// Positional resolution over one of the spec's accepted forms.
63    fn build_uniform(
64        tcx: TyCtxt<'tcx>,
65        def_id: DefId,
66        spec: &spec::PropertySpec,
67        exprs: &[Expr],
68    ) -> Self {
69        let Some(form) = spec.forms.iter().find(|f| f.len() == exprs.len()) else {
70            let expected: Vec<usize> = spec.forms.iter().map(|f| f.len()).collect();
71            rap_error!(
72                "Wrong args length for {:?} Tag! expected one of {expected:?}, got {}",
73                spec.tag,
74                exprs.len()
75            );
76            return Self::new_simple(PropertyKind::Unknown);
77        };
78        let args: Vec<PropertyArg<'tcx>> = exprs
79            .iter()
80            .zip(form.iter())
81            .map(|(expr, &arg_kind)| Self::resolve_arg(tcx, def_id, spec.tag, arg_kind, expr))
82            .collect();
83        Self::new_leaf(spec.kind, args)
84    }
85
86    pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr]) -> Self {
87        match spec::find_spec(name) {
88            Some(spec) => Self::parse_from_spec(tcx, def_id, spec, exprs),
89            None => Self::new_simple(PropertyKind::Unknown),
90        }
91    }
92
93    // ── Special-build constructors ───────────────────────────────
94
95    fn build_size(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
96        match exprs {
97            [ty_expr, const_expr] => {
98                let mut args = Vec::new();
99                if let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "Size") {
100                    args.push(PropertyArg::Ty(ty));
101                }
102                if let Some((ident, _)) = access_ident_recursive(const_expr) {
103                    if ident == "sized" || ident == "unsized" {
104                        args.push(PropertyArg::Ident(ident));
105                        return Self::new_with_args(PropertyKind::Size, args);
106                    }
107                }
108                let c = super::resolve::expr_to_pest(tcx, def_id, const_expr);
109                args.push(PropertyArg::Expr(c));
110                Self::new_with_args(PropertyKind::Size, args)
111            }
112            _ => {
113                rap_error!(
114                    "Wrong args length for Size Tag! expected 2, got {}",
115                    exprs.len()
116                );
117                Self::new_simple(PropertyKind::Unknown)
118            }
119        }
120    }
121
122    fn build_allocated(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
123        match exprs {
124            [target] => Self::new_with_args(
125                PropertyKind::Allocated,
126                vec![super::resolve::parse_target_arg(tcx, def_id, target)],
127            ),
128            [target_expr, ty_expr, len_expr] => {
129                let target = super::resolve::parse_target_arg(tcx, def_id, target_expr);
130                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "Allocated") else {
131                    return Self::new_simple(PropertyKind::Unknown);
132                };
133                let length = super::resolve::expr_to_pest(tcx, def_id, len_expr);
134                Self::new_with_args(
135                    PropertyKind::Allocated,
136                    vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
137                )
138            }
139            [target_expr, ty_expr, len_expr, allocator_expr] => {
140                let target = super::resolve::parse_target_arg(tcx, def_id, target_expr);
141                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "Allocated") else {
142                    return Self::new_simple(PropertyKind::Unknown);
143                };
144                let length = super::resolve::expr_to_pest(tcx, def_id, len_expr);
145                let allocator = access_ident_recursive(allocator_expr)
146                    .map(|(name, _)| name)
147                    .unwrap_or_else(|| "global".to_string());
148                Self::new_with_args(
149                    PropertyKind::Allocated,
150                    vec![
151                        target,
152                        PropertyArg::Ty(ty),
153                        PropertyArg::Expr(length),
154                        PropertyArg::Ident(allocator),
155                    ],
156                )
157            }
158            _ => {
159                rap_error!(
160                    "Wrong args length for Allocated Tag! expected 3 or 4, got {}",
161                    exprs.len()
162                );
163                Self::new_simple(PropertyKind::Unknown)
164            }
165        }
166    }
167
168    fn build_inbound(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
169        match exprs {
170            [expr] => {
171                let expr = super::resolve::expr_to_pest(tcx, def_id, expr);
172                if matches!(expr, ContractExpr::IndexAccess { .. }) {
173                    Self::new_with_args(PropertyKind::InBound, vec![PropertyArg::Expr(expr)])
174                } else {
175                    Self::new_simple(PropertyKind::Unknown)
176                }
177            }
178            [_target, ty_expr, len_expr] => {
179                let target = super::resolve::parse_target_arg(tcx, def_id, &exprs[0]);
180                let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "InBound") else {
181                    return Self::new_simple(PropertyKind::Unknown);
182                };
183                let length = super::resolve::expr_to_pest(tcx, def_id, len_expr);
184                Self::new_with_args(
185                    PropertyKind::InBound,
186                    vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
187                )
188            }
189            [target, index_expr] => {
190                let slice = super::resolve::expr_to_pest(tcx, def_id, target);
191                let index = super::resolve::expr_to_pest(tcx, def_id, index_expr);
192                if matches!(slice, ContractExpr::Unknown)
193                    || matches!(index, ContractExpr::Unknown)
194                {
195                    return Self::new_simple(PropertyKind::Unknown);
196                }
197                // Auto-detect array index for for_each
198                let for_each = super::place::detect_array_for_each(tcx, def_id, index_expr);
199                let mut prop = Self::new_leaf(
200                    PropertyKind::InBound,
201                    vec![PropertyArg::Expr(ContractExpr::IndexAccess {
202                        slice: Box::new(slice),
203                        index: Box::new(index),
204                    })],
205                );
206                prop.set_for_each(for_each);
207                prop
208            }
209            _ => {
210                Self::check_arg_length(exprs.len(), 3, "InBound");
211                Self::new_simple(PropertyKind::Unknown)
212            }
213        }
214    }
215
216    fn build_nonoverlap(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
217        match exprs {
218            [indices] => {
219                let target = super::resolve::parse_target_arg(tcx, def_id, indices);
220                Self::new_with_args(PropertyKind::NonOverlap, vec![target])
221            }
222            [a, b, ty_expr, count_expr] => {
223                let left = super::resolve::parse_target_arg(tcx, def_id, a);
224                let right = super::resolve::parse_target_arg(tcx, def_id, b);
225                let count = super::resolve::expr_to_pest(tcx, def_id, count_expr);
226                let mut args = vec![left, right];
227                if let Some(ty) = super::resolve::parse_type(tcx, def_id, ty_expr, "NonOverlap") {
228                    args.push(PropertyArg::Ty(ty));
229                }
230                args.push(PropertyArg::Expr(count));
231                Self::new_with_args(PropertyKind::NonOverlap, args)
232            }
233            _ => {
234                rap_error!(
235                    "Wrong args length for NonOverlap Tag! expected 4, got {}",
236                    exprs.len()
237                );
238                Self::new_simple(PropertyKind::Unknown)
239            }
240        }
241    }
242
243    fn build_validnum(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
244        let predicates = super::resolve::parse_valid_num(tcx, def_id, exprs);
245        if predicates.is_empty() {
246            Self::new_simple(PropertyKind::Unknown)
247        } else {
248            Self::new_with_args(
249                PropertyKind::ValidNum,
250                vec![PropertyArg::Predicates(predicates)],
251            )
252        }
253    }
254
255    fn build_targets(
256        spec: &spec::PropertySpec,
257        tcx: TyCtxt<'tcx>,
258        def_id: DefId,
259        exprs: &[Expr],
260    ) -> Self {
261        let mut prop = Self::new_with_targets(spec.kind, tcx, def_id, exprs);
262        prop.set_contract_kind(spec.contract_kind);
263        prop
264    }
265
266    fn build_pinned(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
267        match exprs {
268            [ptr_expr, lifetime_expr] => {
269                let target = super::resolve::parse_target_arg(tcx, def_id, ptr_expr);
270                let lifetime = access_ident_recursive(lifetime_expr)
271                    .map(|(name, _)| name)
272                    .unwrap_or_default();
273                let mut args = vec![target];
274                if !lifetime.is_empty() {
275                    args.push(PropertyArg::Ident(lifetime));
276                }
277                Self::new_with_args(PropertyKind::Pinned, args)
278            }
279            _ => {
280                rap_error!(
281                    "Wrong args length for Pinned Tag! expected 2, got {}",
282                    exprs.len()
283                );
284                Self::new_simple(PropertyKind::Unknown)
285            }
286        }
287    }
288
289    fn build_split_transmute(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self {
290        if !Self::check_arg_length(exprs.len(), 2, "SplitTransmute") {
291            return Self::new_simple(PropertyKind::Unknown);
292        }
293        let src_elem = super::resolve::unwrap_array_expr(tcx, def_id, &exprs[0]);
294        let dst_elem = super::resolve::unwrap_array_expr(tcx, def_id, &exprs[1]);
295        let (Some(src_elem), Some(dst_elem)) = (src_elem, dst_elem) else {
296            return Self::new_simple(PropertyKind::Unknown);
297        };
298        Self::new_with_args(
299            PropertyKind::SplitTransmute,
300            vec![PropertyArg::Ty(src_elem), PropertyArg::Ty(dst_elem)],
301        )
302    }
303
304    fn new_simple(kind: PropertyKind) -> Self {
305        Self::new_leaf(kind, Vec::new())
306    }
307
308    /// Parse one annotation entry into the properties it denotes.
309    ///
310    /// Plain entries (`Align(p, T)`, `Owning(p)`, ...) yield one property.
311    /// The `any(...)` combinator may expand to several: see [`Self::parse_any`].
312    pub fn parse_list(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr]) -> Vec<Self> {
313        // User-defined / compound `def` macro expansion takes precedence, so
314        // `#[rapx::requires(MyTag(...))]` can reference DSL-defined contracts.
315        if let Some(props) = super::def::expand_def(tcx, def_id, name, exprs) {
316            return props;
317        }
318        let mut props = if name == "any" {
319            Self::parse_any(tcx, def_id, exprs)
320        } else {
321            vec![Self::new(tcx, def_id, name, exprs)]
322        };
323        for prop in &mut props {
324            if let Property::Leaf(leaf) = prop {
325                if leaf.for_each.is_none() {
326                    for arg in &mut leaf.args {
327                        leaf.for_each = super::place::strip_iter_elements(arg);
328                        if leaf.for_each.is_some() {
329                            break;
330                        }
331                    }
332                }
333            }
334        }
335        props
336    }
337
338    /// Parse the disjunctive combinator `any(D1, D2, ...)` written in DNF:
339    /// `any` means logical OR between disjuncts, and commas inside a
340    /// parenthesised disjunct mean logical AND:
341    ///
342    /// ```text
343    /// any(Null(p), (P1(p, ...), P2(p, ...), ...))
344    /// ```
345    ///
346    /// A disjunct is either a single property application `P(...)` or a
347    /// parenthesised conjunction `(P1(...), ..., Pn(...))`.  Two patterns are
348    /// supported:
349    ///
350    /// 1. **Null guard**: exactly two disjuncts, one being `Null(p)` alone,
351    ///    the other a conjunction of properties over the same place `p`.  The
352    ///    disjunction expands to the conjunct properties, each holding
353    ///    whenever `p` is non-null and vacuously for a null `p`.
354    ///
355    /// 2. **General disjunction**: each disjunct is standalone or a
356    ///    conjunction, e.g., `any(Trait(T, Copy), Trait(T, TrivialClone))`.
357    ///    Produces a single `Property::Or` whose `groups`
358    ///    encode the DNF structure: each inner `Vec` is one AND-group.
359    fn parse_any(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Vec<Self> {
360        if !Self::check_arg_length(exprs.len(), 2, "any") {
361            return vec![Self::new_simple(PropertyKind::Unknown)];
362        }
363
364        let (Some(first), Some(second)) = (
365            Self::disjunct_parts(&exprs[0]),
366            Self::disjunct_parts(&exprs[1]),
367        ) else {
368            rap_error!("any(...) disjuncts must be property applications or (P1, P2, ...) groups");
369            return vec![Self::new_simple(PropertyKind::Unknown)];
370        };
371
372        // --- null-guard pattern ---
373        let is_null_guard =
374            |disjunct: &[(String, Vec<Expr>)]| disjunct.len() == 1 && disjunct[0].0 == "Null";
375        if is_null_guard(&first) && !is_null_guard(&second) {
376            return Self::build_null_guard(tcx, def_id, &first, &second);
377        }
378        if is_null_guard(&second) && !is_null_guard(&first) {
379            return Self::build_null_guard(tcx, def_id, &second, &first);
380        }
381
382        // --- general disjunction: build a single Or property ---
383        let all_standalone = [&first, &second].iter().all(|d| d.len() == 1);
384        if all_standalone {
385            let mut groups: Vec<Vec<Box<Self>>> = Vec::new();
386            for parts in [first, second] {
387                let mut group: Vec<Box<Self>> = Vec::new();
388                for (name, args) in parts {
389                    for prop in Self::parse_list(tcx, def_id, &name, &args) {
390                        group.push(Box::new(prop));
391                    }
392                }
393                groups.push(group);
394            }
395            return vec![Self::new_or(groups)];
396        }
397
398        rap_error!(
399            "any(...) currently supports either a Null(p) guard pattern or \
400             standalone property applications"
401        );
402        vec![Self::new_simple(PropertyKind::Unknown)]
403    }
404
405    /// Build the null-guard expansion: `Null(p) OR (P1 & P2 & ...)`.
406    fn build_null_guard(
407        tcx: TyCtxt<'tcx>,
408        def_id: DefId,
409        guard: &[(String, Vec<Expr>)],
410        conjuncts: &[(String, Vec<Expr>)],
411    ) -> Vec<Self> {
412        let guard_args = &guard[0].1;
413        if guard_args.len() != 1 {
414            rap_error!("Null(...) guard inside any(...) takes exactly one place");
415            return vec![Self::new_simple(PropertyKind::Unknown)];
416        }
417        let Some(guard_place) = super::place::parse_contract_place(tcx, def_id, &guard_args[0]) else {
418            rap_error!("cannot resolve the place guarded by Null(...) inside any(...)");
419            return vec![Self::new_simple(PropertyKind::Unknown)];
420        };
421        let guard_key = crate::verify::def_use::PlaceKey::from_contract_place(&guard_place);
422
423        let mut properties = Vec::new();
424        for (inner_name, inner_args) in conjuncts {
425            // Use `parse_list` so a compound `def` conjunct (e.g. `ValidPtr`)
426            // expands to its primitive components, each guarded by `Null(p)`.
427            let expanded = Self::parse_list(tcx, def_id, inner_name, inner_args);
428            for mut property in expanded {
429                if !Self::apply_null_guard(&mut property, &guard_key) {
430                    rap_error!(
431                        "any(Null(p), ...) requires every conjunct ({inner_name}) to \
432                         constrain the guarded place"
433                    );
434                    return vec![Self::new_simple(PropertyKind::Unknown)];
435                }
436                properties.push(property);
437            }
438        }
439        properties
440    }
441
442    /// Recursively propagate a null-guard to a property and every member of its
443    /// `Or` groups.  Returns `false` if a place-bearing member constrains a
444    /// place other than the guard.
445    fn apply_null_guard(
446        property: &mut Property<'tcx>,
447        guard_key: &crate::verify::def_use::PlaceKey,
448    ) -> bool {
449        match property {
450            Property::Or(or) => {
451                for group in &mut or.groups {
452                    for sub in group.iter_mut() {
453                        if !Self::apply_null_guard(sub, guard_key) {
454                            return false;
455                        }
456                    }
457                }
458                true
459            }
460            Property::Leaf(leaf) => {
461                if let Some(PropertyArg::Expr(ContractExpr::Place(place))) = leaf.args.first() {
462                    if crate::verify::def_use::PlaceKey::from_contract_place(place) != *guard_key {
463                        return false;
464                    }
465                }
466                leaf.null_guard = Some(guard_key.clone());
467                true
468            }
469        }
470    }
471
472    /// Split one disjunct into its conjunct calls: a `(P1, P2, ...)` tuple, a
473    /// parenthesised single property `(P)`, or a bare property application.
474    fn disjunct_parts(expr: &Expr) -> Option<Vec<(String, Vec<Expr>)>> {
475        match expr {
476            Expr::Tuple(tuple) => tuple.elems.iter().map(Self::call_parts).collect(),
477            Expr::Paren(paren) => Self::call_parts(&paren.expr).map(|parts| vec![parts]),
478            _ => Self::call_parts(expr).map(|parts| vec![parts]),
479        }
480    }
481
482    /// Split a `Name(arg, ...)` call expression into its name and arguments.
483    fn call_parts(expr: &Expr) -> Option<(String, Vec<Expr>)> {
484        let Expr::Call(call) = expr else {
485            return None;
486        };
487        let Expr::Path(path) = call.func.as_ref() else {
488            return None;
489        };
490        let name = path.path.get_ident()?.to_string();
491        Some((name, call.args.iter().cloned().collect()))
492    }
493
494    fn new_with_args(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self {
495        Self::new_leaf(kind, args)
496    }
497
498    fn new_with_targets(
499        kind: PropertyKind,
500        tcx: TyCtxt<'tcx>,
501        def_id: DefId,
502        exprs: &[Expr],
503    ) -> Self {
504        let (args, for_each) = Self::parse_target_args_with_for_each(tcx, def_id, exprs);
505        let mut prop = Self::new_leaf(kind, args);
506        prop.set_for_each(for_each);
507        prop
508    }
509
510    fn parse_target_args_with_for_each(
511        tcx: TyCtxt<'tcx>,
512        def_id: DefId,
513        exprs: &[Expr],
514    ) -> (Vec<PropertyArg<'tcx>>, Option<ContractPlace<'tcx>>) {
515        let raw_args: Vec<_> = exprs
516            .iter()
517            .map(|expr| super::resolve::parse_target_arg(tcx, def_id, expr))
518            .collect();
519        let mut for_each = None;
520        let mut clean_args = Vec::with_capacity(raw_args.len());
521        for arg in raw_args {
522            let mut clean = arg;
523            if for_each.is_none() {
524                if let Some(container) = super::place::strip_iter_elements(&mut clean) {
525                    for_each = Some(container);
526                }
527            }
528            clean_args.push(clean);
529        }
530        // Auto-detect array arguments: if no explicit .iter() was used
531        // but an argument is an array type [T; N], automatically set
532        // for_each so the property is checked per-element.
533        if for_each.is_none() {
534            let fn_sig = tcx.fn_sig(def_id).instantiate_identity().skip_binder();
535            for (i, arg_ty) in fn_sig.inputs().iter().enumerate() {
536                if let rustc_middle::ty::TyKind::Array(..) = arg_ty.kind() {
537                    for_each = Some(crate::verify::contract::ContractPlace {
538                        base: PlaceBase::Arg(i),
539                        projections: vec![],
540                    });
541                    break;
542                }
543            }
544        }
545        (clean_args, for_each)
546    }
547
548    fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool {
549        if expr_len != required_len {
550            rap_error!(
551                "Wrong args length for {:?} Tag! expected {required_len}, got {expr_len}",
552                sp
553            );
554            return false;
555        }
556        true
557    }
558}
559
rapx/verify/contract/builder.rs

rapx/verify/contract/
builder.rs
