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 <[email protected]> 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 > [email protected] > http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits _______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
