[PATCH] D54978: Move the SMT API to LLVM

2019-04-07 Thread Artem Dergachev via Phabricator via cfe-commits
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 :)


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-04-06 Thread guangqing.chen via Phabricator via cfe-commits
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 `.so`
> >  However, `opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll` fails:
> >  `opt: symbol lookup error: Passes/libStackPasses.so: undefined symbol: 
> > _ZN4llvm14CreateZ3SolverEv`
> >  (c++filt: `llvm::CreateZ3Solver()`)
> >  If I move the content of `Z3Solver.cpp` into another file of 
> > `llvm/Support` (like `llvm/Support/raw_ostream.cpp`)
> >  everything works.
>
>
> I can't reproduce the error, can you send me a small example?


I build llvm with `cmake -DCMAKE_BUILD_TYPE=Debug -DLLVM_TARGETS_TO_BUILD=X86 
-DLLVM_ENABLE_PROJECTS=clang  ../llvm`
I have make a mini reproduce example at 
https://github.com/gou4shi1/mini-repro-pass
you can build this example with `mkdir build && cd build && cmake 
-DCMAKE_BUILD_TYPE=Debug .. && make`
you can run this example with `opt -load-pass-plugin=t/t.so 
-passes="t" ../test/add100.ll`


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-04-06 Thread Mikhail Ramalho via Phabricator via cfe-commits
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: symbol lookup error: Passes/libStackPasses.so: undefined symbol: 
> _ZN4llvm14CreateZ3SolverEv`
>  (c++filt: `llvm::CreateZ3Solver()`)
>  If I move the content of `Z3Solver.cpp` into another file of `llvm/Support` 
> (like `llvm/Support/raw_ostream.cpp`)
>  everything works.


I can't reproduce the error, can you send me a small example?


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-28 Thread guangqing.chen via Phabricator via cfe-commits
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`
(c++filt: `llvm::CreateZ3Solver()`)
If I move the content of `Z3Solver.cpp` into another file of `llvm/Support` 
(like `llvm/Support/raw_ostream.cpp`)
everything works.


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-26 Thread Adrian Prantl via Phabricator via cfe-commits
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 error.


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-26 Thread Mikhail Ramalho via Phabricator via cfe-commits
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#710926295dd1929ea-7054-4089-b7ef-4624c3781fa4
>
>   Undefined symbols for architecture x86_64:
> "llvm::errs()", referenced from:
> llvm::SMTExpr::dump() const in 
> liblldbDebugserverCommon.a(RNBSocket.cpp.o)
> llvm::SMTSolver::dump() const in 
> liblldbDebugserverCommon.a(RNBSocket.cpp.o)
> llvm::SMTSort::dump() const in 
> liblldbDebugserverCommon.a(RNBSocket.cpp.o)
> llvm::SMTExpr::dump() const in 
> liblldbDebugserverCommon.a(SocketAddress.cpp.o)
> llvm::SMTSolver::dump() const in 
> liblldbDebugserverCommon.a(SocketAddress.cpp.o)
> llvm::SMTSort::dump() const in 
> liblldbDebugserverCommon.a(SocketAddress.cpp.o)
>
>
> Long story short: You can't have an LLVM_DUMP_METHOD defined inline inside of 
> a module.
>
> One way to fix this would be to move the function body of the various
>
>   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
>
>
> functions into .cpp files.


Unfortunately, I was not able to reproduce the bug locally (when I enable 
modules, clang complains about some `std::shared_ptr`), 
however, I just pushed r356994 and I'll keep an eye on the bot.

Thanks for the report.


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-25 Thread Adrian Prantl via Phabricator via cfe-commits
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()", referenced from:
llvm::SMTExpr::dump() const in 
liblldbDebugserverCommon.a(RNBSocket.cpp.o)
llvm::SMTSolver::dump() const in 
liblldbDebugserverCommon.a(RNBSocket.cpp.o)
llvm::SMTSort::dump() const in 
liblldbDebugserverCommon.a(RNBSocket.cpp.o)
llvm::SMTExpr::dump() const in 
liblldbDebugserverCommon.a(SocketAddress.cpp.o)
llvm::SMTSolver::dump() const in 
liblldbDebugserverCommon.a(SocketAddress.cpp.o)
llvm::SMTSort::dump() const in 
liblldbDebugserverCommon.a(SocketAddress.cpp.o)

Long story short: You can't have an LLVM_DUMP_METHOD defined inline inside of a 
module.

One way to fix this would be to move the function body of the various

  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }

functions into .cpp files.


Repository:
  rL LLVM

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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-25 Thread guangqing.chen via Phabricator via cfe-commits
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



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-25 Thread guangqing.chen via Phabricator via cfe-commits
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 ACTION
  https://reviews.llvm.org/D54978/new/

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-25 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 happy with your quickly reply.
>  btw, `Z3_get_bv_sort_size` is also needed :)
>  Thanks for your nice job!


You can get the sort size by calling getBitvectorSortSize().


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-25 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 
> wrote:
> 
> 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!

Sure, I'll create a new revision with the added functions tonight.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-25 Thread guangqing.chen via Phabricator via cfe-commits
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://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-23 Thread Dominic Chen via Phabricator via cfe-commits
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 should just work but I'd like to add a message to 
> warn the user that we found the lib but we don't know if it'll link.


Thanks, sounds good to me.

In D54978#1394613 , @thakis wrote:

> mikhail.ramalho: My guess is that we need to pass on LLVM_OPTIMIZED_TABLEGEN 
> to the child cmake invocation in 
> http://llvm-cs.pcc.me.uk/cmake/modules/CrossCompile.cmake#50 (like we pass on 
> a few other variables) to fix this.


Do you know if this configuration builds fine now?


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-19 Thread Mikhail Ramalho via Phabricator via cfe-commits
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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-19 Thread Mikhail Ramalho via Phabricator via cfe-commits
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/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: llvm/include/llvm/Config/config.h.cmake

[PATCH] D54978: Move the SMT API to LLVM

2019-03-18 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 succeed but the compilation will fail.

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 should just work but I'd like to add a message to warn 
the user that we found the lib but we don't know if it'll link.

Let me know your thoughts.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-18 Thread Dominic Chen via Phabricator via cfe-commits
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.llvm.org/D54978/new/

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-18 Thread Mikhail Ramalho via Phabricator via cfe-commits
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:
  clang/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: 

[PATCH] D54978: Move the SMT API to LLVM

2019-03-18 Thread Dan Liew via Phabricator via cfe-commits
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 contribute to Z3 so I can't do this.
>
>
> I've opened https://github.com/Z3Prover/z3/issues/2184 .


Thanks.

> In D54978#1431936 , @delcypher wrote:
> 
>> This output means you built Z3 from source that was not in a git repository. 
>> In this case the header file should look the same for both Z3's CMake and 
>> Python build systems.
> 
> 
> That's strange, I have been building from a git repository.

Hmm I misread the python code. I inferred that because the extra text from

  def get_full_version_string(major, minor, build, revision):
  global GIT_HASH, GIT_DESCRIBE
  res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision)
  if GIT_HASH:
  res += " " + GIT_HASH
  if GIT_DESCRIBE:
  branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
  res += " " + branch + " " + check_output(['git', 'describe'])
  return '"' + res + '"'

wasn't in your output. However, I didn't actually check to see how `GIT_HASH` 
and `GIT_DESCRIBE` are set. It looks like you need to pass `--githash` and 
`--gitdescribe` respectively to the Python build system configure scripts to 
get those. They are false by default.
The Z3 CMake build system is different. It will add the git hash and 
description by default if it detects you're using git ( see 
https://github.com/Z3Prover/z3/blob/057151c7a80dac44d610f5286799ad7b727b5d2c/CMakeLists.txt#L67
 ). You can switch this off by passing
`-DINCLUDE_GIT_HASH=OFF -DINCLUDE_GIT_DESCRIBE=OFF` to the CMake invocation you 
use when configuring Z3.

