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

Mon Mar 12 00:18:35 PDT 2018

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

On Mon, Mar 12, 2018 at 1:09 AM, Mikhail Ramalho via cfe-dev <
cfe-dev at lists.llvm.org> wrote:

> 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.
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>

-- 
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180312/2b4446df/attachment.html>