Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
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
147 changes: 44 additions & 103 deletions frontend/diagnostics/src/error.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// rustc errors
extern crate rustc_errors;
use rustc_errors::{DiagCtxt, DiagnosticId};
use rustc_errors::DiagCtxt;

// rustc data_structures
extern crate rustc_data_structures;
Expand All @@ -9,182 +9,123 @@ extern crate rustc_data_structures;
extern crate rustc_span;
use rustc_span::Span;

fn warn_span_lint(dcx: &DiagCtxt, span: Span, msg: impl AsRef<str>, lint_name: &str) {
let mut err = dcx.struct_warn(msg.as_ref().to_string()).with_span(span);
err.is_lint(lint_name.to_string(), /* has_future_breakage */ false);
err.emit();
}

pub fn explicit_lifetime(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Explicit lifetimes are not supported",
DiagnosticId::Lint {
name: "Lifetime".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Lifetime",
);
}

pub fn mut_borrow_let(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Mutable borrows are not supported",
DiagnosticId::Lint {
name: "Mut borrow".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Mut borrow",
);
}

pub fn extern_crate(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
span,
"[Hax] External items need a model",
DiagnosticId::Lint {
name: "External".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
);
warn_span_lint(dcx, span, "[Hax] External items need a model", "External");
}

pub fn no_trait_objects(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Trait objects are not supported",
DiagnosticId::Lint {
name: "Trait objects".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Trait objects",
);
}

pub fn no_mut_self(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Mutable self is not supported",
DiagnosticId::Lint {
name: "Mutable self".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Mutable self",
);
}

pub fn no_mut(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Mutable arguments are not supported",
DiagnosticId::Lint {
name: "Mutability".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Mutability",
);
}

pub fn no_assoc_items(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Associated items are not supported",
DiagnosticId::Lint {
name: "Assoc items".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Assoc items",
);
}

pub fn unsupported_item(dcx: &DiagCtxt, span: Span, ident: String) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
format!("[Hax] {ident:?} is not supported"),
DiagnosticId::Lint {
name: "Unsupported item".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Unsupported item",
);
}

pub fn no_fn_mut(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
span,
"[Hax] FnMut is not supported",
DiagnosticId::Lint {
name: "Where".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
);
warn_span_lint(dcx, span, "[Hax] FnMut is not supported", "Where");
}

pub fn no_where_predicate(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Where predicates are not supported",
DiagnosticId::Lint {
name: "Where".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Where",
);
}

pub fn no_async_await(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Async and await are not supported",
DiagnosticId::Lint {
name: "Async".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Async",
);
}

pub fn no_unsafe(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
span,
"[Hax] Unsafe code is not supported",
DiagnosticId::Lint {
name: "Unsafe".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
);
warn_span_lint(dcx, span, "[Hax] Unsafe code is not supported", "Unsafe");
}

pub fn unsupported_loop(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
span,
"[Hax] loop and while are not supported",
DiagnosticId::Lint {
name: "Loops".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
);
warn_span_lint(dcx, span, "[Hax] loop and while are not supported", "Loops");
}

pub fn no_union(dcx: &DiagCtxt, span: Span) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
"[Hax] Unions are not supported",
DiagnosticId::Lint {
name: "Unsupported item".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"Unsupported item",
);
}

