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

[Dominic Chen via cfe-dev]

It should be committed in rL311213.

Thanks,

Dominic

> On Aug 18, 2017, at 7:13 PM, Hans Wennborg <hans at chromium.org> wrote:
> 
> 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
>> 
>>