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.

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.

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.

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#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:

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.

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:

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.

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.

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

In D50818#1206202, @george.karpenkov wrote:

@delcypher @ddcc @mikhail.ramalho Actually, I was thinking about another way of configuring Z3 without CMake entirely, and I would like to hear thoughts on how crazy that is.
What if we

• Remove all CMake checks
• Define the headers we need in the analyzer
• When initializing Z3 objects (done when Z3-visitor or Z3-solver is enabled), we would try to open the dylib, check it's version, and fail if the dylib is not found or the version does not match.

I recall that this problem extends beyond the Z3ConstraintManager. Have you looked at D28955, specifically the changes to BasicValueFactory.h?

I don't see any #ifdef for the tests. Do they pass both with and without z3? I recall needing to case out the expected test output before.

Yeah, I think it would be preferable to fix all three bugs here.

In D48324#1136921, @mikhail.ramalho wrote:

I think the correct type should always be ptrdiff_t, regardless of the type of the pointers involved. ASTContext has a method has a getPointerDiffType() so maybe we should you that instead of Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true)?

The code already tries to handle ptrdiff_t specially, see the comment right above, but it is only executed if RetTy is non-null. Instead, I think it should be refactored so that e.g. a local isBool is always computed, and this is passed to the final call to Z3Expr::fromBinOp.

LGTM

Correct me if I'm wrong, but isn't this function mostly duplicate with assumeSymInclusiveRange? I think it would be preferable to refactor out the constraint generation from both into e.g. getZ3RangeExpr, then modify both addRangeConstraints and assumeSymInclusiveRange to call it instead?

@ddcc To be completely honest, I see a few design issues with the current implementation of Z3 backend,
the main one being that it checks satisfiability after every single exploded node.
To the best of my knowledge, reasonable scalability would not be achieved with such an approach,
and I'm not sure how feasible would it be to change it without rewriting most of the checkers.

In D47726#1121395, @george.karpenkov wrote:

• Do all tests for Z3 run when LLVM is configured to use Z3? I'm not sure if that's the right thing: do all tests start to take 10x time to run once Z3 is enabled?

In D47640#1119273, @george.karpenkov wrote:

@ddcc any objections?

In D47617#1119257, @george.karpenkov wrote:

LGTM with a nit on a test name.

Add test, address comments

In D47603#1118138, @vlad.tsyrklevich wrote:

In D47603#1118106, @george.karpenkov wrote:

Would it be possible to add tests? I know we have very few unit tests, but I assume you could actually use an integration test to exercise this path?

I tested this change and it fixes PR37622. There's a simple crash reproducer included there.

In D35450#1116535, @george.karpenkov wrote:

@ddcc Hi, are you still interested in landing the fixes associated with this patch? I can take a look as I'm currently reviewing https://reviews.llvm.org/D45517, but it is likely that the patch would need to be changed substantially before it could land.

FYI the fix for the 1-bit APSInt issue is in https://reviews.llvm.org/D35450#change-ifYnQ3IlVso

@NoQ Does the proposal in https://reviews.llvm.org/D28955#652465 satisfy your concern?

@dcoughlin No, all three patches are separate. I have been testing them with each applied incrementally onto the previous, in the order trunk, D35450, D28954, then D28955 (this). But since these are a lot of dependencies, I've refactored this patch to apply directly on top of D35450, though the floating-point specific changes will need to be merged into D28954. Also, I think D28954 is waiting for review.

Rebase, factor out floating-point changes, fix Z3 type bug, support general APSInt comparison

All testcases pass, except the issue with range_casts.c. The cause is still the range intersection discussed in https://reviews.llvm.org/D35450#810469.

Rebase, make complexity limits configurable

@NoQ ping

Drop unnecessary code

As an aside, I think it'd be good to land D28954 and D28955 first, since they affect accuracy and precision of various analyzer parts that this depends on.

Revise based on feedback

Minor style fix

As an update, after fixing the typo and updating the tests, the assertion in range_casts.c is no longer triggered and everything seems fine now.

Fix tests after typo fix

Is diff 1 the original diff from D28953? It was ok to reopen it, but the new revision is also fine.

Fix typo

Compared with D28953, this revision fixes the test failure with PR3991.m with RangeConstraintManager, and a few other failures with Z3ConstraintManager. However, there's one remaining test failure in range_casts.c that I'm not sure how to resolve. For reference, this is the simplified code snippet from that testcase:

Modify Z3RangeConstraintManager::fixAPSInt() and add Expr::isCommutativeOp()

Reverted in rL307853

Split plist-macros.cpp, and update analyzer_test.py to support tests that require not z3

I've also uploaded the results to https://dcddcc.com/csa

I tested the following software, both before and after applying this patch, using RangeConstraintManager.

Drop duplicate code

ping

I forgot to mention that the only remaining (Z3) test failure is on plist-macros.cpp; there is a Assuming condition is true path note that only appears with the RangeConstraintManager but not with Z3ConstraintManager, and I can't #ifdef it because the annotations are checked by FileCheck.

Rebase, decrease simplification complexity

Can we drop computing these for some expressions that we know the RangeConstraintManager will not utilize?

@dcoughlin @zaks.anna @NoQ @xazax.hun Ping, I'd appreciate it if I could get a review for this (D33308), D28955, D28953, and D28954. Rebasing and fixing up these commits is fairly time consuming.

Rebase, avoid generating floating-point constraints if unsupported by constraint manager

Fix typo in SymbolCast simplification

I've updated this revision to account for the recent SVal simplification commit by @NoQ, but now there is an exponential blowup problem that prevents testcase PR24184.cpp from terminating, due to an interaction between Simplifier::VisitNonLocSymbolVal() and SValBuilder::makeSymExprValNN() when expanding the loop in case 3. I'm not quite sure what the best way to resolve this is; from some blind testing, I ended up needing to set MaxComp to 10 to force termination in a reasonable amount of time, but this restricts its usefulness for generating other symbolic constraints.

Address SVal simplification from D31886

In D28952#757375, @iris wrote:

Thank you for helping me build clang with z3.I have already applied the above updating.But now I have another question, when running clang with '-Xanalyzer -analyzer-constraints=z3' there is always be a fatal error and I don't know whether it is right to use a command like 'clang -Xanalyzer -analyzer-constraints=z3 -analyzer-checker=debug.DumpExplodedGraph test.cpp-' to get the ExplodedGraph which is analyzed by z3constraint?Sorry to bother.

In D28954#754478, @lirhea wrote:

In D28954#714936, @ddcc wrote:

Rebase, update tests, fix bugs

Excuse me,I want to download full codes of this version,but I have no idea how to do it,can you tell me?
And my system is windows, I haven't install anything about Phabricator.
Thank you!

Rebase

It's been a while since I looked at the code, but I don't believe that all of the new constraints are necessarily unsupported by the current range constraint manager. Rather, they were just not being generated by the SimpleSValBuilder. The changes pass the testsuite for both the Range and Z3 constraint managers, without any special testcase handling that is Z3 specific.

In D28952#750558, @iris wrote:

How can I make z3constraintmanager.cpp work in the command line?Or how to make z3 work?

@dcoughlin : ping

Thanks!

Fix support for 128-bit APInt creation, drop pkg-config from CMake module

Rebase

Rebase, update tests, fix bugs

Rebase

Fix erroneous comment

Thanks for the feedback! My main constraint is that the results from the floating-point analysis weren't very interesting (see #652894), so I'm not actively working on further development.

Use direct bitcasting instead of string conversion for APFloat casting, add reference counting for Z3_sort, eliminate some duplicate code

Thanks for your help! Let me know when the buildbot is ready for this to land.