Make charon-lib fully independent from rustc

charon/Cargo.toml

@@ -40,6 +40,8 @@ path = "tests/cargo.rs"
 harness = false
 
 [dependencies]
+annotate-snippets = "0.11.4"
+anstream = "0.6.18"
 anyhow = "1.0.81"
 assert_cmd = "2.0"
 clap = { version = "4.0", features = ["derive", "env"] }

charon/src/ast/meta.rs

@@ -30,36 +30,12 @@ pub struct Loc {
     pub col: usize,
 }
 
-/// For use when deserializing.
-#[cfg(feature = "rustc")]
-fn dummy_span_data() -> rustc_span::SpanData {
-    rustc_span::DUMMY_SP.data()
-}
-
 /// Span information
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct RawSpan {
     pub file_id: FileId,
     pub beg: Loc,
     pub end: Loc,
-    /// We keep the rust span so as to be able to leverage Rustc to print
-    /// error messages (useful in the micro-passes for instance).
-    /// We use `SpanData` instead of `Span` because `Span` is not `Send` when rustc runs
-    /// single-threaded (default on older versions). We need this to be `Send` because we pass this
-    /// data out of the rustc callbacks in charon-driver.
-    #[cfg(feature = "rustc")]
-    #[serde(skip)]
-    #[drive(skip)]
-    #[serde(default = "dummy_span_data")]
-    #[charon::opaque]
-    pub rust_span_data: rustc_span::SpanData,
-}
-
-#[cfg(feature = "rustc")]
-impl From<RawSpan> for rustc_error_messages::MultiSpan {
-    fn from(span: RawSpan) -> Self {
-        span.rust_span_data.span().into()
-    }
 }
 
 /// Meta information about a piece of code (block, statement, etc.)
@@ -102,27 +78,6 @@ pub struct Span {
     pub generated_from_span: Option<RawSpan>,
 }
 
-#[cfg(feature = "rustc")]
-impl From<Span> for rustc_span::Span {
-    fn from(span: Span) -> Self {
-        span.span.rust_span_data.span()
-    }
-}
-
-#[cfg(feature = "rustc")]
-impl From<Span> for rustc_error_messages::MultiSpan {
-    fn from(span: Span) -> Self {
-        span.span.into()
-    }
-}
-
-impl Span {
-    #[cfg(feature = "rustc")]
-    pub fn rust_span(self) -> rustc_span::Span {
-        self.span.rust_span_data.span()
-    }
-}
-
 /// `#[inline]` built-in attribute.
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
 pub enum InlineAttr {

charon/src/ast/meta_utils.rs

@@ -2,8 +2,24 @@
 use crate::meta::*;
 use crate::names::{Disambiguator, Name, PathElem};
 use itertools::Itertools;
+use std::borrow::Cow;
 use std::cmp::Ordering;
 use std::iter::Iterator;
+use std::ops::Range;
+
+/// Given a line number within a source file, get the byte of the start of the line. Obviously not
+/// efficient to do many times, but this is used is diagnostic paths only. The line numer is
+/// expected to be 1-based.
+fn line_to_start_byte(source: &str, line_nbr: usize) -> usize {
+    let mut cur_byte = 0;
+    for (i, line) in source.split_inclusive('\n').enumerate() {
+        if line_nbr == i + 1 {
+            break;
+        }
+        cur_byte += line.len();
+    }
+    cur_byte
+}
 
 impl Loc {
     fn dummy() -> Self {
@@ -31,6 +47,10 @@ impl Loc {
             Ordering::Less => *l1,
         }
     }
+
+    pub fn to_byte(self, source: &str) -> usize {
+        line_to_start_byte(source, self.line) + self.col
+    }
 }
 
 impl RawSpan {
@@ -39,15 +59,17 @@ impl RawSpan {
             file_id: FileId::from_raw(0),
             beg: Loc::dummy(),
             end: Loc::dummy(),
-            #[cfg(feature = "rustc")]
-            rust_span_data: rustc_span::DUMMY_SP.data(),
         }
     }
 
     /// Value with which we order `RawSpans`s.
     fn sort_key(&self) -> impl Ord {
         (self.file_id, self.beg, self.end)
     }
+
+    pub fn to_byte_range(self, source: &str) -> Range<usize> {
+        self.beg.to_byte(source)..self.end.to_byte(source)
+    }
 }
 
 /// Manual impls because `SpanData` is not orderable.
