- User Since
- Jun 17 2016, 7:04 PM (165 w, 5 d)
Mar 25 2019
Mar 23 2019
Mar 18 2019
Mar 16 2019
Mar 15 2019
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.
Feb 13 2019
Feb 12 2019
Feb 11 2019
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 ).
Nov 11 2018
Aug 20 2018
Aug 16 2018
Aug 15 2018
Jul 13 2018
I recall that this problem extends beyond the Z3ConstraintManager. Have you looked at D28955, specifically the changes to BasicValueFactory.h?
Jun 27 2018
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.
Jun 20 2018
Yeah, I think it would be preferable to fix all three bugs here.
Jun 19 2018
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.
Jun 16 2018
Jun 15 2018
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?
Jun 4 2018
@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.
Jun 1 2018
May 31 2018
Add test, address comments
May 30 2018
May 26 2018
FYI the fix for the 1-bit APSInt issue is in https://reviews.llvm.org/D35450#change-ifYnQ3IlVso
Sep 1 2017
@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
Aug 31 2017
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
Aug 28 2017
Aug 25 2017
Aug 18 2017
Aug 5 2017
Jul 19 2017
Drop unnecessary code
Revise based on feedback
Jul 18 2017
Minor style fix
Jul 17 2017
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.
Jul 15 2017
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()
Jul 14 2017
Jul 12 2017
Reverted in rL307853
Jul 11 2017
Split plist-macros.cpp, and update analyzer_test.py to support tests that require not z3
Jul 10 2017
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
Jul 5 2017
Jun 20 2017
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?
Jun 15 2017
Jun 10 2017
May 18 2017
Rebase, avoid generating floating-point constraints if unsupported by constraint manager
Fix typo in SymbolCast simplification
May 17 2017
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
May 14 2017
May 10 2017
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.
May 5 2017
@dcoughlin : ping
Apr 6 2017
Apr 4 2017
Apr 3 2017
Fix support for 128-bit APInt creation, drop pkg-config from CMake module
Mar 31 2017
Mar 30 2017
Rebase, update tests, fix bugs
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
Mar 21 2017
Mar 6 2017
Thanks for your help! Let me know when the buildbot is ready for this to land.