[cfe-commits] r163444 - in /cfe/trunk: lib/StaticAnalyzer/Core/ProgramState.cpp lib/StaticAnalyzer/Core/SymbolManager.cpp test/Analysis/traversal-path-unification.c

[Jordan Rose]

On Jan 2, 2013, at 13:24 , Ted Kremenek <kremenek at apple.com> wrote:

> Hi Jordan,
> 
> I'm going through my backlog of unread messages, and found this one.  My apologies for the delay in responding!  Comments inline.
> 
> On Sep 10, 2012, at 9:16 AM, Jordan Rose <jordan_rose at apple.com> wrote:
> 
>> I'm glad this was not an accident, because it would have been quite an oversight otherwise. As far as making sure we don't clean out constraints for symbols which are live but look dead:
>> 
>> (1) Region value symbols are live as long as their regions are live.
>> (2) Conjured symbols are live as long as there are bindings to them (and, right now, are only conjured for the current statement or an immediate subexpression).
>> (3) Derived symbols are live as long as their base symbol is live.
>> (4) Extent symbols are live as long as their region is live.
>> (5) Metadata symbols are live as long as their region is live AND they are marked in use by a checker.
>> 
>> (6) Symbolic expressions could be regenerated.
> 
> This all looks correct to me.
> 
>> 
>> Hm. Maybe this isn't a correct change after all. None of our tests broke, but that could just be an oversight, since we only started allowing constraints on symbolic expressions fairly recently.
>> 
>> It's unfortunate because keeping constraints around for dead symbols means paths don't merge very often, if at all -- usually the branch condition itself will lead to constraints on symbols that differ along each path.
> 
> I don't understand this statement.  We do clear our constraints for dead symbols.  Just some symbols need to stay around, per bullets 1-6.  Algorithmically, I think this is the correct behavior.

This was a long time ago, and at that point we were actually never clearing constraints for dead symbols. I added (back?) the missing call to do that, but found out that some of the conditions 1-6 weren't implemented correctly. A later commit fixed this (particularly #6), and this commit was reapplied. I can go dig up the Radar if you want.

> You are right that all of this impacts our opportunities to merge paths.  But if we need to keep a constraint, say because of a branch condition, then that is the right thing to do until that constraint is really no longer needed.  Otherwise we will just lose path-sensitivity.  The other option is to use techniques such as widening to forcefully remove constraints, and have a way of dealing with false positives such as using techniques like iterative refinement.


Our current behavior is to keep constraints on symbolic expressions around until one of the input symbols to the expression is dead (i.e. until the expression can no longer be regenerated).

Jordan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20130102/db2e9112/attachment.html>