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

[Dominic Chen via cfe-dev]

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