[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

> For such test cases i'd consider something like this:
> 
>   // RUN: ... -analyzer-constraints=range -DRANGE ...
>   // RUN: ... -analyzer-constraints=z3 ...
>   
>   #ifdef RANGE
>   foo(); // expected-warning{{}}
>   #else
>   foo(); // no-warning
>   #endif

Would this be assuming that the test setup has Z3 installed and both constraint managers available? I see that `llvm-lit` supports a `REQUIRES` directive, but I don't know if that can be scoped to just one `RUN`.

> Yep, the analyzer core has a lot of code that says "we denote this value with an incorrect symbol here, because even if we provided the correct symbol it would be too hard for the RangeConstraintManager to understand". The most obvious place is the integral cast code, which leaves the symbol intact *most* of the time (all the time until recently).
> 
> I think the right way to address these issues is introduce an API in the base ConstraintManager interface to ask the solver if he implements a certain feature or is capable of dealing with a particular kind of symbol, and change our behavior accordingly. We already have one function that was intended to do something like this - `ConstraintManager::canReasonAbout()`; not sure if it's working or broken.

`canReasonAbout()` works fine, but in its current form, requires parsing each constraint to determine whether its supported or not. In https://reviews.llvm.org/D26061, I've pushed the implementation from SimpleConstraintManager into RangeConstraintManager itself, since Z3ConstraintManager will also inherit from SimpleConstraintManager but with a different feature set. However, even with these changes, `canReasonAbout()` is only called from within SimpleConstraintManager; the feedback doesn't go all the way back to e.g. SimpleSValBuilder to dynamically change the constraint complexity at runtime.


https://reviews.llvm.org/D28952