rapx/verify/vm/
display.rs

1//! Debug and diagnostic display for the symbolic VM.
2//!
3//! Formats `VmState`, `VmValue`, and related types for human-readable output.
4
5use std::fmt;
6
7use super::state::{VmState, VmValue, ValueInvariants};
8
9impl<'ctx, 'tcx> VmState<'ctx, 'tcx> {
10    /// Produce a compact diagnostic summary of the VM state.
11    pub fn describe(&self) -> String {
12        let mut lines = Vec::new();
13
14        // Locals
15        if !self.locals.is_empty() {
16            lines.push("-- VM Locals --".to_string());
17            for (local, value) in self.locals.iter() {
18                lines.push(format!(
19                    "  _{}: {:?}",
20                    local.as_usize(),
21                    value.describe()
22                ));
23            }
24        }
25
26        // Allocations
27        if !self.allocations.is_empty() {
28            lines.push("-- Allocations --".to_string());
29            for (idx, alloc) in self.allocations.iter().enumerate() {
30                lines.push(format!(
31                    "  alloc_{}: base={}, size={}, align={}",
32                    idx,
33                    alloc.base.to_string(),
34                    alloc.size.to_string(),
35                    alloc.align,
36                ));
37            }
38        }
39
40        // Path conditions
41        if !self.path_conditions.is_empty() {
42            lines.push(format!(
43                "  {} path conditions asserted",
44                self.path_conditions.len()
45            ));
46        }
47
48        // Notes
49        if !self.notes.is_empty() {
50            lines.push("-- Notes --".to_string());
51            for note in &self.notes {
52                lines.push(format!("  * {note}"));
53            }
54        }
55
56        lines.join("\n")
57    }
58}
59
60impl<'ctx, 'tcx> VmValue<'ctx, 'tcx> {
61    /// A compact one-line description of a symbolic value.
62    fn describe(&self) -> String {
63        let term_str = self.term.to_string();
64
65        let mut flags = Vec::new();
66        if self.invariants.non_null {
67            flags.push("NN");
68        }
69        if self.invariants.aligned {
70            flags.push("AL");
71        }
72        if self.invariants.init {
73            flags.push("IN");
74        }
75        if self.invariants.in_bounds {
76            flags.push("IB");
77        }
78
79        let provenance = self
80            .provenance
81            .as_ref()
82            .map(|p| format!("@alloc{}", p.alloc_id.0))
83            .unwrap_or_default();
84
85        if flags.is_empty() {
86            format!("{term_str} {provenance}")
87        } else {
88            format!("{term_str} [{}] {}", flags.join(","), provenance)
89        }
90    }
91}
92
93impl fmt::Display for ValueInvariants {
94    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
95        let mut flags = Vec::new();
96        if self.non_null {
97            flags.push("non_null");
98        }
99        if self.aligned {
100            flags.push("aligned");
101        }
102        if self.init {
103            flags.push("init");
104        }
105        if self.in_bounds {
106            flags.push("in_bounds");
107        }
108        write!(f, "{}", flags.join("|"))
109    }
110}
rapx/verify/vm/display.rs

rapx/verify/vm/
display.rs
