Do effects as a global space, don't even need to consider call site transform, taints...
[IRC.git] / Robust / src / Analysis / Disjoint / ReachGraph.java
index e266145993179b5dd26741fcf1d64236ac36bd8f..71a6f98393ef339275d72dfdb779fcfde9bb9efb 100644 (file)
@@ -14,17 +14,17 @@ public class ReachGraph {
                   
   // a special out-of-scope temp
   protected static final TempDescriptor tdReturn = new TempDescriptor( "_Return___" );
+
+  // predicate constants
+  public static final ExistPred    predTrue   = ExistPred.factory(); // if no args, true
+  public static final ExistPredSet predsEmpty = ExistPredSet.factory();
+  public static final ExistPredSet predsTrue  = ExistPredSet.factory( predTrue );
                   
   // some frequently used reachability constants
   protected static final ReachState rstateEmpty        = ReachState.factory();
   protected static final ReachSet   rsetEmpty          = ReachSet.factory();
-  protected static final ReachSet   rsetWithEmptyState = ReachSet.factory( rstateEmpty );
-
-  // predicate constants
-  protected static final ExistPred    predTrue   = ExistPred.factory(); // if no args, true
-  protected static final ExistPredSet predsEmpty = ExistPredSet.factory();
-  protected static final ExistPredSet predsTrue  = ExistPredSet.factory( predTrue );
-
+  protected static final ReachSet   rsetWithEmptyState = Canonical.changePredsTo( ReachSet.factory( rstateEmpty ),
+                                                                                  predsTrue );
 
   // from DisjointAnalysis for convenience
   protected static int      allocationDepth   = -1;
@@ -38,11 +38,16 @@ public class ReachGraph {
   // convenient set of alloc sites for all heap regions
   // present in the graph without having to search
   public HashSet<AllocSite> allocSites;  
+  
+  // set of accessible variables for current program statement
+  // if not contains, it is an inaccessible variable
+  public HashSet<TempDescriptor> accessibleVars;
 
   public ReachGraph() {
     id2hrn     = new Hashtable<Integer,        HeapRegionNode>();
     td2vn      = new Hashtable<TempDescriptor, VariableNode  >();
     allocSites = new HashSet<AllocSite>();
+    accessibleVars = new HashSet<TempDescriptor>();
   }
 
   
@@ -79,6 +84,8 @@ public class ReachGraph {
     return this.id2hrn.get( hrn.getID() ) == hrn;
   }
 
+  
+
 
 
   // the reason for this method is to have the option
@@ -90,7 +97,6 @@ public class ReachGraph {
     createNewHeapRegionNode( Integer        id,
                             boolean        isSingleObject,
                             boolean        isNewSummary,
-                            boolean        isFlagged,
                              boolean        isOutOfContext,
                             TypeDescriptor type,
                             AllocSite      allocSite,
@@ -100,8 +106,6 @@ public class ReachGraph {
                             String         description
                              ) {
 
-    boolean markForAnalysis = isFlagged;
-
     TypeDescriptor typeToUse = null;
     if( allocSite != null ) {
       typeToUse = allocSite.getType();
@@ -110,9 +114,18 @@ public class ReachGraph {
       typeToUse = type;
     }
 
-    if( allocSite != null && allocSite.getDisjointAnalysisId() != null ) {
+    boolean markForAnalysis = false;
+    if( allocSite != null && allocSite.isFlagged() ) {
       markForAnalysis = true;
     }
+    
+    if( allocSite == null ) {
+      assert !markForAnalysis;
+
+    } else if( markForAnalysis != allocSite.isFlagged() ) {
+      assert false;
+    }
+
 
     if( id == null ) {
       id = DisjointAnalysis.generateUniqueHeapRegionNodeID();
@@ -121,15 +134,18 @@ public class ReachGraph {
     if( inherent == null ) {
       if( markForAnalysis ) {
        inherent = 
-          ReachSet.factory(
-                           ReachState.factory(
-                                              ReachTuple.factory( id,
-                                                                  !isSingleObject,
-                                                                  ReachTuple.ARITY_ONE,
-                                                                  false // out-of-context
-                                                                  )
-                                              )
-                           );
+          Canonical.changePredsTo(
+                                  ReachSet.factory(
+                                                   ReachState.factory(
+                                                                      ReachTuple.factory( id,
+                                                                                          !isSingleObject,
+                                                                                          ReachTuple.ARITY_ONE,
+                                                                                          false // out-of-context
+                                                                                          )
+                                                                      )
+                                                   ),
+                                  predsTrue
+                                  );
       } else {
        inherent = rsetWithEmptyState;
       }
@@ -140,7 +156,7 @@ public class ReachGraph {
     }
 
     assert preds != null;
-    
+
     HeapRegionNode hrn = new HeapRegionNode( id,
                                             isSingleObject,
                                             markForAnalysis,
@@ -215,14 +231,26 @@ public class ReachGraph {
        
     referencer.removeReferencee( edge );
     referencee.removeReferencer( edge );
+
+    // TODO
+
+//    int oldTaint=edge.getTaintIdentifier();
+//    if(referencer instanceof HeapRegionNode){
+//     depropagateTaintIdentifier((HeapRegionNode)referencer,oldTaint,new HashSet<HeapRegionNode>());
+//    }
+
+
   }
 
-  protected void clearRefEdgesFrom( RefSrcNode     referencer,
-                                    TypeDescriptor type,
-                                    String         field,
-                                    boolean        removeAll ) {
+  // return whether at least one edge was removed
+  protected boolean clearRefEdgesFrom( RefSrcNode     referencer,
+                                       TypeDescriptor type,
+                                       String         field,
+                                       boolean        removeAll ) {
     assert referencer != null;
 
+    boolean atLeastOneEdgeRemoved = false;
+
     // get a copy of the set to iterate over, otherwise
     // we will be trying to take apart the set as we
     // are iterating over it, which won't work
@@ -240,8 +268,12 @@ public class ReachGraph {
                        referencee,
                        edge.getType(),
                        edge.getField() );
+
+        atLeastOneEdgeRemoved = true;
       }
     }
+
+    return atLeastOneEdgeRemoved;
   }
 
   protected void clearRefEdgesTo( HeapRegionNode referencee,
@@ -319,7 +351,12 @@ public class ReachGraph {
                                             edgeNew.getPreds()
                                             )
                             );
-       
+      edgeExisting.setTaints(
+                             Canonical.unionORpreds( edgeExisting.getTaints(),
+                                                     edgeNew.getTaints()
+                                                     )
+                             );
+      
     } else {                     
       addRefEdge( src, dst, edgeNew );
     }
@@ -341,6 +378,12 @@ public class ReachGraph {
   public void assignTempXEqualToTempY( TempDescriptor x,
                                       TempDescriptor y ) {
     assignTempXEqualToCastedTempY( x, y, null );
+    
+    // x gets status of y
+    // if it is in region, 
+    //if(accessibleVars.contains(y)){
+    //  accessibleVars.add(x);
+    //}
   }
 
   public void assignTempXEqualToCastedTempY( TempDescriptor x,
@@ -446,7 +489,8 @@ public class ReachGraph {
                                        tdNewEdge,
                                        null,
                                        Canonical.intersection( betaY, betaHrn ),
-                                       predsTrue
+                                       predsTrue,
+                                       edgeY.getTaints()
                                        );
 
         addEdgeOrMergeWithExisting( edgeNew );
@@ -465,13 +509,19 @@ public class ReachGraph {
       if( !DISABLE_GLOBAL_SWEEP ) {
        globalSweep();
       }
-    }    
+    }
+    
+    // accessible status update
+    // if it is in region,
+    //accessibleVars.add(x);
+    //accessibleVars.add(y);
   }
 
 
-  public void assignTempXFieldFEqualToTempY( TempDescriptor  x,
-                                            FieldDescriptor f,
-                                            TempDescriptor  y ) {
+  // return whether a strong update was actually effected
+  public boolean assignTempXFieldFEqualToTempY( TempDescriptor  x,
+                                                FieldDescriptor f,
+                                                TempDescriptor  y ) {
 
     VariableNode lnX = getVariableNodeFromTemp( x );
     VariableNode lnY = getVariableNodeFromTemp( y );
@@ -485,7 +535,8 @@ public class ReachGraph {
     Set<RefEdge> impossibleEdges = new HashSet<RefEdge>();
 
     // first look for possible strong updates and remove those edges
-    boolean strongUpdate = false;
+    boolean strongUpdateCond          = false;
+    boolean edgeRemovedByStrongUpdate = false;
 
     Iterator<RefEdge> itrXhrn = lnX.iteratorToReferencees();
     while( itrXhrn.hasNext() ) {
@@ -500,8 +551,16 @@ public class ReachGraph {
              )
          ) {
         if( !DISABLE_STRONG_UPDATES ) {
-          strongUpdate = true;
-          clearRefEdgesFrom( hrnX, f.getType(), f.getSymbol(), false );
+          strongUpdateCond = true;
+
+          boolean atLeastOne = 
+            clearRefEdgesFrom( hrnX, 
+                               f.getType(), 
+                               f.getSymbol(), 
+                               false );
+          if( atLeastOne ) {
+            edgeRemovedByStrongUpdate = true;
+          }
         }
       }
     }
@@ -590,15 +649,21 @@ public class ReachGraph {
                            hrnY.getType()
                            );  
 
-       RefEdge edgeNew = new RefEdge( hrnX,
-                                       hrnY,
-                                       tdNewEdge,
-                                       f.getSymbol(),
-                                       Canonical.pruneBy( edgeY.getBeta(),
-                                                          hrnX.getAlpha() 
-                                                          ),
-                                       predsTrue
-                                       );
+       RefEdge edgeNew = 
+          new RefEdge( hrnX,
+                       hrnY,
+                       tdNewEdge,
+                       f.getSymbol(),
+                       Canonical.changePredsTo(
+                                               Canonical.pruneBy( edgeY.getBeta(),
+                                                                  hrnX.getAlpha() 
+                                                                  ),
+                                               predsTrue
+                                               ),
+                       predsTrue,
+                       Canonical.changePredsTo( edgeY.getTaints(),
+                                                predsTrue )
+                       );
 
         addEdgeOrMergeWithExisting( edgeNew );
       }
@@ -612,11 +677,21 @@ public class ReachGraph {
 
     // if there was a strong update, make sure to improve
     // reachability with a global sweep    
-    if( strongUpdate || !impossibleEdges.isEmpty() ) {    
+    if( edgeRemovedByStrongUpdate || !impossibleEdges.isEmpty() ) {    
       if( !DISABLE_GLOBAL_SWEEP ) {
         globalSweep();
       }
     }    
+    
+
+    // after x.y=f , stall x and y if they are not accessible
+    // also contribute write effects on stall site of x
+    // accessible status update
+    // if it is in region
+    //accessibleVars.add(x);
+    //accessibleVars.add(y);
+
+    return edgeRemovedByStrongUpdate;
   }
 
 
@@ -633,6 +708,10 @@ public class ReachGraph {
       HeapRegionNode referencee = edgeX.getDst();
       RefEdge        edgeNew    = edgeX.copy();
       edgeNew.setSrc( lnR );
+      edgeNew.setTaints( Canonical.changePredsTo( edgeNew.getTaints(),
+                                                  predsTrue 
+                                                  )
+                         );
 
       addRefEdge( lnR, referencee, edgeNew );
     }
@@ -666,10 +745,15 @@ public class ReachGraph {
                    type,                 // type
                    null,                 // field name
                    hrnNewest.getAlpha(), // beta
-                   predsTrue             // predicates
+                   predsTrue,            // predicates
+                   TaintSet.factory()    // taints
                    );
 
     addRefEdge( lnX, hrnNewest, edgeNew );
+    
+    // after x=new , x is accessible
+    // if (isInRegion()) {
+    //accessibleVars.add(x);
   }
 
 
@@ -782,22 +866,12 @@ public class ReachGraph {
 
     if( hrnSummary == null ) {
 
-      boolean hasFlags = false;
-      if( as.getType().isClass() ) {
-       hasFlags = as.getType().getClassDesc().hasFlags();
-      }
-      
-      if( as.getFlag() ){
-        hasFlags = as.getFlag();
-      }
-
       String strDesc = as.toStringForDOT()+"\\nsummary";
 
       hrnSummary = 
         createNewHeapRegionNode( idSummary,    // id or null to generate a new one 
                                  false,        // single object?                
-                                 true,         // summary?      
-                                 hasFlags,     // flagged?
+                                 true,         // summary?                       
                                  false,        // out-of-context?
                                  as.getType(), // type                          
                                  as,           // allocation site                       
@@ -827,21 +901,11 @@ public class ReachGraph {
     
     if( hrnIth == null ) {
 
-      boolean hasFlags = false;
-      if( as.getType().isClass() ) {
-        hasFlags = as.getType().getClassDesc().hasFlags();
-      }
-      
-      if( as.getFlag() ){
-        hasFlags = as.getFlag();
-      }
-
       String strDesc = as.toStringForDOT()+"\\n"+i+" oldest";
 
       hrnIth = createNewHeapRegionNode( idIth,        // id or null to generate a new one 
                                         true,        // single object?                  
                                         false,       // summary?                        
-                                        hasFlags,     // flagged?                       
                                         false,        // out-of-context?
                                         as.getType(), // type                           
                                         as,          // allocation site                         
@@ -1233,6 +1297,81 @@ public class ReachGraph {
   }
 
 
+  public void taintInSetVars( FlatSESEEnterNode sese ) {
+    if( sese.getIsCallerSESEplaceholder() ) {
+      return;
+    }
+
+    Iterator<TempDescriptor> isvItr = sese.getInVarSet().iterator();
+    while( isvItr.hasNext() ) {
+      TempDescriptor isv = isvItr.next();
+      VariableNode   vn  = getVariableNodeFromTemp( isv );
+
+      Iterator<RefEdge> reItr = vn.iteratorToReferencees();
+      while( reItr.hasNext() ) {
+        RefEdge re = reItr.next();
+
+        // these in-set taints should have empty 
+        // predicates so they never propagate
+        // out to callers
+        Taint t = Taint.factory( sese,
+                                 null,
+                                 isv,
+                                 re.getDst().getAllocSite(),
+                                 ExistPredSet.factory()
+                                 );
+      
+        re.setTaints( Canonical.add( re.getTaints(),
+                                     t 
+                                     )
+                      );
+      }
+    }
+  }
+
+  // this is useful for more general tainting
+  public void taintTemp( Taint          taint,
+                         TempDescriptor td,
+                         ExistPredSet   preds
+                         ) {
+    
+    VariableNode vn = getVariableNodeFromTemp( td );
+    
+    Iterator<RefEdge> reItr = vn.iteratorToReferencees();
+    while( reItr.hasNext() ) {
+      RefEdge re = reItr.next();
+            
+      re.setTaints( Canonical.add( re.getTaints(),
+                                   taint 
+                                   )
+                    );
+    }
+  }
+  
+  public void removeInContextTaints( FlatSESEEnterNode sese ) {
+    if( sese.getIsCallerSESEplaceholder() ) {
+      return;
+    }
+
+    Iterator meItr = id2hrn.entrySet().iterator();
+    while( meItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      meItr.next();
+      Integer        id  = (Integer)        me.getKey();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      Iterator<RefEdge> reItr = hrn.iteratorToReferencers();
+      while( reItr.hasNext() ) {
+        RefEdge re = reItr.next();
+
+        re.setTaints( Canonical.removeTaintsBy( re.getTaints(),
+                                                sese
+                                                )
+                      );
+      }
+    }
+  }
+
+
   // used in makeCalleeView below to decide if there is
   // already an appropriate out-of-context edge in a callee
   // view graph for merging, or null if a new one will be added
@@ -1292,7 +1431,7 @@ public class ReachGraph {
   // used below to convert a ReachSet to its callee-context
   // equivalent with respect to allocation sites in this graph
   protected ReachSet toCalleeContext( ReachSet      rs,
-                                      ExistPredSet  preds,
+                                      ExistPredSet  predsNodeOrEdge,
                                       Set<HrnIdOoc> oocHrnIdOoc2callee
                                       ) {
     ReachSet out = ReachSet.factory();
@@ -1375,14 +1514,36 @@ public class ReachGraph {
         stateCallee = stateNew;
       }
       
-      // attach the passed in preds
-      stateCallee = Canonical.attach( stateCallee,
-                                      preds );
+      // make a predicate of the caller graph element
+      // and the caller state we just converted
+      ExistPredSet predsWithState = ExistPredSet.factory();
+
+      Iterator<ExistPred> predItr = predsNodeOrEdge.iterator();
+      while( predItr.hasNext() ) {
+        ExistPred predNodeOrEdge = predItr.next();
+
+        predsWithState = 
+          Canonical.add( predsWithState,
+                         ExistPred.factory( predNodeOrEdge.n_hrnID, 
+                                            predNodeOrEdge.e_tdSrc,
+                                            predNodeOrEdge.e_hrnSrcID,
+                                            predNodeOrEdge.e_hrnDstID,
+                                            predNodeOrEdge.e_type,
+                                            predNodeOrEdge.e_field,
+                                            stateCallee,
+                                            null,
+                                            predNodeOrEdge.e_srcOutCalleeContext,
+                                            predNodeOrEdge.e_srcOutCallerContext                                           
+                                            )
+                         );
+      }
 
+      stateCallee = Canonical.changePredsTo( stateCallee,
+                                             predsWithState );
+      
       out = Canonical.add( out,
                            stateCallee
-                           );
-
+                           );      
     }
     assert out.isCanonical();
     return out;
@@ -1396,6 +1557,12 @@ public class ReachGraph {
                      ) {
     ReachSet out = ReachSet.factory();
 
+    // when the mapping is null it means there were no
+    // predicates satisfied
+    if( calleeStatesSatisfied == null ) {
+      return out;
+    }
+
     Iterator<ReachState> itr = rs.iterator();
     while( itr.hasNext() ) {
       ReachState stateCallee = itr.next();
@@ -1426,13 +1593,14 @@ public class ReachGraph {
                                stateCaller
                                );
         }
-      } 
+      }
     }    
 
     assert out.isCanonical();
     return out;
   }
 
+
   // used below to convert a ReachSet to an equivalent
   // version with shadow IDs merged into unshadowed IDs
   protected ReachSet unshadow( ReachSet rs ) {
@@ -1447,6 +1615,99 @@ public class ReachGraph {
   }
 
 
+  // convert a caller taint set into a callee taint set
+  protected TaintSet
+    toCalleeContext( TaintSet     ts,
+                     ExistPredSet predsEdge ) {
+    
+    TaintSet out = TaintSet.factory();
+
+    // the idea is easy, the taint identifier itself doesn't
+    // change at all, but the predicates should be tautology:
+    // start with the preds passed in from the caller edge
+    // that host the taints, and alter them to have the taint
+    // added, just becoming more specific than edge predicate alone
+
+    Iterator<Taint> itr = ts.iterator();
+    while( itr.hasNext() ) {
+      Taint tCaller = itr.next();
+
+      ExistPredSet predsWithTaint = ExistPredSet.factory();
+
+      Iterator<ExistPred> predItr = predsEdge.iterator();
+      while( predItr.hasNext() ) {
+        ExistPred predEdge = predItr.next();
+
+        predsWithTaint = 
+          Canonical.add( predsWithTaint,
+                         ExistPred.factory( predEdge.e_tdSrc,
+                                            predEdge.e_hrnSrcID,
+                                            predEdge.e_hrnDstID,
+                                            predEdge.e_type,
+                                            predEdge.e_field,
+                                            null,
+                                            tCaller,
+                                            predEdge.e_srcOutCalleeContext,
+                                            predEdge.e_srcOutCallerContext                                           
+                                            )
+                         );
+      }
+
+      Taint tCallee = Canonical.changePredsTo( tCaller,
+                                               predsWithTaint );
+
+      out = Canonical.add( out,
+                           tCallee
+                           );
+    }
+
+    assert out.isCanonical();
+    return out;
+  }
+
+
+  // used below to convert a TaintSet to its caller-context
+  // equivalent, just eliminate Taints with bad preds
+  protected TaintSet 
+    toCallerContext( TaintSet                       ts,
+                     Hashtable<Taint, ExistPredSet> calleeTaintsSatisfied
+                     ) {
+
+    TaintSet out = TaintSet.factory();
+
+    // when the mapping is null it means there were no
+    // predicates satisfied
+    if( calleeTaintsSatisfied == null ) {
+      return out;
+    }
+
+    Iterator<Taint> itr = ts.iterator();
+    while( itr.hasNext() ) {
+      Taint tCallee = itr.next();
+
+      if( calleeTaintsSatisfied.containsKey( tCallee ) ) {
+        
+        Taint tCaller = 
+          Canonical.attach( Taint.factory( tCallee.sese,
+                                           tCallee.stallSite,
+                                           tCallee.var,
+                                           tCallee.allocSite,
+                                           ExistPredSet.factory() ),
+                            calleeTaintsSatisfied.get( tCallee )
+                            );
+        out = Canonical.add( out,
+                             tCaller
+                             );
+      }     
+    }    
+    
+    assert out.isCanonical();
+    return out;
+  }
+
+
+
+
   // use this method to make a new reach graph that is
   // what heap the FlatMethod callee from the FlatCall 
   // would start with reaching from its arguments in
@@ -1597,7 +1858,6 @@ public class ReachGraph {
       rg.createNewHeapRegionNode( hrnCaller.getID(),
                                   hrnCaller.isSingleObject(),
                                   hrnCaller.isNewSummary(),
-                                  hrnCaller.isFlagged(),
                                   false, // out-of-context?
                                   hrnCaller.getType(),
                                   hrnCaller.getAllocSite(),
@@ -1607,7 +1867,7 @@ public class ReachGraph {
                                                    ),
                                   toCalleeContext( hrnCaller.getAlpha(),
                                                    preds,
-                                                   oocHrnIdOoc2callee 
+                                                   oocHrnIdOoc2callee
                                                    ),
                                   preds,
                                   hrnCaller.getDescription()
@@ -1622,29 +1882,31 @@ public class ReachGraph {
       RefEdge   reArg = (RefEdge)   me.getKey();
       Integer   index = (Integer)   me.getValue();
       
-      TempDescriptor arg = fmCallee.getParameter( index );
+      VariableNode   vnCaller  = (VariableNode) reArg.getSrc();
+      TempDescriptor argCaller = vnCaller.getTempDescriptor();
       
-      VariableNode vnCallee = 
-        rg.getVariableNodeFromTemp( arg );
+      TempDescriptor paramCallee = fmCallee.getParameter( index );      
+      VariableNode   vnCallee    = rg.getVariableNodeFromTemp( paramCallee );
       
       HeapRegionNode hrnDstCaller = reArg.getDst();
       HeapRegionNode hrnDstCallee = rg.id2hrn.get( hrnDstCaller.getID() );
       assert hrnDstCallee != null;
       
       ExistPred pred =
-        ExistPred.factory( arg,
+        ExistPred.factory( argCaller,
                            null, 
                            hrnDstCallee.getID(),
                            reArg.getType(),
                            reArg.getField(),
-                           null,
+                           null,  // state
+                           null,  // taint
                            true,  // out-of-callee-context
                            false  // out-of-caller-context
                            );
       
       ExistPredSet preds = 
         ExistPredSet.factory( pred );
-      
+
       RefEdge reCallee = 
         new RefEdge( vnCallee,
                      hrnDstCallee,
@@ -1654,7 +1916,9 @@ public class ReachGraph {
                                       preds,
                                       oocHrnIdOoc2callee
                                       ),
-                     preds
+                     preds,
+                     toCalleeContext( reArg.getTaints(),
+                                      preds )
                      );
       
       rg.addRefEdge( vnCallee,
@@ -1683,7 +1947,8 @@ public class ReachGraph {
                            hrnDstCallee.getID(),
                            reCaller.getType(),
                            reCaller.getField(),
-                           null,
+                           null,  // state
+                           null,  // taint
                            false, // out-of-callee-context
                            false  // out-of-caller-context
                            );
@@ -1700,7 +1965,8 @@ public class ReachGraph {
                                       preds,
                                       oocHrnIdOoc2callee 
                                       ),
-                     preds
+                     preds,
+                     TaintSet.factory() // no taints for in-context edges
                      );
       
       rg.addRefEdge( hrnSrcCallee,
@@ -1755,6 +2021,7 @@ public class ReachGraph {
                            reCaller.getType(),
                            reCaller.getField(),
                            null,
+                           null,
                            outOfCalleeContext,
                            outOfCallerContext
                            );
@@ -1789,7 +2056,6 @@ public class ReachGraph {
             rg.createNewHeapRegionNode( null,  // ID
                                         false, // single object?
                                         false, // new summary?
-                                        false, // flagged?
                                         true,  // out-of-context?
                                         oocNodeType,
                                         null,  // alloc site, shouldn't be used
@@ -1818,7 +2084,6 @@ public class ReachGraph {
               rg.createNewHeapRegionNode( oocHrnID,  // ID
                                           false, // single object?
                                           false, // new summary?
-                                          false, // flagged?
                                           true,  // out-of-context?
                                           oocNodeType,
                                           null,  // alloc site, shouldn't be used
@@ -1858,7 +2123,9 @@ public class ReachGraph {
                                                      preds,
                                                      oocHrnIdOoc2callee
                                                      ),
-                                    preds
+                                    preds,
+                                    toCalleeContext( reCaller.getTaints(),
+                                                     preds )
                                     )
                        );              
         
@@ -1877,6 +2144,13 @@ public class ReachGraph {
                                                   )
                                   );          
 
+        oocEdgeExisting.setTaints( Canonical.unionORpreds( oocEdgeExisting.getTaints(),
+                                                           toCalleeContext( reCaller.getTaints(),
+                                                                            preds
+                                                                            )
+                                                           )
+                                   );
+
         HeapRegionNode hrnCalleeAndOutContext =
           (HeapRegionNode) oocEdgeExisting.getSrc();
         hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
@@ -1893,11 +2167,14 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {    
-      rg.writeGraph( "calleeview", 
+      debugGraphPrefix = String.format( "call%03d", debugCallSiteVisitCounter );
+      rg.writeGraph( debugGraphPrefix+"calleeview", 
                      resolveMethodDebugDOTwriteLabels,    
                      resolveMethodDebugDOTselectTemps,    
-                     resolveMethodDebugDOTpruneGarbage,   
+                     resolveMethodDebugDOTpruneGarbage,
+                     resolveMethodDebugDOThideReach,
                      resolveMethodDebugDOThideSubsetReach,
+                     resolveMethodDebugDOThidePreds,
                      resolveMethodDebugDOThideEdgeTaints );      
     }
 
@@ -1912,10 +2189,17 @@ public class ReachGraph {
   private static boolean resolveMethodDebugDOTwriteLabels     = true;
   private static boolean resolveMethodDebugDOTselectTemps     = true;
   private static boolean resolveMethodDebugDOTpruneGarbage    = true;
-  private static boolean resolveMethodDebugDOThideSubsetReach = false;
+  private static boolean resolveMethodDebugDOThideReach       = true;
+  private static boolean resolveMethodDebugDOThideSubsetReach = true;
+  private static boolean resolveMethodDebugDOThidePreds       = true;
   private static boolean resolveMethodDebugDOThideEdgeTaints  = true;
 
-
+  static String debugGraphPrefix;
+  static int debugCallSiteVisitCounter;
+  static int debugCallSiteVisitStartCapture;
+  static int debugCallSiteNumVisitsToCapture;
+  static boolean debugCallSiteStopAfter;
+  
 
   public void 
     resolveMethodCall( FlatCall     fc,        
@@ -1926,23 +2210,35 @@ public class ReachGraph {
                        ) {
 
     if( writeDebugDOTs ) {
-      rgCallee.writeGraph( "callee", 
+      System.out.println( "  Writing out visit "+
+                          debugCallSiteVisitCounter+
+                          " to debug call site" );
+
+      debugGraphPrefix = String.format( "call%03d", 
+                                        debugCallSiteVisitCounter );
+      
+      rgCallee.writeGraph( debugGraphPrefix+"callee", 
                            resolveMethodDebugDOTwriteLabels,    
                            resolveMethodDebugDOTselectTemps,    
                            resolveMethodDebugDOTpruneGarbage,   
+                           resolveMethodDebugDOThideReach,
                            resolveMethodDebugDOThideSubsetReach,
+                           resolveMethodDebugDOThidePreds,
                            resolveMethodDebugDOThideEdgeTaints );
       
-      writeGraph( "caller00In",  
+      writeGraph( debugGraphPrefix+"caller00In",  
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints,
                   callerNodeIDsCopiedToCallee );
     }
 
 
+
     // method call transfer function steps:
     // 1. Use current callee-reachable heap (CRH) to test callee 
     //    predicates and mark what will be coming in.
@@ -1963,12 +2259,22 @@ public class ReachGraph {
     Hashtable<RefEdge, ExistPredSet> calleeEdgesSatisfied =
       new Hashtable<RefEdge, ExistPredSet>();
 
-    Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied =
-      new Hashtable<ReachState, ExistPredSet>();
+    Hashtable< HeapRegionNode, Hashtable<ReachState, ExistPredSet> >
+      calleeNode2calleeStatesSatisfied =
+      new Hashtable< HeapRegionNode, Hashtable<ReachState, ExistPredSet> >();
+
+    Hashtable< RefEdge, Hashtable<ReachState, ExistPredSet> >
+      calleeEdge2calleeStatesSatisfied =
+      new Hashtable< RefEdge, Hashtable<ReachState, ExistPredSet> >();
+
+    Hashtable< RefEdge, Hashtable<Taint, ExistPredSet> >
+      calleeEdge2calleeTaintsSatisfied =
+      new Hashtable< RefEdge, Hashtable<Taint, ExistPredSet> >();
 
     Hashtable< RefEdge, Set<RefSrcNode> > calleeEdges2oocCallerSrcMatches =
       new Hashtable< RefEdge, Set<RefSrcNode> >();
 
+
     Iterator meItr = rgCallee.id2hrn.entrySet().iterator();
     while( meItr.hasNext() ) {
       Map.Entry      me        = (Map.Entry)      meItr.next();
@@ -1993,6 +2299,8 @@ public class ReachGraph {
       
       // since the node is coming over, find out which reach
       // states on it should come over, too
+      assert calleeNode2calleeStatesSatisfied.get( hrnCallee ) == null;
+
       Iterator<ReachState> stateItr = hrnCallee.getAlpha().iterator();
       while( stateItr.hasNext() ) {
         ReachState stateCallee = stateItr.next();
@@ -2001,7 +2309,18 @@ public class ReachGraph {
           stateCallee.getPreds().isSatisfiedBy( this,
                                                 callerNodeIDsCopiedToCallee
                                                 );
-        if( predsIfSatis != null ) {
+        if( predsIfSatis != null ) {          
+      
+          Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied =
+            calleeNode2calleeStatesSatisfied.get( hrnCallee ); 
+
+          if( calleeStatesSatisfied == null ) {
+            calleeStatesSatisfied = 
+              new Hashtable<ReachState, ExistPredSet>();
+
+            calleeNode2calleeStatesSatisfied.put( hrnCallee, calleeStatesSatisfied );
+          }
+
           calleeStatesSatisfied.put( stateCallee, predsIfSatis );
         } 
       }
@@ -2016,77 +2335,118 @@ public class ReachGraph {
         // have an (out-of-context heap region -> in-context heap region)
         // abstraction in the callEE, so its true we never need to
         // look at a (var node -> heap region) edge in callee to bring
-        // those over for the call site transfer.  What about (param var->heap region)
+        // those over for the call site transfer, except for the special
+        // case of *RETURN var* -> heap region edges.
+        // What about (param var->heap region)
         // edges in callee? They are dealt with below this loop.
-        // So, yes, at this point skip (var->region) edges in callee
+
         if( rsnCallee instanceof VariableNode ) {
-          continue;
-        }        
+          
+          // looking for the return-value variable only 
+          VariableNode vnCallee = (VariableNode) rsnCallee;
+          if( vnCallee.getTempDescriptor() != tdReturn ) {
+            continue;
+          }
 
-        // first see if the source is out-of-context, and only
-        // proceed with this edge if we find some caller-context
-        // matches
-        HeapRegionNode hrnSrcCallee = (HeapRegionNode) rsnCallee;
-        boolean matchedOutOfContext = false;
+          TempDescriptor returnTemp = fc.getReturnTemp();
+          if( returnTemp == null ||
+              !DisjointAnalysis.shouldAnalysisTrack( returnTemp.getType() ) 
+              ) {
+            continue;
+          }
+                                         
+          // note that the assignment of the return value is to a
+          // variable in the caller which is out-of-context with
+          // respect to the callee
+          VariableNode vnLhsCaller = getVariableNodeFromTemp( returnTemp );
+          Set<RefSrcNode> rsnCallers = new HashSet<RefSrcNode>();
+          rsnCallers.add( vnLhsCaller  );
+          calleeEdges2oocCallerSrcMatches.put( reCallee, rsnCallers );
 
-        if( hrnSrcCallee.isOutOfContext() ) {          
+          
+        } else {
+          // for HeapRegionNode callee sources...
 
-          assert !calleeEdges2oocCallerSrcMatches.containsKey( reCallee );
+          // first see if the source is out-of-context, and only
+          // proceed with this edge if we find some caller-context
+          // matches
+          HeapRegionNode hrnSrcCallee = (HeapRegionNode) rsnCallee;
+          boolean matchedOutOfContext = false;
+          
+          if( !hrnSrcCallee.isOutOfContext() ) {          
 
-          Set<RefSrcNode> rsnCallers = new HashSet<RefSrcNode>();            
+            predsIfSatis = 
+              hrnSrcCallee.getPreds().isSatisfiedBy( this,
+                                                     callerNodeIDsCopiedToCallee
+                                                     );          
+            if( predsIfSatis != null ) {
+              calleeNodesSatisfied.put( hrnSrcCallee, predsIfSatis );
+            } else {
+              // otherwise forget this edge
+              continue;
+            }          
+      
+          } else {
+            // hrnSrcCallee is out-of-context
 
-          // is the target node in the caller?
-          HeapRegionNode hrnDstCaller = this.id2hrn.get( hrnCallee.getID() );
-          if( hrnDstCaller == null ) {
-            continue;
-          }          
+            assert !calleeEdges2oocCallerSrcMatches.containsKey( reCallee );
 
-          Iterator<RefEdge> reDstItr = hrnDstCaller.iteratorToReferencers();
-          while( reDstItr.hasNext() ) {
-            // the edge and field (either possibly null) must match
-            RefEdge reCaller = reDstItr.next();
+            Set<RefSrcNode> rsnCallers = new HashSet<RefSrcNode>();            
 
-            if( !reCaller.typeEquals ( reCallee.getType()  ) ||
-                !reCaller.fieldEquals( reCallee.getField() ) 
-                ) {
+            // is the target node in the caller?
+            HeapRegionNode hrnDstCaller = this.id2hrn.get( hrnCallee.getID() );
+            if( hrnDstCaller == null ) {
               continue;
-            }
-            
-            RefSrcNode rsnCaller = reCaller.getSrc();
-            if( rsnCaller instanceof VariableNode ) {
+            }          
+
+            Iterator<RefEdge> reDstItr = hrnDstCaller.iteratorToReferencers();
+            while( reDstItr.hasNext() ) {
+              // the edge and field (either possibly null) must match
+              RefEdge reCaller = reDstItr.next();
 
-              // a variable node matches an OOC region with null type
-              if( hrnSrcCallee.getType() != null ) {
+              if( !reCaller.typeEquals ( reCallee.getType()  ) ||
+                  !reCaller.fieldEquals( reCallee.getField() ) 
+                  ) {
                 continue;
               }
+            
+              RefSrcNode rsnCaller = reCaller.getSrc();
+              if( rsnCaller instanceof VariableNode ) {
 
-            } else {
-              // otherwise types should match
-              HeapRegionNode hrnCallerSrc = (HeapRegionNode) rsnCaller;
-              if( hrnSrcCallee.getType() == null ) {
-                if( hrnCallerSrc.getType() != null ) {
+                // a variable node matches an OOC region with null type
+                if( hrnSrcCallee.getType() != null ) {
                   continue;
                 }
+
               } else {
-                if( !hrnSrcCallee.getType().equals( hrnCallerSrc.getType() ) ) {
-                  continue;
+                // otherwise types should match
+                HeapRegionNode hrnCallerSrc = (HeapRegionNode) rsnCaller;
+                if( hrnSrcCallee.getType() == null ) {
+                  if( hrnCallerSrc.getType() != null ) {
+                    continue;
+                  }
+                } else {
+                  if( !hrnSrcCallee.getType().equals( hrnCallerSrc.getType() ) ) {
+                    continue;
+                  }
                 }
               }
+
+              rsnCallers.add( rsnCaller );
+              matchedOutOfContext = true;
             }
 
-            rsnCallers.add( rsnCaller );
-            matchedOutOfContext = true;
+            if( !rsnCallers.isEmpty() ) {
+              calleeEdges2oocCallerSrcMatches.put( reCallee, rsnCallers );
+            }
           }
 
-          if( !rsnCallers.isEmpty() ) {
-            calleeEdges2oocCallerSrcMatches.put( reCallee, rsnCallers );
+          if( hrnSrcCallee.isOutOfContext() &&
+              !matchedOutOfContext ) {
+            continue;
           }
         }
 
-        if( hrnSrcCallee.isOutOfContext() &&
-            !matchedOutOfContext ) {
-          continue;
-        }
         
         predsIfSatis = 
           reCallee.getPreds().isSatisfiedBy( this,
@@ -2098,6 +2458,8 @@ public class ReachGraph {
 
           // since the edge is coming over, find out which reach
           // states on it should come over, too
+          assert calleeEdge2calleeStatesSatisfied.get( reCallee ) == null;
+
           stateItr = reCallee.getBeta().iterator();
           while( stateItr.hasNext() ) {
             ReachState stateCallee = stateItr.next();
@@ -2107,73 +2469,60 @@ public class ReachGraph {
                                                     callerNodeIDsCopiedToCallee
                                                     );
             if( predsIfSatis != null ) {
-              calleeStatesSatisfied.put( stateCallee, predsIfSatis );
-            } 
-          }
-        }        
-      }
-    }
+              
+              Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied =
+                calleeEdge2calleeStatesSatisfied.get( reCallee );
 
-    // test param -> HRN edges, also
-    for( int i = 0; i < fmCallee.numParameters(); ++i ) {
+              if( calleeStatesSatisfied == null ) {
+                calleeStatesSatisfied = 
+                  new Hashtable<ReachState, ExistPredSet>();
 
-      // parameter defined here is the symbol in the callee
-      TempDescriptor tdParam = fmCallee.getParameter( i );
+                calleeEdge2calleeStatesSatisfied.put( reCallee, calleeStatesSatisfied );
+              }
 
-      if( !DisjointAnalysis.shouldAnalysisTrack( tdParam.getType() ) ) {
-        // skip primitive/immutable parameters
-        continue;
-      }
+              calleeStatesSatisfied.put( stateCallee, predsIfSatis );             
+            } 
+          }
 
-      VariableNode vnCallee = rgCallee.getVariableNodeFromTemp( tdParam );
+          // since the edge is coming over, find out which taints
+          // on it should come over, too          
+          assert calleeEdge2calleeTaintsSatisfied.get( reCallee ) == null;
 
-      Iterator<RefEdge> reItr = vnCallee.iteratorToReferencees();
-      while( reItr.hasNext() ) {
-        RefEdge reCallee = reItr.next();
-        
-        ExistPredSet ifDst = 
-          reCallee.getDst().getPreds().isSatisfiedBy( this,
-                                                      callerNodeIDsCopiedToCallee
-                                                      );
-        if( ifDst == null ) {
-          continue;
-        }
-        
-        ExistPredSet predsIfSatis = 
-          reCallee.getPreds().isSatisfiedBy( this,
-                                             callerNodeIDsCopiedToCallee
-                                             );
-        if( predsIfSatis != null ) {
-          calleeEdgesSatisfied.put( reCallee, predsIfSatis );
+          Iterator<Taint> tItr = reCallee.getTaints().iterator();
+          while( tItr.hasNext() ) {
+            Taint tCallee = tItr.next();
 
-          // since the edge is coming over, find out which reach
-          // states on it should come over, too
-          Iterator<ReachState> stateItr = reCallee.getBeta().iterator();
-          while( stateItr.hasNext() ) {
-            ReachState stateCallee = stateItr.next();
-            
             predsIfSatis = 
-              stateCallee.getPreds().isSatisfiedBy( this,
-                                                    callerNodeIDsCopiedToCallee
-                                                    );
+              tCallee.getPreds().isSatisfiedBy( this,
+                                                callerNodeIDsCopiedToCallee
+                                                );
             if( predsIfSatis != null ) {
-              calleeStatesSatisfied.put( stateCallee, predsIfSatis );
+              
+              Hashtable<Taint, ExistPredSet> calleeTaintsSatisfied =
+                calleeEdge2calleeTaintsSatisfied.get( reCallee );
+
+              if( calleeTaintsSatisfied == null ) {
+                calleeTaintsSatisfied = 
+                  new Hashtable<Taint, ExistPredSet>();
+
+                calleeEdge2calleeTaintsSatisfied.put( reCallee, calleeTaintsSatisfied );
+              }
+
+              calleeTaintsSatisfied.put( tCallee, predsIfSatis );
             } 
           }
-
         }        
       }
     }
 
-
-
-
     if( writeDebugDOTs ) {
-      writeGraph( "caller20BeforeWipe", 
+      writeGraph( debugGraphPrefix+"caller20BeforeWipe", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
 
@@ -2190,18 +2539,34 @@ public class ReachGraph {
       wipeOut( hrnCaller, true );
     }
 
+    // if we are assigning the return value to something, clobber now
+    // as part of the wipe
+    TempDescriptor returnTemp = fc.getReturnTemp();
+    if( returnTemp != null && 
+        DisjointAnalysis.shouldAnalysisTrack( returnTemp.getType() ) 
+        ) {
+      
+      VariableNode vnLhsCaller = getVariableNodeFromTemp( returnTemp );
+      clearRefEdgesFrom( vnLhsCaller, null, null, true );
+    }
+
+
 
 
     if( writeDebugDOTs ) {
-      writeGraph( "caller30BeforeAddingNodes", 
+      writeGraph( debugGraphPrefix+"caller30BeforeAddingNodes", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
 
 
+
+
     // 3. callee elements with satisfied preds come in, note that
     //    the mapping of elements satisfied to preds is like this:
     //    A callee element EE has preds EEp that are satisfied by
@@ -2235,12 +2600,11 @@ public class ReachGraph {
           createNewHeapRegionNode( hrnIDshadow,                // id or null to generate a new one 
                                    hrnCallee.isSingleObject(), // single object?                
                                    hrnCallee.isNewSummary(),   // summary?      
-                                   hrnCallee.isFlagged(),      // flagged?
                                    false,                      // out-of-context?
                                    hrnCallee.getType(),        // type                          
                                    hrnCallee.getAllocSite(),   // allocation site                       
                                    toCallerContext( hrnCallee.getInherent(),
-                                                    calleeStatesSatisfied  ),    // inherent reach
+                                                    calleeNode2calleeStatesSatisfied.get( hrnCallee ) ), // inherent reach
                                    null,                       // current reach                 
                                    predsEmpty,                 // predicates
                                    hrnCallee.getDescription()  // description
@@ -2250,7 +2614,7 @@ public class ReachGraph {
       }
 
       hrnCaller.setAlpha( toCallerContext( hrnCallee.getAlpha(),
-                                           calleeStatesSatisfied 
+                                           calleeNode2calleeStatesSatisfied.get( hrnCallee )
                                            )
                           );
 
@@ -2259,12 +2623,16 @@ public class ReachGraph {
 
 
 
+
+
     if( writeDebugDOTs ) {
-      writeGraph( "caller31BeforeAddingEdges", 
+      writeGraph( debugGraphPrefix+"caller31BeforeAddingEdges", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
 
@@ -2280,6 +2648,7 @@ public class ReachGraph {
 
 
     // 3.b) callee -> callee edges AND out-of-context -> callee
+    //      which includes return temp -> callee edges now, too
     satisItr = calleeEdgesSatisfied.entrySet().iterator();
     while( satisItr.hasNext() ) {
       Map.Entry    me       = (Map.Entry)    satisItr.next();
@@ -2305,6 +2674,13 @@ public class ReachGraph {
       Set<RefSrcNode> oocCallers = 
         calleeEdges2oocCallerSrcMatches.get( reCallee );
 
+      if( rsnCallee instanceof HeapRegionNode ) {
+        HeapRegionNode hrnCalleeSrc = (HeapRegionNode) rsnCallee;
+        if( hrnCalleeSrc.isOutOfContext() ) {
+          assert oocCallers != null;
+        }
+      }
+
       
       if( oocCallers == null ) {
         // there are no out-of-context matches, so it's
@@ -2327,6 +2703,7 @@ public class ReachGraph {
 
         } else {
           // otherwise source is in context, one region
+          
           HeapRegionNode hrnSrcCallee = (HeapRegionNode) rsnCallee;
 
           // translate an in-context node to shadow
@@ -2339,23 +2716,7 @@ public class ReachGraph {
           HeapRegionNode hrnSrcCallerShadow =
             this.id2hrn.get( hrnIDSrcShadow );
           
-          if( hrnSrcCallerShadow == null ) {
-            hrnSrcCallerShadow =
-              createNewHeapRegionNode( hrnIDSrcShadow,                // id or null to generate a new one 
-                                       hrnSrcCallee.isSingleObject(), // single object?                 
-                                       hrnSrcCallee.isNewSummary(),   // summary?       
-                                       hrnSrcCallee.isFlagged(),      // flagged?
-                                       false,                         // out-of-context?
-                                       hrnSrcCallee.getType(),        // type                           
-                                       hrnSrcCallee.getAllocSite(),   // allocation site                        
-                                       toCallerContext( hrnSrcCallee.getInherent(),
-                                                        calleeStatesSatisfied ),    // inherent reach
-                                       toCallerContext( hrnSrcCallee.getAlpha(),
-                                                        calleeStatesSatisfied ),       // current reach                 
-                                       predsEmpty,                    // predicates
-                                       hrnSrcCallee.getDescription()  // description
-                                       );                                        
-          }
+          assert hrnSrcCallerShadow != null;        
           
           rsnCallers.add( hrnSrcCallerShadow );
         }
@@ -2379,8 +2740,10 @@ public class ReachGraph {
                                         reCallee.getType(),
                                         reCallee.getField(),
                                         toCallerContext( reCallee.getBeta(),
-                                                         calleeStatesSatisfied ),
-                                        preds
+                                                         calleeEdge2calleeStatesSatisfied.get( reCallee ) ),
+                                        preds,
+                                        toCallerContext( reCallee.getTaints(),
+                                                         calleeEdge2calleeTaintsSatisfied.get( reCallee ) )
                                         );
 
         ChangeSet cs = ChangeSet.factory();
@@ -2409,28 +2772,16 @@ public class ReachGraph {
                                 );
           }
         }
-        
-
-        // look to see if an edge with same field exists
-        // and merge with it, otherwise just add the edge
-        RefEdge edgeExisting = rsnCaller.getReferenceTo( hrnDstCaller,
-                                                         reCallee.getType(),
-                                                         reCallee.getField()
-                                                         );    
-        if( edgeExisting != null ) {
-          edgeExisting.setBeta(
-                               Canonical.unionORpreds( edgeExisting.getBeta(),
-                                                reCaller.getBeta()
-                                                )
-                               );
-          edgeExisting.setPreds(
-                                Canonical.join( edgeExisting.getPreds(),
-                                                reCaller.getPreds()
-                                                )
-                                );
 
-          // for reach propagation
-          if( !cs.isEmpty() ) {
+        // we're just going to use the convenient "merge-if-exists"
+        // edge call below, but still take a separate look if there
+        // is an existing caller edge to build change sets properly
+        if( !cs.isEmpty() ) {
+          RefEdge edgeExisting = rsnCaller.getReferenceTo( hrnDstCaller,
+                                                           reCallee.getType(),
+                                                           reCallee.getField()
+                                                           );  
+          if( edgeExisting != null ) {
             ChangeSet csExisting = edgePlannedChanges.get( edgeExisting );
             if( csExisting == null ) {
               csExisting = ChangeSet.factory();
@@ -2439,19 +2790,16 @@ public class ReachGraph {
                                     Canonical.union( csExisting,
                                                      cs
                                                      ) 
-                                    );
-          }
-          
-        } else {                         
-          addRefEdge( rsnCaller, hrnDstCaller, reCaller );     
-
-          // for reach propagation
-          if( !cs.isEmpty() ) {
+                                    );                    
+          } else {                       
             edgesForPropagation.add( reCaller );
             assert !edgePlannedChanges.containsKey( reCaller );
-            edgePlannedChanges.put( reCaller, cs );
+            edgePlannedChanges.put( reCaller, cs );        
           }
         }
+
+        // then add new caller edge or merge
+        addEdgeOrMergeWithExisting( reCaller );
       }
     }
 
@@ -2460,95 +2808,13 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      writeGraph( "caller35BeforeAssignReturnValue", 
-                  resolveMethodDebugDOTwriteLabels,    
-                  resolveMethodDebugDOTselectTemps,    
-                  resolveMethodDebugDOTpruneGarbage,   
-                  resolveMethodDebugDOThideSubsetReach,
-                  resolveMethodDebugDOThideEdgeTaints );
-    }
-
-
-
-    // TODO: WAIT! THIS SHOULD BE MERGED INTO OTHER PARTS, BECAUSE
-    // AS IT IS WE'RE NOT VERIFYING PREDICATES OF RETURN VALUE
-    // EDGES, JUST BRINGING THEM ALL!  It'll work for now, over approximation
-    
-    // 3.d) handle return value assignment if needed
-    TempDescriptor returnTemp = fc.getReturnTemp();
-    if( returnTemp != null && 
-        DisjointAnalysis.shouldAnalysisTrack( returnTemp.getType() ) 
-        ) {
-
-      VariableNode vnLhsCaller = getVariableNodeFromTemp( returnTemp );
-      clearRefEdgesFrom( vnLhsCaller, null, null, true );
-
-      VariableNode vnReturnCallee = rgCallee.getVariableNodeFromTemp( tdReturn );
-      Iterator<RefEdge> reCalleeItr = vnReturnCallee.iteratorToReferencees();
-      while( reCalleeItr.hasNext() ) {
-       RefEdge        reCallee     = reCalleeItr.next();
-       HeapRegionNode hrnDstCallee = reCallee.getDst();
-
-       // some edge types are not possible return values when we can
-       // see what type variable we are assigning it to
-       if( !isSuperiorType( returnTemp.getType(), reCallee.getType() ) ) {
-         System.out.println( "*** NOT EXPECTING TO SEE THIS: Throwing out "+
-                              reCallee+" for return temp "+returnTemp );
-         // prune
-         continue;
-       }       
-
-        AllocSite asDst = hrnDstCallee.getAllocSite();
-        allocSites.add( asDst );
-
-        Integer hrnIDDstShadow = asDst.getShadowIDfromID( hrnDstCallee.getID() );
-
-        HeapRegionNode hrnDstCaller = id2hrn.get( hrnIDDstShadow );
-        if( hrnDstCaller == null ) {
-          hrnDstCaller =
-            createNewHeapRegionNode( hrnIDDstShadow,                // id or null to generate a new one 
-                                     hrnDstCallee.isSingleObject(), // single object?           
-                                     hrnDstCallee.isNewSummary(),   // summary?         
-                                     hrnDstCallee.isFlagged(),      // flagged?
-                                     false,                         // out-of-context?
-                                     hrnDstCallee.getType(),        // type                             
-                                     hrnDstCallee.getAllocSite(),   // allocation site                  
-                                     toCallerContext( hrnDstCallee.getInherent(),
-                                                      calleeStatesSatisfied  ),    // inherent reach
-                                     toCallerContext( hrnDstCallee.getAlpha(),
-                                                      calleeStatesSatisfied  ),    // current reach                 
-                                     predsTrue,                     // predicates
-                                     hrnDstCallee.getDescription()  // description
-                                     );                                        
-        }
-
-        TypeDescriptor tdNewEdge =
-          mostSpecificType( reCallee.getType(),
-                            hrnDstCallee.getType(),
-                            hrnDstCaller.getType()
-                            );       
-
-        RefEdge reCaller = new RefEdge( vnLhsCaller,
-                                        hrnDstCaller,
-                                        tdNewEdge,
-                                        null,
-                                        toCallerContext( reCallee.getBeta(),
-                                                         calleeStatesSatisfied ),
-                                        predsTrue
-                                        );
-
-        addRefEdge( vnLhsCaller, hrnDstCaller, reCaller );
-      }
-    }
-
-
-
-    if( writeDebugDOTs ) {
-      writeGraph( "caller38propagateReach", 
+      writeGraph( debugGraphPrefix+"caller38propagateReach", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
 
@@ -2571,12 +2837,15 @@ public class ReachGraph {
 
 
 
+
     if( writeDebugDOTs ) {
-      writeGraph( "caller40BeforeShadowMerge", 
+      writeGraph( debugGraphPrefix+"caller40BeforeShadowMerge", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
     
@@ -2670,12 +2939,18 @@ public class ReachGraph {
     }
 
 
+
+
+
+
     if( writeDebugDOTs ) {
-      writeGraph( "caller45BeforeUnshadow", 
+      writeGraph( debugGraphPrefix+"caller45BeforeUnshadow", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
     
@@ -2696,12 +2971,15 @@ public class ReachGraph {
     
 
 
+
     if( writeDebugDOTs ) {
-      writeGraph( "caller50BeforeGlobalSweep", 
+      writeGraph( debugGraphPrefix+"caller50BeforeGlobalSweep", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThidePreds,
                   resolveMethodDebugDOThideEdgeTaints );
     }
 
@@ -2712,14 +2990,15 @@ public class ReachGraph {
     }
     
 
-
     if( writeDebugDOTs ) {
-      writeGraph( "caller90AfterTransfer", 
+      writeGraph( debugGraphPrefix+"caller90AfterTransfer", 
                   resolveMethodDebugDOTwriteLabels,    
                   resolveMethodDebugDOTselectTemps,    
                   resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideReach,
                   resolveMethodDebugDOThideSubsetReach,
-                  resolveMethodDebugDOThideEdgeTaints );
+                  resolveMethodDebugDOThidePreds,
+                  resolveMethodDebugDOThideEdgeTaints );     
     }
   } 
 
@@ -3081,14 +3360,11 @@ public class ReachGraph {
               B = boldBooc.get( rtOld.getHrnID() ); 
             } else {
 
-
               if( !id2hrn.containsKey( rtOld.getHrnID() ) ) {
-                System.out.println( "\nLooking for "+rtOld );
-                writeGraph( "dbgz" );
+                // let symbols not in the graph get pruned
+                break;
               }
 
-
-              assert id2hrn.containsKey( rtOld.getHrnID() );
               B = boldBic.get( rtOld.getHrnID() ); 
             }
 
@@ -3262,23 +3538,132 @@ public class ReachGraph {
   }  
 
 
+  // a useful assertion for debugging:
+  // every in-context tuple on any edge or
+  // any node should name a node that is
+  // part of the graph
+  public boolean inContextTuplesInGraph() {
 
-  ////////////////////////////////////////////////////
-  // high-level merge operations
-  ////////////////////////////////////////////////////
-  public void merge_sameMethodContext( ReachGraph rg ) {
-    // when merging two graphs that abstract the heap
-    // of the same method context, we just call the
-    // basic merge operation
-    merge( rg );
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      {
+        Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+          
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+            
+            if( !rt.isOutOfContext() ) {
+              if( !id2hrn.containsKey( rt.getHrnID() ) ) {
+                System.out.println( rt.getHrnID()+" is missing" );
+                return false;
+              }
+            }
+          }
+        }
+      }
+
+      Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+      while( edgeItr.hasNext() ) {
+        RefEdge edge = edgeItr.next();
+
+        Iterator<ReachState> stateItr = edge.getBeta().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+        
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+            
+            if( !rt.isOutOfContext() ) {
+              if( !id2hrn.containsKey( rt.getHrnID() ) ) {
+                System.out.println( rt.getHrnID()+" is missing" );
+                return false;
+              }
+            }
+          }
+        }
+      }
+    }
+
+    return true;
   }
 
-  public void merge_diffMethodContext( ReachGraph rg ) {
-    // when merging graphs for abstract heaps in
-    // different method contexts we should:
-    // 1) age the allocation sites?
-    merge( rg );
+
+  // another useful assertion for debugging
+  public boolean noEmptyReachSetsInGraph() {
+    
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      if( !hrn.isOutOfContext() && 
+          !hrn.isWiped()        &&
+          hrn.getAlpha().isEmpty() 
+          ) {
+        System.out.println( "!!! "+hrn+" has an empty ReachSet !!!" );
+        return false;
+      }
+
+      Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+      while( edgeItr.hasNext() ) {
+        RefEdge edge = edgeItr.next();
+
+        if( edge.getBeta().isEmpty() ) {
+          System.out.println( "!!! "+edge+" has an empty ReachSet !!!" );
+          return false;
+        }
+      }
+    }
+    
+    return true;
+  }
+
+
+  public boolean everyReachStateWTrue() {
+
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      {
+        Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+          
+          if( !state.getPreds().equals( predsTrue ) ) {
+            return false;
+          }
+        }
+      }
+
+      Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+      while( edgeItr.hasNext() ) {
+        RefEdge edge = edgeItr.next();
+
+        Iterator<ReachState> stateItr = edge.getBeta().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+
+          if( !state.getPreds().equals( predsTrue ) ) {
+            return false;
+          }
+        }
+      }
+    }
+
+    return true;
   }
+  
+
+
 
   ////////////////////////////////////////////////////
   // in merge() and equals() methods the suffix A
@@ -3297,6 +3682,7 @@ public class ReachGraph {
     mergeNodes     ( rg );
     mergeRefEdges  ( rg );
     mergeAllocSites( rg );
+    mergeAccessibleSet( rg );
   }
   
   protected void mergeNodes( ReachGraph rg ) {
@@ -3329,6 +3715,17 @@ public class ReachGraph {
                                        hrnA.getPreds()
                                        )
                        );
+
+
+
+        if( !hrnA.equals( hrnB ) ) {
+          rg.writeGraph( "graphA" );
+          this.writeGraph( "graphB" );
+          throw new Error( "flagged not matching" );
+        }
+
+
+
       }
     }
 
@@ -3403,14 +3800,19 @@ public class ReachGraph {
          assert edgeToMerge != null;
          edgeToMerge.setBeta(
                               Canonical.unionORpreds( edgeToMerge.getBeta(),
-                                               edgeA.getBeta() 
-                                               )
+                                                      edgeA.getBeta() 
+                                                      )
                               );
           edgeToMerge.setPreds(
                                Canonical.join( edgeToMerge.getPreds(),
                                                edgeA.getPreds()
                                                )
                                );
+          edgeToMerge.setTaints(
+                                Canonical.union( edgeToMerge.getTaints(),
+                                                 edgeA.getTaints()
+                                                 )
+                                );
        }
       }
     }
@@ -3474,6 +3876,11 @@ public class ReachGraph {
                                                 edgeA.getPreds()
                                                 )
                                 );
+          edgeToMerge.setTaints(
+                                Canonical.union( edgeToMerge.getTaints(),
+                                                 edgeA.getTaints()
+                                                 )
+                                );
        }
       }
     }
@@ -3482,6 +3889,23 @@ public class ReachGraph {
   protected void mergeAllocSites( ReachGraph rg ) {
     allocSites.addAll( rg.allocSites );
   }
+  
+  protected void mergeAccessibleSet( ReachGraph rg ){
+    // inaccesible status is prior to accessible status
+    
+    Set<TempDescriptor> varsToMerge=rg.getAccessibleVar();    
+    Set<TempDescriptor> varsRemoved=new HashSet<TempDescriptor>();
+    
+    for (Iterator iterator = accessibleVars.iterator(); iterator.hasNext();) {
+      TempDescriptor accessibleVar = (TempDescriptor) iterator.next();
+      if(!varsToMerge.contains(accessibleVar)){
+        varsRemoved.add(accessibleVar);
+      }
+    }
+    
+    accessibleVars.removeAll(varsRemoved);
+        
+  }
 
 
 
@@ -3527,6 +3951,10 @@ public class ReachGraph {
       }
       return false;
     }
+    
+    if( !accessibleVars.equals( rg.accessibleVars) ){
+      return false;
+    }
 
     // if everything is equal up to this point,
     // assert that allocSites is also equal--
@@ -3607,6 +4035,10 @@ public class ReachGraph {
       return false;
     }
 
+    if( !areallREinAandBequal( rg, this ) ) {
+      return false;
+    }    
+
     return true;
   }
 
@@ -3720,6 +4152,94 @@ public class ReachGraph {
   }
 
 
+  // can be used to assert monotonicity
+  static public boolean isNoSmallerThan( ReachGraph rgA, 
+                                         ReachGraph rgB ) {
+
+    //System.out.println( "*** Asking if A is no smaller than B ***" );
+
+
+    Iterator iA = rgA.id2hrn.entrySet().iterator();
+    while( iA.hasNext() ) {
+      Map.Entry      meA  = (Map.Entry)      iA.next();
+      Integer        idA  = (Integer)        meA.getKey();
+      HeapRegionNode hrnA = (HeapRegionNode) meA.getValue();
+
+      if( !rgB.id2hrn.containsKey( idA ) ) {
+        System.out.println( "  regions smaller" );
+       return false;
+      }
+
+      //HeapRegionNode hrnB = rgB.id2hrn.get( idA );
+      /* NOT EQUALS, NO SMALLER THAN!
+      if( !hrnA.equalsIncludingAlphaAndPreds( hrnB ) ) {
+        System.out.println( "  regions smaller" );
+       return false;
+      }
+      */
+    }
+    
+    // this works just fine, no smaller than
+    if( !areallVNinAalsoinBandequal( rgA, rgB ) ) {
+      System.out.println( "  vars smaller:" );
+      System.out.println( "    A:"+rgA.td2vn.keySet() );
+      System.out.println( "    B:"+rgB.td2vn.keySet() );
+      return false;
+    }
+
+
+    iA = rgA.id2hrn.entrySet().iterator();
+    while( iA.hasNext() ) {
+      Map.Entry      meA  = (Map.Entry)      iA.next();
+      Integer        idA  = (Integer)        meA.getKey();
+      HeapRegionNode hrnA = (HeapRegionNode) meA.getValue();
+
+      Iterator<RefEdge> reItr = hrnA.iteratorToReferencers();
+      while( reItr.hasNext() ) {
+        RefEdge    edgeA = reItr.next();
+        RefSrcNode rsnA  = edgeA.getSrc();
+
+        // we already checked that nodes were present
+        HeapRegionNode hrnB = rgB.id2hrn.get( hrnA.getID() );
+        assert hrnB != null;
+
+        RefSrcNode rsnB;
+        if( rsnA instanceof VariableNode ) {
+          VariableNode vnA = (VariableNode) rsnA;
+          rsnB = rgB.td2vn.get( vnA.getTempDescriptor() );
+
+        } else {
+          HeapRegionNode hrnSrcA = (HeapRegionNode) rsnA;
+          rsnB = rgB.id2hrn.get( hrnSrcA.getID() );
+        }
+        assert rsnB != null;
+
+        RefEdge edgeB = rsnB.getReferenceTo( hrnB,
+                                             edgeA.getType(),
+                                             edgeA.getField()
+                                             );
+        if( edgeB == null ) {
+          System.out.println( "  edges smaller:" );          
+          return false;
+        }        
+
+        // REMEMBER, IS NO SMALLER THAN
+        /*
+          System.out.println( "  edges smaller" );
+          return false;
+          }
+        */
+
+      }
+    }
+
+    
+    return true;
+  }
+
+
+
+
 
   // this analysis no longer has the "match anything"
   // type which was represented by null
@@ -3842,12 +4362,14 @@ public class ReachGraph {
   // the default signature for quick-and-dirty debugging
   public void writeGraph( String graphName ) {
     writeGraph( graphName,
-                true, // write labels
-                true, // label select
-                true, // prune garbage
-                true, // hide subset reachability
-                true, // hide edge taints
-                null  // in-context boundary
+                true,  // write labels
+                true,  // label select
+                true,  // prune garbage
+                false, // hide reachability
+                true,  // hide subset reachability
+                true,  // hide predicates
+                true,  // hide edge taints                
+                null   // in-context boundary
                 );
   }
 
@@ -3855,14 +4377,18 @@ public class ReachGraph {
                           boolean writeLabels,
                           boolean labelSelect,
                           boolean pruneGarbage,
+                          boolean hideReachability,
                           boolean hideSubsetReachability,
+                          boolean hidePredicates,
                           boolean hideEdgeTaints
                           ) {
     writeGraph( graphName,
                 writeLabels,
                 labelSelect,
                 pruneGarbage,
+                hideReachability,
                 hideSubsetReachability,
+                hidePredicates,
                 hideEdgeTaints,
                 null );
   }
@@ -3871,7 +4397,9 @@ public class ReachGraph {
                           boolean      writeLabels,
                           boolean      labelSelect,
                           boolean      pruneGarbage,
+                          boolean      hideReachability,
                           boolean      hideSubsetReachability,
+                          boolean      hidePredicates,
                           boolean      hideEdgeTaints,
                           Set<Integer> callerNodeIDsCopiedToCallee
                           ) {
@@ -3900,10 +4428,12 @@ public class ReachGraph {
           HeapRegionNode hrn = (HeapRegionNode) me.getValue();      
           
           if( callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) {
-            bw.write( "    "+hrn.toString()+
-                      hrn.toStringDOT( hideSubsetReachability )+
-                      ";\n" );
-            
+            bw.write( "    "+
+                      hrn.toString()+
+                      hrn.toStringDOT( hideReachability,
+                                       hideSubsetReachability,
+                                       hidePredicates )+
+                      ";\n" );            
           }
         }
         
@@ -3923,7 +4453,8 @@ public class ReachGraph {
         // not every node at an allocation is referenced
         // (think of it as garbage-collected), etc.
         if( !pruneGarbage        ||
-            hrn.isOutOfContext()
+            hrn.isOutOfContext() ||
+            (hrn.isFlagged() && hrn.getID() > 0 && !hrn.isWiped()) // a non-shadow flagged node
             ) {
           
           if( !visited.contains( hrn ) ) {
@@ -3931,7 +4462,9 @@ public class ReachGraph {
                                      bw,
                                      null,
                                      visited,
+                                     hideReachability,
                                      hideSubsetReachability,
+                                     hidePredicates,
                                      hideEdgeTaints,
                                      callerNodeIDsCopiedToCallee );
           }
@@ -3969,14 +4502,20 @@ public class ReachGraph {
                                        bw,
                                        null,
                                        visited,
+                                       hideReachability,
                                        hideSubsetReachability,
+                                       hidePredicates,
                                        hideEdgeTaints,
                                        callerNodeIDsCopiedToCallee );
             }
           
             bw.write( "  "+vn.toString()+
                       " -> "+hrn.toString()+
-                      edge.toStringDOT( hideSubsetReachability, "" )+
+                      edge.toStringDOT( hideReachability,
+                                        hideSubsetReachability,
+                                        hidePredicates,
+                                        hideEdgeTaints,
+                                        "" )+
                       ";\n" );
           }
         }
@@ -3990,14 +4529,17 @@ public class ReachGraph {
     }
   }
 
-  protected void traverseHeapRegionNodes( HeapRegionNode      hrn,
-                                          BufferedWriter      bw,
-                                          TempDescriptor      td,
-                                          Set<HeapRegionNode> visited,
-                                          boolean             hideSubsetReachability,
-                                          boolean             hideEdgeTaints,
-                                          Set<Integer>        callerNodeIDsCopiedToCallee
-                                          ) throws java.io.IOException {
+  protected void 
+    traverseHeapRegionNodes( HeapRegionNode      hrn,
+                             BufferedWriter      bw,
+                             TempDescriptor      td,
+                             Set<HeapRegionNode> visited,
+                             boolean             hideReachability,
+                             boolean             hideSubsetReachability,
+                             boolean             hidePredicates,
+                             boolean             hideEdgeTaints,
+                             Set<Integer>        callerNodeIDsCopiedToCallee
+                             ) throws java.io.IOException {
 
     if( visited.contains( hrn ) ) {
       return;
@@ -4010,8 +4552,11 @@ public class ReachGraph {
     if( callerNodeIDsCopiedToCallee == null ||
         !callerNodeIDsCopiedToCallee.contains( hrn.getID() ) 
         ) {
-      bw.write( "  "+hrn.toString()+
-                hrn.toStringDOT( hideSubsetReachability )+
+      bw.write( "  "+
+                hrn.toString()+
+                hrn.toStringDOT( hideReachability,
+                                 hideSubsetReachability,
+                                 hidePredicates )+
                 ";\n" );
     }
 
@@ -4028,25 +4573,41 @@ public class ReachGraph {
             ) {
           bw.write( "  "+hrn.toString()+
                     " -> "+hrnChild.toString()+
-                    edge.toStringDOT( hideSubsetReachability, ",color=blue" )+
+                    edge.toStringDOT( hideReachability,
+                                      hideSubsetReachability,
+                                      hidePredicates,
+                                      hideEdgeTaints,
+                                      ",color=blue" )+
                     ";\n");
         } else if( !callerNodeIDsCopiedToCallee.contains( hrnSrc.getID()       ) &&
                    callerNodeIDsCopiedToCallee.contains( edge.getDst().getID() )
                    ) {
           bw.write( "  "+hrn.toString()+
                     " -> "+hrnChild.toString()+
-                    edge.toStringDOT( hideSubsetReachability, ",color=blue,style=dashed" )+
+                    edge.toStringDOT( hideReachability,
+                                      hideSubsetReachability,
+                                      hidePredicates,
+                                      hideEdgeTaints,
+                                      ",color=blue,style=dashed" )+
                     ";\n");
         } else {
           bw.write( "  "+hrn.toString()+
                     " -> "+hrnChild.toString()+
-                    edge.toStringDOT( hideSubsetReachability, "" )+
+                    edge.toStringDOT( hideReachability,
+                                      hideSubsetReachability,
+                                      hidePredicates,
+                                      hideEdgeTaints,
+                                      "" )+
                     ";\n");
         }
       } else {
         bw.write( "  "+hrn.toString()+
                   " -> "+hrnChild.toString()+
-                  edge.toStringDOT( hideSubsetReachability, "" )+
+                  edge.toStringDOT( hideReachability,
+                                    hideSubsetReachability,
+                                    hidePredicates,
+                                    hideEdgeTaints,
+                                    "" )+
                   ";\n");
       }
       
@@ -4054,7 +4615,9 @@ public class ReachGraph {
                                bw,
                                td,
                                visited,
+                               hideReachability,
                                hideSubsetReachability,
+                               hidePredicates,
                                hideEdgeTaints,
                                callerNodeIDsCopiedToCallee );
     }
@@ -4402,5 +4965,18 @@ public class ReachGraph {
     }
 
     return common;
+  }
+  
+  public void addAccessibleVar(TempDescriptor td){
+    accessibleVars.add(td);
+  }
+  
+  public Set<TempDescriptor> getAccessibleVar(){
+    return accessibleVars;
+  }
+  
+  public void clearAccessibleVarSet(){
+    accessibleVars.clear();
   }  
+  
 }