kani Buid Kani on arm linux

We've got Kani building on M1, now let's get it building on arm linux.

Out of scope is CI/install, just like M1.

Jul 12 '22 18:07 tedinski

Hello, I was a bit behind thanks to life things. I checked the model on some arm64 boards and M1s in the M1 thread and missed this new one: https://github.com/model-checking/kani/issues/1167#issuecomment-1190515961

Summary is, it looks like the model will need to differentiate between Linux and Apple/Darwin.

I've built cbmc, cbmc-viewer and run kani/kani-regression with ppc64le (only fails due to inline asm being experimental on non-mainline rust targets) so I think I can probably do this for a T1 Rust target (aarch64) as well if nobody is working on it.

Jul 20 '22 17:07 diagprov

Sure! I was hoping to work on it soon, but I've had other priorities. I'd be happy to accept a PR that adds the Arm Linux machine model and gets Kani working on that platform. :)

Jul 20 '22 17:07 tedinski

Ok, I'll have a go. Would definitely be good to get some reviews though, I'm learning about CBMC on the fly.

Jul 20 '22 17:07 diagprov

Just adding a link to github actions issues about arm linux support:

https://github.com/actions/runner-images/issues/5631

Sep 28 '22 17:09 tedinski

I'm testing the current status w.r.t. ARM64 Linux support. The development build (cargo build-dev) fails with:

error: Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-*` or `arm64-apple-*`, but it is aarch64-unknown-linux-gnu                                        


   Compiling compiler_builtins v0.1.100
   Compiling libc v0.2.147
error: Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-*` or `arm64-apple-*`, but it is aarch64-unknown-linux-gnu                                        


error: aborting due to previous error


error: could not compile `rustc-std-workspace-core` (lib) due to 2 previous errors
warning: build failed, waiting for other jobs to finish...
error: aborting due to previous error    ] 29/55: libc, compiler_builtins, core                                                                                                              


error: could not compile `core` (lib) due to 2 previous errors
error: Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-*` or `arm64-apple-*`, but it is aarch64-unknown-linux-gnu

    
error: aborting due to previous error

    Building [=============>             ] 30/55: libc, compiler_builtins                                                                                                                    
error: could not compile `compiler_builtins` (lib) due to 2 previous errors
    Building [==============>            ] 31/55: libc                                                                                                                                       error: Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-*` or `arm64-apple-*`, but it is aarch64-unknown-linux-gnu


error: aborting due to previous error    ] 31/55: libc                                                                                                                                       


error: could not compile `libc` (lib) due to 2 previous errors
Error: Build failed: `cargo build-dev` didn't complete successfully

This limitation comes from Kani's own checks, which I'll try to remove next.

Aug 23 '23 18:08 adpaco-aws

In addition, I haven't been able to build CBMC from source neither:

Checking /home/ubuntu/cbmc/src/ansi-c/library/stdio.c
__libcheck.c: In function ‘__isoc99_vfscanf’:
__libcheck.c:1050:31: error: incompatible type for argument 1 of ‘__CPROVER_OBJECT_SIZE’
 1050 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:72,
                 from <command-line>:
./library/../cprover_builtin_headers.h:59:40: note: expected ‘const void *’ but argument is of type ‘va_list’
   59 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: In function ‘__isoc99_vsscanf’:
__libcheck.c:1213:31: error: incompatible type for argument 1 of ‘__CPROVER_OBJECT_SIZE’
 1213 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:72,
                 from <command-line>:
./library/../cprover_builtin_headers.h:59:40: note: expected ‘const void *’ but argument is of type ‘va_list’
   59 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: At top level:
cc1: note: unrecognized command-line option ‘-Wno-unknown-warning-option’ may have been intended to silence earlier diagnostics
cc1: note: unrecognized command-line option ‘-Wno-gnu-line-marker’ may have been intended to silence earlier diagnostics
rm: cannot remove '__libcheck.s': No such file or directory
make[2]: *** [src/ansi-c/CMakeFiles/ansi-c.dir/build.make:279: src/ansi-c/library-check.stamp] Error 1
make[2]: Leaving directory '/home/ubuntu/cbmc/build'
make[1]: *** [CMakeFiles/Makefile2:2075: src/ansi-c/CMakeFiles/ansi-c.dir/all] Error 2
make[1]: Leaving directory '/home/ubuntu/cbmc/build'
make: *** [Makefile:166: all] Error 2
make: Leaving directory '/home/ubuntu/cbmc/build'

