rapx/verify/contract/
pest_conv.rs

1//! Semantic converter: pest `Pairs<Rule>` → `ContractExpr` / `NumericPredicate`.
2//!
3//! This is the phase-2 counterpart to `pest_grammar.rs`: it turns the parse
4//! tree produced by the pest grammar into the contract AST (`types.rs`).
5//!
6//! Places (fields, projections) are bridged through the `place.rs` / `resolve.rs`
7//! helpers via a `syn` round-trip, since resolving a field name to a `Ty` still
8//! needs the rustc type context.  The arithmetic / call / if / constant layers
9//! are converted directly from the pest tree.
10
11use pest::iterators::Pair;
12use pest::Parser;
13use rustc_hir::def_id::DefId;
14use rustc_middle::ty::TyCtxt;
15
16use super::pest_grammar::{ContractParser, Rule};
17use super::place::resolve_place_from_ident;
18use super::types::{
19    ContractExpr, ContractPlace, NumericOp, NumericPredicate, NumericUnaryOp, PlaceBase, RelOp,
20};
21use crate::helpers::name::match_ty_with_ident;
22
23fn only_child(pair: Pair<Rule>) -> Pair<Rule> {
24    pair.into_inner().next().expect("expected a single child pair")
25}
26
27fn relop_from_str(s: &str) -> Option<RelOp> {
28    match s {
29        "==" => Some(RelOp::Eq),
30        "!=" => Some(RelOp::Ne),
31        "<" => Some(RelOp::Lt),
32        "<=" => Some(RelOp::Le),
33        ">" => Some(RelOp::Gt),
34        ">=" => Some(RelOp::Ge),
35        _ => None,
36    }
37}
38
39/// Parse a numeric expression (no comparison) into a `ContractExpr`.
40pub fn parse_expr_pest<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, text: &str) -> ContractExpr<'tcx> {
41    let Ok(mut pairs) = ContractParser::parse(Rule::expr, text) else {
42        rap_debug!("contract expression not supported by grammar: {text}");
43        return ContractExpr::Unknown;
44    };
45    conv_expr(tcx, def_id, pairs.next().expect("expr pair"))
46}
47
48/// Parse a predicate (comparison / `!x.is_empty()` / bare expr) into a
49/// `NumericPredicate`.
50pub fn parse_predicate_pest<'tcx>(
51    tcx: TyCtxt<'tcx>,
52    def_id: DefId,
53    text: &str,
54) -> Option<NumericPredicate<'tcx>> {
55    let Ok(mut pairs) = ContractParser::parse(Rule::expr, text) else {
56        rap_debug!("contract predicate not supported by grammar: {text}");
57        return None;
58    };
59    conv_predicate(tcx, def_id, pairs.next().expect("expr pair"))
60}
61
62fn conv_expr<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
63    match pair.as_rule() {
64        Rule::expr => conv_expr(tcx, def_id, only_child(pair)),
65        Rule::if_expr => conv_if(tcx, def_id, pair),
66        Rule::cmp => {
67            // Expression layer carries no comparison operator.
68            let mut inner = pair.into_inner();
69            let lhs = conv_bit_or(tcx, def_id, inner.next().expect("cmp lhs"));
70            if inner.next().is_some() {
71                ContractExpr::Unknown
72            } else {
73                lhs
74            }
75        }
76        Rule::bit_or | Rule::bit_xor | Rule::bit_and | Rule::additive | Rule::multiplicative => {
77            conv_bit_or(tcx, def_id, pair)
78        }
79        Rule::unary => conv_unary(tcx, def_id, pair),
80        Rule::primary => conv_primary(tcx, def_id, pair),
81        Rule::call => conv_call(tcx, def_id, pair),
82        Rule::place => conv_place_bridge(tcx, def_id, pair),
83        Rule::const_path => conv_const_path(tcx, def_id, pair),
84        Rule::int => ContractExpr::Const(pair.as_str().parse::<u128>().unwrap_or(0)),
85        _ => ContractExpr::Unknown,
86    }
87}
88
89fn conv_predicate<'tcx>(
90    tcx: TyCtxt<'tcx>,
91    def_id: DefId,
92    pair: Pair<Rule>,
93) -> Option<NumericPredicate<'tcx>> {
94    match pair.as_rule() {
95        Rule::expr | Rule::cond => conv_predicate(tcx, def_id, only_child(pair)),
96        Rule::cmp => {
97            let mut inner = pair.into_inner();
98            let lhs = conv_bit_or(tcx, def_id, inner.next()?);
99            match inner.next() {
100                Some(relop_pair) => {
101                    let op = relop_from_str(relop_pair.as_str())?;
102                    let rhs = conv_bit_or(tcx, def_id, inner.next()?);
103                    Some(NumericPredicate::new(lhs, op, rhs))
104                }
105                // Bare expression → `expr != 0`.
106                None => Some(NumericPredicate::new(lhs, RelOp::Ne, ContractExpr::Const(0))),
107            }
108        }
109        Rule::not_is_empty => {
110            let mut inner = pair.into_inner();
111            let base_text = inner.next()?.as_str().to_string();
112            let place = conv_base(tcx, def_id, &base_text);
113            Some(NumericPredicate::new(
114                ContractExpr::Len(Box::new(place)),
115                RelOp::Ne,
116                ContractExpr::Const(0),
117            ))
118        }
119        _ => None,
120    }
121}
122
123fn conv_if<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
124    let mut inner = pair.into_inner();
125    let cond_pair = inner.next().expect("if cond");
126    let then_pair = inner.next().expect("if then");
127    let else_pair = inner.next().expect("if else");
128    let Some(cond) = conv_predicate(tcx, def_id, cond_pair) else {
129        return ContractExpr::Unknown;
130    };
131    let then_expr = conv_expr(tcx, def_id, then_pair);
132    let else_expr = conv_expr(tcx, def_id, else_pair);
133    ContractExpr::If {
134        cond: Box::new(cond),
135        then_expr: Box::new(then_expr),
136        else_expr: Box::new(else_expr),
137    }
138}
139
140fn op_from_str(op: &str) -> Option<NumericOp> {
141    match op {
142        "+" => Some(NumericOp::Add),
143        "-" => Some(NumericOp::Sub),
144        "*" => Some(NumericOp::Mul),
145        "/" => Some(NumericOp::Div),
146        "%" => Some(NumericOp::Rem),
147        "&" => Some(NumericOp::BitAnd),
148        "|" => Some(NumericOp::BitOr),
149        "^" => Some(NumericOp::BitXor),
150        _ => None,
151    }
152}
153
154fn conv_left_assoc<'tcx>(
155    tcx: TyCtxt<'tcx>,
156    def_id: DefId,
157    pair: Pair<Rule>,
158    operand: impl Fn(TyCtxt<'tcx>, DefId, Pair<Rule>) -> ContractExpr<'tcx>,
159) -> ContractExpr<'tcx> {
160    let mut inner = pair.into_inner();
161    let mut acc = operand(tcx, def_id, inner.next().expect("first operand"));
162    while let Some(op_pair) = inner.next() {
163        let Some(op) = op_from_str(op_pair.as_str()) else {
164            return ContractExpr::Unknown;
165        };
166        let rhs = operand(tcx, def_id, inner.next().expect("rhs operand"));
167        acc = ContractExpr::Binary {
168            op,
169            lhs: Box::new(acc),
170            rhs: Box::new(rhs),
171        };
172    }
173    acc
174}
175
176fn conv_bit_or<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
177    match pair.as_rule() {
178        Rule::bit_or => conv_left_assoc(tcx, def_id, pair, conv_bit_xor),
179        _ => conv_bit_xor(tcx, def_id, pair),
180    }
181}
182
183fn conv_bit_xor<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
184    match pair.as_rule() {
185        Rule::bit_xor => conv_left_assoc(tcx, def_id, pair, conv_bit_and),
186        _ => conv_bit_and(tcx, def_id, pair),
187    }
188}
189
190fn conv_bit_and<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
191    match pair.as_rule() {
192        Rule::bit_and => conv_left_assoc(tcx, def_id, pair, conv_additive),
193        _ => conv_additive(tcx, def_id, pair),
194    }
195}
196
197fn conv_additive<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
198    match pair.as_rule() {
199        Rule::additive => conv_left_assoc(tcx, def_id, pair, conv_multiplicative),
200        _ => conv_multiplicative(tcx, def_id, pair),
201    }
202}
203
204fn conv_multiplicative<'tcx>(
205    tcx: TyCtxt<'tcx>,
206    def_id: DefId,
207    pair: Pair<Rule>,
208) -> ContractExpr<'tcx> {
209    match pair.as_rule() {
210        Rule::multiplicative => conv_left_assoc(tcx, def_id, pair, conv_unary),
211        _ => conv_unary(tcx, def_id, pair),
212    }
213}
214
215fn conv_unary<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
216    let mut inner = pair.into_inner();
217    let first = inner.next().expect("unary operand");
218    match first.as_rule() {
219        Rule::unop => {
220            let op = match first.as_str() {
221                "!" => NumericUnaryOp::Not,
222                "-" => NumericUnaryOp::Neg,
223                _ => return ContractExpr::Unknown,
224            };
225            let operand = conv_unary(tcx, def_id, inner.next().expect("unary inner"));
226            ContractExpr::Unary {
227                op,
228                expr: Box::new(operand),
229            }
230        }
231        _ => conv_primary(tcx, def_id, first),
232    }
233}
234
235fn conv_primary<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
236    let inner = only_child(pair);
237    match inner.as_rule() {
238        Rule::int => ContractExpr::Const(inner.as_str().parse::<u128>().unwrap_or(0)),
239        Rule::call => conv_call(tcx, def_id, inner),
240        Rule::size_of_call => conv_size_of_call(tcx, def_id, inner),
241        Rule::const_path => conv_const_path(tcx, def_id, inner),
242        Rule::place => conv_place_bridge(tcx, def_id, inner),
243        Rule::expr => conv_expr(tcx, def_id, inner),
244        _ => ContractExpr::Unknown,
245    }
246}
247
248/// Convert `size_of::<T>()` / `align_of::<T>()` (optionally `std::mem::` /
249/// `core::mem::` prefixed) into `SizeOf` / `AlignOf`.
250fn conv_size_of_call<'tcx>(
251    tcx: TyCtxt<'tcx>,
252    def_id: DefId,
253    pair: Pair<Rule>,
254) -> ContractExpr<'tcx> {
255    let text = pair.as_str();
256    let (kind, rest) = if text.contains("align_of") {
257        ("align_of", text.split("align_of").nth(1).unwrap_or(""))
258    } else {
259        ("size_of", text.split("size_of").nth(1).unwrap_or(""))
260    };
261    // rest looks like " :: < usize > ()" — extract the ident between `<` and `>`.
262    let ty_name = rest
263        .find('<')
264        .and_then(|lt| {
265            rest[lt + 1..]
266                .find('>')
267                .map(|gt| rest[lt + 1..lt + 1 + gt].trim().to_string())
268        })
269        .unwrap_or_default();
270    let Some(ty) = match_ty_with_ident(tcx, def_id, ty_name) else {
271        return ContractExpr::Unknown;
272    };
273    match kind {
274        "size_of" => ContractExpr::SizeOf(ty),
275        _ => ContractExpr::AlignOf(ty),
276    }
277}
278
279fn conv_call<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, pair: Pair<Rule>) -> ContractExpr<'tcx> {
280    let mut inner = pair.into_inner();
281    let builtin = inner.next().expect("builtin").as_str().to_string();
282    // `call = builtin "(" arg_list? ")"`; arg_list's children are the `arg`s.
283    let args: Vec<Pair<Rule>> = match inner.next() {
284        Some(arg_list) => arg_list.into_inner().collect(),
285        None => Vec::new(),
286    };
287    match builtin.as_str() {
288        "size_of" | "align_of" => {
289            let ty_name = args
290                .first()
291                .map(|a| a.as_str().trim().to_string())
292                .unwrap_or_default();
293            let Some(ty) = match_ty_with_ident(tcx, def_id, ty_name) else {
294                return ContractExpr::Unknown;
295            };
296            match builtin.as_str() {
297                "size_of" => ContractExpr::SizeOf(ty),
298                _ => ContractExpr::AlignOf(ty),
299            }
300        }
301        "len" => {
302            let Some(arg) = args.first() else {
303                return ContractExpr::Unknown;
304            };
305            ContractExpr::Len(Box::new(conv_arg_expr(tcx, def_id, arg.clone())))
306        }
307        "min" | "max" => {
308            if args.len() != 2 {
309                return ContractExpr::Unknown;
310            }
311            let a = conv_arg_expr(tcx, def_id, args[0].clone());
312            let b = conv_arg_expr(tcx, def_id, args[1].clone());
313            match builtin.as_str() {
314                "min" => ContractExpr::Min {
315                    a: Box::new(a),
316                    b: Box::new(b),
317                },
318                _ => ContractExpr::Max {
319                    a: Box::new(a),
320                    b: Box::new(b),
321                },
322            }
323        }
324        "index_access" => {
325            if args.len() != 2 {
326                return ContractExpr::Unknown;
327            }
328            let slice = conv_arg_expr(tcx, def_id, args[0].clone());
329            let index = conv_arg_expr(tcx, def_id, args[1].clone());
330            ContractExpr::IndexAccess {
331                slice: Box::new(slice),
332                index: Box::new(index),
333            }
334        }
335        _ => ContractExpr::Unknown,
336    }
337}
338
339fn conv_arg_expr<'tcx>(
340    tcx: TyCtxt<'tcx>,
341    def_id: DefId,
342    arg: Pair<Rule>,
343) -> ContractExpr<'tcx> {
344    let inner = only_child(arg);
345    match inner.as_rule() {
346        Rule::expr => conv_expr(tcx, def_id, inner),
347        _ => ContractExpr::Unknown,
348    }
349}
350
351fn conv_const_path<'tcx>(
352    tcx: TyCtxt<'tcx>,
353    def_id: DefId,
354    pair: Pair<Rule>,
355) -> ContractExpr<'tcx> {
356    let text = pair.as_str();
357    let Some((ty_name, which)) = text.rsplit_once("::") else {
358        return ContractExpr::Unknown;
359    };
360    let ty_name = ty_name.trim();
361    let which = which.trim();
362    let Some(ty) = super::resolve::resolve_type_name(tcx, def_id, ty_name) else {
363        return ContractExpr::Unknown;
364    };
365    // `T::BITS` is the bit width, i.e. `size_of::<T>() * 8`.
366    if which == "BITS" {
367        return ContractExpr::Binary {
368            op: NumericOp::Mul,
369            lhs: Box::new(ContractExpr::SizeOf(ty)),
370            rhs: Box::new(ContractExpr::Const(8)),
371        };
372    }
373    let Some((min, max)) = super::resolve::int_type_min_max(tcx, ty) else {
374        return ContractExpr::Unknown;
375    };
376    match which {
377        "MAX" => ContractExpr::Const(max),
378        "MIN" => {
379            // Signed integers: `int_type_min_max` returns the negated magnitude
380            // (`-(MIN) == 2^(bits-1)`) as a `u128` because it cannot represent
381            // the negative `MIN`. Emit an explicit negation so `i32::MIN`
382            // resolves to `-2147483648` rather than `+2147483648`.
383            if let rustc_middle::ty::TyKind::Int(_) = ty.kind() {
384                ContractExpr::Unary {
385                    op: NumericUnaryOp::Neg,
386                    expr: Box::new(ContractExpr::Const(min)),
387                }
388            } else {
389                ContractExpr::Const(min)
390            }
391        }
392        _ => ContractExpr::Unknown,
393    }
394}
395
396/// Bridge a place through the existing syn-based parser (handles field
397/// projections, `unwrap_some`, `iter`, and `x.len` sugar uniformly).
398fn conv_place_bridge<'tcx>(
399    tcx: TyCtxt<'tcx>,
400    def_id: DefId,
401    pair: Pair<Rule>,
402) -> ContractExpr<'tcx> {
403    let text = pair.as_str();
404    let Ok(expr) = safety_parser::syn::parse_str::<safety_parser::syn::Expr>(text) else {
405        return ContractExpr::Unknown;
406    };
407    super::resolve::parse_contract_expr(tcx, def_id, &expr, "pest")
408}
409
410/// Convert a `not_is_empty` base (`self` / `return` / `Arg_N` / ident) into a
411/// place expression.
412fn conv_base<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, base_text: &str) -> ContractExpr<'tcx> {
413    match base_text {
414        "return" => ContractExpr::Place(ContractPlace {
415            base: PlaceBase::Return,
416            projections: Vec::new(),
417        }),
418        s if s.starts_with("Arg_") => {
419            let idx = s[4..].parse::<usize>().unwrap_or(0);
420            ContractExpr::Place(ContractPlace::arg(idx))
421        }
422        _ => {
423            let Some((base, fields, _)) = resolve_place_from_ident(tcx, def_id, base_text, &[]) else {
424                return ContractExpr::Unknown;
425            };
426            ContractExpr::Place(ContractPlace::local(base, fields))
427        }
428    }
429}
rapx/verify/contract/pest_conv.rs

rapx/verify/contract/
pest_conv.rs
