Add support for the ARM64 Linux platform (#2757)

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -387,17 +387,23 @@ fn check_target(session: &Session) {
     // The requirement below is needed to build a valid CBMC machine model
     // in function `machine_model_from_session` from
     // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
-    let is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu";
+    let is_x86_64_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu";
+    let is_arm64_linux_target = session.target.llvm_target == "aarch64-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_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_x86_64_darwin_target && !is_arm64_darwin_target {
+    if !is_x86_64_linux_target
+        && !is_arm64_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-*` or `arm64-apple-*`, but it is {}",
+            "Kani requires the target platform to be `x86_64-unknown-linux-gnu`, \
+            `aarch64-unknown-linux-gnu`, `x86_64-apple-*` or `arm64-apple-*`, but \
+            it is {}",
             &session.target.llvm_target
         );
         session.err(err_msg);
@@ -623,6 +629,7 @@ fn new_machine_model(sess: &Session) -> MachineModel {
     // `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 os = &sess.target.os;
     let pointer_width = sess.target.pointer_width.into();
 
     // The model assumes the following values for session options:
@@ -690,12 +697,18 @@ fn new_machine_model(sess: &Session) -> MachineModel {
             let double_width = 64;
             let float_width = 32;
             let int_width = 32;
-            let long_double_width = 64;
+            let long_double_width = match os.as_ref() {
+                "linux" => 128,
+                _ => 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;
+            // https://developer.arm.com/documentation/dui0491/i/Compiler-Command-line-Options/--signed-chars----unsigned-chars
+            // https://www.arm.linux.org.uk/docs/faqs/signedchar.php
+            // https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms
+            let wchar_t_is_unsigned = matches!(os.as_ref(), "linux");
             let wchar_t_width = 32;
 
             MachineModel {

kani-driver/src/concrete_playback/test_generator.rs

@@ -380,10 +380,22 @@ mod concrete_vals_extractor {
                         next_num.push(next_byte);
                     }
 
-                    return Some(ConcreteVal {
-                        byte_arr: next_num,
-                        interp_val: interp_concrete_val.to_string(),
-                    });
+                    // In ARM64 Linux, CBMC will produce a character instead of a number for
+                    // interpreted values because the char type is unsigned in that platform.
+                    // For example, for the value `101` it will produce `'e'` instead of `101`.
+                    // To correct this, we check if the value starts and ends with `'`, and
+                    // convert the character into its ASCII value in that case.
+                    let interp_val = {
+                        let interp_val_str = interp_concrete_val.to_string();
+                        if interp_val_str.starts_with('\'') && interp_val_str.ends_with('\'') {
+                            let interp_num = interp_val_str.chars().nth(1).unwrap() as u8;
+                            interp_num.to_string()
+                        } else {
+                            interp_val_str
+                        }
+                    };
+
+                    return Some(ConcreteVal { byte_arr: next_num, interp_val });
                 }
             }
         }

tests/kani/Intrinsics/ConstEval/pref_align_of.rs

@@ -41,27 +41,45 @@ fn main() {
     #[cfg(target_arch = "aarch64")]
     {
         // Scalar types
+        #[cfg(target_os = "linux")]
+        assert!(unsafe { pref_align_of::<i8>() } == 4);
+        #[cfg(target_os = "macos")]
         assert!(unsafe { pref_align_of::<i8>() } == 1);
-        assert!(unsafe { pref_align_of::<i16>() } == 2);
+        #[cfg(target_os = "linux")]
+        assert!(unsafe { pref_align_of::<i16>() } == 4);
+        #[cfg(target_os = "macos")]
+        assert!(unsafe { pref_align_of::<i16>() } == 1);
         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);
+        #[cfg(target_os = "linux")]
+        assert!(unsafe { pref_align_of::<u8>() } == 4);
+        #[cfg(target_os = "macos")]
         assert!(unsafe { pref_align_of::<u8>() } == 1);
+        #[cfg(target_os = "linux")]
+        assert!(unsafe { pref_align_of::<u16>() } == 4);
+        #[cfg(target_os = "macos")]
         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);
+        #[cfg(target_os = "linux")]
+        assert!(unsafe { pref_align_of::<bool>() } == 4);
+        #[cfg(target_os = "macos")]
         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);
+        #[cfg(target_os = "linux")]
+        assert!(unsafe { pref_align_of::<MyEnum>() } == 4);
+        #[cfg(target_os = "macos")]
         assert!(unsafe { pref_align_of::<MyEnum>() } == 1);
     }
 }

tests/kani/Stubbing/foreign_functions.rs

@@ -46,16 +46,16 @@ fn function_pointer_call(function_pointer: unsafe extern "C" fn(c_int) -> c_long
 #[kani::proof]
 #[kani::stub(libc::strlen, stubs::strlen)]
 fn standard() {
-    let str: Box<i8> = Box::new(4);
-    let str_ptr: *const i8 = &*str;
+    let str: Box<c_char> = Box::new(4);
+    let str_ptr: *const c_char = &*str;
     assert_eq!(unsafe { libc::strlen(str_ptr) }, 4);
 }
 
 #[kani::proof]
 #[kani::stub(libc::strlen, stubs::strlen)]
 fn function_pointer_standard() {
-    let str: Box<i8> = Box::new(4);
-    let str_ptr: *const i8 = &*str;
+    let str: Box<c_char> = Box::new(4);
+    let str_ptr: *const c_char = &*str;
     let new_ptr = libc::strlen;
     assert_eq!(unsafe { new_ptr(str_ptr) }, 4);
 }

tests/ui/concrete-playback/i8/expected

@@ -11,7 +11,7 @@ fn kani_concrete_playback_harness
         vec![155],
         // 0
         vec![0],
-        // 'e'
+        // 101
         vec![101],
         // 127
         vec![127]