> 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.
> 
> 
> Since the differences in version string depending on the build system are 
> intended behavior, it seems (2) would be preferable?

Yeah, that's the way I would go.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-18 Thread Mikhail Ramalho via Phabricator via cfe-commits
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/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: 

[PATCH] D54978: Move the SMT API to LLVM

2019-03-16 Thread Dominic Chen via Phabricator via cfe-commits
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 .

In D54978#1431936 , @delcypher wrote:

> This output means you built Z3 from source that was not in a git repository. 
> In this case the header file should look the same for both Z3's CMake and 
> Python build systems.


That's strange, I have been building from a git repository.

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.


Since the differences in version string depending on the build system are 
intended behavior, it seems (2) would be preferable?


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-16 Thread Dan Liew via Phabricator via cfe-commits
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 we can get the version number.
>
> I tried to use @brzycki code to get the version from the header, however, 
> it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 
> 4.8.3.0"` but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master 
> z3-4.8.4"` and cmake fails with the following message:
>
>   -- Could NOT find Z3: Found unsuitable version "#define Z3_FULL_VERSION
> "Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"", but required is at least 
> "4.7.1" (found /home/mgadelha/z3/bin/libz3.so)
>


This output means you built Z3 from source that was in a git repository and you 
used Z3's python build system.

In D54978#1431786 , @ddcc wrote:

> Thanks for making the changes! Is this being parsed from e.g. 
> `/usr/include/z3_version.h`? I checked their code, and I have a local build 
> of z3 4.8.5.0, but I'm not seeing those changes to the version string:
>
>   #define Z3_FULL_VERSION"Z3 4.8.5.0"
>


This output means you built Z3 from source that was not in a git repository. In 
this case the header file should look the same for both Z3's CMake and Python 
build systems.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-16 Thread Dan Liew via Phabricator via cfe-commits
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 CMake 
> though, so is it different if you use the python build? I haven't tried the 
> CMake build.


Hmm this looks like there are some bugs in the different Z3 build systems.

So for the CMake build the value of `Z3_FULL_VERSION_STR` is used to populate 
the `Z3_FULL_VERSION` macro in the header file. Initially this is 
`"${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}"`
 but then
If the git has is available we append to it 
https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L96
and if the git description is available we append to it 
https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L109
This was my attempt at mimicking the `get_full_version_string()` function ( 
https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L3065
 ) when I added Z3's CMake build system.

Unfortunately this doesn't quite match what Z3's python build system does.

- In the python build system the `VER_REVISION` global (used to set 
`Z3_REVISION_NUMBER` macro and is the forth integer in `Z3_FULL_VERSION`, i.e. 
`d` in `a.b.c.d`)  tries to count the number of commits reachable from the 
current git `HEAD` (see 
https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L561
 ). The CMake build system doesn't mimic this. Personally I don't think the 
python build system makes sense here at all given that this integer goes in the 
4th position in the version output (i.e. `d` in `a.b.c.d`).

- In the CMake build system the 4th integer in `Z3_FULL_VERSION` is always 
whatever `Z3_VERSION_TWEAK` is set to in the root `CMakeLists.txt` file. So 
far, I think has always been `0`.

So the bug here is that the CMake and python build systems don't agree on the 
meaning of the 4th version field. Personally I think the implementation of Z3's 
CMake build system makes more sense given where it is placed in the version 
string but that means the name `Z3_REVISION_NUMBER` macro name isn't very 
appropriate.

None of this really mattered until the version header file became public

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.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-16 Thread Dominic Chen via Phabricator via cfe-commits
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 might be the way to go, since the format seems to be more 
stable.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-15 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 specific to CMake 
> though, so is it different if you use the python build? I haven't tried the 
> CMake build.


Indeed, it seems to be cmake specific (even the commit message says that the 
python scripts were not changed).


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-15 Thread Dominic Chen via Phabricator via cfe-commits
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 CMake build.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-15 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 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 header, however, 
> > it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 
> > 4.8.3.0"` but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master 
> > z3-4.8.4"` and cmake fails with the following message:
>
>
> Thanks for making the changes! Is this being parsed from e.g. 
> `/usr/include/z3_version.h`? I checked their code, and I have a local build 
> of z3 4.8.5.0, but I'm not seeing those changes to the version string:
>
>   #define Z3_FULL_VERSION"Z3 4.8.5.0"
>


Nope, I downloaded it from release page on github: 
https://github.com/Z3Prover/z3/releases


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-15 Thread Dominic Chen via Phabricator via cfe-commits
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 version number.
>
> I tried to use @brzycki code to get the version from the header, however, 
> it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 
> 4.8.3.0"` but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master 
> z3-4.8.4"` and cmake fails with the following message:


Thanks for making the changes! Is this being parsed from e.g. 
`/usr/include/z3_version.h`? I checked their code, and I have a local build of 
z3 4.8.5.0, but I'm not seeing those changes to the version string:

  #define Z3_FULL_VERSION"Z3 4.8.5.0"


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-15 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 header, however, it's 
not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 4.8.3.0"` 
but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"` and 
cmake fails with the following message:

  -- Could NOT find Z3: Found unsuitable version "#define Z3_FULL_VERSION
"Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"", but required is at least 
"4.7.1" (found /home/mgadelha/z3/bin/libz3.so)

I believe we have a few options here:

1. Update the regex to handle the new format for `Z3_FULL_VERSION`.
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.

But, we'll still face the same problem of them changing the string format and 
breaking the scripts.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-03-15 Thread Mikhail Ramalho via Phabricator via cfe-commits
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/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: 

[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 5c6d3f0..f913686 100644
  --- a/llvm/cmake/modules/FindZ3.cmake
  +++ b/llvm/cmake/modules/FindZ3.cmake
  @@ -30,7 +30,23 @@ find_program(Z3_EXECUTABLE z3
  PATH_SUFFIXES bin
  )
   
  -if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
  +# Searching for the version of the Z3 library is a best-effort task. The 
version
  +# is only recently added to a public header.
  +unset(Z3_VERSION_STRING)
  +
  +if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR}/z3_version.h")
  +# Z3 4.8.1+ has the version is in a public header.
  +file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
  + z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
  +
  +string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1"
  + Z3_VERSION_STRING "${z3_version_str}")
  +unset(z3_version_str)
  +endif()
  +
  +if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND Z3_LIBRARIES AND
  +  Z3_EXECUTABLE))
  +# Run the found z3 executable and parse the version string output.
   execute_process (COMMAND ${Z3_EXECUTABLE} -version
 OUTPUT_VARIABLE libz3_version_str
 ERROR_QUIET
  @@ -41,6 +57,20 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
   unset(libz3_version_str)
   endif()
   
  +if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND Z3_LIBRARIES))
  +# We do not have the Z3 binary to query for a version. Try to use
  +# a small C++ program to detect it via the Z3_get_version() API call.
  +# TODO: add code from Mikhail Ramalho to obtain the version.
  +# TODO: set(Z3_VERSION_STRING) if successful.
  +endif()
  +
  +if(NOT Z3_VERSION_STRING)
  +# Give up: we are unable to obtain a version of the Z3 library. Be
  +# conservative and force the found version to 0.0.0 to make version
  +# checks always fail.
  +set(Z3_VERSION_STRING "0.0.0")
  +endif()
  +


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 `CHECK_CXX_SOURCE_RUNS` call.
>
>
> I think hardcoding the version into the binary is too brittle. Instead, your 
> program can just print out the current z3 version (much like the current 
> execution of the z3 binary), and the remaining logic can remain in CMake, 
> with the fallbacks as suggested above by @brzycki.


