[PATCH] D54978: Move the SMT API to LLVM

NoQ added inline comments. Comment at: cfe/trunk/CMakeLists.txt:453 +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT) message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") endif() This message needs to be updated :) Re

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. In D54978#1457318 , @mikhail.ramalho wrote: > In D54978#1447107 , @gou4shi1 wrote: > > > My own out-of-tree pass `#include ` and use cmake's > > `add_llvm_library` to compile it into a `.

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. In D54978#1447107 , @gou4shi1 wrote: > My own out-of-tree pass `#include ` and use cmake's > `add_llvm_library` to compile it into a `.so` > However, `opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll` fails: > `opt:

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. My own out-of-tree pass `#include ` and use cmake's `add_llvm_library` to compile it into a `.so` However, `opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll` fails: `opt: symbol lookup error: Passes/libStackPasses.so: undefined symbol: _ZN4llvm14CreateZ3SolverEv` (

[PATCH] D54978: Move the SMT API to LLVM

aprantl added a comment. Thanks! The problem with these methods is that LLVM_DUMP_METHOD forces the function to be emitted even if it is not used and Clang modules without local submodule visibility will implicitly include all header files in a module, which will then cause the missing symbol

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. In D54978#1442493 , @aprantl wrote: > I'm afraid this broke some bots that build with `LLVM_ENABLE_MODULES=1`. > > For example: > > http://green.lab.llvm.org/green/view/LLDB/job/lldb-cmake/22411/consoleFull#710926295dd1929e

[PATCH] D54978: Move the SMT API to LLVM

aprantl added a comment. I'm afraid this broke some bots that build with `LLVM_ENABLE_MODULES=1`. For example: http://green.lab.llvm.org/green/view/LLDB/job/lldb-cmake/22411/consoleFull#710926295dd1929ea-7054-4089-b7ef-4624c3781fa4 Undefined symbols for architecture x86_64: "llvm::errs()"

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. > ! In D54978#1441547 , > @mikhail.ramalho wrote: > You can get the sort size by calling getBitvectorSortSize(). found, thx CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 _

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. > ! In D54978#1441417 , > @mikhail.ramalho wrote: > Sure, I'll create a new revision with the added functions tonight. I am very happy with your quickly reply. btw, `Z3_get_bv_sort_size` is also needed :) CHANGES SINCE LAST AC

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. In D54978#1441453 , @gou4shi1 wrote: > > ! In D54978#1441417 , > > @mikhail.ramalho wrote: > > Sure, I'll create a new revision with the added functions tonight. > > I am very happ

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. > ! In D54978#1440464 , @ddcc wrote: > > Do you know if this configuration builds fine now? It's working fine now, I'll push it later today. > ! In D54978#1441355 , @gou4shi1 > wr

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. @mikhail.ramalho Can you plz add some wrappers of overflow predicates like Z3_mk_bvadd_no_overflow, Z3_mk_bvadd_no_underflow, ... to SMTAPI.h and Z3Solver.cpp? It could help me, thanks! CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://review

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1433646 , @mikhail.ramalho wrote: > To fix that, I changed the script slightly: we first try to dinamically get > the Z3's version, if we fail and we are cross compiling, then we try to parse > the headers. Right now, it

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho marked an inline comment as done. mikhail.ramalho added a comment. Fixed. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho updated this revision to Diff 191305. mikhail.ramalho added a comment. Fix copy-and-paste error. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 Files: clang/CMakeLists.txt clang/cmake/modules/FindZ3.cmake clang/include/cla

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. Hi all, I just updated the CMake script to get the version by parsing the header, however, I just found a potential issue in the previous approach: if we have incompatible libs in the path (32-bits libs when compiling in 64-bit mode) the CMake config will succe

[PATCH] D54978: Move the SMT API to LLVM

ddcc added inline comments. Comment at: llvm/cmake/modules/FindZ3.cmake:92 + + set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_MAJOR}) + unset(z3_version_str) Should be ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD_NUMBER} CHANGES SINCE LAST ACTION https://reviews.

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho updated this revision to Diff 191152. mikhail.ramalho added a comment. Updated script to parse Z3's headers and changed the workflow to handle cross compilation cases. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 Files: cla

[PATCH] D54978: Move the SMT API to LLVM

delcypher added a comment. In D54978#1432178 , @ddcc wrote: > In D54978#1431935 , @delcypher wrote: > > > Would one of you be able to file a bug against Z3 to fix this? I am no > > longer in a position to contribut

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho updated this revision to Diff 191095. mikhail.ramalho added a comment. Fixes: - `FindZ3.cmake` format . - Wrong `SMTExpr` namespace in `SMTConstraintManager.h`. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 Files: clang/CMak

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1431935 , @delcypher wrote: > Would one of you be able to file a bug against Z3 to fix this? I am no longer > in a position to contribute to Z3 so I can't do this. I've opened https://github.com/Z3Prover/z3/issues/2184 .

[PATCH] D54978: Move the SMT API to LLVM

