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