diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index e18d9728d..cfb89e165 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -11,7 +11,6 @@ use rustc_middle::{ thir, thir::{Block, BlockId, Expr, ExprId, ExprKind, Pat, PatKind, Stmt, StmtId, StmtKind, Thir}, }; -use rustc_session::parse::ParseSess; use rustc_span::symbol::Symbol; use serde::Serialize; use std::cell::RefCell; @@ -19,19 +18,19 @@ use std::collections::{HashMap, HashSet}; use std::rc::Rc; fn report_diagnostics( + tcx: TyCtxt<'_>, output: &hax_cli_options_engine::Output, - session: &rustc_session::Session, mapping: &Vec<(hax_frontend_exporter::Span, rustc_span::Span)>, ) { for d in &output.diagnostics { use hax_diagnostics::*; - session.span_hax_err(d.convert(mapping).into()); + tcx.dcx().span_hax_err(d.convert(mapping).into()); } } fn write_files( + tcx: TyCtxt<'_>, output: &hax_cli_options_engine::Output, - session: &rustc_session::Session, backend: hax_cli_options::Backend, ) { let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap(); @@ -43,9 +42,9 @@ fn write_files( for file in output.files.clone() { let path = out_dir.join(&file.path); std::fs::create_dir_all(&path.parent().unwrap()).unwrap(); - session.note_without_error(format!("Writing file {:#?}", path)); + tcx.dcx().note(format!("Writing file {:#?}", path)); std::fs::write(&path, file.contents).unwrap_or_else(|e| { - session.fatal(format!( + tcx.dcx().fatal(format!( "Unable to write to file {:#?}. Error: {:#?}", path, e )) @@ -127,11 +126,11 @@ fn precompute_local_thir_bodies<'tcx>( .filter(|ldid| hir.maybe_body_owned_by(*ldid).is_some()) .map(|ldid| { tracing::debug!("⏳ Type-checking THIR body for {:#?}", ldid); - let span = hir.span(hir.local_def_id_to_hir_id(ldid)); + let span = hir.span(tcx.local_def_id_to_hir_id(ldid)); let (thir, expr) = match tcx.thir_body(ldid) { Ok(x) => x, Err(e) => { - tcx.sess.span_err( + tcx.dcx().span_err( span, "While trying to reach a body's THIR defintion, got a typechecking error.", ); @@ -143,7 +142,7 @@ fn precompute_local_thir_bodies<'tcx>( })) { Ok(x) => x, Err(e) => { - tcx.sess.span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid)); + tcx.dcx().span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid)); return (ldid, dummy_thir_body(tcx, span)); } }; @@ -298,7 +297,7 @@ impl Callbacks for ExtractionCallbacks { .into_iter() .map(|(k, v)| { use hax_frontend_exporter::*; - let sess = compiler.session(); + let sess = &compiler.sess; ( translate_span(k, sess), translate_span(argument_span_of_mac_call(&v), sess), @@ -432,9 +431,8 @@ impl Callbacks for ExtractionCallbacks { .unwrap(); let out = engine_subprocess.wait_with_output().unwrap(); - let session = compiler.session(); if !out.status.success() { - session.fatal(format!( + tcx.dcx().fatal(format!( "{} exited with non-zero code {}\nstdout: {}\n stderr: {}", ENGINE_BINARY_NAME, out.status.code().unwrap_or(-1), @@ -456,8 +454,8 @@ impl Callbacks for ExtractionCallbacks { let state = hax_frontend_exporter::state::State::new(tcx, options_frontend.clone()); report_diagnostics( + tcx, &output, - &session, &spans .into_iter() .map(|span| (span.sinto(&state), span.clone())) @@ -467,7 +465,7 @@ impl Callbacks for ExtractionCallbacks { serde_json::to_writer(std::io::BufWriter::new(std::io::stdout()), &output) .unwrap() } else { - write_files(&output, &session, backend.backend); + write_files(tcx, &output, backend.backend); } if let Some(debug_json) = &output.debug_json { use hax_cli_options::DebugEngineMode; diff --git a/cli/driver/src/linter.rs b/cli/driver/src/linter.rs index ba82517f8..eeb2e4d93 100644 --- a/cli/driver/src/linter.rs +++ b/cli/driver/src/linter.rs @@ -28,11 +28,10 @@ impl Callbacks for LinterCallbacks { compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { - let session = compiler.session(); queries .global_ctxt() .unwrap() - .enter(|tcx| hax_lint::Linter::register(tcx, session, self.ltype)); + .enter(|tcx| hax_lint::Linter::register(tcx, self.ltype)); Compilation::Continue } diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 9f5407891..237be4494 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -15,11 +15,10 @@ module Imported = struct | ForeignMod | Use | GlobalAsm - | ClosureExpr + | Closure | Ctor | AnonConst - | ImplTrait - | ImplTraitAssocTy + | OpaqueTy | TypeNs of string | ValueNs of string | MacroNs of string @@ -32,11 +31,10 @@ module Imported = struct | ForeignMod -> ForeignMod | Use -> Use | GlobalAsm -> GlobalAsm - | ClosureExpr -> ClosureExpr + | Closure -> Closure | Ctor -> Ctor | AnonConst -> AnonConst - | ImplTrait -> ImplTrait - | ImplTraitAssocTy -> ImplTraitAssocTy + | OpaqueTy -> OpaqueTy | TypeNs s -> TypeNs s | ValueNs s -> ValueNs s | MacroNs s -> MacroNs s diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 1a5ab4b08..254084df4 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -844,6 +844,7 @@ end) : EXPR = struct | Or { pats } -> POr { subpats = List.map ~f:c_pat pats } | Slice _ -> unimplemented [ pat.span ] "pat Slice" | Range _ -> unimplemented [ pat.span ] "pat Range" + | Never -> unimplemented [ pat.span ] "pat Never" | Error _ -> unimplemented [ pat.span ] "pat Error" in { p = v; span; typ } @@ -1359,7 +1360,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = List.for_all ~f:(fun { data; _ } -> match data with - | Unit _ | Tuple ([], _, _) | Struct ([], _) -> true + | Unit _ | Tuple ([], _, _) | Struct { fields = []; _ } -> true | _ -> false) variants in @@ -1367,11 +1368,13 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = List.map ~f: (fun ({ data; def_id = variant_id; attributes; _ } as original) -> - let is_record = [%matches? Types.Struct (_ :: _, _)] data in + let is_record = + [%matches? Types.Struct { fields = _ :: _; _ }] data + in let name = Concrete_ident.of_def_id kind variant_id in let arguments = match data with - | Tuple (fields, _, _) | Struct (fields, _) -> + | Tuple (fields, _, _) | Struct { fields; _ } -> List.map ~f:(fun { def_id = id; ty; span; attributes; _ } -> ( Concrete_ident.of_def_id Field id, @@ -1415,7 +1418,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = in match v with | Tuple (fields, _, _) -> mk fields false - | Struct ((_ :: _ as fields), _) -> mk fields true + | Struct { fields = _ :: _ as fields; _ } -> mk fields true | _ -> { name; arguments = []; is_record = false; attrs } in let variants = [ v ] in diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs index 80d22a7e1..e4285a518 100644 --- a/engine/names/extract/build.rs +++ b/engine/names/extract/build.rs @@ -46,11 +46,10 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String { DefPathItem::ForeignMod => "ForeignMod".into(), DefPathItem::Use => "Use".into(), DefPathItem::GlobalAsm => "GlobalAsm".into(), - DefPathItem::ClosureExpr => "ClosureExpr".into(), + DefPathItem::Closure => "Closure".into(), DefPathItem::Ctor => "Ctor".into(), DefPathItem::AnonConst => "AnonConst".into(), - DefPathItem::ImplTrait => "ImplTrait".into(), - DefPathItem::ImplTraitAssocTy => "ImplTraitAssocTy".into(), + DefPathItem::OpaqueTy => "OpaqueTy".into(), } } diff --git a/frontend/diagnostics/src/error.rs b/frontend/diagnostics/src/error.rs index 477c6129f..1eb614c29 100644 --- a/frontend/diagnostics/src/error.rs +++ b/frontend/diagnostics/src/error.rs @@ -1,21 +1,16 @@ // rustc errors extern crate rustc_errors; -use rustc_errors::DiagnosticId; - -// rustc session -extern crate rustc_session; -use rustc_session::Session; +use rustc_errors::{DiagCtxt, DiagnosticId}; // rustc data_structures extern crate rustc_data_structures; -use rustc_data_structures::sync::Lrc; // rustc span extern crate rustc_span; use rustc_span::Span; -pub fn explicit_lifetime(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn explicit_lifetime(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Explicit lifetimes are not supported", DiagnosticId::Lint { @@ -26,8 +21,8 @@ pub fn explicit_lifetime(session: &Lrc, span: Span) { ); } -pub fn mut_borrow_let(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn mut_borrow_let(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Mutable borrows are not supported", DiagnosticId::Lint { @@ -38,8 +33,8 @@ pub fn mut_borrow_let(session: &Lrc, span: Span) { ); } -pub fn extern_crate(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn extern_crate(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] External items need a model", DiagnosticId::Lint { @@ -50,8 +45,8 @@ pub fn extern_crate(session: &Lrc, span: Span) { ); } -pub fn no_trait_objects(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_trait_objects(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Trait objects are not supported", DiagnosticId::Lint { @@ -62,8 +57,8 @@ pub fn no_trait_objects(session: &Lrc, span: Span) { ); } -pub fn no_mut_self(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_mut_self(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Mutable self is not supported", DiagnosticId::Lint { @@ -74,8 +69,8 @@ pub fn no_mut_self(session: &Lrc, span: Span) { ); } -pub fn no_mut(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_mut(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Mutable arguments are not supported", DiagnosticId::Lint { @@ -86,8 +81,8 @@ pub fn no_mut(session: &Lrc, span: Span) { ); } -pub fn no_assoc_items(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_assoc_items(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Associated items are not supported", DiagnosticId::Lint { @@ -98,8 +93,8 @@ pub fn no_assoc_items(session: &Lrc, span: Span) { ); } -pub fn unsupported_item(session: &Lrc, span: Span, ident: String) { - session.span_warn_with_code( +pub fn unsupported_item(dcx: &DiagCtxt, span: Span, ident: String) { + dcx.span_warn_with_code( span, format!("[Hax] {ident:?} is not supported"), DiagnosticId::Lint { @@ -110,8 +105,8 @@ pub fn unsupported_item(session: &Lrc, span: Span, ident: String) { ); } -pub fn no_fn_mut(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_fn_mut(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] FnMut is not supported", DiagnosticId::Lint { @@ -122,8 +117,8 @@ pub fn no_fn_mut(session: &Lrc, span: Span) { ); } -pub fn no_where_predicate(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_where_predicate(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Where predicates are not supported", DiagnosticId::Lint { @@ -134,8 +129,8 @@ pub fn no_where_predicate(session: &Lrc, span: Span) { ); } -pub fn no_async_await(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_async_await(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Async and await are not supported", DiagnosticId::Lint { @@ -146,8 +141,8 @@ pub fn no_async_await(session: &Lrc, span: Span) { ); } -pub fn no_unsafe(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_unsafe(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Unsafe code is not supported", DiagnosticId::Lint { @@ -158,8 +153,8 @@ pub fn no_unsafe(session: &Lrc, span: Span) { ); } -pub fn unsupported_loop(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn unsupported_loop(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] loop and while are not supported", DiagnosticId::Lint { @@ -170,8 +165,8 @@ pub fn unsupported_loop(session: &Lrc, span: Span) { ); } -pub fn no_union(session: &Lrc, span: Span) { - session.span_warn_with_code( +pub fn no_union(dcx: &DiagCtxt, span: Span) { + dcx.span_warn_with_code( span, "[Hax] Unions are not supported", DiagnosticId::Lint { @@ -182,8 +177,8 @@ pub fn no_union(session: &Lrc, span: Span) { ); } -pub fn derive_external_trait(session: &Lrc, span: Span, trait_name: String) { - session.span_warn_with_code( +pub fn derive_external_trait(dcx: &DiagCtxt, span: Span, trait_name: String) { + dcx.span_warn_with_code( span, format!("[Hax] Implementation of external trait {trait_name} will require a model"), DiagnosticId::Lint { diff --git a/frontend/diagnostics/src/lib.rs b/frontend/diagnostics/src/lib.rs index 59e4892bf..6ca4e2d82 100644 --- a/frontend/diagnostics/src/lib.rs +++ b/frontend/diagnostics/src/lib.rs @@ -14,7 +14,8 @@ use serde::{Deserialize, Serialize}; pub trait SessionExtTrait { fn span_hax_err + Clone>(&self, diag: Diagnostics); } -impl SessionExtTrait for rustc_session::Session { + +impl SessionExtTrait for rustc_errors::DiagCtxt { fn span_hax_err + Clone>(&self, diag: Diagnostics) { let span: MultiSpan = diag.span.clone().into(); let diag = diag.set_span(span.clone()); diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 76a5b4782..8e3cf3ef4 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -246,7 +246,7 @@ pub(crate) fn scalar_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( ) }); use rustc_middle::mir::interpret::GlobalAlloc; - let contents = match tcx.global_alloc(pointer.provenance.s_unwrap(s)) { + let contents = match tcx.global_alloc(pointer.provenance.s_unwrap(s).alloc_id()) { GlobalAlloc::Static(did) => ConstantExprKind::GlobalName { id: did.sinto(s), generics: Vec::new(), trait_refs: Vec::new() }, GlobalAlloc::Memory(alloc) => { let values = alloc.inner().get_bytes_unchecked(rustc_middle::mir::interpret::AllocRange { diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 6904dae02..f6f873543 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -403,7 +403,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>, T: SInto, U> SInto> /// Reflects [`rustc_middle::infer::canonical::CanonicalVarKind`] #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::infer::canonical::CanonicalVarKind<'tcx>, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::infer::canonical::CanonicalVarKind>, state: S as gstate)] pub enum CanonicalVarInfo { Ty(CanonicalTyVarKind), PlaceholderTy(PlaceholderType), @@ -974,7 +974,6 @@ pub enum BlockSafety { pub struct Block { pub targeted_by_break: bool, pub region_scope: Scope, - pub opt_destruction_scope: Option, pub span: Span, pub stmts: Vec, pub expr: Option, @@ -996,7 +995,6 @@ pub enum BindingMode { #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub struct Stmt { pub kind: StmtKind, - pub opt_destruction_scope: Option, } /// Reflects [`rustc_ast::token::Delimiter`] @@ -1020,7 +1018,7 @@ pub enum Delimiter { )] pub enum TokenTree { Token(Token, Spacing), - Delimited(DelimSpan, Delimiter, TokenStream), + Delimited(DelimSpan, DelimSpacing, Delimiter, TokenStream), } /// Reflects [`rustc_ast::tokenstream::Spacing`] @@ -1032,6 +1030,7 @@ pub enum TokenTree { pub enum Spacing { Alone, Joint, + JointHidden, } /// Reflects [`rustc_ast::token::BinOpToken`] @@ -1670,7 +1669,7 @@ pub enum Ty { RawPtr(TypeAndMut), Ref(Region, Box, Mutability), Dynamic(Vec>, Region, DynKind), - Coroutine(DefId, Vec, Movability), + Coroutine(DefId, Vec), Never, Tuple(Vec), #[custom_arm( @@ -1941,6 +1940,7 @@ pub enum PatKind { Or { pats: Vec, }, + Never, Error(ErrorGuaranteed), } @@ -2893,7 +2893,10 @@ pub enum FnRetTy { #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(<'tcx, S: UnderOwnerState<'tcx> >, from: rustc_hir::VariantData<'tcx>, state: S as tcx)] pub enum VariantData { - Struct(Vec, bool), + Struct { + fields: Vec, + recovered: bool, + }, Tuple(Vec, HirId, GlobalIdent), Unit(HirId, GlobalIdent), } @@ -2949,7 +2952,7 @@ pub struct UsePath { pub res: Vec, pub segments: Vec, #[value(self.segments.iter().last().map_or(None, |segment| { - match s.base().tcx.hir().find_by_def_id(segment.hir_id.owner.def_id) { + match s.base().tcx.opt_hir_node_by_def_id(segment.hir_id.owner.def_id) { Some(rustc_hir::Node::Item(rustc_hir::Item { ident, kind: rustc_hir::ItemKind::Use(_, _), @@ -3483,12 +3486,12 @@ pub enum ClosureKind { pub enum PredicateKind { Clause(ClauseKind), ObjectSafe(DefId), - ClosureKind(DefId, Vec, ClosureKind), Subtype(SubtypePredicate), Coerce(CoercePredicate), ConstEquate(ConstantExpr, ConstantExpr), Ambiguous, AliasRelate(Term, Term, AliasRelationDirection), + NormalizesTo(NormalizesTo), } /// Reflects [`rustc_hir::GenericBounds`] @@ -3502,8 +3505,8 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene // either call `predicates_defined_on` or `item_bounds` let use_item_bounds = { if let Some(oid) = s.owner_id().as_local() { - let hir_id = tcx.hir().local_def_id_to_hir_id(oid); - let node = tcx.hir().get(hir_id); + let hir_id = tcx.local_def_id_to_hir_id(oid); + let node = tcx.hir_node(hir_id); use rustc_hir as hir; matches!( node, diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index ef5c7a33c..e92a2f07b 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -57,9 +57,8 @@ pub enum DefPathItem { ValueNs(Symbol), MacroNs(Symbol), LifetimeNs(Symbol), - ClosureExpr, + Closure, Ctor, AnonConst, - ImplTrait, - ImplTraitAssocTy, + OpaqueTy, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 9c6bf48ae..3a2e2feee 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -899,7 +899,7 @@ pub enum AggregateKind { AggregateKind::Closure(def_id, parent_generics.sinto(s), trait_refs, sig) })] Closure(DefId, Vec, Vec, MirPolyFnSig), - Coroutine(DefId, Vec, Movability), + Coroutine(DefId, Vec), } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] diff --git a/frontend/exporter/src/types/todo.rs b/frontend/exporter/src/types/todo.rs index 6df174278..f1ae0f8fc 100644 --- a/frontend/exporter/src/types/todo.rs +++ b/frontend/exporter/src/types/todo.rs @@ -3,12 +3,14 @@ use crate::sinto_todo; sinto_todo!(rustc_middle::ty, ScalarInt); sinto_todo!(rustc_middle::ty, ExistentialPredicate<'a>); sinto_todo!(rustc_middle::ty, AdtFlags); +sinto_todo!(rustc_middle::ty, NormalizesTo<'tcx>); sinto_todo!(rustc_abi, IntegerType); sinto_todo!(rustc_abi, ReprFlags); sinto_todo!(rustc_abi, Align); sinto_todo!(rustc_middle::mir::interpret, ConstAllocation<'a>); sinto_todo!(rustc_middle::mir, UnwindTerminateReason); sinto_todo!(rustc_ast::tokenstream, DelimSpan); +sinto_todo!(rustc_ast::tokenstream, DelimSpacing); sinto_todo!(rustc_hir::def, DefKind); sinto_todo!(rustc_hir, GenericArgs<'a> as HirGenericArgs); sinto_todo!(rustc_hir, InlineAsm<'a>); diff --git a/frontend/exporter/src/utils.rs b/frontend/exporter/src/utils.rs index b36bc2c58..d5e77d23c 100644 --- a/frontend/exporter/src/utils.rs +++ b/frontend/exporter/src/utils.rs @@ -28,7 +28,7 @@ mod internal_helpers { ($verb:ident, $s:ident, $span:expr, $message:expr) => {{ let backtrace = std::backtrace::Backtrace::capture(); eprintln!("{}", backtrace); - let mut builder = $crate::utils::_verb!($verb, $s.base().tcx.sess, $message); + let mut builder = $crate::utils::_verb!($verb, $s.base().tcx.dcx(), $message); if let Some(span) = $span { builder.set_span(span.clone()); } diff --git a/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index 6d629876c..c7b074f57 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -6,7 +6,11 @@ use hax_diagnostics::error; use rustc_middle::hir::nested_filter::OnlyBodies; use rustc_middle::ty::TyCtxt; -// rustc hier +// rustc errors +extern crate rustc_errors; +use rustc_errors::DiagCtxt; + +// rustc hir extern crate rustc_hir; use rustc_hir::{intravisit::*, *}; @@ -15,13 +19,8 @@ use rustc_hir::{intravisit::*, *}; extern crate rustc_span; use rustc_span::{def_id::LocalDefId, symbol::Ident, Span, Symbol}; -// rustc session -extern crate rustc_session; -use rustc_session::Session; - // rustc data_structures extern crate rustc_data_structures; -use rustc_data_structures::sync::Lrc; // rustc ast extern crate rustc_ast; @@ -33,17 +32,16 @@ pub enum Type { Hacspec, } -pub struct Linter<'a, 'tcx> { - session: &'a Lrc, +pub struct Linter<'tcx> { tcx: TyCtxt<'tcx>, extern_allow_list: Vec<&'static str>, trait_block_list: Vec, ltype: Type, } -impl<'a, 'tcx> Linter<'a, 'tcx> { +impl<'tcx> Linter<'tcx> { /// Register the linter. - pub fn register(tcx: TyCtxt<'tcx>, session: &'a Lrc, ltype: Type) { + pub fn register(tcx: TyCtxt<'tcx>, ltype: Type) { let hir = tcx.hir(); let trait_block_list = vec!["FnMut"]; @@ -62,7 +60,6 @@ impl<'a, 'tcx> Linter<'a, 'tcx> { } let mut linter = Self { - session, tcx, extern_allow_list, trait_block_list, @@ -70,6 +67,10 @@ impl<'a, 'tcx> Linter<'a, 'tcx> { }; hir.visit_all_item_likes_in_crate(&mut linter); } + + fn dcx(&self) -> &'tcx DiagCtxt { + self.tcx.dcx() + } } fn has_attr(attrs: &[ast::Attribute], symbol: Symbol) -> bool { @@ -83,7 +84,7 @@ macro_rules! skip_derived_non_local { return; } if $self.non_local_hir_id($hir_id) { - error::extern_crate($self.session, $self.tcx.def_span($hir_id.owner)); + error::extern_crate($self.dcx(), $self.tcx.def_span($hir_id.owner)); // Don't keep going return; } @@ -111,7 +112,7 @@ macro_rules! skip_v1_lib_macros { }; } -impl<'a, 'v> Linter<'a, 'v> { +impl<'v> Linter<'v> { fn any_parent_has_attr(&self, hir_id: HirId, symbol: Symbol) -> bool { let map = &self.tcx.hir(); let mut prev_enclosing_node = None; @@ -145,7 +146,7 @@ impl<'a, 'v> Linter<'a, 'v> { return true; } // On everything else we warn. - error::extern_crate(self.session, span); + error::extern_crate(self.dcx(), span); // } return true; } @@ -176,7 +177,7 @@ impl<'a, 'v> Linter<'a, 'v> { } } -impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { +impl<'v> Visitor<'v> for Linter<'v> { type NestedFilter = OnlyBodies; fn nested_visit_map(&mut self) -> Self::Map { @@ -212,14 +213,14 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { match i.kind { ItemKind::Union(_, _) => { // TODO: This should be an error (span_err_with_code) - error::no_union(self.session, i.span); + error::no_union(self.dcx(), i.span); // self.no_union(i.span) } - ItemKind::GlobalAsm(_) => error::no_unsafe(self.session, i.span), + ItemKind::GlobalAsm(_) => error::no_unsafe(self.dcx(), i.span), ItemKind::Impl(imp) => { // tracing::trace!(" impl {:?}", imp.self_ty.kind); if imp.unsafety == Unsafety::Unsafe { - error::no_unsafe(self.session, i.span); + error::no_unsafe(self.dcx(), i.span); } if let Some(of_trait) = &imp.of_trait { let def_id = of_trait.hir_ref_id.owner.def_id.to_def_id(); @@ -274,7 +275,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { // XXX: This really shouldn't be done here but earlier. if ident.name.as_str() == "FnMut" { - error::no_fn_mut(self.session, ident.span); + error::no_fn_mut(self.dcx(), ident.span); return; } @@ -317,7 +318,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { ExprKind::AddrOf(x, f, _s) => { // Don't allow raw borrows (pointer) and mutable borrows. if matches!(x, BorrowKind::Raw) || matches!(f, Mutability::Mut) { - error::mut_borrow_let(self.session, b.span) + error::mut_borrow_let(self.dcx(), b.span) } } _ => (), @@ -364,20 +365,18 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { match &ex.kind { ExprKind::Block(block, _) => match block.rules { BlockCheckMode::UnsafeBlock(UnsafeSource::UserProvided) => { - error::no_unsafe(self.session, block.span) + error::no_unsafe(self.dcx(), block.span) } _ => (), }, ExprKind::Loop(_block, _label, source, span) => match source { - LoopSource::Loop | LoopSource::While => { - error::unsupported_loop(self.session, *span) - } + LoopSource::Loop | LoopSource::While => error::unsupported_loop(self.dcx(), *span), LoopSource::ForLoop => tracing::trace!("hir for loop"), }, // FIXME: where to get this from? // ExprKind::Async(e, c, b) => self.no_async_await(b.span), // ExprKind::Await(a) => self.no_async_await(a.span), - ExprKind::InlineAsm(p) => error::no_unsafe(self.session, p.line_spans[0]), + ExprKind::InlineAsm(p) => error::no_unsafe(self.dcx(), p.line_spans[0]), ExprKind::Call(expr, _exprs) => { // tracing::trace!("call: {:#?}", expr); if self.tcx.is_foreign_item(expr.hir_id.owner.def_id) { @@ -436,13 +435,6 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { // tracing::trace!(" bound predicate {:#?}", p.bounds); for bound in p.bounds { match bound { - GenericBound::LangItemTrait(lang_item, span, _hir_id, _generic_args) => { - // XXX: for some reason FnMut is not a lang item - tracing::trace!(" lang trait bound {:?}", span); - if matches!(lang_item, LangItem::FnMut) { - error::no_fn_mut(self.session, *span); - } - } GenericBound::Trait(trait_ref, _bound_modifier) => { tracing::trace!(" trait bound {:?}", trait_ref); // tracing::trace!( @@ -454,7 +446,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { } } } - WherePredicate::RegionPredicate(p) => error::explicit_lifetime(self.session, p.span), + WherePredicate::RegionPredicate(p) => error::explicit_lifetime(self.dcx(), p.span), WherePredicate::EqPredicate(p) => { tracing::trace!(" eq predicate {:?}/{:?}", p.lhs_ty, p.rhs_ty); } @@ -481,16 +473,16 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { ) { tracing::trace!("visiting fn at {:?}", span); - let hir_id = self.tcx.hir().local_def_id_to_hir_id(id); + let hir_id = self.tcx.local_def_id_to_hir_id(id); skip_derived_non_local!(self, hir_id); skip_v1_lib_macros!(self, hir_id); fn check_ty_kind(visitor: &Linter, k: &TyKind, span: Span) { match k { - TyKind::Ptr(_) => error::no_unsafe(visitor.session, span), + TyKind::Ptr(_) => error::no_unsafe(visitor.dcx(), span), TyKind::TraitObject(_, _, _) => { - error::no_trait_objects(visitor.session, span); + error::no_trait_objects(visitor.dcx(), span); } TyKind::Ref(lifetime, ty) => { // TODO: check lifetime. only allow anonymous @@ -502,14 +494,14 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { if matches!(ty.mutbl, Mutability::Mut) { if matches!(visitor.ltype, Type::Hacspec) { // No mutability is allowed here for hacspec - error::no_mut(visitor.session, ty.ty.span); + error::no_mut(visitor.dcx(), ty.ty.span); return; } match &ty.ty.kind { TyKind::Path(path) => match path { QPath::Resolved(_ty, p) => { if p.segments[0].ident.as_str() == "Self" { - error::no_mut_self(visitor.session, p.span) + error::no_mut_self(visitor.dcx(), p.span) } } _ => (), @@ -521,7 +513,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { check_ty_kind(visitor, &ty.ty.kind, span) } TyKind::OpaqueDef(_, _, _) => { - error::no_trait_objects(visitor.session, span); + error::no_trait_objects(visitor.dcx(), span); } TyKind::Path(path) => match path { QPath::Resolved(ty, p) => { @@ -534,11 +526,11 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { .iter() .any(|s| s.ident.to_string().contains("impl")) { - error::no_trait_objects(visitor.session, span); + error::no_trait_objects(visitor.dcx(), span); } } QPath::TypeRelative(ty, _p) => check_ty_kind(visitor, &ty.kind, span), - QPath::LangItem(_lang_item, _span, _hir_id) => (), + QPath::LangItem(_lang_item, _span) => (), }, _ => (), } @@ -550,19 +542,19 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { // TODO: All this should be an error (span_err_with_code) // Unsafe functions if header.unsafety == Unsafety::Unsafe { - error::no_unsafe(self.session, span); + error::no_unsafe(self.dcx(), span); } // async functions if let IsAsync::Async(_) = header.asyncness { - error::no_async_await(self.session, span); + error::no_async_await(self.dcx(), span); } // Check generics for lifetimes for predicate in generics.predicates { match &predicate { WherePredicate::RegionPredicate(region) => { - error::explicit_lifetime(self.session, region.span) + error::explicit_lifetime(self.dcx(), region.span) } WherePredicate::BoundPredicate(bound) => { for bound in bound.bounds { @@ -583,7 +575,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { if self.trait_block_list.contains(&path_string) { error::unsupported_item( - self.session, + self.dcx(), poly_ref.span, path_string, ); @@ -600,7 +592,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { match param.kind { GenericParamKind::Lifetime { kind } => match kind { LifetimeParamKind::Explicit => { - error::explicit_lifetime(self.session, param.span) + error::explicit_lifetime(self.dcx(), param.span) } _ => (), }, @@ -613,12 +605,12 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { // TODO: All this should be an error (span_err_with_code) // Unsafe functions if sig.header.unsafety == Unsafety::Unsafe { - error::no_unsafe(self.session, span); + error::no_unsafe(self.dcx(), span); } // async functions if let IsAsync::Async(_) = sig.header.asyncness { - error::no_async_await(self.session, span); + error::no_async_await(self.dcx(), span); } // Check method input arguments @@ -794,7 +786,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { _ => (), }, QPath::TypeRelative(_ty, _path) => (), - QPath::LangItem(item, _span, _hir_id) => { + QPath::LangItem(item, _span) => { tracing::trace!(" language item {:?}", item); } } @@ -864,7 +856,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { } fn visit_inline_asm(&mut self, asm: &'v InlineAsm<'v>, _id: HirId) { tracing::trace!("visiting inline asm"); - error::no_unsafe(self.session, asm.line_spans[0]); // XXX: what's the right span here? + error::no_unsafe(self.dcx(), asm.line_spans[0]); // XXX: what's the right span here? // don't keep going // walk_inline_asm(self, asm, id); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0ee9750b5..bdb122218 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-11-16" +channel = "nightly-2024-01-01" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index f7bfd661b..f9c9c6e1b 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -156,8 +156,9 @@ let empty_array (_: Prims.unit) : Prims.unit = () let panic_with_msg (_: Prims.unit) : Prims.unit = - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (Rust_primitives.unsize - (let list = ["with msg"] in + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt true + (Core.Fmt.impl_2__new_const true + (Rust_primitives.unsize (let list = ["with msg"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) <: diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index d01460536..ad3aa6b08 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap @@ -52,8 +52,12 @@ let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Core.Slice.impl__swap #u8 true vec (sz 0) (sz 1) + in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Core.Slice.impl__swap #u8 true vec (sz 0) (sz 1) + in vec let h (x: u8) : u8 = @@ -266,14 +270,16 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) } + { x with f_a = Core.Slice.impl__swap #u8 true x.f_a (sz 0) (sz 1) } <: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = { x with - f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo + f_b + = + { x.f_b with f_field = Core.Slice.impl__swap #u8 true x.f_b.f_field (sz 0) (sz 1) } <: t_Foo } <: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index f99f13441..b74e269ab 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -37,7 +37,7 @@ open FStar.Mul /// Helper function let add3 (x y z: u32) : u32 = - Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z + Core.Num.impl__u32__wrapping_add true (Core.Num.impl__u32__wrapping_add true x y <: u32) z /// Question mark without error coercion let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) @@ -99,7 +99,9 @@ let early_returns (x: u32) : u32 = in let! hoist8:Rust_primitives.Hax.t_Never = Core.Ops.Control_flow.ControlFlow_Break - (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x) + (Core.Num.impl__u32__wrapping_add true + (Core.Num.impl__u32__wrapping_add true 123ul hoist5 <: u32) + x) <: Core.Ops.Control_flow.t_ControlFlow u32 Rust_primitives.Hax.t_Never in @@ -110,12 +112,12 @@ let early_returns (x: u32) : u32 = /// Exercise local mutation with control flow and loops let local_mutation (x: u32) : u32 = let y:u32 = 0ul in - let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in + let x:u32 = Core.Num.impl__u32__wrapping_add true x 1ul in if x >. 3ul then - let x:u32 = Core.Num.impl__u32__wrapping_sub x 3ul in + let x:u32 = Core.Num.impl__u32__wrapping_sub true x 3ul in let y:u32 = x /! 2ul in - let y:u32 = Core.Num.impl__u32__wrapping_add y 2ul in + let y:u32 = Core.Num.impl__u32__wrapping_add true y 2ul in let y:u32 = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u32) @@ -128,24 +130,24 @@ let local_mutation (x: u32) : u32 = (fun y i -> let y:u32 = y in let i:u32 = i in - Core.Num.impl__u32__wrapping_add x i <: u32) + Core.Num.impl__u32__wrapping_add true x i <: u32) in - Core.Num.impl__u32__wrapping_add x y + Core.Num.impl__u32__wrapping_add true x y else let (x, y), hoist15:((u32 & u32) & u32) = match x with | 12ul -> - let y:u32 = Core.Num.impl__u32__wrapping_add x y in + let y:u32 = Core.Num.impl__u32__wrapping_add true x y in (x, y <: (u32 & u32)), 3ul <: ((u32 & u32) & u32) | 13ul -> - let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in - (x, y <: (u32 & u32)), add3 x (Core.Num.impl__u32__wrapping_add 123ul x <: u32) x + let x:u32 = Core.Num.impl__u32__wrapping_add true x 1ul in + (x, y <: (u32 & u32)), add3 x (Core.Num.impl__u32__wrapping_add true 123ul x <: u32) x <: ((u32 & u32) & u32) | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32) in let x:u32 = hoist15 in - Core.Num.impl__u32__wrapping_add x y + Core.Num.impl__u32__wrapping_add true x y /// Test question mark on `Option`s with some control flow let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 = @@ -157,7 +159,7 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. match x with | Core.Option.Option_Some hoist21 -> Core.Ops.Control_flow.ControlFlow_Continue - (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist21 3uy) + (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add true hoist21 3uy) <: Core.Option.t_Option u8) <: @@ -175,7 +177,7 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. (match y with | Core.Option.Option_Some hoist23 -> Core.Ops.Control_flow.ControlFlow_Continue - (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist24 hoist23) + (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add true hoist24 hoist23) <: Core.Option.t_Option u8) <: @@ -232,9 +234,8 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. (match y with | Core.Option.Option_Some hoist29 -> Core.Option.Option_Some - (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist28 - <: - u8) + (Core.Num.impl__u8__wrapping_add true + (Core.Num.impl__u8__wrapping_add true v hoist28 <: u8) hoist29) <: Core.Option.t_Option u8 @@ -259,9 +260,9 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 = if x >. 40ul then let y:u32 = 0ul in - let x:u32 = Core.Num.impl__u32__wrapping_add x 3ul in - let y:u32 = Core.Num.impl__u32__wrapping_add x y in - let x:u32 = Core.Num.impl__u32__wrapping_add x y in + let x:u32 = Core.Num.impl__u32__wrapping_add true x 3ul in + let y:u32 = Core.Num.impl__u32__wrapping_add true x y in + let x:u32 = Core.Num.impl__u32__wrapping_add true x y in if x >. 90ul then match Core.Result.Result_Err 12uy <: Core.Result.t_Result Prims.unit u8 with @@ -289,7 +290,7 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 = Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) u32 in Core.Ops.Control_flow.ControlFlow_Continue - (Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 3ul x) + (Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add true 3ul x) <: Core.Result.t_Result u32 u32) <: diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 36079953d..dea9d4b74 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -325,7 +325,9 @@ let impl_SuperTrait_for_i32: t_SuperTrait #i32 = _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; f_function_of_super_trait_pre = (fun (self: i32) -> true); f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true); - f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 + f_function_of_super_trait + = + fun (self: i32) -> cast (Core.Num.impl__i32__abs true self <: i32) <: u32 } class t_Foo (#v_Self: Type0) = {