[cfe-dev] Integration of Z3 for constraint solving [r299463]

[Hans Wennborg via cfe-dev]

Yes, that's excellent.

Would you like to commit that, or would you like me to do it for you?

Thanks,
Hans

On Fri, Aug 18, 2017 at 3:47 PM, Dominic Chen <d.c.ddcc at gmail.com> wrote:
> Is a short summary sufficient? For example, "The static analyzer now
> supports using the z3 theorem prover from Microsoft Research as an
> external constraint solver. This allows reasoning over more complex
> queries, but performance is ~15x slower than the default range-based
> constraint solver. To enable the z3 solver backend, clang must be built
> with the `CLANG_ANALYZER_BUILD_Z3=ON` option, and the `-Xanalyzer
> -analyzer-constraints=z3` arguments passed at runtime."
>
> Thanks,
>
> Dominic
>
> On 8/18/2017 6:30 PM, Hans Wennborg wrote:
>> Do you want to add something about this in the release notes?
>>
>> On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
>> <cfe-dev at lists.llvm.org> wrote:
>>> This is for the clang static analyzer, when performing symbolic
>>> execution on input C code. Since the variables are all fixed-width
>>> bitvectors, and there are no existential/universal quantifiers, in
>>> practice the performance is decent, although still slower than the
>>> current range-based constraint manager. However, it allows for reasoning
>>> over more complex queries, e.g. involving multiple symbolic variables,
>>> symbolic truncation/extension, and symbolic floating-point expressions
>>> (these are all follow-up patches that have not yet been merged). There's
>>> a longer discussion and more concrete performance numbers starting
>>> around comment https://reviews.llvm.org/D28952#652510 .
>>>
>>> Thanks,
>>>
>>> Dominic
>>>
>>> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>>>> Hi,
>>>>
>>>> I just noticed that Z3 was integrated into the clang frontend to solve
>>>> some kind of constraints: https://reviews.llvm.org/rL299463
>>>>
>>>> What kinds of constraints are these, i.e. which problem are they
>>>> solving, and is there a possibility of running into an exponential runtime?
>>>>
>>>> Kind regards,
>>>
>>> _______________________________________________
>>> cfe-dev mailing list
>>> cfe-dev at lists.llvm.org
>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>