From fb183c6c0d46ad0cd1f42607a6d796242ed66426 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 10 Jun 2024 11:26:27 +0200 Subject: [PATCH 1/3] fix(exporter): disable impl expr resolution under type aliases This commits disables trait resolution in the context of a type alias definition. Rust doesn't enforce bounds on generic parameters in type aliases, so it is legal to write: ```rust struct Foo(T); type Synonym = Foo; ``` Thus, if we compute the impl expression for the bound `T: Clone` that appears on the type expression `Foo`, Rustc's trait selection fails: in the context of `Synonym`, `T` indeed doesn't implement `Clone`, _a priori_. This is raising an issue about backends: translating such type synonym with "missing" bounds will fail. See https://github.com/hacspec/hax/issues/708. Fixes #707 --- frontend/exporter/src/state.rs | 7 +++++++ frontend/exporter/src/types/copied.rs | 20 ++++++++++++++++++-- tests/traits/src/lib.rs | 6 ++++++ 3 files changed, 31 insertions(+), 2 deletions(-) diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 2b70d4df9..094408315 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -131,6 +131,12 @@ mod types { >, >, pub tcx: rustc_middle::ty::TyCtxt<'tcx>, + /// Rust doesn't enforce bounds on generic parameters in type + /// aliases. Thus, when translating type aliases, we need to + /// disable the resolution of implementation expressions. For + /// more details, please see + /// https://github.com/hacspec/hax/issues/707. + pub ty_alias_mode: bool, } impl<'tcx> Base<'tcx> { @@ -149,6 +155,7 @@ mod types { local_ctx: Rc::new(RefCell::new(LocalContextS::new())), exported_spans: Rc::new(RefCell::new(HashSet::new())), exported_def_ids: Rc::new(RefCell::new(HashSet::new())), + ty_alias_mode: false, } } } diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 6904dae02..af24471e1 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1651,7 +1651,11 @@ pub enum Ty { rustc_middle::ty::TyKind::Adt(adt_def, generics) => { let def_id = adt_def.did().sinto(state); let generic_args: Vec = generics.sinto(state); - let trait_refs = solve_item_traits(state, state.param_env(), adt_def.did(), generics, None); + let trait_refs = if state.base().ty_alias_mode { + vec![] + } else { + solve_item_traits(state, state.param_env(), adt_def.did(), generics, None) + }; Ty::Adt { def_id, generic_args, trait_refs } }, )] @@ -3044,7 +3048,19 @@ pub enum ItemKind { items: Vec>, }, GlobalAsm(InlineAsm), - TyAlias(Ty, Generics), + TyAlias( + #[map({ + let s = &State { + thir: s.clone(), + owner_id: s.owner_id(), + base: Base {ty_alias_mode: true, ..s.base()}, + mir: (), + }; + x.sinto(s) + })] + Ty, + Generics, + ), OpaqueTy(OpaqueTy), Enum( EnumDef, diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 1d01124ef..8920f2732 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -176,3 +176,9 @@ mod interlaced_consts_types { fn fun(x: [FooType; FooConst], y: [FunType; FunConst]) {} } } + +mod type_alias_bounds_issue_707 { + struct StructWithGenericBounds(T); + type SynonymA = StructWithGenericBounds; + type SynonymB = StructWithGenericBounds<(T, T)>; +} From 99271bae14f81c1713103e678392f7a06235b970 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 10 Jun 2024 12:04:30 +0200 Subject: [PATCH 2/3] feat: turn type aliases extraction off by default Fixes #708 --- cli/options/src/lib.rs | 10 ++++++++++ engine/bin/lib.ml | 7 +++++++ 2 files changed, 17 insertions(+) diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index c50fdc8c8..02574effb 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -313,6 +313,16 @@ pub struct BackendOptions { #[arg(short, long = "debug-engine")] pub debug_engine: Option, + /// Extract type aliases. This is disabled by default, since + /// extracted terms depends on expanded types rather than on type + /// aliases. Turning this option on is discouraged: Rust type + /// synonyms can ommit generic bounds, which are ususally + /// necessary in the hax backends, leading to typechecking + /// errors. For more details see + /// https://github.com/hacspec/hax/issues/708. + #[arg(long)] + pub extract_type_aliases: bool, + #[command(flatten)] pub translation_options: TranslationOptions, } diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index b97fdd7b3..497ac3488 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -94,6 +94,13 @@ let run (options : Types.engine_options) : Types.output = options.backend.translation_options.include_namespaces in let items = import_thir_items include_clauses options.input in + let items = + if options.backend.extract_type_aliases then items + else + List.filter + ~f:(function { v = TyAlias _; _ } -> false | _ -> true) + items + in Logs.info (fun m -> m "Applying phase for backend %s" ([%show: Diagnostics.Backend.t] M.backend)); From b80c24bfaf753902c02419850d6354ebda958266 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 25 Jun 2024 07:58:37 +0200 Subject: [PATCH 3/3] chore: regenerate test snapshots --- .../src/snapshots/toolchain__traits into-fstar.snap | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 36079953d..32b9dbe21 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -240,6 +240,15 @@ let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0) type t_Bar (v_FooConst: usize) (v_FooType: Type0) = | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType ''' +"Traits.Type_alias_bounds_issue_707_.fst" = ''' +module Traits.Type_alias_bounds_issue_707_ +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} = + | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T +''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' module Traits.Unconstrainted_types_issue_677_ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"