diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index ad42e6d98..eb14359db 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -299,15 +299,6 @@ pub trait IntoImplExpr<'tcx> { ) -> ImplExpr; } -impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::TraitRef<'tcx> { - fn impl_expr>( - &self, - s: &S, - param_env: rustc_middle::ty::ParamEnv<'tcx>, - ) -> ImplExpr { - rustc_middle::ty::Binder::dummy(self.clone()).impl_expr(s, param_env) - } -} impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitPredicate<'tcx> { fn impl_expr>( &self, diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 2b2e4e657..effdaa604 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1592,10 +1592,51 @@ impl Alias { use rustc_type_ir::sty::AliasKind as RustAliasKind; let kind = match alias_kind { RustAliasKind::Projection => { + use rustc_middle::ty::{Binder, EarlyBinder, TypeVisitableExt}; let tcx = s.base().tcx; + let trait_ref = alias_ty.trait_ref(tcx); + // Sometimes (see + // https://github.com/hacspec/hax/issues/495), we get + // trait refs with escaping bound vars. Empirically, + // this seems fine. If we detect such a situation, we + // emit a warning with a lot of debugging information. + let poly_trait_ref = if trait_ref.has_escaping_bound_vars() { + let trait_ref_and_substs = alias_ty.trait_ref_and_own_substs(tcx); + let rebased_substs = alias_ty.rebase_substs_onto_impl(alias_ty.substs, tcx); + let norm_rebased_substs = tcx.try_subst_and_normalize_erasing_regions( + rebased_substs, + get_param_env(s), + EarlyBinder::bind(trait_ref), + ); + let norm_substs = tcx.try_subst_and_normalize_erasing_regions( + alias_ty.substs, + get_param_env(s), + EarlyBinder::bind(trait_ref), + ); + let early_binder_substs = + std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { + EarlyBinder::bind(trait_ref).subst(tcx, alias_ty.substs) + })); + let early_binder_rebased_substs = + std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { + EarlyBinder::bind(trait_ref).subst(tcx, alias_ty.substs) + })); + warning!( + s, + "Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495"; + {alias_ty, alias_kind, trait_ref, trait_ref_and_substs, rebased_substs, + norm_rebased_substs, norm_substs, + early_binder_substs, early_binder_rebased_substs} + ); + // we cannot use `Binder::dummy`: it asserts that + // there is no any escaping bound vars + Binder::bind_with_vars(trait_ref, rustc_middle::ty::List::empty()) + } else { + Binder::dummy(trait_ref) + }; AliasKind::Projection { assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s), - impl_expr: alias_ty.trait_ref(tcx).impl_expr(s, get_param_env(s)), + impl_expr: poly_trait_ref.impl_expr(s, get_param_env(s)), } } RustAliasKind::Inherent => AliasKind::Inherent, diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index f1eeafa27..b26c947a8 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -23,12 +23,180 @@ info: exit = 0 stderr = ''' Compiling traits v0.1.0 (WORKSPACE_ROOT/traits) +disabled backtrace +warning[HaxFront]: Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495 + + Context: + - alias_ty: AliasTy { + substs: [ + P, + (&u8,), + ], + def_id: DefId(2:2933 ~ core[7e13]::ops::function::FnOnce::Output), + } + - alias_kind: Projection + - trait_ref:

> + - trait_ref_and_substs: ( +

>, + [], + ) + - rebased_substs: [ + P, + (&u8,), + (&u8,), + ] + - norm_rebased_substs: Ok( +

>, + ) + - norm_substs: Ok( +

>, + ) + - early_binder_substs: Ok( +

>, + ) + - early_binder_rebased_substs: Ok( +

>, + ) + --> traits/src/lib.rs:107:13 + | +107 | impl bool> Trait for P {} + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + = 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)! + +disabled backtrace +disabled backtrace +disabled backtrace +disabled backtrace +disabled backtrace +disabled backtrace +disabled backtrace +disabled backtrace +warning[HaxFront]: Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495 + + Context: + - alias_ty: AliasTy { + substs: [ + P, + (&::Item,), + ], + def_id: DefId(2:2933 ~ core[7e13]::ops::function::FnOnce::Output), + } + - alias_kind: Projection + - trait_ref:

::Item,)>> + - trait_ref_and_substs: ( +

::Item,)>>, + [], + ) + - rebased_substs: [ + P, + (&::Item,), + (&::Item,), + ] + - norm_rebased_substs: Err( + Type( + (&

::Item,), + ), + ) + - norm_substs: Err( + Type( + (&

::Item,), + ), + ) + - early_binder_substs: Ok( + <(&::Item,) as std::ops::FnOnce<(&

::Item,)>>, + ) + - early_binder_rebased_substs: Ok( + <(&::Item,) as std::ops::FnOnce<(&

::Item,)>>, + ) + --> /nix/store/bbq0z3kg0b7hb3n7agk20r7hg3alf4kb-rust-default-1.72.0-nightly-2023-06-28/lib/rustlib/src/rust/library/core/src/iter/adapters/filter.rs:51:1 + | +51 | impl Iterator for Filter + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + = 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)! + +disabled backtrace +disabled backtrace +disabled backtrace +warning: `traits` (lib) generated 2 warnings Finished dev [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] [stdout.files] +"Traits.For_clauses.Issue_495_.Minimized_3_.fst" = ''' +module Traits.For_clauses.Issue_495_.Minimized_3_ +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl + (#v_P: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8) + : t_Trait v_P = { __marker_trait = () } +''' +"Traits.For_clauses.Issue_495_.fst" = ''' +module Traits.For_clauses.Issue_495_ +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_filter ({ + Core.Ops.Range.f_start = 0uy; + Core.Ops.Range.f_end = 5uy + } + <: + Core.Ops.Range.t_Range u8) + (fun temp_0_ -> + let _:u8 = temp_0_ in + true) + <: + Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + +let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + : Prims.unit = + let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global + = + Core.Iter.Traits.Iterator.f_collect it + in + () + +let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit = + let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global + = + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_filter ({ + Core.Ops.Range.f_start = 0uy; + Core.Ops.Range.f_end = 5uy + } + <: + Core.Ops.Range.t_Range u8) + (fun i -> + let i:u8 = i in + let _, out:(Core.Slice.Iter.t_Iter u8 & bool) = + Core.Iter.Traits.Iterator.f_any (Core.Slice.impl__iter (Core.Ops.Deref.f_deref list + <: + t_Slice u8) + <: + Core.Slice.Iter.t_Iter u8) + (fun n -> + let n:u8 = n in + n =. i <: bool) + in + out) + <: + Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + in + () +''' "Traits.For_clauses.fst" = ''' module Traits.For_clauses #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 48d64cb65..cefd74043 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -86,4 +86,25 @@ mod for_clauses { fn _f Foo<&'a u8>>(x: X) { x.to_t(); } + + // From issue #495 + mod issue_495 { + use core::iter::Filter; + use core::ops::Range; + + fn original_function_from_495(list: Vec) { + let _indices: Vec<_> = (0..5).filter(|i| list.iter().any(|n| n == i)).collect(); + } + + fn minimized_1(list: Vec) -> Vec { + (0..5).filter(|_| true).collect() + } + fn minimized_2(it: Filter, for<'a> fn(&'a u8) -> bool>) { + let _indices: Vec<_> = it.collect(); + } + mod minimized_3 { + pub trait Trait {} + impl bool> Trait for P {} + } + } }