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. :smile: 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. :+1: Linux version went wrong in last few releases, i.e.,

• until 4.13.0, see https://github.com/Z3Prover/z3/issues/7201 :lady_beetle:
• and in 4.13.2, see https://github.com/Z3Prover/z3/issues/7406 :lady_beetle:

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 :smile: :pager: :space_invader: --> 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 :gear: 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 <ARCH> directory needs to be supported by Sosy-Lab-commons, i.e., we should add arm64 (see https://github.com/sosy-lab/java-common-lib/issues/38 ). :heavy_check_mark: DONE
  • The symlink itself can be named as required. No conflict. :heavy_check_mark: 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]. :heavy_check_mark: 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). :heavy_check_mark:

  • We need to update the pattern/name and publication scripts. :heavy_check_mark: 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. :gear:
    • JavaSMT's solver Z3 exports solver-z3 as backwards-compatible alias for solver-z3-x64, and an additional solver-z3-arm64. :heavy_check_mark:

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

  • We need to update the publication script. :heavy_check_mark: DONE (not backwards-compatible, but only a small change (see https://github.com/sosy-lab/java-smt/pull/395/commits/78a298e03cf29385d4d451baebc73244c1d3ef17)

• 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. :question:

  • CPAchecker should apply the changed Ivy pattern for repository and cache in the future :gear:

• 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. :heavy_check_mark: DONE (see https://github.com/sosy-lab/java-smt/pull/395/commits/78a298e03cf29385d4d451baebc73244c1d3ef17)

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

[kfriedberger]

Step 4: Do it.

Work in progress. I updated the previous comment with more details. See also https://github.com/sosy-lab/java-smt/pull/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: https://github.com/sosy-lab/java-smt/pull/395/commits/78a298e03cf29385d4d451baebc73244c1d3ef17

[kfriedberger]

Changes in scripts and publication process are applied with https://github.com/sosy-lab/java-smt/pull/395. See the Readme for support in solvers, operating systems, and platforms.