Skip to content

Commit

Permalink
Merge pull request #524 from Nadrieril/simplify-error-handling
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Jan 14, 2025
2 parents 1c628d8 + b74925f commit ac84f11
Show file tree
Hide file tree
Showing 14 changed files with 205 additions and 229 deletions.
2 changes: 1 addition & 1 deletion charon/src/bin/charon-driver/driver.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
}

// Update the error count
internal.error_count = transform_ctx.errors.error_count;
internal.error_count = transform_ctx.errors.borrow().error_count;

export::CrateData::new(&transform_ctx)
}
18 changes: 7 additions & 11 deletions charon/src/bin/charon-driver/translate/translate_constants.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
RawConstantExpr::Adt(vid, fields)
}
ConstantExprKind::Array { .. } => {
error_or_panic!(self, span, "array constants are not supported yet")
raise_error!(self, span, "array constants are not supported yet")
}
ConstantExprKind::Tuple { fields } => {
let fields: Vec<ConstantExpr> = fields
Expand Down Expand Up @@ -130,19 +130,19 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
RawConstantExpr::Ref(Box::new(be))
}
ConstantExprKind::Cast { .. } => {
error_or_panic!(
raise_error!(
self,
span,
&format!("Unsupported constant: `ConstantExprKind::Cast {{..}}`",)
"Unsupported constant: `ConstantExprKind::Cast {{..}}`",
)
}
ConstantExprKind::RawBorrow {
mutability: false, ..
} => {
error_or_panic!(
raise_error!(
self,
span,
&format!("Unsupported constant: `ConstantExprKind::RawBorrow {{mutability: false, ..}}`",)
"Unsupported constant: `ConstantExprKind::RawBorrow {{mutability: false, ..}}`",
)
}
ConstantExprKind::RawBorrow {
Expand Down Expand Up @@ -173,7 +173,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
}
ConstantExprKind::Todo(msg) => {
// Case not yet handled by hax
error_or_panic!(self, span, format!("Unsupported constant: {:?}", msg))
raise_error!(self, span, "Unsupported constant: {:?}", msg)
}
};

Expand Down Expand Up @@ -206,11 +206,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
| RawConstantExpr::Ref(_)
| RawConstantExpr::MutPtr(_)
| RawConstantExpr::FnPtr { .. } => {
error_or_panic!(
self,
span,
format!("Unexpected constant generic: {:?}", value)
)
raise_error!(self, span, "Unexpected constant generic: {:?}", value)
}
RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
}
Expand Down
42 changes: 21 additions & 21 deletions charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ use charon_lib::transform::TransformCtx;
use hax_frontend_exporter as hax;
use rustc_hir::def_id::DefId;
use rustc_middle::ty::TyCtxt;
use std::cell::RefCell;
use std::path::PathBuf;

impl<'tcx, 'ctx> TranslateCtx<'tcx> {
Expand Down Expand Up @@ -97,19 +98,22 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
| FullDefKind::TyParam { .. }
| FullDefKind::Variant { .. } => {
let span = self.def_span(def_id);
self.span_err(
register_error!(
self,
span,
&format!(
"Cannot register this item: `{def_id:?}` with kind `{:?}`",
def.kind()
),
"Cannot register this item: `{def_id:?}` with kind `{:?}`",
def.kind()
);
}
}
}

