rapx/verify/
display.rs

1//! Rendering of contracts, function signatures, and verification results.
2//!
3//! Presentation-only helpers: contract expansion to `(call, meaning)` pairs,
4//! function paths with generic bounds, and grouped result trees with verdicts.
5
6use rustc_hir::def_id::DefId;
7use rustc_middle::ty::ClauseKind;
8use rustc_middle::ty::{self, TyCtxt};
9
10use crate::compat::FxHashMap;
11use crate::helpers::fn_info::get_cons;
12use indexmap::IndexMap;
13
14use super::report::PropertyCheckResult;
15use crate::helpers::mir_scan::CheckpointLocation;
16use crate::verify::contract::render::display_expr_user_friendly;
17
18pub(crate) fn fmt_fn_with_params(path: &str, arg_names: &[String], ret_ty: Option<&str>) -> String {
19    let args = arg_names.join(", ");
20    match ret_ty {
21        Some(ret) => format!("fn {path}({args}) -> {ret}"),
22        None if args.is_empty() => format!("fn {path}"),
23        None => format!("fn {path}({args})"),
24    }
25}
26
27pub(crate) fn fmt_fn_path_with_generics(
28    tcx: rustc_middle::ty::TyCtxt<'_>,
29    def_id: rustc_hir::def_id::DefId,
30) -> String {
31    let path = tcx.def_path_str(def_id);
32    let generics = tcx.generics_of(def_id);
33    let params: Vec<_> = generics
34        .own_params
35        .iter()
36        .map(|p| p.name.to_string())
37        .collect();
38    if params.is_empty() {
39        path
40    } else {
41        format!("{}::<{}>", path, params.join(", "))
42    }
43}
44
45pub(crate) fn fmt_fn_path_with_bounds(tcx: TyCtxt<'_>, def_id: DefId) -> String {
46    let path = tcx.def_path_str(def_id);
47    let predicates = crate::compat::predicates_of(tcx, def_id);
48
49    let mut param_bounds: FxHashMap<String, Vec<String>> = FxHashMap::default();
50
51    macro_rules! collect_bounds {
52        ($iter:expr) => {
53            for (predicate, _span) in $iter {
54                if let ClauseKind::Trait(trait_ref) = predicate.kind().skip_binder() {
55                    let self_ty = trait_ref.self_ty();
56                    if let ty::TyKind::Param(param_ty) = self_ty.kind() {
57                        let param_name = param_ty.name.to_string();
58                        let trait_name = tcx.item_name(trait_ref.def_id()).to_string();
59                        if trait_name != "Sized" {
60                            param_bounds.entry(param_name).or_default().push(trait_name);
61                        }
62                    }
63                }
64            }
65        };
66    }
67
68    #[cfg(not(rapx_ge_100))]
69    {
70        collect_bounds!(predicates.predicates.iter());
71        if let Some(parent_def_id) = predicates.parent {
72            let parent_preds = crate::compat::predicates_of(tcx, parent_def_id);
73            collect_bounds!(parent_preds.predicates.iter());
74        }
75    }
76    #[cfg(rapx_ge_100)]
77    {
78        collect_bounds!(predicates.clauses.iter());
79        if let Some(parent_def_id) = predicates.parent {
80            let parent_preds = crate::compat::predicates_of(tcx, parent_def_id);
81            collect_bounds!(parent_preds.clauses.iter());
82        }
83    }
84
85    if param_bounds.is_empty() {
86        return path;
87    }
88
89    insert_bounds_into_path(&path, &param_bounds)
90}
91
92fn insert_bounds_into_path(path: &str, param_bounds: &FxHashMap<String, Vec<String>>) -> String {
93    let mut result = String::new();
94    let mut remaining = path;
95
96    while let Some(pos) = remaining.find("::<") {
97        result.push_str(&remaining[..pos + 3]);
98        remaining = &remaining[pos + 3..];
99
100        let Some(end) = remaining.find('>') else {
101            result.push_str(remaining);
102            return result;
103        };
104
105        let params_str = &remaining[..end];
106        let params: Vec<&str> = params_str.split(',').map(|s| s.trim()).collect();
107        let mut new_params = Vec::new();
108        let mut has_bounds = false;
109        for p in &params {
110            if let Some(bounds) = param_bounds.get(*p) {
111                new_params.push(format!("{}: {}", p, bounds.join(" + ")));
112                has_bounds = true;
113            } else {
114                new_params.push(p.to_string());
115            }
116        }
117
118        if has_bounds {
119            result.push_str(&new_params.join(", "));
120        } else {
121            result.push_str(params_str);
122        }
123        result.push('>');
124        remaining = &remaining[end + 1..];
125    }
126
127    result.push_str(remaining);
128    result
129}
130
131pub(crate) fn fmt_contract_expanded<'tcx>(
132    tcx: rustc_middle::ty::TyCtxt<'tcx>,
133    property: &crate::verify::contract::Property<'tcx>,
134    struct_def_id: Option<rustc_hir::def_id::DefId>,
135    fn_def_id: Option<rustc_hir::def_id::DefId>,
136) -> (String, String) {
137    use crate::verify::contract::PropertyKind;
138    // Compound `def` (e.g. `Ptr2Ref`, `Deref`, user `pred!`): show it
139    // as a single `name(args)` entry with its doc-derived meaning, instead of
140    // the underlying primitives it expanded into.
141    if let Some(origin) = property.origin() {
142        let meaning = origin.meaning.as_deref().unwrap_or("");
143        return (
144            format!("{}({})", origin.name, origin.args.join(", ")),
145            meaning.to_string(),
146        );
147    }
148    if let crate::verify::contract::Property::Or(or) = property {
149        let disjunct_count = or.disjuncts.len();
150        let mut call_parts = Vec::new();
151        let mut meaning = format!("any of {disjunct_count} alternative(s):\n");
152        for (gi, disjunct) in or.disjuncts.iter().enumerate() {
153            let is_last = gi + 1 == disjunct_count;
154            let branch = if is_last { "`-" } else { "|-" };
155            let (call, m) = fmt_contract_expanded(tcx, disjunct, struct_def_id, fn_def_id);
156            call_parts.push(call);
157            meaning.push_str(&format!("{branch} {}\n", m));
158        }
159        return (
160            format!("Or({})", call_parts.join(", ")),
161            meaning.trim_end().to_string(),
162        );
163    }
164    if let crate::verify::contract::Property::And(and) = property {
165        let mut call_parts = Vec::new();
166        let mut meanings = Vec::new();
167        for conjunct in and.conjuncts.iter() {
168            let (call, m) = fmt_contract_expanded(tcx, conjunct, struct_def_id, fn_def_id);
169            call_parts.push(call);
170            meanings.push(m);
171        }
172        return (
173            format!("And({})", call_parts.join(", ")),
174            meanings.join(" && "),
175        );
176    }
177    let kind = property.kind().expect("atom property");
178    let args: Vec<String> = property
179        .args()
180        .iter()
181        .map(|a| a.display_for_report(tcx, struct_def_id, fn_def_id))
182        .collect();
183    let tag = property
184        .origin()
185        .map(|o| o.name.clone())
186        .unwrap_or_else(|| format!("{:?}", kind));
187    let tag = if property.contract_kind() == crate::verify::contract::ContractKind::Hazard {
188        format!("[hazard] {tag}")
189    } else if property.contract_kind() == crate::verify::contract::ContractKind::Option_ {
190        format!("[option] {tag}")
191    } else {
192        tag
193    };
194    let call = if matches!(kind, PropertyKind::SplitTransmute) {
195        let wrapped: Vec<String> = args.iter().map(|a| format!("[{a}]")).collect();
196        format!("{tag}({})", wrapped.join(", "))
197    } else if matches!(kind, PropertyKind::InBound)
198        && matches!(
199            property.args().first(),
200            Some(crate::verify::contract::PropertyArg::Expr(
201                crate::verify::contract::ContractExpr::IndexAccess { .. }
202            ))
203        )
204    {
205        use crate::verify::contract::{ContractExpr, PropertyArg};
206        if let Some(PropertyArg::Expr(ContractExpr::IndexAccess { slice, index })) =
207            property.args().first()
208        {
209            let (s, i) = fmt_index_access(slice, index, tcx, struct_def_id, fn_def_id);
210            format!("{tag}({s}, {i})")
211        } else {
212            unreachable!()
213        }
214    } else {
215        if matches!(kind, PropertyKind::Alive) && args.len() >= 2 {
216            format!("{tag}({}, '{})", args[0], args[1])
217        } else {
218            format!("{tag}({})", args.join(", "))
219        }
220    };
221    let call = if matches!(kind, PropertyKind::ValidNum)
222        && let Some(crate::verify::contract::PropertyArg::Predicates(preds)) =
223            property.args().first()
224    {
225        let inner = preds
226            .iter()
227            .map(|p| p.display_user_friendly(tcx, struct_def_id, fn_def_id))
228            .collect::<Vec<_>>()
229            .join(", ");
230        format!("{tag}({inner})")
231    } else {
232        call
233    };
234    let meaning = match kind {
235        PropertyKind::InBound => {
236            use crate::verify::contract::{ContractExpr, PropertyArg};
237            let placeholder = format!("InBound({})", args.join(", "));
238            match property.args().first() {
239                Some(PropertyArg::Expr(ContractExpr::IndexAccess { slice, index })) => {
240                    let (s, i) = fmt_index_access(slice, index, tcx, struct_def_id, fn_def_id);
241                    format!("0 <= {i} < {s}.len()")
242                }
243                Some(PropertyArg::Expr(ContractExpr::Place(place))) => {
244                    let ptr = place.display_user_friendly(tcx, struct_def_id, fn_def_id);
245                    let ty = property
246                        .args()
247                        .get(1)
248                        .and_then(|a| match a {
249                            PropertyArg::Ty(ty) => Some(ty.to_string()),
250                            _ => None,
251                        })
252                        .unwrap_or_else(|| "?".to_string());
253                    let cnt = property
254                        .args()
255                        .get(2)
256                        .map(|a| a.display_for_report(tcx, struct_def_id, fn_def_id))
257                        .unwrap_or_else(|| "?".to_string());
258                    format!("same_alloc([{ptr}, {ptr} + sizeof({ty})*{cnt}])")
259                }
260                _ => placeholder,
261            }
262        }
263        PropertyKind::Size => {
264            let ty = args.first().map(|s| s.as_str()).unwrap_or("T");
265            let sz = args.get(1).map(|s| s.as_str()).unwrap_or("1");
266            match sz {
267                "sized" => format!("{ty} is Sized (non-ZST)"),
268                "unsized" => format!("{ty} is !Sized"),
269                n => format!("sizeof({ty}) = {n}"),
270            }
271        }
272        PropertyKind::ValidNum => args.join(" && "),
273        PropertyKind::Alive => {
274            let ptr = args.first().map(|s| s.as_str()).unwrap_or("ptr");
275            if let Some(lt) = args.get(1) {
276                format!("*{ptr} outlives '{lt}")
277            } else {
278                format!("*{ptr} outlives return")
279            }
280        }
281        PropertyKind::Allocated => {
282            let ptr = args.first().map(|s| s.as_str()).unwrap_or("ptr");
283            if args.len() >= 3 {
284                format!(
285                    "{ptr} points to a live allocation of size: size_of({}) * {}",
286                    args[1], args[2]
287                )
288            } else {
289                format!("{ptr} points to a live allocation")
290            }
291        }
292        PropertyKind::NonOverlap => {
293            format!("[{}] are pairwise disjoint memory ranges", args.join(", "))
294        }
295        PropertyKind::Alias => {
296            let p1 = args.first().map(|s| s.as_str()).unwrap_or("p1");
297            let p2 = args.get(1).map(|s| s.as_str()).unwrap_or("p2");
298            format!("{p1} and {p2} alias each other (hazard)")
299        }
300        _ => fmt_meaning_template(crate::verify::contract::spec::kind_meaning(kind), &args),
301    };
302    (call, meaning)
303}
304
305/// Substitute `{0}`, `{1}`, `{2}` placeholders in a meaning template with the
306/// rendered positional arguments.  Missing arguments fall back to `"_"`.
307fn fmt_meaning_template(template: &str, args: &[String]) -> String {
308    let mut out = template.to_string();
309    for i in 0..3 {
310        let value = args.get(i).map(|s| s.as_str()).unwrap_or("_");
311        out = out.replace(&format!("{{{i}}}"), value);
312    }
313    out
314}
315
316/// Drop consecutive duplicate compound-`def` entries: a `def` expands to several
317/// primitives sharing the same origin name and arguments, which should render as
318/// a single `name(args)` line.
319pub(crate) fn dedup_compound_props<'a, 'tcx>(
320    props: impl Iterator<Item = &'a crate::verify::contract::Property<'tcx>>,
321) -> Vec<&'a crate::verify::contract::Property<'tcx>> {
322    let mut out = Vec::new();
323    let mut prev: Option<(String, Vec<String>)> = None;
324    for p in props {
325        if let Some(origin) = p.origin() {
326            let key = (origin.name.clone(), origin.args.clone());
327            if prev.as_ref() == Some(&key) {
328                continue;
329            }
330            prev = Some(key);
331        } else {
332            prev = None;
333        }
334        out.push(p);
335    }
336    out
337}
338
339pub(crate) fn emit_results_counts_and_checkpoints<'tcx>(
340    tcx: TyCtxt<'tcx>,
341    all_results: &[PropertyCheckResult<'tcx>],
342) -> (usize, usize) {
343    use crate::verify::contract::ContractKind;
344    use super::report::CheckResult;
345
346    // Distinguish a *confirmed* violation (`Failed`) from an *incomplete* proof
347    // (`Unknown`).  A `Failed` makes the function UNSOUND; a lone `Unknown`
348    // (e.g. an unannotated unsafe callee) only leaves it UNKNOWN.  Optional
349    // (`Option_`) properties do not take part in the verdict.
350    let failed = all_results
351        .iter()
352        .filter(|r| {
353            r.property.contract_kind() != ContractKind::Option_
354                && r.result == CheckResult::Failed
355        })
356        .count();
357    let unknown = all_results
358        .iter()
359        .filter(|r| {
360            r.property.contract_kind() != ContractKind::Option_
361                && matches!(r.result, CheckResult::Unknown(_))
362        })
363        .count();
364
365    let mut groups: IndexMap<(CheckpointLocation, String), Vec<&PropertyCheckResult<'_>>> =
366        IndexMap::new();
367    for r in all_results {
368        groups
369            .entry((r.checkpoint, r.callee_name.clone()))
370            .or_default()
371            .push(r);
372    }
373
374    let checkpoint_groups: Vec<_> = groups
375        .iter()
376        .filter(|((_, name), _)| !name.starts_with("struct-invariant"))
377        .collect();
378    let invariant_groups: Vec<_> = groups
379        .iter()
380        .filter(|((_, name), _)| name.starts_with("struct-invariant"))
381        .collect();
382
383    if !checkpoint_groups.is_empty() {
384        rap_info!("  --- unsafe checkpoints ---");
385        for ((checkpoint, callee_name), results) in &checkpoint_groups {
386            rap_info!(
387                "      unsafe checkpoint: bb{} -> {callee_name}",
388                checkpoint.block.as_usize(),
389            );
390            emit_property_rows(tcx, results);
391        }
392    }
393
394    if !invariant_groups.is_empty() {
395        rap_info!("  --- struct invariants ---");
396        for ((checkpoint, _), results) in &invariant_groups {
397            rap_info!("      checkpoint bb{}:", checkpoint.block.as_usize());
398            emit_property_rows(tcx, results);
399        }
400    }
401
402    (failed, unknown)
403}
404
405pub(crate) fn emit_verify_summary<'tcx>(
406    tcx: TyCtxt<'tcx>,
407    target_path: &str,
408    def_id: rustc_hir::def_id::DefId,
409    all_results: &[PropertyCheckResult<'tcx>],
410    skip_invariant: bool,
411) {
412    rap_info!("============================================================");
413    rap_info!("[rapx::verify] function: {target_path}");
414    rap_info!("============================================================");
415
416    if skip_invariant {
417        let cons = get_cons(tcx, def_id);
418        for con in &cons {
419            rap_info!("  + constructor: {}", tcx.def_path_str(*con));
420        }
421    }
422
423    emit_results_and_verdict(tcx, all_results);
424    rap_info!("");
425}
426
427pub(crate) fn emit_results_and_verdict<'tcx>(
428    tcx: TyCtxt<'tcx>,
429    all_results: &[PropertyCheckResult<'tcx>],
430) {
431    let (failed, unknown) = emit_results_counts_and_checkpoints(tcx, all_results);
432
433    if failed == 0 && unknown == 0 {
434        rap_info!(green, "  result: SOUND");
435    } else if failed > 0 {
436        rap_warn!("  result: UNSOUND ({failed} failed, {unknown} unknown)");
437    } else {
438        rap_warn!("  result: UNKNOWN ({unknown} unproved)");
439    }
440}
441
442pub(crate) fn emit_property_rows<'tcx>(_tcx: TyCtxt<'tcx>, results: &[&PropertyCheckResult<'tcx>]) {
443    let path_groups: Vec<(&str, Vec<_>)> = {
444        let mut map: FxHashMap<&str, Vec<_>> = FxHashMap::default();
445        for r in results.iter() {
446            map.entry(r.path_description.as_str()).or_default().push(r);
447        }
448        let mut entries: Vec<_> = map.into_iter().collect();
449        entries.sort_by_key(|(desc, _)| desc.matches(',').count());
450        entries
451    };
452    for (path_desc, props) in &path_groups {
453        rap_info!("        path {path_desc}:");
454        // Count identical (kind, origin, hazard, result) groups for dedup.
455        let mut counts: Vec<(
456            Option<crate::verify::contract::PropertyKind>,
457            Option<String>,
458            bool,
459            bool,
460            super::report::CheckResult,
461            usize,
462        )> = Vec::new();
463        for r in props.iter() {
464            let result = r.result.clone();
465            if let Some(on) = r.property.origin().map(|o| o.name.as_str()) {
466                // Compound `def`: one entry per origin name, its primitives
467                // AND-combined into a single verdict (no hazard/option prefix).
468                if let Some(entry) = counts
469                    .iter_mut()
470                    .find(|(_, o, _, _, _, _)| o.as_deref() == Some(on))
471                {
472                    entry.4 = entry.4.clone().and(result);
473                } else {
474                    counts.push((None, Some(on.to_string()), false, false, result, 1usize));
475                }
476            } else {
477                let is_hazard =
478                    r.property.contract_kind() == crate::verify::contract::ContractKind::Hazard;
479                let is_option =
480                    r.property.contract_kind() == crate::verify::contract::ContractKind::Option_;
481                if let Some(entry) = counts.iter_mut().find(|(k, o, h, opt, res, _)| {
482                    *k == r.property.kind()
483                        && o.is_none()
484                        && *h == is_hazard
485                        && *opt == is_option
486                        && *res == result
487                }) {
488                    entry.5 += 1;
489                } else {
490                    counts.push((
491                        r.property.kind(),
492                        None,
493                        is_hazard,
494                        is_option,
495                        result,
496                        1usize,
497                    ));
498                }
499            }
500        }
501        let n = counts.len();
502        for (i, (kind, origin, is_hazard, is_option, result, count)) in counts.iter().enumerate() {
503            let is_last = i + 1 == n;
504            let conn = if n > 1 {
505                if is_last { "└── " } else { "├── " }
506            } else {
507                ""
508            };
509            let name = origin.clone().unwrap_or_else(|| match kind {
510                Some(k) => format!("{k:?}"),
511                None => "Or".to_string(),
512            });
513            let tag = if *is_hazard {
514                format!("[hazard] {name}")
515            } else if *is_option {
516                format!("[option] {name}")
517            } else {
518                name
519            };
520            let mut line = format!("          {conn}{tag} | {}", result.label());
521            if *count > 1 {
522                line.push_str(&format!(" (x{count})"));
523            }
524            if result.is_proved() {
525                rap_info!(green, "{line}");
526            } else {
527                rap_warn!("{line}");
528            }
529        }
530    }
531}
532
533/// Render an `IndexAccess { slice, index }` into `(slice_str, index_str)`,
534/// stripping leading `&mut `/`&` from the slice display.
535fn fmt_index_access<'tcx>(
536    slice: &crate::verify::contract::ContractExpr<'tcx>,
537    index: &crate::verify::contract::ContractExpr<'tcx>,
538    tcx: TyCtxt<'tcx>,
539    struct_def_id: Option<DefId>,
540    fn_def_id: Option<DefId>,
541) -> (String, String) {
542    let mut s = display_expr_user_friendly(slice, tcx, struct_def_id, fn_def_id);
543    s = s.strip_prefix("&mut ").unwrap_or(&s).to_string();
544    s = s.strip_prefix("&").unwrap_or(&s).to_string();
545    let i = display_expr_user_friendly(index, tcx, struct_def_id, fn_def_id);
546    (s, i)
547}
rapx/verify/display.rs

rapx/verify/
display.rs
