From f44d4ae12379c3c3fde06f374102162eb3b0c773 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 22 Mar 2022 14:06:53 -0700
Subject: [PATCH] Add fixme tests that reproduce issues #555, #556, and #560
 (#952)

Add tests for a few open issues.
---
 .../cast_abstract_args_to_concrete_fixme.rs   | 24 ++++++++++
 tests/kani/Iterator/into_iter_fixme.rs        | 14 ++++++
 tests/kani/PhantomData/phantom_fixme.rs       | 45 +++++++++++++++++++
 3 files changed, 83 insertions(+)
 create mode 100644 tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs
 create mode 100644 tests/kani/Iterator/into_iter_fixme.rs
 create mode 100644 tests/kani/PhantomData/phantom_fixme.rs

diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs
new file mode 100644
index 000000000000..d648391eb36b
--- /dev/null
+++ b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs
@@ -0,0 +1,24 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is a modified version of cast_abstract_args_to_concrete_fixme.rs.
+//! The original test requires --no-undefined-function-checks to pass. This is an issue that
+//! require investigation. See https://github.com/model-checking/kani/issues/555.
+//!
+//! Once this issue is fixed. Please remove this test and remove the kani flag from the original
+//! test: --no-undefined-function-check
+
+fn main() {
+    let _x32 = 1.0f32.powi(2);
+    let _x64 = 1.0f64.powi(2);
+
+    unsafe {
+        let size: libc::size_t = mem::size_of::<i32>();
+        let my_num: *mut libc::c_void = libc::malloc(size);
+        if my_num.is_null() {
+            panic!("failed to allocate memory");
+        }
+        let my_num2 = libc::memset(my_num, 1, size);
+        libc::free(my_num);
+    }
+}
diff --git a/tests/kani/Iterator/into_iter_fixme.rs b/tests/kani/Iterator/into_iter_fixme.rs
new file mode 100644
index 000000000000..d29ca3baea01
--- /dev/null
+++ b/tests/kani/Iterator/into_iter_fixme.rs
@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// compile-flags: --edition 2018
+// kani-flags: --unwind 4
+//
+// This reproduces the issue seen in "Failures when iterating over results".
+// See https://github.com/model-checking/kani/issues/556 for more information.
+#[kani::proof]
+pub fn main() {
+    let numbers = vec![1, 10, -1];
+    let positives: Vec<_> = numbers.into_iter().filter(|&n| n > 0).collect();
+    assert_eq!(positives.len(), 2);
+}
diff --git a/tests/kani/PhantomData/phantom_fixme.rs b/tests/kani/PhantomData/phantom_fixme.rs
new file mode 100644
index 000000000000..2b112244257d
--- /dev/null
+++ b/tests/kani/PhantomData/phantom_fixme.rs
@@ -0,0 +1,45 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// compile-flags: --edition 2018
+// kani-flags: --unwind 4
+//
+// Testcase based on https://doc.rust-lang.org/rust-by-example/generics/phantom/testcase_units.html
+// which reproduces issue https://github.com/model-checking/kani/issues/560
+
+use std::marker::PhantomData;
+use std::ops::Add;
+
+#[derive(Debug, Clone, Copy)]
+enum Mm {}
+
+/// `Length` is a type with phantom type parameter `Unit`,
+/// and is not generic over the length type (that is `u32`).
+///
+/// `u32` already implements the `Clone` and `Copy` traits.
+#[derive(Debug, Clone, Copy)]
+struct Length<Unit>(u32, PhantomData<Unit>);
+
+/// The `Add` trait defines the behavior of the `+` operator.
+impl<Unit> Add for Length<Unit> {
+    type Output = Length<Unit>;
+
+    // add() returns a new `Length` struct containing the sum.
+    fn add(self, rhs: Length<Unit>) -> Length<Unit> {
+        // `+` calls the `Add` implementation for `u32`.
+        Length(self.0 + rhs.0, PhantomData)
+    }
+}
+
+fn main() {
+    // `one_meter` has phantom type parameter `Mm`.
+    let one_meter: Length<Mm> = Length(1000, PhantomData);
+
+    // `+` calls the `add()` method we implemented for `Length<Unit>`.
+    //
+    // Since `Length` implements `Copy`, `add()` does not consume
+    // `one_foot` and `one_meter` but copies them into `self` and `rhs`.
+    let two_meters = one_meter + one_meter;
+
+    assert!(two_meters.0 == 2000);
+}