I don't think there is a mechanism to do so easily within CMake. The 
`CHECK_CXX_SOURCE_RUNS` call only returns a boolean answer, not stdout. You 
have to use the underlying `try_run()` command along with `RUN_OUTPUT_VARIABLE` 
to obtain a given version. This interface seems less simple than the 
`CHECK_CXX_*` macros.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Dominic Chen via Phabricator via cfe-commits
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, your 
program can just print out the current z3 version (much like the current 
execution of the z3 binary), and the remaining logic can remain in CMake, with 
the fallbacks as suggested above by @brzycki.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Mikhail Ramalho via Phabricator via cfe-commits
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_package` call or 
remove the minimum version from the `find_package` call and rely only on the 
program. I'm not a big fan of the latter.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Mikhail Ramalho via Phabricator via cfe-commits
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/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -151,6 +158,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -176,7 +184,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: llvm/include/llvm/Config/config.h.cmake

[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 unfortunately I think the second check 
> for `version.h` is superfluous. Instead, I think it'd be ok to still query 
> the executable as the primary, then fallback to this header as the secondary?


Thanks @ddcc for checking on `version.h`, I meant to do so but got side-tracked 
with other items today.

I think your suggestion is a good compromise, possibly something like the 
following as pseudo-code:

  if z3_version.h:
use_regex_parsed_version
  
  if version_not_valid and z3_executable:
use_z3_execution output_version
  
  if version_not_valid z3_include_dir:
try_mikhail.ramalho_runtime_check
  
  if version_not_valid:
warning "Z3 is not installed correctly or too old to detect its version"
version = 0.0.0


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-13 Thread Dominic Chen via Phabricator via cfe-commits
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 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 unfortunately I think the second check for 
`version.h` is superfluous. Instead, I think it'd be ok to still query the 
executable as the primary, then fallback to this header as the secondary?


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 set.


I'm not sure, cross-compilation is tricky to get right.

> I just finished a small patch that checks the version as a run-time property. 
> Please, let me know your thoughts.
>  If you agree with this approach I'll create a separate revision for it (it 
> seems to work on ubuntu and fedora for me).

I'd be interested in seeing it and I'll happily provide feedback. I'm not sure 
if this method is better or worse than regex parsing of headers that @ddcc 
suggested.

No matter what algorithm chosen I'd strongly prefer the case when we are unable 
to ascertain the correct `Z3_VERSION_STRING` we should conservatively set this 
to `"0.0.0"` with a warning to inform the users early on something is strange 
with the version of Z3 being tested.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" 
> Z3_VERSION_STRING "${z3_version_str}")
> unset(z3_version_str)
>   endif()

That is almost exactly what I was thinking about this morning. I'd prefer the 
following since it's more robust for older versions:

  if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/z3_version.h")
# For 4.8.0 or newer
file(STRINGS "${Z3_INCLUDE_DIR }/z3_version.h" z3_version_str REGEX 
"^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
  
string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" 
Z3_VERSION_STRING "${z3_version_str}")
unset(z3_version_str)
  elseif(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/version.h")
file(STRINGS "${Z3_INCLUDE_DIR }/version.h" z3_version_str REGEX 
"^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
  
string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" 
Z3_VERSION_STRING "${z3_version_str}")
unset(z3_version_str)
  else()
message(WARNING "Unable to locate the Z3 version.h header. Setting the 
found version to 0.0.0.")
set(Z3_VERSION_STRING "0.0.0")
  endif()


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Dominic Chen via Phabricator via cfe-commits
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 good to emit a warning or at least 
a message about assuming the version due to a missing executable.

In D54978#1395561 , @brzycki wrote:

> I looked at the Z3 source and they do have a `z3_version.h` file now and was 
> added in version 4.4.2.0. You may be able to use the header directly, but I'm 
> not sure how `find_package()` parses for library versions and if this is 
> useful or not.  The generated header is named `src/util/version.h` in this 
> initial commit:
>  
> https://github.com/Z3Prover/z3/commit/251527603df01904f70ed884f8695fedab5caed9


You're right, it looks like it was originally internal-only, but them became 
exposed as part of the interface with the second commit, starting around the 
release of z3 4.8.1. It's been a while since I've used CMake, but 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_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" 
Z3_VERSION_STRING "${z3_version_str}")
unset(z3_version_str)
  endif()



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?


I see other projects do something similar; e.g. 
https://github.com/SRI-CSL/sally/blob/master/cmake/FindZ3.cmake#L20 . I'm less 
fond of that approach because it involves even more moving parts, but then 
again, parsing C header files with regular expressions isn't particularly 
robust either.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Nico Weber via Phabricator via cfe-commits
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/CrossCompile.cmake
>   +++ b/llvm/cmake/modules/CrossCompile.cmake
>   @@ -53,6 +53,7 @@ function(llvm_create_cross_target_internal target_name 
> toolchain buildtype)
>-DLLVM_DEFAULT_TARGET_TRIPLE="${TARGET_TRIPLE}"
>-DLLVM_TARGET_ARCH="${LLVM_TARGET_ARCH}"
>
> -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="${LLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN}"
>   +-DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
>${build_type_flags} ${linker_flag} ${external_clang_dir}
>WORKING_DIRECTORY ${LLVM_${target_name}_BUILD}
>DEPENDS CREATE_LLVM_${target_name}
>


Independent of the rest of the discussion, this patch should be part of the 
reland, to make sure that explicitly turning off Z3 works reliably. Thanks for 
coming up with that, and thanks everyone for the good discussion here :)


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 run a small program that would return EXIT_SUCCESS if the 
> > library is the correct version?
>
>
> Hi @mikhail.ramalho, I don't think this is feasible unfortunately. If we're 
> using a cross-compiler the emitted binary won't be native to the platform. In 
> other words, you cannot test for Z3 as a run-time property.


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.

I just finished a small patch that checks the version as a run-time property. 
Please, let me know your thoughts.

If you agree with this approach I'll create a separate revision for it (it 
seems to work on ubuntu and fedora for me).


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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?


Hi @mikhail.ramalho, I don't think this is feasible unfortunately. If we're 
using a cross-compiler the emitted binary won't be native to the platform. In 
other words, you cannot test for Z3 as a run-time property.

I looked at the Z3 source and they do have a `z3_version.h` file now and was 
added in version 4.4.2.0. You may be able to use the header directly, but I'm 
not sure how `find_package()` parses for library versions and if this is useful 
or not.  The generated header is named `src/util/version.h` in this initial 
commit:
https://github.com/Z3Prover/z3/commit/251527603df01904f70ed884f8695fedab5caed9

and was renamed last September to `src/util/z3_version.h` in this commit:
https://github.com/Z3Prover/z3/commit/0c4754d94bdfaf07077120f5cbff780d8fb0971d


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Mikhail Ramalho via Phabricator via cfe-commits
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()
  {
unsigned int major, minor, build, revision;
Z3_get_version(, , , );

if(major >= 4 && minor >= 7 && build >= 1)
  return EXIT_SUCCESS;
  
return EXIT_FAILURE;
  }

This would be part of FindZ3.cmake and would set Z3_FOUND.

Do you guys think it's possible? I'm almost certain it can be done with 
autotools, but I'm clueless when it comes to cmake.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Mikhail Ramalho via Phabricator via cfe-commits
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



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


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

2019-02-12 Thread Mikhail Ramalho via cfe-commits
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..b213342df37 100644
>   --- a/llvm/cmake/modules/FindZ3.cmake
>   +++ b/llvm/cmake/modules/FindZ3.cmake
>   @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
>string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
>   Z3_VERSION_STRING "${libz3_version_str}")
>unset(libz3_version_str)
>   +else()
>   +# The version could not be determined from running Z3_EXECUTABLE.
> Set the
>   +# version Z3 to the lowest possible value such that all checks for a
>   +# minimum version will fail.
>   +set(Z3_VERSION_STRING "0.0.0")
>endif()
>
># handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
>
> 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.
>
>
This seems fine but 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()
{
  unsigned int major, minor, build, revision;
  Z3_get_version(, , , );

  if(major >= 4 && minor >= 7 && build >= 1)
return EXIT_SUCCESS;

  return EXIT_FAILURE;
}
```

This would be part of FindZ3.cmake and would set Z3_FOUND.

Do you guys think it's possible? I'm almost certain it can be done with
autotools, but I'm clueless when it comes to cmake.

-- 

