[GSOC 2018] Integrate with Z3 SMT solver

Hello,

I looked at the references on this mail http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html and then looked at Z3ConstraintManager.cpp and I have some questions regarding the solver:

  1. Right now we are not letting Z3 manage memory. Will it be a good idea to do that?

  2. Can we flush the cache memory in the destructor of Z3Solver https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834 class?

Thank you very much,
Ashish Kumar Gahlot

I’m not sure what you mean by letting Z3 manage memory. Unless something has changed significantly since I looked at the source, the Z3 C++ API simply wraps memory management functions from the lower-level Z3 C API using C++ objects. Since the constraint manager is using the C API, due to compatibility issues with RTTI and exceptions, it needs to call the appropriate memory management functions.

Likewise, I’m not sure what cache memory you’re referring to. There was some discussion of a SMT query cache in CSA, but I don’t believe that was ever implemented.

Dominic

Hi,

I’m not sure what you mean by letting Z3 manage memory. Unless something has
changed significantly since I looked at the source, the Z3 C++ API simply
wraps memory management functions from the lower-level Z3 C API using C++
objects. Since the constraint manager is using the C API, due to
compatibility issues with RTTI and exceptions, it needs to call the
appropriate memory management functions.

I think he probably means the reference counting Z3_context. Z3
provides two ways to create a context.
`Z3_mk_context()` makes a context where the reference counting of
Z3_ast objects is done automatically, but the reference counting of
other objects (e.g. Z3_model) still need to be done manually.
`Z3_mk_context_rc()` makes a context where everything (including
`Z3_ast` objects) must be manually reference counted.

The Z3 C++ API actually now supports being used with exceptions and
RTTI. However I still think the C API is the better choice because its
more stable.

In KLEE we use `Z3_mk_context_rc()` because we want to be able to
cache expressions but we don't want to do so indefinitely (i.e. we
want to control when the reference counts goes to zero and memory gets
freed).

Likewise, I’m not sure what cache memory you’re referring to. There was some
discussion of a SMT query cache in CSA, but I don’t believe that was ever
implemented.

@Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
internal expression cache that it uses when `Z3_mk_context()`? is
used. This gets cleared when the created expressions go out of scope
when `Z3_solver_pop()` gets used.

@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.

Actually there is a third way... If you create your own custom tactic
you will by-pass Z3's internal logic for trying to set up own solving
strategy. I think if you use push/pop with a custom tactic you'll
by-pass incremental solving
and likely get better performance.

Note in KLEE we end up creating a new `Z3_solver()` object for every
solver query. This isn't great but you have to do this (or use
`Z3_solver_reset()`) to clear the assertion stack without using
push/pop.
Because we don't use push/pop this necessitates that we do reference
counting manually (otherwise we'd never free Z3_asts until the
Z3_context gets destroyed).

[1] Unexpected huge performance difference between solver using "default" tactic, Z3_mk_solver() and Z3_mk_simple_solver() · Issue #1035 · Z3Prover/z3 · GitHub
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Thanks,
Dan.

Yes, I recall Nuno Lopes made a similar comment about the effect of
pushes and pops on the internal solver state, and that the performance
can differ depending on the workload. In fact, the initial
implementation did recreate the solver for each satisfiability query,
but it ended up being slower than the current version that reuses the
solver state.

Dominic

Hello,

Thank you for the detailed explanation.

Hello,

Thank you for the detailed explanation.

It does not recompile everything, whenever you type “ninja clang” (or “make clang”)
from the build folder it only recompiles the changed file and does the relinking.
Headers are a different story — then it has to recompile all the files that transitively include that header,
unfortunately, nothing that can be done there.

Hello,

I am having some doubts regarding the z3 constraint manager:

  1. what is the correct way of invoking the z3 constraint on a c++/c file. Right now I am using clang -cc1 -analyzer-constraints=z3 -analyze -analyzer-checker=core,unix,debug.ExprInspection -verify /root/clang-llvm/llvm/tools/clang/test/Analysis/region-store.c which reports WARNING: unknown parameter ‘timeout’
    Legal parameters are:
    auto_config (bool) (default: true)
    debug_ref_count (bool) (default: false)

……

I also tried the syntax mentioned in the last comment here but it gives the same error mentioned above.

  1. when I remove timeout option from Z3Config(), the output is null. Is it the correct behavior?

  2. how can I test the performance of the analyzer when I make changes in Z3ConstraintManager.cpp?

Thank you very much,
Ashish Kumar Gahlot

The implementation of the incremental stuff has improved in Z3 in the past year. Now the "fast" SAT solver supports a bit of incrementally. So the major difference now is that with push() you switch to the SMT solver that does lazy bit-blasting and the new solver does it eagerly for the whole formula.
BTW, there's a 3rd option which is to reset the solver.

I agree that going with a custom tactic is the way to go. Otherwise you are exposed to changes in the internals of Z3 and you never know what's running underneath. Also, you can tune the set of tactics for the formulas that clang generates. I can help with this if there's interest.

Nuno

Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don’t use the incremental mode); maybe that’s something to try on clang.

Thank you,

Interesting, thanks for the update. I'm not actively working on
Z3ConstraintManager, so anyone interested should go for it. There's
plenty of room for performance improvements.

Dominic

Hello,

Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don’t use the incremental mode); maybe that’s something to try on clang.

Can you tell me how do you perform those tests?

Thank you,

Ashish Kumar Gahlot

Hello all,

I was looking at Klee source and found that there was an API change in Z3 4.4.1 in function Z3_get_error_msg().
Since Z3 4.6.0 is already released, would it be useful to provide backward compatibility?

Thank you,

Ashish Kumar Gahlot