From 246be4145354131e51a498aa49e7da5e2f5d9ff4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Tue, 12 Sep 2023 19:19:38 -0400 Subject: [PATCH] Add support for the ARM64 Linux platform (#2757) --- .../compiler_interface.rs | 25 ++++++++++++++----- .../src/concrete_playback/test_generator.rs | 20 ++++++++++++--- .../Intrinsics/ConstEval/pref_align_of.rs | 20 ++++++++++++++- tests/kani/Stubbing/foreign_functions.rs | 8 +++--- tests/ui/concrete-playback/i8/expected | 2 +- 5 files changed, 59 insertions(+), 16 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 34e1a085040b..b3262c23c9c8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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 { diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 8bd29ae69d2c..049b294c9848 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/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 }); } } } diff --git a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs index 3a571faace68..238bf37c67f7 100644 --- a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs +++ b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs @@ -41,13 +41,25 @@ fn main() { #[cfg(target_arch = "aarch64")] { // Scalar types + #[cfg(target_os = "linux")] + assert!(unsafe { pref_align_of::() } == 4); + #[cfg(target_os = "macos")] assert!(unsafe { pref_align_of::() } == 1); - assert!(unsafe { pref_align_of::() } == 2); + #[cfg(target_os = "linux")] + assert!(unsafe { pref_align_of::() } == 4); + #[cfg(target_os = "macos")] + assert!(unsafe { pref_align_of::() } == 1); assert!(unsafe { pref_align_of::() } == 4); assert!(unsafe { pref_align_of::() } == 8); assert!(unsafe { pref_align_of::() } == 16); assert!(unsafe { pref_align_of::() } == 8); + #[cfg(target_os = "linux")] + assert!(unsafe { pref_align_of::() } == 4); + #[cfg(target_os = "macos")] assert!(unsafe { pref_align_of::() } == 1); + #[cfg(target_os = "linux")] + assert!(unsafe { pref_align_of::() } == 4); + #[cfg(target_os = "macos")] assert!(unsafe { pref_align_of::() } == 2); assert!(unsafe { pref_align_of::() } == 4); assert!(unsafe { pref_align_of::() } == 8); @@ -55,6 +67,9 @@ fn main() { assert!(unsafe { pref_align_of::() } == 8); assert!(unsafe { pref_align_of::() } == 4); assert!(unsafe { pref_align_of::() } == 8); + #[cfg(target_os = "linux")] + assert!(unsafe { pref_align_of::() } == 4); + #[cfg(target_os = "macos")] assert!(unsafe { pref_align_of::() } == 1); assert!(unsafe { pref_align_of::() } == 4); // Compound types (tuple and array) @@ -62,6 +77,9 @@ fn main() { assert!(unsafe { pref_align_of::<[i32; 5]>() } == 4); // Custom data types (struct and enum) assert!(unsafe { pref_align_of::() } == 8); + #[cfg(target_os = "linux")] + assert!(unsafe { pref_align_of::() } == 4); + #[cfg(target_os = "macos")] assert!(unsafe { pref_align_of::() } == 1); } } diff --git a/tests/kani/Stubbing/foreign_functions.rs b/tests/kani/Stubbing/foreign_functions.rs index 07306b1cdf6b..cdf57ba33863 100644 --- a/tests/kani/Stubbing/foreign_functions.rs +++ b/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 = Box::new(4); - let str_ptr: *const i8 = &*str; + let str: Box = 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 = Box::new(4); - let str_ptr: *const i8 = &*str; + let str: Box = Box::new(4); + let str_ptr: *const c_char = &*str; let new_ptr = libc::strlen; assert_eq!(unsafe { new_ptr(str_ptr) }, 4); } diff --git a/tests/ui/concrete-playback/i8/expected b/tests/ui/concrete-playback/i8/expected index b2d5484e2b1a..e585fd6afe27 100644 --- a/tests/ui/concrete-playback/i8/expected +++ b/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]