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

[Ted Kremenek]

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