support for Mac with M series chips

[baoluomeng]

Curious about the timeline to support Mac with Apple M1,2,3?

[kfriedberger]

We currently do not have Apple hardware for development and testing. Cross-compilation for Apple might not work. That operating system is special. 💰

If an SMT solver provides native libraries on its own, such as Z3 maybe, we can include it.
Otherwise, you can use Java-based SMT solvers like SMTInterpol on any platform.

[baoluomeng]

The latest Z3 has native support for arm64 Mac: https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0. I downloaded the dylib files and plugged them into JavaSMT on my arm64 Mac. It works fine so far. But I would prefer a centralized approach like JavaSMT so that I don't have to tell my teammates how to set it up. Thanks.

[ThomasHaas]

See this long-standing discussion. The issue seems to be somewhat orthogonal to MacOS as it applies to all ARM machines.

[hernanponcedeleon]

@kfriedberger since z3 already provides native libraries for arm, would it be possible to make these available via maven?

[kfriedberger]

Hi @hernanponcedeleon .

The topic appeared often enough to make me really think about it. 😄
I will try to find a solution within the next week, and report here.

Step 1: Define a goal.

Users want X64 and ARM64 binaries for Z3.

Step 2: Make a plan.

Therefore we need:

• publication of binaries into Ivy and Maven:
  • find a future-proof artifact pattern for naming (avoid name collision from X64 and ARM64, including directory structure for sosy_lab-related stuff)
  • update publication scripts
• download via Ivy and Maven:
  • test download,
  • test execution on different architectures (I might even have a ARM64 device available, but no Apple device)

Step 3: Do it. ... Coming soon.

[hernanponcedeleon]

I am pretty sure @ThomasHaas would be willing to help with the testing 😉

[ThomasHaas]

Sure, I can test it on my machine.

[kfriedberger]

Step 3: Collect data and knowhow

Z3

Z3 is available in x64 and arm64 version for Linux, Windows, and OSX. This is impressive. 👍
Linux version went wrong in last few releases, i.e.,

• until 4.13.0, see Linux arm64 build is actually an x86_64 build Z3Prover/z3#7201 🐞
• and in 4.13.2, see Missing Java bindings for Linux on ARM64 in release 4.13.2 Z3Prover/z3#7406 🐞

The nightly build des not provide the Java bindings for Linux. We either wait for an upcoming release, ignore Linux for now, or compile it on our own.
Currently, I can test and debug with Linux-x64 and Windows-x64. Additionally, I played with my arm64-based phone and could execute z3 v4.13.0 and MathSAT v5.6.11 (the plain application binaries) and JavaSMT (the Java-based part, no native libraries, not yet...).

Android (no root) with some ARM8 CPU

• Termux
• SSH reverse tunnel, see documentation for remote access
• proot-distro/ubuntu for glibc and to avoid TLS segment underalignment
  --> yeah 😄 📟 👾
  --> UPDATE: This works for some binaries, but not for default libraries, due to missing glibc and libld on Android. Lets find another way to test ARM64 with some real Linux/Ubuntu.

Directory structures to consider:

(The symbol ⚙️ implies work to do.)

• JavaSMT internally (for development):
  lib/native/<ARCH>/*.so is a symlink to the downloaded dependency in lib/java/runtime-z3/*so.

  • The directory needs to be supported by Sosy-Lab-commons, i.e., we should add arm64 (see NativeLibraries could support more architectures, such as ARMv7 or ARMv8  java-common-lib#38 ). ⚙️
  • The symlink itself can be named as required. No conflict. ✔️ DONE
  • In the runtime directory, there are all libraries from Z3 for all architectures. We can use a unique naming through subdirectories, like arm64/*.[so|dll|dylib] and x64/*.[so|dll|dylib]. ✔️ DONE

• Ant/Ivy:
  The name of a dependency in Ant/Ivy is based on a pattern, which needs to be compatible with other libraries in Sosy-Lab context. The z3 directory is here: https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/. It looks like a classifier (suffix) can be used for the architecture, e.g. like 'libz3-4.13.0-arm64.so`. The downloaded dependency will also get that name, which should avoid conflicts automatically (see above: runtime directory for development). ✔️

  • We need to update the pattern/name and publication scripts. ✔️ DONE for JavaSMT
  • Currently JavaSMT exports configurations like runtime and runtime-z3. We can export more/different configurations for each architecture (and operating system, and solver, and license, ... maybe too many combinations). This can help with including JavaSMT configuration in Ant/Ivy-based applications without getting too fat and too complex. ⚙️
    • JavaSMT's solver Z3 exports solver-z3 as backwards-compatible alias for solver-z3-x64, and an additional solver-z3-arm64. ✔️

• Maven:
  The classifier from Ant/Ivy should also work in some way for Maven. This could be simple. ✔️

  • We need to update the publication script. ✔️ DONE (not backwards-compatible, but only a small change (see 78a298e)

• Apps like CPAchecker, when using JavaSMT as Ant/Ivy dependency:
  CPAchecker stores all dependencies in one directory: lib/java/runtime/. It automatically loads native libraries from there, i.e., the classpath is set in bin/cpachecker. This is caused by the configuration runtime. Maybe we could split it into architecturally separated configurations, or only include JavaSMT for x64 by default. ❓

  • CPAchecker should apply the changed Ivy pattern for repository and cache in the future ⚙️

• Apps like <insert user application>, when using JavaSMT as Maven dependency:
  Maven already requires the copy-dependency-plugin and can rename libraries with it. This should make it possible to provide an example that only downloads dependencies for a specific architetcure and operating system. ✔️ DONE (see 78a298e)

Step 4: Do it. ... Coming soon.

[kfriedberger]

Step 4: Do it.

Work in progress. I updated the previous comment with more details.
See also #395.

Step 5: Testing

Z3 v4.13.0 was published to Maven: https://central.sonatype.com/artifact/org.sosy-lab/javasmt-solver-z3/4.13.0
Feel free to give feedback whether it works on ARM-based Apple machines.
Please use the updated example pom-file as reference: 78a298e