Use precompiled z3 libs by default

.github/workflows/rust.yml

@@ -2,36 +2,105 @@ name: Rust
 
 on:
  push:
- branches: [ master ]
+ branches: [ master, buildfix3.1, buildfix3.2 ]
  pull_request:
  branches: [ master ]
 
 env:
  CARGO_INCREMENTAL: 0
- RUSTFLAGS: "-D warnings"
+ Z3_RELEASE: 'z3-4.12.1'
+ RUST_BACKTRACE: 'full'
 
 jobs:
  build:
- runs-on: ubuntu-latest
+ strategy:
+ matrix:
+ os: [ubuntu-latest, windows-latest, macos-latest]
+ link: [default, static, system]
+ exclude:
+ - os: ubuntu-latest
+ link: system
+ - os: macos-latest
+ link: system
+ runs-on: ${{ matrix.os }}
  steps:
- - uses: actions/checkout@v2
- - name: Install Z3
- run: sudo apt-get install libz3-dev
- - name: Build
- run: cargo build -vv --all
- # XXX: Ubuntu's Z3 package seems to be missing some symbols, like
- # `Z3_mk_pbeq`, leading to linker errors. Just ignore this, I guess, until
- # we figure out how to work around it. At least we have the
- # statically-linked Z3 tests below...
- if: ${{ success() || failure() }}
- - name: Run tests
- run: cargo test -vv --all
- # See above.
- if: ${{ success() || failure() }}
- - name: Run tests with `arbitrary-size-numeral` enabled
- run: cargo test --manifest-path z3/Cargo.toml -vv --features arbitrary-size-numeral
- # See above.
- if: ${{ success() || failure() }}
+ - name: Checkout
+ uses: actions/checkout@v2
+ if: ${{ matrix.link != 'static' }}
+
+ - name: Checkout with submodules
+ uses: actions/checkout@v2
+ if: ${{ matrix.link == 'static' }}
+ with:
+ submodules: recursive
+
+ - name: Uninstall Z3 on Linux for non-system builds
+ if: ${{ matrix.os == 'ubuntu-latest' && matrix.link != 'system' }}
+ run: sudo apt-get remove libz3-dev
+
+ - name: Install Z3 on Windows for system builds
+ if: ${{ matrix.os == 'windows-latest' && matrix.link == 'system' }}
+ run: |
+ mkdir .tmp
+ curl.exe -L "https://github.com/Z3Prover/z3/releases/download/${env:Z3_RELEASE}/${env:Z3_RELEASE}-x64-win.zip" -o ".tmp/${env:Z3_RELEASE}-x64-win.zip"
+ tar -xf ".tmp/${env:Z3_RELEASE}-x64-win.zip" -C ".tmp"
+ echo "${PWD}\.tmp\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_PATH
+ echo "LIB=${PWD}\.tmp\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_ENV
+ echo "Z3_SYS_Z3_HEADER=${PWD}\.tmp\${env:Z3_RELEASE}-x64-win\include\z3.h" >> $env:GITHUB_ENV
+
+ - name: Build with Z3 releases
+ if: ${{ matrix.link == 'default' }}
+ run: cargo build --workspace --all-targets
+
+ - name: Build with Z3 system installation
+ if: ${{ matrix.link == 'system'}}
+ run: cargo build --workspace --all-targets --features dynamic-link-z3
+
+ - name: Build with static Z3 builds
+ if: ${{ matrix.link == 'static' }}
+ run: cargo build --workspace --all-targets --features static-link-z3
+
+ - name: Mitigate cargo bug (https://github.com/rust-lang/cargo/issues/8531) by setting LD_LIBRARY_PATH
+ if: ${{ matrix.os == 'ubuntu-latest' && matrix.link == 'default' }}
+ run: echo LD_LIBRARY_PATH=$(pwd)/$(find . -wholename './target/debug/build/z3-sys-*/out/z3-*-x64-glibc-*/bin') >> $GITHUB_ENV
+
+ - name: Mitigate cargo bug (https://github.com/rust-lang/cargo/issues/8531) by setting LD_LIBRARY_PATH
+ if: ${{ matrix.os == 'macos-latest' && matrix.link == 'default' }}
+ run: echo LD_LIBRARY_PATH=$(pwd)/$(find . -wholename './target/debug/build/z3-sys-*/out/z3-*-x64-osx-*/bin') >> $GITHUB_ENV
+
+ - name: Mitigate cargo bug (https://github.com/rust-lang/cargo/issues/8531) by setting PATH
+ if: ${{ matrix.os == 'windows-latest' && matrix.link == 'default' }}
+ run: echo (get-item ".\target\debug\build\z3-sys-*\out\z3-*-x64-win\bin").FullName >> $env:GITHUB_PATH
+
+ - name: Test with Z3 releases
+ if: ${{ matrix.link == 'default' }}
+ run: cargo test -vv
+
+ - name: Test with Z3 system installation
+ if: ${{ matrix.link == 'system' }}
+ run: cargo test -vv --features dynamic-link-z3
+
+ - name: Test with static Z3 builds
+ if: ${{ matrix.link == 'static' }}
+ run: cargo test -vv --features static-link-z3
+
+ - name: Assert bindgen correctness for system builds
+ if: ${{ matrix.link == 'system'}}
+ run: |
+ cargo run -p z3-sys-bindgen -- z3-sys/wrapper.h
+ git status && git add . && git diff --cached --exit-code
+
+ - name: Assert bindgen correctness for default builds
+ if: ${{ matrix.link == 'default' }}
+ run: |
+ cargo run -p z3-sys-bindgen -- $(find . -wholename './target/debug/build/z3-sys-*/out/z3-*-x64-*-*/include/z3.h')
+ git status && git add . && git diff --cached --exit-code
+
+ - name: Assert bindgen correctness for static builds
+ if: ${{ matrix.link == 'static' }}
+ run: |
+ cargo run -p z3-sys-bindgen -- z3-sys/z3/src/api/z3.h
+ git status && git add . && git diff --cached --exit-code
 
  build_on_wasm:
  runs-on: ubuntu-latest
@@ -56,44 +125,7 @@ jobs:
  source ./emsdk_env.sh
  - name: Install wasm32-unknown-emscripten target
  run: rustup target add wasm32-unknown-emscripten
- - name: Build z3-sys with statically linked Z3
- run: |
- source ~/emsdk/emsdk_env.sh
- cargo build --target=wasm32-unknown-emscripten --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3
- - name: Build z3 with statically linked Z3
+ - name: Build z3 and z3-sys with statically linked Z3
  run: |
  source ~/emsdk/emsdk_env.sh
- cargo build --target=wasm32-unknown-emscripten --manifest-path z3/Cargo.toml -vv --features static-link-z3
- build_z3_statically:
- strategy:
- matrix:
- build: [linux, macos, windows]
- include:
- - build: linux
- os: ubuntu-latest
- - build: macos
- os: macos-latest
- - build: windows
- os: windows-latest
- runs-on: ${{ matrix.os }}
- steps:
- - uses: actions/checkout@v2
- with:
- submodules: recursive
- - name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797
- uses: KyleMayes/install-llvm-action@v1
- if: matrix.os == 'windows-latest'
- with:
- version: "11.0"
- directory: ${{ runner.temp }}/llvm
- - name: Set LIBCLANG_PATH
- run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
- if: matrix.os == 'windows-latest'
- - name: Build z3-sys with statically linked Z3
- run: cargo build --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3
- - name: Build z3 with statically linked Z3
- run: cargo build --manifest-path z3/Cargo.toml -vv --features static-link-z3
- - name: Test `z3` with statically linked Z3
- run: cargo test --manifest-path z3/Cargo.toml -vv --features static-link-z3
- - name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled
- run: cargo test --manifest-path z3/Cargo.toml -vv --features 'static-link-z3 arbitrary-size-numeral'
+ cargo build --target=wasm32-unknown-emscripten -vv -p z3 -p z3-sys --features static-link-z3

.gitignore

@@ -2,3 +2,4 @@ target
 Cargo.lock
 *~
 .z3-trace
+.tmp

Cargo.toml

@@ -1,2 +1,2 @@
 [workspace]
-members = ["z3", "z3-sys"]
+members = ["z3", "z3-sys", "z3-sys-bindgen"]

z3-sys-bindgen/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "z3-sys-bindgen"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+bindgen = { version = "0.64", default-features = false, features = ["runtime"] }

z3-sys-bindgen/src/main.rs

@@ -0,0 +1,42 @@
+use std::{env, path::PathBuf};
+
+fn main() {
+ let args: Vec<String> = env::args().collect();
+ assert_eq!(args.len(), 2);
+ bindgen(PathBuf::from(&args[1]))
+}
+
+fn bindgen(z3_header: PathBuf) {
+ let header = z3_header.display().to_string();
+ #[cfg(target_os = "linux")]
+ let out_path = PathBuf::new().join("z3-sys").join("src").join("generated_linux");
+ #[cfg(target_os = "windows")]
+ let out_path = PathBuf::new().join("z3-sys").join("src").join("generated_windows");
+ #[cfg(target_os = "macos")]
+ let out_path = PathBuf::new().join("z3-sys").join("src").join("generated_macos");
+
+ for x in &[
+ "ast_kind",
+ "ast_print_mode",
+ "decl_kind",
+ "error_code",
+ "goal_prec",
+ "param_kind",
+ "parameter_kind",
+ "sort_kind",
+ "symbol_kind",
+ ] {
+ let enum_bindings = bindgen::Builder::default()
+ .header(&header)
+ .parse_callbacks(Box::new(bindgen::CargoCallbacks))
+ .generate_comments(false)
+ .rustified_enum(format!("Z3_{}", x))
+ .allowlist_type(format!("Z3_{}", x));
+
+ enum_bindings
+ .generate()
+ .expect("Unable to generate bindings")
+ .write_to_file(out_path.join(format!("{}.rs", x)))
+ .expect("Couldn't write bindings!");
+ }
+}

z3-sys/Cargo.toml

@@ -16,10 +16,10 @@ homepage = "https://github.com/prove-rs/z3.rs"
 repository = "https://github.com/prove-rs/z3.rs.git"
 
 [build-dependencies]
-bindgen = { version = "0.64.0", default-features = false, features = ["runtime"] }
 cmake = { version = "0.1.49", optional = true }
+ureq = "2.6.2"
+zip = "0.6"
 
 [features]
-# Enable this feature to statically link our own build of Z3, rather than
-# dynamically linking to the system's `libz3.so`.
-static-link-z3 = ["cmake"]
+static-link-z3 = ["cmake"] # Locally build and statically link a fresh Z3 build.
+dynamic-link-z3 = [] # Dynamically link the system's Z3 installation.