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 <[email protected]> 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. 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. > > Any ideas? > Jordan > > > On Sep 9, 2012, at 21:35 , Ted Kremenek <[email protected]> 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 <[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
