Release `arm64` / universal binaries for macOS #5848

thpani · 2022-02-17T09:49:09Z

It would be great to include arm64 binaries for macOS in the github releases, given the adoption of Apple's M1.

The text was updated successfully, but these errors were encountered:

NikolajBjorner · 2022-02-17T10:13:09Z

what is the build configuration for this?

NikolajBjorner · 2022-02-17T16:28:29Z

releases use hosted agents configured as:
https://github.com/actions/virtual-environments/blob/main/images/macos/macos-11-Readme.md
It will probably be cross compiled, but I am unsure of details, https://www.starmessagesoftware.com/blog/compile-macos-desktop-application-arm64-apple-silicon-m1-chip-cpu

thpani · 2022-02-17T16:44:04Z

On my M1 Mac, the usual python3 scripts/mk_make.py; cd build; make produces arm64 binaries without modifications.

I took a quick stab at cross-compiling by passing -arch arm64 to compiler and linker, which seems to work fine. Haven't done any testing though. Passing both -arch arm64 -arch x86_64 may also work to produce fat binaries that support both architectures.

thpani · 2022-02-18T13:27:42Z

Build config for cross-compilation on x86_64: https://gist.github.com/thpani/7d23c8e6eabdae8edaf7ce1e44179a87

Overall, I had to

add -arch arm64 to CXXFLAGS, LINK_EXTRA_FLAGS, SLINK_EXTRA_FLAGS
remove -mfpmath=sse -msse -msse2 from CXXFLAGS

(Keeping SSE would fail with clang: error: unknown FP unit 'sse', which makes sense on ARM.)

NikolajBjorner · 2022-02-20T22:12:03Z

I read somewhere, but can't find it, that you can pass -arch x86_64 amd64 and get a single (universal?) binary.
This could get me past the hump of updating https://github.com/Z3Prover/z3/blob/master/scripts/nightly.yaml to produce binaries of general use. The other option would be separate binaries.

thpani · 2022-02-21T08:26:54Z

Yes, passing -arch multiple times with different architectures will build a universal binary.

On my machine, the results look fine:

~/s/z/build $ file z3 libz3.*
z3:          Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit executable x86_64] [arm64]
z3 (for architecture x86_64):	Mach-O 64-bit executable x86_64
z3 (for architecture arm64):	Mach-O 64-bit executable arm64
libz3.a:     Mach-O universal binary with 2 architectures: [x86_64:current ar archive] [arm64]
libz3.a (for architecture x86_64):	current ar archive
libz3.a (for architecture arm64):	current ar archive
libz3.dylib: Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit dynamically linked shared library x86_64] [arm64]
libz3.dylib (for architecture x86_64):	Mach-O 64-bit dynamically linked shared library x86_64
libz3.dylib (for architecture arm64):	Mach-O 64-bit dynamically linked shared library arm64

I don't know if there's a way to control per-architecture switches (FP unit / SSE) this way, though.

NikolajBjorner · 2022-02-21T16:15:09Z

Thanks, closer with scripts/nightly.yaml. nightly now builds, but I see:

Only the archive contains some trace of arm64.
Though, note that I am unfamiliar whether "file" elides some information that is not transparent on x64 machines.
Can you download the latest nightly release and see what it says for you?

thpani · 2022-02-21T17:41:33Z

Cool, thanks for working on this!

I checked the latest nightly, can confirm that only the static library reports as a universal binary on my machine.

Maybe it's the toolchain version? This mentions that XCode >= 12.2 is necessary to build universal binaries.

I'm running the command-line tools, which report as

$ pkgutil --pkg-info=com.apple.pkg.CLTools_Executables | grep version
version: 13.0.0.0.1.1627064638
$ clang --version
Apple clang version 13.0.0 (clang-1300.0.27.3)
Target: x86_64-apple-darwin21.3.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

NikolajBjorner · 2022-02-21T18:32:08Z

