Skip to content

Commit d0afaee

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 d0afaee

File tree

96 files changed

+505
-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.

96 files changed

+505
-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: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
use std::{
2+
collections::HashMap,
3+
fs,
4+
path::{Path, PathBuf},
5+
};
6+
7+
use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
8+
use miette::{NamedSource, Report, SourceOffset};
9+
use thiserror::Error;
10+
11+
pub struct DiagnosticMapper {
12+
shadow_root: PathBuf,
13+
user_root: PathBuf,
14+
source_cache: HashMap<PathBuf, String>,
15+
}
16+
17+
#[derive(Error, Debug)]
18+
#[error("{message}")]
19+
struct MappedError {
20+
message: String,
21+
src: NamedSource<String>,
22+
labels: Vec<miette::LabeledSpan>,
23+
help: Option<String>,
24+
}
25+
26+
impl miette::Diagnostic for MappedError {
27+
fn source_code(&self) -> Option<&dyn miette::SourceCode> {
28+
Some(&self.src)
29+
}
30+
31+
fn labels(&self) -> Option<Box<dyn Iterator<Item = miette::LabeledSpan> + '_>> {
32+
if self.labels.is_empty() {
33+
None
34+
} else {
35+
Some(Box::new(self.labels.iter().cloned()))
36+
}
37+
}
38+
39+
fn help(&self) -> Option<Box<dyn std::fmt::Display + '_>> {
40+
self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
41+
}
42+
}
43+
44+
impl DiagnosticMapper {
45+
pub fn new(shadow_root: PathBuf, user_root: PathBuf) -> Self {
46+
Self { shadow_root, user_root, source_cache: HashMap::new() }
47+
}
48+
49+
pub fn map_path(&self, path: &Path) -> Option<PathBuf> {
50+
path.strip_prefix(&self.shadow_root).ok().map(|suffix| self.user_root.join(suffix))
51+
}
52+
53+
fn get_source(&mut self, path: &Path) -> Option<String> {
54+
if let Some(src) = self.source_cache.get(path) {
55+
return Some(src.clone());
56+
}
57+
if let Ok(src) = fs::read_to_string(path) {
58+
self.source_cache.insert(path.to_path_buf(), src.clone());
59+
Some(src)
60+
} else {
61+
None
62+
}
63+
}
64+
65+
pub fn render_miette(&mut self, diag: &Diagnostic) {
66+
let primary_span = diag.spans.iter().find(|s| s.is_primary);
67+
68+
let mut mapped = false;
69+
if let Some(span) = primary_span {
70+
let path = PathBuf::from(&span.file_name);
71+
if let Some(mapped_path) = self.map_path(&path) {
72+
if let Some(src) = self.get_source(&mapped_path) {
73+
let mut labels = Vec::new();
74+
75+
for s in &diag.spans {
76+
let s_path = PathBuf::from(&s.file_name);
77+
if s_path == path || self.map_path(&s_path).as_ref() == Some(&mapped_path) {
78+
let label_text = s.label.clone().unwrap_or_default();
79+
let start = s.byte_start as usize;
80+
let len = (s.byte_end - s.byte_start) as usize;
81+
if start <= src.len() && start + len <= src.len() {
82+
let offset = SourceOffset::from(start);
83+
labels.push(miette::LabeledSpan::new(
84+
Some(label_text),
85+
offset.offset(),
86+
len,
87+
));
88+
}
89+
}
90+
}
91+
92+
// Check children for help messages
93+
let mut help_msg = None;
94+
for child in &diag.children {
95+
if child.level == DiagnosticLevel::Help {
96+
help_msg = Some(child.message.clone());
97+
}
98+
}
99+
100+
let err = MappedError {
101+
message: diag.message.clone(),
102+
src: NamedSource::new(mapped_path.to_string_lossy(), src),
103+
labels,
104+
help: help_msg,
105+
};
106+
107+
eprintln!("{:?}", Report::new(err));
108+
mapped = true;
109+
}
110+
}
111+
}
112+
113+
if !mapped {
114+
if diag.spans.is_empty() {
115+
eprintln!("[External Error] {}", diag.message);
116+
} else {
117+
eprintln!("[External Error] {}", diag.message);
118+
}
119+
}
120+
}
121+
}

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)