Mikhail Ramalho.
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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` installed. This provides the `/usr/bin/z3` 
> > executable which `llvm/cmake/modules/FindZ3.cmake` relies upon to determine 
> > the correct `Z3_VERSION_STRING`.
>
>
> Yeah, that's what I meant by best-effort only. Due to upstream Z3's design, 
> without the binary, there is no easy way to retrieve the current installed 
> version, so when I originally wrote the Z3 integration, it seemed fine to let 
> the version check pass. Given the issues that have come up, it might make 
> more sense to at least emit a warning, or explicitly fail if the version 
> can't be determined, and prompt the user to install the binary.


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..b213342df37 100644
  --- a/llvm/cmake/modules/FindZ3.cmake
  +++ b/llvm/cmake/modules/FindZ3.cmake
  @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
   string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
  Z3_VERSION_STRING "${libz3_version_str}")
   unset(libz3_version_str)
  +else()
  +# The version could not be determined from running Z3_EXECUTABLE. Set the
  +# version Z3 to the lowest possible value such that all checks for a
  +# minimum version will fail.
  +set(Z3_VERSION_STRING "0.0.0")
   endif()
  
   # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if

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.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Dominic Chen via Phabricator via cfe-commits
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/FindZ3.cmake` relies upon to determine 
> the correct `Z3_VERSION_STRING`.


Yeah, that's what I meant by best-effort only. Due to upstream Z3's design, 
without the binary, there is no easy way to retrieve the current installed 
version, so when I originally wrote the Z3 integration, it seemed fine to let 
the version check pass. Given the issues that have come up, it might make more 
sense to at least emit a warning, or explicitly fail if the version can't be 
determined, and prompt the user to install the binary.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 perform the following on an unpatched checkout of sha b0a227049fda 
 the build 
works :

  sudo apt install -y z3 libz3-4 libz3-dev
  mkdir build && cd build

Either of the following CMake commands build successfully:

  cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm
  cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF 
../llvm-project/llvm

And if I try `-D LLVM_ENABLE_Z3_SOLVER=ON` I receive a top-leve CMake error 
immediately:

  -- Could NOT find Z3: Found unsuitable version "4.4.1", but required is at 
least "4.7.1" (found /usr/lib/x86_64-linux-gnu/libz3.so)
  CMake Error at CMakeLists.txt:406 (message):
LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.
  
  
  -- Configuring incomplete, errors occurred!
  See also "/work/brzycki/build/CMakeFiles/CMakeOutput.log".
  ninja: error: loading 'build.ninja': No such file or directory

Unfortunately it's completely valid to install packages `libz3-4` and 
`libz3-dev` without pulling in `z3` on Ubuntu 18.04.  I've added this to my 
internal build notes.

I'm also looking to see if there's a way to better  handle this case inside the 
`find_package(Z3 ...)` subsystem of llvm.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 @@ function(llvm_create_cross_target_internal target_name 
toolchain buildtype)
   -DLLVM_DEFAULT_TARGET_TRIPLE="${TARGET_TRIPLE}"
   -DLLVM_TARGET_ARCH="${LLVM_TARGET_ARCH}"
   
-DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="${LLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN}"
  +-DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
   ${build_type_flags} ${linker_flag} ${external_clang_dir}
   WORKING_DIRECTORY ${LLVM_${target_name}_BUILD}
   DEPENDS CREATE_LLVM_${target_name}

fixes the build break when CMake is called in the following manner:

  cmake -v -G Ninja  -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF 
../llvm-project/llvm

However, the custom command sub-call to CMake always fails in the same way with 
either of these invocations:

  cmake -v -G Ninja  -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=ON 
../llvm-project/llvm
  cmake -v -G Ninja  -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm

The error is the following:

  [209/2543] /usr/bin/c++  -DGTEST_HAS_RTTI=0 -D_DEBUG -D_GNU_SOURCE 
-D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS 
-Iutils/TableGen -I/work/brzycki/llvm-project/llvm/utils/TableGen 
-I/usr/include/libxml2 -Iinclude -I/work/brzycki/llvm-project/llvm/include 
-fPIC -fvisibility-inlines-hidden -Werror=date-time -std=c++11 -Wall -Wextra 
-Wno-unused-parameter -Wwrite-strings -Wcast-qual 
-Wno-missing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough 
-Wno-maybe-uninitialized -Wno-noexcept-type -Wdelete-non-virtual-dtor 
-Wno-comment -fdiagnostics-color -g-fno-exceptions -fno-rtti -MD -MT 
utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o -MF 
utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o.d -o 
utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o -c 
/work/brzycki/llvm-project/llvm/utils/TableGen/GlobalISelEmitter.cpp
  [210/2543] cd /work/brzycki/build/NATIVE && 
/sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake -G Ninja 
-DCMAKE_MAKE_PROGRAM="/sarc-c/compiler_tmp/tools/build/ninja-1.8.2/ninja" 
-DCMAKE_C_COMPILER=/usr/bin/cc -DCMAKE_CXX_COMPILER=/usr/bin/c++ 
/work/brzycki/llvm-project/llvm -DLLVM_TARGET_IS_CROSSCOMPILE_HOST=TRUE 
-DLLVM_TARGETS_TO_BUILD="AArch64;AMDGPU;ARM;BPF;Hexagon;Lanai;Mips;MSP430;NVPTX;PowerPC;Sparc;SystemZ;WebAssembly;X86;XCore"
 -DLLVM_EXPERIMENTAL_TARGETS_TO_BUILD="" 
-DLLVM_DEFAULT_TARGET_TRIPLE="x86_64-unknown-linux-gnu" 
-DLLVM_TARGET_ARCH="host" -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="OFF" 
-DLLVM_ENABLE_Z3_SOLVER="ON" -DCMAKE_BUILD_TYPE=Release
  -- The C compiler identification is GNU 7.3.0
  -- The CXX compiler identification is GNU 7.3.0
  -- The ASM compiler identification is GNU
  -- Found assembler: /usr/bin/cc
  ...
  ...
  -- Performing Test HAVE_GNU_POSIX_REGEX -- failed to compile
  -- Performing Test HAVE_POSIX_REGEX
  -- Performing Test HAVE_POSIX_REGEX
  -- Performing Test HAVE_POSIX_REGEX -- success
  -- Performing Test HAVE_STEADY_CLOCK
  -- Performing Test HAVE_STEADY_CLOCK
  -- Performing Test HAVE_STEADY_CLOCK -- success
  -- Configuring done
  -- Generating done
  -- Build files have been written to: /work/brzycki/build/NATIVE
  ninja: build stopped: subcommand failed.

I tried passing more information to the sub CMake call, but it yielded the 
exact same results:

  +-DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
  +-DLLVM_Z3_INSTALL_DIR="${LLVM_Z3_INSTALL_DIR}"
  +-DZ3_EXECUTABLE="${Z3_EXECUTABLE}"
  +-DZ3_INCLUDE_DIR="${Z3_INCLUDE_DIR}"
  +-DZ3_LIBRARIES="${Z3_LIBRARIES}"

When I diff the successful sub-CMake with the failing one, the only difference 
is the detection of the Z3 solver library:

  $ diff -u good_submake.txt bad_submake.txt
  --- good_submake.txt2019-02-12 11:41:54.638892191 -0600
  +++ bad_submake.txt 2019-02-12 11:43:30.096484824 -0600
  @@ -14,7 +14,7 @@
   -- Detecting CXX compiler ABI info - done
   -- Detecting CXX compile features
   -- Detecting CXX compile features - done
  --- Could NOT find Z3 (missing: Z3_LIBRARIES Z3_INCLUDE_DIR) (Required is at 
least version "4.7.1")
  +-- Found Z3: /usr/lib/x86_64-linux-gnu/libz3.so (Required is at least 
version "4.7.1")
   -- Looking for dlfcn.h
   -- Looking for dlfcn.h - found
   -- Looking for errno.h


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-12 Thread Nico Weber via Phabricator via cfe-commits
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 several times, the CMake option `-D 
> LLVM_OPTIMIZED_TABLEGEN=ON` spawns a sub-command of CMake and **is required 
> for the break to occur**. I don't know how to make this any more clear: if 
> you build with optimized tablegen, it breaks. I strongly suspect an 
> interaction between LLVM's top-level CMake and the TableGen one but I haven't 
> had time to debug it down to the exact cause.
> 
> It is important to me because the detection of the correct version of Z3 is 
> imprecise, at best.  If a Z3 library is found  I have no way to guarantee a 
> build I run will not attempt to include the library.