toolchains should be >= 12.2 (https://docs.microsoft.com/en-us/azure/devops/pipelines/agents/hosted?view=azure-devops&tabs=yaml)

During compilation it shows
/Applications/Xcode_13.2.1.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr

NikolajBjorner · 2022-02-21T19:32:35Z

Is clang required?

It currently configures with gcc.

Host platform: Darwin
C++ Compiler: g++
C Compiler : gcc
Archive Tool: ar
Arithmetic: internal
Prefix: /Library/Frameworks/Python.framework/Versions/2.7
64-bit: True
FP math: Disabled
Python pkg dir: /Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages
Python version: 2.7
JNI Bindings: /Users/runner/hostedtoolcache/Java_Temurin-Hotspot_jdk/8.0.322-6/x64/Contents/Home/include
Java Compiler: /usr/bin/javac
C# Compiler: dotnet

thpani · 2022-02-25T11:29:15Z

Is clang required?

So far, I have only tried this with Apple's clang that's distributed with the Xcode command line tools.
Would it help if I try another compiler?

NikolajBjorner · 2022-02-25T12:52:00Z

I am a bit stuck here: the build uses g++ by default. It can be changed but requires some bandwidth and understanding of what may work.

NikolajBjorner · 2022-04-09T07:26:22Z

Could you try the arm64 releases from the Nightly build?
https://github.com/Z3Prover/z3/releases
See

thpani · 2022-04-12T08:57:11Z

This is great, thank you!

I verified the binary, dynamic and static libraries working natively on arm64.

The Java dynamic library still seems to be built for x86_64?

$ lipo -detailed_info libz3java.dylib
input file libz3java.dylib is not a fat file
Non-fat file: libz3java.dylib is architecture: x86_64

When I try running the Java example on an arm64 JVM I get:

$ DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: .:/Users/thomas/Library/Java/Extensions:/Library/Java/Extensions:/Network/Library/Java/Extensions:/System/Library/Java/Extensions:/usr/lib/java:.
    at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2434)
    at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:848)
    at java.base/java.lang.System.loadLibrary(System.java:2015)
    at com.microsoft.z3.Native.<clinit>(Native.java:17)
    at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87)
    at JavaExample.main(JavaExample.java:2267)

The exception ("no libz3java") is expected if the library file is for a wrong architecture; I confirmed that the paths are set correctly.

NikolajBjorner · 2022-04-12T10:25:12Z

what is the command line for javac to cross compile to arm64?

thpani · 2022-04-12T12:43:13Z

This is C++ code, the Makefile target is libz3java$(SO_EXT) compiling/linking src/api/java/Native.cpp.

NikolajBjorner · 2022-04-12T15:04:09Z

CXXFLAGS should have arch arm64 already, so I don't see immediately how it can miss the cross compile.

This is probably easiest to debug on a non-arm MacOS x64 by running
the scripts/mk_unix_release.py command using parameters from nightly.yaml for the MaxArm64 build.

0xAnon101 · 2022-05-16T14:36:39Z

Could you try the arm64 releases from the Nightly build? https://github.com/Z3Prover/z3/releases See

https://github.com/Z3Prover/z3/releases/download/Nightly/z3-4.8.16-arm64-osx-10.16.zip

https://github.com/Z3Prover/z3/releases/download/Nightly/z3_solver-4.8.16.0-py2.py3-none-macosx_10_16_arm64.whl

Hey there, the second link doesn't exist anymore. I was trying to do pip install z3-solver but there is this build error for z3-solver

NikolajBjorner · 2022-05-16T16:46:02Z

The new link is https://github.com/Z3Prover/z3/releases/download/Nightly/z3_solver-4.8.18.0-py2.py3-none-macosx_10_16_arm64.whl

In other words, the version number increased since I pasted in the link. The path to the "Nightly" build does not change:
That is, if you click on

    https://github.com/Z3Prover/z3/releases/download/Nightly

you get directed to the nightly builds and you can browse the assets of the nightly build.
You will see a pulldown "Assets". There are 22 of them. Click on the arrow to expand the assets.
Then there is a list of assets from the nightly build including one with an arm64 suffix.

The bad news is that I don't think this works. It was tested before and I was told it didn't install / work properly.
I don't have a good way to test it myself nor bandwidth to figure out the fix.
The pipeline for the nightly is here

 https://github.com/Z3Prover/z3/blob/master/scripts/nightly.yaml

You can see the steps used for building the arm64 version.
Thanks to help the cmake dependencies for pypi have been included so that a pypi install is possible (but after building z3 yourself, and that can trigger some local issues). Overall there are several tasks that are left for good support for arm64. I tried to summarize them here:

 https://github.com/Z3Prover/z3/discussions/6020

It definitely isn't a project that goes to the core of developing automated reasoning tools, but I think it is an issue that affects a growing audience. So maybe we can call it "take one for the team not-so-beach project". I am even happy to facilitate a vendor position for this, with the caveat that the overhead of setting it up for this specific task probably outweighs the overall efforts.

