Em qui., 15 de out. de 2020 às 07:25, Ella Ma via Phabricator <
reviews@reviews.llvm.org> escreveu:

Hi, sorry for the delay.

This is actually failing on another machine I have because of the lib name. This fixes it:

 -----------------------
index a571d269b39..2da2f203a28 100644
@@ -57,9 +57,7 @@ endif()

LGTM!

LGTM

In D86223#2231991, @steakhal wrote:

In D86223#2231959, @mikhail.ramalho wrote:

I don't mind having it for release builds as well, why are you applying it only for debug builds?

It might introduce a slight overhead since Z3 will parse longer the symbol names.

I don't mind having it for release builds as well, why are you applying it only for debug builds?

Do you have permission to push the patch? Otherwise, I can push it.

Nice work, @steakhal!

Update the condition to flag an issue.

Two changes:

I can give some help here, but my time is quite limited as well :/

Hi, I just found this revision.

In D54978#1447107, @gou4shi1 wrote:

My own out-of-tree pass #include <llvm/Support/SMTAPI.h> 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.

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.

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!

! In D54978#1440464, @ddcc wrote:

Do you know if this configuration builds fine now?

Fixed.

Fix copy-and-paste error.

Hi all,

Updated script to parse Z3's headers and changed the workflow to handle cross compilation cases.

Fixes:

• FindZ3.cmake format .
• Wrong SMTExpr namespace in SMTConstraintManager.h.

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.

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"

Hi all,

Update Z3 script to use cmake's try_run in order to retrieve the version from the lib.

Hi guys,

Update FindZ3.cmake to do a runtime check of the version.

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.

Looks like my last email got lost:

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.

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

@brzycki, I can't reproduce your error. Maybe you're missing -DLLVM_ENABLE_Z3_SOLVER=OFF?

Reopening the revision as it was reverted.

@michaelplatings, thanks for the report.

Hi everyone, I just saw your messages and reverted the commits.

ping

Updates:

• Don't abort cmake if enabling Z3 but not the CSA.
• Fixed guards in llvm/Support/SMTAPI.h
• Moved using namespace llvm; to outside the #if

• Updated patch due to changes in D54976.

In the future, CreateZ3Solver should be renamed CreateSMTSolver to handle all backends.

In D54977#1310620, @george.karpenkov wrote:

The advantage is it's easier to find stuff with a 1-1 correspondence between class names and files.
Thus for this change I see a disadvantage and no clear advantages.

In D54975#1310619, @george.karpenkov wrote:

TBH this seems overly complicated. Z3 already hash-conses all objects; I don't think there is benefit of doing it again on the LLVM side.

What is the benefit from this patch, apart from being able to use ImmutableSet?

Since we're supporting version 4.8.1 now, the cmake file should be changed to "minimum" instead of "exact".

It doesn't make any difference in practice, for now.

Hey guys, the assertion is being triggered for me (I'm using clang r342322):

$ cat ~/main.c
void foo(unsigned width)
{
  int base;
  int i = 0;

Nit. Rename this something like CLANG_ANALYZER_Z3_INSTALL_PREFIX. The

description is also not very accurate

• Again this is an install prefix, just saying prefix is too vague.
• Z3 is a constraint solver, not a constraint manager.
• builds the static analyzer? I presume you mean this option being on

implies the static analyzer is built? Maybe say `Implies
CLANG_ANALYZER_BUILD_Z3`?

Prefix is the location where Z3 is installed on the machine. You can see
it's used in FindZ3.cmake:

Yeah, although the C API is considered to be fairly stable, it looks like a bunch of types have changed around recently. As of Z3 4.8.0, they've moved to stdbool.h and stdint.h, so I believe there's a couple of reinterpret_cast that can be removed from the code now. It looks like Z3_bool is also now typedef'd to a bool instead of an int. The configuration options can also be bit unstable, and my impression is that they've changed around over time.

Add comment to the cache member

I can't comment on the code but it works correctly for me.

Uhm, dunno, plist/FileCheck tests are annoying. What i usually do to make sense out of them is update the tested output with the actual output and look at git diff. From that it's usually obvious what exactly happened (warnings added, warnings removed, warnings moved to a different location, intermediate diagnostics added, intermediate diagnostics removed, intermediate diagnostics moved to a different location). Could you do that and see if it makes sense or attach the diff here so that we could have a look?

I getting the following error when analyzing test/Analysis/plist-macros.cpp, usign z3 as constraint manager (-analyzer-constraints=z3 -DANALYZER_CM_Z3):

/home/mgadelha/llvm/tools/clang/test/Analysis/plist-macros.cpp:640:16: error: CHECK-NEXT: expected string not found in input
// CHECK-NEXT: <key>line</key><integer>36</integer>
               ^
/home/mgadelha/llvm/build/tools/clang/test/Analysis/Output/plist-macros.cpp.tmp.plist:562:2: note: scanning from here
 <key>line</key><integer>37</integer>
 ^

Added a comment explaining why we have a weird if condition in toAPSInt.

It fixes Xerces verification. Thanks.