Got it now, sorry about being dense.

mikhail.ramalho: My guess is that we need to pass on LLVM_OPTIMIZED_TABLEGEN to 
the child cmake invocation in 
http://llvm-cs.pcc.me.uk/cmake/modules/CrossCompile.cmake#50 (like we pass on a 
few other variables) to fix this.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 to OFF?


Yes, Please see my recreation instructions above. I created a new, empty 
`build` directory.

> 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 several times, the CMake option `-D 
LLVM_OPTIMIZED_TABLEGEN=ON` spawns a sub-command of CMake and **is required for 
the break to occur**. I don't know how to make this any more clear. If you 
build with optimized tablegen, it breaks. I strongly suspect an interaction 
between LLVM's top-level CMake and the TableGen one but I haven't had time to 
debug it down to the exact cause.

It is important to me because the detection of the correct version of Z3 is 
imprecise, at best.  If a Z3 library is found  I have no way to guarantee a 
build I run will not attempt to include the library.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-11 Thread Nico Weber via Phabricator via cfe-commits
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 case I'd really prefer if 
> `LLVM_ENABLE_Z3_SOLVER` was explicit opt-in and defaulted to `OFF` regardless 
> of what `find_package` returned.

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 to OFF? 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.)


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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`:

  find_package(Z3 4.7.1)
  ...
  set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
  
  option(LLVM_ENABLE_Z3_SOLVER
"Enable Support for the Z3 constraint solver in LLVM."
${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
  )

If `find_package()` idenfiies a suitable `Z3_FOUND` the default is to enable 
builds with the Z3 framework. In other words the entire Z3 feature is manual 
opt-out and implicit opt-in when CMake thinks a suitable Z3 library is found.

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 case I'd really prefer if 
`LLVM_ENABLE_Z3_SOLVER` was explicit opt-in and defaulted to `OFF` regardless 
of what `find_package` returned.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-11 Thread Dominic Chen via Phabricator via cfe-commits
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 number 
from standard output, otherwise, it fails silently. This is because upstream Z3 
doesn't define the API version in a header file, and uses a homebrew 
python-based build system that also doesn't export the version. I believe 
@delcypher 's CMake-based build system for upstream Z3 might solve this 
problem, but I haven't looked at it in a long time, and it it appears to be 
stalled ( https://github.com/Z3Prover/z3/issues/986 ).

I also agree that more notice about this patch would have been appreciated; I 
didn't hear it until I read LLVM weekly today.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 available.
  Distributor ID: Ubuntu
  Description:Ubuntu 18.04.1 LTS
  Release:18.04
  Codename:   bionic
  
  sudo apt install -y libz3-4 libz3-dev
  
  # Clone llvm-project and checkout the test SHA
  tmpd=$(mktemp -d)
  cd $tmpd
  git clone https://github.com/llvm/llvm-project.git
  git checkout b0a227049fda
  
  # Setup symlinks under llvm to compile correctly
  cd $tmpd/llvm-project/llvm
  ln -s ../../clang
  ln -s ../../polly
  ln -s ../../libcxx
  ln -s ../../libcxxabi
  
  # CMake and Ninja
  mkdir $tmpd/build
  cd $tmpd/build
  cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF 
../llvm-project/llvm
  ninja -v

These steps produce the error:

  [70/187] Building CXX object 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  /usr/bin/c++  -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS 
-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Ilib/Support 
-I/work/brzycki/llvm-project/llvm/lib/Support -I/usr/include/libxml2 -Iinclude 
-I/work/brzycki/llvm-project/llvm/include -fPIC -fvisibility-inlines-hidden 
-Werror=date-time -std=c++11 -Wall -Wextra -Wno-unused-parameter 
-Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic 
-Wno-long-long -Wimplicit-fallthrough -Wno-maybe-uninitialized 
-Wno-noexcept-type -Wdelete-non-virtual-dtor -Wno-comment -fdiagnostics-color 
-ffunction-sections -fdata-sections -O3 -DNDEBUG-fno-exceptions -fno-rtti 
-MD -MT lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -MF 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o.d -o 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -c 
/work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp
  /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp: In function ‘void 
{anonymous}::Z3ErrorHandler(Z3_context, Z3_error_code)’:
  /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp:44:71: error: cannot 
convert ‘Z3_context {aka _Z3_context*}’ to ‘Z3_error_code’ for argument ‘1’ to 
‘const char* Z3_get_error_msg(Z3_error_code)’
  llvm::Twine(Z3_get_error_msg(Context, Error)));
 ^

If I remove `-D LLVM_ENABLE_Z3_SOLVER=OFF` the actual TableGen CMake fails to 
succeed:

  cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm
  ninja -v

And here's the TableGen CMake error:

  [218/3618] cd /work/brzycki/build/NATIVE && 
/sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake -G Ninja 
-DCMAKE_MAKE_PROGRAM="/sarc-c/compiler_tmp/tools/build/ninja-1.8.2/ninja" 
-DCMAKE_C_COMPILER=/usr/bin/cc -DCMAKE_CXX_COMPILER=/usr/bin/c++ 
/work/brzycki/llvm-project/llvm -DLLVM_TARGET_IS_CROSSCOMPILE_HOST=TRUE 
-DLLVM_TARGETS_TO_BUILD="AArch64;AMDGPU;ARM;BPF;Hexagon;Lanai;Mips;MSP430;NVPTX;PowerPC;Sparc;SystemZ;WebAssembly;X86;XCore"
 -DLLVM_EXPERIMENTAL_TARGETS_TO_BUILD="" 
-DLLVM_DEFAULT_TARGET_TRIPLE="x86_64-unknown-linux-gnu" 
-DLLVM_TARGET_ARCH="host" -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="OFF" 
-DCMAKE_BUILD_TYPE=Release
  -- The C compiler identification is GNU 7.3.0
  -- The CXX compiler identification is GNU 7.3.0
  -- The ASM compiler identification is GNU
  -- Found assembler: /usr/bin/cc
  -- Check for working C compiler: /usr/bin/cc
  -- Check for working C compiler: /usr/bin/cc -- works
  -- Detecting C compiler ABI info
  -- Detecting C compiler ABI info - done
  -- Detecting C compile features
  -- Detecting C compile features - done
  -- Check for working CXX compiler: /usr/bin/c++
  -- Check for working CXX compiler: /usr/bin/c++ -- works
  -- Detecting CXX compiler ABI info
  -- Detecting CXX compiler ABI info - done
  -- Detecting CXX compile features
  -- Detecting CXX compile features - done
  -- Found Z3: /usr/lib/x86_64-linux-gnu/libz3.so (Required is at least version 
"4.7.1")
  -- Looking for dlfcn.h
  -- Looking for dlfcn.h - found
  -- Looking for errno.h
  -- Looking for errno.h - found
  -- Looking for fcntl.h
  -- Looking for fcntl.h - found
  -- Looking for link.h
  -- Looking for link.h - found
  -- Looking for malloc/malloc.h
  -- Looking for malloc/malloc.h - not found
  -- Looking for pthread.h
  -- Looking for pthread.h - found
  -- Looking for signal.h
  -- Looking for signal.h - found
  -- Looking for sys/ioctl.h
  -- Looking for sys/ioctl.h - found
  -- Looking for sys/mman.h
  -- Looking for sys/mman.h - found
  -- Looking for sys/param.h
  -- Looking for sys/param.h - found
  -- Looking for sys/resource.h
  -- Looking for sys/resource.h - found
  -- Looking for sys/stat.h
  -- Looking for sys/stat.h - found
  -- Looking for sys/time.h
  -- Looking for sys/time.h - 

[PATCH] D54978: Move the SMT API to LLVM

2019-02-11 Thread Kristóf Umann via Phabricator via cfe-commits
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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-10 Thread Mikhail Ramalho via Phabricator via cfe-commits
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_BACKTRACES=OFF -DLLVM_TARGETS_TO_BUILD=host 
-DLLVM_ENABLE_Z3_SOLVER=ON -DCMAKE_BUILD_TYPE=RelWithDebInfo
  -- clang project is enabled
  -- compiler-rt project is disabled
  -- debuginfo-tests project is disabled
  -- libclc project is disabled
  -- libcxx project is disabled
  -- libcxxabi project is disabled
  -- libunwind project is disabled
  -- lld project is disabled
  -- lldb project is disabled
  -- llgo project is disabled
  -- llvm project is disabled
  -- openmp project is disabled
  -- parallel-libs project is disabled
  -- polly project is disabled
  -- pstl project is disabled
  -- Could NOT find Z3: Found unsuitable version "4.4.1", but required is at 
least "4.7.1" (found /usr/lib/x86_64-linux-gnu/libz3.so)
  CMake Error at CMakeLists.txt:406 (message):
LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.
  
  
  -- Configuring incomplete, errors occurred!
  See also "/home/mgadelha/llvm/build/CMakeFiles/CMakeOutput.log".


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-10 Thread Mikhail Ramalho via Phabricator via cfe-commits
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



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-09 Thread Kristóf Umann via Phabricator via cfe-commits
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 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 error.
> >
> > @thakis, do you have any idea why this was not sent to the llvm mailing 
> > lists?
>
>
> I'm guessing you didn't add llvm-commits and cfe-commits as subscribers when 
> sending this out?


As far as I know, that happens automatically if you add LLVM or Clang as 
project, that usually works for me.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-09 Thread Nico Weber via Phabricator via cfe-commits
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 with the failure?
>
> @brzycki, I'm using Ubuntu 18.04.2 and I'll try to reproduce the error.
>
> @thakis, do you have any idea why this was not sent to the llvm mailing lists?


I'm guessing you didn't add llvm-commits and cfe-commits as subscribers when 
sending this out?


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-08 Thread Mikhail Ramalho via Phabricator via cfe-commits
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 error.

@thakis, do you have any idea why this was not sent to the llvm mailing lists?


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-08 Thread George Karpenkov via Phabricator via cfe-commits
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.

@mikhail.ramalho could you take a look?


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 
. There is at least one other conflicting 
commit rL353465  on top of this code already.

I don't feel comfortable reverting 2+ patches in a sub-section of the code I 
know little about on a Friday afternoon. :)


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-08 Thread Nico Weber via Phabricator via cfe-commits
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-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[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 
 from Feb 
8, 2019.

First, make sure Ubuntu has installed its version of Z3:

  sudo apt install libz3-4 libz3-dev
  dpkg -l | grep libz3
  ii  libz3-4:amd64 4.4.1-0.3build4 
amd64theorem prover from Microsoft Research - runtime libraries
  ii  libz3-dev:amd64   4.4.1-0.3build4 
amd64theorem prover from Microsoft Research - development files

Next, run CMake with the following arguments:

  mkdir build && cd build
  cmake \
-G Ninja \
-D LLVM_OPTIMIZED_TABLEGEN=ON \
-D LLVM_ENABLE_Z3_SOLVER=OFF \
  /path/to/llvm-project/llvm

First, you'll see that CMake detects a version of Z3:

  -- Found Z3: /usr/lib/x86_64-linux-gnu/libz3.so (Required is at least version 
"4.7.1")

At around ninja command 600-700 a second CMake instance is spawned for the 
TableGen optimizations:

  [666/3618] cd /work/brzycki/b/NATIVE && 
/sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake -G Ninja 
-DCMAKE_MAKE_PROGRAM="/sarc-c/compiler_tmp/tools/build/ninja-1.8.2/ninja" 
-DCMAKE_C_COMPILER=/usr/bin/cc -DCMAKE_CXX_COMPILER=/usr/bin/c++ 
/work/brzycki/llvm-project/llvm -DLLVM_TARGET_IS_CROSSCOMPILE_HOST=TRUE 
-DLLVM_TARGETS_TO_BUILD="AArch64;AMDGPU;ARM;BPF;Hexagon;Lanai;Mips;MSP430;NVPTX;PowerPC;Sparc;SystemZ;WebAssembly;X86;XCore"
 -DLLVM_EXPERIMENTAL_TARGETS_TO_BUILD="" 
-DLLVM_DEFAULT_TARGET_TRIPLE="x86_64-unknown-linux-gnu" 
-DLLVM_TARGET_ARCH="host" -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="OFF" 
-DCMAKE_BUILD_TYPE=Release
  -- The C compiler identification is GNU 7.3.0
  -- The CXX compiler identification is GNU 7.3.0
  -- The ASM compiler identification is GNU
  -- Found assembler: /usr/bin/cc
  -- Check for working C compiler: /usr/bin/cc
  -- Check for working C compiler: /usr/bin/cc -- works
  ...

And shortly after that we fail:

  -- Build files have been written to: /work/brzycki/b/NATIVE
  [666/3618] cd /work/brzycki/b/NATIVE && 
/sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake --build 
/work/brzycki/b/NATIVE --target llvm-tblgen --config Release
  [72/187] Building CXX object 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  /usr/bin/c++  -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS 
-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Ilib/Support 
-I/work/brzycki/llvm-project/llvm/lib/Support -I/usr/include/libxml2 -Iinclude 
-I/work/brzycki/llvm-project/llvm/include -fPIC -fvisibility-inlines-hidden 
-Werror=date-time -std=c++11 -Wall -Wextra -Wno-unused-parameter 
-Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic 
-Wno-long-long -Wimplicit-fallthrough -Wno-maybe-uninitialized 
-Wno-noexcept-type -Wdelete-non-virtual-dtor -Wno-comment -fdiagnostics-color 
-ffunction-sections -fdata-sections -O3 -DNDEBUG-fno-exceptions -fno-rtti 
-MD -MT lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -MF 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o.d -o 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -c 
/work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp
  /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp: In function ‘void 
{anonymous}::Z3ErrorHandler(Z3_context, Z3_error_code)’:
  /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp:44:71: error: cannot 
convert ‘Z3_context {aka _Z3_context* ’ to ‘Z3_error_code’ for argument ‘1’ to 
‘const char* Z3_get_error_msg(Z3_error_code)’
  llvm::Twine(Z3_get_error_msg(Context, Error)));
 ^
  [183/187] Building CXX object 
utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o
  ninja: build stopped: subcommand failed.
  FAILED: NATIVE/bin/llvm-tblgen
  cd /work/brzycki/b/NATIVE && 
/sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake --build 
/work/brzycki/b/NATIVE --target llvm-tblgen --config Release
  ninja: build stopped: subcommand failed.

I consider this to be 2 bugs:

1. CMake should not set Z3_FOUND when the library is too old. The 
llvm/CMakeLists.txt file correctly states `find_package(Z3 4.7.1)` but it 
doesn't work right and consideres the 4.4.1 one valid. It's why I'm in this 
mess in the first place.
2. There's some sort of interaction bug between the top-level 
llvm/CMakeLists.txt and the tablegen one when optimizations are turned on. It 
doesn't seem to respect the `LLVM_ENABLE_Z3_SOLVER` directive.


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

2019-02-08 Thread Nico Weber via Phabricator via cfe-commits
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 the exact same 
> invocation.
>
> The problem is our build machine (Ubuntu 18.04 LTS) installs an old version 
> of Z3 that is incompatible with LLVM's tip of tree. To deal with this we add 
> `-D CLANG_ANALYZER_ENABLE_Z3_SOLVER=OFF` to force disabling Z3 even if CMake 
> detects the library is installed.
>
>   With this patch I am unable to disable Z3 because 
> `CLANG_ANALYZER_ENABLE_Z3_SOLVER` is no longer in the codebase and setting 
> `-D LLVM_ENABLE_Z3_SOLVER=OFF` still builds Z3 support (which fails):
>
>   [74/187] Building CXX object 
> lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
>   FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
>   /usr/bin/clang++-6.0  -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE 
> -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS 
> -Ilib/Support -I/tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support 
> -I/usr/include/libxml2 -Iinclude -I/tmp/tmp.UCDOJjmgJ1/src/llvm/include -fPIC 
> -fvisibility-inlines-hidden -Werror=date-time 
> -Werror=unguarded-availability-new -std=c++11 -Wall -Wextra 
> -Wno-unused-parameter -Wwrite-strings -Wcast-qual 
> -Wmissing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough 
> -Wcovered-switch-default -Wno-noexcept-type -Wnon-virtual-dtor 
> -Wdelete-non-virtual-dtor -Wstring-conversion -fdiagnostics-color 
> -ffunction-sections -fdata-sections -O3 -DNDEBUG-fno-exceptions -fno-rtti 
> -MD -MT lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -MF 
> lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o.d -o 
> lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -c 
> /tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp
>   /tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp:44:40: error: no 
> matching function for call to 'Z3_get_error_msg'
>  llvm::Twine(Z3_get_error_msg(Context, Error)));
>  ^~~~
>


From what I understand, setting `-DLLVM_ENABLE_Z3_SOLVER=OFF` is supposed to 
work – the contents of Z3Solver.cpp are wrapped in a `#if LLVM_WITH_Z3`, and 
the logic in the llvm cmake file looks identical to the logic in the clang 
cmake file previously. Can you maybe debug a bit to see what goes wrong on your 
bot?