NikolajBjorner · 2022-06-08T16:00:45Z

Java bindings with nightly were tested by Isabel Garcia Contreras and reported to work.

TodAmon · 2022-06-09T14:34:22Z

Did the path to the nightly change? I am seeking the Java bindings for arm64 and am getting 404s

agurfinkel · 2022-06-09T14:37:51Z

agurfinkel · 2022-06-09T14:38:17Z

@TodAmon they have, new links above

0xAnon101 · 2022-07-04T13:39:00Z

Great

NikolajBjorner · 2022-07-11T23:55:13Z

in release 4.9.1

Niggelgame · 2022-07-14T21:45:54Z

The libz3java.dylib in 4.9.1 still seems to be compiled as x86_64.

When compiling it myself with an M1 chip I needed to add -arch arm64 to the linker step of libz3java in the generated Makefile to get a working arm64 library.

NikolajBjorner · 2022-07-14T23:52:39Z

Can you paste the line from your Makefile?
I guess it corresponds to this

z3/scripts/mk_util.py

Line 1834 in af80bd1

    
           out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %

but it is easier if there is some corrobation. I can then run the nightly build and we can try this before I release 4.9.2 fully (it will be soon).

agurfinkel · 2022-07-15T03:19:53Z

I don't think current compilation pipeline can produce universal binaries. However, there are both x86 and arm releases of z3.

Is the claim that x86 binary included in arm release?

NikolajBjorner · 2022-07-15T03:34:32Z

mk_unix_dist.py takes a command-line to specify arm64. See

z3/scripts/release.yml

Line 51 in af80bd1

    
           - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0

Niggelgame · 2022-07-15T06:44:03Z

Can you paste the line from your Makefile? I guess it corresponds to this

$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) api/java/Native$(OBJ_EXT) libz3$(SO_EXT)

It seems to be the one from

z3/scripts/mk_util.py

Line 1834 in af80bd1

    
           out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %

TodAmon · 2022-07-15T15:11:32Z

@agurfinkel yes the arm release does not include an arm binary:

$ file libz3.dylib
libz3.dylib: Mach-O 64-bit dynamically linked shared library arm64
$ file libz3java.dylib 
libz3java.dylib: Mach-O 64-bit dynamically linked shared library x86_64

NikolajBjorner · 2022-07-17T00:25:07Z

Could you (one of you) see if the current nightly is built correctly?

https://github.com/Z3Prover/z3/releases/download/Nightly/z3-4.9.2-arm64-osx-11.0.zip

Some context: the link flags did not have the arm64 flag specified. I have updated the build script to include link flags that include the -arm64 option (at least should).

thpani · 2022-07-18T09:06:03Z

Could you (one of you) see if the current nightly is built correctly?

https://github.com/Z3Prover/z3/releases/download/Nightly/z3-4.9.2-arm64-osx-11.0.zip

Looks good! Confirmed via

$ lipo -detailed_info libz3.a libz3.dylib libz3java.dylib z3
Non-fat file: libz3.a is architecture: arm64
Non-fat file: libz3.dylib is architecture: arm64
Non-fat file: libz3java.dylib is architecture: arm64
Non-fat file: z3 is architecture: arm64

NikolajBjorner · 2022-08-22T00:32:35Z

release 11.0 includes these fixes

thpani changed the title ~~Publish arm64 / universal binaries for macOS~~ Release arm64 / universal binaries for macOS Feb 17, 2022

no-preserve-root mentioned this issue Feb 17, 2022

Add support for aarch64 tudo-aqua/z3-turnkey#12

Closed

breandan mentioned this issue Apr 13, 2022

Example Gradle Project sosy-lab/java-smt#224

Open

MatthewShao mentioned this issue Apr 22, 2022

MacOS installation error KeenSecurityLab/BinAbsInspector#12

Closed

NikolajBjorner added the Arm64 label Jun 2, 2022

NikolajBjorner closed this as completed Jul 11, 2022

NikolajBjorner reopened this Jul 14, 2022

NikolajBjorner added a commit that referenced this issue Jul 15, 2022

give java dynamic lib a chance for extra flags for #5848

b743e21

waywardmonkeys mentioned this issue Aug 3, 2022

getting Z3 version #6218

Closed

NikolajBjorner closed this as completed Aug 22, 2022

hlolli mentioned this issue Dec 28, 2022

fix: don't use opmtimization flag sse for m1 apple silicon compiler csound/csound#1673

Closed

