Support for macOS arm64

[fcoury]

I get the following error from running Prusti within the VSCode extension:

[stderr] dyld[62808]: Library not loaded: '@rpath/libjli.dylib'
  Referenced from: '/Users/fcoury/Library/Application Support/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/prusti-server-driver'
  Reason: tried: '/opt/homebrew/Cellar/openjdk@17/17.0.4.1_1/libexec/openjdk.jdk/Contents/Home/lib/libjli.dylib' (mach-o file, but is an incompatible architecture (have (arm64), need (x86_64)))

Seems like it's looking for the x84_64 version of this library, which I obviously don't have due to my computer's architecture.

> $ java -version
openjdk version "17.0.4.1" 2022-08-12
OpenJDK Runtime Environment Homebrew (build 17.0.4.1+1)
OpenJDK 64-Bit Server VM Homebrew (build 17.0.4.1+1, mixed mode, sharing)

[Gadiguibou]

I tried installing a x86_64 Java SDK and pointing Prusti Assistant to it using prusti-assistant.javaHome and it fixed the original error but I ran into the following error shortly after:

error: failed to run `rustc` to learn about target-specific information

Caused by:
  process didn't exit successfully: `/Users/gabriel/Library/Application Support/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/prusti-rustc rustc - --crate-name ___ --print=file-names --crate-type bin --crate-type rlib --crate-type dylib --crate-type cdylib --crate-type staticlib --crate-type proc-macro --print=sysroot --print=cfg` (exit status: 255)
  --- stderr
  dyld[34221]: Library not loaded: @rpath/librustc_driver-88b66bfaeeb90970.dylib
    Referenced from: <0B8B796C-EA8F-3D3B-AFAB-2988B0AF6C6C> /Users/gabriel/Library/Application Support/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/prusti-driver
    Reason: tried: '/System/Volumes/Preboot/Cryptexes/OS@rpath/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/Users/gabriel/.rustup/toolchains/nightly-2022-09-18-aarch64-apple-darwin/lib/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/Users/gabriel/.rustup/toolchains/nightly-2022-09-18-aarch64-apple-darwin/bin/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/Users/gabriel/.sdkman/candidates/java/11.0.2-open/lib/jli/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/Users/gabriel/.rustup/toolchains/nightly-2022-09-18-aarch64-apple-darwin/lib/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/Users/gabriel/lib/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/usr/local/lib/librustc_driver-88b66bfaeeb90970.dylib' (no such file), '/usr/lib/librustc_driver-88b66bfaeeb90970.dylib' (no such file, not in dyld cache)

[fpoli]

I think it's because we only compile and publish MacOS binaries using Github's runners, which use Intel and not M1. So, one solution for us should be to cross compile for M1 from the Intel VM offered by Github.

[fpoli]

Here is an example of how to cross-compile binaries for M1 from Intel: mbrubeck/agate@2853ba5. With that, we can release precompiled binaries for macOS M1, but we cannot properly test them. Nor even rustc can run tests on macOS M1 at the moment: rust-lang/rust#73908.

[fpoli]

• Support for macOS with M1 is blocked by Viper on macOS arm64 viper-ide#327
• Cross-compiling Prusti for M1 from x64 fails because of issues with OpenSSL: https://github.com/viperproject/prusti-dev/actions/runs/3297086761/jobs/5437491326

  run pkg_config fail: "pkg-config has not been configured to support cross-compilation.\n\nInstall a sysroot for the target platform and configure it via\nPKG_CONFIG_SYSROOT_DIR and PKG_CONFIG_PATH, or install a\ncross-compiling wrapper for pkg-config and set it via\nPKG_CONFIG environment variable."

  --- stderr
  thread 'main' panicked at '

  Could not find directory of OpenSSL installation, and this `-sys` crate cannot
  proceed without this knowledge. If OpenSSL is installed and this crate had
  trouble finding it,  you can set the `OPENSSL_DIR` environment variable for the
  compilation process.

  Make sure you also have the development packages of openssl installed.
  For example, `libssl-dev` on Ubuntu or `openssl-devel` on Fedora.

  If you're in a situation where you think the directory *should* be found
  automatically, please open a bug at https://github.com/sfackler/rust-openssl
  and include information about your system as well as this message.

  $HOST = x86_64-apple-darwin
  $TARGET = aarch64-apple-darwin
  openssl-sys = 0.9.76

  ', /Users/runner/.cargo/registry/src/github.com-1ecc6299db9ec823/openssl-sys-0.9.76/build/find_normal.rs:191:5
  stack backtrace:
     0: rust_begin_unwind
               at /rustc/bf15a9e5263fcea065a7ae9c179b2d24c2deb670/library/std/src/panicking.rs:575:5
     1: core::panicking::panic_fmt
               at /rustc/bf15a9e5263fcea065a7ae9c179b2d24c2deb670/library/core/src/panicking.rs:65:14
     2: core::panicking::panic_display
     3: build_script_main::find_normal::find_openssl_dir
     4: build_script_main::find_normal::get_openssl::{{closure}}
     5: core::option::Option<T>::unwrap_or_else
     6: build_script_main::find_normal::get_openssl
     7: build_script_main::find_openssl
     8: build_script_main::main
     9: core::ops::function::FnOnce::call_once
  note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
