Skip to content

Commit 54babda

Browse files
yasuo-ozuyasuo-ozu
committed
Implement static-link-z3 and download-z3 flag
1 parent 18a5efd commit 54babda

File tree

5 files changed

+290
-85
lines changed

5 files changed

+290
-85
lines changed

‎.github/workflows/rust.yml

Lines changed: 71 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,16 @@ name: Rust
22

33
on:
44
push:
5-
branches: [ master ]
5+
branches: [ master , download_z3 ]
66
pull_request:
77
branches: [ master ]
88

99
env:
1010
CARGO_INCREMENTAL: 0
1111
CARGO_REGISTRIES_CRATES_IO_PROTOCOL: sparse
1212
RUSTFLAGS: "-D warnings"
13+
Z3_RELEASE: 'z3-4.12.1'
14+
RUST_BACKTRACE: 'full'
1315

1416
jobs:
1517
check-formatting:
@@ -20,26 +22,77 @@ jobs:
2022
run: cargo fmt -- --check
2123

2224
build:
23-
runs-on: ubuntu-latest
25+
strategy:
26+
fail-fast: false
27+
matrix:
28+
os: [ubuntu-latest, windows-latest, macos-latest]
29+
link: [download, build, system]
30+
runs-on: ${{ matrix.os }}
2431
steps:
2532
- uses: actions/checkout@v3
26-
- name: Install Z3
27-
run: sudo apt-get install libz3-dev
33+
with:
34+
submodules: recursive
35+
- name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797
36+
uses: KyleMayes/install-llvm-action@v1
37+
if: runner.os == 'Windows'
38+
with:
39+
version: "11.0"
40+
directory: ${{ runner.temp }}/llvm
41+
- name: install c++ runtime on windows
42+
if: runner.os == 'Windows'
43+
shell: bash
44+
run: |
45+
choco install vcredist2017
46+
echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
47+
- name: Uninstall Z3 on Linux for non-system builds
48+
if: runner.os == 'Linux' && matrix.link != 'system'
49+
run: sudo apt-get remove libz3-dev
50+
- name: Setup homebrew (macOS)
51+
if: runner.os == 'macOS' && matrix.link == 'system'
52+
shell: bash
53+
run: |
54+
echo "/home/linuxbrew/.linuxbrew/bin:/home/linuxbrew/.linuxbrew/sbin" >> $GITHUB_PATH
55+
- name: Install Z3 (macOS)
56+
if: runner.os == 'macOS' && matrix.link == 'system'
57+
shell: bash
58+
run: (yes || true) | brew install z3
59+
60+
- name: Install Z3 on Windows for system builds
61+
if: startsWith(matrix.os, 'windows-') && matrix.link == 'system'
62+
run: |
63+
mkdir .tmp
64+
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"
65+
tar -xf ".tmp/${env:Z3_RELEASE}-x64-win.zip" -C ".tmp"
66+
echo "${PWD}\.tmp\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_PATH
67+
echo "LIB=${PWD}\.tmp\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_ENV
68+
echo "Z3_SYS_Z3_HEADER=${PWD}\.tmp\${env:Z3_RELEASE}-x64-win\include\z3.h" >> $env:GITHUB_ENV
69+
- name: Config rust for windows
70+
if: matrix.os == 'windows-latest'
71+
run: rustup set default-host x86_64-pc-windows-msvc
72+
73+
- id: build-param
74+
shell: bash
75+
run: |
76+
case "${{ matrix.link }}" in
77+
"system" ) echo "param=" >> $GITHUB_OUTPUT ;;
78+
"build" ) echo "param=--features force-build-z3" >> $GITHUB_OUTPUT ;;
79+
"download" ) echo "param=--features static-link-z3" >> $GITHUB_OUTPUT ;;
80+
esac
2881
- name: Build
29-
run: cargo build -vv --all
30-
# XXX: Ubuntu's Z3 package seems to be missing some symbols, like
31-
# `Z3_mk_pbeq`, leading to linker errors. Just ignore this, I guess, until
32-
# we figure out how to work around it. At least we have the
33-
# statically-linked Z3 tests below...
34-
if: ${{ success() || failure() }}
35-
- name: Run tests
36-
run: cargo test -vv --all
37-
# See above.
38-
if: ${{ success() || failure() }}
39-
- name: Run tests with `arbitrary-size-numeral` enabled
40-
run: cargo test --manifest-path z3/Cargo.toml -vv --features arbitrary-size-numeral
41-
# See above.
42-
if: ${{ success() || failure() }}
82+
run: cargo build -vv --workspace --all-targets ${{ steps.build-param.outputs.param }}
83+
# Avoid to run rustdoc tests due to toolchain bug (https://github.com/rust-lang/cargo/issues/8531)
84+
- name: Run tests (non-Windows)
85+
if: runner.os != 'Windows'
86+
run: cargo test -vv --workspace ${{ steps.build-param.outputs.param }}
87+
- name: Run tests (Windows)
88+
if: runner.os == 'Windows'
89+
run: cargo test -vv --workspace --tests ${{ steps.build-param.outputs.param }}
90+
- name: Run tests with `arbitrary-size-numeral` enabled (non-Windows)
91+
if: runner.os != 'Windows'
92+
run: cargo test --manifest-path z3/Cargo.toml -vv --features=arbitrary-size-numeral ${{ steps.build-param.outputs.param }}
93+
- name: Run tests with `arbitrary-size-numeral` enabled (Windows)
94+
if: runner.os == 'Windows'
95+
run: cargo test --manifest-path z3/Cargo.toml --tests -vv --features=arbitrary-size-numeral ${{ steps.build-param.outputs.param }}
4396