pub(crate) fn translate_item(&mut self, item_src: TransItemSource, trans_id: AnyTransId) {
if self.errors.ignored_failed_decls.contains(&trans_id)
if self
.errors
.borrow()
.ignored_failed_decls
.contains(&trans_id)
|| self.translated.get_item(trans_id).is_some()
{
return;
Expand All @@ -119,12 +123,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
let span = ctx.def_span(rust_id);
// Catch cycles
let res = if ctx.translate_stack.contains(&trans_id) {
ctx.span_err(
register_error!(
ctx,
span,
&format!(
"Cycle detected while translating {rust_id:?}! Stack: {:?}",
&ctx.translate_stack
),
"Cycle detected while translating {rust_id:?}! Stack: {:?}",
&ctx.translate_stack
);
Err(())
} else {
Expand All @@ -141,10 +144,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
Ok(Err(_)) => Err(()),
// Panic
Err(_) => {
register_error_or_panic!(
register_error!(
ctx,
span,
format!("Thread panicked when extracting item `{rust_id:?}`.")
"Thread panicked when extracting item `{rust_id:?}`."
);
Err(())
}
Expand All @@ -155,11 +158,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
};

if res.is_err() {
ctx.span_err(
span,
&format!("Item `{rust_id:?}` caused errors; ignoring."),
);
ctx.errors.ignore_failed_decl(trans_id);
register_error!(ctx, span, "Item `{rust_id:?}` caused errors; ignoring.");
ctx.errors.borrow_mut().ignore_failed_decl(trans_id);
}
})
}
Expand Down Expand Up @@ -215,9 +215,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
// Translate if not already translated.
self.translate_item(item_source, id);

if self.errors.ignored_failed_decls.contains(&id) {
if self.errors.borrow().ignored_failed_decls.contains(&id) {
let span = self.def_span(item_source.to_def_id());
error_or_panic!(self, span, format!("Failed to translate item {id:?}."))
raise_error!(self, span, "Failed to translate item {id:?}.")
}
Ok(self.translated.get_item(id).unwrap())
}
Expand Down Expand Up @@ -255,7 +255,7 @@ pub fn translate<'tcx, 'ctx>(
sysroot,
hax_state,
options: translate_options,
errors: error_ctx,
errors: RefCell::new(error_ctx),
translated: TranslatedCrate {
crate_name: requested_crate_name,
options: options.clone(),
Expand Down
79 changes: 39 additions & 40 deletions charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,17 +14,18 @@ use macros::VariantIndexArity;
use rustc_hir::def_id::DefId;
use rustc_middle::ty::TyCtxt;
use std::borrow::Cow;
use std::cell::RefCell;
use std::cmp::Ord;
use std::collections::HashMap;
use std::collections::{BTreeMap, VecDeque};
use std::fmt;
use std::fmt::Debug;
use std::path::{Component, PathBuf};
use std::sync::Arc;
use std::{fmt, mem};

// Re-export to avoid having to fix imports.
pub(crate) use charon_lib::errors::{
error_assert, error_or_panic, register_error_or_panic, DepSource, ErrorCtx,
error_assert, raise_error, register_error, DepSource, ErrorCtx,
};

/// TODO: maybe we should always target MIR Built, this would make things
Expand Down Expand Up @@ -55,8 +56,12 @@ impl TranslateOptions {
let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
Ok(p) => Ok(p),
Err(e) => {
let msg = format!("failed to parse pattern `{s}` ({e})");
error_or_panic!(error_ctx, &TranslatedCrate::default(), Span::dummy(), msg)
raise_error!(
error_ctx,
crate(&TranslatedCrate::default()),
Span::dummy(),
"failed to parse pattern `{s}` ({e})"
)
}
};

Expand Down Expand Up @@ -179,7 +184,7 @@ pub struct TranslateCtx<'tcx> {
pub file_to_id: HashMap<FileName, FileId>,

/// Context for tracking and reporting errors.
pub errors: ErrorCtx,
pub errors: RefCell<ErrorCtx>,
/// The declarations we came accross and which we haven't translated yet. We keep them sorted
/// to make the output order a bit more stable.
pub items_to_translate: BTreeMap<TransItemSource, AnyTransId>,
Expand Down Expand Up @@ -366,23 +371,21 @@ where
let unwind_safe_s = std::panic::AssertUnwindSafe(s);
let unwind_safe_x = std::panic::AssertUnwindSafe(x);
std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
error_or_panic!(
raise_error!(
err,
krate,
crate(krate),
span,
format!("Hax panicked when translating `{x:?}`.")
"Hax panicked when translating `{x:?}`."
)
})
}

impl<'tcx, 'ctx> TranslateCtx<'tcx> {
pub fn continue_on_failure(&self) -> bool {
self.errors.continue_on_failure()
}

/// Span an error and register the error.
pub fn span_err(&mut self, span: Span, msg: &str) {
self.errors.span_err(&self.translated, span, msg)
pub fn span_err(&self, span: Span, msg: &str) -> Error {
self.errors
.borrow_mut()
.span_err(&self.translated, span, msg)
}

/// Register a file if it is a "real" file and was not already registered
Expand Down Expand Up @@ -471,10 +474,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
DefPathItem::Use => Some(PathElem::Ident("<use>".to_string(), disambiguator)),
_ => {
let def_id = def.to_rust_def_id();
error_or_panic!(
raise_error!(
self,
span,
format!("Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}")
"Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
);
}
};
Expand Down Expand Up @@ -554,7 +557,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
where
T: Debug + SInto<S, U>,
{
catch_sinto(s, &mut self.errors, &self.translated, span, x)
catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
}

pub fn hax_def(&mut self, def_id: impl Into<DefId>) -> Result<Arc<hax::FullDef>, Error> {
Expand All @@ -563,7 +566,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
// Hax takes care of caching the translation.
catch_sinto(
&self.hax_state,
&mut self.errors,
&mut *self.errors.borrow_mut(),
&self.translated,
span,
&def_id,
Expand All @@ -585,7 +588,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
let rename = renames.next();
if renames.next().is_some() {
let span = self.translate_span_from_hax(&def.span);
self.span_err(
register_error!(
self,
span,
"There should be at most one `charon::rename(\"...\")` \
or `aeneas::rename(\"...\")` attribute per declaration",
Expand Down Expand Up @@ -795,7 +799,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
Ok(a) => Some(a),
Err(msg) => {
let span = self.translate_span_from_hax(&attr.span);
self.span_err(span, &format!("Error parsing attribute: {msg}"));
register_error!(self, span, "Error parsing attribute: {msg}");
None
}
}
Expand Down Expand Up @@ -884,6 +888,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
}
};
self.errors
.borrow_mut()
.register_dep_source(src, item_id, id.to_def_id().is_local());
item_id
}
Expand Down Expand Up @@ -958,13 +963,14 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
where
F: FnOnce(&mut Self) -> T,
{
let current_def_id = self.errors.def_id;
let current_def_id_is_local = self.errors.def_id_is_local;
self.errors.def_id = Some(item_id);
self.errors.def_id_is_local = def_id.is_local();
let mut errors = self.errors.borrow_mut();
let current_def_id = mem::replace(&mut errors.def_id, Some(item_id));
let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local());
drop(errors); // important: release the refcell "lock"
let ret = f(self);
self.errors.def_id = current_def_id;
self.errors.def_id_is_local = current_def_id_is_local;
let mut errors = self.errors.borrow_mut();
errors.def_id = current_def_id;
errors.def_id_is_local = current_def_id_is_local;
ret
}
}
Expand Down Expand Up @@ -994,11 +1000,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
}
}

pub fn continue_on_failure(&self) -> bool {
self.t_ctx.continue_on_failure()
}

pub fn span_err(&mut self, span: Span, msg: &str) {
pub fn span_err(&self, span: Span, msg: &str) -> Error {
self.t_ctx.span_err(span, msg)
}

Expand Down Expand Up @@ -1102,10 +1104,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
{
Ok(self.bind_var(dbid, *rid))
} else {
error_or_panic!(
raise_error!(
self,
span,
&format!("Unexpected error: could not find region '{dbid}_{var}")
"Unexpected error: could not find region '{dbid}_{var}"
)
}
}
Expand All @@ -1122,11 +1124,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
}
}
let err = mk_err();
error_or_panic!(
self,
span,
&format!("Unexpected error: could not find {}", err)
)
raise_error!(self, span, "Unexpected error: could not find {}", err)
}

pub(crate) fn lookup_early_region(
Expand Down Expand Up @@ -1192,10 +1190,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
}
}
// Actually unreachable
error_or_panic!(
raise_error!(
self,
span,
&format!("Unexpected error: could not find clause variable {}", id)
"Unexpected error: could not find clause variable {}",
id
)
}

Expand Down
Loading

0 comments on commit ac84f11

Please sign in to comment.