lebedev.ri's point about this not being reviewed properly is a good one though.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-08 Thread Nico Weber via Phabricator via cfe-commits
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 
other people using then gn build) to fix this. If you're not comfortable with 
that, please don't use the GN build. (I just merged this to the GN build in 
r353518, so syncing will make things go again for you.)


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-07 Thread George Karpenkov via Phabricator via cfe-commits
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



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-07 Thread Shakeel Mahate via Phabricator via cfe-commits
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/clang/test/lit.site.cfg.py ../../clang/test/lit.site.cfg.py.in 
LIT_SITE_CFG_IN_HEADER=\#\#\ Autogenerated\ from\ 
//clang/test/lit.site.cfg.py.in,\ do\ not\ edit 
CLANG_BINARY_DIR=/home/shakeel/devel/llvm-project/out/gn/obj/clang 
CLANG_SOURCE_DIR=/home/shakeel/devel/llvm-project/clang ENABLE_SHARED=0 
LLVM_BINARY_DIR=/home/shakeel/devel/llvm-project/out/gn/obj/llvm LLVM_LIBS_DIR= 
LLVM_SOURCE_DIR=/home/shakeel/devel/llvm-project/llvm 
LLVM_TOOLS_DIR=/home/shakeel/devel/llvm-project/out/gn/bin 
TARGET_TRIPLE=x86_64-unknown-linux-gnu 
SHLIBDIR=/home/shakeel/devel/llvm-project/out/gn/lib CLANG_ANALYZER_WITH_Z3= 
CLANG_BUILD_EXAMPLES=0 CLANG_DEFAULT_CXX_STDLIB= 
CLANG_TOOLS_DIR=/home/shakeel/devel/llvm-project/out/gn/bin 
CMAKE_CXX_COMPILER=c++ ENABLE_BACKTRACES=1 
LLVM_HOST_TRIPLE=x86_64-unknown-linux-gnu LLVM_LIT_TOOLS_DIR= 
LLVM_USE_SANITIZER= PYTHON_EXECUTABLE=python USE_Z3_SOLVER= 
CLANG_ENABLE_ARCMT=1 CLANG_ENABLE_STATIC_ANALYZER=1 HAVE_LIBZ=1 
HOST_ARCH=x86_64 LLVM_PLUGIN_EXT=.so
Traceback (most recent call last):

  File "../../llvm/utils/gn/build/write_cmake_config.py", line 108, in 
