Add tests for constant-evaluated intrinsics

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

@@ -244,6 +244,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
+        // Intrinsics which encode a value known during compilation (e.g., `size_of`)
         macro_rules! codegen_intrinsic_const {
             () => {{
                 let value = self

tests/kani/Intrinsics/ConstEval/min_align_of.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we get the expected results for the `min_align_of` intrinsic
+// with common data types
+#![feature(core_intrinsics)]
+use std::intrinsics::min_align_of;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    // Scalar types
+    assert!(min_align_of::<i8>() == 1);
+    assert!(min_align_of::<i16>() == 2);
+    assert!(min_align_of::<i32>() == 4);
+    assert!(min_align_of::<i64>() == 8);
+    assert!(min_align_of::<i128>() == 8);
+    assert!(min_align_of::<isize>() == 8);
+    assert!(min_align_of::<u8>() == 1);
+    assert!(min_align_of::<u16>() == 2);
+    assert!(min_align_of::<u32>() == 4);
+    assert!(min_align_of::<u64>() == 8);
+    assert!(min_align_of::<u128>() == 8);
+    assert!(min_align_of::<usize>() == 8);
+    assert!(min_align_of::<f32>() == 4);
+    assert!(min_align_of::<f64>() == 8);
+    assert!(min_align_of::<bool>() == 1);
+    assert!(min_align_of::<char>() == 4);
+    // Compound types (tuple and array)
+    assert!(min_align_of::<(i32, i32)>() == 4);
+    assert!(min_align_of::<[i32; 5]>() == 4);
+    // Custom data types (struct and enum)
+    assert!(min_align_of::<MyStruct>() == 1);
+    assert!(min_align_of::<MyEnum>() == 1);
+}

tests/kani/Intrinsics/needs_drop.rs → tests/kani/Intrinsics/ConstEval/needs_drop.rs

@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that we get the expected results for needs_drop intrinsic
+// Check that we get the expected results for the `needs_drop` intrinsic
 
 use std::mem;
 

tests/kani/Intrinsics/ConstEval/pref_align_of.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we get the expected results for the `pref_align_of` intrinsic
+// with common data types
+#![feature(core_intrinsics)]
+use std::intrinsics::pref_align_of;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    // Scalar types
+    assert!(unsafe { pref_align_of::<i8>() } == 1);
+    assert!(unsafe { pref_align_of::<i16>() } == 2);
+    assert!(unsafe { pref_align_of::<i32>() } == 4);
+    assert!(unsafe { pref_align_of::<i64>() } == 8);
+    assert!(unsafe { pref_align_of::<i128>() } == 8);
+    assert!(unsafe { pref_align_of::<isize>() } == 8);
+    assert!(unsafe { pref_align_of::<u8>() } == 1);
+    assert!(unsafe { pref_align_of::<u16>() } == 2);
+    assert!(unsafe { pref_align_of::<u32>() } == 4);
+    assert!(unsafe { pref_align_of::<u64>() } == 8);
+    assert!(unsafe { pref_align_of::<u128>() } == 8);
+    assert!(unsafe { pref_align_of::<usize>() } == 8);
+    assert!(unsafe { pref_align_of::<f32>() } == 4);
+    assert!(unsafe { pref_align_of::<f64>() } == 8);
+    assert!(unsafe { pref_align_of::<bool>() } == 1);
+    assert!(unsafe { pref_align_of::<char>() } == 4);
+    // Compound types (tuple and array)
+    assert!(unsafe { pref_align_of::<(i32, i32)>() } == 8);
+    assert!(unsafe { pref_align_of::<[i32; 5]>() } == 4);
+    // Custom data types (struct and enum)
+    assert!(unsafe { pref_align_of::<MyStruct>() } == 8);
+    assert!(unsafe { pref_align_of::<MyEnum>() } == 1);
+}

tests/kani/Intrinsics/ConstEval/size_of.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we get the expected results for the `size_of` intrinsic
+// with common data types
+#![feature(core_intrinsics)]
+use std::intrinsics::size_of;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    // Scalar types
+    assert!(size_of::<i8>() == 1);
+    assert!(size_of::<i16>() == 2);
+    assert!(size_of::<i32>() == 4);
+    assert!(size_of::<i64>() == 8);
+    assert!(size_of::<i128>() == 16);
+    assert!(size_of::<isize>() == 8);
+    assert!(size_of::<u8>() == 1);
+    assert!(size_of::<u16>() == 2);
+    assert!(size_of::<u32>() == 4);
+    assert!(size_of::<u64>() == 8);
+    assert!(size_of::<u128>() == 16);
+    assert!(size_of::<usize>() == 8);
+    assert!(size_of::<f32>() == 4);
+    assert!(size_of::<f64>() == 8);
+    assert!(size_of::<bool>() == 1);
+    assert!(size_of::<char>() == 4);
+    // Compound types (tuple and array)
+    assert!(size_of::<(i32, i32)>() == 8);
+    assert!(size_of::<[i32; 5]>() == 20);
+    // Custom data types (struct and enum)
+    assert!(size_of::<MyStruct>() == 0);
+    assert!(size_of::<MyEnum>() == 0);
+}

