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

[Dominic Chen via cfe-dev]

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,