Get Kani to run on Apple M1 (#1323)

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -229,11 +229,14 @@ fn check_target(session: &Session) {
     let is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu";
     // Comparison with `x86_64-apple-darwin` does not work well because the LLVM
     // target may become `x86_64-apple-macosx10.7.0` (or similar) and fail
-    let is_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-");
+    let is_x86_64_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-");
+    // looking for `arm64-apple-*`
+    let is_arm64_darwin_target = session.target.llvm_target.starts_with("arm64-apple-");
 
-    if !is_linux_target && !is_darwin_target {
+    if !is_linux_target && !is_x86_64_darwin_target && !is_arm64_darwin_target {
         let err_msg = format!(
-            "Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin`, but it is {}",
+            "Kani requires the target platform to be `x86_64-unknown-linux-gnu` or \
+            `x86_64-apple-*` or `arm64-apple-*`, but it is {}",
             &session.target.llvm_target
         );
         session.err(&err_msg);

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -350,10 +350,10 @@ impl MetadataLoader for GotocMetadataLoader {
 
 /// Builds a machine model which is required by CBMC
 fn machine_model_from_session(sess: &Session) -> MachineModel {
-    // The model assumes a `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin`
-    // platform. We check the target platform in function `check_target` from
-    // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs and
-    // error if it is not any of the ones we expect.
+    // The model assumes a `x86_64-unknown-linux-gnu`, `x86_64-apple-darwin`
+    // or `aarch64-apple-darwin` platform. We check the target platform in function
+    // `check_target` from src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+    // and error if it is not any of the ones we expect.
     let architecture = &sess.target.arch;
     let pointer_width = sess.target.pointer_width.into();
 
@@ -372,45 +372,90 @@ fn machine_model_from_session(sess: &Session) -> MachineModel {
 
     // The values below cannot be obtained from the session so they are
     // hardcoded using standard ones for the supported platforms
-    let bool_width = 8;
-    let char_is_unsigned = false;
-    let char_width = 8;
-    let double_width = 64;
-    let float_width = 32;
-    let int_width = 32;
-    let long_double_width = 128;
-    let long_int_width = 64;
-    let long_long_int_width = 64;
-    let memory_operand_size = 4;
-    let null_is_zero = true;
-    let short_int_width = 16;
-    let single_width = 32;
-    let wchar_t_is_unsigned = false;
-    let wchar_t_width = 32;
-    let word_size = 32;
-    let rounding_mode = RoundingMode::ToNearest;
-
-    MachineModel {
-        architecture: architecture.to_string(),
-        alignment,
-        bool_width,
-        char_is_unsigned,
-        char_width,
-        double_width,
-        float_width,
-        int_width,
-        is_big_endian,
-        long_double_width,
-        long_int_width,
-        long_long_int_width,
-        memory_operand_size,
-        null_is_zero,
-        pointer_width,
-        rounding_mode,
-        short_int_width,
-        single_width,
-        wchar_t_is_unsigned,
-        wchar_t_width,
-        word_size,
+    // see /tools/sizeofs/main.cpp.
+    // For reference, the definition in CBMC:
+    //https://github.com/diffblue/cbmc/blob/develop/src/util/config.cpp
+    match architecture.as_ref() {
+        "x86_64" => {
+            let bool_width = 8;
+            let char_is_unsigned = false;
+            let char_width = 8;
+            let double_width = 64;
+            let float_width = 32;
+            let int_width = 32;
+            let long_double_width = 128;
+            let long_int_width = 64;
+            let long_long_int_width = 64;
+            let short_int_width = 16;
+            let single_width = 32;
+            let wchar_t_is_unsigned = false;
+            let wchar_t_width = 32;
+
+            MachineModel {
+                architecture: architecture.to_string(),
+                alignment,
+                bool_width,
+                char_is_unsigned,
+                char_width,
+                double_width,
+                float_width,
+                int_width,
+                is_big_endian,
+                long_double_width,
+                long_int_width,
+                long_long_int_width,
+                memory_operand_size: int_width / 8,
+                null_is_zero: true,
+                pointer_width,
+                rounding_mode: RoundingMode::ToNearest,
+                short_int_width,
+                single_width,
+                wchar_t_is_unsigned,
+                wchar_t_width,
+                word_size: int_width,
+            }
+        }
+        "aarch64" => {
+            let bool_width = 8;
+            let char_is_unsigned = true;
+            let char_width = 8;
+            let double_width = 64;
+            let float_width = 32;
+            let int_width = 32;
+            let long_double_width = 64;
+            let long_int_width = 64;
+            let long_long_int_width = 64;
+            let short_int_width = 16;
+            let single_width = 32;
+            let wchar_t_is_unsigned = false;
+            let wchar_t_width = 32;
+
+            MachineModel {
+                architecture: architecture.to_string(),
+                alignment,
+                bool_width,
+                char_is_unsigned,
+                char_width,
+                double_width,
+                float_width,
+                int_width,
+                is_big_endian,
+                long_double_width,
+                long_int_width,
+                long_long_int_width,
+                memory_operand_size: int_width / 8,
+                null_is_zero: true,
+                pointer_width,
+                rounding_mode: RoundingMode::ToNearest,
+                short_int_width,
+                single_width,
+                wchar_t_is_unsigned,
+                wchar_t_width,
+                word_size: int_width,
+            }
+        }
+        _ => {
+            panic!("Unsupported architecture: {}", architecture);
+        }
     }
 }

tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs

@@ -23,6 +23,7 @@ enum MyEnum {
 
 #[kani::proof]
 fn main() {
+    #[cfg(target_arch = "x86_64")]
     unsafe {
         // Scalar types
         assert!(min_align_of_val(&0i8) == 1);
@@ -49,4 +50,31 @@ fn main() {
         assert!(min_align_of_val(&MyEnum::Variant) == 1);
         assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4);
     }
+    #[cfg(target_arch = "aarch64")]
+    unsafe {
+        // Scalar types
+        assert!(min_align_of_val(&0i8) == 1);
+        assert!(min_align_of_val(&0i16) == 2);
+        assert!(min_align_of_val(&0i32) == 4);
+        assert!(min_align_of_val(&0i64) == 8);
+        assert!(min_align_of_val(&0i128) == 16);
+        assert!(min_align_of_val(&0isize) == 8);
+        assert!(min_align_of_val(&0u8) == 1);
+        assert!(min_align_of_val(&0u16) == 2);
+        assert!(min_align_of_val(&0u32) == 4);
+        assert!(min_align_of_val(&0u64) == 8);
+        assert!(min_align_of_val(&0u128) == 16);
+        assert!(min_align_of_val(&0usize) == 8);
+        assert!(min_align_of_val(&0f32) == 4);
+        assert!(min_align_of_val(&0f64) == 8);
+        assert!(min_align_of_val(&false) == 1);
+        assert!(min_align_of_val(&(0 as char)) == 4);
+        // Compound types (tuple and array)
+        assert!(min_align_of_val(&(0i32, 0i32)) == 4);
+        assert!(min_align_of_val(&[0i32; 5]) == 4);
+        // Custom data types (struct and enum)
+        assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4);
+        assert!(min_align_of_val(&MyEnum::Variant) == 1);
+        assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4);
+    }
 }

tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs

@@ -18,7 +18,10 @@ impl T for A {}
 fn check_align_simple() {
     let a = A { id: 0 };
     let t: &dyn T = &a;
+    #[cfg(target_arch = "x86_64")]
     assert_eq!(align_of_val(t), 8);
+    #[cfg(target_arch = "aarch64")]
+    assert_eq!(align_of_val(t), 16);
     assert_eq!(align_of_val(&t), 8);
 }
 

tests/kani/Intrinsics/ConstEval/min_align_of.rs

@@ -12,27 +12,57 @@ 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);
+    #[cfg(target_arch = "x86_64")]
+    {
+        // 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);
+    }
+
+    #[cfg(target_arch = "aarch64")]
+    {
+        // 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>() == 16);
+        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>() == 16);
+        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/ConstEval/pref_align_of.rs

@@ -12,27 +12,56 @@ 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);
+    #[cfg(target_arch = "x86_64")]
+    {
+        // 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);
+    }
+    #[cfg(target_arch = "aarch64")]
+    {
+        // 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>() } == 16);
+        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>() } == 16);
+        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);
+    }
 }