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

[Jordan Rose]

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.

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.

Any ideas?
Jordan


On Sep 9, 2012, at 21:35 , Ted Kremenek <kremenek at apple.com> wrote:

> I now recall that these were intentionally not cleaned from the ProgramState, so this at least wasn't an accidental bug.  That said, I now think this is the right thing to do, as long as we design for the point were there are some symbols that can be re-conjured later in a path.  For such symbols, we should just treat them as being always live.
> 
> On Sep 9, 2012, at 1:38 PM, Ted Kremenek <kremenek at apple.com> wrote:
> 
>> I'm now wondering if this is correct.  If it is possible for a symbol to get conjured a second time along a path, even after all the original bindings are gone, then dropping the constraints is the wrong thing to do.  That said, we could address such issues by ensuring that a particular symbol (when applicable) stays live outside of losing all references to it.
>> 
>> On Sep 7, 2012, at 6:24 PM, Jordan Rose <jordan_rose at apple.com> wrote:
>> 
>>> Author: jrose
>>> Date: Fri Sep  7 20:24:53 2012
>>> New Revision: 163444
>>> 
>>> URL: http://llvm.org/viewvc/llvm-project?rev=163444&view=rev
>>> Log:
>>> [analyzer] Remove constraints on dead symbols as part of removeDeadBindings.
>>> 
>>> Previously, we'd just keep constraints around forever, which means we'd
>>> never be able to merge paths that differed only in constraints on dead
>>> symbols.
>>> 
>>> Because we now allow constraints on symbolic expressions, not just single
>>> symbols, this requires changing SymExpr::symbol_iterator to include
>>> intermediate symbol nodes in its traversal, not just the SymbolData leaf
>>> nodes.
>>> 
>>> Added:
>>>  cfe/trunk/test/Analysis/traversal-path-unification.c
>>> Modified:
>>>  cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp
>>>  cfe/trunk/lib/StaticAnalyzer/Core/SymbolManager.cpp
>>> 
>>> Modified: cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp
>>> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp?rev=163444&r1=163443&r2=163444&view=diff
>>> ==============================================================================
>>> --- cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp (original)
>>> +++ cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp Fri Sep  7 20:24:53 2012
>>> @@ -106,8 +106,9 @@
>>>                                                  SymReaper);
>>> NewState.setStore(newStore);
>>> SymReaper.setReapedStore(newStore);
>>> -  
>>> -  return getPersistentState(NewState);
>>> +
>>> +  ProgramStateRef Result = getPersistentState(NewState);
>>> +  return ConstraintMgr->removeDeadBindings(Result, SymReaper);
>>> }
>>> 
>>> ProgramStateRef ProgramStateManager::MarshalState(ProgramStateRef state,
>>> @@ -697,7 +698,9 @@
>>> bool Tainted = false;
>>> for (SymExpr::symbol_iterator SI = Sym->symbol_begin(), SE =Sym->symbol_end();
>>>      SI != SE; ++SI) {
>>> -    assert(isa<SymbolData>(*SI));
>>> +    if (!isa<SymbolData>(*SI))
>>> +      continue;
>>> +    
>>>   const TaintTagType *Tag = get<TaintMap>(*SI);
>>>   Tainted = (Tag && *Tag == Kind);
>>> 
>>> 
>>> Modified: cfe/trunk/lib/StaticAnalyzer/Core/SymbolManager.cpp
>>> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SymbolManager.cpp?rev=163444&r1=163443&r2=163444&view=diff
>>> ==============================================================================
>>> --- cfe/trunk/lib/StaticAnalyzer/Core/SymbolManager.cpp (original)
>>> +++ cfe/trunk/lib/StaticAnalyzer/Core/SymbolManager.cpp Fri Sep  7 20:24:53 2012
>>> @@ -117,21 +117,17 @@
>>> 
>>> SymExpr::symbol_iterator::symbol_iterator(const SymExpr *SE) {
>>> itr.push_back(SE);
>>> -  while (!isa<SymbolData>(itr.back())) expand();
>>> }
>>> 
>>> SymExpr::symbol_iterator &SymExpr::symbol_iterator::operator++() {
>>> assert(!itr.empty() && "attempting to iterate on an 'end' iterator");
>>> -  assert(isa<SymbolData>(itr.back()));
>>> -  itr.pop_back();
>>> -  if (!itr.empty())
>>> -    while (!isa<SymbolData>(itr.back())) expand();
>>> +  expand();
>>> return *this;
>>> }
>>> 
>>> SymbolRef SymExpr::symbol_iterator::operator*() {
>>> assert(!itr.empty() && "attempting to dereference an 'end' iterator");
>>> -  return cast<SymbolData>(itr.back());
>>> +  return itr.back();
>>> }
>>> 
>>> void SymExpr::symbol_iterator::expand() {
>>> 
>>> Added: cfe/trunk/test/Analysis/traversal-path-unification.c
>>> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/traversal-path-unification.c?rev=163444&view=auto
>>> ==============================================================================
>>> --- cfe/trunk/test/Analysis/traversal-path-unification.c (added)
>>> +++ cfe/trunk/test/Analysis/traversal-path-unification.c Fri Sep  7 20:24:53 2012
>>> @@ -0,0 +1,21 @@
>>> +// RUN: %clang_cc1 -analyze -analyzer-checker=core,debug.DumpTraversal %s | FileCheck %s
>>> +
>>> +int a();
>>> +int b();
>>> +int c();
>>> +
>>> +void testRemoveDeadBindings() {
>>> +  int i = a();
>>> +  if (i)
>>> +    a();
>>> +  else
>>> +    b();
>>> +
>>> +  // At this point the symbol bound to 'i' is dead.
>>> +  // The effects of a() and b() are identical (they both invalidate globals).
>>> +  // We should unify the two paths here and only get one end-of-path node.
>>> +  c();
>>> +}
>>> +
>>> +// CHECK: --END PATH--
>>> +// CHECK-NOT: --END PATH--
>>> \ No newline at end of file
>>> 
>>> 
>>> _______________________________________________
>>> cfe-commits mailing list
>>> cfe-commits at cs.uiuc.edu
>>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
>> 
>> _______________________________________________
>> cfe-commits mailing list
>> cfe-commits at cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
>