mirage/cfg/
summary.rs

1//! Natural language summaries of control flow structures
2//!
3//! Distills raw MIR/AST data into compact "Truth Proofs" for LLM consumption.
4
5use crate::cfg::{BasicBlock, BlockKind, Cfg, Path, PathKind, Terminator};
6
7pub struct PathSummarizer;
8
9impl PathSummarizer {
10    /// Generate a compact "Truth Proof" for a sequence of blocks
11    pub fn summarize(blocks: &[BasicBlock]) -> String {
12        if blocks.is_empty() {
13            return "Empty path".to_string();
14        }
15
16        let mut flow = Vec::new();
17        for block in blocks {
18            let summary = Self::summarize_block(block);
19            if !summary.is_empty() {
20                flow.push(summary);
21            }
22        }
23
24        if flow.is_empty() {
25            return "no logical effects".to_string();
26        }
27
28        flow.join(" -> ")
29    }
30
31    /// Distill a single block into its primary logical effects
32    pub fn summarize_block(block: &BasicBlock) -> String {
33        let mut effects = Vec::new();
34
35        // 1. Add Entry/Exit markers
36        match block.kind {
37            BlockKind::Entry => effects.push("[Entry]".to_string()),
38            BlockKind::Exit => {}
39            BlockKind::Normal => {}
40        }
41
42        // 2. Filter and distill statements
43        for stmt in &block.statements {
44            if let Some(distilled) = Self::distill_statement(stmt) {
45                effects.push(distilled);
46            }
47        }
48
49        // 3. Add terminator effect
50        match &block.terminator {
51            Terminator::Return => effects.push("[Return]".to_string()),
52            Terminator::Abort(msg) => effects.push(format!("[Abort: {}]", msg)),
53            Terminator::Unreachable => effects.push("[Unreachable]".to_string()),
54            _ => {}
55        }
56
57        effects.join(" -> ")
58    }
59
60    fn distill_statement(stmt: &str) -> Option<String> {
61        // Noise filters for MIR bookkeeping statements
62        if stmt.contains("StorageLive")
63            || stmt.contains("StorageDead")
64            || stmt.contains("Nop")
65            || stmt.contains("FakeRead")
66        {
67            return None;
68        }
69
70        let stmt = stmt.trim();
71
72        // 1. Call Signal: Extracts function action regardless of assignment
73        // Prefer Call signals as they represent primary actions
74        if let Some(call_start) = stmt.find("Call(") {
75            let inner = &stmt[call_start + 5..];
76            let mut depth = 0;
77            let mut end = None;
78            for (i, c) in inner.char_indices() {
79                match c {
80                    '(' => depth += 1,
81                    ')' => {
82                        if depth == 0 {
83                            end = Some(i);
84                            break;
85                        }
86                        depth -= 1;
87                    }
88                    ',' if depth == 0 => {
89                        end = Some(i);
90                        break;
91                    }
92                    _ => {}
93                }
94            }
95            if let Some(e) = end {
96                return Some(format!("[Call: {}]", inner[..e].trim()));
97            }
98        }
99
100        // 2. State Signal: Extracts assignments like Local(1) = 42
101        if stmt.starts_with("Assign(") && stmt.ends_with(')') {
102            let inner = &stmt[7..stmt.len() - 1];
103            let mut depth = 0;
104            let mut comma_pos = None;
105
106            for (i, c) in inner.char_indices() {
107                match c {
108                    '(' | '[' => depth += 1,
109                    ')' | ']' => depth -= 1,
110                    ',' if depth == 0 => {
111                        comma_pos = Some(i);
112                        break;
113                    }
114                    _ => {}
115                }
116            }
117
118            if let Some(pos) = comma_pos {
119                let lhs = inner[..pos].trim();
120                let rhs = inner[pos + 1..].trim();
121
122                // Clean up RHS: Constant(42) -> 42
123                let rhs_display = if rhs.starts_with("Constant(") && rhs.ends_with(')') {
124                    &rhs[9..rhs.len() - 1].trim()
125                } else {
126                    rhs
127                };
128
129                return Some(format!("[State: {} = {}]", lhs, rhs_display));
130            }
131        }
132
133        None
134    }
135}
136
137/// Legacy compatible entry point that uses the new summarization logic
138pub fn summarize_path(cfg: &Cfg, path: &Path) -> String {
139    let mut blocks = Vec::new();
140    for &bid in &path.blocks {
141        if let Some(node_idx) = cfg.node_indices().find(|&n| cfg[n].id == bid) {
142            blocks.push(cfg[node_idx].clone());
143        }
144    }
145
146    let summary = PathSummarizer::summarize(&blocks);
147
148    match path.kind {
149        PathKind::Normal => format!("{} ({} blocks)", summary, path.len()),
150        PathKind::Error => format!("{} -> error ({} blocks)", summary, path.len()),
151        PathKind::Degenerate => format!("{} -> dead end ({} blocks)", summary, path.len()),
152        PathKind::Unreachable => format!("Unreachable: {} ({} blocks)", summary, path.len()),
153    }
154}
mirage/cfg/summary.rs

mirage/cfg/
summary.rs
