[PATCH] D54978: Move the SMT API to LLVM

2019-02-07 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. This commit is causing a build-break for our nightly cross compilers of arm and aarch64. The immediately preceding commit of D54977 does not break with the exact same invocation. The problem is our build machine (Ubuntu 18.04 LTS)

[PATCH] D54978: Move the SMT API to LLVM

2019-02-08 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. > From what I understand, setting `-DLLVM_ENABLE_Z3_SOLVER=OFF` is supposed to > work Hello @thakis, I have reduced it down to the minimal required flags on Ubuntu 18.04. I ran this on llvm-project SHA b0a227049fda9d0d229ea801ae77bf1b812f7328

[PATCH] D54978: Move the SMT API to LLVM

2019-02-08 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1390698 , @thakis wrote: > Thanks for the analysis. I think it's fine if you revert, given that. I'm running in to conflict dependency issues when attempting to revert rL353373 .

[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1394613 , @thakis wrote: > Got it now, sorry about being dense. No problem, I appreciate you looking into this. :) I hope to have some time in the next few days to help out and debug this further. Repository: rC

[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. The following patch: diff --git a/llvm/cmake/modules/CrossCompile.cmake b/llvm/cmake/modules/CrossCompile.cmake index bc3b210f018..0c30b88f80f 100644 --- a/llvm/cmake/modules/CrossCompile.cmake +++ b/llvm/cmake/modules/CrossCompile.cmake @@ -53,6 +53,7 @@

[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. I think I found why others are struggling to recreate this issue. I did not have the package `z3/bionic` installed. This provides the `/usr/bin/z3` executable which `llvm/cmake/modules/FindZ3.cmake` relies upon to determine the correct `Z3_VERSION_STRING`. If I

[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1395476 , @mikhail.ramalho wrote: > I'm wondering if we can remove the binary requirement all together: is it > possible to run a small program that would return EXIT_SUCCESS if the library > is the correct version?

[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1395288 , @ddcc wrote: > In D54978#1395268 , @brzycki wrote: > > > I think I found why others are struggling to recreate this issue. I did not > > have the package `z3/bionic`

[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. > perhaps something like this: > > if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/z3_version.h") > file(STRINGS "${Z3_INCLUDE_DIR }/z3_version.h" z3_version_str REGEX > "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"") > > string(REGEX REPLACE

[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1395562 , @mikhail.ramalho wrote: > Hi @brzycki, but isn't it exactly what we want? I mean, if we try to > cross-compile and it fails for any reason (non-native library, wrong > version), then Z3_FOUND shouldn't be

[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1396927 , @ddcc wrote: > The old `version.h` header isn't externally exposed, only the newer > `z3_version.h` header starting with version 4.8.1. I built a copy of 4.7.1 > from source, and I don't see it, so

[PATCH] D54978: Move the SMT API to LLVM

2019-02-11 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1392464 , @Szelethus wrote: > Shouldn't that be off by default? The default for `LLVM_ENABLE_Z3_SOLVER` depends entirely on what CMake detects from `find_package()`. Here is the relevant code in `llvm/CMakeLists.txt`:

[PATCH] D54978: Move the SMT API to LLVM

2019-02-11 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1393968 , @thakis wrote: > Do you understand why the default matters for you? You seem to explicitly > disable the setting, and you still get Z3 as part of your build. Did you make > a clean build dir before turning it

[PATCH] D54978: Move the SMT API to LLVM

2019-02-14 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. In D54978#1397354 , @ddcc wrote: > In D54978#1397316 , @mikhail.ramalho > wrote: > > > I just sent the first prototype of the solution. All the magic happens > > inside the

[PATCH] D54978: Move the SMT API to LLVM

2019-02-14 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. Here's my proposed logic as actual CMake code. @mikhail.ramalho if you can get your code to emit the version string I made a `TODO` placeholder for it in the 3rd block below. diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake index

[PATCH] D54978: Move the SMT API to LLVM

2019-02-11 Thread Brian Rzycki via Phabricator via cfe-commits
brzycki added a comment. > @brzycki, I can't reproduce your error. Maybe you're missing > `-DLLVM_ENABLE_Z3_SOLVER=OFF`? Hello @mikhail.ramalho, here are my exact reproduction steps. I just verified them about 5 minutes ago. # Setup Ubuntu's Z3 lsb_release -a No LSB modules are