[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:
> 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.


https://reviews.llvm.org/D35450