support Apple M1 (arm64), cpp kernel as x86_64

[vogler]

Related issues:

• Frontc.ParseError for arm/_structs.h on Apple M1 cil#41
  • TODO fix __int128 in CIL , then change the definition in arm64.h which currently uses unsigned long long instead
• add linux-headers/arch/arm64 since we only have x86 #312

We can try afterwards if this also helps with running on RPi or other ARM-based machines.
However, uname -m for 32bit kernel rpi3 says armv7l and for 64bit kernel rpi4 aarch64.

[michael-schwarz]

Do you want to address these related issues before merging this or should we merge it first (to get something working on M1 machines) and then tackle these separately?

[vogler]

There are actually two goals:

• running on arm64 and analyzing as x86_64 requires Frontc.ParseError for arm/_structs.h on Apple M1 cil#41 and -D__x86_64__ added to cppflags
• running on any and analyzing arm64 requires add linux-headers/arch/arm64 since we only have x86 #312

I haven't tested how different preprocessing results for arm64 vs. x86_64 are (can be done on any machine).
To have comparable benchmarks, it might make sense to analyze as x86_64 even on other architectures.
OTOH it may conflict with the sizes determined by CIL in machdep.ml which would depend on #54.

With goblint/cil#41 fixed, we could merge this to cover the first goal.
I'll add -D__x86_64__ on arm64 (could do it for any arch I guess). #54 can then introduce an option arch or sth similar.

[michael-schwarz]

I think unlocked regression tests fail because the goblint.opam file was not regenerated in this PR and still has the old pin. We just don't see those failures yet on master because they only run nightly.

[vogler]

Wow, so there are three files to update... I thought goblint.opam is generated on build, but apparently not.
Maybe we should add some dune rule for generating or at least checking goblint.opam and goblint.opam.locked when goblint.opam.template changes.
Fixed in 6c021ef - github apparently doesn't show commits on the PR branch after merge...

[sim642]

Maybe we should add some dune rule for generating or at least checking goblint.opam and goblint.opam.locked when goblint.opam.template changes.

This would happen if we build everything with dune build directly, instead of having make just compile the .exe target. But I think then it also tries to do the JS build, which last I tried failed for me (JS dependencies aren't declared?).

[vogler]

Also missing benchmark:

Error: Program js_of_ocaml not found in the tree or in PATH
 (context: default)
Hint: opam install js_of_ocaml-compiler
File "bench/deriving/dune", line 3, characters 12-21:
3 |  (libraries benchmark batteries.unthreaded)
                ^^^^^^^^^
Error: Library "benchmark" not found.