tests/kani/Intrinsics/ConstEval/type_id.rs

@@ -0,0 +1,49 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that the `type_id` intrinsic is supported with common data types
+// and that there are no duplicate type IDs
+#![feature(core_intrinsics)]
+use std::intrinsics::type_id;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    let type_ids = [
+        // Scalar types
+        type_id::<i8>(),
+        type_id::<i16>(),
+        type_id::<i32>(),
+        type_id::<i64>(),
+        type_id::<i128>(),
+        type_id::<isize>(),
+        type_id::<u8>(),
+        type_id::<u16>(),
+        type_id::<u32>(),
+        type_id::<u64>(),
+        type_id::<u128>(),
+        type_id::<usize>(),
+        type_id::<f32>(),
+        type_id::<f64>(),
+        type_id::<bool>(),
+        type_id::<char>(),
+        // Compound types (tuple and array)
+        type_id::<(i32, i32)>(),
+        type_id::<[i32; 5]>(),
+        // Custom data types (struct and enum)
+        type_id::<MyStruct>(),
+        type_id::<MyEnum>(),
+    ];
+
+    // Check that there are no duplicate type IDs
+    let i: usize = kani::any();
+    let j: usize = kani::any();
+    kani::assume(i < type_ids.len());
+    kani::assume(j < type_ids.len());
+    if i != j {
+        assert_ne!(type_ids[i], type_ids[j]);
+    }
+}

tests/kani/Intrinsics/ConstEval/type_name.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we get the expected results for the `type_name` intrinsic
+// with common data types
+#![feature(core_intrinsics)]
+use std::intrinsics::type_name;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    // Scalar types
+    assert!(type_name::<i8>() == "i8");
+    assert!(type_name::<i16>() == "i16");
+    assert!(type_name::<i32>() == "i32");
+    assert!(type_name::<i64>() == "i64");
+    assert!(type_name::<i128>() == "i128");
+    assert!(type_name::<isize>() == "isize");
+    assert!(type_name::<u8>() == "u8");
+    assert!(type_name::<u16>() == "u16");
+    assert!(type_name::<u32>() == "u32");
+    assert!(type_name::<u64>() == "u64");
+    assert!(type_name::<u128>() == "u128");
+    assert!(type_name::<usize>() == "usize");
+    assert!(type_name::<f32>() == "f32");
+    assert!(type_name::<f64>() == "f64");
+    assert!(type_name::<bool>() == "bool");
+    assert!(type_name::<char>() == "char");
+    // Compound types (tuple and array)
+    assert!(type_name::<(i32, i32)>() == "(i32, i32)");
+    assert!(type_name::<[i32; 5]>() == "[i32; 5]");
+    // Custom data types (struct and enum)
+    assert!(type_name::<MyStruct>() == "type_name::MyStruct");
+    assert!(type_name::<MyEnum>() == "type_name::MyEnum");
+}