diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 7b3aee31..fd6de90b 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -2,7 +2,7 @@ name: Rust on: push: - branches: [ master ] + branches: [ master , download_z3 ] pull_request: branches: [ master ] @@ -10,6 +10,8 @@ env: CARGO_INCREMENTAL: 0 CARGO_REGISTRIES_CRATES_IO_PROTOCOL: sparse RUSTFLAGS: "-D warnings" + Z3_RELEASE: 'z3-4.12.1' + RUST_BACKTRACE: 'full' jobs: check-formatting: @@ -20,26 +22,77 @@ jobs: run: cargo fmt -- --check build: - runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + os: [ubuntu-latest, windows-latest, macos-latest] + link: [download, build, system] + runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v3 - - name: Install Z3 - run: sudo apt-get install libz3-dev + 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: runner.os == 'Windows' + with: + version: "11.0" + directory: ${{ runner.temp }}/llvm + - name: install c++ runtime on windows + if: runner.os == 'Windows' + shell: bash + run: | + choco install vcredist2017 + echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV + - name: Uninstall Z3 on Linux for non-system builds + if: runner.os == 'Linux' && matrix.link != 'system' + run: sudo apt-get remove libz3-dev + - name: Setup homebrew (macOS) + if: runner.os == 'macOS' && matrix.link == 'system' + shell: bash + run: | + echo "/home/linuxbrew/.linuxbrew/bin:/home/linuxbrew/.linuxbrew/sbin" >> $GITHUB_PATH + - name: Install Z3 (macOS) + if: runner.os == 'macOS' && matrix.link == 'system' + shell: bash + run: (yes || true) | brew install z3 + + - name: Install Z3 on Windows for system builds + if: startsWith(matrix.os, 'windows-') && 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: Config rust for windows + if: matrix.os == 'windows-latest' + run: rustup set default-host x86_64-pc-windows-msvc + + - id: build-param + shell: bash + run: | + case "${{ matrix.link }}" in + "system" ) echo "param=" >> $GITHUB_OUTPUT ;; + "build" ) echo "param=--features force-build-z3" >> $GITHUB_OUTPUT ;; + "download" ) echo "param=--features static-link-z3" >> $GITHUB_OUTPUT ;; + esac - 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() }} + run: cargo build -vv --workspace --all-targets ${{ steps.build-param.outputs.param }} + # Avoid to run rustdoc tests due to toolchain bug (https://github.com/rust-lang/cargo/issues/8531) + - name: Run tests (non-Windows) + if: runner.os != 'Windows' + run: cargo test -vv --workspace ${{ steps.build-param.outputs.param }} + - name: Run tests (Windows) + if: runner.os == 'Windows' + run: cargo test -vv --workspace --tests ${{ steps.build-param.outputs.param }} + - name: Run tests with `arbitrary-size-numeral` enabled (non-Windows) + if: runner.os != 'Windows' + run: cargo test --manifest-path z3/Cargo.toml -vv --features=arbitrary-size-numeral ${{ steps.build-param.outputs.param }} + - name: Run tests with `arbitrary-size-numeral` enabled (Windows) + if: runner.os == 'Windows' + run: cargo test --manifest-path z3/Cargo.toml --tests -vv --features=arbitrary-size-numeral ${{ steps.build-param.outputs.param }} build_on_wasm: runs-on: ubuntu-latest @@ -63,38 +116,6 @@ jobs: source ~/emsdk/emsdk_env.sh cargo build --target=wasm32-unknown-emscripten -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@v3 - 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` and `z3` with statically linked Z3 - run: cargo build -vv --features static-link-z3 - - name: Test `z3-sys` and `z3` with statically linked Z3 - run: cargo test -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' - run_clippy: runs-on: ubuntu-latest steps: @@ -102,4 +123,4 @@ jobs: with: submodules: recursive - name: Run clippy - run: cargo clippy -vv --features static-link-z3 --all-targets \ No newline at end of file + run: cargo clippy -vv --features force-build-z3 --lib --tests \ No newline at end of file diff --git a/z3-sys/Cargo.toml b/z3-sys/Cargo.toml index bb2ec14b..572bdad0 100644 --- a/z3-sys/Cargo.toml +++ b/z3-sys/Cargo.toml @@ -18,8 +18,16 @@ repository = "https://github.com/prove-rs/z3.rs.git" [build-dependencies] bindgen = { version = "0.66.0", default-features = false, features = ["runtime"] } cmake = { version = "0.1.49", optional = true } +sha2 = { version = "~0.7.0", optional = true } +zip = { version = "~0.3.1", optional = true } +reqwest = { version = "0.11", features = ["blocking"], optional = true } [features] -# Enable this feature to statically link our own build of Z3, rather than +# Enable this feature to statically link Z3 library, rather than # dynamically linking to the system's `libz3.so`. -static-link-z3 = ["cmake"] +# If binary release of z3 is not available for the architecture, +# then fallback to 'force-build-z3'. +static-link-z3 = ["sha2", "zip", "reqwest", "cmake"] + +# Force to build z3 locally, which may reads to more efficiency. +force-build-z3 = ["static-link-z3"] diff --git a/z3-sys/build.rs b/z3-sys/build.rs index 010c1aeb..8a2379e4 100644 --- a/z3-sys/build.rs +++ b/z3-sys/build.rs @@ -4,13 +4,11 @@ const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER"; fn main() { #[cfg(feature = "static-link-z3")] - build_z3(); + let include_dir = prepare_z3(); println!("cargo:rerun-if-changed=build.rs"); - let header = if cfg!(feature = "static-link-z3") { - "z3/src/api/z3.h".to_string() - } else if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) { + let header = if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) { header_path } else { "wrapper.h".to_string() @@ -36,6 +34,12 @@ fn main() { .generate_comments(false) .rustified_enum(format!("Z3_{}", x)) .allowlist_type(format!("Z3_{}", x)); + + #[cfg(feature = "static-link-z3")] + { + enum_bindings = enum_bindings.clang_arg(&format!("-I{}", &include_dir)); + } + if env::var("TARGET").unwrap() == "wasm32-unknown-emscripten" { enum_bindings = enum_bindings.clang_arg(format!( "--sysroot={}/upstream/emscripten/cache/sysroot", @@ -51,7 +55,82 @@ fn main() { } #[cfg(feature = "static-link-z3")] -fn build_z3() { +fn prepare_z3() -> String { + // Z3 needs a C++ standard library. Customize which one we use with the + // `CXXSTDLIB` environment variable, if needed. + let cxx = match std::env::var("CXXSTDLIB") { + Ok(s) if s.is_empty() => None, + Ok(s) => Some(s), + Err(_) => { + let target = std::env::var("TARGET").unwrap(); + if target.contains("msvc") { + None + } else if target.contains("apple") + | target.contains("freebsd") + | target.contains("openbsd") + { + Some("c++".to_string()) + } else { + Some("stdc++".to_string()) + } + } + }; + println!("cargo:rerun-if-env-changed=CXXSTDLIB"); + + if let Some(cxx) = cxx { + println!("cargo:rustc-link-lib={}", cxx); + + // The following linker flags are needed for `cargo test` to compile + // test binaries. + #[cfg(all(target_os = "linux", target_arch = "x86_64"))] + { + let cxx_paths = [ + "/usr/lib/gcc/x86_64-linux-gnu/13", + "/usr/lib/gcc/x86_64-linux-gnu/12", + "/usr/lib/gcc/x86_64-linux-gnu/11", + "/usr/lib/gcc/x86_64-linux-gnu/10", + "/usr/lib/gcc/x86_64-linux-gnu/9", + "/usr/lib/gcc/x86_64-linux-gnu/8", + "/usr/lib/gcc/x86_64-linux-gnu/7", + "/usr/lib/x86_64-linux-gnu", + "/usr/lib64", + "/usr/lib", + ]; + + for path in cxx_paths { + if std::fs::read_dir(std::path::PathBuf::from(path)).is_ok() { + println!("cargo:rustc-link-arg=-Lnative={}", path); + } + } + println!("cargo:rustc-link-arg=-l{}", cxx); + } + } + + if cfg!(target_os = "windows") { + println!("cargo:rustc-link-lib=static=libz3"); + } else { + println!("cargo:rustc-link-lib=static=z3"); + } + #[cfg(not(feature = "force-build-z3"))] + if let Some(ret) = download_z3() { + // #[cfg(target_os = "windows")] + // { + // println!("cargo:rustc-link-lib=dylib=msvcp140"); + // println!("cargo:rustc-link-lib=dylib=msvcp140_1"); + // println!("cargo:rustc-link-lib=dylib=msvcp140_2"); + // println!("cargo:rustc-link-lib=dylib=msvcp140_atomic_wait"); + // println!("cargo:rustc-link-lib=dylib=msvcp140_codecvt_ids"); + // println!("cargo:rustc-link-lib=dylib=vcomp140"); + // println!("cargo:rustc-link-lib=dylib=vcruntime140"); + // println!("cargo:rustc-link-lib=dylib=vcruntime140_1"); + // } + return ret; + } + build_z3() +} + +#[cfg(feature = "static-link-z3")] +fn build_z3() -> String { let mut cfg = cmake::Config::new("z3"); cfg // Don't build `libz3.so`, build `libz3.a` instead. @@ -73,26 +152,6 @@ fn build_z3() { let dst = cfg.build(); - // Z3 needs a C++ standard library. Customize which one we use with the - // `CXXSTDLIB` environment variable, if needed. - let cxx = match std::env::var("CXXSTDLIB") { - Ok(s) if s.is_empty() => None, - Ok(s) => Some(s), - Err(_) => { - let target = std::env::var("TARGET").unwrap(); - if target.contains("msvc") { - None - } else if target.contains("apple") - | target.contains("freebsd") - | target.contains("openbsd") - { - Some("c++".to_string()) - } else { - Some("stdc++".to_string()) - } - } - }; - let mut found_lib_dir = false; for lib_dir in &[ "lib", @@ -118,13 +177,132 @@ fn build_z3() { "Should have found the lib directory for our built Z3" ); - if cfg!(target_os = "windows") { - println!("cargo:rustc-link-lib=static=libz3"); - } else { - println!("cargo:rustc-link-lib=static=z3"); + "z3/src/api".to_string() +} + +#[cfg(feature = "static-link-z3")] +#[cfg(not(feature = "force-build-z3"))] +fn download_z3() -> Option { + use reqwest::blocking; + use sha2::{Digest, Sha256}; + use std::ffi::OsStr; + use std::fs::File; + use std::io::{Cursor, Read, Write}; + use std::path::{Path, PathBuf}; + use zip::ZipArchive; + fn download(url: &str, sha256: &str) -> Result, String> { + let buf = (|| -> reqwest::Result<_> { + let response = blocking::get(url)?.error_for_status()?; + Ok(response.bytes()?.iter().cloned().collect::>()) + })() + .map_err(|e| e.to_string())?; + if sha256 != "PASS" { + let hash = Sha256::digest(&buf); + if format!("{:x}", hash) != sha256 { + return Err("Hash check failed".to_string()); + } + } + Ok(buf) } - if let Some(cxx) = cxx { - println!("cargo:rustc-link-lib={}", cxx); + fn get_archive_url() -> Option<(String, String)> { + if cfg!(target_os = "linux") && cfg!(target_arch = "x86_64") { + Some(( + "https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.35.zip".into(), + "c5360fd157b0f861ec8780ba3e51e2197e9486798dc93cd878df69a4b0c2b7c5".into(), + )) + } else if cfg!(target_os = "macos") && cfg!(target_arch = "x86_64") { + Some(( + "https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-osx-10.16.zip".into(), + "7601f844de6d906235140d0f76cca58be7ac716f3e2c29c35845aa24b24f73b9".into(), + )) + } else if cfg!(target_os = "macos") && cfg!(target_arch = "aarch64") { + Some(( + "https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-arm64-osx-11.0.zip".into(), + "91664cb7c10279e533f7ec568d63e0d04ada352217a6710655d41739c4ea1fc8".into(), + )) + } else if cfg!(target_os = "windows") + && cfg!(target_arch = "x86_64") + && cfg!(target_env = "msvc") + { + Some(( + "https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-win.zip" + .into(), + "ce2d658d007c4f5873d2279bd031d4e72500b388e1ef2d716bd5f86af19b20d2".into(), + )) + } else if cfg!(target_os = "windows") + && cfg!(target_arch = "x86") + && cfg!(target_env = "msvc") + { + Some(( + "https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x86-win.zip" + .into(), + "1fbe8e2a87f42ca6f3348b8c48a1ffcd8fc376ac3144c9b588a5452de01ca2ef".into(), + )) + } else { + None + } + } + + fn find_origin_dir_and_get_successor_path(path: &Path, name: &OsStr) -> Option { + let segs = path.parent()?.iter().collect::>(); + segs.iter() + .enumerate() + .find(|seg| *seg.1 == name) + .map(|(i, _)| { + segs[segs.len() - i + 1..] + .iter() + .fold(PathBuf::new(), |path, seg| path.join(seg)) + }) } + + fn write_lib_to_dir(out_dir: &Path) -> Option<()> { + let (url, hash) = get_archive_url()?; + let archive = download(&url, &hash).unwrap(); + let mut archive = ZipArchive::new(Cursor::new(archive)).unwrap(); + for i in 0..archive.len() { + let mut file = archive.by_index(i).unwrap(); + let path = PathBuf::from(file.name()); + let out_dir = if let Some(succ) = + find_origin_dir_and_get_successor_path(&path, OsStr::new("bin")) + { + Some(out_dir.to_path_buf().join(Path::new("lib")).join(succ)) + } else if let Some(succ) = + find_origin_dir_and_get_successor_path(&path, OsStr::new("include")) + { + Some(out_dir.to_path_buf().join(Path::new("include")).join(succ)) + } else { + None + }; + + if let Some(mut out_dir) = out_dir { + let mut buf = Vec::with_capacity(file.size() as usize); + file.read_to_end(&mut buf).unwrap(); + std::fs::create_dir_all(&out_dir).unwrap(); + out_dir.push(path.file_name().unwrap()); + let mut outfile = File::create(&out_dir).unwrap(); + outfile.write_all(&buf).unwrap(); + } + } + Some(()) + } + + let out_dir = PathBuf::from(env::var("OUT_DIR").unwrap()); + write_lib_to_dir(&out_dir)?; + println!( + "cargo:rustc-link-search=native={}", + out_dir + .clone() + .join(&PathBuf::from("lib")) + .to_str() + .unwrap() + ); + + Some( + std::fs::canonicalize(out_dir.clone().join(&PathBuf::from("include"))) + .unwrap() + .to_str() + .unwrap() + .to_string(), + ) } diff --git a/z3/Cargo.toml b/z3/Cargo.toml index 483ed66f..f19d219e 100644 --- a/z3/Cargo.toml +++ b/z3/Cargo.toml @@ -17,10 +17,15 @@ repository = "https://github.com/prove-rs/z3.rs.git" default = [] arbitrary-size-numeral = ["num"] -# Enable this feature to statically link our own build of Z3, rather than +# Enable this feature to statically link Z3 library, rather than # dynamically linking to the system's `libz3.so`. +# If binary release of z3 is not available for the architecture, +# then fallback to 'force-build-z3'. static-link-z3 = ["z3-sys/static-link-z3"] +# Force to build z3 locally, which may reads to more efficiency. +force-build-z3 = ["z3-sys/force-build-z3"] + [dependencies] log = "0.4" diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 7efaea45..3028a3e9 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -1221,7 +1221,7 @@ fn test_tactic_fail() { let tactic = Tactic::new(&ctx, "fail"); let apply_results = tactic.apply(&goal, Some(¶ms)); - assert!(matches!(apply_results, Err(_))); + assert!(apply_results.is_err()); } #[test]