Skip to content

Commit 0062c3c

Browse files
committed
diagnostics: finalize robust shadow-to-user path mapping for compiler errors
* Normalize paths between integration runner's * Map cargo's absolute shadow output paths reliably by replacing temporary workspaces * Inject effectively through Charon driver * Remove diagnostic prints and fallback to deterministic string-replacement for verification assertions * Fix mapping of outputs to use robust non-spanning fallbacks gherrit-pr-id: Gd1a7f9c4436f266d37e83ebc2310f5a99a73d24d
1 parent e17001b commit 0062c3c

File tree

166 files changed

+676
-16
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

166 files changed

+676
-16
lines changed

tools/hermes/src/charon.rs

Lines changed: 54 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
use std::process::Command;
22

33
use anyhow::{bail, Context as _, Result};
4+
use cargo_metadata::diagnostic::DiagnosticLevel;
45

56
use crate::{
67
resolve::{Args, HermesTargetKind, Roots},
@@ -39,6 +40,9 @@ pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Re
3940
// Separator for the underlying cargo command
4041
cmd.arg("--");
4142

43+
// Ensure cargo emits json msgs which charon-driver natively generates
44+
cmd.arg("--message-format=json");
45+
4246
cmd.arg("--manifest-path").arg(&artifact.shadow_manifest_path);
4347

4448
match artifact.target_kind {
@@ -77,9 +81,57 @@ pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Re
7781

7882
log::debug!("Command: {:?}", cmd);
7983

80-
let status = cmd.status().context("Failed to execute charon")?;
84+
cmd.stdout(std::process::Stdio::piped());
85+
let mut child = cmd.spawn().context("Failed to spawn charon")?;
86+
87+
let mut output_error = false;
88+
if let Some(stdout) = child.stdout.take() {
89+
use std::io::{BufRead, BufReader};
90+
let reader = BufReader::new(stdout);
91+
92+
// When resolving mapped diagnostic paths, the original workspace is either test_case_root/source or workspace root.
93+
let user_root = if roots.workspace.join("source").exists() {
94+
roots.workspace.join("source")
95+
} else {
96+
roots.workspace.clone()
97+
};
98+
let mut mapper = crate::diagnostics::DiagnosticMapper::new(
99+
artifact.shadow_manifest_path.parent().unwrap().to_path_buf(),
100+
user_root,
101+
);
102+
103+
for line in reader.lines() {
104+
if let Ok(line) = line {
105+
if let Ok(msg) = serde_json::from_str::<cargo_metadata::Message>(&line) {
106+
use cargo_metadata::Message;
107+
match msg {
108+
Message::CompilerMessage(msg) => {
109+
mapper.render_miette(&msg.message);
110+
if matches!(
111+
msg.message.level,
112+
DiagnosticLevel::Error | DiagnosticLevel::Ice
113+
) {
114+
output_error = true;
115+
}
116+
}
117+
Message::TextLine(t) => {
118+
eprintln!("{}", t);
119+
}
120+
_ => {}
121+
}
122+
} else {
123+
// Print non-JSON lines to stderr
124+
eprintln!("{}", line);
125+
}
126+
}
127+
}
128+
}
129+
130+
let status = child.wait().context("Failed to wait for charon")?;
81131

82-
if !status.success() {
132+
if output_error {
133+
bail!("Diagnostic error in charon");
134+
} else if !status.success() {
83135
bail!("Charon failed with status: {}", status);
84136
}
85137
}

tools/hermes/src/diagnostics.rs

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
use std::{
2+
collections::HashMap,
3+
fs,
4+
path::{Path, PathBuf},
5+
};
6+
7+
use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel, DiagnosticSpan};
8+
use miette::{NamedSource, Report, SourceOffset};
9+
use thiserror::Error;
10+
11+
pub struct DiagnosticMapper {
12+
shadow_root: PathBuf,
13+
user_root: PathBuf,
14+
user_root_canonical: PathBuf,
15+
source_cache: HashMap<PathBuf, String>,
16+
}
17+
18+
#[derive(Error, Debug)]
19+
#[error("{message}")]
20+
struct MappedError {
21+
message: String,
22+
src: NamedSource<String>,
23+
labels: Vec<miette::LabeledSpan>,
24+
help: Option<String>,
25+
related: Vec<MappedError>,
26+
}
27+
28+
impl miette::Diagnostic for MappedError {
29+
fn source_code(&self) -> Option<&dyn miette::SourceCode> {
30+
Some(&self.src)
31+
}
32+
33+
fn labels(&self) -> Option<Box<dyn Iterator<Item = miette::LabeledSpan> + '_>> {
34+
if self.labels.is_empty() {
35+
None
36+
} else {
37+
Some(Box::new(self.labels.iter().cloned()))
38+
}
39+
}
40+
41+
fn help(&self) -> Option<Box<dyn std::fmt::Display + '_>> {
42+
self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
43+
}
44+
45+
fn related<'a>(&'a self) -> Option<Box<dyn Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
46+
if self.related.is_empty() {
47+
None
48+
} else {
49+
let iter = self.related.iter().map(|e| e as &dyn miette::Diagnostic);
50+
Some(Box::new(iter))
51+
}
52+
}
53+
}
54+
55+
impl DiagnosticMapper {
56+
pub fn new(shadow_root: PathBuf, user_root: PathBuf) -> Self {
57+
let user_root_canonical =
58+
fs::canonicalize(&user_root).unwrap_or_else(|_| user_root.clone());
59+
Self { shadow_root, user_root, user_root_canonical, source_cache: HashMap::new() }
60+
}
61+
62+
pub fn map_path(&self, path: &Path) -> Option<PathBuf> {
63+
let mut p = path.to_path_buf();
64+
if p.is_relative() {
65+
p = self.user_root.join(p);
66+
}
67+
68+
// Strategy A: Starts with shadow_root
69+
if let Ok(suffix) = p.strip_prefix(&self.shadow_root) {
70+
return Some(self.user_root.join(suffix));
71+
}
72+
73+
// Strategy B: Starts with user_root or user_root_canonical
74+
if p.starts_with(&self.user_root) || p.starts_with(&self.user_root_canonical) {
75+
return Some(p);
76+
}
77+
78+
None
79+
}
80+
81+
fn get_source(&mut self, path: &Path) -> Option<String> {
82+
if let Some(src) = self.source_cache.get(path) {
83+
return Some(src.clone());
84+
}
85+
if let Ok(src) = fs::read_to_string(path) {
86+
self.source_cache.insert(path.to_path_buf(), src.clone());
87+
Some(src)
88+
} else {
89+
None
90+
}
91+
}
92+
93+
pub fn render_miette(&mut self, diag: &Diagnostic) {
94+
let mut mapped_paths_and_spans: HashMap<PathBuf, Vec<&DiagnosticSpan>> = HashMap::new();
95+
96+
// 1) Group spans by mapped path
97+
for s in &diag.spans {
98+
let p = PathBuf::from(&s.file_name);
99+
if let Some(mapped_path) = self.map_path(&p) {
100+
mapped_paths_and_spans.entry(mapped_path).or_default().push(s);
101+
}
102+
}
103+
104+
// Check children for help messages
105+
let mut help_msg = None;
106+
for child in &diag.children {
107+
if child.level == DiagnosticLevel::Help {
108+
help_msg = Some(child.message.clone());
109+
}
110+
}
111+
112+
if !mapped_paths_and_spans.is_empty() {
113+
// Find the path that contains the primary span, or just take the first one
114+
let primary_path = diag
115+
.spans
116+
.iter()
117+
.find(|s| s.is_primary)
118+
.and_then(|s| self.map_path(&PathBuf::from(&s.file_name)))
119+
.or_else(|| mapped_paths_and_spans.keys().next().cloned());
120+
121+
if let Some(main_path) = primary_path {
122+
let mut all_errors = Vec::new();
123+
124+
// Sort the paths to have the primary path first
125+
let mut paths: Vec<PathBuf> = mapped_paths_and_spans.keys().cloned().collect();
126+
paths.sort_by_key(|p| p != &main_path);
127+
128+
for p in paths {
129+
if let Some(src) = self.get_source(&p) {
130+
let mut labels = Vec::new();
131+
for s in mapped_paths_and_spans.get(&p).unwrap() {
132+
let label_text = s.label.clone().unwrap_or_default();
133+
let start = s.byte_start as usize;
134+
let len = (s.byte_end - s.byte_start) as usize;
135+
if start <= src.len() && start + len <= src.len() {
136+
let offset = SourceOffset::from(start);
137+
labels.push(miette::LabeledSpan::new(
138+
Some(label_text),
139+
offset.offset(),
140+
len,
141+
));
142+
}
143+
}
144+
145+
let err = MappedError {
146+
message: if p == main_path {
147+
diag.message.clone()
148+
} else {
149+
format!("related to: {}", p.display())
150+
},
151+
src: NamedSource::new(p.to_string_lossy(), src),
152+
labels,
153+
help: if p == main_path { help_msg.clone() } else { None },
154+
related: Vec::new(),
155+
};
156+
all_errors.push(err);
157+
}
158+
}
159+
160+
if !all_errors.is_empty() {
161+
let mut main_err = all_errors.remove(0);
162+
main_err.related = all_errors;
163+
eprintln!("{:?}", Report::new(main_err));
164+
return;
165+
}
166+
}
167+
}
168+
169+
// If we get here, no span was successfully mapped
170+
let prefix = match diag.level {
171+
DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
172+
DiagnosticLevel::Warning => "[External Warning]",
173+
_ => "[External Info]",
174+
};
175+
eprintln!("{} {}", prefix, diag.message);
176+
}
177+
}

tools/hermes/src/main.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
mod charon;
2+
mod diagnostics;
23
mod errors;
34
mod parse;
45
mod resolve;
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
failure
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
Line 1 from charon
2+
× interleaved error
3+
╭─[[PROJECT_ROOT]/src/lib.rs:1:1]
4+
1 │ pub fn foo() {}
5+
· ─────┬────
6+
· ╰── label
7+
2 │
8+
╰────
9+
10+
Line 2 from charon
11+
Error: Diagnostic error in charon
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
[dependencies]
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Line 1 from charon
2+
{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: interleaved\n", "children": [], "code": null, "level": "error", "message": "interleaved error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "label", "text": [], "expansion": null}]}}
3+
Line 2 from charon
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
[package]
2+
name = "test_pkg"
3+
version = "0.1.0"
4+
edition = "2021"
5+
6+
[dependencies]
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
pub fn foo() {}
2+
3+
/// ```lean
4+
/// ```
5+
pub fn dummy() {}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
failure

0 commit comments

Comments
 (0)