Is it possible to compile on arm?

[paolo-di-biase]

I need the tool compiled for arm for some experiments using benchexec, so I'd need the compiled file as you release it for sv-comp but for the arm architecture. I was wondering if I can have some compilation instructions since I can't find them, or if you already have the compiled versions for arm. Thanks.

[maul-esel]

You can find information on building Ultimate in our wiki.

Generally, I'd expect Ultimate itself to run on ARM processors without changes, given a suitable Java runtime. However, you will likely have to create/download ARM builds of the SMT solvers (z3, cvc4/5, mathsat, ...) to replace the binaries that are shipped with Ultimate (located in releaseScripts/default/adds in the repo, resp. in the ZIP files created by the build script).

Maybe our build system experts @danieldietsch @bahnwaerter can point out if I missed something?

[bahnwaerter]

We currently provide Ultimate for the x86-64 architecture on Windows, Linux, and MacOS. As @maul-esel already pointed out, ARM support is conceptually possible. However, this would require not only building the solvers for ARM, but also replacing platform-specific components of our used framework (Equinox). We don't have support for this, but we may add it in the future.

@paolo-di-biase do you need Ultimate for the 64-bit ARM (aarch64) architecture? And what operating system are you using?

[paolo-di-biase]

oKk thanks for the reply.
Yes i need it for aarch64 architecture and Linux operating system, specifically Linux raspi

[maul-esel]

@bahnwaerter are these the same steps we would also have to take if we want ARM-based docker images that run on MacOS host machines?

[bahnwaerter]

@bahnwaerter are these the same steps we would also have to take if we want ARM-based docker images that run on MacOS host machines?

Yes, we could use that setup for the building of ARM-based Docker images, too. All those images are based on a simple Linux distribution (Alpine Linux) and are build to match the specific target architecture (x86-64 or aarch64). First experiments for the x86-64 architecture have shown, that this approach runs smooth on Windows using Docker Desktop. I'm sure this also works on MacOS.

[bahnwaerter]

oKk thanks for the reply. Yes i need it for aarch64 architecture and Linux operating system, specifically Linux raspi

Thanks @paolo-di-biase for your quick reply. I always like to ask about this because it's important to be able to test it. I also have a simple 64-bit ARM hardware running Linux available for testing. I'll take a look at your request soon and provide a prototype if possible. It would be great if you could test it, too.

[paolo-di-biase]

Yes no problem, I can do it.
Thank you.

[maul-esel]

Yes, we could use that setup for the building of ARM-based Docker images, too

👍 Ok, then that could be useful for us as well, e.g. some conferences now ask for ARM-based images when submitting artifacts.

[bahnwaerter]

I've added initial prototype support for the ARM64 architecture on Linux for @paolo-di-biase. By checking out the wip/mb/target-architecture-aarch64 branch, Ultimate can be manually built for the ARM64 hardware architecture. The building process can be performed on any host machine. For performance reasons, it is recommended to use a regular desktop computer and then copy the built artifacts to the ARM64 computer. The only requirements are Java Development Kit version 21 and Maven version 3.9.11 or higher. The build can then be executed using the following commands:

cd trunk/source/BA_MavenParentUltimate
mvn clean package -Pmaterialize

The built Ultimate command line tool for the ARM64 architecture can be found under trunk/source/BA_SiteRepository/target/products/CLI-E4/linux/gtk/aarch64. If necessary, the content of this folder can be copied to the ARM64 computer. Ultimate can then be started by calling the launcher executable of the command line tool via

Ultimate -tc <TOOLCHAIN> -s <SETTINGS> -i <PROGRAM>

where a path to a toolchain and an individual settings file must be specified in order to verify a given program. Toolchain and settings files can be found in the Ultimate repository under trunk/examples/toolchains and trunk/examples/settings/default. Please note that ARM64 versions of our solvers (z3, cvc4, etc.) are currently not included in the build. They must be obtained from the package repositories of the used Linux distribution.

At this prototypical development stage, it's not yet possible to create complete release builds (incl. packaging) for the automatic use with BenchExec. However, it's already possible to test whether the Ultimate build runs correctly on ARM64 hardware. Once this compatibility test is successful, I will continue the work on release builds, so that we can provide packaged versions of each Ultimate tool, which are compatible and ready to be used with BenchExec on ARM64.

The ARM64 build of Ultimate runs smoothly on a Banana Pi BPI-M2 Pro computer running Armbian (based on Debian bookworm). The debug GUI also works (if anyone needs it). It would be great if the test also succeeds on a Raspberry Pi computer running Raspbian OS. @paolo-di-biase, could you please check that?

[paolo-di-biase]

Thank you @bahnwaerter
I don't have raspbian os but I have ubuntu linux on my raspberry pi. I will check everything as soon as I have time to.
Thank you very much.