diff --git a/charon/Cargo.lock b/charon/Cargo.lock index de71a8687..e1ee05336 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -788,7 +788,7 @@ checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" [[package]] name = "hax-adt-into" version = "0.2.0" -source = "git+https://github.com/cryspen/hax?branch=main#9c118e5544b5b713f282aca487c414cb449134a4" +source = "git+https://github.com/cryspen/hax?branch=main#e88b5707b796e85a30efd44fa085fdb97f7e04f8" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -799,7 +799,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.2.0" -source = "git+https://github.com/cryspen/hax?branch=main#9c118e5544b5b713f282aca487c414cb449134a4" +source = "git+https://github.com/cryspen/hax?branch=main#e88b5707b796e85a30efd44fa085fdb97f7e04f8" dependencies = [ "extension-traits", "hax-adt-into", @@ -816,7 +816,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.2.0" -source = "git+https://github.com/cryspen/hax?branch=main#9c118e5544b5b713f282aca487c414cb449134a4" +source = "git+https://github.com/cryspen/hax?branch=main#e88b5707b796e85a30efd44fa085fdb97f7e04f8" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/rust-toolchain b/charon/rust-toolchain index b374f8a1f..1ea405992 100644 --- a/charon/rust-toolchain +++ b/charon/rust-toolchain @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2024-10-23" +channel = "nightly-2024-11-23" components = [ "rustc-dev", "llvm-tools-preview" ] diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index 44d099507..1d714a55c 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -967,6 +967,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // Used in the interpreter to check that const code doesn't run for too long or even // indefinitely. StatementKind::ConstEvalCounter => None, + // Semantically equivalent to `Nop`, used only for rustc lints. + StatementKind::BackwardIncompatibleDropHint { .. } => None, StatementKind::Nop => None, }; diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index b6e145581..98faa2eef 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -143,7 +143,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { ClauseKind::WellFormed(_) => { raise_error!(self, span, "Well-formedness clauses are unsupported") } - kind @ ClauseKind::ConstEvaluatable(_) => { + kind => { raise_error!(self, span, "Unsupported clause: {:?}", kind) } } diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 200b853de..e513d6d08 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -21,9 +21,9 @@ fn check_region_name(s: String) -> Option { pub fn translate_bound_region_kind_name(kind: &hax::BoundRegionKind) -> Option { use hax::BoundRegionKind::*; let s = match kind { - BrAnon => None, - BrNamed(_, symbol) => Some(symbol.clone()), - BrEnv => Some("@env".to_owned()), + Anon => None, + Named(_, symbol) => Some(symbol.clone()), + ClosureEnv => Some("@env".to_owned()), }; s.and_then(check_region_name) } diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index 04e9120f1..24ef33ac9 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -171,6 +171,7 @@ pub fn test_crate::test_vec_push() return } +#[lang_item("Cell")] pub opaque type core::cell::Cell pub fn core::cell::{core::cell::Cell}#10::get<'_0, T>(@1: &'_0 (core::cell::Cell)) -> T diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 075d4f207..e5c2cc52a 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -173,7 +173,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd for u8}#60 : core::cmp::P fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd for u8}#60::partial_cmp<'_0_0, '_0_1> } -pub fn core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward_checked(@1: u8, @2: usize) -> core::option::Option[core::marker::Sized] @@ -381,7 +381,7 @@ pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self) pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self::Output -pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::Step::forward_checked(@1: Self, @2: usize) -> core::option::Option[Self::parent_clause0] diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index 4fc92b00a..40756d3d6 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -767,7 +767,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd for i32}#76 : core::cmp: fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd for i32}#76::partial_cmp<'_0_0, '_0_1> } -pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked(@1: i32, @2: usize) -> core::option::Option[core::marker::Sized] @@ -806,7 +806,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd for usize}#58 : core:: fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd for usize}#58::partial_cmp<'_0_0, '_0_1> } -pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_checked(@1: usize, @2: usize) -> core::option::Option[core::marker::Sized] @@ -976,7 +976,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd for u32}#64 : core::cmp: fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd for u32}#64::partial_cmp<'_0_0, '_0_1> } -pub fn core::iter::range::{impl core::iter::range::Step for u32}#39::steps_between<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::{impl core::iter::range::Step for u32}#39::steps_between<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::{impl core::iter::range::Step for u32}#39::forward_checked(@1: u32, @2: usize) -> core::option::Option[core::marker::Sized] @@ -1470,7 +1470,7 @@ where fn index_mut<'_0> = alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#14::index_mut<'_0_0, T, I, A>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] } -pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::Step::forward_checked(@1: Self, @2: usize) -> core::option::Option[Self::parent_clause0] diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index 8e6062ff6..79d094317 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -277,11 +277,11 @@ pub fn test_crate::test_list1() return } -pub fn alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#39::deref_mut<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0])) -> &'_0 mut (T) +pub fn alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#25::deref_mut<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0])) -> &'_0 mut (T) where [@TraitClause0]: core::marker::Sized, -pub fn alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#38::deref<'_0, T, A>(@1: &'_0 (alloc::boxed::Box[@TraitClause0])) -> &'_0 (T) +pub fn alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#24::deref<'_0, T, A>(@1: &'_0 (alloc::boxed::Box[@TraitClause0])) -> &'_0 (T) where [@TraitClause0]: core::marker::Sized, @@ -300,12 +300,12 @@ pub fn test_crate::test_box1() b@1 := @BoxNew[core::marker::Sized](const (0 : i32)) @fake_read(b@1) @3 := &two-phase-mut b@1 - x@2 := alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#39::deref_mut<'_, i32, alloc::alloc::Global>[core::marker::Sized](move (@3)) + x@2 := alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#25::deref_mut<'_, i32, alloc::alloc::Global>[core::marker::Sized](move (@3)) drop @3 @fake_read(x@2) *(x@2) := const (1 : i32) @5 := &b@1 - x@4 := alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#38::deref<'_, i32, alloc::alloc::Global>[core::marker::Sized](move (@5)) + x@4 := alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#24::deref<'_, i32, alloc::alloc::Global>[core::marker::Sized](move (@5)) drop @5 @fake_read(x@4) @8 := copy (*(x@4)) @@ -624,20 +624,20 @@ pub trait core::ops::deref::DerefMut #[lang_item("deref_mut_method")] pub fn core::ops::deref::DerefMut::deref_mut<'_0, Self>(@1: &'_0 mut (Self)) -> &'_0 mut (Self::parent_clause0::Target) -impl alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#38 : core::ops::deref::Deref[@TraitClause0]> +impl alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#24 : core::ops::deref::Deref[@TraitClause0]> where [@TraitClause0]: core::marker::Sized, { type Target = T - fn deref<'_0> = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#38::deref<'_0_0, T, A>[@TraitClause0] + fn deref<'_0> = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#24::deref<'_0_0, T, A>[@TraitClause0] } -impl alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#39 : core::ops::deref::DerefMut[@TraitClause0]> +impl alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#25 : core::ops::deref::DerefMut[@TraitClause0]> where [@TraitClause0]: core::marker::Sized, { - parent_clause0 = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#38[@TraitClause0] - fn deref_mut<'_0> = alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#39::deref_mut<'_0_0, T, A>[@TraitClause0] + parent_clause0 = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box[@TraitClause0]}#24[@TraitClause0] + fn deref_mut<'_0> = alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box[@TraitClause0]}#25::deref_mut<'_0_0, T, A>[@TraitClause0] } #[lang_item("deref_method")] diff --git a/charon/tests/ui/rvalues.rs b/charon/tests/ui/rvalues.rs index 1d9fe3206..963dc7cdd 100644 --- a/charon/tests/ui/rvalues.rs +++ b/charon/tests/ui/rvalues.rs @@ -1,4 +1,3 @@ -#![feature(const_ub_checks)] #![feature(core_intrinsics)] #![feature(rustc_attrs)] #![allow(internal_features)] diff --git a/charon/tests/ui/simple/gat-default.out b/charon/tests/ui/simple/gat-default.out index 46e17ef7e..542b865bc 100644 --- a/charon/tests/ui/simple/gat-default.out +++ b/charon/tests/ui/simple/gat-default.out @@ -1,4 +1,4 @@ -thread 'rustc' panicked at /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/compiler/rustc_type_ir/src/binder.rs:697:9: +thread 'rustc' panicked at /rustc/a47555110cf09b3ed59811d9b02235443e76a595/compiler/rustc_type_ir/src/binder.rs:735:9: type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()] note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace error: Hax panicked when translating `test_crate::{impl#0}`. @@ -22,7 +22,7 @@ error: Item `test_crate::Collection` caused errors; ignoring. | ^^^^^^^^^^^^^^^^ | -thread 'rustc' panicked at /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/compiler/rustc_type_ir/src/binder.rs:697:9: +thread 'rustc' panicked at /rustc/a47555110cf09b3ed59811d9b02235443e76a595/compiler/rustc_type_ir/src/binder.rs:735:9: type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()] error: Hax panicked when translating `test_crate::{impl#0}`. --> tests/ui/simple/gat-default.rs:9:1 diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out index 271b3c073..c16f24238 100644 --- a/charon/tests/ui/ullbc-control-flow.out +++ b/charon/tests/ui/ullbc-control-flow.out @@ -110,7 +110,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd for i32}#76 : core::cmp: fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd for i32}#76::partial_cmp<'_0_0, '_0_1> } -pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked(@1: i32, @2: usize) -> core::option::Option[core::marker::Sized] @@ -149,7 +149,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd for usize}#58 : core:: fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd for usize}#58::partial_cmp<'_0_0, '_0_1> } -pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_checked(@1: usize, @2: usize) -> core::option::Option[core::marker::Sized] @@ -375,7 +375,7 @@ where #[lang_item("next")] pub fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option[Self::parent_clause0] -pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::option::Option[core::marker::Sized] +pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> (usize, core::option::Option[core::marker::Sized]) pub fn core::iter::range::Step::forward_checked(@1: Self, @2: usize) -> core::option::Option[Self::parent_clause0]