delcypher added a comment. In D54978#1431430 , @mikhail.ramalho wrote: > Hi all, > > Sorry for the massive delay, but I just updated the `FindZ3` script to > retrieve the version from the lib. I changed it to use `try_run` instead of > `try_compile` so

[PATCH] D54978: Move the SMT API to LLVM

delcypher added a comment. In D54978#1431788 , @ddcc wrote: > The only relevant commit that I can find is > https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 > , but it first landed in z3 4.6.0. It looks like it's specific to

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1431430 , @mikhail.ramalho wrote: > 2. Instead of parsing `Z3_FULL_VERSION`, we can parse `Z3_MAJOR_VERSION`, > `Z3_MINOR_VERSION` and `Z3_BUILD_NUMBER` which are also available in the same > header. Sounds like this mi

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. In D54978#1431788 , @ddcc wrote: > The only relevant commit that I can find is > https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 > , but it first landed in z3 4.6.0. It looks like it's speci

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. The only relevant commit that I can find is https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 , but it first landed in z3 4.6.0. It looks like it's specific to CMake though, so is it different if you use the python build? I haven't tried the CM

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. In D54978#1431786 , @ddcc wrote: > In D54978#1431430 , @mikhail.ramalho > wrote: > > > Sorry for the massive delay, but I just updated the `FindZ3` script to > > retrieve the versi

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1431430 , @mikhail.ramalho wrote: > Sorry for the massive delay, but I just updated the `FindZ3` script to > retrieve the version from the lib. I changed it to use `try_run` instead of > `try_compile` so we can get the ve

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. Hi all, Sorry for the massive delay, but I just updated the `FindZ3` script to retrieve the version from the lib. I changed it to use `try_run` instead of `try_compile` so we can get the version number. I tried to use @brzycki code to get the version from the h

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho updated this revision to Diff 190893. mikhail.ramalho added a comment. Update Z3 script to use cmake's `try_run` in order to retrieve the version from the lib. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 Files: clang/CMake

[PATCH] D54978: Move the SMT API to LLVM

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 5c6d3f

[PATCH] D54978: Move the SMT API to LLVM

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 `CHECK_CXX_SOUR

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1397316 , @mikhail.ramalho wrote: > I just sent the first prototype of the solution. All the magic happens inside > the `CHECK_CXX_SOURCE_RUNS` call. I think hardcoding the version into the binary is too brittle. Instead

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. Hi guys, I just sent the first prototype of the solution. All the magic happens inside the `CHECK_CXX_SOURCE_RUNS` call. There is still one thing to do: currently, the program is hard-coded to check for version 4.7.1. We should either get it from the `find_pack

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho updated this revision to Diff 186757. mikhail.ramalho added a comment. Update FindZ3.cmake to do a runtime check of the version. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 Files: clang/CMakeLists.txt clang/cmake/modules/

[PATCH] D54978: Move the SMT API to LLVM

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 unfortunate

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1396403 , @brzycki wrote: > That is almost exactly what I was thinking about this morning. I'd prefer the > following since it's more robust for older versions: The old `version.h` header isn't externally exposed, only th

[PATCH] D54978: Move the SMT API to LLVM

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 set

[PATCH] D54978: Move the SMT API to LLVM

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 "^.*Z3_FULL_VERSI

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1395425 , @brzycki wrote: > This works for everything I could throw at it. If you think it's reasonable I > can open another ticket and have the code reviewed as a separate fix. Sounds good to me, although I think it'd be

[PATCH] D54978: Move the SMT API to LLVM

thakis added a comment. In D54978#1395136 , @brzycki wrote: > 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/Cr

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. In D54978#1395561 , @brzycki wrote: > In D54978#1395476 , @mikhail.ramalho > wrote: > > > I'm wondering if we can remove the binary requirement all together: is it > > possible to

[PATCH] D54978: Move the SMT API to LLVM

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

mikhail.ramalho added a comment. Looks like my last email got lost: 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? Something like: #include int main() {

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. I found a `CHECK_CXX_SOURCE_COMPILES`, which seems to be used in a number of places in LLVM. I'll give it a try. Repository: rC Clang CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978

Re: [PATCH] D54978: Move the SMT API to LLVM

Hi, Thank you for the discussion, I was finally able to reproduce the error. > Hello @ddcc. > I agree with your reasoning here and developed a patch based on this line > of thought: > > diff --git a/llvm/cmake/modules/FindZ3.cmake > b/llvm/cmake/modules/FindZ3.cmake > index 5c6d3f0b427..b213

