Update hax and rustc

AeneasVerif · Aug 14, 2024 · 27d851d · 27d851d
1 parent 93c558c
commit 27d851d
Show file tree

Hide file tree

Showing 26 changed files with 69 additions and 107 deletions.
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
@@ -69,7 +69,7 @@ tracing-tree = "0.3"
 tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_warn" ] }
 which = "6.0.1"
 
-hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs
@@ -7,7 +7,6 @@
 #![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
 #![feature(let_chains)]
-#![feature(lint_reasons)]
 
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;

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
@@ -1162,17 +1162,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     target,
                 }
             }
-            TerminatorKind::Yield {
-                value: _,
-                resume: _,
-                resume_arg: _,
-                drop: _,
-            } => {
-                error_or_panic!(self, rustc_span, "Unsupported terminator: yield");
-            }
-            TerminatorKind::CoroutineDrop => {
-                error_or_panic!(self, rustc_span, "Unsupported terminator: coroutine drop");
-            }
             TerminatorKind::FalseEdge {
                 real_target,
                 imaginary_target,
@@ -1203,6 +1192,15 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             TerminatorKind::InlineAsm { .. } => {
                 error_or_panic!(self, rustc_span, "Inline assembly is not supported");
             }
+            TerminatorKind::CoroutineDrop
+            | TerminatorKind::TailCall { .. }
+            | TerminatorKind::Yield { .. } => {
+                error_or_panic!(
+                    self,
+                    rustc_span,
+                    format!("Unsupported terminator: {:?}", terminator.kind)
+                );
+            }
         };
 
         // Add the span information

diff --git a/charon/src/lib.rs b/charon/src/lib.rs
@@ -19,7 +19,6 @@
 #![feature(impl_trait_in_assoc_type)]
 #![feature(iterator_try_collect)]
 #![feature(let_chains)]
-#![feature(lint_reasons)]
 #![feature(trait_alias)]
 #![feature(register_tool)]
 // For when we use charon on itself :3

diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs
@@ -1,5 +1,4 @@
 #![feature(rustc_private)]
-#![feature(lint_reasons)]
 
 use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt};
 use itertools::Itertools;

diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out
@@ -52,7 +52,7 @@ impl core::clone::impls::{impl core::clone::Clone for u32}#8 : core::clone::Clon
     fn clone = core::clone::impls::{impl core::clone::Clone for u32}#8::clone
 }
 
-impl core::marker::{impl core::marker::Copy for u32}#41 : core::marker::Copy<u32>
+impl core::marker::{impl core::marker::Copy for u32}#40 : core::marker::Copy<u32>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for u32}#8
 }
@@ -75,7 +75,7 @@ impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzer
 
 impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for u32}#20 : core::num::nonzero::ZeroablePrimitive<u32>
 {
-    parent_clause0 = core::marker::{impl core::marker::Copy for u32}#41
+    parent_clause0 = core::marker::{impl core::marker::Copy for u32}#40
     parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for u32}#19
     parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroU32Inner}#12
     parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner}#11
@@ -153,7 +153,7 @@ fn test_crate::use_get<'_0>(@1: &'_0 (core::cell::Cell<u32>)) -> u32
     let @2: &'_ (core::cell::Cell<u32>); // anonymous local
 
     @2 := &*(rc@1)
-    @0 := core::cell::{core::cell::Cell<T>}#10::get<u32>[core::marker::{impl core::marker::Copy for u32}#41](move (@2))
+    @0 := core::cell::{core::cell::Cell<T>}#10::get<u32>[core::marker::{impl core::marker::Copy for u32}#40](move (@2))
     drop @2
     return
 }

