rapx/verify/contract/
render.rs

1//! User-facing rendering of contract data structures.
2//!
3//! Converts `ContractPlace`, `ContractExpr`, `NumericPredicate`, `PropertyArg`
4//! and `Property` into readable strings for reports and debug output.  Kept
5//! separate from the data model (`types.rs`) so the model stays
6//! presentation-free.
7
8use rustc_hir::def_id::DefId;
9use rustc_middle::ty::TyCtxt;
10
11use super::types::{
12    ContractExpr, ContractPlace, ContractProjection, NumericBinOp, NumericPredicate,
13    NumericUnaryOp, PlaceBase, Property, PropertyArg, PropertyKind, RelOp,
14};
15
16/// Best-effort source snippet for a MIR local's declaration, if its function
17/// MIR is available and the local index is in range.
18fn local_snippet<'tcx>(
19    tcx: TyCtxt<'tcx>,
20    fn_def_id: Option<DefId>,
21    mir_local: usize,
22) -> Option<String> {
23    let fn_def_id = fn_def_id?;
24    if !tcx.is_mir_available(fn_def_id) {
25        return None;
26    }
27    let body = tcx.optimized_mir(fn_def_id);
28    if mir_local >= body.local_decls.len() {
29        return None;
30    }
31    let local = rustc_middle::mir::Local::from_usize(mir_local);
32    let span = body.local_decls[local].source_info.span;
33    tcx.sess.source_map().span_to_snippet(span).ok()
34}
35
36impl<'tcx> ContractPlace<'tcx> {
37    pub(crate) fn display_user_friendly(
38        &self,
39        tcx: TyCtxt<'tcx>,
40        struct_def_id: Option<DefId>,
41        fn_def_id: Option<DefId>,
42    ) -> String {
43        let has_projections = !self.projections.is_empty();
44
45        let base_str = match self.base {
46            PlaceBase::Return => {
47                if has_projections {
48                    String::new()
49                } else {
50                    "return".to_string()
51                }
52            }
53            PlaceBase::Arg(idx) => local_snippet(tcx, fn_def_id, idx + 1)
54                .filter(|s| !s.is_empty())
55                .unwrap_or_else(|| format!("arg{}", idx)),
56            PlaceBase::Local(n) => {
57                if n == 0 {
58                    "return".to_string()
59                } else {
60                    local_snippet(tcx, fn_def_id, n).unwrap_or_else(|| format!("arg{}", n))
61                }
62            }
63        };
64
65        let base_str = base_str
66            .strip_prefix("&mut ")
67            .unwrap_or(&base_str)
68            .to_string();
69        let base_str = base_str.strip_prefix("&").unwrap_or(&base_str).to_string();
70
71        if self.projections.is_empty() {
72            return base_str;
73        }
74
75        let mut result = base_str;
76        for projection in &self.projections {
77            match projection {
78                ContractProjection::Field { index, ty: _ } => {
79                    let field_name =
80                        crate::helpers::name::resolve_field_name(tcx, index, struct_def_id);
81                    if result.is_empty() {
82                        result = field_name;
83                    } else {
84                        result.push_str(&format!(".{}", field_name));
85                    }
86                }
87                ContractProjection::Downcast { .. } => {
88                    result.push_str(".unwrap_some()");
89                }
90                ContractProjection::ForEach => {
91                    result.push_str(".iter()");
92                }
93            }
94        }
95        result
96    }
97}
98
99impl<'tcx> NumericPredicate<'tcx> {
100    pub(crate) fn display_user_friendly(
101        &self,
102        tcx: TyCtxt<'tcx>,
103        struct_def_id: Option<DefId>,
104        fn_def_id: Option<DefId>,
105    ) -> String {
106        let op_str = match self.op {
107            RelOp::Eq => "==",
108            RelOp::Ne => "!=",
109            RelOp::Lt => "<",
110            RelOp::Le => "<=",
111            RelOp::Gt => ">",
112            RelOp::Ge => ">=",
113        };
114        format!(
115            "{} {} {}",
116            display_expr_user_friendly(&self.lhs, tcx, struct_def_id, fn_def_id),
117            op_str,
118            display_expr_user_friendly(&self.rhs, tcx, struct_def_id, fn_def_id),
119        )
120    }
121}
122
123pub(crate) fn display_expr_user_friendly<'tcx>(
124    expr: &ContractExpr<'tcx>,
125    tcx: TyCtxt<'tcx>,
126    struct_def_id: Option<DefId>,
127    fn_def_id: Option<DefId>,
128) -> String {
129    match expr {
130        ContractExpr::Const(n) => format!("{n}"),
131        ContractExpr::ConstParam { name, .. } => name.clone(),
132        ContractExpr::Place(p) => p.display_user_friendly(tcx, struct_def_id, fn_def_id),
133        ContractExpr::SizeOf(ty) => format!("size_of({ty})"),
134        ContractExpr::AlignOf(ty) => format!("align_of({ty})"),
135        ContractExpr::Len(e) => {
136            format!(
137                "len({})",
138                display_expr_user_friendly(e, tcx, struct_def_id, fn_def_id)
139            )
140        }
141        ContractExpr::IndexAccess { slice, index } => {
142            format!(
143                "{}[{}]",
144                display_expr_user_friendly(slice, tcx, struct_def_id, fn_def_id),
145                display_expr_user_friendly(index, tcx, struct_def_id, fn_def_id),
146            )
147        }
148        ContractExpr::Binary { op, lhs, rhs } => {
149            let lhs_str = display_expr_user_friendly(lhs, tcx, struct_def_id, fn_def_id);
150            let rhs_str = display_expr_user_friendly(rhs, tcx, struct_def_id, fn_def_id);
151            let op_str = match op {
152                NumericBinOp::Min => return format!("min({lhs_str}, {rhs_str})"),
153                NumericBinOp::Max => return format!("max({lhs_str}, {rhs_str})"),
154                NumericBinOp::Add => "+",
155                NumericBinOp::Sub => "-",
156                NumericBinOp::Mul => "*",
157                NumericBinOp::Div => "/",
158                NumericBinOp::Rem => "%",
159                NumericBinOp::BitAnd => "&",
160                NumericBinOp::BitOr => "|",
161                NumericBinOp::BitXor => "^",
162            };
163            format!("{lhs_str} {op_str} {rhs_str}")
164        }
165        ContractExpr::Unary { op, expr } => {
166            let op_str = match op {
167                NumericUnaryOp::Not => "!",
168                NumericUnaryOp::Neg => "-",
169            };
170            format!(
171                "{}{}",
172                op_str,
173                display_expr_user_friendly(expr, tcx, struct_def_id, fn_def_id),
174            )
175        }
176        ContractExpr::If {
177            cond,
178            then_expr,
179            else_expr,
180        } => {
181            format!(
182                "if {} {{ {} }} else {{ {} }}",
183                cond.display_user_friendly(tcx, struct_def_id, fn_def_id),
184                display_expr_user_friendly(then_expr, tcx, struct_def_id, fn_def_id),
185                display_expr_user_friendly(else_expr, tcx, struct_def_id, fn_def_id),
186            )
187        }
188        _ => format!("{:?}", expr),
189    }
190}
191
192impl<'tcx> PropertyArg<'tcx> {
193    pub(crate) fn display_for_report(
194        &self,
195        tcx: TyCtxt<'tcx>,
196        struct_def_id: Option<DefId>,
197        fn_def_id: Option<DefId>,
198    ) -> String {
199        match self {
200            PropertyArg::Ty(ty) => format!("{}", ty),
201            PropertyArg::Expr(expr) => {
202                display_expr_user_friendly(expr, tcx, struct_def_id, fn_def_id)
203            }
204            PropertyArg::Predicates(preds) => {
205                let p: Vec<_> = preds
206                    .iter()
207                    .map(|pred| pred.display_user_friendly(tcx, struct_def_id, fn_def_id))
208                    .collect();
209                p.join(" && ")
210            }
211            PropertyArg::Ident(s) => s.clone(),
212            PropertyArg::Region(r) => format!("'{r}"),
213        }
214    }
215}
216
217impl<'tcx> Property<'tcx> {
218    pub(crate) fn display_for_report(
219        &self,
220        tcx: TyCtxt<'tcx>,
221        struct_def_id: Option<DefId>,
222        fn_def_id: Option<DefId>,
223    ) -> String {
224        // Compound property (e.g. `Ptr2Ref`, `Deref`, user `pred!`): show
225        // it as a single `name(args)` entry instead of its underlying primitives.
226        if let Some(origin) = self.origin() {
227            return format!("{}({})", origin.name, origin.args.join(", "));
228        }
229
230        let kind_str = match self.kind() {
231            Some(k) => format!("{k:?}"),
232            None => {
233                if self.is_and() {
234                    "And".to_string()
235                } else {
236                    "Or".to_string()
237                }
238            }
239        };
240
241        if matches!(self.kind(), Some(PropertyKind::InBound))
242            && matches!(
243                self.args().first(),
244                Some(PropertyArg::Expr(ContractExpr::IndexAccess { .. }))
245            )
246        {
247            if let Some(PropertyArg::Expr(ContractExpr::IndexAccess { slice, index })) =
248                self.args().first()
249            {
250                let slice_str = display_expr_user_friendly(slice, tcx, struct_def_id, fn_def_id);
251                let index_str = display_expr_user_friendly(index, tcx, struct_def_id, fn_def_id);
252                return format!("{}({}, {})", kind_str, slice_str, index_str);
253            }
254        }
255
256        if matches!(self.kind(), Some(PropertyKind::ValidNum))
257            && let Some(PropertyArg::Predicates(preds)) = self.args().first()
258        {
259            let inner: Vec<String> = preds
260                .iter()
261                .map(|pred| pred.display_user_friendly(tcx, struct_def_id, fn_def_id))
262                .collect();
263            if inner.is_empty() {
264                return format!("{}", kind_str);
265            }
266            return format!("{}({})", kind_str, inner.join(", "));
267        }
268
269        let args: Vec<String> = self
270            .args()
271            .iter()
272            .map(|arg| arg.display_for_report(tcx, struct_def_id, fn_def_id))
273            .collect();
274        if args.is_empty() {
275            kind_str
276        } else {
277            format!("{}({})", kind_str, args.join(", "))
278        }
279    }
280}
rapx/verify/contract/render.rs

rapx/verify/contract/
render.rs
