[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'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