Integration of Z3 for constraint solving [r299463]

Clang Frontend
1

Hi,

I just noticed that Z3 was integrated into the clang frontend to solve
some kind of constraints: rG08f943c5630d

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,

2

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

3

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

Dominic

4

Ah, interesting. Thanks for the explanation. That's what I needed to know.

5

Do you want to add something about this in the release notes?

6

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

7

Yes, that's excellent.

Would you like to commit that, or would you like me to do it for you?

Thanks,
Hans

8

It should be committed in rL311213.

Thanks,

Dominic

9

Perfect, thanks!