warning: build failed, waiting for other jobs to finish...

[tatsuya6502]

Here is a possible workaround as of today (Nov 14, 2002). By using it, I was able to verify the examples on the Basic Usage chapter of the Prusti user guide.

1. Install arm64 version of OpenJDK using Homebrew: brew install openjdk
   • This will install OpenJDK 19.0.1 (2022-10-18).
   • Make sure you use arm64 version of Homebrew.
2. Set the JAVA_HOME environment variable to /opt/homebrew/opt/openjdk
3. Clone the Prusti repository.
4. Download the Viper command line tools (ViperToolsMac.zip) (release 2022.7) from the download page.
   • Note: This should contain a x86_64 version of Z3.
5. Expand ViperToolsMac.zip into viper_tools directory of prusti-dev.
6. Download an arm64 version of Z3 (z3-4.11.2-arm64-osx-11.0.zip).
7. Expand it and copy bin/z3 into prusti-dev/viper_tools/z3/bin/. (Overwrite the existing x86_64 one)
8. Run the following command on the Z3 binary so that macOS will allow it to be opened:
   • xattr -d com.apple.quarantine prusti-dev/viper_tools/z3/bin/z3
9. Follow the instructions of the Setup chapter of the Prusti dev guide. Build Prusti from source and configure the VS Code extension.

[fpoli]

• Download an arm64 version of Z3 (z3-4.11.2-arm64-osx-11.0.zip).

• Expand it and copy bin/z3 into prusti-dev/viper_tools/z3/bin/. (Overwrite the existing x86_64 one)

• Run the following command on the Z3 binary so that macOS will allow it to be opened:

  • xattr -d com.apple.quarantine prusti-dev/viper_tools/z3/bin/z3

We got reports saying that the x86_64 version of z3 works fine, but might be slower than the arm64 one.

[damienstanton]

There is no viper_tools dir in the repo. Are the instructions from November 2022 still accurate?

[Aurel300]

@damienstanton The viper_tools directory is created by the setup script (/x.py setup), which automatically downloads the correct version of Viper for the current OS.

[fpoli]

Note for the Prusti developers: upgrading the jni dependency from version 0.20 to 0.21 should make it possible to cross-compile Prusti for arm64 from the x86 macOS runner provided by GitHub, so that we can later release macOS arm64 precompiled binaries. That's because with jni 0.21 it's possible to use different JVM versions when compiling vs when running Prusti. When (cross-)compiling we should use the x86 JVM version available in the macos-latest image, but when running Prusti should use the arm64 JVM version installed on the computer of the users.

[fpoli]

M1 runners are now available: https://github.blog/changelog/2024-01-30-github-actions-introducing-the-new-m1-macos-runner-available-to-open-source

[fpoli]

We now release pre-compiled Prusti binaries also for macOS arm64: https://github.com/viperproject/prusti-dev/releases/tag/v-2024-02-29-1455. Let us know if there are still issues with that.

(Note that the Prusti Assistant IDE extension doesn't use those new binaries yet. That's tracked in viperproject/prusti-assistant#191.)