From 23a5e94bbfd4e856a73409da43e556d4894126f0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Jun 2024 16:43:08 +0200 Subject: [PATCH 01/16] Bump rustc --- cli/driver/src/exporter.rs | 6 +-- cli/driver/src/linter.rs | 2 +- engine/lib/import_thir.ml | 1 + frontend/diagnostics/src/error.rs | 31 +++++++------- frontend/exporter/src/types/copied.rs | 6 +-- frontend/lint/src/lib.rs | 11 +++-- rust-toolchain.toml | 2 +- .../toolchain__literals into-fstar.snap | 5 ++- ..._mut-ref-functionalization into-fstar.snap | 14 +++++-- .../toolchain__side-effects into-fstar.snap | 41 ++++++++++--------- .../toolchain__traits into-fstar.snap | 4 +- 11 files changed, 66 insertions(+), 57 deletions(-) diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index e18d9728d..649fae3b2 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -127,7 +127,7 @@ 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) => { @@ -298,7 +298,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,7 +432,7 @@ impl Callbacks for ExtractionCallbacks { .unwrap(); let out = engine_subprocess.wait_with_output().unwrap(); - let session = compiler.session(); + let session = &compiler.sess; if !out.status.success() { session.fatal(format!( "{} exited with non-zero code {}\nstdout: {}\n stderr: {}", diff --git a/cli/driver/src/linter.rs b/cli/driver/src/linter.rs index ba82517f8..718d9b0a7 100644 --- a/cli/driver/src/linter.rs +++ b/cli/driver/src/linter.rs @@ -28,7 +28,7 @@ impl Callbacks for LinterCallbacks { compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { - let session = compiler.session(); + let session = &compiler.sess; queries .global_ctxt() .unwrap() diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 1a5ab4b08..1a723823c 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 } diff --git a/frontend/diagnostics/src/error.rs b/frontend/diagnostics/src/error.rs index 477c6129f..b52e17fa3 100644 --- a/frontend/diagnostics/src/error.rs +++ b/frontend/diagnostics/src/error.rs @@ -8,13 +8,12 @@ use rustc_session::Session; // 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) { +pub fn explicit_lifetime(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Explicit lifetimes are not supported", @@ -26,7 +25,7 @@ pub fn explicit_lifetime(session: &Lrc, span: Span) { ); } -pub fn mut_borrow_let(session: &Lrc, span: Span) { +pub fn mut_borrow_let(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Mutable borrows are not supported", @@ -38,7 +37,7 @@ pub fn mut_borrow_let(session: &Lrc, span: Span) { ); } -pub fn extern_crate(session: &Lrc, span: Span) { +pub fn extern_crate(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] External items need a model", @@ -50,7 +49,7 @@ pub fn extern_crate(session: &Lrc, span: Span) { ); } -pub fn no_trait_objects(session: &Lrc, span: Span) { +pub fn no_trait_objects(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Trait objects are not supported", @@ -62,7 +61,7 @@ pub fn no_trait_objects(session: &Lrc, span: Span) { ); } -pub fn no_mut_self(session: &Lrc, span: Span) { +pub fn no_mut_self(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Mutable self is not supported", @@ -74,7 +73,7 @@ pub fn no_mut_self(session: &Lrc, span: Span) { ); } -pub fn no_mut(session: &Lrc, span: Span) { +pub fn no_mut(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Mutable arguments are not supported", @@ -86,7 +85,7 @@ pub fn no_mut(session: &Lrc, span: Span) { ); } -pub fn no_assoc_items(session: &Lrc, span: Span) { +pub fn no_assoc_items(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Associated items are not supported", @@ -98,7 +97,7 @@ pub fn no_assoc_items(session: &Lrc, span: Span) { ); } -pub fn unsupported_item(session: &Lrc, span: Span, ident: String) { +pub fn unsupported_item(session: &Session, span: Span, ident: String) { session.span_warn_with_code( span, format!("[Hax] {ident:?} is not supported"), @@ -110,7 +109,7 @@ pub fn unsupported_item(session: &Lrc, span: Span, ident: String) { ); } -pub fn no_fn_mut(session: &Lrc, span: Span) { +pub fn no_fn_mut(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] FnMut is not supported", @@ -122,7 +121,7 @@ pub fn no_fn_mut(session: &Lrc, span: Span) { ); } -pub fn no_where_predicate(session: &Lrc, span: Span) { +pub fn no_where_predicate(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Where predicates are not supported", @@ -134,7 +133,7 @@ pub fn no_where_predicate(session: &Lrc, span: Span) { ); } -pub fn no_async_await(session: &Lrc, span: Span) { +pub fn no_async_await(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Async and await are not supported", @@ -146,7 +145,7 @@ pub fn no_async_await(session: &Lrc, span: Span) { ); } -pub fn no_unsafe(session: &Lrc, span: Span) { +pub fn no_unsafe(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Unsafe code is not supported", @@ -158,7 +157,7 @@ pub fn no_unsafe(session: &Lrc, span: Span) { ); } -pub fn unsupported_loop(session: &Lrc, span: Span) { +pub fn unsupported_loop(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] loop and while are not supported", @@ -170,7 +169,7 @@ pub fn unsupported_loop(session: &Lrc, span: Span) { ); } -pub fn no_union(session: &Lrc, span: Span) { +pub fn no_union(session: &Session, span: Span) { session.span_warn_with_code( span, "[Hax] Unions are not supported", @@ -182,7 +181,7 @@ pub fn no_union(session: &Lrc, span: Span) { ); } -pub fn derive_external_trait(session: &Lrc, span: Span, trait_name: String) { +pub fn derive_external_trait(session: &Session, span: Span, trait_name: String) { session.span_warn_with_code( span, format!("[Hax] Implementation of external trait {trait_name} will require a model"), diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 6904dae02..06063d28f 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), @@ -1941,6 +1941,7 @@ pub enum PatKind { Or { pats: Vec, }, + Never, Error(ErrorGuaranteed), } @@ -3483,7 +3484,6 @@ pub enum ClosureKind { pub enum PredicateKind { Clause(ClauseKind), ObjectSafe(DefId), - ClosureKind(DefId, Vec, ClosureKind), Subtype(SubtypePredicate), Coerce(CoercePredicate), ConstEquate(ConstantExpr, ConstantExpr), @@ -3502,7 +3502,7 @@ 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 hir_id = tcx.local_def_id_to_hir_id(oid); let node = tcx.hir().get(hir_id); use rustc_hir as hir; matches!( diff --git a/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index 6d629876c..174ee36c5 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -21,7 +21,6 @@ use rustc_session::Session; // rustc data_structures extern crate rustc_data_structures; -use rustc_data_structures::sync::Lrc; // rustc ast extern crate rustc_ast; @@ -34,7 +33,7 @@ pub enum Type { } pub struct Linter<'a, 'tcx> { - session: &'a Lrc, + session: &'a Session, tcx: TyCtxt<'tcx>, extern_allow_list: Vec<&'static str>, trait_block_list: Vec, @@ -43,7 +42,7 @@ pub struct Linter<'a, 'tcx> { impl<'a, 'tcx> Linter<'a, 'tcx> { /// Register the linter. - pub fn register(tcx: TyCtxt<'tcx>, session: &'a Lrc, ltype: Type) { + pub fn register(tcx: TyCtxt<'tcx>, session: &'a Session, ltype: Type) { let hir = tcx.hir(); let trait_block_list = vec!["FnMut"]; @@ -481,7 +480,7 @@ 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); @@ -538,7 +537,7 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { } } QPath::TypeRelative(ty, _p) => check_ty_kind(visitor, &ty.kind, span), - QPath::LangItem(_lang_item, _span, _hir_id) => (), + QPath::LangItem(_lang_item, _span) => (), }, _ => (), } @@ -794,7 +793,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); } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0ee9750b5..db9676ec9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-11-16" +channel = "nightly-2023-12-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) = { From eb689539cd74c4a318b512c5fd20a09ab81615aa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Jun 2024 17:20:31 +0200 Subject: [PATCH 02/16] Bump rustc --- cli/driver/src/exporter.rs | 2 +- engine/lib/concrete_ident/concrete_ident.ml | 10 ++++------ engine/names/extract/build.rs | 5 ++--- frontend/exporter/src/constant_utils.rs | 2 +- frontend/exporter/src/types/copied.rs | 10 +++++----- frontend/exporter/src/types/def_id.rs | 5 ++--- frontend/exporter/src/types/todo.rs | 2 ++ rust-toolchain.toml | 2 +- 8 files changed, 18 insertions(+), 20 deletions(-) diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index 649fae3b2..3abe9a828 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -43,7 +43,7 @@ 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)); + session.note(format!("Writing file {:#?}", path)); std::fs::write(&path, file.contents).unwrap_or_else(|e| { session.fatal(format!( "Unable to write to file {:#?}. Error: {:#?}", 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/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/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 06063d28f..92b1d5ea3 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -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`] @@ -2950,7 +2949,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(_, _), @@ -3489,6 +3488,7 @@ pub enum PredicateKind { ConstEquate(ConstantExpr, ConstantExpr), Ambiguous, AliasRelate(Term, Term, AliasRelationDirection), + NormalizesTo(NormalizesTo), } /// Reflects [`rustc_hir::GenericBounds`] @@ -3503,7 +3503,7 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene let use_item_bounds = { if let Some(oid) = s.owner_id().as_local() { let hir_id = tcx.local_def_id_to_hir_id(oid); - let node = tcx.hir().get(hir_id); + 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/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/rust-toolchain.toml b/rust-toolchain.toml index db9676ec9..9058ae52d 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-12-01" +channel = "nightly-2023-12-15" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From 8124bf4174cf656ede51ff68370a432f8eda9b4c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Jun 2024 17:44:49 +0200 Subject: [PATCH 03/16] Bump rustc --- cli/driver/src/exporter.rs | 22 ++++----- engine/lib/import_thir.ml | 10 ++-- frontend/diagnostics/src/error.rs | 66 ++++++++++++------------- frontend/diagnostics/src/lib.rs | 3 +- frontend/exporter/src/types/copied.rs | 7 ++- frontend/exporter/src/types/mir.rs | 2 +- frontend/exporter/src/utils.rs | 2 +- frontend/lint/src/lib.rs | 69 +++++++++++++-------------- rust-toolchain.toml | 2 +- 9 files changed, 91 insertions(+), 92 deletions(-) diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index 3abe9a828..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(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 )) @@ -131,7 +130,7 @@ fn precompute_local_thir_bodies<'tcx>( 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)); } }; @@ -432,9 +431,8 @@ impl Callbacks for ExtractionCallbacks { .unwrap(); let out = engine_subprocess.wait_with_output().unwrap(); - let session = &compiler.sess; 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/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 1a723823c..254084df4 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1360,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 @@ -1368,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, @@ -1416,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/frontend/diagnostics/src/error.rs b/frontend/diagnostics/src/error.rs index b52e17fa3..1eb614c29 100644 --- a/frontend/diagnostics/src/error.rs +++ b/frontend/diagnostics/src/error.rs @@ -1,10 +1,6 @@ // 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; @@ -13,8 +9,8 @@ extern crate rustc_data_structures; extern crate rustc_span; use rustc_span::Span; -pub fn explicit_lifetime(session: &Session, 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 { @@ -25,8 +21,8 @@ pub fn explicit_lifetime(session: &Session, span: Span) { ); } -pub fn mut_borrow_let(session: &Session, 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 { @@ -37,8 +33,8 @@ pub fn mut_borrow_let(session: &Session, span: Span) { ); } -pub fn extern_crate(session: &Session, 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 { @@ -49,8 +45,8 @@ pub fn extern_crate(session: &Session, span: Span) { ); } -pub fn no_trait_objects(session: &Session, 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 { @@ -61,8 +57,8 @@ pub fn no_trait_objects(session: &Session, span: Span) { ); } -pub fn no_mut_self(session: &Session, 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 { @@ -73,8 +69,8 @@ pub fn no_mut_self(session: &Session, span: Span) { ); } -pub fn no_mut(session: &Session, 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 { @@ -85,8 +81,8 @@ pub fn no_mut(session: &Session, span: Span) { ); } -pub fn no_assoc_items(session: &Session, 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 { @@ -97,8 +93,8 @@ pub fn no_assoc_items(session: &Session, span: Span) { ); } -pub fn unsupported_item(session: &Session, 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 { @@ -109,8 +105,8 @@ pub fn unsupported_item(session: &Session, span: Span, ident: String) { ); } -pub fn no_fn_mut(session: &Session, 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 { @@ -121,8 +117,8 @@ pub fn no_fn_mut(session: &Session, span: Span) { ); } -pub fn no_where_predicate(session: &Session, 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 { @@ -133,8 +129,8 @@ pub fn no_where_predicate(session: &Session, span: Span) { ); } -pub fn no_async_await(session: &Session, 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 { @@ -145,8 +141,8 @@ pub fn no_async_await(session: &Session, span: Span) { ); } -pub fn no_unsafe(session: &Session, 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 { @@ -157,8 +153,8 @@ pub fn no_unsafe(session: &Session, span: Span) { ); } -pub fn unsupported_loop(session: &Session, 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 { @@ -169,8 +165,8 @@ pub fn unsupported_loop(session: &Session, span: Span) { ); } -pub fn no_union(session: &Session, 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 { @@ -181,8 +177,8 @@ pub fn no_union(session: &Session, span: Span) { ); } -pub fn derive_external_trait(session: &Session, 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/types/copied.rs b/frontend/exporter/src/types/copied.rs index 92b1d5ea3..f6f873543 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1669,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( @@ -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), } 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/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 174ee36c5..b1d694b52 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::*, *}; @@ -69,6 +73,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 { @@ -82,7 +90,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; } @@ -144,7 +152,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; } @@ -211,14 +219,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(); @@ -273,7 +281,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; } @@ -316,7 +324,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) } } _ => (), @@ -363,20 +371,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) { @@ -435,13 +441,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!( @@ -453,7 +452,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); } @@ -487,9 +486,9 @@ impl<'v, 'a> Visitor<'v> for Linter<'a, 'v> { 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 @@ -501,14 +500,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) } } _ => (), @@ -520,7 +519,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) => { @@ -533,7 +532,7 @@ 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), @@ -549,19 +548,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 { @@ -582,7 +581,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, ); @@ -599,7 +598,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) } _ => (), }, @@ -612,12 +611,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 @@ -863,7 +862,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 9058ae52d..bdb122218 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-12-15" +channel = "nightly-2024-01-01" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From a8d0a7d968764bdabc3cb141903b7be19d3bc2d3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 14 Jun 2024 09:59:10 +0200 Subject: [PATCH 04/16] `Linter` no longer needs to hold on to a `Session` --- cli/driver/src/linter.rs | 3 +-- frontend/lint/src/lib.rs | 16 +++++----------- 2 files changed, 6 insertions(+), 13 deletions(-) diff --git a/cli/driver/src/linter.rs b/cli/driver/src/linter.rs index 718d9b0a7..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.sess; 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/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index b1d694b52..c7b074f57 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -19,10 +19,6 @@ 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; @@ -36,17 +32,16 @@ pub enum Type { Hacspec, } -pub struct Linter<'a, 'tcx> { - session: &'a Session, +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 Session, ltype: Type) { + pub fn register(tcx: TyCtxt<'tcx>, ltype: Type) { let hir = tcx.hir(); let trait_block_list = vec!["FnMut"]; @@ -65,7 +60,6 @@ impl<'a, 'tcx> Linter<'a, 'tcx> { } let mut linter = Self { - session, tcx, extern_allow_list, trait_block_list, @@ -118,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; @@ -183,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 { From a4c0c2679e829e2705bda071052b158a041c9764 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 09:53:03 +0200 Subject: [PATCH 05/16] Add nix utility to retrieve the rustc commit for the given toolchain --- flake.nix | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/flake.nix b/flake.nix index b85e532e6..f63a2ebdb 100644 --- a/flake.nix +++ b/flake.nix @@ -85,6 +85,15 @@ check-toolchain = checks.toolchain; check-examples = checks.examples; check-readme-coherency = checks.readme-coherency; + + # The commit that corresponds to our nightly pin, helpful when updating rusrc. + toolchain_commit = pkgs.runCommand "hax-toolchain-commit" { } '' + # This is sad but I don't know a better way. + cat ${rustc}/share/doc/rust/html/version_info.html \ + | grep 'github.com' \ + | sed 's#.*"https://github.com/rust-lang/rust/commit/\([^"]*\)".*#\1#' \ + > $out + ''; }; checks = { toolchain = packages.hax.tests; From 241c7f617bfe9897b7e1bbc0cd2de78c4e09f490 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 10:53:27 +0200 Subject: [PATCH 06/16] Update rustc --- frontend/diagnostics/src/error.rs | 147 ++++++++------------------ frontend/diagnostics/src/lib.rs | 6 +- frontend/exporter/src/traits.rs | 2 +- frontend/exporter/src/types/copied.rs | 19 ++-- frontend/exporter/src/types/mir.rs | 2 +- frontend/exporter/src/utils.rs | 4 +- frontend/lint/src/lib.rs | 4 - rust-toolchain.toml | 2 +- 8 files changed, 58 insertions(+), 128 deletions(-) diff --git a/frontend/diagnostics/src/error.rs b/frontend/diagnostics/src/error.rs index 1eb614c29..449b50762 100644 --- a/frontend/diagnostics/src/error.rs +++ b/frontend/diagnostics/src/error.rs @@ -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; @@ -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, 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", ); } diff --git a/frontend/diagnostics/src/lib.rs b/frontend/diagnostics/src/lib.rs index 6ca4e2d82..63ce5ad8a 100644 --- a/frontend/diagnostics/src/lib.rs +++ b/frontend/diagnostics/src/lib.rs @@ -19,11 +19,7 @@ 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()); - self.span_err_with_code( - span, - format!("{}", diag), - rustc_errors::DiagnosticId::Error(diag.kind.code().into()), - ); + self.span_err(span, diag.to_string()); } } diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 648e45092..5cb43f3be 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -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); } } diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index f6f873543..57dc2588c 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -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, + pub guard: Option, pub body: Expr, pub lint_level: LintLevel, pub scope: Scope, @@ -2045,6 +2036,12 @@ pub enum LitKind { Err, } +impl SInto 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 @@ -2596,7 +2593,7 @@ pub struct FnHeader { pub type ThirBody = Expr; -impl<'x, 'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_hir::Ty<'x> { +impl<'x: 'tcx, 'tcx, S: UnderOwnerState<'tcx>> SInto 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 diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 3a2e2feee..d5e3f3647 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -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, - args: Vec, + args: Vec>, destination: Place, target: Option, unwind: UnwindAction, diff --git a/frontend/exporter/src/utils.rs b/frontend/exporter/src/utils.rs index d5e77d23c..fc5691f44 100644 --- a/frontend/exporter/src/utils.rs +++ b/frontend/exporter/src/utils.rs @@ -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)!", diff --git a/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index c7b074f57..6850d2fd7 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -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) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index bdb122218..3bdcdfb71 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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" ] From 50b195bbc360eb63a2be578c502d76ada80c95e6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 11:50:34 +0200 Subject: [PATCH 07/16] Update rustc --- cli/driver/src/exporter.rs | 22 ++++++++++------- engine/lib/concrete_ident/concrete_ident.ml | 2 ++ engine/lib/import_thir.ml | 2 +- engine/names/extract/build.rs | 2 +- frontend/exporter/src/state.rs | 2 +- frontend/exporter/src/traits.rs | 2 +- frontend/exporter/src/types/copied.rs | 16 ++++++++++--- frontend/exporter/src/types/def_id.rs | 1 + frontend/exporter/src/types/mir.rs | 2 ++ hax-lib-macros/src/quote.rs | 1 - hax-lib-macros/src/syn_ext.rs | 18 +++++++------- hax-lib-macros/src/utils.rs | 24 +++++++++---------- rust-toolchain.toml | 2 +- ...oolchain__attribute-opaque into-fstar.snap | 2 +- .../toolchain__attributes into-fstar.snap | 2 +- .../toolchain__enum-repr into-coq.snap | 2 +- .../toolchain__enum-repr into-fstar.snap | 2 +- .../toolchain__enum-repr into-ssprove.snap | 2 +- .../snapshots/toolchain__fnmut lint-rust.snap | 20 ++++++++++++++-- .../toolchain__generics into-fstar.snap | 2 +- .../toolchain__interface-only into-fstar.snap | 2 +- .../toolchain__literals into-coq.snap | 2 +- .../toolchain__literals into-fstar.snap | 2 +- .../toolchain__loops into-fstar.snap | 2 +- .../toolchain__mut_arg lint-hacspec.snap | 4 +++- .../toolchain__pattern-or into-coq.snap | 2 +- .../toolchain__pattern-or into-fstar.snap | 2 +- .../toolchain__recursion into-fstar.snap | 2 +- .../toolchain__side-effects into-fstar.snap | 2 +- .../toolchain__side-effects into-ssprove.snap | 3 +-- .../snapshots/toolchain__slices into-coq.snap | 2 +- .../toolchain__slices into-fstar.snap | 2 +- .../toolchain__v1-lib lint-hacspec.snap | 4 +++- 33 files changed, 98 insertions(+), 61 deletions(-) diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index cfb89e165..fce600ac1 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -54,17 +54,21 @@ fn write_files( type ThirBundle<'tcx> = (Rc>, ExprId); /// Generates a dummy THIR body with an error literal as first expression -fn dummy_thir_body<'tcx>(tcx: TyCtxt<'tcx>, span: rustc_span::Span) -> ThirBundle<'tcx> { +fn dummy_thir_body<'tcx>( + tcx: TyCtxt<'tcx>, + span: rustc_span::Span, + guar: rustc_errors::ErrorGuaranteed, +) -> ThirBundle<'tcx> { use rustc_middle::thir::*; let ty = tcx.mk_ty_from_kind(rustc_type_ir::TyKind::Never); let mut thir = Thir::new(BodyTy::Const(ty)); - const ERR_LITERAL: &'static rustc_hir::Lit = &rustc_span::source_map::Spanned { - node: rustc_ast::ast::LitKind::Err, + let lit_err = tcx.hir_arena.alloc(rustc_span::source_map::Spanned { + node: rustc_ast::ast::LitKind::Err(guar), span: rustc_span::DUMMY_SP, - }; + }); let expr = thir.exprs.push(Expr { kind: ExprKind::Literal { - lit: ERR_LITERAL, + lit: lit_err, neg: false, }, ty, @@ -130,11 +134,11 @@ fn precompute_local_thir_bodies<'tcx>( let (thir, expr) = match tcx.thir_body(ldid) { Ok(x) => x, Err(e) => { - tcx.dcx().span_err( + let guar = tcx.dcx().span_err( span, "While trying to reach a body's THIR defintion, got a typechecking error.", ); - return (ldid, dummy_thir_body(tcx, span)); + return (ldid, dummy_thir_body(tcx, span, guar)); } }; let thir = match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { @@ -142,8 +146,8 @@ fn precompute_local_thir_bodies<'tcx>( })) { Ok(x) => x, Err(e) => { - 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)); + let guar = 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, guar)); } }; tracing::debug!("✅ Type-checked THIR body for {:#?}", ldid); diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 237be4494..35907afa2 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -18,6 +18,7 @@ module Imported = struct | Closure | Ctor | AnonConst + | AnonAdt | OpaqueTy | TypeNs of string | ValueNs of string @@ -39,6 +40,7 @@ module Imported = struct | ValueNs s -> ValueNs s | MacroNs s -> MacroNs s | LifetimeNs s -> LifetimeNs s + | AnonAdt -> AnonAdt let of_disambiguated_def_path_item : Types.disambiguated_def_path_item -> disambiguated_def_path_item = diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 254084df4..bec506d55 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -161,7 +161,7 @@ let c_lit' span negative (lit : Thir.lit_kind) (ty : ty) : extended_literal = ^ "] instead.") in match lit with - | Err -> + | Err _ -> assertion_failure [ span ] "[import_thir:literal] got an error literal: this means the Rust \ compiler or Hax's frontend probably reported errors above." diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs index e4285a518..4c25e6e53 100644 --- a/engine/names/extract/build.rs +++ b/engine/names/extract/build.rs @@ -1,4 +1,3 @@ -use serde_json; use serde_json::Value; use std::process::{Command, Stdio}; @@ -50,6 +49,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String { DefPathItem::Ctor => "Ctor".into(), DefPathItem::AnonConst => "AnonConst".into(), DefPathItem::OpaqueTy => "OpaqueTy".into(), + DefPathItem::AnonAdt => "AnonAdt".into(), } } diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 2b70d4df9..c84d05dd5 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -99,7 +99,7 @@ macro_rules! mk { mod types { use crate::prelude::*; use std::cell::RefCell; - use std::collections::{HashMap, HashSet}; + use std::collections::HashSet; pub struct LocalContextS { pub vars: HashMap, diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 5cb43f3be..83f570102 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -403,7 +403,7 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>( let s = &with_owner_id(s.base(), (), (), impl_trait_ref.def_id()); clause.predicate_id(s) }; - let new_clause = clause.subst_supertrait(tcx, &impl_trait_ref); + let new_clause = clause.instantiate_supertrait(tcx, &impl_trait_ref); let impl_expr = new_clause .as_predicate() .to_opt_poly_trait_pred()? diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 57dc2588c..449f9fea6 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -736,6 +736,7 @@ pub enum DesugaringKind { Await, ForLoop, WhileLoop, + BoundModifier, } /// Reflects [`rustc_span::hygiene::AstPass`] @@ -1100,6 +1101,15 @@ pub enum TokenKind { Todo(String), } +impl SInto for rustc_ast::token::IdentIsRaw { + fn sinto(&self, _s: &S) -> bool { + match self { + Self::Yes => true, + Self::No => false, + } + } +} + /// Reflects [`rustc_ast::token::Token`] #[derive(AdtInto)] #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_ast::token::Token, state: S as gstate)] @@ -1179,7 +1189,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto for rustc_middle::thir::Expr<'tcx> let contents = kind.sinto(s); use crate::rustc_middle::ty::util::IntTypeExt; let repr_type = tcx - .repr_options_of_def(def.did()) + .repr_options_of_def(def.did().as_local().unwrap()) .discr_type() .to_ty(s.base().tcx); if repr_type == ty { @@ -2033,7 +2043,7 @@ pub enum LitKind { Int(u128, LitIntType), Float(Symbol, LitFloatType), Bool(bool), - Err, + Err(ErrorGuaranteed), } impl SInto for rustc_data_structures::packed::Pu128 { @@ -3051,7 +3061,7 @@ pub enum ItemKind { Generics, #[value({ let tcx = s.base().tcx; - tcx.repr_options_of_def(s.owner_id()).sinto(s) + tcx.repr_options_of_def(s.owner_id().as_local().unwrap()).sinto(s) })] ReprOptions, ), diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index e92a2f07b..bed97280a 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -61,4 +61,5 @@ pub enum DefPathItem { Ctor, AnonConst, OpaqueTy, + AnonAdt, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index d5e3f3647..1bbe9ef3d 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -900,6 +900,7 @@ pub enum AggregateKind { })] Closure(DefId, Vec, Vec, MirPolyFnSig), Coroutine(DefId, Vec), + CoroutineClosure(DefId, Vec), } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] @@ -924,6 +925,7 @@ pub enum NullOp { SizeOf, AlignOf, OffsetOf(Vec<(usize, FieldIdx)>), + DebugAssertions, } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs index b06927817..24e0c81e4 100644 --- a/hax-lib-macros/src/quote.rs +++ b/hax-lib-macros/src/quote.rs @@ -13,7 +13,6 @@ //! - `:`, the antiquotation is a type. use crate::prelude::*; -use quote::ToTokens; /// Marker that indicates a place where a antiquotation will be inserted const SPLIT_MARK: &str = "SPLIT_QUOTE"; diff --git a/hax-lib-macros/src/syn_ext.rs b/hax-lib-macros/src/syn_ext.rs index c9a5e7312..0620fc31f 100644 --- a/hax-lib-macros/src/syn_ext.rs +++ b/hax-lib-macros/src/syn_ext.rs @@ -7,15 +7,15 @@ pub struct ExprClosure1 { pub body: syn::Expr, } -pub trait PatExt { - // Make sure to remove type ascriptions - fn untype(mut pat: syn::Pat) -> syn::Pat { - if let syn::Pat::Type(sub) = pat { - pat = *sub.pat.clone(); - } - pat - } -} +// pub trait PatExt { +// // Make sure to remove type ascriptions +// fn untype(mut pat: syn::Pat) -> syn::Pat { +// if let syn::Pat::Type(sub) = pat { +// pat = *sub.pat.clone(); +// } +// pat +// } +// } impl Parse for ExprClosure1 { fn parse(ps: ParseStream) -> Result { diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index 4c9247b27..f6d7c995b 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -1,19 +1,19 @@ use crate::prelude::*; use crate::rewrite_self::*; -pub trait BlockExt { - /// Bring in the scope of the block quantifiers helpers (the `forall` and `exists` functions) - fn make_quantifiers_available(&mut self); -} +// pub trait BlockExt { +// /// Bring in the scope of the block quantifiers helpers (the `forall` and `exists` functions) +// fn make_quantifiers_available(&mut self); +// } -impl BlockExt for Block { - fn make_quantifiers_available(&mut self) { - self.stmts.insert( - 0, - Stmt::Item(Item::Verbatim(HaxQuantifiers.to_token_stream())), - ); - } -} +// impl BlockExt for Block { +// fn make_quantifiers_available(&mut self) { +// self.stmts.insert( +// 0, +// Stmt::Item(Item::Verbatim(HaxQuantifiers.to_token_stream())), +// ); +// } +// } /// `HaxQuantifiers` expands to the definition of the `forall` and `exists` functions pub struct HaxQuantifiers; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 3bdcdfb71..6344e680a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-02-01" +channel = "nightly-2024-03-01" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index 3e5e8e8fb..fd801bc73 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -25,7 +25,7 @@ info: exit = 0 stderr = ''' Compiling attribute-opaque v0.1.0 (WORKSPACE_ROOT/attribute-opaque) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index d49db0fb5..31c1426ac 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -79,7 +79,7 @@ open FStar.Mul type t_Foo = | Foo : u8 -> t_Foo [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo = +let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo true = { f_Output = t_Foo; f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8)); diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap index 0a0fb4381..0190e2c33 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap index a12f5701a..d58e0846e 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap index 17f556d1b..3f57950ad 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__fnmut lint-rust.snap b/test-harness/src/snapshots/toolchain__fnmut lint-rust.snap index dfaf541c2..e8caed1c8 100644 --- a/test-harness/src/snapshots/toolchain__fnmut lint-rust.snap +++ b/test-harness/src/snapshots/toolchain__fnmut lint-rust.snap @@ -17,6 +17,8 @@ info: snapshot: stderr: true stdout: true + include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' @@ -33,6 +35,20 @@ warning: [Hax] FnMut is not supported 16 | F: FnMut(u32) -> u8, | ^^^^^ -warning: `fnmut` (lib) generated 2 warnings - Finished dev [unoptimized + debuginfo] target(s) in XXs''' +warning: trait `SomeTrait` is never used + --> lint/rust/fnmut/src/lib.rs:5:7 + | +5 | trait SomeTrait { + | ^^^^^^^^^ + | + = note: `#[warn(dead_code)]` on by default + +warning: struct `UpdatableStruct` is never constructed + --> lint/rust/fnmut/src/lib.rs:11:8 + | +11 | struct UpdatableStruct {} + | ^^^^^^^^^^^^^^^ + +warning: `fnmut` (lib) generated 4 warnings + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' stdout = '' diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index 33d524da6..a69b5ac9b 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling generics v0.1.0 (WORKSPACE_ROOT/generics) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap index e4173e16e..66e83f692 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling interface-only v0.1.0 (WORKSPACE_ROOT/cli/interface-only) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index fa56c7eca..ae2c4990e 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling literals v0.1.0 (WORKSPACE_ROOT/literals) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index f9c9c6e1b..0d38b1b32 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling literals v0.1.0 (WORKSPACE_ROOT/literals) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 169518fc5..9fbd8e950 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling loops v0.1.0 (WORKSPACE_ROOT/loops) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__mut_arg lint-hacspec.snap b/test-harness/src/snapshots/toolchain__mut_arg lint-hacspec.snap index 82d85c40c..e6dda41ca 100644 --- a/test-harness/src/snapshots/toolchain__mut_arg lint-hacspec.snap +++ b/test-harness/src/snapshots/toolchain__mut_arg lint-hacspec.snap @@ -17,6 +17,8 @@ info: snapshot: stderr: true stdout: true + include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' @@ -28,5 +30,5 @@ warning: [Hax] Mutable arguments are not supported | ^^^^^ warning: `mut_arg` (lib) generated 1 warning - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' stdout = '' diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap index 982cd7001..58a1d4c4d 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling pattern-or v0.1.0 (WORKSPACE_ROOT/pattern-or) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap index 7f00c86cf..72caa49b6 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling pattern-or v0.1.0 (WORKSPACE_ROOT/pattern-or) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__recursion into-fstar.snap b/test-harness/src/snapshots/toolchain__recursion into-fstar.snap index 2f2f67f10..a6ab18608 100644 --- a/test-harness/src/snapshots/toolchain__recursion into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__recursion into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling recursion v0.1.0 (WORKSPACE_ROOT/recursion) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] 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 b74e269ab..87a96102e 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap index b2979b525..43aaaaf48 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -1,6 +1,5 @@ --- source: test-harness/src/harness.rs -assertion_line: 214 expression: snapshot info: kind: @@ -24,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__slices into-coq.snap b/test-harness/src/snapshots/toolchain__slices into-coq.snap index df241e88f..03c01f905 100644 --- a/test-harness/src/snapshots/toolchain__slices into-coq.snap +++ b/test-harness/src/snapshots/toolchain__slices into-coq.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling slices v0.1.0 (WORKSPACE_ROOT/slices) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__slices into-fstar.snap b/test-harness/src/snapshots/toolchain__slices into-fstar.snap index e723cddd9..e454a1d6a 100644 --- a/test-harness/src/snapshots/toolchain__slices into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__slices into-fstar.snap @@ -23,7 +23,7 @@ info: exit = 0 stderr = ''' Compiling slices v0.1.0 (WORKSPACE_ROOT/slices) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] diff --git a/test-harness/src/snapshots/toolchain__v1-lib lint-hacspec.snap b/test-harness/src/snapshots/toolchain__v1-lib lint-hacspec.snap index 67c48fc48..8cd6cfa62 100644 --- a/test-harness/src/snapshots/toolchain__v1-lib lint-hacspec.snap +++ b/test-harness/src/snapshots/toolchain__v1-lib lint-hacspec.snap @@ -17,9 +17,11 @@ info: snapshot: stderr: true stdout: true + include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' Compiling v1-lib v0.1.0 (WORKSPACE_ROOT/lint/hacspec/v1-lib) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' stdout = '' From bbbd02d7c07d4cb8ce7463b49494f5bd105fc4f1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 15:14:52 +0200 Subject: [PATCH 08/16] Cleanup --- frontend/exporter/src/types/copied.rs | 4 ++-- hax-lib-macros/src/syn_ext.rs | 10 ---------- hax-lib-macros/src/utils.rs | 14 -------------- 3 files changed, 2 insertions(+), 26 deletions(-) diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 449f9fea6..bd25cd66b 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1189,7 +1189,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto for rustc_middle::thir::Expr<'tcx> let contents = kind.sinto(s); use crate::rustc_middle::ty::util::IntTypeExt; let repr_type = tcx - .repr_options_of_def(def.did().as_local().unwrap()) + .repr_options_of_def(def.did().expect_local()) .discr_type() .to_ty(s.base().tcx); if repr_type == ty { @@ -3061,7 +3061,7 @@ pub enum ItemKind { Generics, #[value({ let tcx = s.base().tcx; - tcx.repr_options_of_def(s.owner_id().as_local().unwrap()).sinto(s) + tcx.repr_options_of_def(s.owner_id().expect_local()).sinto(s) })] ReprOptions, ), diff --git a/hax-lib-macros/src/syn_ext.rs b/hax-lib-macros/src/syn_ext.rs index 0620fc31f..f3a85b28a 100644 --- a/hax-lib-macros/src/syn_ext.rs +++ b/hax-lib-macros/src/syn_ext.rs @@ -7,16 +7,6 @@ pub struct ExprClosure1 { pub body: syn::Expr, } -// pub trait PatExt { -// // Make sure to remove type ascriptions -// fn untype(mut pat: syn::Pat) -> syn::Pat { -// if let syn::Pat::Type(sub) = pat { -// pat = *sub.pat.clone(); -// } -// pat -// } -// } - impl Parse for ExprClosure1 { fn parse(ps: ParseStream) -> Result { let closure: syn::ExprClosure = Parse::parse(ps as ParseStream)?; diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index f6d7c995b..8a998bf78 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -1,20 +1,6 @@ use crate::prelude::*; use crate::rewrite_self::*; -// pub trait BlockExt { -// /// Bring in the scope of the block quantifiers helpers (the `forall` and `exists` functions) -// fn make_quantifiers_available(&mut self); -// } - -// impl BlockExt for Block { -// fn make_quantifiers_available(&mut self) { -// self.stmts.insert( -// 0, -// Stmt::Item(Item::Verbatim(HaxQuantifiers.to_token_stream())), -// ); -// } -// } - /// `HaxQuantifiers` expands to the definition of the `forall` and `exists` functions pub struct HaxQuantifiers; impl ToTokens for HaxQuantifiers { From e1439bf00530a89a4f8b24dc79d8e25b004c6cfc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 15:13:47 +0200 Subject: [PATCH 09/16] Update rustc --- cli/driver/src/callbacks_wrapper.rs | 2 +- cli/driver/src/exporter.rs | 12 +---- cli/options/src/lib.rs | 1 - engine/lib/ast.ml | 9 +++- engine/lib/generic_printer/generic_printer.ml | 6 +-- engine/lib/import_thir.ml | 18 ++++--- engine/lib/print_rust.ml | 6 +-- frontend/exporter/src/constant_utils.rs | 8 ++- frontend/exporter/src/rustc_utils.rs | 2 +- frontend/exporter/src/types/copied.rs | 52 ++++++++++++------- frontend/exporter/src/types/mir.rs | 16 ++---- frontend/exporter/src/types/todo.rs | 1 + frontend/lint/src/lib.rs | 4 +- rust-toolchain.toml | 2 +- 14 files changed, 73 insertions(+), 66 deletions(-) diff --git a/cli/driver/src/callbacks_wrapper.rs b/cli/driver/src/callbacks_wrapper.rs index 3fa124373..209ded8a2 100644 --- a/cli/driver/src/callbacks_wrapper.rs +++ b/cli/driver/src/callbacks_wrapper.rs @@ -14,7 +14,7 @@ pub struct CallbacksWrapper<'a> { impl<'a> Callbacks for CallbacksWrapper<'a> { fn config(&mut self, config: &mut interface::Config) { let options = self.options.clone(); - config.parse_sess_created = Some(Box::new(move |parse_sess| { + config.psess_created = Some(Box::new(move |parse_sess| { parse_sess.env_depinfo.get_mut().insert(( Symbol::intern(hax_cli_options::ENV_VAR_OPTIONS_FRONTEND), Some(Symbol::intern(&serde_json::to_string(&options).unwrap())), diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index fce600ac1..7a62fa8af 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -365,29 +365,19 @@ impl Callbacks for ExtractionCallbacks { include_extra, }; mod from { - pub use hax_cli_options::ExportBodyKind::{ - MirBuilt as MB, MirConst as MC, Thir as T, - }; + pub use hax_cli_options::ExportBodyKind::{MirBuilt as MB, Thir as T}; } mod to { pub type T = hax_frontend_exporter::ThirBody; pub type MB = hax_frontend_exporter::MirBody; - pub type MC = - hax_frontend_exporter::MirBody; } kind.sort(); kind.dedup(); match kind.as_slice() { [from::MB] => driver.to_json::(), - [from::MC] => driver.to_json::(), [from::T] => driver.to_json::(), - [from::MB, from::MC] => driver.to_json::<(to::MB, to::MC)>(), [from::T, from::MB] => driver.to_json::<(to::MB, to::T)>(), - [from::T, from::MC] => driver.to_json::<(to::MC, to::T)>(), - [from::T, from::MB, from::MC] => { - driver.to_json::<(to::MB, (to::MC, to::T))>() - } [] => driver.to_json::<()>(), _ => panic!("Unsupported kind {:#?}", kind), } diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index c50fdc8c8..02e39ef19 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -360,7 +360,6 @@ pub enum ExporterCommand { pub enum ExportBodyKind { Thir, MirBuilt, - MirConst, } #[derive(JsonSchema, Subcommand, Debug, Clone, Serialize, Deserialize)] diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 1fdcb5b93..aff2e8901 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -78,9 +78,14 @@ let show_int_kind { size; signedness } = |> Option.map ~f:Int.to_string |> Option.value ~default:"size") -type float_kind = F32 | F64 [@@deriving show, yojson, hash, compare, eq] +type float_kind = F16 | F32 | F64 | F128 +[@@deriving show, yojson, hash, compare, eq] -let show_float_kind = function F32 -> "f32" | F64 -> "f64" +let show_float_kind = function + | F16 -> "f16" + | F32 -> "f32" + | F64 -> "f64" + | F128 -> "f128" type literal = | String of string diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml index 1193c8e3a..b8788d1ad 100644 --- a/engine/lib/generic_printer/generic_printer.ml +++ b/engine/lib/generic_printer/generic_printer.ml @@ -66,8 +66,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct | Float { value; kind; negative } -> string value |> precede (if negative then minus else empty) - |> terminate - (string (match kind with F32 -> "f32" | F64 -> "f64")) + |> terminate (string (show_float_kind kind)) | Bool b -> OCaml.bool b method generic_value : generic_value fn = @@ -101,8 +100,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct in string signedness ^^ size - method ty_float : float_kind fn = - (function F32 -> "f32" | F64 -> "f64") >> string + method ty_float : float_kind fn = show_float_kind >> string method generic_values : generic_value list fn = function diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index bec506d55..fd87ec0fd 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -82,9 +82,10 @@ let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function | Fake -> unimplemented [ span ] "Shallow borrows" | Mut _ -> Mut W.mutable_reference -let c_binding_mode span : Thir.binding_mode -> binding_mode = function - | ByValue -> ByValue - | ByRef k -> ByRef (c_borrow_kind span k, W.reference) +let c_binding_mode : Thir.by_ref -> binding_mode = function + | No -> ByValue + | Yes true -> ByRef (Mut W.mutable_reference, W.reference) + | Yes false -> ByRef (Shared, W.reference) let unit_typ : ty = TApp { ident = `TupleType 0; args = [] } @@ -800,13 +801,13 @@ end) : EXPR = struct let typ, typ_span = c_canonical_user_type_annotation annotation in let pat = c_pat subpattern in PAscription { typ; typ_span; pat } - | Binding { mode; mutability; subpattern; ty; var; _ } -> - let mut = c_mutability W.mutable_variable mutability in + | Binding { mode; subpattern; ty; var; _ } -> + let mut = c_mutability W.mutable_variable mode.mutability in let subpat = Option.map ~f:(c_pat &&& Fn.const W.as_pattern) subpattern in let typ = c_ty pat.span ty in - let mode = c_binding_mode pat.span mode in + let mode = c_binding_mode mode.by_ref in let var = local_ident Expr var in PBinding { mut; mode; var; typ; subpat } | Variant { info; subpatterns; _ } -> @@ -844,6 +845,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" + | DerefPattern _ -> unimplemented [ pat.span ] "pat DerefPattern" | Never -> unimplemented [ pat.span ] "pat Never" | Error _ -> unimplemented [ pat.span ] "pat Error" in @@ -918,7 +920,9 @@ end) : EXPR = struct | Char -> TChar | Int k -> TInt (c_int_ty k) | Uint k -> TInt (c_uint_ty k) - | Float k -> TFloat (match k with F32 -> F32 | F64 -> F64) + | Float k -> + TFloat + (match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128) | Arrow value -> let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in let inputs = diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index 653e67475..a1ad5f46e 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -76,10 +76,8 @@ module Raw = struct | String s -> "\"" ^ String.escaped s ^ "\"" | Char c -> "'" ^ Char.to_string c ^ "'" | Int { value; _ } -> value - | Float { value; kind = F32; negative } -> - pnegative negative ^ value ^ "f32" - | Float { value; kind = F64; negative } -> - pnegative negative ^ value ^ "f64" + | Float { value; kind; negative } -> + pnegative negative ^ value ^ show_float_kind kind | Bool b -> Bool.to_string b let pprimitive_ident span : _ -> AnnotatedString.t = diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 8e3cf3ef4..bcdbf9e1e 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -389,14 +389,18 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { } impl<'tcx> ConstantExt<'tcx> for ty::Const<'tcx> { fn eval_constant>(&self, s: &S) -> Option { - let evaluated = self.eval(s.base().tcx, s.param_env(), None).ok()?; + let evaluated = self + .eval(s.base().tcx, s.param_env(), rustc_span::DUMMY_SP) + .ok()?; let evaluated = ty::Const::new(s.base().tcx, ty::ConstKind::Value(evaluated), self.ty()); (&evaluated != self).then_some(evaluated) } } impl<'tcx> ConstantExt<'tcx> for mir::Const<'tcx> { fn eval_constant>(&self, s: &S) -> Option { - let evaluated = self.eval(s.base().tcx, s.param_env(), None).ok()?; + let evaluated = self + .eval(s.base().tcx, s.param_env(), rustc_span::DUMMY_SP) + .ok()?; let evaluated = mir::Const::Val(evaluated, self.ty()); (&evaluated != self).then_some(evaluated) } diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs index 23b02744f..023765079 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -198,7 +198,7 @@ pub(crate) fn read_span_from_file(span: &Span) -> Result { #[tracing::instrument(skip(sess))] pub fn translate_span(span: rustc_span::Span, sess: &rustc_session::Session) -> Span { - let smap: &rustc_span::source_map::SourceMap = sess.parse_sess.source_map(); + let smap: &rustc_span::source_map::SourceMap = sess.psess.source_map(); let filename = smap.span_to_filename(span); let lo = smap.lookup_char_pos(span.lo()); diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index bd25cd66b..f6fd4884c 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -981,13 +981,24 @@ pub struct Block { pub safety_mode: BlockSafety, } -/// Reflects [`rustc_middle::thir::BindingMode`] +/// Reflects [`rustc_ast::ast::BindingAnnotation`] #[derive(AdtInto)] -#[args(, from: rustc_middle::thir::BindingMode, state: S as s)] +#[args(, from: rustc_ast::ast::BindingAnnotation, state: S as s)] #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] -pub enum BindingMode { - ByValue, - ByRef(BorrowKind), +pub struct BindingAnnotation { + #[value(self.0.sinto(s))] + pub by_ref: ByRef, + #[value(self.1.sinto(s))] + pub mutability: Mutability, +} + +/// Reflects [`rustc_ast::ast::ByRef`] +#[derive(AdtInto)] +#[args(, from: rustc_ast::ast::ByRef, state: S as s)] +#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] +pub enum ByRef { + Yes(Mutability), + No, } /// Reflects [`rustc_middle::thir::Stmt`] @@ -1391,16 +1402,20 @@ pub enum IntTy { Copy, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, )] pub enum FloatTy { + F16, F32, F64, + F128, } impl<'tcx, S> SInto for rustc_ast::ast::FloatTy { fn sinto(&self, _: &S) -> FloatTy { use rustc_ast::ast::FloatTy as T; match self { + T::F16 => FloatTy::F16, T::F32 => FloatTy::F32, T::F64 => FloatTy::F64, + T::F128 => FloatTy::F128, } } } @@ -1676,7 +1691,7 @@ pub enum Ty { Str, Array(Box, #[map(Box::new(x.sinto(state)))] Box), Slice(Box), - RawPtr(TypeAndMut), + RawPtr(Box, Mutability), Ref(Region, Box, Mutability), Dynamic(Vec>, Region, DynKind), Coroutine(DefId, Vec), @@ -1879,11 +1894,10 @@ pub enum PatKind { subpattern: Pat, }, #[custom_arm( - rustc_middle::thir::PatKind::Binding {mutability, name, mode, var, ty, subpattern, is_primary} => { + rustc_middle::thir::PatKind::Binding {name, mode, var, ty, subpattern, is_primary} => { let local_ctx = gstate.base().local_ctx; local_ctx.borrow_mut().vars.insert(var.clone(), name.to_string()); PatKind::Binding { - mutability: mutability.sinto(gstate), mode: mode.sinto(gstate), var: var.sinto(gstate), ty: ty.sinto(gstate), @@ -1893,8 +1907,7 @@ pub enum PatKind { } )] Binding { - mutability: Mutability, - mode: BindingMode, + mode: BindingAnnotation, var: LocalIdent, // name VS var? TODO ty: Ty, subpattern: Option, @@ -1929,6 +1942,9 @@ pub enum PatKind { Deref { subpattern: Pat, }, + DerefPattern { + subpattern: Pat, + }, Constant { value: ConstantExpr, }, @@ -2070,8 +2086,8 @@ pub struct MacroInvokation { pub enum ImplicitSelfKind { Imm, Mut, - ImmRef, - MutRef, + RefImm, + RefMut, None, } @@ -2612,7 +2628,7 @@ impl<'x: 'tcx, 'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_hir::Ty<'x // access to the HIR of external objects, only their MIR). let ctx = rustc_hir_analysis::collect::ItemCtxt::new(s.base().tcx, s.owner_id().expect_local()); - ctx.to_ty(self).sinto(s) + ctx.lower_ty(self).sinto(s) } } @@ -2711,7 +2727,7 @@ pub enum ParamName { #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub enum LifetimeParamKind { Explicit, - Elided, + Elided(MissingLifetimeKind), Error, } @@ -2959,12 +2975,12 @@ pub struct UsePath { pub res: Vec, pub segments: Vec, #[value(self.segments.iter().last().map_or(None, |segment| { - match s.base().tcx.opt_hir_node_by_def_id(segment.hir_id.owner.def_id) { - Some(rustc_hir::Node::Item(rustc_hir::Item { + match s.base().tcx.hir_node_by_def_id(segment.hir_id.owner.def_id) { + rustc_hir::Node::Item(rustc_hir::Item { ident, kind: rustc_hir::ItemKind::Use(_, _), .. - })) if ident.name.to_ident_string() != "" => Some(ident.name.to_ident_string()), + }) if ident.name.to_ident_string() != "" => Some(ident.name.to_ident_string()), _ => None, } }))] @@ -3238,7 +3254,7 @@ pub struct TraitRef { )] pub struct TraitPredicate { pub trait_ref: TraitRef, - #[map(x.clone() == rustc_middle::ty::ImplPolarity::Positive)] + #[map(x.clone() == rustc_middle::ty::PredicatePolarity::Positive)] #[from(polarity)] pub is_positive: bool, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 1bbe9ef3d..c10fbdf9b 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -90,20 +90,12 @@ pub mod mir_kinds { fn get_mir<'tcx>(tcx: TyCtxt<'tcx>, id: LocalDefId) -> &'tcx Steal>; } #[derive(Clone, Copy, Debug, JsonSchema, Serialize, Deserialize)] - pub struct Const; - impl IsMirKind for Const { - fn get_mir<'tcx>(tcx: TyCtxt<'tcx>, id: LocalDefId) -> &'tcx Steal> { - tcx.mir_const(id) - } - } - #[derive(Clone, Copy, Debug, JsonSchema, Serialize, Deserialize)] pub struct Built; impl IsMirKind for Built { fn get_mir<'tcx>(tcx: TyCtxt<'tcx>, id: LocalDefId) -> &'tcx Steal> { tcx.mir_built(id) } } - // TODO: Add [Promoted] MIR } pub use mir_kinds::IsMirKind; @@ -585,7 +577,7 @@ pub enum TerminatorKind { operands: Vec, options: InlineAsmOptions, line_spans: Vec, - destination: Option, + targets: Vec, unwind: UnwindAction, }, } @@ -613,7 +605,7 @@ pub enum StatementKind { Retag(RetagKind, Place), PlaceMention(Place), AscribeUserType((Place, UserTypeProjection), Variance), - Coverage(Coverage), + Coverage(CoverageKind), Intrinsic(NonDivergingIntrinsic), ConstEvalCounter, Nop, @@ -925,7 +917,7 @@ pub enum NullOp { SizeOf, AlignOf, OffsetOf(Vec<(usize, FieldIdx)>), - DebugAssertions, + UbChecks, } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] @@ -981,11 +973,11 @@ sinto_todo!(rustc_middle::mir, AssertMessage<'tcx>); sinto_todo!(rustc_middle::mir, UnwindAction); sinto_todo!(rustc_middle::mir, FakeReadCause); sinto_todo!(rustc_middle::mir, RetagKind); -sinto_todo!(rustc_middle::mir, Coverage); sinto_todo!(rustc_middle::mir, NonDivergingIntrinsic<'tcx>); sinto_todo!(rustc_middle::mir, UserTypeProjection); sinto_todo!(rustc_middle::mir, MirSource<'tcx>); sinto_todo!(rustc_middle::mir, CoroutineInfo<'tcx>); sinto_todo!(rustc_middle::mir, VarDebugInfo<'tcx>); sinto_todo!(rustc_middle::mir, CallSource); +sinto_todo!(rustc_middle::mir::coverage, CoverageKind); sinto_todo!(rustc_span, ErrorGuaranteed); diff --git a/frontend/exporter/src/types/todo.rs b/frontend/exporter/src/types/todo.rs index f1ae0f8fc..5a92d0d2d 100644 --- a/frontend/exporter/src/types/todo.rs +++ b/frontend/exporter/src/types/todo.rs @@ -15,6 +15,7 @@ sinto_todo!(rustc_hir::def, DefKind); sinto_todo!(rustc_hir, GenericArgs<'a> as HirGenericArgs); sinto_todo!(rustc_hir, InlineAsm<'a>); sinto_todo!(rustc_target::spec::abi, Abi); +sinto_todo!(rustc_hir, MissingLifetimeKind); sinto_todo!(rustc_hir, WhereRegionPredicate<'tcx>); sinto_todo!(rustc_hir, WhereEqPredicate<'tcx>); sinto_todo!(rustc_hir, OwnerId); diff --git a/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index 6850d2fd7..2524196c3 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -291,7 +291,7 @@ impl<'v> Visitor<'v> for Linter<'v> { tracing::trace!("visiting foreign item {:?} at {:?}", i.ident, i.span); walk_foreign_item(self, i) } - fn visit_local(&mut self, l: &'v Local<'v>) { + fn visit_local(&mut self, l: &'v LetStmt<'v>) { tracing::trace!("visiting local {:?}", l.span); walk_local(self, l) } @@ -311,7 +311,7 @@ impl<'v> Visitor<'v> for Linter<'v> { skip_derived_non_local!(self, s.hir_id); match &s.kind { - StmtKind::Local(b) => { + StmtKind::Let(b) => { // tracing::trace!(" local stmt"); if let Some(init) = b.init { match init.kind { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 6344e680a..886c5c183 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-03-01" +channel = "nightly-2024-04-01" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From caaf85b0f282e8d81a89f942f8da404b875a6b42 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 16:21:12 +0200 Subject: [PATCH 10/16] Update rustc --- engine/lib/import_thir.ml | 10 ++++++++-- frontend/exporter/src/traits.rs | 10 ++-------- frontend/exporter/src/types/copied.rs | 28 +++++++++++++++++++++------ frontend/exporter/src/types/mir.rs | 15 +++----------- rust-toolchain.toml | 2 +- 5 files changed, 36 insertions(+), 29 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index fd87ec0fd..c95258a27 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -79,7 +79,7 @@ let c_mutability (witness : 'a) : bool -> 'a Ast.mutability = function let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function | Shared -> Shared - | Fake -> unimplemented [ span ] "Shallow borrows" + | Fake _ -> unimplemented [ span ] "Shallow borrows" | Mut _ -> Mut W.mutable_reference let c_binding_mode : Thir.by_ref -> binding_mode = function @@ -257,6 +257,9 @@ end) : EXPR = struct | Ge -> Core__cmp__PartialOrd__ge | Gt -> Core__cmp__PartialOrd__gt | Eq -> Core__cmp__PartialEq__eq + | Cmp -> + assertion_failure (Span.to_thir span) + "`Cmp` binary operator is not suppored" | Offset -> Core__ptr__const_ptr__Impl__offset in let primitive_names_of_binop : Thir.bin_op -> Concrete_ident.name = function @@ -276,6 +279,9 @@ end) : EXPR = struct | Ge -> Rust_primitives__u128__ge | Gt -> Rust_primitives__u128__gt | Eq -> Rust_primitives__u128__eq + | Cmp -> + assertion_failure (Span.to_thir span) + "`Cmp` binary operator is not suppored" | Offset -> Rust_primitives__offset in let name = @@ -318,7 +324,7 @@ end) : EXPR = struct | Rem -> both int | BitXor | BitAnd | BitOr -> both int <|> both bool | Shl | Shr -> int <*> int - | Lt | Le | Ne | Ge | Gt -> both int <|> both float + | Lt | Le | Ne | Ge | Gt | Cmp -> both int <|> both float | Eq -> both int <|> both float <|> both bool | Offset -> ("", fun _ -> Some "") in diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 83f570102..83fd4423d 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -434,7 +434,7 @@ pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>( pub mod copy_paste_from_rustc { use rustc_infer::infer::TyCtxtInferExt; use rustc_infer::traits::{FulfillmentErrorCode, TraitEngineExt as _}; - use rustc_middle::traits::{CodegenObligationError, DefiningAnchor}; + use rustc_middle::traits::CodegenObligationError; use rustc_middle::ty::{self, TyCtxt}; use rustc_trait_selection::traits::error_reporting::TypeErrCtxtExt; use rustc_trait_selection::traits::{ @@ -456,13 +456,7 @@ pub mod copy_paste_from_rustc { // Do the initial selection for the obligation. This yields the // shallow result we are looking for -- that is, what specific impl. - let infcx = tcx - .infer_ctxt() - .ignoring_regions() - .with_opaque_type_inference(DefiningAnchor::Bubble) - .build(); - //~^ HACK `Bubble` is required for - // this test to pass: type-alias-impl-trait/assoc-projection-ice.rs + let infcx = tcx.infer_ctxt().ignoring_regions().build(); let mut selcx = SelectionContext::new(&infcx); let obligation_cause = ObligationCause::dummy(); diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index f6fd4884c..2a282b701 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -162,6 +162,7 @@ pub enum BinOp { Ne, Ge, Gt, + Cmp, Offset, } @@ -981,11 +982,11 @@ pub struct Block { pub safety_mode: BlockSafety, } -/// Reflects [`rustc_ast::ast::BindingAnnotation`] +/// Reflects [`rustc_ast::ast::BindingMode`] #[derive(AdtInto)] -#[args(, from: rustc_ast::ast::BindingAnnotation, state: S as s)] +#[args(, from: rustc_ast::ast::BindingMode, state: S as s)] #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] -pub struct BindingAnnotation { +pub struct BindingMode { #[value(self.0.sinto(s))] pub by_ref: ByRef, #[value(self.1.sinto(s))] @@ -1092,7 +1093,6 @@ pub enum TokenKind { Comma, Semi, Colon, - ModSep, RArrow, LArrow, FatArrow, @@ -1907,7 +1907,7 @@ pub enum PatKind { } )] Binding { - mode: BindingAnnotation, + mode: BindingMode, var: LocalIdent, // name VS var? TODO ty: Ty, subpattern: Option, @@ -2017,7 +2017,7 @@ pub enum PointerCoercion { )] pub enum BorrowKind { Shared, - Fake, + Fake(FakeBorrowKind), Mut { kind: MutBorrowKind }, } @@ -2033,6 +2033,22 @@ pub enum MutBorrowKind { ClosureCapture, } +/// Reflects [`rustc_middle::mir::FakeBorrowKind`] +#[derive(AdtInto)] +#[args(, from: rustc_middle::mir::FakeBorrowKind, state: S as _s)] +#[derive( + Copy, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, +)] +pub enum FakeBorrowKind { + /// A shared (deep) borrow. Data must be immutable and is aliasable. + Deep, + /// The immediately borrowed place must be immutable, but projections from + /// it don't need to be. This is used to prevent match guards from replacing + /// the scrutinee. For example, a fake borrow of `a.b` doesn't + /// conflict with a mutable borrow of `a.b.c`. + Shallow, +} + /// Reflects [`rustc_ast::ast::StrStyle`] #[derive(AdtInto)] #[args(, from: rustc_ast::ast::StrStyle, state: S as gstate)] diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index c10fbdf9b..d6f01ab8f 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -162,16 +162,6 @@ pub struct Instance { #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::mir::SourceScopeLocalData, state: S as s)] pub struct SourceScopeLocalData { pub lint_root: HirId, - pub safety: Safety, -} - -#[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::mir::Safety, state: S as s)] -pub enum Safety { - Safe, - BuiltinUnsafe, - FnUnsafe, - ExplicitUnsafe(HirId), } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] @@ -893,13 +883,14 @@ pub enum AggregateKind { Closure(DefId, Vec, Vec, MirPolyFnSig), Coroutine(DefId, Vec), CoroutineClosure(DefId, Vec), + RawPtr(Ty, Mutability), } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>, from: rustc_middle::mir::CastKind, state: S as s)] pub enum CastKind { - PointerExposeAddress, - PointerFromExposedAddress, + PointerExposeProvenance, + PointerWithExposedProvenance, PointerCoercion(PointerCoercion), DynStar, IntToInt, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 886c5c183..e81508d48 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-04-01" +channel = "nightly-2024-05-01" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From 34482efc11d43342009238fb832a85c24628ca28 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 16:25:31 +0200 Subject: [PATCH 11/16] Fix type of `Cmp` --- engine/lib/import_thir.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index c95258a27..cc4b69ff0 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -321,10 +321,10 @@ end) : EXPR = struct let expected, f = match op with | Add | Sub | Mul | Div -> both int <|> both float - | Rem -> both int + | Rem | Cmp -> both int | BitXor | BitAnd | BitOr -> both int <|> both bool | Shl | Shr -> int <*> int - | Lt | Le | Ne | Ge | Gt | Cmp -> both int <|> both float + | Lt | Le | Ne | Ge | Gt -> both int <|> both float | Eq -> both int <|> both float <|> both bool | Offset -> ("", fun _ -> Some "") in From ff74ed24a7a99413cfb81e02ca527c269d909742 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 16:48:32 +0200 Subject: [PATCH 12/16] Update rustc --- engine/lib/import_thir.ml | 23 +++++-- frontend/exporter/Cargo.toml | 3 + frontend/exporter/src/sinto.rs | 8 ++- frontend/exporter/src/traits.rs | 15 ++--- frontend/exporter/src/types/copied.rs | 65 +++++++++++-------- frontend/exporter/src/types/mir.rs | 5 +- frontend/exporter/src/types/mir_traits.rs | 4 +- .../exporter/src/types/new/predicate_id.rs | 4 +- frontend/lint/src/lib.rs | 14 ++-- hax-lib/Cargo.toml | 3 + rust-toolchain.toml | 2 +- .../toolchain__literals into-coq.snap | 6 +- .../toolchain__literals into-fstar.snap | 25 ++++--- .../toolchain__loops into-fstar.snap | 2 +- .../snapshots/toolchain__naming into-coq.snap | 6 +- .../toolchain__naming into-fstar.snap | 30 ++++----- 16 files changed, 119 insertions(+), 96 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index cc4b69ff0..ce5a17233 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -257,6 +257,9 @@ end) : EXPR = struct | Ge -> Core__cmp__PartialOrd__ge | Gt -> Core__cmp__PartialOrd__gt | Eq -> Core__cmp__PartialEq__eq + | AddWithOverflow | SubWithOverflow | MulWithOverflow -> + assertion_failure (Span.to_thir span) + "Overflowing binary operators are not suppored" | Cmp -> assertion_failure (Span.to_thir span) "`Cmp` binary operator is not suppored" @@ -279,6 +282,9 @@ end) : EXPR = struct | Ge -> Rust_primitives__u128__ge | Gt -> Rust_primitives__u128__gt | Eq -> Rust_primitives__u128__eq + | AddWithOverflow | SubWithOverflow | MulWithOverflow -> + assertion_failure (Span.to_thir span) + "Overflowing binary operators are not suppored" | Cmp -> assertion_failure (Span.to_thir span) "`Cmp` binary operator is not suppored" @@ -320,7 +326,9 @@ end) : EXPR = struct let name = primitive_names_of_binop op in let expected, f = match op with - | Add | Sub | Mul | Div -> both int <|> both float + | Add | Sub | Mul | AddWithOverflow | SubWithOverflow + | MulWithOverflow | Div -> + both int <|> both float | Rem | Cmp -> both int | BitXor | BitAnd | BitOr -> both int <|> both bool | Shl | Shr -> int <*> int @@ -464,7 +472,10 @@ end) : EXPR = struct (U.call (match op with | Not -> Core__ops__bit__Not__not - | Neg -> Core__ops__arith__Neg__neg) + | Neg -> Core__ops__arith__Neg__neg + | PtrMetadata -> + assertion_failure (Span.to_thir span) + "Unsupported unary operator: `PtrMetadata`") [ c_expr arg ] span typ) .e @@ -889,7 +900,7 @@ end) : EXPR = struct and c_pointer e typ span cast source = match cast with - | ClosureFnPointer Normal | ReifyFnPointer -> + | ClosureFnPointer Safe | ReifyFnPointer -> (* we have arrow types, we do not distinguish between top-level functions and closures *) (c_expr source).e | Unsize -> @@ -1443,7 +1454,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = span = Span.of_thir span; witness = W.macro; } - | Trait (No, Normal, generics, _bounds, items) -> + | Trait (No, Safe, generics, _bounds, items) -> let items = List.filter ~f:(fun { attributes; _ } -> not (should_skip attributes)) @@ -1510,14 +1521,14 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = let attrs = c_item_attrs item.attributes in { span = Span.of_thir item.span; v; ident; attrs }) items - | Impl { unsafety = Unsafe; _ } -> unsafe_block [ item.span ] + | Impl { safety = Unsafe; _ } -> unsafe_block [ item.span ] | Impl { of_trait = Some of_trait; generics; self_ty; items; - unsafety = Normal; + safety = Safe; parent_bounds; _; } -> diff --git a/frontend/exporter/Cargo.toml b/frontend/exporter/Cargo.toml index 3ac731416..fb52c5cad 100644 --- a/frontend/exporter/Cargo.toml +++ b/frontend/exporter/Cargo.toml @@ -23,3 +23,6 @@ tracing.workspace = true paste = "1.0.11" extension-traits = "1.0.1" lazy_static = "1.4.0" + +[features] +extract_names_mode = [] diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs index 6fedd7267..81e24e56e 100644 --- a/frontend/exporter/src/sinto.rs +++ b/frontend/exporter/src/sinto.rs @@ -64,8 +64,12 @@ impl> SInto> for Option { } impl> SInto for Box { fn sinto(&self, s: &S) -> D { - let box x = self; - x.sinto(s) + (**self).sinto(s) + } +} +impl> SInto for &T { + fn sinto(&self, s: &S) -> D { + (**self).sinto(s) } } impl> SInto> for [T] { diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 83fd4423d..55f4e96ae 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -171,7 +171,7 @@ pub(crate) mod search_clause { s: &S, ) -> Vec<( AssocItem, - EarlyBinder)>>, + EarlyBinder<'tcx, Vec<(usize, PolyTraitPredicate<'tcx>)>>, )> { let tcx = s.base().tcx; tcx.associated_items(self.def_id()) @@ -201,12 +201,7 @@ pub(crate) mod search_clause { param_env: rustc_middle::ty::ParamEnv<'tcx>, ) -> Option> { let tcx = s.base().tcx; - if predicate_equality( - self.to_predicate(tcx), - target.to_predicate(tcx), - param_env, - s, - ) { + if predicate_equality(self.upcast(tcx), target.upcast(tcx), param_env, s) { return Some(vec![]); } @@ -336,7 +331,7 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> { let Some((apred, path)) = predicates.into_iter().find_map(|apred| { apred .predicate - .to_opt_poly_trait_pred() + .as_trait_clause() .map(|poly_trait_predicate| poly_trait_predicate) .and_then(|poly_trait_predicate| { poly_trait_predicate.path_to(s, self.clone(), param_env) @@ -350,7 +345,7 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> { use rustc_middle::ty::ToPolyTraitRef; let r#trait = apred .predicate - .to_opt_poly_trait_pred() + .as_trait_clause() .s_unwrap(s) .to_poly_trait_ref() .sinto(s); @@ -406,7 +401,7 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>( let new_clause = clause.instantiate_supertrait(tcx, &impl_trait_ref); let impl_expr = new_clause .as_predicate() - .to_opt_poly_trait_pred()? + .as_trait_clause()? .impl_expr(s, s.param_env()); let mut new_clause_no_binder = new_clause.sinto(s); new_clause_no_binder.id = original_predicate_id; diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 2a282b701..afde9fa63 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -124,6 +124,7 @@ pub struct Decorated { pub enum UnOp { Not, Neg, + PtrMetadata, } /// Reflects [`rustc_middle::mir::BinOp`] @@ -143,6 +144,9 @@ pub enum BinOp { rustc_middle::mir::BinOp::Mul | rustc_middle::mir::BinOp::MulUnchecked => BinOp::Mul, )] Mul, + AddWithOverflow, + SubWithOverflow, + MulWithOverflow, Div, Rem, BitXor, @@ -585,7 +589,6 @@ impl VariantDef { )] #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::EarlyParamRegion, state: S as gstate)] pub struct EarlyParamRegion { - pub def_id: DefId, pub index: u32, pub name: Symbol, } @@ -1536,6 +1539,7 @@ pub enum GenericParamDefKind { pub struct TyGenerics { pub parent: Option, pub parent_count: usize, + #[from(own_params)] pub params: Vec, // pub param_def_id_to_index: FxHashMap, pub has_self: bool, @@ -1577,10 +1581,10 @@ impl Alias { #[tracing::instrument(level = "trace", skip(s))] fn from<'tcx, S: BaseState<'tcx> + HasOwnerId>( s: &S, - alias_kind: &rustc_type_ir::AliasKind, + alias_kind: &rustc_type_ir::AliasTyKind, alias_ty: &rustc_middle::ty::AliasTy<'tcx>, ) -> Self { - use rustc_type_ir::AliasKind as RustAliasKind; + use rustc_type_ir::AliasTyKind as RustAliasKind; let kind = match alias_kind { RustAliasKind::Projection => { use rustc_middle::ty::{Binder, EarlyBinder, TypeVisitableExt}; @@ -1664,7 +1668,7 @@ pub enum Ty { }, FROM_TYPE::Closure (_defid, generics) => { let sig = generics.as_closure().sig(); - let sig = state.base().tcx.signature_unclosure(sig, rustc_hir::Unsafety::Normal); + let sig = state.base().tcx.signature_unclosure(sig, rustc_hir::Safety::Safe); arrow_of_sig(&sig, state) }, )] @@ -1985,15 +1989,15 @@ pub struct Arm { attributes: Vec, } -/// Reflects [`rustc_hir::Unsafety`] +/// Reflects [`rustc_hir::Safety`] #[derive(AdtInto)] -#[args(, from: rustc_hir::Unsafety, state: S as _s)] +#[args(, from: rustc_hir::Safety, state: S as _s)] #[derive( Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, )] -pub enum Unsafety { +pub enum Safety { Unsafe, - Normal, + Safe, } /// Reflects [`rustc_middle::ty::adjustment::PointerCoercion`] @@ -2003,7 +2007,7 @@ pub enum Unsafety { pub enum PointerCoercion { ReifyFnPointer, UnsafeFnPointer, - ClosureFnPointer(Unsafety), + ClosureFnPointer(Safety), MutToConstPointer, ArrayToPointer, Unsize, @@ -2586,7 +2590,7 @@ pub struct TyFnSig { #[value(self.output().sinto(s))] pub output: Ty, pub c_variadic: bool, - pub unsafety: Unsafety, + pub safety: Safety, pub abi: Abi, } @@ -2627,7 +2631,7 @@ pub struct FnSig { #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_hir::FnHeader, state: S as tcx)] pub struct FnHeader { - pub unsafety: Unsafety, + pub safety: Safety, pub constness: Constness, pub asyncness: IsAsync, pub abi: Abi, @@ -2868,7 +2872,7 @@ impl< S, D: Clone, T: SInto + rustc_middle::ty::TypeFoldable>, - > SInto for rustc_middle::ty::EarlyBinder + > SInto for rustc_middle::ty::EarlyBinder<'tcx, T> { fn sinto(&self, s: &S) -> D { self.clone().instantiate_identity().sinto(s) @@ -2880,7 +2884,7 @@ impl< #[args(<'tcx, S: UnderOwnerState<'tcx> >, from: rustc_hir::Impl<'tcx>, state: S as s)] #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub struct Impl { - pub unsafety: Unsafety, + pub safety: Safety, pub polarity: ImplPolarity, pub defaultness: Defaultness, pub defaultness_span: Option, @@ -2940,6 +2944,15 @@ pub enum VariantData { Unit(HirId, GlobalIdent), } +impl SInto for rustc_ast::ast::Recovered { + fn sinto(&self, _s: &S) -> bool { + match self { + Self::Yes(_) => true, + Self::No => false, + } + } +} + /// Reflects [`rustc_hir::FieldDef`] #[derive(AdtInto)] #[args(<'tcx, S: UnderOwnerState<'tcx> >, from: rustc_hir::FieldDef<'tcx>, state: S as s)] @@ -3101,7 +3114,7 @@ pub enum ItemKind { Union(VariantData, Generics), Trait( IsAuto, - Unsafety, + Safety, Generics, GenericBounds, Vec>, @@ -3282,18 +3295,17 @@ pub struct TraitPredicate { #[derive( Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, )] -pub struct OutlivesPredicate { - pub lhs: A, - pub rhs: B, +pub struct OutlivesPredicate { + pub lhs: T, + pub rhs: Region, } -impl<'tcx, S: UnderOwnerState<'tcx>, A1, A2, B1, B2> SInto> - for rustc_middle::ty::OutlivesPredicate +impl<'tcx, S: UnderOwnerState<'tcx>, T, U> SInto> + for rustc_middle::ty::OutlivesPredicate<'tcx, T> where - A1: SInto, - B1: SInto, + T: SInto, { - fn sinto(&self, s: &S) -> OutlivesPredicate where { + fn sinto(&self, s: &S) -> OutlivesPredicate where { OutlivesPredicate { lhs: self.0.sinto(s), rhs: self.1.sinto(s), @@ -3302,9 +3314,9 @@ where } /// Reflects [`rustc_middle::ty::RegionOutlivesPredicate`] -pub type RegionOutlivesPredicate = OutlivesPredicate; +pub type RegionOutlivesPredicate = OutlivesPredicate; /// Reflects [`rustc_middle::ty::TypeOutlivesPredicate`] -pub type TypeOutlivesPredicate = OutlivesPredicate; +pub type TypeOutlivesPredicate = OutlivesPredicate; /// Reflects [`rustc_middle::ty::Term`] #[derive( @@ -3349,13 +3361,14 @@ impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto for rustc_middle::ty::ProjectionPredicate<'tcx> { fn sinto(&self, s: &S) -> ProjectionPredicate { + let tcx = s.base().tcx; let AliasKind::Projection { impl_expr, assoc_item, } = Alias::from( s, - &rustc_middle::ty::AliasKind::Projection, - &self.projection_ty, + &rustc_middle::ty::AliasTyKind::Projection, + &self.projection_term.expect_ty(tcx), ) .kind else { diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index d6f01ab8f..04984afe5 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -802,7 +802,7 @@ pub struct MirFnSig { pub inputs: Vec, pub output: Ty, pub c_variadic: bool, - pub unsafety: Unsafety, + pub safety: Safety, pub abi: Abi, } @@ -816,7 +816,7 @@ impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto for rustc_middle: inputs, output, c_variadic: self.c_variadic, - unsafety: self.unsafety.sinto(s), + safety: self.safety.sinto(s), abi: self.abi.sinto(s), } } @@ -928,7 +928,6 @@ pub enum Rvalue { Len(Place), Cast(CastKind, Operand, Ty), BinaryOp(BinOp, (Operand, Operand)), - CheckedBinaryOp(BinOp, (Operand, Operand)), NullaryOp(NullOp, Ty), UnaryOp(UnOp, Operand), Discriminant(Place), diff --git a/frontend/exporter/src/types/mir_traits.rs b/frontend/exporter/src/types/mir_traits.rs index e74cfaa17..422253a42 100644 --- a/frontend/exporter/src/types/mir_traits.rs +++ b/frontend/exporter/src/types/mir_traits.rs @@ -174,9 +174,9 @@ pub fn get_params_info<'tcx, S: BaseState<'tcx> + HasOwnerId>( let mut num_trait_type_constraints = 0; let generics = tcx.generics_of(def_id); - let num_generic_params = generics.params.len(); + let num_generic_params = generics.own_params.len(); use rustc_middle::ty::GenericParamDefKind; - for param in &generics.params { + for param in &generics.own_params { match param.kind { GenericParamDefKind::Lifetime => num_region_params += 1, GenericParamDefKind::Type { .. } => num_type_params += 1, diff --git a/frontend/exporter/src/types/new/predicate_id.rs b/frontend/exporter/src/types/new/predicate_id.rs index 04fa8b49d..cd71bbe2b 100644 --- a/frontend/exporter/src/types/new/predicate_id.rs +++ b/frontend/exporter/src/types/new/predicate_id.rs @@ -34,8 +34,8 @@ impl<'tcx, S: UnderOwnerState<'tcx>> IntoPredicateId<'tcx, S> for ty::Predicate< impl<'tcx, S: UnderOwnerState<'tcx>> IntoPredicateId<'tcx, S> for ty::PolyTraitPredicate<'tcx> { fn predicate_id(&self, s: &S) -> PredicateId { - use ty::ToPredicate; - let predicate: ty::Predicate<'tcx> = (*self).to_predicate(s.base().tcx); + use ty::Upcast; + let predicate: ty::Predicate<'tcx> = (*self).upcast(s.base().tcx); predicate.predicate_id(s) } } diff --git a/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index 2524196c3..654be8760 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -219,7 +219,7 @@ impl<'v> Visitor<'v> for Linter<'v> { ItemKind::GlobalAsm(_) => error::no_unsafe(self.dcx(), i.span), ItemKind::Impl(imp) => { // tracing::trace!(" impl {:?}", imp.self_ty.kind); - if imp.unsafety == Unsafety::Unsafe { + if imp.safety == Safety::Unsafe { error::no_unsafe(self.dcx(), i.span); } if let Some(of_trait) = &imp.of_trait { @@ -245,7 +245,7 @@ impl<'v> Visitor<'v> for Linter<'v> { // keep going walk_item(self, i); } - fn visit_body(&mut self, b: &'v Body<'v>) { + fn visit_body(&mut self, b: &Body<'v>) { tracing::trace!("visiting body"); skip_derived_non_local!(self, b.value.hir_id); @@ -537,7 +537,7 @@ impl<'v> Visitor<'v> for Linter<'v> { tracing::trace!(" ItemFn: {:?}", ident); // TODO: All this should be an error (span_err_with_code) // Unsafe functions - if header.unsafety == Unsafety::Unsafe { + if header.safety == Safety::Unsafe { error::no_unsafe(self.dcx(), span); } @@ -600,7 +600,7 @@ impl<'v> Visitor<'v> for Linter<'v> { tracing::trace!(" Method: {:?}", ident); // TODO: All this should be an error (span_err_with_code) // Unsafe functions - if sig.header.unsafety == Unsafety::Unsafe { + if sig.header.safety == Safety::Unsafe { error::no_unsafe(self.dcx(), span); } @@ -823,12 +823,12 @@ impl<'v> Visitor<'v> for Linter<'v> { tracing::trace!("visiting generic args {:?}", generic_args.span_ext); walk_generic_args(self, generic_args) } - fn visit_assoc_type_binding(&mut self, type_binding: &'v TypeBinding<'v>) { - tracing::trace!("visiting assoc type binding {:?}", type_binding.span); + fn visit_assoc_item_constraint(&mut self, constraint: &'v AssocItemConstraint<'v>) { + tracing::trace!("visiting assoc item constraint {:?}", constraint.span); // self.no_assoc_items(type_binding.span); // keep going - walk_assoc_type_binding(self, type_binding); + walk_assoc_item_constraint(self, constraint); } fn visit_attribute(&mut self, attr: &'v rustc_ast::ast::Attribute) { tracing::trace!("visiting attribute: {:?}", attr.span); diff --git a/hax-lib/Cargo.toml b/hax-lib/Cargo.toml index 299fd8b8e..5207f0e7b 100644 --- a/hax-lib/Cargo.toml +++ b/hax-lib/Cargo.toml @@ -17,3 +17,6 @@ num-traits = { version = "0.2.15", default-features = false } [features] default = ["macros"] macros = ["dep:hax-lib-macros"] + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)'] } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e81508d48..2dc24fb75 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-05-01" +channel = "nightly-2024-06-01" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index ae2c4990e..60bc0ec80 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -90,13 +90,13 @@ Definition numeric (_ : unit) : unit := let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in tt. +Definition panic_with_msg (_ : unit) : unit := + never_to_any (panic_fmt (impl_2__new_const (array_from_list [with msg]))). + Definition empty_array (_ : unit) : unit := let (_ : seq int8) := unsize !TODO empty array! : seq int8 in tt. -Definition panic_with_msg (_ : unit) : unit := - never_to_any (panic_fmt (impl_2__new_const (unsize (array_from_list [with msg])))). - Record t_Foo : Type := { f_field : int8; }. diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index 0d38b1b32..ff09cf532 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -147,6 +147,18 @@ let numeric (_: Prims.unit) : Prims.unit = let (_: u128):u128 = pub_u128 22222222222222222222 in () +let panic_with_msg (_: Prims.unit) : Prims.unit = + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt true + (Core.Fmt.impl_2__new_const (sz 1) + true + (let list = ["with msg"] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list) + <: + Core.Fmt.t_Arguments) + <: + Rust_primitives.Hax.t_Never) + let empty_array (_: Prims.unit) : Prims.unit = let (_: t_Slice u8):t_Slice u8 = Rust_primitives.unsize (let list:Prims.list u8 = [] in @@ -155,19 +167,6 @@ let empty_array (_: Prims.unit) : Prims.unit = in () -let panic_with_msg (_: Prims.unit) : Prims.unit = - 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) - <: - t_Slice string) - <: - Core.Fmt.t_Arguments) - <: - Rust_primitives.Hax.t_Never) - type t_Foo = { f_field:u8 } let v_CONSTANT: t_Foo = { f_field = 3uy } <: t_Foo diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 9fbd8e950..a0e25da02 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -73,7 +73,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global in let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize) - (Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize) + (Core.Slice.Iter.impl_88__remainder #usize chunks <: t_Slice usize) <: Core.Slice.Iter.t_Iter usize) acc diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap index 49243dce6..a759500c0 100644 --- a/test-harness/src/snapshots/toolchain__naming into-coq.snap +++ b/test-harness/src/snapshots/toolchain__naming into-coq.snap @@ -163,11 +163,11 @@ Open Scope bool_scope. (*Not implemented yet? todo(item)*) Definition debug (label : int32) (value : int32) : unit := - let _ := v__print (impl_2__new_v1 (unsize (array_from_list [[; + let _ := v__print (impl_2__new_v1 (array_from_list [[; ] a=; -])) (unsize (array_from_list [impl_1__new_display label; - impl_1__new_display value]))) : unit in +]) (array_from_list [impl_1__new_display label; + impl_1__new_display value])) : unit in tt. Definition f (_ : unit) : unit := diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index 9162f2abc..1da402b0f 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -34,23 +34,19 @@ open FStar.Mul let debug (label value: u32) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize (let list = - ["["; "] a="; "\n"] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); - Rust_primitives.Hax.array_of_list 3 list) - <: - t_Slice string) - (Rust_primitives.unsize (let list = - [ - Core.Fmt.Rt.impl_1__new_display #u32 label <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl_1__new_display #u32 value <: Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); - Rust_primitives.Hax.array_of_list 2 list) - <: - t_Slice Core.Fmt.Rt.t_Argument) + Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (sz 3) + (sz 2) + (let list = ["["; "] a="; "\n"] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); + Rust_primitives.Hax.array_of_list 3 list) + (let list = + [ + Core.Fmt.Rt.impl_1__new_display #u32 label <: Core.Fmt.Rt.t_Argument; + Core.Fmt.Rt.impl_1__new_display #u32 value <: Core.Fmt.Rt.t_Argument + ] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); + Rust_primitives.Hax.array_of_list 2 list) <: Core.Fmt.t_Arguments) in From 88614bc8ac58facf4887ac0b4dff3ed997c27ed5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 17:35:04 +0200 Subject: [PATCH 13/16] Update rustc --- flake.lock | 9 ++-- flake.nix | 1 - frontend/diagnostics/src/error.rs | 34 +++++++-------- frontend/diagnostics/src/lib.rs | 2 +- frontend/exporter/src/constant_utils.rs | 40 ++++++++++-------- frontend/exporter/src/traits.rs | 32 ++++++++------- frontend/exporter/src/types/copied.rs | 27 ++++++------ frontend/exporter/src/types/mir.rs | 7 ++-- frontend/lint/src/lib.rs | 4 +- rust-toolchain.toml | 2 +- .../toolchain__attributes into-fstar.snap | 2 +- .../toolchain__literals into-fstar.snap | 4 +- ..._mut-ref-functionalization into-fstar.snap | 14 ++----- .../toolchain__side-effects into-fstar.snap | 41 +++++++++---------- .../toolchain__traits into-fstar.snap | 4 +- 15 files changed, 108 insertions(+), 115 deletions(-) diff --git a/flake.lock b/flake.lock index ad39d86a8..cf8bccd66 100644 --- a/flake.lock +++ b/flake.lock @@ -105,19 +105,16 @@ }, "rust-overlay": { "inputs": { - "flake-utils": [ - "flake-utils" - ], "nixpkgs": [ "nixpkgs" ] }, "locked": { - "lastModified": 1717381101, - "narHash": "sha256-TcM4+oHTSLw8neTxk/Q0beODr8YiL+oI2j0ENYnNfk4=", + "lastModified": 1719281921, + "narHash": "sha256-LIBMfhM9pMOlEvBI757GOK5l0R58SRi6YpwfYMbf4yc=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "07098b424d114cd2dddec40be8d5586da339fddc", + "rev": "b6032d3a404d8a52ecfc8571ff0c26dfbe221d07", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index f63a2ebdb..5799df0b0 100644 --- a/flake.nix +++ b/flake.nix @@ -10,7 +10,6 @@ }; rust-overlay = { url = "github:oxalica/rust-overlay"; - inputs.flake-utils.follows = "flake-utils"; inputs.nixpkgs.follows = "nixpkgs"; }; fstar = { diff --git a/frontend/diagnostics/src/error.rs b/frontend/diagnostics/src/error.rs index 449b50762..30c780149 100644 --- a/frontend/diagnostics/src/error.rs +++ b/frontend/diagnostics/src/error.rs @@ -1,6 +1,6 @@ // rustc errors extern crate rustc_errors; -use rustc_errors::DiagCtxt; +use rustc_errors::DiagCtxtHandle; // rustc data_structures extern crate rustc_data_structures; @@ -9,13 +9,13 @@ extern crate rustc_data_structures; extern crate rustc_span; use rustc_span::Span; -fn warn_span_lint(dcx: &DiagCtxt, span: Span, msg: impl AsRef, lint_name: &str) { +fn warn_span_lint(dcx: DiagCtxtHandle<'_>, span: Span, msg: impl AsRef, 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) { +pub fn explicit_lifetime(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -24,7 +24,7 @@ pub fn explicit_lifetime(dcx: &DiagCtxt, span: Span) { ); } -pub fn mut_borrow_let(dcx: &DiagCtxt, span: Span) { +pub fn mut_borrow_let(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -33,11 +33,11 @@ pub fn mut_borrow_let(dcx: &DiagCtxt, span: Span) { ); } -pub fn extern_crate(dcx: &DiagCtxt, span: Span) { +pub fn extern_crate(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint(dcx, span, "[Hax] External items need a model", "External"); } -pub fn no_trait_objects(dcx: &DiagCtxt, span: Span) { +pub fn no_trait_objects(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -46,7 +46,7 @@ pub fn no_trait_objects(dcx: &DiagCtxt, span: Span) { ); } -pub fn no_mut_self(dcx: &DiagCtxt, span: Span) { +pub fn no_mut_self(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -55,7 +55,7 @@ pub fn no_mut_self(dcx: &DiagCtxt, span: Span) { ); } -pub fn no_mut(dcx: &DiagCtxt, span: Span) { +pub fn no_mut(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -64,7 +64,7 @@ pub fn no_mut(dcx: &DiagCtxt, span: Span) { ); } -pub fn no_assoc_items(dcx: &DiagCtxt, span: Span) { +pub fn no_assoc_items(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -73,7 +73,7 @@ pub fn no_assoc_items(dcx: &DiagCtxt, span: Span) { ); } -pub fn unsupported_item(dcx: &DiagCtxt, span: Span, ident: String) { +pub fn unsupported_item(dcx: DiagCtxtHandle<'_>, span: Span, ident: String) { warn_span_lint( dcx, span, @@ -82,11 +82,11 @@ pub fn unsupported_item(dcx: &DiagCtxt, span: Span, ident: String) { ); } -pub fn no_fn_mut(dcx: &DiagCtxt, span: Span) { +pub fn no_fn_mut(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint(dcx, span, "[Hax] FnMut is not supported", "Where"); } -pub fn no_where_predicate(dcx: &DiagCtxt, span: Span) { +pub fn no_where_predicate(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -95,7 +95,7 @@ pub fn no_where_predicate(dcx: &DiagCtxt, span: Span) { ); } -pub fn no_async_await(dcx: &DiagCtxt, span: Span) { +pub fn no_async_await(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -104,15 +104,15 @@ pub fn no_async_await(dcx: &DiagCtxt, span: Span) { ); } -pub fn no_unsafe(dcx: &DiagCtxt, span: Span) { +pub fn no_unsafe(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint(dcx, span, "[Hax] Unsafe code is not supported", "Unsafe"); } -pub fn unsupported_loop(dcx: &DiagCtxt, span: Span) { +pub fn unsupported_loop(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint(dcx, span, "[Hax] loop and while are not supported", "Loops"); } -pub fn no_union(dcx: &DiagCtxt, span: Span) { +pub fn no_union(dcx: DiagCtxtHandle<'_>, span: Span) { warn_span_lint( dcx, span, @@ -121,7 +121,7 @@ pub fn no_union(dcx: &DiagCtxt, span: Span) { ); } -pub fn derive_external_trait(dcx: &DiagCtxt, span: Span, trait_name: String) { +pub fn derive_external_trait(dcx: DiagCtxtHandle<'_>, span: Span, trait_name: String) { warn_span_lint( dcx, span, diff --git a/frontend/diagnostics/src/lib.rs b/frontend/diagnostics/src/lib.rs index 63ce5ad8a..5c7af4bd5 100644 --- a/frontend/diagnostics/src/lib.rs +++ b/frontend/diagnostics/src/lib.rs @@ -19,7 +19,7 @@ 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()); - self.span_err(span, diag.to_string()); + self.handle().span_err(span, diag.to_string()); } } diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index bcdbf9e1e..65b862313 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -200,11 +200,11 @@ pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>( .s_expect(s, "scalar_int_to_constant_literal: expected a bool"), ), ty::Int(kind) => { - let v = x.try_to_int(x.size()).s_unwrap(s); + let v = x.to_int(x.size()); ConstantLiteral::Int(ConstantInt::Int(v, kind.sinto(s))) } ty::Uint(kind) => { - let v = x.try_to_uint(x.size()).s_unwrap(s); + let v = x.to_uint(x.size()); ConstantLiteral::Int(ConstantInt::Uint(v, kind.sinto(s))) } _ => fatal!( @@ -227,7 +227,7 @@ pub(crate) fn scalar_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( // We match on the type and use it to convert the value. let kind = match ty.kind() { ty::Char | ty::Bool | ty::Int(_) | ty::Uint(_) => { - let scalar_int = scalar.try_to_int().unwrap_or_else(|_| { + let scalar_int = scalar.try_to_scalar_int().unwrap_or_else(|_| { fatal!( s[span], "Type is primitive, but the scalar {:#?} is not a [Int]", @@ -330,7 +330,7 @@ impl ConstantExprKind { pub enum TranslateUnevalRes { // TODO: rename - GlobalName(ConstantExprKind), + GlobalName(ConstantExpr), EvaluatedConstant(T), } @@ -344,6 +344,7 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { &self, s: &impl UnderOwnerState<'tcx>, ucv: rustc_middle::ty::UnevaluatedConst<'tcx>, + span: rustc_span::Span, ) -> TranslateUnevalRes { let tcx = s.base().tcx; if is_anon_const(ucv.def, tcx) { @@ -352,7 +353,7 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { supposely_unreachable_fatal!(s, "TranslateUneval"; {self, ucv}); })) } else { - let cv = if let Some(assoc) = s.base().tcx.opt_associated_item(ucv.def) { + let kind = if let Some(assoc) = s.base().tcx.opt_associated_item(ucv.def) { if assoc.trait_item_def_id.is_some() { // This must be a trait declaration constant trait_const_to_constant_expr_kind(s, ucv.def, ucv.args, &assoc) @@ -383,16 +384,18 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { trait_refs: vec![], } }; + let ty = s.base().tcx.type_of(s.owner_id()); + let cv = kind.decorate(ty.sinto(s), span.sinto(s)); TranslateUnevalRes::GlobalName(cv) } } } impl<'tcx> ConstantExt<'tcx> for ty::Const<'tcx> { fn eval_constant>(&self, s: &S) -> Option { - let evaluated = self + let (ty, evaluated) = self .eval(s.base().tcx, s.param_env(), rustc_span::DUMMY_SP) .ok()?; - let evaluated = ty::Const::new(s.base().tcx, ty::ConstKind::Value(evaluated), self.ty()); + let evaluated = ty::Const::new(s.base().tcx, ty::ConstKind::Value(ty, evaluated)); (&evaluated != self).then_some(evaluated) } } @@ -409,26 +412,29 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::Const<'tcx> fn sinto(&self, s: &S) -> ConstantExpr { use rustc_middle::query::Key; let span = self.default_span(s.base().tcx); - let kind = match self.kind() { - ty::ConstKind::Param(p) => ConstantExprKind::ConstRef { id: p.sinto(s) }, + match self.kind() { + ty::ConstKind::Param(p) => { + let kind = ConstantExprKind::ConstRef { id: p.sinto(s) }; + let tcx = s.base().tcx; + let param_env = tcx.param_env(s.owner_id()); + let ty = p.find_ty_from_env(param_env); + kind.decorate(ty.sinto(s), span.sinto(s)) + } ty::ConstKind::Infer(..) => fatal!(s[span], "ty::ConstKind::Infer node? {:#?}", self), - ty::ConstKind::Unevaluated(ucv) => match self.translate_uneval(s, ucv) { + ty::ConstKind::Unevaluated(ucv) => match self.translate_uneval(s, ucv, span) { TranslateUnevalRes::EvaluatedConstant(c) => return c.sinto(s), TranslateUnevalRes::GlobalName(c) => c, }, - ty::ConstKind::Value(valtree) => { - return valtree_to_constant_expr(s, valtree, self.ty(), span) - } + ty::ConstKind::Value(ty, valtree) => valtree_to_constant_expr(s, valtree, ty, span), ty::ConstKind::Error(_) => fatal!(s[span], "ty::ConstKind::Error"), ty::ConstKind::Expr(e) => fatal!(s[span], "ty::ConstKind::Expr {:#?}", e), ty::ConstKind::Bound(i, bound) => { - supposely_unreachable_fatal!(s[span], "ty::ConstKind::Bound"; {i, bound, self.ty()}); + supposely_unreachable_fatal!(s[span], "ty::ConstKind::Bound"; {i, bound}); } _ => fatal!(s[span], "unexpected case"), - }; - kind.decorate(self.ty().sinto(s), span.sinto(s)) + } } } @@ -445,7 +451,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( } (ty::ValTree::Branch(valtrees), ty::Str) => ConstantExprKind::Literal( ConstantLiteral::byte_str(valtrees.iter().map(|x| match x { - ty::ValTree::Leaf(leaf) => leaf.try_to_u8().unwrap_or_else(|e| fatal!(s[span], "Expected a u8 leaf while translating a str literal, got something else. Error: {:#?}", e)), + ty::ValTree::Leaf(leaf) => leaf.to_u8(), _ => fatal!(s[span], "Expected a flat list of leaves while translating a str literal, got a arbitrary valtree.") }).collect(), StrStyle::Cooked)) , diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 55f4e96ae..368d13a47 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -398,7 +398,7 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>( let s = &with_owner_id(s.base(), (), (), impl_trait_ref.def_id()); clause.predicate_id(s) }; - let new_clause = clause.instantiate_supertrait(tcx, &impl_trait_ref); + let new_clause = clause.instantiate_supertrait(tcx, impl_trait_ref); let impl_expr = new_clause .as_predicate() .as_trait_clause()? @@ -428,12 +428,12 @@ pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>( pub mod copy_paste_from_rustc { use rustc_infer::infer::TyCtxtInferExt; - use rustc_infer::traits::{FulfillmentErrorCode, TraitEngineExt as _}; use rustc_middle::traits::CodegenObligationError; - use rustc_middle::ty::{self, TyCtxt}; + use rustc_middle::ty::{self, TyCtxt, TypeVisitableExt}; use rustc_trait_selection::traits::error_reporting::TypeErrCtxtExt; use rustc_trait_selection::traits::{ - Obligation, ObligationCause, SelectionContext, TraitEngine, TraitEngineExt, Unimplemented, + Obligation, ObligationCause, ObligationCtxt, ScrubbedTraitError, SelectionContext, + Unimplemented, }; /// Attempts to resolve an obligation to an `ImplSource`. The result is @@ -472,22 +472,23 @@ pub mod copy_paste_from_rustc { // Currently, we use a fulfillment context to completely resolve // all nested obligations. This is because they can inform the // inference of the impl's type parameters. - let mut fulfill_cx = >::new(&infcx); - let impl_source = selection.map(|predicate| { - fulfill_cx.register_predicate_obligation(&infcx, predicate.clone()); - predicate + // FIXME(-Znext-solver): Doesn't need diagnostics if new solver. + let ocx = ObligationCtxt::new(&infcx); + let impl_source = selection.map(|obligation| { + ocx.register_obligation(obligation.clone()); + obligation }); // In principle, we only need to do this so long as `impl_source` // contains unbound type parameters. It could be a slight // optimization to stop iterating early. - let errors = fulfill_cx.select_all_or_error(&infcx); + let errors = ocx.select_all_or_error(); if !errors.is_empty() { // `rustc_monomorphize::collector` assumes there are no type errors. // 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::Cycle(cycle) = err.code { + if let ScrubbedTraitError::Cycle(cycle) = err { infcx.err_ctxt().report_overflow_obligation_cycle(&cycle); } } @@ -497,10 +498,13 @@ pub mod copy_paste_from_rustc { let impl_source = infcx.resolve_vars_if_possible(impl_source); let impl_source = infcx.tcx.erase_regions(impl_source); - // Opaque types may have gotten their hidden types constrained, but we can ignore them safely - // as they will get constrained elsewhere, too. - // (ouz-a) This is required for `type-alias-impl-trait/assoc-projection-ice.rs` to pass - let _ = infcx.take_opaque_types(); + if impl_source.has_infer() { + // Unused lifetimes on an impl get replaced with inference vars, but never resolved, + // causing the return value of a query to contain inference vars. We do not have a concept + // for this and will in fact ICE in stable hashing of the return value. So bail out instead. + infcx.tcx.dcx().has_errors().unwrap(); + return Err(CodegenObligationError::FulfillmentError); + } Ok(impl_source) } diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index afde9fa63..92e786b68 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -204,17 +204,16 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::mi const_value.clone(), rustc_span::DUMMY_SP, ), - Const::Ty(c) => c.sinto(s), - Const::Unevaluated(ucv, ty) => match self.translate_uneval(s, ucv.shrink()) { - TranslateUnevalRes::EvaluatedConstant(c) => c.sinto(s), - TranslateUnevalRes::GlobalName(c) => { - let span = tcx - .def_ident_span(ucv.def) - .unwrap_or_else(|| ucv.def.default_span(tcx)) - .sinto(s); - c.decorate(ty.sinto(s), span) + Const::Ty(_ty, c) => c.sinto(s), + Const::Unevaluated(ucv, _ty) => { + let span = tcx + .def_ident_span(ucv.def) + .unwrap_or_else(|| ucv.def.default_span(tcx)); + match self.translate_uneval(s, ucv.shrink(), span) { + TranslateUnevalRes::EvaluatedConstant(c) => c.sinto(s), + TranslateUnevalRes::GlobalName(c) => c, } - }, + } } } } @@ -414,8 +413,8 @@ pub enum CanonicalVarInfo { PlaceholderTy(PlaceholderType), Region(UniverseIndex), PlaceholderRegion(PlaceholderRegion), - Const(UniverseIndex, Ty), - PlaceholderConst(PlaceholderConst, Ty), + Const(UniverseIndex), + PlaceholderConst(PlaceholderConst), Effect, } @@ -3203,8 +3202,8 @@ impl<'a, 'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto>> #[args(<'tcx, S: UnderOwnerState<'tcx> >, from: rustc_hir::ForeignItemKind<'tcx>, state: S as tcx)] #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub enum ForeignItemKind { - Fn(FnDecl, Vec, Generics), - Static(Ty, Mutability), + Fn(FnDecl, Vec, Generics, Safety), + Static(Ty, Mutability, Safety), Type, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 04984afe5..be4e44c08 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -154,7 +154,7 @@ pub struct SourceScopeData { #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::Instance<'tcx>, state: S as s)] pub struct Instance { - pub def: InstanceDef, + pub def: InstanceKind, pub args: Vec, } @@ -317,10 +317,9 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>( // Regular function case let c = c.deref(); let (def_id, generics) = match &c.const_ { - Const::Ty(c) => { + Const::Ty(c_ty, _c) => { // The type of the constant should be a FnDef, allowing // us to retrieve the function's identifier and instantiation. - let c_ty = c.ty(); assert!(c_ty.is_fn()); match c_ty.kind() { TyKind::FnDef(def_id, generics) => (*def_id, *generics), @@ -953,7 +952,7 @@ make_idx_wrapper!(rustc_middle::mir, Local); make_idx_wrapper!(rustc_middle::ty, UserTypeAnnotationIndex); make_idx_wrapper!(rustc_target::abi, FieldIdx); -sinto_todo!(rustc_middle::ty, InstanceDef<'tcx>); +sinto_todo!(rustc_middle::ty, InstanceKind<'tcx>); sinto_todo!(rustc_middle::mir, UserTypeProjections); sinto_todo!(rustc_middle::mir, LocalInfo<'tcx>); sinto_todo!(rustc_ast::ast, InlineAsmTemplatePiece); diff --git a/frontend/lint/src/lib.rs b/frontend/lint/src/lib.rs index 654be8760..9b418ce7f 100644 --- a/frontend/lint/src/lib.rs +++ b/frontend/lint/src/lib.rs @@ -8,7 +8,7 @@ use rustc_middle::ty::TyCtxt; // rustc errors extern crate rustc_errors; -use rustc_errors::DiagCtxt; +use rustc_errors::DiagCtxtHandle; // rustc hir extern crate rustc_hir; @@ -68,7 +68,7 @@ impl<'tcx> Linter<'tcx> { hir.visit_all_item_likes_in_crate(&mut linter); } - fn dcx(&self) -> &'tcx DiagCtxt { + fn dcx(&self) -> DiagCtxtHandle<'tcx> { self.tcx.dcx() } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2dc24fb75..555c69568 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-06-01" +channel = "nightly-2024-06-24" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 31c1426ac..d49db0fb5 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -79,7 +79,7 @@ open FStar.Mul type t_Foo = | Foo : u8 -> t_Foo [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo true = +let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo = { f_Output = t_Foo; f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8)); diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index ff09cf532..bd997c950 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -148,9 +148,7 @@ let numeric (_: Prims.unit) : Prims.unit = () let panic_with_msg (_: Prims.unit) : Prims.unit = - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt true - (Core.Fmt.impl_2__new_const (sz 1) - true + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1) (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 ad3aa6b08..d01460536 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,12 +52,8 @@ 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 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 + 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 vec let h (x: u8) : u8 = @@ -270,16 +266,14 @@ 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 true x.f_a (sz 0) (sz 1) } + { x with f_a = Core.Slice.impl__swap #u8 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 true x.f_b.f_field (sz 0) (sz 1) } <: t_Foo + f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 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 87a96102e..7ba2bd1f5 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 true (Core.Num.impl__u32__wrapping_add true x y <: u32) z + Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z /// Question mark without error coercion let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) @@ -99,9 +99,7 @@ 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 true - (Core.Num.impl__u32__wrapping_add true 123ul hoist5 <: u32) - x) + (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x) <: Core.Ops.Control_flow.t_ControlFlow u32 Rust_primitives.Hax.t_Never in @@ -112,12 +110,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 true x 1ul in + let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in if x >. 3ul then - let x:u32 = Core.Num.impl__u32__wrapping_sub true x 3ul in + let x:u32 = Core.Num.impl__u32__wrapping_sub x 3ul in let y:u32 = x /! 2ul in - let y:u32 = Core.Num.impl__u32__wrapping_add true y 2ul in + let y:u32 = Core.Num.impl__u32__wrapping_add 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) @@ -130,24 +128,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 true x i <: u32) + Core.Num.impl__u32__wrapping_add x i <: u32) in - Core.Num.impl__u32__wrapping_add true x y + Core.Num.impl__u32__wrapping_add x y else let (x, y), hoist15:((u32 & u32) & u32) = match x with | 12ul -> - let y:u32 = Core.Num.impl__u32__wrapping_add true x y in + let y:u32 = Core.Num.impl__u32__wrapping_add x y in (x, y <: (u32 & u32)), 3ul <: ((u32 & u32) & u32) | 13ul -> - 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 + 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 <: ((u32 & u32) & u32) | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32) in let x:u32 = hoist15 in - Core.Num.impl__u32__wrapping_add true x y + Core.Num.impl__u32__wrapping_add 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 = @@ -159,7 +157,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 true hoist21 3uy) + (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist21 3uy) <: Core.Option.t_Option u8) <: @@ -177,7 +175,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 true hoist24 hoist23) + (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist24 hoist23) <: Core.Option.t_Option u8) <: @@ -234,8 +232,9 @@ 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 true - (Core.Num.impl__u8__wrapping_add true v hoist28 <: u8) + (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist28 + <: + u8) hoist29) <: Core.Option.t_Option u8 @@ -260,9 +259,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 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 + 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 if x >. 90ul then match Core.Result.Result_Err 12uy <: Core.Result.t_Result Prims.unit u8 with @@ -290,7 +289,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 true 3ul x) + (Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 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 dea9d4b74..36079953d 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -325,9 +325,7 @@ 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 true self <: i32) <: u32 + f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 } class t_Foo (#v_Self: Type0) = { From f5b704fb73083a9c739f64dff61c113240f69ee4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 26 Jun 2024 14:16:56 +0200 Subject: [PATCH 14/16] Add a bit of information to traces --- cli/driver/src/driver.rs | 5 +++++ frontend/exporter/adt-into/src/lib.rs | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs index 5120911ec..c22e2dab9 100644 --- a/cli/driver/src/driver.rs +++ b/cli/driver/src/driver.rs @@ -65,6 +65,11 @@ fn setup_logging() { }; let subscriber = tracing_subscriber::Registry::default() .with(tracing_subscriber::EnvFilter::from_default_env()) + .with( + tracing_subscriber::fmt::layer() + .with_file(true) + .with_line_number(true), + ) .with( tracing_tree::HierarchicalLayer::new(2) .with_ansi(enable_colors) diff --git a/frontend/exporter/adt-into/src/lib.rs b/frontend/exporter/adt-into/src/lib.rs index 28628646f..b73a035a4 100644 --- a/frontend/exporter/adt-into/src/lib.rs +++ b/frontend/exporter/adt-into/src/lib.rs @@ -390,7 +390,7 @@ pub fn adt_into(input: proc_macro::TokenStream) -> proc_macro::TokenStream { impl #generics SInto<#state_type, #to #to_generics> for #from_with_generics { #[tracing::instrument(level = "trace", skip(#state))] fn sinto(&self, #state: &#state_type) -> #to #to_generics { - tracing::trace!("Enters sinto"); + tracing::trace!("Enters sinto ({})", stringify!(#from_with_generics)); #body } } From 09f3985663ec20098dee3ecf947ed0c649eff620 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 26 Jun 2024 15:38:37 +0200 Subject: [PATCH 15/16] One day more to fix a bug Specifically https://github.com/rust-lang/rustfmt/issues/6210. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 555c69568..09b19906c 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-06-24" +channel = "nightly-2024-06-25" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From 40b47867abddc7a318be5ee3288e9ca36da894d5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 26 Jun 2024 15:54:30 +0200 Subject: [PATCH 16/16] Get the type of uneval constants properly I was using the wrong `DefId` and forgot to substitute arguments. --- frontend/exporter/src/constant_utils.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 65b862313..738c67f0c 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -353,6 +353,9 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { supposely_unreachable_fatal!(s, "TranslateUneval"; {self, ucv}); })) } else { + let param_env = s.param_env(); + let ty = s.base().tcx.type_of(ucv.def); + let ty = tcx.instantiate_and_normalize_erasing_regions(ucv.args, param_env, ty); let kind = if let Some(assoc) = s.base().tcx.opt_associated_item(ucv.def) { if assoc.trait_item_def_id.is_some() { // This must be a trait declaration constant @@ -362,7 +365,6 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { // Solve the trait obligations let parent_def_id = tcx.parent(ucv.def); - let param_env = s.param_env(); let trait_refs = solve_item_traits(s, param_env, parent_def_id, ucv.args, None); // Convert @@ -384,7 +386,6 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { trait_refs: vec![], } }; - let ty = s.base().tcx.type_of(s.owner_id()); let cv = kind.decorate(ty.sinto(s), span.sinto(s)); TranslateUnevalRes::GlobalName(cv) } @@ -414,10 +415,8 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::Const<'tcx> let span = self.default_span(s.base().tcx); match self.kind() { ty::ConstKind::Param(p) => { + let ty = p.find_ty_from_env(s.param_env()); let kind = ConstantExprKind::ConstRef { id: p.sinto(s) }; - let tcx = s.base().tcx; - let param_env = tcx.param_env(s.owner_id()); - let ty = p.find_ty_from_env(param_env); kind.decorate(ty.sinto(s), span.sinto(s)) } ty::ConstKind::Infer(..) => fatal!(s[span], "ty::ConstKind::Infer node? {:#?}", self),