[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356
                                    QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-    return UnknownVal();
----------------
zaks.anna wrote:
> I am concerned that removing the guard will regress performance in the vanilla case. (Note that Z3 support as well as taint are not on by default.)
> 
> I am curious how much of the regression you've measured could be gained back if we make this conditional.
To clarify, the changes made in this patch aren't specific to Z3 support, especially simplifying `SymbolCast` and `IntSymExpr`. With the exception of `PR24184.cpp` and `plist-macros.cpp`, all testcases pass with both the default and Z3 constraint managers. However, creating additional constraints does have performance overhead, and it may be useful to consider the parameters for gating this functionality.

On a combined execution (Range + Z3) through the testcases, except the two mentioned above, the runtime is 327 sec with this patch applied, and 195 sec without this patch applied. On a separate execution through the testcases with only the Z3 constraint manager, I get runtimes 320 and 191, respectively.

For testing purposes, I also tried the following code, which has combined runtime 311 sec, but loses the accuracy improvements with the Range constraint manager on `bitwise-ops.c`, `conditional-path-notes.c`, `explain-svals.cpp`, and `std-c-library-functions.c`.

```
ConstraintManager &CM = getStateManager().getConstraintManager();
if (!State->isTainted(RHS) && !State->isTainted(LHS) && !CM.isZ3())
```


================
Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:363
   // instead of generating an Unknown value and propagate the taint info to it.
-  const unsigned MaxComp = 10000; // 100000 28X
 
----------------
zaks.anna wrote:
> Reducing the MaxComp is going to regress taint analysis..
> 
> > I've updated this revision to account for the recent SVal simplification commit by @NoQ, 
> 
> Which commit introduced the regression?
> 
> > but now there is an exponential blowup problem that prevents testcase PR24184.cpp from terminating, 
> 
> What triggers the regression? Removing the if statement above? Does the regression only effect the Z3 "mode" (I am guessing not since you said "due to an interaction between Simplifier::VisitNonLocSymbolVal() and SValBuilder::makeSymExprValNN()")? 
> 
> Reducing the MaxComp is going to regress taint analysis..

I think the original intention was to increase `MaxComp`, not decrease it, but I will restore the original value here.

> What triggers the regression? Removing the if statement above? Does the regression only effect the Z3 "mode"

No, the regression isn't specifically due to this code, but with @NoQ 's patch for `SVal` simplification (rL300178), and this commit extending it to handle `SymbolCast` and `IntSymExpr`, the cast of `ST *` used in the loop of case 3 of PR24184.cpp becomes "simplified" (inlined) repeatedly on each recursive iteration through `Simplifier::VisitNonLocSymbolVal()` -> `SValBuilder::makeSymExprValNN()`, causing a big slowdown in runtime performance.

The naive way to prevent it is to drop `MaxComp` (but this isn't reasonable, since it needs to be absurdly low, e.g. `10`). Alternatively, simplification for `SymbolCast` can be dropped from this commit (but it will eliminate some of the other analysis improvements), or, most likely, introduce another parameter to reduce recursion between these two functions.


https://reviews.llvm.org/D28953