rapx/check/senryx/
diagnostics.rs

1//! Diagnostic and result-recording helpers for Senryx contract checks.
2//!
3//! The verifier records passed and failed safety properties per unsafe callsite
4//! so the top-level driver can summarize whether a target function discharged
5//! its unsafe API obligations.
6
7use std::collections::HashSet;
8
9use crate::{
10    analysis::utils::fn_info::{display_hashmap, get_cleaned_def_path_name},
11    check::senryx::visitor::{BodyVisitor, CheckResult},
12};
13use rustc_span::Span;
14
15impl<'tcx> BodyVisitor<'tcx> {
16    /// Record one property-checking result for the current unsafe callsite.
17    pub fn insert_checking_result(
18        &mut self,
19        sp: &str,
20        is_passed: bool,
21        func_name: String,
22        fn_span: Span,
23        idx: usize,
24    ) {
25        if sp == "Unknown" {
26            return;
27        }
28        if is_passed {
29            self.insert_successful_check_result(func_name.clone(), fn_span, idx + 1, sp);
30        } else {
31            self.insert_failed_check_result(func_name.clone(), fn_span, idx + 1, sp);
32        }
33    }
34
35    /// Record one failed safety-property check for an unsafe callsite.
36    pub fn insert_failed_check_result(
37        &mut self,
38        func_name: String,
39        fn_span: Span,
40        idx: usize,
41        sp: &str,
42    ) {
43        if let Some(existing) = self
44            .check_results
45            .iter_mut()
46            .find(|result| result.func_name == func_name && result.func_span == fn_span)
47        {
48            if let Some(passed_set) = existing.passed_contracts.get_mut(&idx) {
49                passed_set.remove(sp);
50                if passed_set.is_empty() {
51                    existing.passed_contracts.remove(&idx);
52                }
53            }
54            existing
55                .failed_contracts
56                .entry(idx)
57                .and_modify(|set| {
58                    set.insert(sp.to_string());
59                })
60                .or_insert_with(|| {
61                    let mut new_set = HashSet::new();
62                    new_set.insert(sp.to_string());
63                    new_set
64                });
65        } else {
66            let mut new_result = CheckResult::new(&func_name, fn_span);
67            new_result
68                .failed_contracts
69                .insert(idx, HashSet::from([sp.to_string()]));
70            self.check_results.push(new_result);
71        }
72    }
73
74    /// Record one successful safety-property check for an unsafe callsite.
75    pub fn insert_successful_check_result(
76        &mut self,
77        func_name: String,
78        fn_span: Span,
79        idx: usize,
80        sp: &str,
81    ) {
82        if let Some(existing) = self
83            .check_results
84            .iter_mut()
85            .find(|result| result.func_name == func_name && result.func_span == fn_span)
86        {
87            if let Some(failed_set) = existing.failed_contracts.get_mut(&idx) {
88                if failed_set.contains(sp) {
89                    return;
90                }
91            }
92
93            existing
94                .passed_contracts
95                .entry(idx)
96                .and_modify(|set| {
97                    set.insert(sp.to_string());
98                })
99                .or_insert_with(|| HashSet::from([sp.to_string()]));
100        } else {
101            let mut new_result = CheckResult::new(&func_name, fn_span);
102            new_result
103                .passed_contracts
104                .insert(idx, HashSet::from([sp.to_string()]));
105            self.check_results.push(new_result);
106        }
107    }
108
109    /// Print graph context when a checker cannot locate a requested node.
110    pub fn show_error_info(&self, arg: usize) {
111        rap_warn!(
112            "In func {:?}, visitor checker error! Can't get {arg} in chain!",
113            get_cleaned_def_path_name(self.tcx, self.def_id)
114        );
115        display_hashmap(&self.chains.variables, 1);
116    }
117}
rapx/check/senryx/diagnostics.rs

rapx/check/senryx/
diagnostics.rs
