prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Build fails but used to work #303

Closed dragazo closed 1 month ago

dragazo commented 1 month ago

I've been using this crate for over a year without issue, even on this same exact machine. But all of a sudden when I try to build my projects I get the following pointer size error:

error: failed to run custom build command for `z3-sys v0.8.1`

Caused by:
  process didn't exit successfully: `/home/devin/Desktop/dom-graph-theory/det-set/target/debug/build/z3-sys-24c358aa7224cb95/build-script-build` (exit status: 101)
  --- stdout
  cargo:rerun-if-changed=build.rs
  cargo:rerun-if-env-changed=Z3_SYS_Z3_HEADER
  cargo:rerun-if-changed=wrapper.h
  cargo:rerun-if-env-changed=TARGET
  cargo:rerun-if-env-changed=BINDGEN_EXTRA_CLANG_ARGS_x86_64-unknown-linux-gnu
  cargo:rerun-if-env-changed=BINDGEN_EXTRA_CLANG_ARGS_x86_64_unknown_linux_gnu
  cargo:rerun-if-env-changed=BINDGEN_EXTRA_CLANG_ARGS

  --- stderr
  /usr/include/x86_64-linux-gnu/gnu/stubs.h:7:11: fatal error: 'gnu/stubs-32.h' file not found
  thread 'main' panicked at /home/devin/.cargo/registry/src/index.crates.io-6f17d22bba15001f/bindgen-0.66.1/lib.rs:881:13:
  assertion `left == right` failed: "x86_64-unknown-linux-gnu" "x86_64-unknown-linux-gnu"
    left: 4
   right: 8
  note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I get this same error with and without the static-link-z3 feature flag. It seems to either be finding a 32-bit installation of Z3 (which should not be the case) or is trying to use a 32-bit version of clang (but I tested that the clang command is defaulted to 64-bit). And the strangest thing is that my code was running just fine two weeks ago when I last used it without change (on this same machine) and without even cleaning compile artifacts...

Does anyone have any advice on how to get this back to working?

dragazo commented 1 month ago

I've uninstalled and reinstalled the latest version of Z3 (built from source for my 64-bit target), but the issue persists. The fact that it's mentioning it failed to find gnu/stubs-32.h seems telling, because that's only included on 32-bit targets (which mine is not)...

Content of stubs.h:

#if !defined __x86_64__
# include <gnu/stubs-32.h>
#endif
#if defined __x86_64__ && defined __LP64__
# include <gnu/stubs-64.h>
#endif
#if defined __x86_64__ && defined __ILP32__
# include <gnu/stubs-x32.h>
#endif
dragazo commented 1 month ago

Digging into it a bit more, I found out the target arch bindgen was deducing was riscv32-esp-unknown-elf, which was installed via espup (toolchain manager for espressif chipset targets). After removing the esp targets, I got a lookup error for libclang.so, which somehow wasn't in path. I'm not certain how this happened, as I've been using both Z3 and espup together without issue in the past. My guess is that a recent espup update cycle broke some symlinks that were being used for libclang. The final fix was explicitly setting LIBCLANG_PATH in my .bashrc to point to the real local target version of libclang.