@@ -80,13 +102,6 @@ pub fn combine_span(m0: &Span, m1: &Span) -> Span {
             file_id: m0.span.file_id,
             beg: Loc::min(&m0.span.beg, &m1.span.beg),
             end: Loc::max(&m0.span.end, &m1.span.end),
-            #[cfg(feature = "rustc")]
-            rust_span_data: m0
-                .span
-                .rust_span_data
-                .span()
-                .to(m1.span.rust_span_data.span())
-                .data(),
         };
 
         // We don't attempt to merge the "generated from" spans: they might
@@ -114,6 +129,15 @@ pub fn combine_span_iter<'a, T: Iterator<Item = &'a Span>>(mut ms: T) -> Span {
     mc
 }
 
+impl FileName {
+    pub fn to_string(&self) -> Cow<'_, str> {
+        match self {
+            FileName::Virtual(path_buf) | FileName::Local(path_buf) => path_buf.to_string_lossy(),
+            FileName::NotReal(path) => Cow::Borrowed(path),
+        }
+    }
+}
+
 impl Attribute {
     /// Parse a raw attribute to recognize our special `charon::*` and `aeneas::*` attributes.
     pub fn parse_from_raw(raw_attr: RawAttribute) -> Result<Self, String> {

charon/src/bin/charon-driver/main.rs

@@ -283,9 +283,13 @@ fn main() {
     }
 
     match res {
+        Ok(()) if error_count == 0 => {}
         Ok(()) => {
-            if error_count > 0 {
-                assert!(!options.error_on_warnings);
+            if options.error_on_warnings {
+                let msg = format!("The extraction generated {} errors", error_count);
+                log::error!("{}", msg);
+                std::process::exit(1);
+            } else {
                 let msg = format!("The extraction generated {} warnings", error_count);
                 log::warn!("{}", msg);
             }

charon/src/bin/charon-driver/translate/translate_constants.rs

@@ -3,7 +3,7 @@ use super::translate_ctx::*;
 use charon_lib::ast::*;
 use hax_frontend_exporter as hax;
 
-impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
+impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     fn translate_constant_literal_to_raw_constant_expr(
         &mut self,
         v: &hax::ConstantLiteral,

charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs

@@ -8,7 +8,7 @@ use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use std::path::PathBuf;
 
-impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
+impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     /// Register a HIR item and all its children. We call this on the crate root items and end up
     /// exploring the whole crate.
     fn register_local_item(&mut self, def_id: DefId) {
@@ -228,7 +228,7 @@ pub fn translate<'tcx, 'ctx>(
     options: &CliOpts,
     tcx: TyCtxt<'tcx>,
     sysroot: PathBuf,
-) -> TransformCtx<'tcx> {
+) -> TransformCtx {
     let hax_state = hax::state::State::new(
         tcx,
         hax::options::Options {
@@ -248,11 +248,7 @@ pub fn translate<'tcx, 'ctx>(
         .clone();
     trace!("# Crate: {}", requested_crate_name);
 
-    let mut error_ctx = ErrorCtx::new(
-        !options.abort_on_error,
-        options.error_on_warnings,
-        tcx.dcx(),
-    );
+    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
     let translate_options = TranslateOptions::new(&mut error_ctx, options);
     let mut ctx = TranslateCtx {
         tcx,
@@ -270,6 +266,7 @@ pub fn translate<'tcx, 'ctx>(
         file_to_id: Default::default(),
         items_to_translate: Default::default(),
         translate_stack: Default::default(),
+        cached_item_metas: Default::default(),
         cached_names: Default::default(),
     };