[KIP] - Apple Silicon support

[Baltoli]

Motivation

We currently offer Mac support for K, but not on Apple Silicon. As their product lineup removes legacy x86 macs, we need to work on support for K on macos/ARM.

#2276 summarises some of the early issues with AS support.

Potential Alternatives/Work-arounds

There isn't much alternative, other than dropping support for macOS entirely.

Testing Approach

For the moment, I'm using a single ARM mac mini through macstadium to prototype the necessary changes. In the future we'll need to work out how best to include an AS machine into our CI infrastructure.

[dwightguth]

As far as CI goes, I intend to replace our use of the Mac server and Anka with GitHub Actions as soon as I get the time. I can only assume that at some point, GitHub will start offering an ARM Mac GitHub Actions runner. We can probably wait until then to implement the release process, and tell people to build k from source in the meantime.

[Baltoli]

They currently seem to be tracking for a 2022 release of an Apple Silicon environment, per this thread. Supporting source builds but not releases on AS until then seems like a reasonable compromise.

[radumereuta]

Look into different output formats. Just to narrow down the code path that fails.
Look into valgrind.

[Baltoli]

First blocking issue is runtimeverification/llvm-backend#445 - appears to be some kind of stack corruption bug in our generated code on ARM64 macos.

Looking into building the backend on ARM64 Linux to see if I can reproduce the same bug in an environment where Valgrind is available.

[Baltoli]

Once PRs runtimeverification/llvm-backend#446 and runtimeverification/llvm-backend#443 are merged, the LLVM backend will support compilation for Apple Silicon and I'll move on to the other parts of the toolchain.

[Baltoli]

The Haskell backend should support Apple Silicon without much work, though I haven't closed the loop to run the integration tests yet. runtimeverification/haskell-backend#2893 adds documentation for the additional stack options that are required to get a working copy of ghc.

This will require a change to K to allow the requisite options to be passed through to stack when building the Haskell backend.

[Baltoli]

I can build a working version of the mpfr_java library on ARM macos. However, it fails unit tests (presumably either a change in MPFR from upstream - confirm the version we expect). Once this is versioned and uploaded to our maven repo, we should be able to use the mpfr bindings.

[Baltoli]

It seems like some Java dependencies that rely on native code will need to be updated to newer versions that properly support Apple Silicon (for example, here @ACassimiro identifies an issue with JANSI).

I'll work on updating these dependencies properly.

[Baltoli]

More on the availability of GitHub actions for Apple Silicon in this issue; the gist of the problem is that the .NET release GH use to run actions doesn't yet support AS properly.

If it were to become an issue for us sooner than the next 6-12 months, there seem to be plenty of hacky workarounds. Further ahead than that, it's likely we'll get some kind of official support.

[Baltoli]

The MPFR library now has support for building on Apple Silicon; once runtimeverification/mpfr-java#12 is merged I'll be able to get a new version of the dependency deployed to our Maven repo.

[Baltoli]

Finally tracked down the bug with Jansi - the root problem seems to be Jline bundling an incompatible version. Working on updating both at once.

[Baltoli]

Closed by #2286