[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

[Dominic Chen via Phabricator via cfe-commits]

ddcc added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364
   if (symLHS && symRHS &&
-      (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+      (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
     return makeNonLoc(symLHS, Op, symRHS, ResultTy);
----------------
zaks.anna wrote:
> ddcc wrote:
> > zaks.anna wrote:
> > > As a follow up to the previous version of this patch, I do not think we should set the default complexity limit to 10000.
> > > 
> > > What is the relation between this limit and the limit in VisitNonLocSymbolVal? If they are related, would it be worthwhile turning these into an analyzer option?
> > To clarify, the current version of this patch does not modify the `MaxComp` parameter.
> > 
> > My understanding is that `MaxComp` is the upper bound for building a new `NonLoc` symbol from two children, based on the sum of the number of child symbols (complexity) across both children.
> > 
> > In contrast, the limit in `VisitNonLocSymbolVal` (@NoQ, correct me if I'm wrong), is the upper bound for recursively evaluating and inlining a `NonLoc` symbol, triggered from `simplifySVal` by `evalBinOpNN`. Note that these two latter functions indirectly call each other recursively (through `evalBinOp`), causing the previous runtime blowup. Furthermore, each call to `computeComplexity`will re-iterate through all child symbols of the current symbol, but only the first complexity check at the root symbol is actually necessary, because by definition the complexity of a child symbol at each recursive call is monotonically decreasing.
> > 
> > I think it'd be useful to allow both to be configurable, but I don't see a direct relationship between the two.
> > To clarify, the current version of this patch does not modify the MaxComp parameter.
> 
> I know. Also, currently, it is only used in the unsupported taint tracking mode and only for tainted symbols. I would like a different smaller default for all expressions.
Ok. I can make both configurable as part of this patch, with a new default of 10 for `VisitNonLocSymbolVal`. But I've never used the taint tracking mode, so I don't know what would be a reasonable default for `MaxComp`.


https://reviews.llvm.org/D35450