Kani won't install on Apple M1

[markrtuttle]

I've installed kani on Apple M1 running MacOS 11.6.5 with

git clone https://github.com/model-checking/kani.git kani
cd kani && git submodule update --init
PATH=$HOME/.cargo/bin:$PATH && cd kani && \
	    ./scripts/setup/macos-10.15/install_deps.sh && \
	    ./scripts/setup/install_rustup.sh && \
	    cargo build --workspace
export PATH=$HOME/.cargo/bin:$(pwd)/kani/scripts:$PATH

(Actually, I modified install_deps.h to brew install universal-ctags instead of ctags.)

Now I run kani on a regression test with

pushd kani/tests/kani/FunctionCall_NoRet-NoParam/
kani main.rs

and I get an exception and stack trace with

error: Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin`, but it is arm64-apple-macosx11.0.0
error: aborting due to previous error

[diagprov]

I have the same problem but for the architectures I use. I have aarch64-unknown-linux-gnu and powerpc64le-unknown-linux-gnu that I use frequently. I'm going to say that aarch64-* support is going to be interesting for a lot of people, including cross compiling to it (Android/iOS).

I'm happy to try to help out in whatever way I can, for either/both platforms. I'll investigate why and see if I think it is something I can work on. If I should join on Zulip or some other chat please let me know.

[zhassan-aws]

Thanks @diagprov. We've disabled support for architectures other than x86_64-unknown-linux-gnu and x86_64-apple-darwin, because we weren't sure whether the hard-coded values in

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

Line 352 in f719b56

fn machine_model_from_session(sess: &Session) -> MachineModel {

are correct for other architectures. Figuring out the values for other architectures would be a great help.

[tedinski]

Do people want to have direct bit-precise support for ARM yet? I mean, sure eventually, but is that the immediate need here?

One possibility here is we can support the easy installation of Kani on M1... by downloading the x86_64 mac binaries and running them under Rosetta.

edit: I should read better. It looked like diagprov was requesting exactly that! Maybe I should ask: would running the x86_64 reasoning under Rosetta on M1 be good enough for some customers? If so, we should split this issue into two and try to add that until we can figure out how to do CI with M1?

[tedinski]

• Github has (as of yesterday!) a pre-release of their runner: Add ARM + MacOS target to be able to use on self-hosted runners actions/runner#805 and EC2 has M1 instances in preview since Dec.
• This appears to be the github tracking issue for github-hosted M1 runners: Support for VMs on Apple M1 actions/runner-images#2187
• Github roadmap item: Actions: Self-hosted runners now support Apple M1 silicon github/roadmap#507

[AGSaidi]

I'd like to see aarch64-* support including Mac OS and aarch64-unknown-linux-gnu.

Is it just the values in defined here that you need?

Are these the rust types or the C types? For example a char in unsigned by default on Arm, but afaik rust defines it explicitly as i8 so that doesn't appy.

[tedinski]

Ah, I'd been meaning to break this issue down into smaller chunks.

I think in general, for bare minimum support, we'll be looking at:

• We need to correctly generate a CBMC Machine Model (as linked in the previous comment) for ARM. (Q1: Is this any different between mac and linux? Or M1 and Graviton?) (Q2: Does Rust or its FFI impose any difficulties on these platforms? For instance, char's signedness in the previous comment? And maybe... does that matter right now?)
• I'm sure trying to build on ARM will result in issues where we've baked platform assumptions. I'd be happy to track these down and fix them once we have the above. (Only major thing off the top of my head: some test cases in our regression suite might be relying on platform assumptions, having never been run on another platform.)

That should allow us to at least build from source on ARM platforms. Notably, however, I believe CBMC isn't distributing pre-built binaries for ARM platforms either (I assume also limited by github actions), so you'd also have to build that from source, too.

Then a few more steps:

• We should add support for --targeting different platforms. (I vaguely recall, but have not investigated, that cross-compiling is "easy" with Rust. In fact, I think the "hard part" is needing the target platform linker and we don't need one of those for Kani.) This should both build the code for that platform (Rust-side) and set the machine model appropriately. I'm not sure how hard this will be. Needs investigation. We likely have a lot of further assumptions baked in about our target being the same platform as we're built for.
• As a temporary workaround, we should allow our installer to install on M1, by downloading and install the x86 binaries, to be run under Rosetta. With the above proper --target support, we should be able to build ARM "binaries" even from this emulated compiler.
• Either when M1 CI is available on github actions, or when we break down and decide to add runners of our own (?? Who knows?) we can finally offer pre-built binaries for M1. (And same for ARM linux.) I suppose we could also try to investigate cross-compiling?

I think that might cover everything.

[ssoudan]

Had a try at adding support for M1 here: https://github.com/ssoudan/kani/tree/feature/m1
Few notes:

• regression tests are passing.
• used a short c++ program (in tools/sizeofs/main.cpp) for most of the values defined in goto_ctx.rs but there are a couple I'm not sure to test for. Namely: memory_operand_size, word_size, null_is_zero, rounding_mode. The other ones were pretty obvious. Help appreciated here.
• tried generating the bundle for cargo-kani and installed it with cargo-kani setup --use-local-bundle kani-0.5.0-aarch64-apple-darwin.tar.gz seems to work, but need more mileage.
• have not looked at the CI aspects.

let me know if I missed something, or if this can be useful. happy to spend a bit more time on that to polish it if needed.

[tedinski]

Ah, the joys of CBMC's undocumented internals! :D

• memory_operand_size appears to be set to int_width/8 on all platforms within CBMC's C frontend. It looks like it is related to alignment_checks.cpp which looks at something about struct layouts. Not sure what. Also, we seem to pass in the same value as int_width... Possibly a bug in Kani, that.
• word_size may actually be deprecated within CBMC. Set it to int_width.
• null_is_zero should always be true. I'm not sure if CBMC even still uses this, actually!
• rounding_mode is apparently always "round-to-nearest" in CBMC unless overridden on the command line. I suspect this might actually be language semantics rather than architecture. I'm guessing Rust may actually document which rounding mode should be used. So, probably use the same.

This appears to be where CBMC sets these parameters: https://github.com/diffblue/cbmc/blob/develop/src/util/config.cpp

I'll probably want to refactor how we construct machine models once we support more than one, but that's not something you need to do to get a PR merged.

[tedinski]

(reopening because I don't think this is fully resolved until we can cargo install kani-verifier like anything else.)

[diagprov]

Hello again, nice to see some work for the M1 :) Summer here so I am slow.

I extracted out what cbmc does to test C bitfield width (and learned that C23 will by the looks of things include separate definitions for certain bitfield widths... which is interesting and I wonder what they're doing r.e. moving away from a char-based memory model) into a small self-contained (C only) executable: https://gist.github.com/diagprov/382ebfc3ac621f29ea4ee54b39c34860 so I can just dump and run that on platforms of interest, and ran it. My compile targets are as follows:

• Solid-Run Honeycomb LX2K running Fedora, $(uname -sm) = Linux aarch64.
• Rockchip RockPro, rk3399, running Armbian, a Ubuntu derivative, Linux aarch64 also.

Compilation is always with -Wall -Werror, checking both clang and gcc.

In all cases I get:

// Constants for 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 = 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 = true;
let wchar_t_width = 32;

The main difference, in case you missed it: wchar is unsigned on these platforms. I've double checked this pretty thoroughly because I didn't believe it, but a straight up comparison of WCHAR_MAX between platforms verifies this is true.

Unfortunately it therefore looks like we'll need to differentiate between whatever the target triple is for aarch64-macos and aarch64-linux, or put another way, yes it is different between mac and linux. I haven't checked freebsd, as none of my machines are currently set up for VMs, but I can try this.

I mentioned ppc64le and other architectures. I'm still interested in them and I'm currently working on a ppc64le patch (biggest challenge has been building an up to date cbmc), particularly as I care mostly about embedded environments so want to port to those in the future (ppc64le isn't embedded, but it is a target I have that is not likely already done). These might be better as separate issues though.

[AGSaidi]

The AAPCS for aarch64 specifies char is an unsigned byte: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#table-3

[diagprov]

I'm not worried about the char type but the wchar_t one. According to that doc, wchar_t should be an unsigned half word or word. Linux distros are following this.

I tried also on an M1 and my code also indicates wchar_t_is_unsigned = false. So Apple is doing something different.

[tedinski]

Just refreshing the links to github actions issues for getting this in CI:

• Support for VMs on Apple M1 actions/runner-images#2187
• GitHub Actions: Apple Silicon (M1) powered macOS runners (Public Beta) github/roadmap#528

They still haven't committed to it yet. :(