Skip to content

Commit 64753f4

Browse files
committed
[anneal][v2] Add DiagnosticMapper to map compiler errors back to Rust source code
TAG=agy gherrit-pr-id: Gzq7escrh5c2qcrgidomnfaxbsi6xn7yu
1 parent 26c45cf commit 64753f4

1 file changed

Lines changed: 335 additions & 0 deletions

File tree

anneal/v2/src/diagnostics.rs

Lines changed: 335 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,335 @@
1+
// Copyright 2026 The Fuchsia Authors
2+
//
3+
// Licensed under the 2-Clause BSD License <LICENSE-BSD or
4+
// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
5+
// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
6+
// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
7+
// This file may not be copied, modified, or distributed except according to
8+
// those terms.
9+
10+
// Handling of Lean diagnostics and error mapping.
11+
//
12+
// This module provides the [`crate::diagnostics::DiagnosticMapper`] struct, which is responsible
13+
// for translating diagnostics from external tools (like Lean or Charon) back
14+
// to the original Rust source code. It maps errors in generated files back to
15+
// their origin spans in the user's codebase.
16+
17+
pub use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel, DiagnosticSpan};
18+
19+
/// Maps diagnostics from generated intermediate code back to pristine,
20+
/// original source code files.
21+
///
22+
/// Lean has no knowledge of the Rust files that orchestrated its execution.
23+
/// It only reports errors against the generated `.lean` artifact files.
24+
///
25+
/// To create a first-class user experience, this mapper actively
26+
/// cross-references Lean's emitted byte spans against the sidecar
27+
/// `SourceMapping`s built by `src/generate.rs`, dynamically synthesizing a
28+
/// [`miette::NamedSource`] that points directly into the user's actual `.rs`
29+
/// workspace files.
30+
pub struct DiagnosticMapper {
31+
user_root: std::path::PathBuf,
32+
user_root_canonical: std::path::PathBuf,
33+
source_cache: std::collections::HashMap<std::path::PathBuf, String>,
34+
}
35+
36+
#[derive(thiserror::Error, Debug)]
37+
#[error("{message}")]
38+
struct MappedError {
39+
message: String,
40+
src: miette::NamedSource<String>,
41+
labels: Vec<miette::LabeledSpan>,
42+
help: Option<String>,
43+
related: Vec<MappedError>,
44+
severity: Option<miette::Severity>,
45+
}
46+
47+
impl miette::Diagnostic for MappedError {
48+
fn source_code(&self) -> Option<&dyn miette::SourceCode> {
49+
Some(&self.src)
50+
}
51+
52+
fn labels(&self) -> Option<Box<dyn std::iter::Iterator<Item = miette::LabeledSpan> + '_>> {
53+
if self.labels.is_empty() { None } else { Some(Box::new(self.labels.iter().cloned())) }
54+
}
55+
56+
fn help(&self) -> Option<Box<dyn std::fmt::Display + '_>> {
57+
self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
58+
}
59+
60+
fn related<'a>(
61+
&'a self,
62+
) -> Option<Box<dyn std::iter::Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
63+
if self.related.is_empty() {
64+
None
65+
} else {
66+
let iter = self.related.iter().map(|e| e as &dyn miette::Diagnostic);
67+
Some(Box::new(iter))
68+
}
69+
}
70+
71+
fn severity(&self) -> Option<miette::Severity> {
72+
self.severity
73+
}
74+
}
75+
76+
impl DiagnosticMapper {
77+
/// Creates a new mapper rooted at `user_root`.
78+
pub fn new(user_root: std::path::PathBuf) -> Self {
79+
let user_root_canonical =
80+
std::fs::canonicalize(&user_root).unwrap_or_else(|_| user_root.clone());
81+
Self { user_root, user_root_canonical, source_cache: std::collections::HashMap::new() }
82+
}
83+
84+
/// Resolves a path relative to the user root, if applicable.
85+
///
86+
/// This ensures we only report diagnostics for files within the user's
87+
/// workspace, avoiding noise from dependencies or system files.
88+
pub fn map_path(&self, path: &std::path::Path) -> Option<std::path::PathBuf> {
89+
let mut p = path.to_path_buf();
90+
if p.is_relative() {
91+
p = self.user_root.join(p);
92+
}
93+
94+
p = {
95+
let mut normalized = std::path::PathBuf::new();
96+
for component in p.components() {
97+
let most_recent = normalized.components().next_back();
98+
match (component, most_recent) {
99+
(std::path::Component::ParentDir, Some(std::path::Component::Normal(_))) => {
100+
normalized.pop();
101+
}
102+
(std::path::Component::CurDir, _) => {}
103+
_ => normalized.push(component),
104+
}
105+
}
106+
normalized
107+
};
108+
109+
// Strategy B: Starts with user_root or user_root_canonical.
110+
(p.starts_with(&self.user_root) || p.starts_with(&self.user_root_canonical)).then_some(p)
111+
}
112+
113+
fn get_source(&mut self, path: &std::path::Path) -> Option<String> {
114+
if let Some(src) = self.source_cache.get(path) {
115+
return Some(src.clone());
116+
}
117+
if let Ok(src) = std::fs::read_to_string(path) {
118+
self.source_cache.insert(path.to_path_buf(), src.clone());
119+
Some(src)
120+
} else {
121+
None
122+
}
123+
}
124+
125+
/// Renders a diagnostic (from Cargo or Charon) using `miette`.
126+
///
127+
/// This is strictly for rendering errors native to Rust processing (where
128+
/// the structured error originates from our `syn` parser or Charon's
129+
/// processing), bringing them into a unified, colorized `miette` format.
130+
pub fn render_miette<F>(&mut self, diag: &Diagnostic, mut printer: F)
131+
where
132+
F: FnMut(String),
133+
{
134+
let mut mapped_paths_and_spans: std::collections::HashMap<
135+
std::path::PathBuf,
136+
Vec<&DiagnosticSpan>,
137+
> = std::collections::HashMap::new();
138+
139+
// 1) Group spans by mapped path.
140+
for s in &diag.spans {
141+
let p = std::path::PathBuf::from(&s.file_name);
142+
if let Some(mapped_path) = self.map_path(&p) {
143+
mapped_paths_and_spans.entry(mapped_path).or_default().push(s);
144+
}
145+
}
146+
147+
// TODO: Should we be collecting all of them, not just the first?
148+
let help_msg = diag
149+
.children
150+
.iter()
151+
.find(|child| child.level == DiagnosticLevel::Help)
152+
.map(|child| child.message.clone());
153+
154+
if !mapped_paths_and_spans.is_empty() {
155+
// Find the path that contains the primary span, or just take the
156+
// first one.
157+
let primary_path = diag
158+
.spans
159+
.iter()
160+
.find(|s| s.is_primary)
161+
.and_then(|s| self.map_path(&std::path::PathBuf::from(&s.file_name)))
162+
.or_else(|| mapped_paths_and_spans.keys().next().cloned());
163+
164+
if let Some(main_path) = primary_path {
165+
let mut all_errors = Vec::new();
166+
167+
// Sort the paths to have the primary path first.
168+
let mut paths: Vec<std::path::PathBuf> =
169+
mapped_paths_and_spans.keys().cloned().collect();
170+
paths.sort_by_key(|p| p != &main_path);
171+
172+
for p in paths {
173+
if let Some(src) = self.get_source(&p) {
174+
let labels: Vec<_> = mapped_paths_and_spans
175+
.get(&p)
176+
.unwrap()
177+
.iter()
178+
.filter_map(|s| {
179+
let label_text = s.label.clone().unwrap_or_default();
180+
let start: usize = s.byte_start.try_into().unwrap();
181+
let len = (s.byte_end - s.byte_start).try_into().unwrap();
182+
(start <= src.len() && start + len <= src.len()).then(|| {
183+
let offset = miette::SourceOffset::from(start);
184+
miette::LabeledSpan::new(Some(label_text), offset.offset(), len)
185+
})
186+
})
187+
.collect();
188+
189+
let err = MappedError {
190+
message: if p == main_path {
191+
diag.message.clone()
192+
} else {
193+
format!("related to: {}", p.display())
194+
},
195+
src: miette::NamedSource::new(p.to_string_lossy(), src),
196+
labels,
197+
help: if p == main_path { help_msg.clone() } else { None },
198+
related: Vec::new(),
199+
severity: match diag.level {
200+
DiagnosticLevel::Error | DiagnosticLevel::Ice => {
201+
Some(miette::Severity::Error)
202+
}
203+
DiagnosticLevel::Warning => Some(miette::Severity::Warning),
204+
_ => Some(miette::Severity::Advice),
205+
},
206+
};
207+
all_errors.push(err);
208+
}
209+
}
210+
211+
if !all_errors.is_empty() {
212+
let mut main_err = all_errors.remove(0);
213+
main_err.related = all_errors;
214+
printer(format!("{:?}", miette::Report::new(main_err)));
215+
return;
216+
}
217+
}
218+
}
219+
220+
// If we get here, no span was successfully mapped.
221+
let prefix = match diag.level {
222+
DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
223+
DiagnosticLevel::Warning => "[External Warning]",
224+
_ => "[External Info]",
225+
};
226+
227+
if let Some(span) = diag.spans.first() {
228+
printer(format!("{} {}:{}: {}", prefix, span.file_name, span.line_start, diag.message));
229+
} else {
230+
printer(format!("{} {}", prefix, diag.message));
231+
}
232+
}
233+
234+
/// Renders a diagnostic (e.g., from Lean) directly at a mapped byte
235+
/// range.
236+
///
237+
/// The fundamental workflow for an external error is:
238+
/// 1. Lean encounters a verification failure and emits a JSON line
239+
/// containing its local start/end bytes in the `.lean` artifact.
240+
/// 2. Anneal checks the cached `SourceMapping` array for that artifact,
241+
/// and discovers exactly where the Lean bytes translate back to Rust
242+
/// bytes.
243+
/// 3. Anneal calls this method to print the error onto the Rust file
244+
/// canvas.
245+
pub fn render_raw<F>(
246+
&mut self,
247+
file_name: &str,
248+
message: String,
249+
level: DiagnosticLevel,
250+
byte_start: usize,
251+
byte_end: usize,
252+
mut printer: F,
253+
) where
254+
F: FnMut(String),
255+
{
256+
let p = std::path::PathBuf::from(file_name);
257+
if let Some(mapped_path) = self.map_path(&p)
258+
&& let Some(src) = self.get_source(&mapped_path)
259+
{
260+
let start = byte_start;
261+
if byte_end >= start {
262+
let len = byte_end - start;
263+
if start <= src.len() && start + len <= src.len() {
264+
let offset = miette::SourceOffset::from(start);
265+
let label =
266+
miette::LabeledSpan::new(Some("here".to_string()), offset.offset(), len);
267+
let err = MappedError {
268+
message,
269+
src: miette::NamedSource::new(mapped_path.to_string_lossy(), src),
270+
labels: vec![label],
271+
help: None,
272+
related: Vec::new(),
273+
severity: match level {
274+
DiagnosticLevel::Error | DiagnosticLevel::Ice => {
275+
Some(miette::Severity::Error)
276+
}
277+
DiagnosticLevel::Warning => Some(miette::Severity::Warning),
278+
_ => Some(miette::Severity::Advice),
279+
},
280+
};
281+
printer(format!("{:?}", miette::Report::new(err)));
282+
return;
283+
}
284+
}
285+
}
286+
287+
// Fallback.
288+
let prefix = match level {
289+
DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
290+
DiagnosticLevel::Warning => "[External Warning]",
291+
_ => "[External Info]",
292+
};
293+
printer(format!("{} {}: {}", prefix, file_name, message));
294+
}
295+
}
296+
297+
#[cfg(test)]
298+
mod tests {
299+
use super::*;
300+
301+
#[test]
302+
fn test_map_path_traversal() {
303+
let temp = tempfile::tempdir().unwrap();
304+
let user_root = temp.path().join("workspace");
305+
std::fs::create_dir(&user_root).unwrap();
306+
307+
// Create a symlink in the workspace pointing outside.
308+
let outside = temp.path().join("outside");
309+
std::fs::create_dir(&outside).unwrap();
310+
std::os::unix::fs::symlink(&outside, user_root.join("symlink")).unwrap();
311+
312+
let mapper = DiagnosticMapper::new(user_root.clone());
313+
314+
let malicious_path = user_root.join("symlink/../passwd");
315+
316+
let mapped = mapper.map_path(&malicious_path);
317+
318+
// The path normalization routine relies on lexical analysis. It
319+
// normalizes `workspace/symlink/../passwd` into `workspace/passwd`.
320+
// Even though a physical resolution of this path would point to
321+
// `outside/passwd` via the symlink, the lexical flattening grounds it
322+
// back into the workspace root. Because the mapped path is inside the
323+
// tree, the logic considers it sound and explicitly strips the
324+
// traversal.
325+
//
326+
// Conversely, attempts to escape the root directory directly using `..`
327+
// without an internal symlink are trapped and rejected.
328+
let escaped_path = user_root.join("../outside/passwd");
329+
assert_eq!(mapper.map_path(&escaped_path), None, "Path traversal should be rejected");
330+
331+
// The lexically normalized path inside the symlink safely maps to
332+
// `workspace/passwd`.
333+
assert_eq!(mapped, Some(user_root.join("passwd")));
334+
}
335+
}

0 commit comments

Comments
 (0)