KE7 mentioned this issue Aug 10, 2023

Mac m1 uclid-org/uclid#226

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Release `arm64` / universal binaries for macOS #5848

Release `arm64` / universal binaries for macOS #5848

thpani commented Feb 17, 2022

NikolajBjorner commented Feb 17, 2022

NikolajBjorner commented Feb 17, 2022

thpani commented Feb 17, 2022 •

edited

Loading

thpani commented Feb 18, 2022 •

edited

Loading

NikolajBjorner commented Feb 20, 2022

thpani commented Feb 21, 2022

NikolajBjorner commented Feb 21, 2022 •

edited

Loading

thpani commented Feb 21, 2022

NikolajBjorner commented Feb 21, 2022 •

edited

Loading

NikolajBjorner commented Feb 21, 2022

thpani commented Feb 25, 2022

NikolajBjorner commented Feb 25, 2022

NikolajBjorner commented Apr 9, 2022

thpani commented Apr 12, 2022 •

edited

Loading

NikolajBjorner commented Apr 12, 2022

thpani commented Apr 12, 2022 •

edited

Loading

NikolajBjorner commented Apr 12, 2022

0xAnon101 commented May 16, 2022

NikolajBjorner commented May 16, 2022

NikolajBjorner commented Jun 8, 2022

TodAmon commented Jun 9, 2022

agurfinkel commented Jun 9, 2022

agurfinkel commented Jun 9, 2022

0xAnon101 commented Jul 4, 2022

NikolajBjorner commented Jul 11, 2022

Niggelgame commented Jul 14, 2022

NikolajBjorner commented Jul 14, 2022

agurfinkel commented Jul 15, 2022

NikolajBjorner commented Jul 15, 2022

Niggelgame commented Jul 15, 2022

TodAmon commented Jul 15, 2022 •

edited

Loading

NikolajBjorner commented Jul 17, 2022 •

edited

Loading

thpani commented Jul 18, 2022

NikolajBjorner commented Aug 22, 2022

Release arm64 / universal binaries for macOS #5848

Release arm64 / universal binaries for macOS #5848

Comments

thpani commented Feb 17, 2022

NikolajBjorner commented Feb 17, 2022

NikolajBjorner commented Feb 17, 2022

thpani commented Feb 17, 2022 • edited Loading

thpani commented Feb 18, 2022 • edited Loading

NikolajBjorner commented Feb 20, 2022

thpani commented Feb 21, 2022

NikolajBjorner commented Feb 21, 2022 • edited Loading

thpani commented Feb 21, 2022

NikolajBjorner commented Feb 21, 2022 • edited Loading

NikolajBjorner commented Feb 21, 2022

thpani commented Feb 25, 2022

NikolajBjorner commented Feb 25, 2022

NikolajBjorner commented Apr 9, 2022

thpani commented Apr 12, 2022 • edited Loading

NikolajBjorner commented Apr 12, 2022

thpani commented Apr 12, 2022 • edited Loading

NikolajBjorner commented Apr 12, 2022

0xAnon101 commented May 16, 2022

NikolajBjorner commented May 16, 2022

NikolajBjorner commented Jun 8, 2022

TodAmon commented Jun 9, 2022

agurfinkel commented Jun 9, 2022

agurfinkel commented Jun 9, 2022

0xAnon101 commented Jul 4, 2022

NikolajBjorner commented Jul 11, 2022

Niggelgame commented Jul 14, 2022

NikolajBjorner commented Jul 14, 2022

agurfinkel commented Jul 15, 2022

NikolajBjorner commented Jul 15, 2022

Niggelgame commented Jul 15, 2022

TodAmon commented Jul 15, 2022 • edited Loading

NikolajBjorner commented Jul 17, 2022 • edited Loading

thpani commented Jul 18, 2022

NikolajBjorner commented Aug 22, 2022

Release `arm64` / universal binaries for macOS #5848

Release `arm64` / universal binaries for macOS #5848

thpani commented Feb 17, 2022 •

edited

Loading

thpani commented Feb 18, 2022 •

edited

Loading

NikolajBjorner commented Feb 21, 2022 •

edited

Loading

NikolajBjorner commented Feb 21, 2022 •

edited

Loading

thpani commented Apr 12, 2022 •

edited

Loading

thpani commented Apr 12, 2022 •

edited

Loading

TodAmon commented Jul 15, 2022 •

edited

Loading

NikolajBjorner commented Jul 17, 2022 •

edited

Loading