Aug 23 '23 18:08 adpaco-aws

Update:

On CBMC's end: I've opened issue https://github.com/diffblue/cbmc/issues/7862 and submitted a fix for it in https://github.com/diffblue/cbmc/pull/7863. That should allow us to build the next release of CBMC on ARM64 Linux platforms.
On Kani's end: I'm using the patch in this branch to test the current status w.r.t. ARM64 Linux support. There are at least two regression tests failing:

Check compiletest suite=kani mode=kani

running 516 tests
i.......i...i...................ii..i....i......................i......................i 88/516
.............i.......................................................................... 176/516
.......................i.....i......i....i..........i..............i.....i..i........... 264/516
................................................i.........i..........................F.. 352/516
....test [kani] kani/Vectors/any/push_slow.rs has been running for over 60 seconds
....i...........i................................................................... 440/516
....i..............i.......................................i..F.............
failures:

---- [kani] kani/Intrinsics/ConstEval/pref_align_of.rs stdout ----

error: test failed: expected verification success, got failure
status: exit status: 1
command: "kani" "/home/ubuntu/kani/tests/kani/Intrinsics/ConstEval/pref_align_of.rs"
stdout:
------------------------------------------
Kani Rust Verifier 0.34.0 (standalone)
Checking harness main...
CBMC 5.90.0 (cbmc-5.90.0-19-g9a0c662384)
CBMC version 5.90.0 (cbmc-5.90.0-19-g9a0c662384) 64-bit arm64 linux
Reading GOTO program from file /home/ubuntu/kani/tests/kani/Intrinsics/ConstEval/pref_align_of_main.out
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.139649s
size of program expression: 6006 steps
slicing removed 3639 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 0.00234961s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00579712s
Running propositional reduction
Post-processing
Runtime Post-process: 5.2422e-05s
Solving with CaDiCaL sc2021
0 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00024668s
Runtime decision procedure: 0.00670585s

RESULTS:
Check 1: main.assertion.1
        - Status: FAILURE
        - Description: "assertion failed: unsafe { pref_align_of::<i8>() } == 1"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:44:9 in function main

Check 2: main.assertion.2
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<i16>() } == 2"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:45:9 in function main

Check 3: main.assertion.3
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<i32>() } == 4"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:46:9 in function main

Check 4: main.assertion.4
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<i64>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:47:9 in function main

Check 5: main.assertion.5
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<i128>() } == 16"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:48:9 in function main

Check 6: main.assertion.6
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<isize>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:49:9 in function main

Check 7: main.assertion.7
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<u8>() } == 1"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:50:9 in function main

Check 8: main.assertion.8
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<u16>() } == 2"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:51:9 in function main

Check 9: main.assertion.9
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<u32>() } == 4"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:52:9 in function main

Check 10: main.assertion.10
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<u64>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:53:9 in function main

Check 11: main.assertion.11
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<u128>() } == 16"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:54:9 in function main

Check 12: main.assertion.12
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<usize>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:55:9 in function main

Check 13: main.assertion.13
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<f32>() } == 4"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:56:9 in function main

Check 14: main.assertion.14
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<f64>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:57:9 in function main

Check 15: main.assertion.15
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<bool>() } == 1"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:58:9 in function main

Check 16: main.assertion.16
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<char>() } == 4"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:59:9 in function main

Check 17: main.assertion.17
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<(i32, i32)>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:61:9 in function main

Check 18: main.assertion.18
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<[i32; 5]>() } == 4"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:62:9 in function main

Check 19: main.assertion.19
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<MyStruct>() } == 8"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:64:9 in function main

Check 20: main.assertion.20
        - Status: UNREACHABLE
        - Description: "assertion failed: unsafe { pref_align_of::<MyEnum>() } == 1"
        - Location: tests/kani/Intrinsics/ConstEval/pref_align_of.rs:65:9 in function main


SUMMARY:
** 1 of 20 failed (19 unreachable)
Failed Checks: assertion failed: unsafe { pref_align_of::<i8>() } == 1
File: "/home/ubuntu/kani/tests/kani/Intrinsics/ConstEval/pref_align_of.rs", line 44, in main

VERIFICATION:- FAILED
Verification Time: 0.2779707s

Summary:
Verification failed for - main
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

------------------------------------------
stderr:
------------------------------------------

------------------------------------------


---- [kani] kani/Stubbing/foreign_functions.rs stdout ----

