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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Late-joining the round of applause for the awesome progression of this project!

Not sure how to deal with the massive test run-line changes at the moment, will take some extra time to think.

In https://reviews.llvm.org/D28952#652436, @ddcc wrote:

> Another issue is that some testcases will have different results depending on the constraint manager in use, but I don't believe it's possible to change the expected testcase output based on the presence of a feature flag. Unless this changes, there'll need to be (mostly) duplicate testcases for each constraint manager.


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

.

In https://reviews.llvm.org/D28952#652436, @ddcc wrote:

> Furthermore, this and the child patches will cause the static analyzer to generate more complex constraints at runtime. But, I'm not sure if just having RangeConstraintManager ignore unsupported constraints will be sufficient, from a performance and correctness perspective.


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.


https://reviews.llvm.org/D28952