sys.exit(main())
  File "../../llvm/utils/gn/build/write_cmake_config.py", line 72, in main
in_line = var_re.sub(repl, in_line)
  File "../../llvm/utils/gn/build/write_cmake_config.py", line 71, in repl
return values[key]

KeyError: 'LLVM_WITH_Z3'
[2/3182] ACTION 
//llvm/include/llvm/Config:config(//llvm/utils/gn/build/toolchain:unix)
FAILED: gen/llvm/include/llvm/Config/config.h 
python ../../llvm/utils/gn/build/write_cmake_config.py -o 
gen/llvm/include/llvm/Config/config.h 
../../llvm/include/llvm/Config/config.h.cmake 
BUG_REPORT_URL=https://bugs.llvm.org/ ENABLE_BACKTRACES=1 
ENABLE_CRASH_OVERRIDES=1 BACKTRACE_HEADER=execinfo.h 
HAVE_CRASHREPORTERCLIENT_H= HAVE_DECL_FE_ALL_EXCEPT=1 HAVE_DECL_FE_INEXACT=1 
LLVM_ENABLE_DIA_SDK= LLVM_ENABLE_CRASH_DUMPS= HAVE_ERRNO_H=1 HAVE_FCNTL_H=1 
HAVE_FENV_H=1 HAVE_FFI_CALL= HAVE_FFI_FFI_H= HAVE_FFI_H= HAVE_LIBPFM= 
HAVE_LIBPSAPI= HAVE_MALLCTL= HAVE_SIGNAL_H=1 HAVE_STD_IS_TRIVIALLY_COPYABLE=1 
HAVE_STRERROR=1 HAVE_SYS_STAT_H=1 HAVE_SYS_TYPES_H=1 HAVE_VALGRIND_VALGRIND_H= 
HAVE__ALLOCA= HAVE___ALLOCA= HAVE___ASHLDI3= HAVE___ASHRDI3= HAVE___CHKSTK= 
HAVE___CHKSTK_MS= HAVE___CMPDI2= HAVE___DIVDI3= HAVE___FIXDFDI= HAVE___FIXSFDI= 
HAVE___FLOATDIDF= HAVE___LSHRDI3= HAVE___MAIN= HAVE___MODDI3= HAVE___UDIVDI3= 
HAVE___UMODDI3= HAVECHKSTK= HAVECHKSTK_MS= HOST_LINK_VERSION= 
LLVM_TARGET_TRIPLE_ENV= LLVM_VERSION_INFO= 
LLVM_VERSION_PRINTER_SHOW_HOST_TARGET_INFO=1 
PACKAGE_BUGREPORT=https://bugs.llvm.org/ PACKAGE_NAME=LLVM PACKAGE_STRING=LLVM\ 
9.0.0svn PACKAGE_VERSION=9.0.0svn PACKAGE_VENDOR= RETSIGTYPE=void 
LLVM_GISEL_COV_ENABLED= LLVM_GISEL_COV_PREFIX= 
LLVM_DEFAULT_TARGET_TRIPLE=x86_64-unknown-linux-gnu HAVE_FUTIMENS=1 
HAVE_LINK_H=1 HAVE_LSEEK64=1 HAVE_MALLINFO=1 HAVE_POSIX_FALLOCATE=1 
HAVE_SCHED_GETAFFINITY=1 HAVE_CPU_COUNT=1 HAVE_STRUCT_STAT_ST_MTIM_TV_NSEC=1 
HAVE_CRASHREPORTER_INFO= HAVE_DECL_ARC4RANDOM= HAVE_DLADDR= HAVE_MACH_MACH_H= 
HAVE_MALLOC_MALLOC_H= HAVE_MALLOC_ZONE_STATISTICS= 
HAVE_STRUCT_STAT_ST_MTIMESPEC_TV_NSEC= HAVE_BACKTRACE=1 HAVE_POSIX_SPAWN=1 
HAVE_PTHREAD_GETNAME_NP=1 HAVE_DECL_STRERROR_S= HAVE_DLFCN_H=1 HAVE_DLOPEN=1 
HAVE_FUTIMES=1 HAVE_GETPAGESIZE=1 HAVE_GETRLIMIT=1 HAVE_GETRUSAGE=1 
HAVE_ISATTY=1 HAVE_LIBPTHREAD=1 HAVE_PTHREAD_SETNAME_NP=1 HAVE_LIBZ=1 
HAVE_PREAD=1 HAVE_PTHREAD_GETSPECIFIC=1 HAVE_PTHREAD_H=1 
HAVE_PTHREAD_MUTEX_LOCK=1 HAVE_PTHREAD_RWLOCK_INIT=1 HAVE_REALPATH=1 
HAVE_SBRK=1 HAVE_SETENV=1 HAVE_SETRLIMIT=1 HAVE_SIGALTSTACK=1 HAVE_STRERROR_R=1 
HAVE_SYSCONF=1 HAVE_SYS_IOCTL_H=1 HAVE_SYS_MMAN_H=1 HAVE_SYS_PARAM_H=1 
HAVE_SYS_RESOURCE_H=1 HAVE_SYS_TIME_H=1 HAVE_TERMIOS_H=1 HAVE_UNISTD_H=1 
HAVE_ZLIB_H=1 HAVE__CHSIZE_S= HAVE__UNWIND_BACKTRACE=1 stricmp= strdup= 
LTDL_SHLIB_EXT=.so HAVE_LIBEDIT= HAVE_LIBXAR= HAVE_TERMINFO= LLVM_ENABLE_ZLIB=1 
LLVM_LIBXML2_ENABLED=1
Traceback (most recent call last):

  File "../../llvm/utils/gn/build/write_cmake_config.py", line 108, in 
