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

Wed Mar 14 00:32:08 PDT 2018

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

On Mon, Mar 12, 2018 at 12:48 PM, Ashish Gahlot <dreamashish21 at gmail.com>
wrote:

> 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
>

-- 
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/20180314/722a8fbe/attachment.html>