pub fn derive_external_trait(dcx: &DiagCtxt, span: Span, trait_name: String) {
dcx.span_warn_with_code(
warn_span_lint(
dcx,
span,
format!("[Hax] Implementation of external trait {trait_name} will require a model"),
DiagnosticId::Lint {
name: "External trait".to_string(),
has_future_breakage: false,
is_force_warn: true,
},
"External trait",
);
}
6 changes: 1 addition & 5 deletions frontend/diagnostics/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,7 @@ impl SessionExtTrait for rustc_errors::DiagCtxt {
fn span_hax_err<S: Into<MultiSpan> + Clone>(&self, diag: Diagnostics<S>) {
let span: MultiSpan = diag.span.clone().into();
let diag = diag.set_span(span.clone());
self.span_err_with_code(
span,
format!("{}", diag),
rustc_errors::DiagnosticId::Error(diag.kind.code().into()),
);
self.span_err(span, diag.to_string());
}
}

Expand Down
2 changes: 1 addition & 1 deletion frontend/exporter/src/traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -498,7 +498,7 @@ pub mod copy_paste_from_rustc {
// Cycle errors are the only post-monomorphization errors possible; emit them now so
// `rustc_ty_utils::resolve_associated_item` doesn't return `None` post-monomorphization.
for err in errors {
if let FulfillmentErrorCode::CodeCycle(cycle) = err.code {
if let FulfillmentErrorCode::Cycle(cycle) = err.code {
infcx.err_ctxt().report_overflow_obligation_cycle(&cycle);
}
}
Expand Down
19 changes: 8 additions & 11 deletions frontend/exporter/src/types/copied.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1944,22 +1944,13 @@ pub enum PatKind {
Error(ErrorGuaranteed),
}

/// Reflects [`rustc_middle::thir::Guard`]
#[derive(AdtInto)]
#[args(<'tcx, S: ExprState<'tcx>>, from: rustc_middle::thir::Guard<'tcx>, state: S as gstate)]
#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
pub enum Guard {
If(Expr),
IfLet(Pat, Expr),
}

/// Reflects [`rustc_middle::thir::Arm`]
#[derive(AdtInto)]
#[args(<'tcx, S: ExprState<'tcx>>, from: rustc_middle::thir::Arm<'tcx>, state: S as gstate)]
#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
pub struct Arm {
pub pattern: Pat,
pub guard: Option<Guard>,
pub guard: Option<Expr>,
pub body: Expr,
pub lint_level: LintLevel,
pub scope: Scope,
Expand Down Expand Up @@ -2045,6 +2036,12 @@ pub enum LitKind {
Err,
}

impl<S> SInto<S, u128> for rustc_data_structures::packed::Pu128 {
fn sinto(&self, _s: &S) -> u128 {
self.0
}
}

// FIXME: typo: invo**C**ation
#[allow(rustdoc::private_intra_doc_links)]
/// Describe a macro invocation, using
Expand Down Expand Up @@ -2596,7 +2593,7 @@ pub struct FnHeader {

pub type ThirBody = Expr;

impl<'x, 'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ty> for rustc_hir::Ty<'x> {
impl<'x: 'tcx, 'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ty> for rustc_hir::Ty<'x> {
fn sinto(self: &rustc_hir::Ty<'x>, s: &S) -> Ty {
// **Important:**
// We need a local id here, and we get it from the owner id, which must
Expand Down
2 changes: 1 addition & 1 deletion frontend/exporter/src/types/mir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -547,7 +547,7 @@ pub enum TerminatorKind {
/// relevant to the method (and not the trait) if it is a trait method
/// call. See [ParamsInfo] for the full details.
generics: Vec<GenericArg>,
args: Vec<Operand>,
args: Vec<Spanned<Operand>>,
destination: Place,
target: Option<BasicBlock>,
unwind: UnwindAction,
Expand Down
4 changes: 2 additions & 2 deletions frontend/exporter/src/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,9 @@ mod internal_helpers {
eprintln!("{}", backtrace);
let mut builder = $crate::utils::_verb!($verb, $s.base().tcx.dcx(), $message);
if let Some(span) = $span {
builder.set_span(span.clone());
builder.span(span.clone());
}
builder.code(rustc_errors::DiagnosticId::Error(format!("HaxFront")));
builder.code(rustc_errors::codes::ErrCode::MAX);
builder.note(
"⚠️ This is a bug in Hax's frontend.
Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!",
Expand Down
4 changes: 0 additions & 4 deletions frontend/lint/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -401,10 +401,6 @@ impl<'v> Visitor<'v> for Linter<'v> {
// keep going
walk_expr(self, ex);
}
fn visit_let_expr(&mut self, lex: &'v Let<'v>) {
tracing::trace!("visiting let expr {:?}", lex.span);
walk_let_expr(self, lex)
}
fn visit_expr_field(&mut self, field: &'v ExprField<'v>) {
tracing::trace!("visiting expr field {:?}", field.ident);
walk_expr_field(self, field)
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[toolchain]
channel = "nightly-2024-01-01"
channel = "nightly-2024-02-01"
components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]