sys.exit(main())
  File "../../llvm/utils/gn/build/write_cmake_config.py", line 72, in main
in_line = var_re.sub(repl, in_line)
  File "../../llvm/utils/gn/build/write_cmake_config.py", line 71, in repl
return values[key]

KeyError: 'LLVM_WITH_Z3'
[3/3182] ACTION 
//clang/include/clang/Config:Config(//llvm/utils/gn/build/toolchain:unix)
FAILED: gen/clang/include/clang/Config/config.h 
python ../../llvm/utils/gn/build/write_cmake_config.py -o 
gen/clang/include/clang/Config/config.h 
../../clang/include/clang/Config/config.h.cmake 
BUG_REPORT_URL=https://bugs.llvm.org/ CLANG_DEFAULT_LINKER= 
CLANG_DEFAULT_STD_C= CLANG_DEFAULT_STD_CXX= CLANG_DEFAULT_CXX_STDLIB= 

[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) installs an old version of 
Z3 that is incompatible with LLVM's tip of tree. To deal with this we add `-D 
CLANG_ANALYZER_ENABLE_Z3_SOLVER=OFF` to force disabling Z3 even if CMake 
detects the library is installed.

With this patch I am unable to disable Z3 because 
`CLANG_ANALYZER_ENABLE_Z3_SOLVER` is no longer in the codebase and setting `-D 
LLVM_ENABLE_Z3_SOLVER=OFF` still builds Z3 support (which fails):

  [74/187] Building CXX object 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  /usr/bin/clang++-6.0  -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE 
-D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS 
-Ilib/Support -I/tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support -I/usr/include/libxml2 
-Iinclude -I/tmp/tmp.UCDOJjmgJ1/src/llvm/include -fPIC 
-fvisibility-inlines-hidden -Werror=date-time 
-Werror=unguarded-availability-new -std=c++11 -Wall -Wextra 
-Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wmissing-field-initializers 
-pedantic -Wno-long-long -Wimplicit-fallthrough -Wcovered-switch-default 
-Wno-noexcept-type -Wnon-virtual-dtor -Wdelete-non-virtual-dtor 
-Wstring-conversion -fdiagnostics-color -ffunction-sections -fdata-sections -O3 
-DNDEBUG-fno-exceptions -fno-rtti -MD -MT 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -MF 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o.d -o 
lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -c 
/tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp
  /tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp:44:40: error: no 
matching function for call to 'Z3_get_error_msg'
 llvm::Twine(Z3_get_error_msg(Context, Error)));
 ^~~~


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-06 Thread Roman Lebedev via Phabricator via cfe-commits
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-commits and llvm-commits lists during review, which means it was 
essentially not reviewed by the wider audience.


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://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[PATCH] D54978: Move the SMT API to LLVM

2019-02-06 Thread Phabricator via Phabricator via cfe-commits
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=177582=185698#toc

Repository:
  rC Clang

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D54978/new/

https://reviews.llvm.org/D54978

Files:
  CMakeLists.txt
  cmake/modules/FindZ3.cmake
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/CMakeLists.txt
  lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/CMakeLists.txt
  test/lit.site.cfg.py.in

Index: lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
@@ -0,0 +1,18 @@
+//== SMTConstraintManager.cpp ---*- C++ -*--==//
+//
+// The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===--===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
+
+using namespace clang;
+using namespace ento;
+
+std::unique_ptr
+ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
+  return llvm::make_unique(Eng, StMgr.getSValBuilder());
+}
Index: lib/StaticAnalyzer/Core/CMakeLists.txt
===
--- lib/StaticAnalyzer/Core/CMakeLists.txt
+++ lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -1,12 +1,5 @@
 set(LLVM_LINK_COMPONENTS support)
 
-# Link Z3 if the user wants to build it.
-if(CLANG_ANALYZER_WITH_Z3)
-  set(Z3_LINK_FILES ${Z3_LIBRARIES})
-else()
-  set(Z3_LINK_FILES "")
-endif()
-
 add_clang_library(clangStaticAnalyzerCore
   APSIntType.cpp
   AnalysisManager.cpp
@@ -46,6 +39,7 @@
   SarifDiagnostics.cpp
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
+  SMTConstraintManager.cpp
   Store.cpp
   SubEngine.cpp
   SValBuilder.cpp
@@ -53,7 +47,6 @@
   SymbolManager.cpp
   TaintManager.cpp
   WorkList.cpp
-  Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST
@@ -63,12 +56,5 @@
   clangCrossTU
   clangLex
   clangRewrite
-  ${Z3_LINK_FILES}
   )
 
-if(CLANG_ANALYZER_WITH_Z3)
-  target_include_directories(clangStaticAnalyzerCore SYSTEM
-PRIVATE
-${Z3_INCLUDE_DIR}
-)
-endif()
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2411,7 +2411,7 @@
   VisitNode(EndPathNode, BRC, BR);
 
   // Create a refutation manager
-  SMTSolverRef RefutationSolver = CreateZ3Solver();
+  llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
   ASTContext  = BRC.getASTContext();
 
   // Add constraints to the solver
@@ -2419,7 +2419,7 @@
 const SymbolRef Sym = I.first;
 auto RangeIt = I.second.begin();
 
-SMTExprRef Constraints = SMTConv::getRangeExpr(
+llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
 RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
 /*InRange=*/true);
 while ((++RangeIt) != I.second.end()) {
Index: include/clang/Config/config.h.cmake
===
--- include/clang/Config/config.h.cmake
+++ include/clang/Config/config.h.cmake
@@ -54,9 +54,6 @@
 /* Define if we have libxml2 */
 #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}
 
-/* Define if we have z3 and want to build it */
-#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
-
 /* Define if we have sys/resource.h (rlimits) */
 #cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS}
 
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -18,7 +18,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
 typedef llvm::ImmutableSet<
-std::pair>
+std::pair>
 ConstraintSMTTy;
 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
 
@@ -26,7 +26,7 @@
 namespace ento {
 
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
-  mutable SMTSolverRef Solver = CreateZ3Solver();
+  mutable llvm::SMTSolverRef Solver =