Skip to content

SQUASH ME: First round of review focused on charon.rs; mostly style and comment changes #3390

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
mdittmer wants to merge 1 commit into from
Closed

SQUASH ME: First round of review focused on charon.rs; mostly style and comment changes #3390

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
256 changes: 113 additions & 143 deletions anneal/v2/src/charon.rs
View file
Open in desktop

Large diffs are not rendered by default.

80 changes: 36 additions & 44 deletions anneal/v2/src/diagnostics.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,11 @@
// Handling of Lean diagnostics and error mapping.
//
// This module provides the `DiagnosticMapper` struct, which is responsible
// This module provides the [`crate::diagnostics::DiagnosticMapper`] struct, which is responsible
// for translating diagnostics from external tools (like Lean or Charon) back
// to the original Rust source code. It maps errors in generated files back to
// their origin spans in the user's codebase.

use std::{
collections::HashMap,
fs,
path::{Component, Path, PathBuf},
};

pub use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel, DiagnosticSpan};
use miette::{NamedSource, Report, SourceOffset};
use thiserror::Error;

/// Maps diagnostics from generated intermediate code back to pristine,
/// original source code files.
Expand All @@ -24,19 +16,19 @@ use thiserror::Error;
/// To create a first-class user experience, this mapper actively
/// cross-references Lean's emitted byte spans against the sidecar
/// `SourceMapping`s built by `src/generate.rs`, dynamically synthesizing a
/// `miette::NamedSource` that points directly into the user's actual `.rs`
/// [`miette::NamedSource`] that points directly into the user's actual `.rs`
/// workspace files.
pub struct DiagnosticMapper {
user_root: PathBuf,
user_root_canonical: PathBuf,
source_cache: HashMap<PathBuf, String>,
user_root: std::path::PathBuf,
user_root_canonical: std::path::PathBuf,
source_cache: std::collections::HashMap<std::path::PathBuf, String>,
}

#[derive(Error, Debug)]
#[derive(thiserror::Error, Debug)]
#[error("{message}")]
struct MappedError {
message: String,
src: NamedSource<String>,
src: miette::NamedSource<String>,
labels: Vec<miette::LabeledSpan>,
help: Option<String>,
related: Vec<MappedError>,
Expand All @@ -48,15 +40,15 @@ impl miette::Diagnostic for MappedError {
Some(&self.src)
}

fn labels(&self) -> Option<Box<dyn Iterator<Item = miette::LabeledSpan> + '_>> {
fn labels(&self) -> Option<Box<dyn std::iter::Iterator<Item = miette::LabeledSpan> + '_>> {
if self.labels.is_empty() { None } else { Some(Box::new(self.labels.iter().cloned())) }
}

fn help(&self) -> Option<Box<dyn std::fmt::Display + '_>> {
self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
}