diff --git a/charon/tests/ui/generic-associated-types.out b/charon/tests/ui/generic-associated-types.out
@@ -16,7 +16,7 @@ error: Ignoring the following item due to an error: test_crate::{impl#0}
 10 | impl<'a, T> LendingIterator for Option<&'a T> {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-thread 'rustc' panicked at /rustc/6b0f4b5ec3aa707ecaa78230722117324a4ce23c/compiler/rustc_type_ir/src/binder.rs:785:9:
+thread 'rustc' panicked at /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/compiler/rustc_type_ir/src/binder.rs:783:9:
 const parameter `'a/#1` ('a/#1/1) out of range when instantiating args=[Self/#0]
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `test_crate::LendingIterator::next`.
@@ -38,9 +38,10 @@ warning[E9999]: Hax frontend found a projected type with escaping bound vars. Pl
                  - alias_ty: AliasTy {
                     args: [
                         impl for<'a> FnMut(I::Item<'a>)/#1,
-                        (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                        (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                     ],
                     def_id: core::ops::function::FnOnce::Output,
+                    ..
                 }
                  - alias_kind: Projection
                  - trait_ref: <impl for<'a> FnMut(I::Item<'a>) as std::ops::FnOnce<(<I as LendingIterator>::Item<'a>,)>>
@@ -50,17 +51,17 @@ warning[E9999]: Hax frontend found a projected type with escaping bound vars. Pl
                 )
                  - rebased_generics: [
                     impl for<'a> FnMut(I::Item<'a>)/#1,
-                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
-                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
+                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                 ]
                  - norm_rebased_generics: Err(
                     Type(
-                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                     ),
                 )
                  - norm_generics: Err(
                     Type(
-                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                     ),
                 )
                  - early_binder_generics: Ok(
@@ -73,7 +74,7 @@ warning[E9999]: Hax frontend found a projected type with escaping bound vars. Pl
   = 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)!
 
-thread 'rustc' panicked at /rustc/6b0f4b5ec3aa707ecaa78230722117324a4ce23c/compiler/rustc_type_ir/src/binder.rs:785:9:
+thread 'rustc' panicked at /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/compiler/rustc_type_ir/src/binder.rs:783:9:
 const parameter `'a/#1` ('a/#1/1) out of range when instantiating args=[I/#0]
 error: Thread panicked when extracting item `test_crate::for_each`.
   --> tests/ui/generic-associated-types.rs:24:1
@@ -97,5 +98,4 @@ warning: unused variable: `x`
 
 error: aborting due to 6 previous errors; 2 warnings emitted
 
-[ERROR charon_driver:249] Compilation encountered 6 errors
-Error: Charon driver exited with code 1
+Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out
@@ -63,7 +63,7 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
     fn clone = core::clone::impls::{impl core::clone::Clone for u8}#6::clone
 }
 
-impl core::marker::{impl core::marker::Copy for u8}#39 : core::marker::Copy<u8>
+impl core::marker::{impl core::marker::Copy for u8}#38 : core::marker::Copy<u8>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8}#6
 }
@@ -102,7 +102,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     let @5: (); // anonymous local
 
     @4 := &*(s@1)
-    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#39]]::try_into(move (@4))
+    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#38]]::try_into(move (@4))
     drop @4
     _array@2 := core::result::{core::result::Result<T, E>}::unwrap<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3))
     drop @3

diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out
@@ -63,7 +63,7 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
     fn clone = core::clone::impls::{impl core::clone::Clone for u8}#6::clone
 }
 
-impl core::marker::{impl core::marker::Copy for u8}#39 : core::marker::Copy<u8>
+impl core::marker::{impl core::marker::Copy for u8}#38 : core::marker::Copy<u8>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8}#6
 }
@@ -102,7 +102,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     let @5: (); // anonymous local
 
     @4 := &*(s@1)
-    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#39]]::try_into(move (@4))
+    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#38]]::try_into(move (@4))
     drop @4
     _array@2 := core::result::{core::result::Result<T, E>}::unwrap<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3))
     drop @3

diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out
@@ -301,7 +301,7 @@ impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Cl
     fn clone = core::clone::impls::{impl core::clone::Clone for usize}#5::clone
 }
 
-impl core::marker::{impl core::marker::Copy for usize}#38 : core::marker::Copy<usize>
+impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
 }
@@ -324,7 +324,7 @@ impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzer
 
 impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
 {
-    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#38
+    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#37
     parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
     parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
     parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26

diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out
@@ -6,5 +6,4 @@ error: Unsupported statement kind: intrinsic
 
 error: aborting due to 1 previous error
 
-[ERROR charon_driver:249] Compilation encountered 1 errors
-Error: Charon driver exited with code 1
+Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out
@@ -1030,7 +1030,7 @@ impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Cl
     fn clone = core::clone::impls::{impl core::clone::Clone for usize}#5::clone
 }
 
-impl core::marker::{impl core::marker::Copy for usize}#38 : core::marker::Copy<usize>
+impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
 }
@@ -1053,7 +1053,7 @@ impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzer
 
 impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
 {
-    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#38
+    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#37
     parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
     parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
     parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26

diff --git a/charon/tests/ui/matches.out b/charon/tests/ui/matches.out
@@ -16,16 +16,8 @@ fn test_crate::test1(@1: test_crate::E1) -> bool
         0 | 1 => {
             @0 := const (true)
         },
-        _ => {
-            match x@1 {
-                2 => {
-                    @0 := const (false)
-                },
-                _ => {
-                    @fake_read(x@1)
-                    undefined_behavior
-                }
-            }
+        2 => {
+            @0 := const (false)
         }
     }
     return
@@ -65,16 +57,8 @@ fn test_crate::test2(@1: test_crate::E2) -> u32
             @0 := copy (n@2)
             drop n@2
         },
-        _ => {
-            match x@1 {
-                2 => {
-                    @0 := const (0 : u32)
-                },
-                _ => {
-                    @fake_read(x@1)
-                    undefined_behavior
-                }
-            }
+        2 => {
+            @0 := const (0 : u32)
         }
     }
     return
@@ -106,16 +90,8 @@ fn test_crate::test3(@1: test_crate::E2) -> u32
             y@3 := copy (n@4)
             drop n@4
         },
-        _ => {
-            match x@1 {
-                2 => {
-                    y@3 := const (0 : u32)
-                },
-                _ => {
-                    @fake_read(x@1)
-                    undefined_behavior
-                }
-            }
+        2 => {
+            y@3 := const (0 : u32)
         }
     }
     @fake_read(y@3)