rapx 0.7.1

A static analysis platform for use-after-free, memory leakage detection, etc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

//! Diagnostics and summaries for the staged verifier pipeline.
//!
//! The driver and later checking stages report their per-path property results
//! through the types in this module.  Keeping these types here leaves the driver
//! focused on orchestration.

use rustc_hir::def_id::DefId;

use super::{contract::Property, helpers::CallsiteLocation};

/// Verification status for one required property on one path.
#[derive(Clone, Debug)]
pub enum CheckResult {
    /// The property has been proved for this path.
    Proved,
    /// The verifier found a possible violation for this path.
    Failed,
    /// The verifier has not implemented or completed the proof for this path.
    Unknown,
}

/// Result for one required property along one path to a callsite.
#[derive(Clone, Debug)]
pub struct PropertyCheckResult<'tcx> {
    /// Unsafe callsite being checked.
    pub callsite: CallsiteLocation,
    /// Index of the callsite in the function-level callsite list.
    pub callsite_index: usize,
    /// Index of the path in the callsite path set.
    pub path_index: usize,
    /// Index of the property in the callsite-level property list.
    pub property_index: usize,
    /// Required property checked on this path.
    pub property: Property<'tcx>,
    /// Current verification status.
    pub result: CheckResult,
    /// Optional path-local diagnostics generated by the staged visitors.
    pub diagnostics: Option<VisitDiagnostics>,
    /// Human-readable path description.
    pub path_description: String,
    /// Callee name for this callsite.
    pub callee_name: String,
}

/// Human-readable diagnostics emitted for one path/property check.
#[derive(Clone, Debug)]
pub struct VisitDiagnostics {
    /// Backward visit summary for relevant MIR items.
    pub backward: String,
    /// Forward visit summary for abstract facts collected from those items.
    pub forward: String,
}

impl VisitDiagnostics {
    /// Create diagnostics from backward and forward visitor summaries.
    pub fn new(backward: String, forward: String) -> Self {
        Self { backward, forward }
    }
}

/// Verification report for one function target.
#[derive(Clone, Debug)]
pub struct VerificationReport<'tcx> {
    /// Function that was verified.
    pub function: DefId,
    /// Per-path property results emitted by the verifier.
    pub results: Vec<PropertyCheckResult<'tcx>>,
}

impl<'tcx> VerificationReport<'tcx> {
    /// Create an empty report for a function target.
    pub fn new(function: DefId) -> Self {
        Self {
            function,
            results: Vec::new(),
        }
    }

    /// Add one path/property check result to this report.
    pub fn push(&mut self, result: PropertyCheckResult<'tcx>) {
        self.results.push(result);
    }

    /// Return the number of check results in this report.
    pub fn len(&self) -> usize {
        self.results.len()
    }

    /// Return true when this report contains no check results.
    pub fn is_empty(&self) -> bool {
        self.results.is_empty()
    }

    /// Render the whole report as a readable multi-line diagnostic.
    pub fn describe(&self) -> String {
        let mut out = String::new();
        out.push_str(&format!(
            "[rapx::verify::diagnostics] function {:?}: {} check item(s)\n",
            self.function,
            self.results.len()
        ));

        for (index, result) in self.results.iter().enumerate() {
            out.push_str(&format!(
                "  check #{index}: callsite #{}, bb{}, path #{}, property #{} {:?}, result {:?}\n",
                result.callsite_index,
                result.callsite.block.as_usize(),
                result.path_index,
                result.property_index,
                result.property.kind,
                result.result
            ));

            if let Some(diagnostics) = &result.diagnostics {
                out.push_str(&diagnostics.backward);
                if !diagnostics.backward.ends_with('\n') {
                    out.push('\n');
                }
                out.push_str(&diagnostics.forward);
                if !diagnostics.forward.ends_with('\n') {
                    out.push('\n');
                }
            }
        }

        out
    }
}