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

[Hans Wennborg via cfe-dev]

Perfect, thanks!

On Fri, Aug 18, 2017 at 5:11 PM, Dominic Chen <d.c.ddcc at gmail.com> wrote:
> 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
>>>
>>>
>