rapx 0.7.32

A static analysis platform for Rust program analysis and verification
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

//! Debug and diagnostic display for the symbolic VM.
//!
//! Formats `VmState`, `VmValue`, and related types for human-readable output.

use std::fmt;

use super::state::{VmState, VmValue, ValueInvariants};

impl<'ctx, 'tcx> VmState<'ctx, 'tcx> {
    /// Produce a compact diagnostic summary of the VM state.
    pub fn describe(&self) -> String {
        let mut lines = Vec::new();

        // Locals
        if !self.locals.is_empty() {
            lines.push("-- VM Locals --".to_string());
            for (local, value) in self.locals.iter() {
                lines.push(format!(
                    "  _{}: {:?}",
                    local.as_usize(),
                    value.describe()
                ));
            }
        }

        // Allocations
        if !self.allocations.is_empty() {
            lines.push("-- Allocations --".to_string());
            for alloc in &self.allocations {
                lines.push(format!(
                    "  alloc_{}: base={}, size={}, align={}",
                    alloc.id.0,
                    alloc.base.to_string(),
                    alloc.size.to_string(),
                    alloc.align,
                ));
            }
        }

        // Path conditions
        if !self.path_conditions.is_empty() {
            lines.push(format!(
                "  {} path conditions asserted",
                self.path_conditions.len()
            ));
        }

        // Notes
        if !self.notes.is_empty() {
            lines.push("-- Notes --".to_string());
            for note in &self.notes {
                lines.push(format!("  * {note}"));
            }
        }

        lines.join("\n")
    }
}

impl<'ctx, 'tcx> VmValue<'ctx, 'tcx> {
    /// A compact one-line description of a symbolic value.
    fn describe(&self) -> String {
        let term_str = self.term.to_string();

        let mut flags = Vec::new();
        if self.invariants.non_null {
            flags.push("NN");
        }
        if self.invariants.aligned {
            flags.push("AL");
        }
        if self.invariants.init {
            flags.push("IN");
        }
        if self.invariants.in_bounds {
            flags.push("IB");
        }

        let provenance = self
            .provenance
            .as_ref()
            .map(|p| format!("@alloc{}", p.alloc_id.0))
            .unwrap_or_default();

        if flags.is_empty() {
            format!("{term_str} {provenance}")
        } else {
            format!("{term_str} [{}] {}", flags.join(","), provenance)
        }
    }
}

impl fmt::Display for ValueInvariants {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let mut flags = Vec::new();
        if self.non_null {
            flags.push("non_null");
        }
        if self.aligned {
            flags.push("aligned");
        }
        if self.init {
            flags.push("init");
        }
        if self.in_bounds {
            flags.push("in_bounds");
        }
        write!(f, "{}", flags.join("|"))
    }
}