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,37 @@
+// 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
+#![feature(core_intrinsics)]
+use std::intrinsics::type_id;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    // Scalar types
+    let _ = type_id::<i8>();
+    let _ = type_id::<i16>();
+    let _ = type_id::<i32>();
+    let _ = type_id::<i64>();
+    let _ = type_id::<i128>();
+    let _ = type_id::<isize>();
+    let _ = type_id::<u8>();
+    let _ = type_id::<u16>();
+    let _ = type_id::<u32>();
+    let _ = type_id::<u64>();
+    let _ = type_id::<u128>();
+    let _ = type_id::<usize>();
+    let _ = type_id::<f32>();
+    let _ = type_id::<f64>();
+    let _ = type_id::<bool>();
+    let _ = type_id::<char>();
+    // Compound types (tuple and array)
+    let _ = type_id::<(i32, i32)>();
+    let _ = type_id::<[i32; 5]>();
+    // Custom data types (struct and enum)
+    let _ = type_id::<MyStruct>();
+    let _ = type_id::<MyEnum>();
+}

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");
+}