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

[Anna Zaks via Phabricator via cfe-commits]

zaks.anna 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);
----------------
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.


https://reviews.llvm.org/D35450