[PATCH] D54978: Move the SMT API to LLVM

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` ins

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. 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` installed. This provides the `/usr/bin/z3` > executable which `llvm/cmake/modules/FindZ

[PATCH] D54978: Move the SMT API to LLVM

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 perform

[PATCH] D54978: Move the SMT API to LLVM

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 @@ funct

[PATCH] D54978: Move the SMT API to LLVM

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 C

[PATCH] D54978: Move the SMT API to LLVM

thakis added a comment. Herald added a subscriber: jdoerfert. >> If so, I don't understand why the default setting is important to you and >> why this doesn't work for you. (I don't disagree with the default being off, >> I'm just confused why things don't work for you.) > > As I have stated se

[PATCH] D54978: Move the SMT API to LLVM

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

thakis added a comment. > In D54978#1393552 , @ddcc wrote: > >> The likely reason for this versioning problem is that the current versioning >> implementation in FindZ3.cmake is best-effort only. > > > Thank you @ddcc for this explanation. If that's the

[PATCH] D54978: Move the SMT API to LLVM

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

ddcc added subscribers: delcypher, ddcc. ddcc added a comment. The likely reason for this versioning problem is that the current versioning implementation in FindZ3.cmake is best-effort only: among other conditions, if the z3 binary is available, it will execute it and parse out the version numb

[PATCH] D54978: Move the SMT API to LLVM

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 available

[PATCH] D54978: Move the SMT API to LLVM

Szelethus added a comment. Shouldn't that be off by default? Repository: rC Clang CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://li

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. @brzycki, I can't reproduce your error. Maybe you're missing `-DLLVM_ENABLE_Z3_SOLVER=OFF`? $ cmake -GNinja ../llvm -DLLVM_ENABLE_PROJECTS=clang -DBUILD_SHARED_LIBS=ON -DCMAKE_INSTALL_PREFIX=/home/mgadelha/myclang -DCMAKE_LINKER=/usr/bin/ld.gold -DLLVM_ENABLE

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho reopened this revision. mikhail.ramalho added a comment. This revision is now accepted and ready to land. Reopening the revision as it was reverted. Repository: rC Clang CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 __

[PATCH] D54978: Move the SMT API to LLVM

Szelethus added a comment. In D54978#1391785 , @thakis wrote: > In D54978#1391436 , @mikhail.ramalho > wrote: > > > Hi everyone, I just saw your messages and reverted the commits. > > > > Sorry for the inconvenienc

[PATCH] D54978: Move the SMT API to LLVM

thakis added a comment. In D54978#1391436 , @mikhail.ramalho wrote: > Hi everyone, I just saw your messages and reverted the commits. > > Sorry for the inconvenience, but for some reason I didn't get any email from > the bots. Could you send me the link

[PATCH] D54978: Move the SMT API to LLVM

mikhail.ramalho added a comment. Hi everyone, I just saw your messages and reverted the commits. Sorry for the inconvenience, but for some reason I didn't get any email from the bots. Could you send me the link with the failure? @brzycki, I'm using Ubuntu 18.04.2 and I'll try to reproduce the e

[PATCH] D54978: Move the SMT API to LLVM

george.karpenkov added a comment. > There is at least one other conflicting commit rL353465 > on top of this code already. Sorry about that. I think it would be fine to revert both or to replay the other commit on top of reverted version of this one. @mikhai

[PATCH] D54978: Move the SMT API to LLVM

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 . Ther

[PATCH] D54978: Move the SMT API to LLVM

thakis added a comment. Thanks for the analysis. I think it's fine if you revert, given that. Repository: rC Clang CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 ___ cfe-commits mailing list cfe-

[PATCH] D54978: Move the SMT API to LLVM

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

thakis added a comment. In D54978#1389110 , @brzycki wrote: > 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 th

[PATCH] D54978: Move the SMT API to LLVM

thakis added a comment. In D54978#1389260 , @shakeel.mahate wrote: > The ninja build also fails That's not the ninja build, that's the GN build. If you use that, please read llvm/utils/gn/README.rst. If something like this happens, it's on you (and ot

[PATCH] D54978: Move the SMT API to LLVM

george.karpenkov added a comment. @mikhail.ramalho could you revert then? In general, we should not use Z3 unless it's explicitly requested. Repository: rC Clang CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 __

[PATCH] D54978: Move the SMT API to LLVM

shakeel.mahate added a comment. The ninja build also fails ninja -C out/gn ninja: Entering directory `out/gn' [1/3182] ACTION //clang/test:lit_site_cfg(//llvm/utils/gn/build/toolchain:unix) FAILED: gen/clang/test/lit.site.cfg.py python ../../llvm/utils/gn/build/write_cmake_config.py -o gen/clan

[PATCH] D54978: Move the SMT API to LLVM

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) insta

[PATCH] D54978: Move the SMT API to LLVM

lebedev.ri added subscribers: mehdi_amini, lebedev.ri. lebedev.ri added a comment. Looks like this (all all other related Z3 reviews - D54975 , D54976 , D54977 ) review has completely omitted cfe-c

[PATCH] D54978: Move the SMT API to LLVM

This revision was automatically updated to reflect the committed changes. Closed by commit rC353373: Move the SMT API to LLVM (authored by mramalho, committed by ). Herald added a project: clang. Herald added a subscriber: cfe-commits. Changed prior to commit: https://reviews.llvm.org/D54978?vs