search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.17k stars 86 forks source link

Kani won't install on Apple M1 #1167

Closed markrtuttle closed 1 year ago

markrtuttle commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 https://github.com/model-checking/kani/blob/f719b565968568335d9be03ef27c5d05bb8fd0b7/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs#L352 are correct for other architectures. Figuring out the values for other architectures would be a great help.

tedinski commented 2 years ago

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 commented 2 years ago
AGSaidi commented 2 years ago

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 commented 2 years ago

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:

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:

I think that might cover everything.

ssoudan commented 2 years ago

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

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 commented 2 years ago

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

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 commented 2 years ago

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

diagprov commented 2 years ago

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:

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

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