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

[Dominic Chen via cfe-dev]

Just realized I meant input code, there's nothing specific to just C.

Dominic

On 4/10/2017 3:21 PM, Dominic Chen 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,
>