error: test failed: expected verification success, got failure
status: exit status: 1
command: "kani" "/home/ubuntu/kani/tests/kani/Stubbing/foreign_functions.rs" "--enable-unstable" "--enable-stubbing"
stdout:
------------------------------------------
Kani Rust Verifier 0.34.0 (standalone)
error: /home/ubuntu/kani/target/kani/bin/kani-compiler exited with status exit status: 1

------------------------------------------
stderr:
------------------------------------------
error[E0308]: mismatched types
  --> /home/ubuntu/kani/tests/kani/Stubbing/foreign_functions.rs:51:38
   |
51  |     assert_eq!(unsafe { libc::strlen(str_ptr) }, 4);
   |                         ------------ ^^^^^^^ expected `*const u8`, found `*const i8`
   |                         |
   |                         arguments to this function are incorrect
   |
   = note: expected raw pointer `*const u8`
              found raw pointer `*const i8`
note: function defined here
  --> /home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/src/unix/mod.rs:560:12
   |
560 |     pub fn strlen(cs: *const c_char) -> size_t;
   |            ^^^^^^

error[E0308]: mismatched types
  --> /home/ubuntu/kani/tests/kani/Stubbing/foreign_functions.rs:60:33
   |
60  |     assert_eq!(unsafe { new_ptr(str_ptr) }, 4);
   |                         ------- ^^^^^^^ expected `*const u8`, found `*const i8`
   |                         |
   |                         arguments to this function are incorrect
   |
   = note: expected raw pointer `*const u8`
              found raw pointer `*const i8`
note: function defined here
  --> /home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/src/unix/mod.rs:560:12
   |
560 |     pub fn strlen(cs: *const c_char) -> size_t;
   |            ^^^^^^

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0308`.

------------------------------------------



failures:
   [kani] kani/Intrinsics/ConstEval/pref_align_of.rs
   [kani] kani/Stubbing/foreign_functions.rs

test result: FAILED. 489 passed; 2 failed; 25 ignored; 0 measured; 0 filtered out; finished in 377.91s

Some tests failed in compiletest suite=kani mode=kani host=(none) target=(none)

Aug 23 '23 21:08 adpaco-aws

I've been able to fix the two tests above, but now there's some more failures on the ui regression suite:

failures:
    [expected] ui/concrete-playback/array/main.rs
    [expected] ui/concrete-playback/custom/main.rs
    [expected] ui/concrete-playback/i8/main.rs
    [expected] ui/concrete-playback/non_zero/main.rs
    [expected] ui/concrete-playback/option/main.rs
    [expected] ui/concrete-playback/result/main.rs
    [expected] ui/concrete-playback/u8/main.rs

test result: FAILED. 97 passed; 7 failed; 0 ignored; 0 measured; 0 filtered out; finished in 18.54s

Aug 24 '23 18:08 adpaco-aws

I've been able to fix the two tests above, but now there's some more failures on the ui regression suite

All these seem to be failing for the same reason, let me explain using ui/concrete-playback/u8/main.rs as an example. The test expects concrete playback to print the following:

#[test]
fn kani_concrete_playback_harness
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 0
        vec![0],
        // 101
        vec![101],
        // 255
        vec![255]
    ];
    kani::concrete_playback_run(concrete_vals, harness);
}

However, in ARM64 Linux it's print this:

#[test]
fn kani_concrete_playback_harness_6199617291819462955() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 0
        vec![0],
        // 'e'
        vec![101],
        // 255
        vec![255],
    ];
    kani::concrete_playback_run(concrete_vals, harness);
}

Note that the interpreted value for the byte with value 101 is 'e'.

At first, I thought this could be a formatting issue in Kani, but apparently the value is already 'e' when we extract it from the trace. The trace item is being deserialized into a String; maybe the ASCII values are coming from CBMC?

Aug 24 '23 22:08 adpaco-aws

Yes, that’s CBMC’s doing: one peculiarity of ARM64 is that the char type is unsigned. That makes CBMC print ASCII characters here.

Aug 25 '23 04:08 tautschnig

It’s amazing how many times that choice has bitten Arm software. Either making the ‘char’ explicitly ‘signed char’ or building with ‘-fsigned-char’ should fix it.

Aug 25 '23 12:08 AGSaidi

Thank you @tautschnig and @AGSaidi !

Got some good news: All other tests in our standard regression suites are passing 😄

Aug 29 '23 20:08 adpaco-aws