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

rapx/verify/contract/
render.rs
