rapx/verify/
display.rs

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

rapx/verify/
display.rs
