From e8ae892aa66b820e63355febaa7351affe70eb61 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 16 Sep 2024 11:37:24 +0200
Subject: [PATCH 1/6] Disable all MIR optimization passes by default

---
 charon/src/bin/charon-driver/main.rs          | 47 ++++++++++++++++
 .../ui/issue-120-bare-discriminant-read.out   | 20 +++----
 charon/tests/ui/ptr_to_promoted.out           | 28 ++++++----
 charon/tests/ui/rvalues.out                   | 54 +++++++++++++++----
 charon/tests/ui/stealing.out                  |  2 +-
 5 files changed, 123 insertions(+), 28 deletions(-)

diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs
index 8596a42e..01190207 100644
--- a/charon/src/bin/charon-driver/main.rs
+++ b/charon/src/bin/charon-driver/main.rs
@@ -34,6 +34,7 @@ use crate::driver::{
 use charon_lib::logger;
 use charon_lib::options;
 use charon_lib::trace;
+use itertools::Itertools;
 
 fn main() {
     // Initialize the logger
@@ -191,6 +192,52 @@ fn main() {
         compiler_args.push(extra_flag);
     }
 
+    let disabled_mir_passes = [
+        "AfterConstProp",
+        "AfterGVN",
+        "AfterUnreachableEnumBranching)",
+        "BeforeConstProp",
+        "CheckAlignment",
+        "CopyProp",
+        "CriticalCallEdges",
+        "DataflowConstProp",
+        "DeduplicateBlocks",
+        "DestinationPropagation",
+        "EarlyOtherwiseBranch",
+        "EnumSizeOpt",
+        "GVN",
+        "Initial",
+        "Inline",
+        "InstSimplify",
+        "JumpThreading",
+        "LowerSliceLenCalls",
+        "MatchBranchSimplification",
+        "MentionedItems",
+        "MultipleReturnTerminators",
+        "ReferencePropagation",
+        "RemoveNoopLandingPads",
+        "RemoveStorageMarkers",
+        "RemoveUnneededDrops",
+        "RemoveZsts",
+        "RenameReturnPlace",
+        "ReorderBasicBlocks",
+        "ReorderLocals",
+        "ScalarReplacementOfAggregates",
+        "SimplifyComparisonIntegral",
+        "SimplifyLocals",
+        "SingleUseConsts",
+        "UnreachableEnumBranching",
+        "UnreachablePropagation",
+    ];
+    // Disable all these mir passes.
+    compiler_args.push(format!(
+        "-Zmir-enable-passes={}",
+        disabled_mir_passes
+            .iter()
+            .map(|p| format!("-{p}"))
+            .format(",")
+    ));
+
     trace!("Compiler arguments: {:?}", compiler_args);
 
     // Call the Rust compiler with our custom callback.
diff --git a/charon/tests/ui/issue-120-bare-discriminant-read.out b/charon/tests/ui/issue-120-bare-discriminant-read.out
index d6cd51b3..63b01418 100644
--- a/charon/tests/ui/issue-120-bare-discriminant-read.out
+++ b/charon/tests/ui/issue-120-bare-discriminant-read.out
@@ -16,8 +16,10 @@ where
 {
     let @0: isize; // return
     let opt@1: &'_ (core::option::Option<T>[@TraitClause0]); // arg #1
+    let @2: &'_ (core::option::Option<T>[@TraitClause0]); // anonymous local
 
-    match *(opt@1) {
+    @2 := copy (opt@1)
+    match *(@2) {
         0 => {
             @0 := const (0 : isize)
         },
@@ -25,6 +27,7 @@ where
             @0 := const (1 : isize)
         },
     }
+    drop @2
     return
 }
 
@@ -35,17 +38,16 @@ where
     let @0: bool; // return
     let opt@1: core::option::Option<T>[@TraitClause0]; // arg #1
     let @2: isize; // anonymous local
+    let @3: &'_ (core::option::Option<T>[@TraitClause0]); // anonymous local
+    let @4: &'_ (core::option::Option<T>[@TraitClause0]); // anonymous local
 
-    match opt@1 {
-        0 => {
-            @2 := const (0 : isize)
-        },
-        1 => {
-            @2 := const (1 : isize)
-        },
-    }
+    @4 := &opt@1
+    @3 := copy (@4)
+    @2 := test_crate::discriminant_value<T>[@TraitClause0](move (@3))
+    drop @3
     @0 := move (@2) != const (0 : isize)
     drop @2
+    drop @4
     drop opt@1
     return
 }
diff --git a/charon/tests/ui/ptr_to_promoted.out b/charon/tests/ui/ptr_to_promoted.out
index bd874d2f..6864b6c0 100644
--- a/charon/tests/ui/ptr_to_promoted.out
+++ b/charon/tests/ui/ptr_to_promoted.out
@@ -3,18 +3,28 @@
 fn test_crate::main()
 {
     let @0: (); // return
-    let @1: *const u8; // anonymous local
-    let @2: usize; // anonymous local
-    let x@3: &'_ (u8); // local
-    let @4: u8; // anonymous local
+    let x@1: *const u8; // local
+    let @2: &'_ (u8); // anonymous local
+    let @3: usize; // anonymous local
+    let @4: *const u8; // anonymous local
     let @5: &'_ (u8); // anonymous local
+    let @6: u8; // anonymous local
+    let @7: &'_ (u8); // anonymous local
+    let @8: (); // anonymous local
 
-    @4 := const ([0])
-    @5 := &@4
-    x@3 := move (@5)
-    @1 := &raw const *(x@3)
-    @2 := cast<*const u8, usize>(copy (@1))
+    @6 := const ([0])
+    @7 := &@6
+    @5 := move (@7)
+    @2 := copy (@5)
+    x@1 := &raw const *(@2)
     drop @2
+    @4 := copy (x@1)
+    @3 := cast<*const u8, usize>(move (@4))
+    drop @4
+    drop @3
+    @8 := ()
+    @0 := move (@8)
+    drop x@1
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out
index b1d9846e..5be6dd03 100644
--- a/charon/tests/ui/rvalues.out
+++ b/charon/tests/ui/rvalues.out
@@ -258,9 +258,12 @@ fn test_crate::transmute(@1: Array<u32, 2 : usize>) -> u64
 {
     let @0: u64; // return
     let x@1: Array<u32, 2 : usize>; // arg #1
+    let @2: Array<u32, 2 : usize>; // anonymous local
 
     // When optimized, this becomes a built-in cast. Otherwise this is just a call to `transmute`.
-    @0 := transmute<Array<u32, 2 : usize>, u64>(copy (x@1))
+    @2 := copy (x@1)
+    @0 := transmute<Array<u32, 2 : usize>, u64>(move (@2))
+    drop @2
     return
 }
 
@@ -274,6 +277,14 @@ global test_crate::STEAL2  {
     return
 }
 
+fn core::mem::size_of<T>() -> usize
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+
+fn core::mem::align_of<T>() -> usize
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+
 struct test_crate::nullary_ops::Struct<T>
   where
       [@TraitClause0]: core::marker::Sized<T>,
@@ -290,15 +301,40 @@ where
     let @0: usize; // return
     let size@1: usize; // local
     let align@2: usize; // local
-    let offset@3: usize; // local
-    let @4: usize; // anonymous local
-
+    let ub@3: bool; // local
+    let offset@4: usize; // local
+    let @5: usize; // anonymous local
+    let @6: usize; // anonymous local
+    let @7: usize; // anonymous local
+    let @8: usize; // anonymous local
+    let @9: usize; // anonymous local
+    let @10: bool; // anonymous local
+    let @11: usize; // anonymous local
+
+    size@1 := core::mem::size_of<T>[@TraitClause0]()
+    align@2 := core::mem::align_of<T>[@TraitClause0]()
     // This one seems to be optimized out.
-    size@1 := size_of<T>
-    align@2 := align_of<T>
-    offset@3 := offset_of(?)<test_crate::nullary_ops::Struct<T>[@TraitClause0]>
-    @4 := copy (size@1) + copy (align@2)
-    @0 := copy (@4) + copy (offset@3)
+    ub@3 := const (false)
+    offset@4 := offset_of(?)<test_crate::nullary_ops::Struct<T>[@TraitClause0]>
+    @7 := copy (size@1)
+    @8 := copy (align@2)
+    @6 := move (@7) + move (@8)
+    drop @8
+    drop @7
+    @10 := copy (ub@3)
+    @9 := cast<bool, usize>(move (@10))
+    drop @10
+    @5 := move (@6) + move (@9)
+    drop @9
+    drop @6
+    @11 := copy (offset@4)
+    @0 := move (@5) + move (@11)
+    drop @11
+    drop @5
+    drop offset@4
+    drop ub@3
+    drop align@2
+    drop size@1
     return
 }
 
diff --git a/charon/tests/ui/stealing.out b/charon/tests/ui/stealing.out
index 2ba1904e..d6c4f170 100644
--- a/charon/tests/ui/stealing.out
+++ b/charon/tests/ui/stealing.out
@@ -14,7 +14,7 @@ fn test_crate::four() -> usize
 {
     let @0: usize; // return
 
-    @0 := const (4 : usize)
+    @0 := const (2 : usize) + const (2 : usize)
     return
 }
 

From 469ef6c01cae820b019f74f953d9305df5efd91f Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 15 Oct 2024 13:56:20 +0200
Subject: [PATCH 2/6] Update hax

---
 charon/Cargo.lock                             |  6 +-
 .../translate/translate_predicates.rs         |  6 +-
 .../translate/translate_types.rs              |  3 +
 charon/tests/ui/impl-trait.out                | 76 +++++++++++++----
 charon/tests/ui/impl-trait.rs                 |  2 -
 .../tests/ui/issue-394-rpit-with-lifetime.out | 85 +++++++++++++++----
 .../tests/ui/issue-394-rpit-with-lifetime.rs  |  2 -
 charon/tests/ui/non-lifetime-gats.out         |  8 +-
 .../unsupported/advanced-const-generics.out   |  2 +-
 9 files changed, 141 insertions(+), 49 deletions(-)

diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index db7a2971..9d201058 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -506,7 +506,7 @@ dependencies = [
 [[package]]
 name = "hax-adt-into"
 version = "0.1.0-alpha.1"
-source = "git+https://github.com/hacspec/hax?branch=main#e2734c854c286eed2405967c7940d934c1fcd72e"
+source = "git+https://github.com/hacspec/hax?branch=main#f48e911e6f18ea500fae1a79d7f3467ffd58bbce"
 dependencies = [
  "itertools 0.11.0",
  "proc-macro2",
@@ -517,7 +517,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.1.0-alpha.1"
-source = "git+https://github.com/hacspec/hax?branch=main#e2734c854c286eed2405967c7940d934c1fcd72e"
+source = "git+https://github.com/hacspec/hax?branch=main#f48e911e6f18ea500fae1a79d7f3467ffd58bbce"
 dependencies = [
  "bincode",
  "extension-traits",
@@ -535,7 +535,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter-options"
 version = "0.1.0-alpha.1"
-source = "git+https://github.com/hacspec/hax?branch=main#e2734c854c286eed2405967c7940d934c1fcd72e"
+source = "git+https://github.com/hacspec/hax?branch=main#f48e911e6f18ea500fae1a79d7f3467ffd58bbce"
 dependencies = [
  "bincode",
  "hax-adt-into",
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 30d72202..1c212edd 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -380,7 +380,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             item,
                             predicate,
                             index,
-                            predicate_id: _,
+                            ..
                         } => {
                             trait_id = TraitRefKind::ItemClause(
                                 Box::new(trait_id),
@@ -394,9 +394,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             );
                         }
                         Parent {
-                            predicate,
-                            index,
-                            predicate_id: _,
+                            predicate, index, ..
                         } => {
                             trait_id = TraitRefKind::ParentClause(
                                 Box::new(trait_id),
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 1062a6f5..718d484e 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -177,6 +177,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     let name = TraitItemName(assoc_item.name.clone().into());
                     TyKind::TraitType(trait_ref, name)
                 }
+                hax::AliasKind::Opaque { hidden_ty, .. } => {
+                    return self.translate_ty(span, erase_regions, hidden_ty)
+                }
                 _ => {
                     error_or_panic!(self, span, format!("Unimplemented: {:?}", ty))
                 }
diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out
index a17a0fab..2bdacbc4 100644
--- a/charon/tests/ui/impl-trait.out
+++ b/charon/tests/ui/impl-trait.out
@@ -1,17 +1,59 @@
-error: Unimplemented: Ty { kind: Alias(Alias { kind: Opaque, args: [Type(Ty { kind: Param(ParamTy { index: 0, name: "U" }) })], def_id: test_crate::wrap::{opaque#0} }) }
- --> tests/ui/impl-trait.rs:4:1
-  |
-4 | / pub fn wrap<U>() -> impl for<'a> FnOnce(&'a U) -> WrapClone<&'a U> {
-5 | |     |x| WrapClone(x)
-6 | | }
-  | |_^
-
-error: Ignoring the following item due to an error: test_crate::wrap
- --> tests/ui/impl-trait.rs:4:1
-  |
-4 | pub fn wrap<U>() -> impl for<'a> FnOnce(&'a U) -> WrapClone<&'a U> {
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-error: aborting due to 2 previous errors
-
-Error: Charon driver exited with code 101
+# Final LLBC before serialization:
+
+trait core::marker::Sized<Self>
+
+trait core::clone::Clone<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    fn clone : core::clone::Clone::clone
+    fn clone_from : core::clone::Clone::clone_from
+}
+
+struct test_crate::WrapClone<T>
+  where
+      [@TraitClause0]: core::marker::Sized<T>,
+      [@TraitClause1]: core::clone::Clone<T>,
+ =
+{
+  T,
+}
+
+fn core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3::clone<'_0, '_1, T>(@1: &'_1 (&'_0 (T))) -> &'_0 (T)
+
+impl<'_0, T> core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_0, T> : core::clone::Clone<&'_0 (T)>
+{
+    parent_clause0 = core::marker::Sized<&'_ (T)>
+    fn clone = core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3::clone
+}
+
+fn test_crate::wrap::closure<'_0, U>(@1: (), @2: (&'_0 (U))) -> test_crate::WrapClone<&'_0 (U)>[core::marker::Sized<&'_1_0 (U)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, U>]
+where
+    [@TraitClause0]: core::marker::Sized<U>,
+{
+    let @0: test_crate::WrapClone<&'_ (U)>[core::marker::Sized<&'_ (U)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, U>]; // return
+    let state@1: (); // arg #1
+    let x@2: &'_ (U); // arg #2
+    let @3: &'_ (U); // anonymous local
+
+    @3 := copy (x@2)
+    @0 := test_crate::WrapClone { 0: move (@3) }
+    drop @3
+    return
+}
+
+fn test_crate::wrap<U>() -> fn<'_1_0>(&'_1_0 (U)) -> test_crate::WrapClone<&'_1_0 (U)>[core::marker::Sized<&'_2_0 (U)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, U>]
+where
+    [@TraitClause0]: core::marker::Sized<U>,
+{
+    let @0: fn<'_1_0>(&'_1_0 (U)) -> test_crate::WrapClone<&'_1_0 (U)>[core::marker::Sized<&'_2_0 (U)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, U>]; // return
+
+    @0 := {test_crate::wrap::closure<U>[@TraitClause0]} {}
+    return
+}
+
+fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
+
+fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
+
+
+
diff --git a/charon/tests/ui/impl-trait.rs b/charon/tests/ui/impl-trait.rs
index a626beaf..202bffb9 100644
--- a/charon/tests/ui/impl-trait.rs
+++ b/charon/tests/ui/impl-trait.rs
@@ -1,5 +1,3 @@
-//@ known-failure
-
 pub struct WrapClone<T: Clone>(T);
 pub fn wrap<U>() -> impl for<'a> FnOnce(&'a U) -> WrapClone<&'a U> {
     |x| WrapClone(x)
diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.out b/charon/tests/ui/issue-394-rpit-with-lifetime.out
index bbe59022..842caa66 100644
--- a/charon/tests/ui/issue-394-rpit-with-lifetime.out
+++ b/charon/tests/ui/issue-394-rpit-with-lifetime.out
@@ -1,17 +1,68 @@
-error: Unimplemented: Ty { kind: Alias(Alias { kind: Opaque, args: [Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }), Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) })], def_id: test_crate::sparse_transitions::{opaque#0} }) }
- --> tests/ui/issue-394-rpit-with-lifetime.rs:3:1
-  |
-3 | / fn sparse_transitions<'a>() -> impl Iterator<Item = u8> + 'a {
-4 | |     core::iter::from_fn(|| None)
-5 | | }
-  | |_^
-
-error: Ignoring the following item due to an error: test_crate::sparse_transitions
- --> tests/ui/issue-394-rpit-with-lifetime.rs:3:1
-  |
-3 | fn sparse_transitions<'a>() -> impl Iterator<Item = u8> + 'a {
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-error: aborting due to 2 previous errors
-
-Error: Charon driver exited with code 101
+# Final LLBC before serialization:
+
+trait core::marker::Sized<Self>
+
+opaque type core::iter::sources::from_fn::FromFn<F>
+  where
+      [@TraitClause0]: core::marker::Sized<F>,
+
+enum core::option::Option<T>
+  where
+      [@TraitClause0]: core::marker::Sized<T>,
+ =
+|  None()
+|  Some(T)
+
+
+fn test_crate::sparse_transitions::closure<'a, '_1>(@1: &'_1 mut (()), @2: ()) -> core::option::Option<u8>[core::marker::Sized<u8>]
+{
+    let @0: core::option::Option<u8>[core::marker::Sized<u8>]; // return
+    let state@1: &'_1 mut (()); // arg #1
+
+    @0 := core::option::Option::None {  }
+    return
+}
+
+trait core::marker::Tuple<Self>
+
+trait core::ops::function::FnOnce<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Args>
+    parent_clause1 : [@TraitClause1]: core::marker::Tuple<Args>
+    parent_clause2 : [@TraitClause2]: core::marker::Sized<Self::Output>
+    type Output
+    fn call_once : core::ops::function::FnOnce::call_once
+}
+
+trait core::ops::function::FnMut<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce<Self, Args>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Args>
+    parent_clause2 : [@TraitClause2]: core::marker::Tuple<Args>
+    fn call_mut : core::ops::function::FnMut::call_mut
+}
+
+fn core::iter::sources::from_fn::from_fn<T, F>(@1: F) -> core::iter::sources::from_fn::FromFn<F>[@TraitClause1]
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+    [@TraitClause1]: core::marker::Sized<F>,
+    [@TraitClause2]: core::ops::function::FnMut<F, ()>,
+    @TraitClause2::parent_clause0::Output = core::option::Option<T>[@TraitClause0],
+
+fn test_crate::sparse_transitions<'a>() -> core::iter::sources::from_fn::FromFn<fn() -> core::option::Option<u8>[core::marker::Sized<u8>]>[core::marker::Sized<fn() -> core::option::Option<u8>[core::marker::Sized<u8>]>]
+{
+    let @0: core::iter::sources::from_fn::FromFn<fn() -> core::option::Option<u8>[core::marker::Sized<u8>]>[core::marker::Sized<fn() -> core::option::Option<u8>[core::marker::Sized<u8>]>]; // return
+    let @1: fn() -> core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
+
+    @1 := {test_crate::sparse_transitions::closure<'_>} {}
+    @0 := core::iter::sources::from_fn::from_fn<u8, fn() -> core::option::Option<u8>[core::marker::Sized<u8>]>[core::marker::Sized<u8>, core::marker::Sized<fn() -> core::option::Option<u8>[core::marker::Sized<u8>]>, core::ops::function::FnMut<fn() -> core::option::Option<u8>[core::marker::Sized<u8>], ()>](move (@1))
+    drop @1
+    return
+}
+
+fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output
+
+fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
+
+
+
diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.rs b/charon/tests/ui/issue-394-rpit-with-lifetime.rs
index eaff512b..9ae64f31 100644
--- a/charon/tests/ui/issue-394-rpit-with-lifetime.rs
+++ b/charon/tests/ui/issue-394-rpit-with-lifetime.rs
@@ -1,5 +1,3 @@
-//@ known-failure
-
 fn sparse_transitions<'a>() -> impl Iterator<Item = u8> + 'a {
     core::iter::from_fn(|| None)
 }
diff --git a/charon/tests/ui/non-lifetime-gats.out b/charon/tests/ui/non-lifetime-gats.out
index 6ba04304..f50747cb 100644
--- a/charon/tests/ui/non-lifetime-gats.out
+++ b/charon/tests/ui/non-lifetime-gats.out
@@ -1,5 +1,7 @@
-thread 'rustc' panicked at src/bin/charon-driver/translate/translate_predicates.rs:356:17:
-assertion failed: nested.is_empty()
+error: Could not find the type variable "T" (index: 1)
+
+thread 'rustc' panicked at src/bin/charon-driver/translate/translate_predicates.rs:229:80:
+called `Result::unwrap()` on an `Err` value: Error { span: Span { span: RawSpan { file_id: 0, beg: Loc { line: 1, col: 0 }, end: Loc { line: 1, col: 0 }, rust_span_data: no-location (#0) }, generated_from_span: None }, msg: "Could not find the type variable \"T\" (index: 1)" }
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `test_crate::PointerFamily`.
  --> tests/ui/non-lifetime-gats.rs:4:1
@@ -37,6 +39,6 @@ error: Ignoring the following item due to an error: test_crate::moar_variables::
 38 |     impl<T> Trait<Option<T>> for Foo {
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: aborting due to 6 previous errors
+error: aborting due to 7 previous errors
 
 Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out
index 4d1f88df..d69e45c8 100644
--- a/charon/tests/ui/unsupported/advanced-const-generics.out
+++ b/charon/tests/ui/unsupported/advanced-const-generics.out
@@ -20,7 +20,7 @@ error[E9999]: Supposely unreachable place in the Rust AST. The label is "Transla
    = 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 src/bin/charon-driver/translate/translate_types.rs:790:50:
+thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:793:50:
 called `Option::unwrap()` on a `None` value
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `test_crate::foo`.

From de20cd62c3ed67aff47e9cbf91dad68d282ee4e9 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 15 Oct 2024 13:56:39 +0200
Subject: [PATCH 3/6] Emit a good error message for complex expressions in
 const generics

---
 .../translate/translate_types.rs              | 27 +++++++++----------
 .../unsupported/advanced-const-generics.out   |  9 +++----
 2 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 718d484e..934a6e31 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -666,7 +666,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         }
         if let Some((generics, predicates)) = def.generics() {
             // Add the generic params.
-            self.push_generic_params(span, generics)?;
+            self.push_generic_params(generics)?;
             // Add the self trait clause.
             match &def.kind {
                 FullDefKind::Impl {
@@ -757,22 +757,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         Ok(())
     }
 
-    pub(crate) fn push_generic_params(
-        &mut self,
-        span: Span,
-        generics: &hax::TyGenerics,
-    ) -> Result<(), Error> {
+    pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
         for param in &generics.params {
-            self.push_generic_param(span, param)?;
+            self.push_generic_param(param)?;
         }
         Ok(())
     }
 
-    pub(crate) fn push_generic_param(
-        &mut self,
-        span: Span,
-        param: &hax::GenericParamDef,
-    ) -> Result<(), Error> {
+    pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
         match &param.kind {
             hax::GenericParamDefKind::Lifetime => {
                 let region = hax::Region {
@@ -787,11 +779,18 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let _ = self.push_type_var(param.index, param.name.clone());
             }
             hax::GenericParamDefKind::Const { ty, .. } => {
+                let span = self.def_span(&param.def_id);
                 // The type should be primitive, meaning it shouldn't contain variables,
                 // non-primitive adts, etc. As a result, we can use an empty context.
                 let ty = self.translate_ty(span, false, ty)?;
-                let ty = *ty.kind().as_literal().unwrap();
-                self.push_const_generic_var(param.index, ty, param.name.clone());
+                match ty.kind().as_literal() {
+                    Some(ty) => self.push_const_generic_var(param.index, *ty, param.name.clone()),
+                    None => error_or_panic!(
+                        self,
+                        span,
+                        "Constant parameters of non-literal type are not supported"
+                    ),
+                }
             }
         }
 
diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out
index d69e45c8..e7103da8 100644
--- a/charon/tests/ui/unsupported/advanced-const-generics.out
+++ b/charon/tests/ui/unsupported/advanced-const-generics.out
@@ -20,14 +20,11 @@ error[E9999]: Supposely unreachable place in the Rust AST. The label is "Transla
    = 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 src/bin/charon-driver/translate/translate_types.rs:793:50:
-called `Option::unwrap()` on a `None` value
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-error: Thread panicked when extracting item `test_crate::foo`.
-  --> tests/ui/unsupported/advanced-const-generics.rs:14:1
+error: Constant parameters of non-literal type are not supported
+  --> tests/ui/unsupported/advanced-const-generics.rs:14:8
    |
 14 | fn foo<const X: Foo>() -> Foo {
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |        ^^^^^^^^^^^^
 
 error: Ignoring the following item due to an error: test_crate::foo
   --> tests/ui/unsupported/advanced-const-generics.rs:14:1

From 0c053c5e15ad830622ed622ecfa7a161351186c7 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 15 Oct 2024 16:39:58 +0200
Subject: [PATCH 4/6] Emit a proper error message for GATs

---
 .../translate/translate_predicates.rs         | 16 ++++-
 .../translate/translate_traits.rs             | 35 +++++++---
 .../translate/translate_types.rs              | 11 ++-
 charon/tests/ui/generic-associated-types.out  | 70 ++++++++++++++++---
 charon/tests/ui/non-lifetime-gats.out         | 31 ++++----
 5 files changed, 132 insertions(+), 31 deletions(-)

diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 1c212edd..45059601 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -1,7 +1,9 @@
 use super::translate_ctx::*;
 use super::translate_traits::PredicateLocation;
 use charon_lib::ast::*;
+use charon_lib::formatter::IntoFormatter;
 use charon_lib::ids::Vector;
+use charon_lib::pretty::FmtWithCtx;
 use hax_frontend_exporter as hax;
 
 impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
@@ -226,7 +228,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             // The trait ref should be Some(...): the marker traits (that
                             // we may filter) don't have associated types.
                             let trait_ref = trait_ref.unwrap();
-                            let ty = ctx.translate_ty(span, erase_regions, ty).unwrap();
+                            let ty = ctx.translate_ty(span, erase_regions, ty)?;
                             let type_name = TraitItemName(assoc_item.name.clone().into());
                             ctx.generic_params
                                 .trait_type_constraints
@@ -378,10 +380,22 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     match path_elem {
                         AssocItem {
                             item,
+                            generic_args,
                             predicate,
                             index,
                             ..
                         } => {
+                            if !generic_args.is_empty() {
+                                error_or_panic!(
+                                    self,
+                                    span,
+                                    format!(
+                                        "Found unsupported GAT `{}` when resolving trait `{}`",
+                                        item.name,
+                                        trait_decl_ref.fmt_with_ctx(&self.into_fmt())
+                                    )
+                                )
+                            }
                             trait_id = TraitRefKind::ItemClause(
                                 Box::new(trait_id),
                                 current_trait_decl_id,
diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index 1c6f4342..2f071716 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -156,6 +156,13 @@ impl BodyTransCtx<'_, '_, '_> {
                     let ty = self.translate_ty(item_span, erase_regions, ty)?;
                     consts.push((item_name.clone(), ty));
                 }
+                hax::FullDefKind::AssocTy { generics, .. } if !generics.params.is_empty() => {
+                    error_or_panic!(
+                        self,
+                        item_span,
+                        &format!("Generic associated types are not supported")
+                    );
+                }
                 hax::FullDefKind::AssocTy { value, .. } => {
                     // TODO: handle generics (i.e. GATs).
                     if let Some(clauses) = self.item_trait_clauses.get(item_name) {
@@ -309,12 +316,12 @@ impl BodyTransCtx<'_, '_, '_> {
         for (item, item_def) in impl_items {
             let name = TraitItemName(item.name.clone());
             let item_span = self.def_span(&item.def_id);
-            match &item.kind {
-                hax::AssocKind::Fn => {
+            match item_def.kind() {
+                hax::FullDefKind::AssocFn { .. } => {
                     let fun_id = self.register_fun_decl_id(item_span, &item.def_id);
                     methods.insert(name, fun_id);
                 }
-                hax::AssocKind::Const => {
+                hax::FullDefKind::AssocConst { .. } => {
                     // The parameters of the constant are the same as those of the item that
                     // declares them.
                     let gref = GlobalDeclRef {
@@ -323,7 +330,14 @@ impl BodyTransCtx<'_, '_, '_> {
                     };
                     consts.insert(name, gref);
                 }
-                hax::AssocKind::Type => {
+                hax::FullDefKind::AssocTy { generics, .. } if !generics.params.is_empty() => {
+                    error_or_panic!(
+                        self,
+                        item_span,
+                        &format!("Generic associated types are not supported")
+                    );
+                }
+                hax::FullDefKind::AssocTy { .. } => {
                     let hax::FullDefKind::AssocTy {
                         value: Some(ty), ..
                     } = item_def.kind()
@@ -333,6 +347,7 @@ impl BodyTransCtx<'_, '_, '_> {
                     let ty = self.translate_ty(item_span, erase_regions, &ty)?;
                     types.insert(name, ty);
                 }
+                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
             }
         }
 
@@ -351,8 +366,8 @@ impl BodyTransCtx<'_, '_, '_> {
             let item_def_id = decl_item_def.rust_def_id();
             let item_span = self.translate_span_from_hax(&decl_item_def.span);
             let name = TraitItemName(decl_item.name.to_string());
-            match &decl_item.kind {
-                hax::AssocKind::Fn => {
+            match decl_item_def.kind() {
+                hax::FullDefKind::AssocFn { .. } => {
                     if let Some(&fun_id) = methods.get(&name) {
                         // Check if we implement a required method or reimplement a provided
                         // method.
@@ -364,7 +379,7 @@ impl BodyTransCtx<'_, '_, '_> {
                     }
                 }
 
-                hax::AssocKind::Const => {
+                hax::FullDefKind::AssocConst { .. } => {
                     // Does the trait impl provide an implementation for this const?
                     let c = match partial_consts.get(&name) {
                         Some(c) => c.clone(),
@@ -381,7 +396,10 @@ impl BodyTransCtx<'_, '_, '_> {
                     };
                     consts.push((name, c));
                 }
-                hax::AssocKind::Type => {
+                hax::FullDefKind::AssocTy { generics, .. } if !generics.params.is_empty() => {
+                    // The error was already reported in the trait declaration.
+                }
+                hax::FullDefKind::AssocTy { .. } => {
                     // Does the trait impl provide an implementation for this type?
                     let ty = match partial_types.get(&name) {
                         Some(ty) => ty.clone(),
@@ -405,6 +423,7 @@ impl BodyTransCtx<'_, '_, '_> {
                     )?;
                     type_clauses.push((name, trait_refs));
                 }
+                _ => panic!("Unexpected definition for trait item: {decl_item_def:?}"),
             }
         }
         if item_meta.opacity.is_opaque() {
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 934a6e31..53d96ea1 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -715,12 +715,19 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             };
             self.register_predicates(predicates, origin, &location)?;
 
-            // Also add the predicates on associated types.
             if let hax::FullDefKind::Trait { items, .. } = &def.kind
                 && !is_parent
             {
+                // Also add the predicates on associated types.
+                // FIXME(gat): don't skip GATs.
                 for (item, item_def) in items {
-                    if let hax::FullDefKind::AssocTy { predicates, .. } = &item_def.kind {
+                    if let hax::FullDefKind::AssocTy {
+                        generics,
+                        predicates,
+                        ..
+                    } = &item_def.kind
+                        && generics.params.is_empty()
+                    {
                         let name = TraitItemName(item.name.clone());
                         self.register_predicates(
                             &predicates,
diff --git a/charon/tests/ui/generic-associated-types.out b/charon/tests/ui/generic-associated-types.out
index 57a82c7b..02f5e6be 100644
--- a/charon/tests/ui/generic-associated-types.out
+++ b/charon/tests/ui/generic-associated-types.out
@@ -1,10 +1,28 @@
-error: Could not find region: Region { kind: ReEarlyParam(EarlyParamRegion { index: 2, name: "'b" }) }
-       
-       Region vars map:
-       {Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }: 0}
-       
-       Bound region vars:
-       []
+error: Generic associated types are not supported
+ --> tests/ui/generic-associated-types.rs:5:5
+  |
+5 |     type Item<'a>
+  |     ^^^^^^^^^^^^^
+
+error: Ignoring the following item due to an error: test_crate::LendingIterator
+ --> tests/ui/generic-associated-types.rs:4:1
+  |
+4 | trait LendingIterator {
+  | ^^^^^^^^^^^^^^^^^^^^^
+
+error: Generic associated types are not supported
+  --> tests/ui/generic-associated-types.rs:46:9
+   |
+46 |         type Type<'b>: for<'c> Foo<&'a &'b &'c ()>;
+   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: Ignoring the following item due to an error: test_crate::lifetimes::Bar
+  --> tests/ui/generic-associated-types.rs:45:5
+   |
+45 |     trait Bar<'a> {
+   |     ^^^^^^^^^^^^^
+
+error: Generic associated types are not supported
   --> tests/ui/generic-associated-types.rs:13:5
    |
 13 |     type Item<'b> = &'b T;
@@ -16,6 +34,30 @@ error: Ignoring the following item due to an error: test_crate::{impl#0}
 12 | impl<'a, T> LendingIterator for Option<&'a T> {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
+error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>`
+  --> tests/ui/generic-associated-types.rs:27:28
+   |
+27 |     while let Some(item) = iter.next() {
+   |                            ^^^^^^^^^^^
+
+error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>`
+  --> tests/ui/generic-associated-types.rs:27:28
+   |
+27 |     while let Some(item) = iter.next() {
+   |                            ^^^^^^^^^^^
+
+error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<Self::Item>`
+ --> tests/ui/generic-associated-types.rs:9:5
+  |
+9 |     fn next<'a>(&'a mut self) -> Option<Self::Item<'a>>;
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<Self::Item>`
+ --> tests/ui/generic-associated-types.rs:9:5
+  |
+9 |     fn next<'a>(&'a mut self) -> Option<Self::Item<'a>>;
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 warning: unused variable: `x`
   --> tests/ui/generic-associated-types.rs:33:9
    |
@@ -24,6 +66,18 @@ warning: unused variable: `x`
    |
    = note: `#[warn(unused_variables)]` on by default
 
-error: aborting due to 2 previous errors; 1 warning emitted
+error: Found unsupported GAT `Type` when resolving trait `test_crate::lifetimes::Foo<@TraitClause1::Type, &'_ (&'_ (&'_ (())))>`
+  --> tests/ui/generic-associated-types.rs:53:9
+   |
+53 |         x.foo()
+   |         ^^^^^^^
+
+error: Error during trait resolution: Found unsupported GAT `Type` when resolving trait `test_crate::lifetimes::Foo<@TraitClause1::Type, &'_ (&'_ (&'_ (())))>`
+  --> tests/ui/generic-associated-types.rs:53:9
+   |
+53 |         x.foo()
+   |         ^^^^^^^
+
+error: aborting due to 12 previous errors; 1 warning emitted
 
 Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/non-lifetime-gats.out b/charon/tests/ui/non-lifetime-gats.out
index f50747cb..ffac7358 100644
--- a/charon/tests/ui/non-lifetime-gats.out
+++ b/charon/tests/ui/non-lifetime-gats.out
@@ -1,13 +1,8 @@
-error: Could not find the type variable "T" (index: 1)
-
-thread 'rustc' panicked at src/bin/charon-driver/translate/translate_predicates.rs:229:80:
-called `Result::unwrap()` on an `Err` value: Error { span: Span { span: RawSpan { file_id: 0, beg: Loc { line: 1, col: 0 }, end: Loc { line: 1, col: 0 }, rust_span_data: no-location (#0) }, generated_from_span: None }, msg: "Could not find the type variable \"T\" (index: 1)" }
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-error: Thread panicked when extracting item `test_crate::PointerFamily`.
- --> tests/ui/non-lifetime-gats.rs:4:1
+error: Generic associated types are not supported
+ --> tests/ui/non-lifetime-gats.rs:5:5
   |
-4 | trait PointerFamily {
-  | ^^^^^^^^^^^^^^^^^^^
+5 |     type Pointer<T>: Deref<Target = T>;
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 error: Ignoring the following item due to an error: test_crate::PointerFamily
  --> tests/ui/non-lifetime-gats.rs:4:1
@@ -15,7 +10,19 @@ error: Ignoring the following item due to an error: test_crate::PointerFamily
 4 | trait PointerFamily {
   | ^^^^^^^^^^^^^^^^^^^
 
-error: Could not find the type variable "T" (index: 0)
+error: Generic associated types are not supported
+  --> tests/ui/non-lifetime-gats.rs:34:9
+   |
+34 |         type Type<U>: Link<T>;
+   |         ^^^^^^^^^^^^^^^^^^^^^
+
+error: Ignoring the following item due to an error: test_crate::moar_variables::Trait
+  --> tests/ui/non-lifetime-gats.rs:33:5
+   |
+33 |     trait Trait<T> {
+   |     ^^^^^^^^^^^^^^
+
+error: Generic associated types are not supported
   --> tests/ui/non-lifetime-gats.rs:13:5
    |
 13 |     type Pointer<T> = Box<T>;
@@ -27,7 +34,7 @@ error: Ignoring the following item due to an error: test_crate::{impl#0}
 12 | impl PointerFamily for BoxFamily {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: Could not find the type variable "U" (index: 1)
+error: Generic associated types are not supported
   --> tests/ui/non-lifetime-gats.rs:39:9
    |
 39 |         type Type<U> = (T, U);
@@ -39,6 +46,6 @@ error: Ignoring the following item due to an error: test_crate::moar_variables::
 38 |     impl<T> Trait<Option<T>> for Foo {
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: aborting due to 7 previous errors
+error: aborting due to 8 previous errors
 
 Error: Charon driver exited with code 101

From 5818d1eec88209385bbacea0b03d1e8bc3f79559 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 15 Oct 2024 16:31:18 +0200
Subject: [PATCH 5/6] Remove leftover code path

We no longer filter traits during translation.
---
 .../translate/translate_constants.rs          |  3 --
 .../translate/translate_functions_to_ullbc.rs | 12 ++-----
 .../translate/translate_predicates.rs         | 33 +++++++------------
 .../translate/translate_traits.rs             |  4 +--
 .../translate/translate_types.rs              |  5 +--
 5 files changed, 16 insertions(+), 41 deletions(-)

diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs
index aa7f34e9..d3d51f89 100644
--- a/charon/src/bin/charon-driver/translate/translate_constants.rs
+++ b/charon/src/bin/charon-driver/translate/translate_constants.rs
@@ -111,9 +111,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             }
             ConstantExprKind::TraitConst { impl_expr, name } => {
                 let trait_ref = self.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
-                // The trait ref should be Some(...): trait markers (that we
-                // may eliminate) don't have constants.
-                let trait_ref = trait_ref.unwrap();
                 let name = TraitItemName(name.clone());
                 RawConstantExpr::TraitConst(trait_ref, name)
             }
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 75cc3963..dbe20cac 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
@@ -848,18 +848,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             let fun_id = self.register_fun_decl_id(span, def_id);
             // Two cases depending on whether we call a trait method or not
             match trait_info {
-                None => {
-                    // "Regular" function call
-                    FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id))
-                }
+                // Direct function call
+                None => FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)),
+                // Trait method
                 Some(trait_info) => {
-                    // Trait method
                     let impl_expr =
                         self.translate_trait_impl_expr(span, erase_regions, trait_info)?;
-                    // The impl source should be Some(...): trait markers (that we may
-                    // eliminate) don't have methods.
-                    let impl_expr = impl_expr.unwrap();
-
                     let method_name = self.t_ctx.translate_trait_item_name(def_id)?;
                     FunIdOrTraitMethodRef::Trait(impl_expr, method_name, fun_id)
                 }
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 45059601..456b8137 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -81,14 +81,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         Ok(())
     }
 
-    /// Returns an [Option] because we may filter trait refs about builtin or
-    /// auto traits like [core::marker::Sized] and [core::marker::Sync].
     pub(crate) fn translate_trait_decl_ref(
         &mut self,
         span: Span,
         erase_regions: bool,
         bound_trait_ref: &hax::Binder<hax::TraitRef>,
-    ) -> Result<Option<PolyTraitDeclRef>, Error> {
+    ) -> Result<PolyTraitDeclRef, Error> {
         let binder = bound_trait_ref.rebind(());
         self.with_locally_bound_regions_group(span, binder, move |ctx| {
             let trait_ref = bound_trait_ref.hax_skip_binder_ref();
@@ -102,10 +100,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 &parent_trait_refs,
             )?;
 
-            Ok(Some(RegionBinder {
+            Ok(RegionBinder {
                 regions: ctx.region_vars[0].clone(),
                 skip_binder: TraitDeclRef { trait_id, generics },
-            }))
+            })
         })
     }
 
@@ -225,9 +223,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                             let trait_ref =
                                 ctx.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
-                            // The trait ref should be Some(...): the marker traits (that
-                            // we may filter) don't have associated types.
-                            let trait_ref = trait_ref.unwrap();
                             let ty = ctx.translate_ty(span, erase_regions, ty)?;
                             let type_name = TraitItemName(assoc_item.name.clone().into());
                             ctx.generic_params
@@ -272,27 +267,21 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         erase_regions: bool,
         impl_sources: &[hax::ImplExpr],
     ) -> Result<Vector<TraitClauseId, TraitRef>, Error> {
-        let res: Vec<_> = impl_sources
+        impl_sources
             .iter()
             .map(|x| self.translate_trait_impl_expr(span, erase_regions, x))
-            .try_collect()?;
-        Ok(res.into_iter().flatten().collect())
+            .try_collect()
     }
 
-    /// Returns an [Option] because we may ignore some builtin or auto traits
-    /// like [core::marker::Sized] or [core::marker::Sync].
     #[tracing::instrument(skip(self, span, erase_regions, impl_expr))]
     pub(crate) fn translate_trait_impl_expr(
         &mut self,
         span: Span,
         erase_regions: bool,
         impl_expr: &hax::ImplExpr,
-    ) -> Result<Option<TraitRef>, Error> {
+    ) -> Result<TraitRef, Error> {
         let trait_decl_ref =
-            match self.translate_trait_decl_ref(span, erase_regions, &impl_expr.r#trait)? {
-                None => return Ok(None),
-                Some(tr) => tr,
-            };
+            self.translate_trait_decl_ref(span, erase_regions, &impl_expr.r#trait)?;
 
         match self.translate_trait_impl_expr_aux(
             span,
@@ -307,10 +296,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 } else {
                     let msg = format!("Error during trait resolution: {}", &err.msg);
                     self.span_err(span, &msg);
-                    Ok(Some(TraitRef {
+                    Ok(TraitRef {
                         kind: TraitRefKind::Unknown(err.msg),
                         trait_decl_ref,
-                    }))
+                    })
                 }
             }
         }
@@ -322,7 +311,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         erase_regions: bool,
         impl_source: &hax::ImplExpr,
         trait_decl_ref: PolyTraitDeclRef,
-    ) -> Result<Option<TraitRef>, Error> {
+    ) -> Result<TraitRef, Error> {
         trace!("impl_expr: {:#?}", impl_source);
         use hax::ImplExprAtom;
 
@@ -453,6 +442,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 trait_ref
             }
         };
-        Ok(Some(trait_ref))
+        Ok(trait_ref)
     }
 }
diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index 2f071716..64724228 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -57,9 +57,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let trait_ref = bound.kind().rebind(trait_pred.trait_ref);
                 let trait_ref = hax::solve_trait(&self.hax_state, trait_ref);
                 let trait_ref = self.translate_trait_impl_expr(span, erase_regions, &trait_ref)?;
-                if let Some(trait_ref) = trait_ref {
-                    trait_refs.push(trait_ref);
-                }
+                trait_refs.push(trait_ref);
             }
         }
 
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 53d96ea1..575cb0cf 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -171,10 +171,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 } => {
                     let trait_ref =
                         self.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
-                    // This should succeed because no marker trait (that we may
-                    // ignore) has associated types.
-                    let trait_ref = trait_ref.unwrap();
-                    let name = TraitItemName(assoc_item.name.clone().into());
+                    let name = TraitItemName(assoc_item.name.clone());
                     TyKind::TraitType(trait_ref, name)
                 }
                 hax::AliasKind::Opaque { hidden_ty, .. } => {

From a1566c06bc3d4e8642c5882104f9ca47f0f15eb3 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 15 Oct 2024 17:30:30 +0200
Subject: [PATCH 6/6] Improve some error messages

---
 .../charon-driver/translate/translate_ctx.rs  |  5 +++
 .../translate/translate_functions_to_ullbc.rs | 32 ++++++++++++-------
 .../translate/translate_predicates.rs         |  9 +++++-
 .../translate/translate_types.rs              |  6 +++-
 charon/src/transform/hide_marker_traits.rs    |  3 +-
 charon/tests/ui/error-dependencies.rs         |  2 +-
 charon/tests/ui/issue-378-ctor-as-fn.out      | 16 ++++++++--
 .../tests/ui/unsupported/unbound-lifetime.out | 12 +++----
 .../tests/ui/unsupported/unbound-lifetime.rs  |  1 +
 .../ui/unsupported/well-formedness-bound.out  |  2 +-
 10 files changed, 63 insertions(+), 25 deletions(-)

diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
index 3f96eeb7..3a41944c 100644
--- a/charon/src/bin/charon-driver/translate/translate_ctx.rs
+++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -397,6 +397,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                 // block.
                 None
             }
+            DefPathData::Ctor => {
+                // Do nothing, the constructor of a struct/variant has the same name as the
+                // struct/variant.
+                None
+            }
             _ => {
                 error_or_panic!(
                     self,
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 dbe20cac..edf99a90 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
@@ -55,14 +55,6 @@ fn translate_borrow_kind(borrow_kind: hax::BorrowKind) -> BorrowKind {
     }
 }
 
-fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp {
-    match binop {
-        hax::UnOp::Not => UnOp::Not,
-        hax::UnOp::Neg => UnOp::Neg,
-        hax::UnOp::PtrMetadata => unimplemented!("Unop::PtrMetadata"),
-    }
-}
-
 impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
     fn translate_binaryop_kind(&mut self, span: Span, binop: hax::BinOp) -> Result<BinOp, Error> {
         Ok(match binop {
@@ -601,10 +593,19 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 };
                 Ok(Rvalue::NullaryOp(op, ty))
             }
-            hax::Rvalue::UnaryOp(unop, operand) => Ok(Rvalue::UnaryOp(
-                translate_unaryop_kind(*unop),
-                self.translate_operand(span, operand)?,
-            )),
+            hax::Rvalue::UnaryOp(unop, operand) => {
+                let unop = match unop {
+                    hax::UnOp::Not => UnOp::Not,
+                    hax::UnOp::Neg => UnOp::Neg,
+                    hax::UnOp::PtrMetadata => {
+                        error_or_panic!(self, span, "Unsupported operation: PtrMetadata")
+                    }
+                };
+                Ok(Rvalue::UnaryOp(
+                    unop,
+                    self.translate_operand(span, operand)?,
+                ))
+            }
             hax::Rvalue::Discriminant(place) => {
                 let (place, ty) = self.translate_place_with_type(span, place)?;
                 if let TyKind::Adt(TypeId::Adt(adt_id), _) = ty.kind() {
@@ -1362,6 +1363,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             hax::FullDefKind::Closure { args, .. } => &args.sig,
             hax::FullDefKind::Fn { sig, .. } => sig,
             hax::FullDefKind::AssocFn { sig, .. } => sig,
+            hax::FullDefKind::Ctor { .. } => {
+                error_or_panic!(
+                    self,
+                    span,
+                    "Casting constructors to function pointers is not supported"
+                )
+            }
             _ => panic!("Unexpected definition for function: {def:?}"),
         };
 
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 456b8137..8ecaebac 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -241,7 +241,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             // the type information in the const generic parameters
                             // directly? For now we just ignore it.
                         }
-                        ClauseKind::WellFormed(_) | ClauseKind::ConstEvaluatable(_) => {
+                        ClauseKind::WellFormed(_) => {
+                            error_or_panic!(
+                                ctx,
+                                span,
+                                format!("Well-formedness clauses are unsupported")
+                            )
+                        }
+                        ClauseKind::ConstEvaluatable(_) => {
                             error_or_panic!(ctx, span, format!("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 575cb0cf..9bd7565a 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -178,7 +178,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     return self.translate_ty(span, erase_regions, hidden_ty)
                 }
                 _ => {
-                    error_or_panic!(self, span, format!("Unimplemented: {:?}", ty))
+                    error_or_panic!(
+                        self,
+                        span,
+                        format!("Unsupported alias type: {:?}", alias.kind)
+                    )
                 }
             },
 
diff --git a/charon/src/transform/hide_marker_traits.rs b/charon/src/transform/hide_marker_traits.rs
index 83a822f7..fa3c7e40 100644
--- a/charon/src/transform/hide_marker_traits.rs
+++ b/charon/src/transform/hide_marker_traits.rs
@@ -94,7 +94,8 @@ impl TransformPass for Transform {
             .item_names
             .iter()
             .filter(|(_, name)| exclude.iter().any(|p| p.matches(&ctx.translated, name)))
-            .map(|(id, _)| *id.as_trait_decl().unwrap())
+            .filter_map(|(id, _)| id.as_trait_decl())
+            .copied()
             .collect();
 
         for &id in &exclude {
diff --git a/charon/tests/ui/error-dependencies.rs b/charon/tests/ui/error-dependencies.rs
index b0ab6aa8..e573af17 100644
--- a/charon/tests/ui/error-dependencies.rs
+++ b/charon/tests/ui/error-dependencies.rs
@@ -1,5 +1,5 @@
 //@ known-failure
-//! This file tests the error messages that indicates why we attempte to translate a given
+//! This file tests the error messages that indicates why we attempt to translate a given
 //! definition.
 #![feature(register_tool)]
 #![register_tool(charon)]
diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out
index 483f4935..13e09ad4 100644
--- a/charon/tests/ui/issue-378-ctor-as-fn.out
+++ b/charon/tests/ui/issue-378-ctor-as-fn.out
@@ -1,6 +1,18 @@
-error: Unexpected DefPathData for `core::option::Option::Some::{constructor#0}`: DisambiguatedDefPathData { data: Ctor, disambiguator: 0 }
+error: Casting constructors to function pointers is not supported
  --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:579:5
 
-error: aborting due to 1 previous error
+error: Ignoring the following item due to an error: core::option::Option::Some::{constructor#0}
+ --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:579:5
+
+error: The external definition `core::option::Option::Some` triggered errors. It is (transitively) used at the following location(s):
+ --> tests/ui/issue-378-ctor-as-fn.rs:3:34
+  |
+3 | static F: fn(u8) -> Option<u8> = Some;
+  |                                  ^^^^
+...
+6 |     let f: fn(u8) -> _ = Some;
+  |                          ^^^^
+
+error: aborting due to 3 previous errors
 
 Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/unsupported/unbound-lifetime.out b/charon/tests/ui/unsupported/unbound-lifetime.out
index c412b5f3..881685ef 100644
--- a/charon/tests/ui/unsupported/unbound-lifetime.out
+++ b/charon/tests/ui/unsupported/unbound-lifetime.out
@@ -1,7 +1,7 @@
 error[E0261]: use of undeclared lifetime name `'a`
- --> tests/ui/unsupported/unbound-lifetime.rs:4:13
+ --> tests/ui/unsupported/unbound-lifetime.rs:5:13
   |
-4 | fn get(_x: &'a u32) {}
+5 | fn get(_x: &'a u32) {}
   |       -     ^^ undeclared lifetime
   |       |
   |       help: consider introducing lifetime `'a` here: `<'a>`
@@ -13,15 +13,15 @@ error: Could not find region: Region { kind: ReError(ErrorGuaranteed { todo: "Er
        
        Bound region vars:
        [[]]
- --> tests/ui/unsupported/unbound-lifetime.rs:4:1
+ --> tests/ui/unsupported/unbound-lifetime.rs:5:1
   |
-4 | fn get(_x: &'a u32) {}
+5 | fn get(_x: &'a u32) {}
   | ^^^^^^^^^^^^^^^^^^^^^^
 
 error: Ignoring the following item due to an error: test_crate::get
- --> tests/ui/unsupported/unbound-lifetime.rs:4:1
+ --> tests/ui/unsupported/unbound-lifetime.rs:5:1
   |
-4 | fn get(_x: &'a u32) {}
+5 | fn get(_x: &'a u32) {}
   | ^^^^^^^^^^^^^^^^^^^
 
 error: aborting due to 3 previous errors
diff --git a/charon/tests/ui/unsupported/unbound-lifetime.rs b/charon/tests/ui/unsupported/unbound-lifetime.rs
index db498815..466bb46d 100644
--- a/charon/tests/ui/unsupported/unbound-lifetime.rs
+++ b/charon/tests/ui/unsupported/unbound-lifetime.rs
@@ -1,4 +1,5 @@
 //@ known-failure
+// See https://github.com/AeneasVerif/charon/issues/306
 
 // This is incorrect code but the error is weird.
 fn get(_x: &'a u32) {}
diff --git a/charon/tests/ui/unsupported/well-formedness-bound.out b/charon/tests/ui/unsupported/well-formedness-bound.out
index f576b183..bc782121 100644
--- a/charon/tests/ui/unsupported/well-formedness-bound.out
+++ b/charon/tests/ui/unsupported/well-formedness-bound.out
@@ -1,4 +1,4 @@
-error: Unsupported clause: WellFormed(Type(Ty { kind: Ref(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }, Ty { kind: Tuple([]) }, false) }))
+error: Well-formedness clauses are unsupported
  --> tests/ui/unsupported/well-formedness-bound.rs:4:5
   |
 4 |     &'a ():,