Merge pull request #415 from Nadrieril/mismatched-trait-refs

charon/Cargo.toml

@@ -76,6 +76,7 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] }
 which = "6.0.1"
 
 hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+# hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 
 [features]

charon/tests/ui/generic-associated-types.out

@@ -1,18 +1,3 @@
-thread 'rustc' panicked at compiler/rustc_trait_selection/src/traits/normalize.rs:151:9:
-Normalizing <<Self as LendingIterator>::Item<'a> as std::marker::Sized> without wrapping in a `Binder`
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-error: Thread panicked when extracting item `test_crate::LendingIterator`.
- --> tests/ui/generic-associated-types.rs:4:1
-  |
-4 | trait LendingIterator {
-  | ^^^^^^^^^^^^^^^^^^^^^
-
-error: Ignoring the following item due to an error: test_crate::LendingIterator
- --> tests/ui/generic-associated-types.rs:4:1
-  |
-4 | trait LendingIterator {
-  | ^^^^^^^^^^^^^^^^^^^^^
-
 error: Could not find region: Region { kind: ReEarlyParam(EarlyParamRegion { index: 2, name: "'b" }) }
 
        Region vars map:
@@ -31,20 +16,6 @@ error: Ignoring the following item due to an error: test_crate::{impl#0}
 12 | impl<'a, T> LendingIterator for Option<&'a T> {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-thread 'rustc' panicked at compiler/rustc_trait_selection/src/traits/normalize.rs:151:9:
-Normalizing <<Self as LendingIterator>::Item<'a> as std::marker::Sized> without wrapping in a `Binder`
-error: Thread panicked when extracting item `test_crate::LendingIterator::next`.
- --> tests/ui/generic-associated-types.rs:9:5
-  |
-9 |     fn next<'a>(&'a mut self) -> Option<Self::Item<'a>>;
-  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-error: Ignoring the following item due to an error: test_crate::LendingIterator::next
- --> 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
    |
@@ -53,6 +24,6 @@ warning: unused variable: `x`
    |
    = note: `#[warn(unused_variables)]` on by default
 
-error: aborting due to 6 previous errors; 1 warning emitted
+error: aborting due to 2 previous errors; 1 warning emitted
 
 Error: Charon driver exited with code 101

charon/tests/ui/issue-369-mismatched-genericparams.out

@@ -1,13 +1,42 @@
-error: Mismatched generics:
-       expected: GenericParams { regions: [], types: [Some(TypeVar { index: 0, name: "T" })], const_generics: [], trait_clauses: [Some(TraitClause { clause_id: 0, span: Some(Span { span: RawSpan { file_id: 0, beg: Loc { line: 12, col: 5 }, end: Loc { line: 12, col: 6 }, rust_span_data: tests/ui/issue-369-mismatched-genericparams.rs:12:6: 12:7 (#0) }, generated_from_span: None }), origin: WhereClauseOnImpl, trait_: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 2, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })], regions_outlive: [], types_outlive: [], trait_type_constraints: [] }
-            got: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 2, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } }), Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 2, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })] }
-  --> tests/ui/issue-369-mismatched-genericparams.rs:8:1
-   |
-8  | / impl<T> Try for Option<T> {
-9  | |     type Residual = ();
-10 | | }
-   | |_^
-
-error: aborting due to 1 previous error
-
-Error: Charon driver exited with code 101
+# Final LLBC before serialization:
+
+trait core::marker::Sized<Self>
+
+trait test_crate::FromResidual<Self, R>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<R>
+}
+
+trait test_crate::Try<Self>
+{
+    parent_clause0 : [@TraitClause0]: test_crate::FromResidual<Self, ()>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::Residual>
+    type Residual
+}
+
+enum core::option::Option<T>
+  where
+      [@TraitClause0]: core::marker::Sized<T>,
+ =
+|  None()
+|  Some(T)
+
+
+impl<T> test_crate::{impl test_crate::Try for core::option::Option<T>[@TraitClause0]}<T> : test_crate::Try<core::option::Option<T>[@TraitClause0]>
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+{
+    parent_clause0 = test_crate::{impl test_crate::FromResidual<test_crate::{impl test_crate::Try for core::option::Option<T>[@TraitClause0]}<T>[@TraitClause0]::Residual> for core::option::Option<T>[@TraitClause0]}#1<T>[@TraitClause0]
+    parent_clause1 = core::marker::Sized<()>
+    type Residual = ()
+}
+
+impl<T> test_crate::{impl test_crate::FromResidual<test_crate::{impl test_crate::Try for core::option::Option<T>[@TraitClause0]}<T>[@TraitClause0]::Residual> for core::option::Option<T>[@TraitClause0]}#1<T> : test_crate::FromResidual<core::option::Option<T>[@TraitClause0], test_crate::{impl test_crate::Try for core::option::Option<T>[@TraitClause0]}<T>[@TraitClause0]::Residual>
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+{
+    parent_clause0 = core::marker::Sized<()>
+}
+
+
+

charon/tests/ui/issue-369-mismatched-genericparams.rs

@@ -1,4 +1,3 @@
-//@ known-failure
 pub trait Try: FromResidual<()> {
     type Residual;
 }

charon/tests/ui/issue-393-shallowinitbox.out

@@ -6,11 +6,6 @@ error: Unexpected `ShallowInitBox`
 5 | | }
   | |_^
 
-error: Mismatched generics:
-       expected: GenericParams { regions: [], types: [Some(TypeVar { index: 0, name: "T" })], const_generics: [], trait_clauses: [Some(TraitClause { clause_id: 0, span: Some(Span { span: RawSpan { file_id: 5, beg: Loc { line: 2498, col: 5 }, end: Loc { line: 2498, col: 6 }, rust_span_data: /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2498:6: 2498:7 (#0) }, generated_from_span: None }), origin: WhereClauseOnImpl, trait_: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })], regions_outlive: [], types_outlive: [], trait_type_constraints: [] }
-            got: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } }), Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })] }
- --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2479:1
-
-error: aborting due to 2 previous errors
+error: aborting due to 1 previous error
 
 Error: Charon driver exited with code 101

charon/tests/ui/quantified-clause.out

@@ -19,21 +19,6 @@ error: Ignoring the following item due to an error: test_crate::{impl#0}
 26 | |     for<'a> <&'a Result<T, U> as IntoIterator>::Item: Copy,
    | |___________________________________________________________^
 
-thread 'rustc' panicked at compiler/rustc_trait_selection/src/traits/normalize.rs:151:9:
-Normalizing &'^1_0.Named(test_crate::f::'a, "'a") u8 without wrapping in a `Binder`
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-error: Thread panicked when extracting item `test_crate::f`.
-  --> tests/ui/quantified-clause.rs:16:1
-   |
-16 | pub fn f<'a>(_: &'a ()) -> Option<(&'a u8,)> {
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-error: Ignoring the following item due to an error: test_crate::f
-  --> tests/ui/quantified-clause.rs:16:1
-   |
-16 | pub fn f<'a>(_: &'a ()) -> Option<(&'a u8,)> {
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-error: aborting due to 4 previous errors; 1 warning emitted
+error: aborting due to 2 previous errors; 1 warning emitted
 
 Error: Charon driver exited with code 101

charon/tests/ui/traits.out

@@ -947,6 +947,72 @@ impl test_crate::{impl test_crate::RecursiveImpl for ()}#17 : test_crate::Recurs
     type Item = ()
 }
 
+fn test_crate::flabada<'a>(@1: &'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>]
+{
+    let @0: test_crate::Wrapper<(bool, &'_ (()))>[core::marker::Sized<(bool, &'_ (()))>]; // return
+    let _x@1: &'_ (()); // arg #1
+
+    panic(core::panicking::panic)
+}
+
+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
+}
+
+trait core::ops::function::Fn<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: core::ops::function::FnMut<Self, Args>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Args>
+    parent_clause2 : [@TraitClause2]: core::marker::Tuple<Args>
+    fn call : core::ops::function::Fn::call
+}
+
+fn test_crate::call<'a, F>(@1: F)
+where
+    [@TraitClause0]: core::marker::Sized<F>,
+    [@TraitClause1]: core::ops::function::Fn<F, (&'_ (()))>,
+    @TraitClause1::parent_clause0::parent_clause0::Output = test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'_ (()))>],
+{
+    let @0: (); // return
+    let @1: F; // arg #1
+    let @2: (); // anonymous local
+
+    @2 := ()
+    @0 := move (@2)
+    drop @1
+    @0 := ()
+    return
+}
+
+fn test_crate::flibidi()
+{
+    let @0: (); // return
+    let @1: (); // anonymous local
+    let @2: (); // anonymous local
+
+    @1 := test_crate::call<'_, fn<'a>(&'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>]>[core::marker::Sized<fn<'a>(&'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>]>, core::ops::function::Fn<fn<'a>(&'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>], (&'_ (()))>](const (test_crate::flabada))
+    drop @1
+    @2 := ()
+    @0 := move (@2)
+    @0 := ()
+    return
+}
+
 fn test_crate::WithConstTy::f<'_0, '_1, Self, const LEN : usize>(@1: &'_0 mut (Self::W), @2: &'_1 (Array<u8, const LEN : usize>))
 
 fn test_crate::IntoIterator::into_iter<Self>(@1: Self) -> Self::IntoIter
@@ -959,5 +1025,11 @@ fn test_crate::CFnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args)
 
 fn test_crate::CFn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> Self::parent_clause0::parent_clause0::Output
 
+fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> Self::parent_clause0::parent_clause0::Output
+
+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
+
 
 

charon/tests/ui/traits.rs

@@ -346,3 +346,13 @@ trait RecursiveImpl {
 impl RecursiveImpl for () {
     type Item = ();
 }
+
+pub fn flabada<'a>(_x: &'a ()) -> Wrapper<(bool, &'a ())> {
+    todo!()
+}
+
+pub fn call<'a, F: Fn(&'a ()) -> Wrapper<(bool, &'a ())>>(_: F) {}
+
+pub fn flibidi() -> () {
+    call(flabada);
+}