ddcc added a comment.
This is a fairly large patch, but the core of it is the actual implementation
of the Z3 constraint solver backend. In its current form, the backend is
implemented as a Clang plugin, but I also have a git commit that has it inside
the static analyzer. The non-plugin approa
rgov added a comment.
Do you think you could upload the patch omitting all of the test case changes
for now? Maybe include one as an example but it seems to be just adding
`%z3_cc1` so we don't need to see all of them right now.
The KLEE project has a useful abstraction layer around multiple bi
a.sidorin added a comment.
Amazing work, Dominic. That's what I wanted to test for long time. But,
personally, I'm not happy with massive changes in tests.
1. I don't think that we need to change run line for tests if they pass with
both managers. These changes are pretty noisy,
2. If Z3 is opt
ddcc added a comment.
Do you want me to replace this version of the patch with one that omits the
test case changes? The underlying git commit for just the Z3 constraint manager
implementation is
https://github.com/ddcc/clang/commit/e1414d300882c1459f461424d3e89d1613ecf03c ,
and
https://githu
NoQ added a comment.
Late-joining the round of applause for the awesome progression of this project!
Not sure how to deal with the massive test run-line changes at the moment, will
take some extra time to think.
In https://reviews.llvm.org/D28952#652436, @ddcc wrote:
> Another issue is that so
ddcc added a comment.
> For such test cases i'd consider something like this:
>
> // RUN: ... -analyzer-constraints=range -DRANGE ...
> // RUN: ... -analyzer-constraints=z3 ...
>
> #ifdef RANGE
> foo(); // expected-warning{{}}
> #else
> foo(); // no-warning
> #endif
Would this b
zaks.anna added a comment.
Thanks for working on this Dominic!!!
Can you talk a bit about your motivation for working on this project and what
your goals are?
Have you compared the performance when using Z3 vs the current builtin solver?
I saw that you mention performance issues on large codeb
nlopes added a comment.
Cool work Dominic!
Just a few random comments from the peanut gallery regarding the usage of Z3:
- I would definitely split the Z3Expr into expr/solver/model classes. Several
advantages: plugging in new solvers becomes easier and reference counting can
be handled more sa
ddcc updated this revision to Diff 85313.
ddcc added a comment.
Convert to plugin, add move/assignment constructor, avoid Z3_simplify(), use
Z3_mk_simple_solver(), generate logical and of all constraints in solver
https://reviews.llvm.org/D28952
Files:
CMakeLists.txt
cmake/modules/FindZ3.c
ddcc added a comment.
I'd like to note that one of the main challenges with this implementation was
needing to perform type reinference and implicit casting within the constraint
manager, since the constraints are sometimes implicit. (e.g. `(int) x` instead
of `x == 0`). It also didn't help tha
dcoughlin added a comment.
This is super-exciting work!
Some high-level notes:
- The running-time numbers you report are very high. At a ~20x slowdown, the
benefits from improved solver reasoning will have to be very, very large to
justify the performance cost. It is worth thinking about ways
ddcc added a comment.
> - That said, I think there are still significant optimization opportunities.
> It looks like when performing a query you create a new solver for each set of
> constraints. My understanding (and perhaps @nlopes can correct me here) is
> that these days Z3 is quite good at
ddcc updated this revision to Diff 85621.
ddcc added a comment.
Add CMake CLANG_BUILD_Z3 option, add Z3Model and Z3Solver classes, reuse solver
in checkNull() and getSymVal()
https://reviews.llvm.org/D28952
Files:
CMakeLists.txt
cmake/modules/FindZ3.cmake
include/clang/Config/config.h.cm
dcoughlin added a comment.
In https://reviews.llvm.org/D28952#655278, @ddcc wrote:
> > - That said, I think there are still significant optimization
> > opportunities. It looks like when performing a query you create a new
> > solver for each set of constraints. My understanding (and perhaps @n
nlopes added a comment.
Regarding incremental solving with Z3 (or with most SMT solvers in general),
let me just lower the expectations a bit:
In Z3, when you do push(), there are a few things that change immediately: 1)
it uses a different SAT solver (one that supports incremental reasoning), a
ddcc added a comment.
> Regarding incremental solving with Z3 (or with most SMT solvers in general),
> let me just lower the expectations a bit:
Ok, that is good to know. It seems that the performance benefits of incremental
solving are unclear, and would be nontrivial to implement (maybe stor
nlopes added a comment.
Let me give just 2 more Z3-related suggestions:
- instead of re-creating the solver, it might be faster to do Z3_solver_reset
- "once in a while" it might be helpful to delete everything (all solvers,
asts, context) and call Z3_reset_memory. Z3's small object pool is not
ddcc added a comment.
In https://reviews.llvm.org/D28952#659728, @nlopes wrote:
> Let me give just 2 more Z3-related suggestions:
>
> - instead of re-creating the solver, it might be faster to do Z3_solver_reset
> - "once in a while" it might be helpful to delete everything (all solvers,
> asts,
ddcc added a comment.
I added support for a callback field in lit's configuration (see
https://reviews.llvm.org/D29684), which is used to execute each testcase for
each supported constraint solver backends at runtime. I believe this resolves
all remaining issues, except for the remaining two te
dcoughlin added a comment.
Thanks for updating the tests to be able to run both the z3 and
range-constraint managers! I think this will make it much easier to ensure the
z3-backed manager continues to work as as expected moving forward. I suggested
an alternative approach inline to running the
iris added a comment.
How can I make z3constraintmanager.cpp work in the command line?Or how to make
z3 work?
Repository:
rL LLVM
https://reviews.llvm.org/D28952
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-b
ddcc added a comment.
In https://reviews.llvm.org/D28952#750558, @iris wrote:
> How can I make z3constraintmanager.cpp work in the command line?Or how to
> make z3 work?
You'll need a bleeding-edge build of Clang/LLVM, since this isn't available in
any stable release yet. First, build or inst
iris added a comment.
In https://reviews.llvm.org/D28952#751431, @ddcc wrote:
> In https://reviews.llvm.org/D28952#750558, @iris wrote:
>
> > How can I make z3constraintmanager.cpp work in the command line?Or how to
> > make z3 work?
>
>
> You'll need a bleeding-edge build of Clang/LLVM, since t
ddcc added a comment.
In https://reviews.llvm.org/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 er
delcypher added a comment.
I'm a little late to the review but hopefully I'll have useful comments. Nice
work @ddc
> I looked around for a generic smt-lib interface earlier, but couldn't find
> much available, and since I wanted floating-point arithmetic support, I ended
> up just directly usi
delcypher added a comment.
In https://reviews.llvm.org/D28952#655337, @dcoughlin wrote:
> In https://reviews.llvm.org/D28952#655278, @ddcc wrote:
>
> > > - That said, I think there are still significant optimization
> > > opportunities. It looks like when performing a query you create a new
> >
delcypher added inline comments.
Comment at: CMakeLists.txt:188
+find_package(Z3 4.5)
+
@ddcc It is of course up to you but I recently [[ added support for using
`libz3` directly | added support for using `libz3` directly ]] from CMake. via
it's own CMake con
delcypher added inline comments.
Comment at: CMakeLists.txt:188
+find_package(Z3 4.5)
+
delcypher wrote:
> @ddcc It is of course up to you but I recently [[ added support for using
> `libz3` directly | added support for using `libz3` directly ]] from CMake.
>
ddcc updated this revision to Diff 93587.
ddcc marked 4 inline comments as done.
ddcc added a comment.
Use direct bitcasting instead of string conversion for APFloat casting, add
reference counting for Z3_sort, eliminate some duplicate code
https://reviews.llvm.org/D28952
Files:
CMakeLists.t
ddcc added a comment.
Thanks for the feedback! My main constraint is that the results from the
floating-point analysis weren't very interesting (see #652894 <#652894>), so
I'm not actively working on further development.
> FYI I've been working on floating point support in KLEE and have extende
ddcc updated this revision to Diff 93588.
ddcc added a comment.
Fix erroneous comment
https://reviews.llvm.org/D28952
Files:
CMakeLists.txt
cmake/modules/FindZ3.cmake
include/clang/Config/config.h.cmake
include/clang/StaticAnalyzer/Core/Analyses.def
include/clang/StaticAnalyzer/Core/P
delcypher added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:559
+ Float.toString(Chars, 0, 0);
+ AST = Z3_mk_numeral(Z3Context::ZC, Chars.c_str(), Sort);
+ break;
ddcc wrote:
> delcypher wrote:
> > @ddcc I'm not con
delcypher added inline comments.
Comment at: cmake/modules/FindZ3.cmake:3
+# in the find_path() and find_library() calls
+find_package(PkgConfig QUIET)
+PKG_CHECK_MODULES(PC_Z3 QUIET libz3)
@ddcc Seeing as you don't want to use the new upstream Z3 CMake package c
delcypher added inline comments.
Comment at: CMakeLists.txt:188
+find_package(Z3 4.5)
+
ddcc wrote:
> delcypher wrote:
> > delcypher wrote:
> > > @ddcc It is of course up to you but I recently [[ added support for using
> > > `libz3` directly | added support f
delcypher added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:619
+
+llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
+Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
@ddcc Why use APSInt here? Why not APInt, we are lo
ddcc added inline comments.
Comment at: cmake/modules/FindZ3.cmake:3
+# in the find_path() and find_library() calls
+find_package(PkgConfig QUIET)
+PKG_CHECK_MODULES(PC_Z3 QUIET libz3)
delcypher wrote:
> @ddcc Seeing as you don't want to use the new upstream Z3 C
delcypher added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:674
+ // are the same size.
+ Z3_get_numeral_uint64(Z3Context::ZC, AST,
+reinterpret_cast<__uint64 *>(&Value));
ddcc wrote:
> The on
delcypher added inline comments.
Comment at: cmake/modules/FindZ3.cmake:5
+PKG_CHECK_MODULES(PC_Z3 QUIET libz3)
+set(Z3_DEFINITIONS ${PC_LIBZ3_CFLAGS_OTHER})
+
ddcc wrote:
> delcypher wrote:
> > @ddcc This CMake variable is set but never used. Also based on the n
ddcc updated this revision to Diff 93974.
ddcc added a comment.
Fix support for 128-bit APInt creation, drop pkg-config from CMake module
https://reviews.llvm.org/D28952
Files:
CMakeLists.txt
cmake/modules/FindZ3.cmake
include/clang/Config/config.h.cmake
include/clang/StaticAnalyzer/Cor
dcoughlin added a comment.
Dominic: I don't have a bot set up yet, but let's get this committed. Thanks
for all your hard work on this!
https://reviews.llvm.org/D28952
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cg
This revision was automatically updated to reflect the committed changes.
Closed by commit rL299463: [analyzer] Add new Z3 constraint manager backend
(authored by ddcc).
Changed prior to commit:
https://reviews.llvm.org/D28952?vs=93974&id=94107#toc
Repository:
rL LLVM
https://reviews.llvm.o
dcoughlin accepted this revision.
dcoughlin added a comment.
This revision is now accepted and ready to land.
Dominic, this (https://reviews.llvm.org/D28952) and
https://reviews.llvm.org/D26061 look get to me! Let's get these two committed!
We'd like to get to a place where in-tree incremental
ddcc added a comment.
Sounds good, I will commit https://reviews.llvm.org/D26061 and split out the
tests from this (https://reviews.llvm.org/D28952).
https://reviews.llvm.org/D28952
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lis
ddcc updated this revision to Diff 89777.
ddcc added a comment.
Drop tests, move to https://reviews.llvm.org/D30373
https://reviews.llvm.org/D28952
Files:
CMakeLists.txt
cmake/modules/FindZ3.cmake
include/clang/Config/config.h.cmake
include/clang/StaticAnalyzer/Core/Analyses.def
inclu
ddcc added a comment.
Thanks for your help! Let me know when the buildbot is ready for this to land.
https://reviews.llvm.org/D28952
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
xazax.hun added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:60
+// Set timeout to 15000ms = 15s
+Z3_set_param_value(Config, "timeout", "15000");
+ }
Sorry for being a bit late in the party, I was wondering whether this ti
ddcc added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:60
+// Set timeout to 15000ms = 15s
+Z3_set_param_value(Config, "timeout", "15000");
+ }
xazax.hun wrote:
> Sorry for being a bit late in the party, I was wondering w
47 matches
Mail list logo
