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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

I tested the following software, both before and after applying this patch, using RangeConstraintManager.

Software, Version, Compile Time (before), Bugs Reported (before), Compile Time (after), Bugs Reported (after)
openssl, 1.1.0f, 11 min, 126, 12 min, 126
sqlite, 3.18.2, 31 min, 86, 31 min, 82
wireshark, 2.2.7, 105 min, 109, 119 min, 108

For sqlite, the differences of four reported bugs all appear to be false positives, but for wireshark, the one difference appears to be a false negative.



================
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
 
----------------
NoQ wrote:
> 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.
Just to clarify, the current change from 100 to 10 in `simplifySVal::SimplyVisitNonLocSymbolVal` resolves the problem; the value of `MaxComp` here is unchanged.


================
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
----------------
NoQ wrote:
> > `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`.
I agree that'd be useful, but I think that it should be a separate future patch.


https://reviews.llvm.org/D28953