diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index ff9fef100..eb14359db 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -127,12 +127,13 @@ pub(crate) mod search_clause { s: &S, ) -> bool { let tcx = s.base().tcx; - let x = tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x); - let y = tcx.try_normalize_erasing_regions(param_env, y).unwrap_or(y); - // Below: "~const " may appear in the string, and comes from the way the - // trait ref is internalized by rustc. We remove such occurrences (yes, this is sad). - let sx = format!("{:?}", x).replace("~const ", ""); - let sy = format!("{:?}", y).replace("~const ", ""); + let erase_and_norm = + |x| tcx.erase_regions(tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x)); + // Lifetime and constantness are irrelevant when resolving instances + let x = erase_and_norm(x).without_const(tcx); + let y = erase_and_norm(y).without_const(tcx); + let sx = format!("{:?}", x.kind().skip_binder()); + let sy = format!("{:?}", y.kind().skip_binder()); let result = sx == sy; const DEBUG: bool = false; if DEBUG && result { @@ -298,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 b3f7449b3..c54b93f95 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -15,20 +15,103 @@ info: issue_id: ~ positive: true snapshot: - stderr: true + stderr: false stdout: true include_flag: ~ backend_options: ~ --- exit = 0 -stderr = ''' -Compiling traits v0.1.0 (WORKSPACE_ROOT/traits) - 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" +open Core +open FStar.Mul + +class t_Foo (v_Self: Type0) (v_T: Type0) = { + f_to_t_pre:v_Self -> bool; + f_to_t_post:v_Self -> v_T -> bool; + f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result) +} + +let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X) + : Prims.unit = + let _:u8 = f_to_t x in + () +''' "Traits.fst" = ''' module Traits #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/traits/Cargo.toml b/tests/traits/Cargo.toml index 147a72f70..77a50c080 100644 --- a/tests/traits/Cargo.toml +++ b/tests/traits/Cargo.toml @@ -6,5 +6,5 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar" = { } +into."fstar" = { snapshot = "stdout" } diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index bf6e56704..cefd74043 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -77,3 +77,34 @@ impl Error { || Self::Fail } } + +mod for_clauses { + trait Foo { + fn to_t(&self) -> T; + } + + 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 {} + } + } +}