Fix type mixmatch of types with projection (rust-lang#1125)

* Add tests to associated types

* Fix type mistmatch of types with projection

Structures with members that had type projections in their declaration
were being handled incorrectly. We were only normalizing the types when
the projection was visited, which could impact on how we identify
whether this structure already existed or not.

This change normalizes all types before starting to codegen the
entire type.

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: celinval

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -533,10 +533,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// also c.f. https://www.ralfj.de/blog/2020/04/04/layout-debugging.html
     ///      c.f. https://rust-lang.github.io/unsafe-code-guidelines/introduction.html
     pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type {
-        let goto_typ = self.codegen_ty_inner(ty);
+        let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty);
+        let goto_typ = self.codegen_ty_inner(normalized);
         if let Some(tag) = goto_typ.tag() {
             if !self.type_map.contains_key(&tag) {
-                self.type_map.insert(tag, ty);
+                debug!(mir_type=?normalized, gotoc_name=?tag, ?goto_typ,  "codegen_ty: new type");
+                self.type_map.insert(tag, normalized);
             }
         }
         goto_typ
@@ -624,9 +626,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
             ty::Projection(_) | ty::Opaque(_, _) => {
-                // hidden types that can be revealed by the compiler via normalization
-                let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty);
-                self.codegen_ty(normalized)
+                unreachable!("Type should've been normalized already")
             }
 
             // shouldn't come to here after mormomorphization

tests/kani/AssociatedTypes/associated_types.rs

@@ -0,0 +1,61 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Tests the behavior of associated types.
+//! See https://doc.rust-lang.org/book/ch19-03-advanced-traits.html for more details.
+
+/// Covert Source -> Target
+trait Convert {
+    type Source;
+    type Target;
+
+    fn convert(&self) -> Self::Target;
+}
+
+/// Dummy trait that returns an u8
+trait U8Wrapper {
+    fn get(&self) -> u8;
+}
+
+impl<T: U8Wrapper> Convert for T {
+    type Source = T;
+    type Target = u8;
+
+    fn convert(&self) -> u8 {
+        self.get()
+    }
+}
+
+#[derive(Copy, Clone, PartialEq, Eq)]
+struct MyU8 {
+    inner: u8,
+}
+
+impl U8Wrapper for MyU8 {
+    fn get(&self) -> u8 {
+        self.inner
+    }
+}
+
+#[kani::proof]
+pub fn check_source_type() {
+    let obj1 = Some(MyU8 { inner: 10 });
+    let obj2: Option<<MyU8 as Convert>::Source> = obj1;
+    assert_eq!(obj1.unwrap(), obj2.unwrap());
+}
+
+#[kani::proof]
+pub fn check_fn_convert() {
+    let val: u8 = kani::any();
+    let obj1 = Some(MyU8 { inner: val });
+    assert_eq!(obj1.unwrap().get(), val);
+    assert_eq!(obj1.unwrap().convert(), val);
+}
+
+#[kani::proof]
+pub fn check_dyn_convert() {
+    let val: u8 = kani::any();
+    let obj1 = MyU8 { inner: val };
+    let con: &dyn Convert<Source = MyU8, Target = u8> = &obj1;
+    assert_eq!(con.convert(), val);
+}

tests/kani/AssociatedTypes/into_iter.rs

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Tests the handling of IntoIter associated types for Iterators.
+//! For Iterators, the IntoIter associated type is the type of the iterator itself.
+//! In this case, Kani should treat the types as the same type.
+
+use std::str::Chars;
+
+struct MyStruct<'a> {
+    copy1: Option<<Chars<'a> as IntoIterator>::IntoIter>,
+    copy2: Option<Chars<'a>>,
+}
+
+impl<'a> MyStruct<'a> {
+    fn new(source: Chars<'a>) -> Self {
+        MyStruct { copy1: Some(source.clone()), copy2: Some(source) }
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(2)]
+pub fn check_into_iter_type() {
+    let original = "h";
+    let mut wrapper = MyStruct::new(original.chars());
+    assert!(wrapper.copy1.unwrap().eq(wrapper.copy2.unwrap()));
+}

tests/kani/AssociatedTypes/type_of.rs

@@ -0,0 +1,32 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Tests the behavior of TypeId for structs with associated types in their member declaration.
+//!
+//! See https://github.com/model-checking/kani/issues/1124 for more details.
+use std::any::TypeId;
+
+trait Associated {
+    type Typ;
+}
+
+impl<T> Associated for T {
+    type Typ = T;
+}
+
+struct Wrapper<T>(T);
+
+struct MyStruct {
+    first: Wrapper<u8>,
+    second: Wrapper<<u8 as Associated>::Typ>,
+}
+
+fn same_type<T: 'static, U: 'static>(_: T, _: U) -> bool {
+    TypeId::of::<T>() == TypeId::of::<U>()
+}
+
+#[kani::proof]
+fn check_type() {
+    let mine = MyStruct { first: Wrapper(10), second: Wrapper(10) };
+    assert!(same_type(mine.first, mine.second));
+}

tests/kani/Iterator/flat_map.rs

@@ -0,0 +1,23 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// This test checks the result of using Iterator::flat_map. We had some projection
+// issues with this in the past.
+
+#[kani::proof]
+#[kani::unwind(3)]
+pub fn check_flat_map_char() {
+    let hi = ["H", "i"];
+    let mut hi_flat = hi.iter().flat_map(|s| s.chars());
+    assert_eq!(hi_flat.next(), Some('H'));
+    assert_eq!(hi_flat.next(), Some('i'));
+    assert_eq!(hi_flat.next(), None);
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn check_flat_map_len() {
+    let hello = ["Hi", "!"];
+    let length = hello.iter().flat_map(|s| s.chars()).count();
+    assert_eq!(length, 3);
+}