fn related<'a>(&'a self) -> Option<Box<dyn Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
fn related<'a>(&'a self) -> Option<Box<dyn std::iter::Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
if self.related.is_empty() {
None
} else {
Expand All @@ -72,46 +64,46 @@ impl miette::Diagnostic for MappedError {

impl DiagnosticMapper {
/// Creates a new mapper rooted at `user_root`.
pub fn new(user_root: PathBuf) -> Self {
pub fn new(user_root: std::path::PathBuf) -> Self {
let user_root_canonical =
fs::canonicalize(&user_root).unwrap_or_else(|_| user_root.clone());
Self { user_root, user_root_canonical, source_cache: HashMap::new() }
std::fs::canonicalize(&user_root).unwrap_or_else(|_| user_root.clone());
Self { user_root, user_root_canonical, source_cache: std::collections::HashMap::new() }
}

/// Resolves a path relative to the user root, if applicable.
///
/// This ensures we only report diagnostics for files within the user's
/// workspace, avoiding noise from dependencies or system files.
pub fn map_path(&self, path: &Path) -> Option<PathBuf> {
pub fn map_path(&self, path: &std::path::Path) -> Option<std::path::PathBuf> {
let mut p = path.to_path_buf();
if p.is_relative() {
p = self.user_root.join(p);
}

p = {
let mut normalized = PathBuf::new();
let mut normalized = std::path::PathBuf::new();
for component in p.components() {
let most_recent = normalized.components().next_back();
match (component, most_recent) {
(Component::ParentDir, Some(Component::Normal(_))) => {
(std::path::Component::ParentDir, Some(std::path::Component::Normal(_))) => {
normalized.pop();
}
(Component::CurDir, _) => {}
(std::path::Component::CurDir, _) => {}
_ => normalized.push(component),
}
}
normalized
};

// Strategy B: Starts with user_root or user_root_canonical
// Strategy B: Starts with user_root or user_root_canonical.
(p.starts_with(&self.user_root) || p.starts_with(&self.user_root_canonical)).then_some(p)
}

fn get_source(&mut self, path: &Path) -> Option<String> {
fn get_source(&mut self, path: &std::path::Path) -> Option<String> {
if let Some(src) = self.source_cache.get(path) {
return Some(src.clone());
}
if let Ok(src) = fs::read_to_string(path) {
if let Ok(src) = std::fs::read_to_string(path) {
self.source_cache.insert(path.to_path_buf(), src.clone());
Some(src)
} else {
Expand All @@ -128,11 +120,11 @@ impl DiagnosticMapper {
where
F: FnMut(String),
{
let mut mapped_paths_and_spans: HashMap<PathBuf, Vec<&DiagnosticSpan>> = HashMap::new();
let mut mapped_paths_and_spans: std::collections::HashMap<std::path::PathBuf, Vec<&DiagnosticSpan>> = std::collections::HashMap::new();

// 1) Group spans by mapped path
// 1) Group spans by mapped path.
for s in &diag.spans {
let p = PathBuf::from(&s.file_name);
let p = std::path::PathBuf::from(&s.file_name);
if let Some(mapped_path) = self.map_path(&p) {
mapped_paths_and_spans.entry(mapped_path).or_default().push(s);
}
Expand All @@ -152,14 +144,14 @@ impl DiagnosticMapper {
.spans
.iter()
.find(|s| s.is_primary)
.and_then(|s| self.map_path(&PathBuf::from(&s.file_name)))
.and_then(|s| self.map_path(&std::path::PathBuf::from(&s.file_name)))
.or_else(|| mapped_paths_and_spans.keys().next().cloned());

if let Some(main_path) = primary_path {
let mut all_errors = Vec::new();

// Sort the paths to have the primary path first
let mut paths: Vec<PathBuf> = mapped_paths_and_spans.keys().cloned().collect();
// Sort the paths to have the primary path first.
let mut paths: Vec<std::path::PathBuf> = mapped_paths_and_spans.keys().cloned().collect();
paths.sort_by_key(|p| p != &main_path);

for p in paths {
Expand All @@ -173,7 +165,7 @@ impl DiagnosticMapper {
let start: usize = s.byte_start.try_into().unwrap();
let len = (s.byte_end - s.byte_start).try_into().unwrap();
(start <= src.len() && start + len <= src.len()).then(|| {
let offset = SourceOffset::from(start);
let offset = miette::SourceOffset::from(start);
miette::LabeledSpan::new(Some(label_text), offset.offset(), len)
})
})
Expand All @@ -185,7 +177,7 @@ impl DiagnosticMapper {
} else {
format!("related to: {}", p.display())
},
src: NamedSource::new(p.to_string_lossy(), src),
src: miette::NamedSource::new(p.to_string_lossy(), src),
labels,
help: if p == main_path { help_msg.clone() } else { None },
related: Vec::new(),
Expand All @@ -204,13 +196,13 @@ impl DiagnosticMapper {
if !all_errors.is_empty() {
let mut main_err = all_errors.remove(0);
main_err.related = all_errors;
printer(format!("{:?}", Report::new(main_err)));
printer(format!("{:?}", miette::Report::new(main_err)));
return;
}
}
}

// If we get here, no span was successfully mapped
// If we get here, no span was successfully mapped.
let prefix = match diag.level {
DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
DiagnosticLevel::Warning => "[External Warning]",
Expand All @@ -224,7 +216,7 @@ impl DiagnosticMapper {
}
}

/// Renders a raw diagnostic (e.g., from Lean) directly at a mapped byte
/// Renders a diagnostic (e.g., from Lean) directly at a mapped byte
/// range.
///
/// The fundamental workflow for an external error is:
Expand All @@ -246,20 +238,20 @@ impl DiagnosticMapper {
) where
F: FnMut(String),
{
let p = PathBuf::from(file_name);
let p = std::path::PathBuf::from(file_name);
if let Some(mapped_path) = self.map_path(&p)
&& let Some(src) = self.get_source(&mapped_path)
{
let start = byte_start;
if byte_end >= start {
let len = byte_end - start;
if start <= src.len() && start + len <= src.len() {
let offset = SourceOffset::from(start);
let offset = miette::SourceOffset::from(start);
let label =
miette::LabeledSpan::new(Some("here".to_string()), offset.offset(), len);
let err = MappedError {
message,
src: NamedSource::new(mapped_path.to_string_lossy(), src),
src: miette::NamedSource::new(mapped_path.to_string_lossy(), src),
labels: vec![label],
help: None,
related: Vec::new(),
Expand All @@ -271,13 +263,13 @@ impl DiagnosticMapper {
_ => Some(miette::Severity::Advice),
},
};
printer(format!("{:?}", Report::new(err)));
printer(format!("{:?}", miette::Report::new(err)));
return;
}
}
}

// Fallback
// Fallback.
let prefix = match level {
DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
DiagnosticLevel::Warning => "[External Warning]",
Expand All @@ -297,7 +289,7 @@ mod tests {
let user_root = temp.path().join("workspace");
std::fs::create_dir(&user_root).unwrap();

// Create a symlink in the workspace pointing outside
// Create a symlink in the workspace pointing outside.
let outside = temp.path().join("outside");
std::fs::create_dir(&outside).unwrap();
std::os::unix::fs::symlink(&outside, user_root.join("symlink")).unwrap();
Expand Down
30 changes: 20 additions & 10 deletions anneal/v2/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ mod scanner;
mod charon;
mod setup;

/// Anneal: A Literate Verification Toolchain
/// Anneal: A Literate Verification Toolchain.
#[derive(clap::Parser, Debug)]
#[command(name = "cargo-anneal", version, about, long_about = None)]
struct Cli {
Expand All @@ -27,10 +27,13 @@ struct Cli {

#[derive(clap::Subcommand, Debug)]
enum Commands {
/// Setup Anneal dependencies
/// Setup Anneal dependencies.
Setup(SetupArgs),
/// Expand a crate (runs Charon)
/// Expand a crate (runs Charon).
Expand(ExpandArgs),
/// Setup test-only stripped toolchain (dev only).
#[cfg(feature = "exocrate_tests")]
TestSetup,
}

#[derive(clap::Parser, Debug)]
Expand All @@ -43,23 +46,23 @@ pub struct SetupArgs {
#[derive(clap::Parser, Debug)]
pub struct ExpandArgs {
#[command(flatten)]
pub resolve_args: resolve::Args,
pub resolve_args: crate::resolve::Args,

/// Controls where LLBC output is placed on the filesystem.
#[arg(long, value_name = "output-dir")]
pub output_dir: Option<std::path::PathBuf>,
}

fn setup(args: SetupArgs) {
setup::run_setup(setup::SetupArgs {
crate::setup::run_setup(crate::setup::SetupArgs {
local_archive: args.local_archive,
})
.expect("failed to setup toolchain");
}

fn expand(args: ExpandArgs) -> anyhow::Result<()> {
let roots = resolve::resolve_roots(&args.resolve_args)?;
let packages = scanner::scan_workspace(&roots)?;
let roots = crate::resolve::resolve_roots(&args.resolve_args)?;
let packages = crate::scanner::scan_workspace(&roots)?;
if packages.is_empty() {
log::warn!("No targets found to expand.");
return Ok(());
Expand All @@ -68,7 +71,8 @@ fn expand(args: ExpandArgs) -> anyhow::Result<()> {
if let Some(output_dir) = args.output_dir {
locked_roots.llbc_override = Some(output_dir);
}
charon::run_charon(&args.resolve_args, &locked_roots, &packages)?;
let toolchain = crate::setup::Toolchain::resolve()?;
crate::charon::run_charon(&args.resolve_args, &locked_roots, &packages, &toolchain)?;
Ok(())
}

Expand All @@ -93,12 +97,18 @@ fn main() {
std::process::exit(1);
}
}
#[cfg(feature = "exocrate_tests")]
Commands::TestSetup => {
if let Err(e) = crate::setup::run_test_setup() {
eprintln!("TestSetup failed: {:?}", e);
std::process::exit(1);
}
}
}
}

#[cfg(test)]
#[cfg(all(test, feature = "exocrate_tests"))]
mod tests {
#[cfg(feature = "exocrate_tests")]
#[test]
fn test_setup() {
super::setup(super::SetupArgs {
Expand Down
9 changes: 3 additions & 6 deletions anneal/v2/src/parse.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
use std::marker::PhantomData;
use std::path::PathBuf;

pub mod hkd {
pub struct Safe;
pub trait ThreadSafety {}
Expand All @@ -17,7 +14,7 @@ pub struct AnnealDecorated<T, B> {

#[derive(Clone, Debug)]
pub enum FunctionItem<M> {
Free(PhantomData<M>),
Free(std::marker::PhantomData<M>),
}

impl<M> FunctionItem<M> {
Expand All @@ -35,7 +32,7 @@ pub enum FunctionBlockInner {
#[derive(Clone, Debug)]
pub struct FunctionAnnealBlock<M> {
pub inner: FunctionBlockInner,
_phantom: PhantomData<M>,
_phantom: std::marker::PhantomData<M>,
}

#[derive(Clone, Debug)]
Expand All @@ -48,7 +45,7 @@ pub enum ParsedItem<M> {
pub struct ParsedLeanItem<M> {
pub item: ParsedItem<M>,
pub module_path: Vec<String>,
pub source_file: PathBuf,
pub source_file: std::path::PathBuf,
}

pub mod attr {
Expand Down
Loading
Loading