1use rustc_hir::def_id::DefId;
2use rustc_middle::mir::BinOp as MirBinOp;
3use rustc_middle::ty::{Ty, TyCtxt};
4use safety_parser::syn::{BinOp as SynBinOp, Expr, Lit, UnOp};
5
6use super::helpers::{
7 access_ident_recursive, match_ty_with_ident, parse_expr_into_local_and_ty,
8 parse_expr_into_number,
9};
10
11#[derive(Clone, Debug)]
12pub enum PlaceBase {
13 Return,
14 Arg(usize),
15 Local(usize),
16}
17
18#[derive(Clone, Debug)]
19pub enum ContractProjection<'tcx> {
20 Field { index: usize, ty: Option<Ty<'tcx>> },
21}
22
23#[derive(Clone, Debug)]
24pub struct ContractPlace<'tcx> {
25 pub base: PlaceBase,
26 pub projections: Vec<ContractProjection<'tcx>>,
27}
28
29impl<'tcx> ContractPlace<'tcx> {
30 pub fn local(base: usize, fields: Vec<(usize, Ty<'tcx>)>) -> Self {
31 Self {
32 base: if base == 0 {
33 PlaceBase::Return
34 } else {
35 PlaceBase::Local(base)
36 },
37 projections: fields
38 .into_iter()
39 .map(|(index, ty)| ContractProjection::Field {
40 index,
41 ty: Some(ty),
42 })
43 .collect(),
44 }
45 }
46
47 pub fn arg(index: usize) -> Self {
48 Self {
49 base: PlaceBase::Arg(index),
50 projections: Vec::new(),
51 }
52 }
53
54 pub fn local_base(&self) -> Option<usize> {
55 match self.base {
56 PlaceBase::Return => Some(0),
57 PlaceBase::Local(local) => Some(local),
58 PlaceBase::Arg(_) => None,
59 }
60 }
61
62 pub fn field_indices(&self) -> Vec<usize> {
63 self.projections
64 .iter()
65 .map(|projection| match projection {
66 ContractProjection::Field { index, .. } => *index,
67 })
68 .collect()
69 }
70}
71
72#[derive(Clone, Copy, Debug)]
73pub enum NumericOp {
74 Add,
75 Sub,
76 Mul,
77 Div,
78 Rem,
79 BitAnd,
80 BitOr,
81 BitXor,
82}
83
84impl NumericOp {
85 fn from_syn(op: &SynBinOp) -> Option<Self> {
86 match op {
87 SynBinOp::Add(_) => Some(Self::Add),
88 SynBinOp::Sub(_) => Some(Self::Sub),
89 SynBinOp::Mul(_) => Some(Self::Mul),
90 SynBinOp::Div(_) => Some(Self::Div),
91 SynBinOp::Rem(_) => Some(Self::Rem),
92 SynBinOp::BitAnd(_) => Some(Self::BitAnd),
93 SynBinOp::BitOr(_) => Some(Self::BitOr),
94 SynBinOp::BitXor(_) => Some(Self::BitXor),
95 _ => None,
96 }
97 }
98}
99
100#[derive(Clone, Copy, Debug)]
101pub enum NumericUnaryOp {
102 Not,
103 Neg,
104}
105
106impl NumericUnaryOp {
107 fn from_syn(op: &UnOp) -> Option<Self> {
108 match op {
109 UnOp::Not(_) => Some(Self::Not),
110 UnOp::Neg(_) => Some(Self::Neg),
111 _ => None,
112 }
113 }
114}
115
116#[derive(Clone, Debug)]
117pub enum ContractExpr<'tcx> {
118 Place(ContractPlace<'tcx>),
119 Const(u128),
120 SizeOf(Ty<'tcx>),
121 AlignOf(Ty<'tcx>),
122 Binary {
123 op: NumericOp,
124 lhs: Box<ContractExpr<'tcx>>,
125 rhs: Box<ContractExpr<'tcx>>,
126 },
127 Unary {
128 op: NumericUnaryOp,
129 expr: Box<ContractExpr<'tcx>>,
130 },
131 Unknown,
132}
133
134impl<'tcx> ContractExpr<'tcx> {
135 pub fn new_var(base: usize) -> Self {
136 Self::Place(ContractPlace::local(base, Vec::new()))
137 }
138
139 pub fn new_value(value: usize) -> Self {
140 Self::Const(value as u128)
141 }
142
143 pub fn new_unknown() -> Self {
144 Self::Unknown
145 }
146
147 pub fn get_var_base(&self) -> Option<usize> {
148 match self {
149 Self::Place(place) => place.local_base(),
150 _ => None,
151 }
152 }
153}
154
155#[derive(Clone, Copy, Debug)]
156pub enum RelOp {
157 Eq,
158 Ne,
159 Lt,
160 Le,
161 Gt,
162 Ge,
163}
164
165impl RelOp {
166 pub fn from_mir(op: MirBinOp) -> Option<Self> {
167 match op {
168 MirBinOp::Eq => Some(Self::Eq),
169 MirBinOp::Ne => Some(Self::Ne),
170 MirBinOp::Lt => Some(Self::Lt),
171 MirBinOp::Le => Some(Self::Le),
172 MirBinOp::Gt => Some(Self::Gt),
173 MirBinOp::Ge => Some(Self::Ge),
174 _ => None,
175 }
176 }
177
178 fn from_syn(op: &SynBinOp) -> Option<Self> {
179 match op {
180 SynBinOp::Eq(_) => Some(Self::Eq),
181 SynBinOp::Ne(_) => Some(Self::Ne),
182 SynBinOp::Lt(_) => Some(Self::Lt),
183 SynBinOp::Le(_) => Some(Self::Le),
184 SynBinOp::Gt(_) => Some(Self::Gt),
185 SynBinOp::Ge(_) => Some(Self::Ge),
186 _ => None,
187 }
188 }
189
190 pub fn reversed(self) -> Self {
191 match self {
192 Self::Eq => Self::Eq,
193 Self::Ne => Self::Ne,
194 Self::Lt => Self::Gt,
195 Self::Le => Self::Ge,
196 Self::Gt => Self::Lt,
197 Self::Ge => Self::Le,
198 }
199 }
200}
201
202#[derive(Clone, Debug)]
203pub struct NumericPredicate<'tcx> {
204 pub lhs: ContractExpr<'tcx>,
205 pub op: RelOp,
206 pub rhs: ContractExpr<'tcx>,
207}
208
209impl<'tcx> NumericPredicate<'tcx> {
210 pub fn new(lhs: ContractExpr<'tcx>, op: RelOp, rhs: ContractExpr<'tcx>) -> Self {
211 Self { lhs, op, rhs }
212 }
213
214 pub fn from_mir_locals(lhs: usize, rhs: usize, op: MirBinOp) -> Option<Self> {
215 RelOp::from_mir(op)
216 .map(|rel| Self::new(ContractExpr::new_var(lhs), rel, ContractExpr::new_var(rhs)))
217 }
218}
219
220#[derive(Clone, Debug)]
221pub enum PropertyKind {
222 Align,
223 Size,
224 NoPadding,
225 NonNull,
226 Allocated,
227 InBound,
228 NonOverlap,
229 ValidNum,
230 ValidString,
231 ValidCStr,
232 Init,
233 Unwrap,
234 Typed,
235 Owning,
236 Alias,
237 Alive,
238 Pinned,
239 NonVolatile,
240 Opened,
241 Trait,
242 Unreachable,
243 ValidPtr,
244 Deref,
245 Ptr2Ref,
246 Layout,
247 Unknown,
248}
249
250#[derive(Clone, Debug)]
251pub enum PropertyArg<'tcx> {
252 Place(ContractPlace<'tcx>),
253 Ty(Ty<'tcx>),
254 Expr(ContractExpr<'tcx>),
255 Predicates(Vec<NumericPredicate<'tcx>>),
256 Ident(String),
257}
258
259#[derive(Clone, Debug)]
260pub struct Property<'tcx> {
261 pub kind: PropertyKind,
262 pub args: Vec<PropertyArg<'tcx>>,
263}
264
265impl<'tcx> Property<'tcx> {
266 pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr]) -> Self {
267 match name {
268 "Align" => {
269 Self::check_arg_length(exprs.len(), 2, "Align");
270 let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
271 let ty = Self::parse_type(tcx, def_id, &exprs[1], "Align");
272 Self::new_with_args(PropertyKind::Align, vec![target, PropertyArg::Ty(ty)])
273 }
274 "Size" => Self::new_with_target(PropertyKind::Size, tcx, def_id, exprs),
275 "NoPadding" => Self::new_with_target(PropertyKind::NoPadding, tcx, def_id, exprs),
276 "NonNull" => Self::new_with_target(PropertyKind::NonNull, tcx, def_id, exprs),
277 "Allocated" => {
278 Self::check_arg_length(exprs.len(), 3, "Allocated");
279 let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
280 let ty = Self::parse_type(tcx, def_id, &exprs[1], "Allocated");
281 let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "Allocated");
282 Self::new_with_args(
283 PropertyKind::Allocated,
284 vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
285 )
286 }
287 "InBound" | "InBounded" => match exprs {
288 [_target, ty_expr, len_expr] => {
289 let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
290 let ty = Self::parse_type(tcx, def_id, ty_expr, "InBound");
291 let length = Self::parse_contract_expr(tcx, def_id, len_expr, "InBound");
292 Self::new_with_args(
293 PropertyKind::InBound,
294 vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
295 )
296 }
297 [target, len_expr] => {
298 let Some(ty) = Self::parse_target_type(tcx, def_id, target) else {
299 return Self::new_simple(PropertyKind::Unknown);
300 };
301 let target = Self::parse_target_arg(tcx, def_id, target);
302 let length = Self::parse_contract_expr(tcx, def_id, len_expr, "InBound");
303 Self::new_with_args(
304 PropertyKind::InBound,
305 vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
306 )
307 }
308 _ => {
309 Self::check_arg_length(exprs.len(), 3, "InBound");
310 Self::new_simple(PropertyKind::Unknown)
311 }
312 },
313 "NonOverlap" => Self::new_with_target(PropertyKind::NonOverlap, tcx, def_id, exprs),
314 "ValidNum" => {
315 let predicates = Self::parse_valid_num(tcx, def_id, exprs);
316 if predicates.is_empty() {
317 Self::new_simple(PropertyKind::Unknown)
318 } else {
319 Self::new_with_args(
320 PropertyKind::ValidNum,
321 vec![PropertyArg::Predicates(predicates)],
322 )
323 }
324 }
325 "ValidString" => Self::new_with_target(PropertyKind::ValidString, tcx, def_id, exprs),
326 "ValidCStr" => Self::new_with_target(PropertyKind::ValidCStr, tcx, def_id, exprs),
327 "Init" => {
328 Self::check_arg_length(exprs.len(), 3, "Init");
329 let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
330 let ty = Self::parse_type(tcx, def_id, &exprs[1], "Init");
331 let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "Init");
332 Self::new_with_args(
333 PropertyKind::Init,
334 vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
335 )
336 }
337 "Unwrap" => Self::new_with_target(PropertyKind::Unwrap, tcx, def_id, exprs),
338 "Typed" => {
339 Self::check_arg_length(exprs.len(), 2, "Typed");
340 let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
341 let ty = Self::parse_type(tcx, def_id, &exprs[1], "Typed");
342 Self::new_with_args(PropertyKind::Typed, vec![target, PropertyArg::Ty(ty)])
343 }
344 "Owning" => Self::new_with_target(PropertyKind::Owning, tcx, def_id, exprs),
345 "Alias" => Self::new_with_target(PropertyKind::Alias, tcx, def_id, exprs),
346 "Alive" => Self::new_with_target(PropertyKind::Alive, tcx, def_id, exprs),
347 "Pinned" => Self::new_with_target(PropertyKind::Pinned, tcx, def_id, exprs),
348 "NonVolatile" => Self::new_with_target(PropertyKind::NonVolatile, tcx, def_id, exprs),
349 "Opened" => Self::new_with_target(PropertyKind::Opened, tcx, def_id, exprs),
350 "Trait" => Self::new_with_target(PropertyKind::Trait, tcx, def_id, exprs),
351 "Unreachable" => Self::new_with_target(PropertyKind::Unreachable, tcx, def_id, exprs),
352 "ValidPtr" => {
353 Self::check_arg_length(exprs.len(), 3, "ValidPtr");
354 let target = Self::parse_target_arg(tcx, def_id, &exprs[0]);
355 let ty = Self::parse_type(tcx, def_id, &exprs[1], "ValidPtr");
356 let length = Self::parse_contract_expr(tcx, def_id, &exprs[2], "ValidPtr");
357 Self::new_with_args(
358 PropertyKind::ValidPtr,
359 vec![target, PropertyArg::Ty(ty), PropertyArg::Expr(length)],
360 )
361 }
362 "Deref" => Self::new_with_target(PropertyKind::Deref, tcx, def_id, exprs),
363 "Ptr2Ref" | "ValidPtr2Ref" => {
364 Self::new_with_target(PropertyKind::Ptr2Ref, tcx, def_id, exprs)
365 }
366 "Layout" => Self::new_with_target(PropertyKind::Layout, tcx, def_id, exprs),
367 _ => Self::new_simple(PropertyKind::Unknown),
368 }
369 }
370
371 pub fn new_partial_order(lhs: usize, rhs: usize, op: MirBinOp) -> Self {
372 if let Some(predicate) = NumericPredicate::from_mir_locals(lhs, rhs, op) {
373 Self::new_with_args(
374 PropertyKind::ValidNum,
375 vec![PropertyArg::Predicates(vec![predicate])],
376 )
377 } else {
378 Self::new_simple(PropertyKind::Unknown)
379 }
380 }
381
382 pub fn new_obj_boundary(ty: Ty<'tcx>, len: ContractExpr<'tcx>) -> Self {
383 Self::new_with_args(
384 PropertyKind::InBound,
385 vec![
386 PropertyArg::Expr(ContractExpr::Unknown),
387 PropertyArg::Ty(ty),
388 PropertyArg::Expr(len),
389 ],
390 )
391 }
392
393 fn new_simple(kind: PropertyKind) -> Self {
394 Self {
395 kind,
396 args: Vec::new(),
397 }
398 }
399
400 fn new_with_args(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self {
401 Self { kind, args }
402 }
403
404 fn new_with_target(
405 kind: PropertyKind,
406 tcx: TyCtxt<'tcx>,
407 def_id: DefId,
408 exprs: &[Expr],
409 ) -> Self {
410 let args = exprs
411 .first()
412 .map(|expr| Self::parse_target_arg(tcx, def_id, expr))
413 .into_iter()
414 .collect();
415 Self { kind, args }
416 }
417
418 fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool {
419 if expr_len != required_len {
420 panic!("Wrong args length for {:?} Tag!", sp);
421 }
422 true
423 }
424
425 fn parse_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str) -> Ty<'tcx> {
426 let ty_ident_full = access_ident_recursive(expr);
427 if ty_ident_full.is_none() {
428 rap_error!("Incorrect expression for the type of {:?} Tag!", sp);
429 }
430 let ty_ident = ty_ident_full.unwrap().0;
431 let ty = match_ty_with_ident(tcx, def_id, ty_ident);
432 if ty.is_none() {
433 rap_error!("Cannot get type in {:?} Tag!", sp);
434 }
435 ty.unwrap()
436 }
437
438 fn parse_target_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr) -> Option<Ty<'tcx>> {
439 parse_expr_into_local_and_ty(tcx, def_id, expr).map(|(_, _, ty)| ty)
440 }
441
442 fn parse_target_arg(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr) -> PropertyArg<'tcx> {
443 Self::parse_contract_place(tcx, def_id, expr)
444 .map(PropertyArg::Place)
445 .unwrap_or_else(|| {
446 PropertyArg::Expr(Self::parse_contract_expr(tcx, def_id, expr, "target"))
447 })
448 }
449
450 fn parse_contract_expr(
451 tcx: TyCtxt<'tcx>,
452 def_id: DefId,
453 expr: &Expr,
454 sp: &str,
455 ) -> ContractExpr<'tcx> {
456 match expr {
457 Expr::Paren(paren) => Self::parse_contract_expr(tcx, def_id, &paren.expr, sp),
458 Expr::Group(group) => Self::parse_contract_expr(tcx, def_id, &group.expr, sp),
459 Expr::Lit(expr_lit) => match &expr_lit.lit {
460 Lit::Int(lit_int) => lit_int
461 .base10_parse::<u128>()
462 .map(ContractExpr::Const)
463 .unwrap_or(ContractExpr::Unknown),
464 _ => ContractExpr::Unknown,
465 },
466 Expr::Unary(expr_unary) => {
467 let Some(op) = NumericUnaryOp::from_syn(&expr_unary.op) else {
468 return ContractExpr::Unknown;
469 };
470 ContractExpr::Unary {
471 op,
472 expr: Box::new(Self::parse_contract_expr(tcx, def_id, &expr_unary.expr, sp)),
473 }
474 }
475 Expr::Binary(expr_binary) => {
476 let Some(op) = NumericOp::from_syn(&expr_binary.op) else {
477 return ContractExpr::Unknown;
478 };
479 ContractExpr::Binary {
480 op,
481 lhs: Box::new(Self::parse_contract_expr(
482 tcx,
483 def_id,
484 &expr_binary.left,
485 sp,
486 )),
487 rhs: Box::new(Self::parse_contract_expr(
488 tcx,
489 def_id,
490 &expr_binary.right,
491 sp,
492 )),
493 }
494 }
495 _ => {
496 if let Some(place) = Self::parse_contract_place(tcx, def_id, expr) {
497 ContractExpr::Place(place)
498 } else if let Some(value) = parse_expr_into_number(expr) {
499 ContractExpr::new_value(value)
500 } else {
501 rap_debug!(
502 "Numeric expression in {:?} could not be resolved: {:?}",
503 sp,
504 expr
505 );
506 ContractExpr::Unknown
507 }
508 }
509 }
510 }
511
512 fn parse_contract_place(
513 tcx: TyCtxt<'tcx>,
514 def_id: DefId,
515 expr: &Expr,
516 ) -> Option<ContractPlace<'tcx>> {
517 if let Some((base, fields, _ty)) = parse_expr_into_local_and_ty(tcx, def_id, expr) {
518 return Some(ContractPlace::local(base, fields));
519 }
520 Self::parse_arg_place(expr)
521 }
522
523 fn parse_arg_place(expr: &Expr) -> Option<ContractPlace<'tcx>> {
524 if let Expr::Path(expr_path) = expr {
525 if let Some(ident) = expr_path.path.get_ident() {
526 let s = ident.to_string();
527 if let Some(num_str) = s.strip_prefix("Arg_") {
528 if let Ok(idx) = num_str.parse::<usize>() {
529 return Some(ContractPlace::arg(idx));
530 }
531 }
532 }
533 }
534 None
535 }
536
537 fn parse_valid_num(
538 tcx: TyCtxt<'tcx>,
539 def_id: DefId,
540 exprs: &[Expr],
541 ) -> Vec<NumericPredicate<'tcx>> {
542 match exprs {
543 [] => Vec::new(),
544 [expr] => Self::parse_numeric_predicate(tcx, def_id, expr)
545 .into_iter()
546 .collect(),
547 [value, range, ..] => {
548 if let Some(predicates) = Self::parse_interval_predicates(tcx, def_id, value, range)
549 {
550 predicates
551 } else {
552 Self::parse_numeric_predicate(tcx, def_id, value)
553 .into_iter()
554 .collect()
555 }
556 }
557 }
558 }
559
560 fn parse_numeric_predicate(
561 tcx: TyCtxt<'tcx>,
562 def_id: DefId,
563 expr: &Expr,
564 ) -> Option<NumericPredicate<'tcx>> {
565 if let Expr::Binary(expr_binary) = expr {
566 if let Some(op) = RelOp::from_syn(&expr_binary.op) {
567 return Some(NumericPredicate::new(
568 Self::parse_contract_expr(tcx, def_id, &expr_binary.left, "ValidNum"),
569 op,
570 Self::parse_contract_expr(tcx, def_id, &expr_binary.right, "ValidNum"),
571 ));
572 }
573 }
574
575 Some(NumericPredicate::new(
576 Self::parse_contract_expr(tcx, def_id, expr, "ValidNum"),
577 RelOp::Ne,
578 ContractExpr::Const(0),
579 ))
580 }
581
582 fn parse_interval_predicates(
583 tcx: TyCtxt<'tcx>,
584 def_id: DefId,
585 value: &Expr,
586 range: &Expr,
587 ) -> Option<Vec<NumericPredicate<'tcx>>> {
588 match range {
589 Expr::Array(array) if array.elems.len() == 2 => {
590 let mut elems = array.elems.iter();
591 let lower = elems.next().unwrap();
592 let upper = elems.next().unwrap();
593 Some(Self::build_interval_predicates(
594 tcx, def_id, value, lower, true, upper, true,
595 ))
596 }
597 Expr::Lit(expr_lit) => {
598 let Lit::Str(range_lit) = &expr_lit.lit else {
599 return None;
600 };
601 Self::parse_string_interval(tcx, def_id, value, &range_lit.value())
602 }
603 _ => None,
604 }
605 }
606
607 fn parse_string_interval(
608 tcx: TyCtxt<'tcx>,
609 def_id: DefId,
610 value: &Expr,
611 raw_range: &str,
612 ) -> Option<Vec<NumericPredicate<'tcx>>> {
613 let trimmed = raw_range.trim();
614 if trimmed.len() < 5 {
615 return None;
616 }
617
618 let lower_inclusive = trimmed.starts_with('[');
619 let upper_inclusive = trimmed.ends_with(']');
620 if !(lower_inclusive || trimmed.starts_with('('))
621 || !(upper_inclusive || trimmed.ends_with(')'))
622 {
623 return None;
624 }
625
626 let body = &trimmed[1..trimmed.len() - 1];
627 let (lower_raw, upper_raw) = body.split_once(',')?;
628 let lower = safety_parser::syn::parse_str::<Expr>(lower_raw.trim()).ok()?;
629 let upper = safety_parser::syn::parse_str::<Expr>(upper_raw.trim()).ok()?;
630
631 Some(Self::build_interval_predicates(
632 tcx,
633 def_id,
634 value,
635 &lower,
636 lower_inclusive,
637 &upper,
638 upper_inclusive,
639 ))
640 }
641
642 fn build_interval_predicates(
643 tcx: TyCtxt<'tcx>,
644 def_id: DefId,
645 value: &Expr,
646 lower: &Expr,
647 lower_inclusive: bool,
648 upper: &Expr,
649 upper_inclusive: bool,
650 ) -> Vec<NumericPredicate<'tcx>> {
651 let value_expr = Self::parse_contract_expr(tcx, def_id, value, "ValidNum");
652 let lower_expr = Self::parse_contract_expr(tcx, def_id, lower, "ValidNum");
653 let upper_expr = Self::parse_contract_expr(tcx, def_id, upper, "ValidNum");
654 vec![
655 NumericPredicate::new(
656 lower_expr,
657 if lower_inclusive {
658 RelOp::Le
659 } else {
660 RelOp::Lt
661 },
662 value_expr.clone(),
663 ),
664 NumericPredicate::new(
665 value_expr,
666 if upper_inclusive {
667 RelOp::Le
668 } else {
669 RelOp::Lt
670 },
671 upper_expr,
672 ),
673 ]
674 }
675}