[cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

[Mikhail Ramalho via cfe-dev]

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,

2018-03-11 12:57 GMT+00:00 Nuno Lopes via cfe-dev <cfe-dev at lists.llvm.org>:

> 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
>
>
> -----Original Message-----
> From: Dominic Chen via cfe-dev
> Sent: Thursday, March 8, 2018 10:13 PM
> Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver
>
> 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
>
> On 3/8/2018 4:46 PM, Dan Liew wrote:
>
>> Hi,
>>
>> On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
>> <cfe-dev at lists.llvm.org> wrote:
>>
>>> 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] https://github.com/Z3Prover/z3/issues/1035
>> [2] https://github.com/Z3Prover/z3/issues/1459
>> [3] https://github.com/Z3Prover/z3/issues/1053
>>
>> Thanks,
>> Dan.
>>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>



-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180311/812127d0/attachment.html>