[cfe-commits] r163444 - in /cfe/trunk: lib/StaticAnalyzer/Core/ProgramState.cpp lib/StaticAnalyzer/Core/SymbolManager.cpp test/Analysis/traversal-path-unification.c
Ted Kremenek
kremenek at apple.com
Wed Jan 2 13:24:14 PST 2013
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 <jordan_rose at apple.com> 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 <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
>>
>
More information about the cfe-commits
mailing list