Merge pull request #709 from hacspec/fix-707

fix(exporter): disable impl expr resolution under type aliases
hacspec · Jun 25, 2024 · 18e21e2 · 18e21e2
2 parents 1fc4a03 + b80c24b
commit 18e21e2
Show file tree

Hide file tree

Showing 6 changed files with 57 additions and 2 deletions.
diff --git 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<DebugEngineMode>,
 
+    /// 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
@@ -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));

diff --git 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
@@ -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<GenericArg> = 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<Body: IsBody> {
         items: Vec<ForeignItem<Body>>,
     },
     GlobalAsm(InlineAsm),
-    TyAlias(Ty, Generics<Body>),
+    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<Body>,
+    ),
     OpaqueTy(OpaqueTy<Body>),
     Enum(
         EnumDef<Body>,

diff --git 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"

diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
@@ -176,3 +176,9 @@ mod interlaced_consts_types {
         fn fun<const FunConst: usize, FunType>(x: [FooType; FooConst], y: [FunType; FunConst]) {}
     }
 }
+
+mod type_alias_bounds_issue_707 {
+    struct StructWithGenericBounds<T: Clone>(T);
+    type SynonymA<T> = StructWithGenericBounds<T>;
+    type SynonymB<T> = StructWithGenericBounds<(T, T)>;
+}