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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Because this patch affects the default behavior, i think it's necessary to understand the performance impact on a large codebase. I may lend a hand eventually, but if you're in a hurry you could probably at least run an overnight analysis over llvm and sqlite with range constraint manager and see how performance changes with this patch, and ideally also if we get new reports or lose old reports.

In https://reviews.llvm.org/D28953#785679, @ddcc wrote:

> I forgot to mention that the only remaining (Z3) test failure is on `plist-macros.cpp`; there is a `Assuming condition is true` path note that only appears with the RangeConstraintManager but not with Z3ConstraintManager, and I can't `#ifdef` it because the annotations are checked by `FileCheck`.


This test case could be separated into a different file if nothing else helps.



================
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
 
----------------
ddcc wrote:
> 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.
We talked a bit and we're pretty much fine with reduce `MaxComp` to 10 if it's worth it in terms of performance.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:997-1003
   if (SymbolRef Sym = V.getAsSymbol())
     return state->getConstraintManager().getSymVal(state, Sym);
 
-  // FIXME: Add support for SymExprs.
+  if (Optional<NonLoc> NV = V.getAs<NonLoc>())
+    if (SymbolRef Sym = NV->getAsSymExpr())
+      return state->getConstraintManager().getSymVal(state, Sym);
+
----------------
These two ifs are completely identical (apart from the fact that the one you added ignores symbolic region values due to explicit NonLoc cast). In fact `getAsSymbol()` (with its optional argument equal to `false`) and `getAsSymExpr()` are equivalent; we need to refactor this API.

I believe that the FIXME should in fact be addressed in `RangeConstraintManager`, in which currently `getSymVal()` works for atomic symbols only. Or, alternatively, we should stick `simplifySVal()` here - i think i'd have a look at this soon.

In any case, i suggest removing this change for now, unless i missed anything and it does in fact have an effect.


================
Comment at: test/Analysis/plist-macros.cpp:2
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
----------------
> `path-diagnostics-alternate=ture`

Ouch. Thanks for fixing this.

Maybe it'd be great to implement an option that enables validating analyzer config option values, and turn this option on in `%clang_analyze_cc1`.


https://reviews.llvm.org/D28953