4497
build_on_wasm:
4598
runs-on: ubuntu-latest
@@ -63,38 +116,6 @@ jobs:
63116
source ~/emsdk/emsdk_env.sh
64117
cargo build --target=wasm32-unknown-emscripten -vv --features static-link-z3
65118
66-
build_z3_statically:
67-
strategy:
68-
matrix:
69-
build: [linux, macos, windows]
70-
include:
71-
- build: linux
72-
os: ubuntu-latest
73-
- build: macos
74-
os: macos-latest
75-
- build: windows
76-
os: windows-latest
77-
runs-on: ${{ matrix.os }}
78-
steps:
79-
- uses: actions/checkout@v3
80-
with:
81-
submodules: recursive
82-
- name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797
83-
uses: KyleMayes/install-llvm-action@v1
84-
if: matrix.os == 'windows-latest'
85-
with:
86-
version: "11.0"
87-
directory: ${{ runner.temp }}/llvm
88-
- name: Set LIBCLANG_PATH
89-
run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
90-
if: matrix.os == 'windows-latest'
91-
- name: Build `z3-sys` and `z3` with statically linked Z3
92-
run: cargo build -vv --features static-link-z3
93-
- name: Test `z3-sys` and `z3` with statically linked Z3
94-
run: cargo test -vv --features static-link-z3
95-
- name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled
96-
run: cargo test --manifest-path z3/Cargo.toml -vv --features 'static-link-z3 arbitrary-size-numeral'
97-
98119
run_clippy:
99120
runs-on: ubuntu-latest
100121
steps:

‎z3-sys/Cargo.toml

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,16 @@ repository = "https://github.com/prove-rs/z3.rs.git"
1818
[build-dependencies]
1919
bindgen = { version = "0.66.0", default-features = false, features = ["runtime"] }
2020
cmake = { version = "0.1.49", optional = true }
21+
sha2 = { version = "~0.7.0", optional = true }
22+
zip = { version = "~0.3.1", optional = true }
23+
reqwest = { version = "0.11", features = ["blocking"], optional = true }
2124

2225
[features]
23-
# Enable this feature to statically link our own build of Z3, rather than
26+
# Enable this feature to statically link Z3 library, rather than
2427
# dynamically linking to the system's `libz3.so`.
25-
static-link-z3 = ["cmake"]
28+
# If binary release of z3 is not available for the architecture,
29+
# then fallback to 'force-build-z3'.
30+
static-link-z3 = ["sha2", "zip", "reqwest", "cmake"]
31+
32+
# Force to build z3 locally, which may reads to more efficiency.
33+
force-build-z3 = ["static-link-z3"]

0 commit comments

Comments
 (0)