rapx/verify/contract/
resolve.rs

1//! Expression / argument resolution: `syn::Expr` → semantic values.
2//!
3//! The numeric-expression layer is parsed by the pest grammar (`pest_conv.rs`);
4//! everything that still needs rustc's type context or `syn` structure lives
5//! here: places (via `place.rs`), const generics, builtin integer bounds, the
6//! `x.len()` sugar, tag argument types/targets, and `ValidNum` predicates.
7
8use quote::ToTokens;
9use rustc_hir::def_id::DefId;
10use rustc_middle::ty::{GenericParamDefKind, Ty, TyCtxt};
11use safety_parser::syn::{Expr, Lit};
12
13use crate::helpers::fn_info::parse_expr_into_number;
14use crate::helpers::name::{access_ident_recursive, match_ty_with_ident};
15
16use super::place;
17use super::types::{ContractExpr, NumericPredicate, PropertyArg, RelOp};
18
19pub(crate) fn parse_contract_expr<'tcx>(
20    tcx: TyCtxt<'tcx>,
21    def_id: DefId,
22    expr: &Expr,
23    sp: &str,
24) -> ContractExpr<'tcx> {
25    // `x.len` / `x.len()` sugar -> len(x).
26    if let Expr::Field(expr_field) = expr
27        && matches!(&expr_field.member, safety_parser::syn::Member::Named(ident) if ident == "len")
28    {
29        return ContractExpr::Len(Box::new(parse_contract_expr(
30            tcx,
31            def_id,
32            &expr_field.base,
33            sp,
34        )));
35    }
36    if let Expr::MethodCall(expr_method) = expr
37        && expr_method.method == "len"
38        && expr_method.args.is_empty()
39    {
40        return ContractExpr::Len(Box::new(parse_contract_expr(
41            tcx,
42            def_id,
43            &expr_method.receiver,
44            sp,
45        )));
46    }
47
48    // A place (fields, projections), a const generic, or a builtin constant.
49    if let Some(place) = place::parse_contract_place(tcx, def_id, expr) {
50        return ContractExpr::Place(place);
51    }
52    if let Some(e) = parse_const_param(tcx, def_id, expr) {
53        return e;
54    }
55    if let Some(value) = parse_builtin_const(tcx, expr) {
56        return ContractExpr::Const(value);
57    }
58    if let Some(value) = parse_expr_into_number(expr) {
59        return ContractExpr::new_value(value);
60    }
61    rap_debug!(
62        "Numeric expression in {:?} could not be resolved: {:?}",
63        sp,
64        expr
65    );
66    ContractExpr::Unknown
67}
68
69pub(crate) fn resolve_type_name<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str) -> Option<Ty<'tcx>> {
70    if name == "Self" {
71        let sig = tcx.fn_sig(def_id).skip_binder();
72        return sig.inputs().skip_binder().first().copied();
73    }
74    match_ty_with_ident(tcx, def_id, name.to_string())
75}
76
77pub(crate) fn int_type_min_max<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> Option<(u128, u128)> {
78    use rustc_middle::ty::IntTy;
79    use rustc_middle::ty::UintTy;
80    let bits: u32 = match ty.kind() {
81        rustc_middle::ty::TyKind::Uint(ut) => match ut {
82            UintTy::U8 => 8,
83            UintTy::U16 => 16,
84            UintTy::U32 => 32,
85            UintTy::U64 => 64,
86            UintTy::U128 => 128,
87            UintTy::Usize => tcx.data_layout.pointer_size().bits() as u32,
88        },
89        rustc_middle::ty::TyKind::Int(it) => match it {
90            IntTy::I8 => 8,
91            IntTy::I16 => 16,
92            IntTy::I32 => 32,
93            IntTy::I64 => 64,
94            IntTy::I128 => 128,
95            IntTy::Isize => tcx.data_layout.pointer_size().bits() as u32,
96        },
97        _ => return None,
98    };
99    if bits == 0 {
100        return None;
101    }
102    match ty.kind() {
103        rustc_middle::ty::TyKind::Uint(_) => {
104            let max = if bits == 128 {
105                u128::MAX
106            } else {
107                (1u128 << bits) - 1
108            };
109            Some((0, max))
110        }
111        rustc_middle::ty::TyKind::Int(_) => {
112            let max = (1u128 << (bits - 1)) - 1;
113            let min = max + 1;
114            Some((min, max))
115        }
116        _ => None,
117    }
118}
119
120fn parse_builtin_const<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr) -> Option<u128> {
121    let Expr::Path(expr_path) = expr else {
122        return None;
123    };
124    let mut segments = expr_path.path.segments.iter();
125    let first = segments.next()?.ident.to_string();
126    let second = segments.next()?.ident.to_string();
127    if segments.next().is_some() || second != "MAX" {
128        return None;
129    }
130
131    let pointer_bits = tcx.data_layout.pointer_size().bits();
132    match first.as_str() {
133        "isize" => Some((1_u128 << (pointer_bits - 1)) - 1),
134        "usize" => Some((1_u128 << pointer_bits) - 1),
135        _ => None,
136    }
137}
138
139fn parse_const_param<'tcx>(
140    tcx: TyCtxt<'tcx>,
141    def_id: DefId,
142    expr: &Expr,
143) -> Option<ContractExpr<'tcx>> {
144    let Expr::Path(expr_path) = expr else {
145        return None;
146    };
147    let ident = expr_path.path.get_ident()?.to_string();
148    let mut generics = Some(tcx.generics_of(def_id));
149    while let Some(current) = generics {
150        if let Some(param) = current.own_params.iter().find(|param| {
151            matches!(param.kind, GenericParamDefKind::Const { .. })
152                && param.name.as_str() == ident
153        }) {
154            return Some(ContractExpr::ConstParam {
155                index: param.index,
156                name: ident,
157            });
158        }
159        generics = current.parent.map(|parent| tcx.generics_of(parent));
160    }
161    None
162}
163
164pub(crate) fn parse_type<'tcx>(
165    tcx: TyCtxt<'tcx>,
166    def_id: DefId,
167    expr: &Expr,
168    sp: &str,
169) -> Option<Ty<'tcx>> {
170    let ty_ident_full = access_ident_recursive(expr);
171    if ty_ident_full.is_none() {
172        rap_debug!("Incorrect expression for the type of {:?} Tag!", sp);
173        return None;
174    }
175    let ty_ident = ty_ident_full.unwrap().0;
176    let ty = match_ty_with_ident(tcx, def_id, ty_ident);
177    if ty.is_none() {
178        rap_debug!("Cannot get type in {:?} Tag!", sp);
179    }
180    ty
181}
182
183pub(crate) fn parse_target_arg<'tcx>(
184    tcx: TyCtxt<'tcx>,
185    def_id: DefId,
186    expr: &Expr,
187) -> PropertyArg<'tcx> {
188    // For simple identifiers that aren't local variables (e.g., lifetime param
189    // 'a parsed as ident `a`), store as Ident rather than Expr (which would
190    // become Unknown).
191    if let Expr::Path(expr_path) = expr {
192        if let Some(ident) = expr_path.path.get_ident() {
193            let s = ident.to_string();
194            if s != "return"
195                && !s.starts_with("Arg_")
196                && place::parse_expr_into_local_and_ty(tcx, def_id, expr).is_none()
197            {
198                return PropertyArg::Ident(s);
199            }
200        }
201    }
202    place::parse_contract_place(tcx, def_id, expr)
203        .map(|p| PropertyArg::Expr(ContractExpr::Place(p)))
204        .unwrap_or_else(|| PropertyArg::Expr(parse_contract_expr(tcx, def_id, expr, "target")))
205}
206
207pub(crate) fn parse_valid_num<'tcx>(
208    tcx: TyCtxt<'tcx>,
209    def_id: DefId,
210    exprs: &[Expr],
211) -> Vec<NumericPredicate<'tcx>> {
212    match exprs {
213        [] => Vec::new(),
214        [expr] => parse_numeric_predicate(tcx, def_id, expr).into_iter().collect(),
215        [value, range, ..] => {
216            if let Some(predicates) = parse_interval_predicates(tcx, def_id, value, range) {
217                predicates
218            } else {
219                parse_numeric_predicate(tcx, def_id, value)
220                    .into_iter()
221                    .collect()
222            }
223        }
224    }
225}
226
227fn parse_numeric_predicate<'tcx>(
228    tcx: TyCtxt<'tcx>,
229    def_id: DefId,
230    expr: &Expr,
231) -> Option<NumericPredicate<'tcx>> {
232    let text = expr.to_token_stream().to_string();
233    super::pest_conv::parse_predicate_pest(tcx, def_id, &text)
234}
235
236pub(crate) fn expr_to_pest<'tcx>(
237    tcx: TyCtxt<'tcx>,
238    def_id: DefId,
239    expr: &Expr,
240) -> ContractExpr<'tcx> {
241    let text = expr.to_token_stream().to_string();
242    super::pest_conv::parse_expr_pest(tcx, def_id, &text)
243}
244
245fn parse_interval_predicates<'tcx>(
246    tcx: TyCtxt<'tcx>,
247    def_id: DefId,
248    value: &Expr,
249    range: &Expr,
250) -> Option<Vec<NumericPredicate<'tcx>>> {
251    match range {
252        Expr::Array(array) if array.elems.len() == 2 => {
253            let mut elems = array.elems.iter();
254            let lower = elems.next().unwrap();
255            let upper = elems.next().unwrap();
256            Some(build_interval_predicates(
257                tcx, def_id, value, lower, true, upper, true,
258            ))
259        }
260        Expr::Lit(expr_lit) => {
261            let Lit::Str(range_lit) = &expr_lit.lit else {
262                return None;
263            };
264            parse_string_interval(tcx, def_id, value, &range_lit.value())
265        }
266        _ => None,
267    }
268}
269
270fn parse_string_interval<'tcx>(
271    tcx: TyCtxt<'tcx>,
272    def_id: DefId,
273    value: &Expr,
274    raw_range: &str,
275) -> Option<Vec<NumericPredicate<'tcx>>> {
276    let trimmed = raw_range.trim();
277    if trimmed.len() < 5 {
278        return None;
279    }
280
281    let lower_inclusive = trimmed.starts_with('[');
282    let upper_inclusive = trimmed.ends_with(']');
283    if !(lower_inclusive || trimmed.starts_with('('))
284        || !(upper_inclusive || trimmed.ends_with(')'))
285    {
286        return None;
287    }
288
289    let body = &trimmed[1..trimmed.len() - 1];
290    let (lower_raw, upper_raw) = body.split_once(',')?;
291    let lower = safety_parser::syn::parse_str::<Expr>(lower_raw.trim()).ok()?;
292    let upper = safety_parser::syn::parse_str::<Expr>(upper_raw.trim()).ok()?;
293
294    Some(build_interval_predicates(
295        tcx,
296        def_id,
297        value,
298        &lower,
299        lower_inclusive,
300        &upper,
301        upper_inclusive,
302    ))
303}
304
305fn build_interval_predicates<'tcx>(
306    tcx: TyCtxt<'tcx>,
307    def_id: DefId,
308    value: &Expr,
309    lower: &Expr,
310    lower_inclusive: bool,
311    upper: &Expr,
312    upper_inclusive: bool,
313) -> Vec<NumericPredicate<'tcx>> {
314    let value_expr = expr_to_pest(tcx, def_id, value);
315    let lower_expr = expr_to_pest(tcx, def_id, lower);
316    let upper_expr = expr_to_pest(tcx, def_id, upper);
317    vec![
318        NumericPredicate::new(
319            lower_expr,
320            if lower_inclusive {
321                RelOp::Le
322            } else {
323                RelOp::Lt
324            },
325            value_expr.clone(),
326        ),
327        NumericPredicate::new(
328            value_expr,
329            if upper_inclusive {
330                RelOp::Le
331            } else {
332                RelOp::Lt
333            },
334            upper_expr,
335        ),
336    ]
337}
338
339/// Extract the inner type from an `Expr::Array` (the `[T]` notation in
340/// `SplitTransmute([T], [U])`), then resolve it via `parse_type`.
341pub(crate) fn unwrap_array_expr<'tcx>(
342    tcx: TyCtxt<'tcx>,
343    def_id: DefId,
344    expr: &Expr,
345) -> Option<Ty<'tcx>> {
346    if let Expr::Array(arr) = expr
347        && arr.elems.len() == 1
348    {
349        return parse_type(tcx, def_id, &arr.elems[0], "SplitTransmute");
350    }
351    parse_type(tcx, def_id, expr, "SplitTransmute")
352}
rapx/verify/contract/resolve.rs

rapx/verify/contract/
resolve.rs
