couple fixes to make sure out-of-context nodes get all the states they need, and...
[IRC.git] / Robust / src / Analysis / Disjoint / ReachGraph.java
index e695e57060fb7e40899aabb3f8fd055534738b04..3f13f4901b268c0adab3040bdd5c70062f6b4f8e 100644 (file)
@@ -10,7 +10,7 @@ public class ReachGraph {
 
   // use to disable improvements for comparison
   protected static final boolean DISABLE_STRONG_UPDATES = false;
-  protected static final boolean DISABLE_GLOBAL_SWEEP   = true;
+  protected static final boolean DISABLE_GLOBAL_SWEEP   = false;
                   
   // a special out-of-scope temp
   protected static final TempDescriptor tdReturn = new TempDescriptor( "_Return___" );
@@ -63,6 +63,24 @@ public class ReachGraph {
   }
 
 
+  // this suite of methods can be used to assert a
+  // very important property of ReachGraph objects:
+  // some element, HeapRegionNode, RefEdge etc.
+  // should be referenced by at most ONE ReachGraph!!
+  // If a heap region or edge or variable should be
+  // in another graph, make a new object with
+  // equivalent properties for a new graph
+  public boolean belongsToThis( RefSrcNode rsn ) {
+    if( rsn instanceof VariableNode ) {
+      VariableNode vn = (VariableNode) rsn;
+      return this.td2vn.get( vn.getTempDescriptor() ) == vn;
+    }
+    HeapRegionNode hrn = (HeapRegionNode) rsn;
+    return this.id2hrn.get( hrn.getID() ) == hrn;
+  }
+
+
+
   // the reason for this method is to have the option
   // of creating new heap regions with specific IDs, or
   // duplicating heap regions with specific IDs (especially
@@ -107,7 +125,8 @@ public class ReachGraph {
                            ReachState.factory(
                                               ReachTuple.factory( id,
                                                                   !isSingleObject,
-                                                                  ReachTuple.ARITY_ONE
+                                                                  ReachTuple.ARITY_ONE,
+                                                                  false // out-of-context
                                                                   )
                                               )
                            );
@@ -120,10 +139,7 @@ public class ReachGraph {
       alpha = inherent;
     }
 
-    if( preds == null ) {
-      // TODO: do this right?  For out-of-context nodes?
-      preds = ExistPredSet.factory();
-    }
+    assert preds != null;
     
     HeapRegionNode hrn = new HeapRegionNode( id,
                                             isSingleObject,
@@ -160,6 +176,8 @@ public class ReachGraph {
     assert edge       != null;
     assert edge.getSrc() == referencer;
     assert edge.getDst() == referencee;
+    assert belongsToThis( referencer );
+    assert belongsToThis( referencee );
 
     // edges are getting added twice to graphs now, the
     // kind that should have abstract facts merged--use
@@ -253,6 +271,25 @@ public class ReachGraph {
     }
   }
 
+  protected void clearNonVarRefEdgesTo( HeapRegionNode referencee ) {
+    assert referencee != null;
+
+    // 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
+    Iterator<RefEdge> i = referencee.iteratorToReferencersClone();
+    while( i.hasNext() ) {
+      RefEdge edge = i.next();
+      RefSrcNode referencer = edge.getSrc();
+      if( !(referencer instanceof VariableNode) ) {
+       removeRefEdge( referencer,
+                       referencee,
+                       edge.getType(),
+                       edge.getField() );
+      }
+    }
+  }
+
 
   ////////////////////////////////////////////////////
   //
@@ -366,7 +403,7 @@ public class ReachGraph {
        TypeDescriptor tdNewEdge =
          mostSpecificType( edgeHrn.getType(), 
                            hrnHrn.getType() 
-                           );       
+                           );
          
        RefEdge edgeNew = new RefEdge( lnX,
                                        hrnHrn,
@@ -376,7 +413,7 @@ public class ReachGraph {
                                        predsTrue
                                        );
        
-       addRefEdge( lnX, hrnHrn, edgeNew );     
+       addRefEdge( lnX, hrnHrn, edgeNew );
       }
     }
 
@@ -535,7 +572,7 @@ public class ReachGraph {
        
        if( edgeExisting != null ) {
          edgeExisting.setBeta(
-                               Canonical.union( edgeExisting.getBeta(),
+                               Canonical.unionORpreds( edgeExisting.getBeta(),
                                                 edgeNew.getBeta()
                                                 )
                                );
@@ -648,7 +685,7 @@ public class ReachGraph {
 
       // retrieve the summary node, or make it
       // from scratch
-      HeapRegionNode hrnSummary = getSummaryNode( as );      
+      HeapRegionNode hrnSummary = getSummaryNode( as, false );      
       
       mergeIntoSummary( hrnK, hrnSummary );
     }
@@ -658,23 +695,17 @@ public class ReachGraph {
     // to and from i-1 to node i.
     for( int i = allocationDepth - 1; i > 0; --i ) {
 
-      // if the target (ith) node exists, clobber it
-      // whether the i-1 node exists or not
-      Integer idIth = as.getIthOldest( i );
-      if( id2hrn.containsKey( idIth ) ) {
-        HeapRegionNode hrnI = id2hrn.get( idIth );
-
-        // clear all references in and out
-        wipeOut( hrnI );
-      }
-
       // only do the transfer if the i-1 node exists
       Integer idImin1th = as.getIthOldest( i - 1 );
       if( id2hrn.containsKey( idImin1th ) ) {
         HeapRegionNode hrnImin1 = id2hrn.get( idImin1th );
+        if( hrnImin1.isWiped() ) {
+          // there is no info on this node, just skip
+          continue;
+        }
 
         // either retrieve or make target of transfer
-        HeapRegionNode hrnI = getIthNode( as, i );
+        HeapRegionNode hrnI = getIthNode( as, i, false );
 
         transferOnto( hrnImin1, hrnI );
       }
@@ -684,8 +715,8 @@ public class ReachGraph {
     // as stated above, the newest node should have had its
     // references moved over to the second oldest, so we wipe newest
     // in preparation for being the new object to assign something to
-    HeapRegionNode hrn0 = getIthNode( as, 0 );
-    wipeOut( hrn0 );
+    HeapRegionNode hrn0 = getIthNode( as, 0, false );
+    wipeOut( hrn0, true );
 
     // now tokens in reachability sets need to "age" also
     Iterator itrAllVariableNodes = td2vn.entrySet().iterator();
@@ -721,9 +752,16 @@ public class ReachGraph {
 
 
   // either retrieve or create the needed heap region node
-  protected HeapRegionNode getSummaryNode( AllocSite as ) {
+  protected HeapRegionNode getSummaryNode( AllocSite as, 
+                                           boolean   shadow ) {
+
+    Integer idSummary;
+    if( shadow ) {
+      idSummary = as.getSummaryShadow();
+    } else {
+      idSummary = as.getSummary();
+    }
 
-    Integer        idSummary  = as.getSummary();
     HeapRegionNode hrnSummary = id2hrn.get( idSummary );
 
     if( hrnSummary == null ) {
@@ -738,6 +776,10 @@ public class ReachGraph {
       }
 
       String strDesc = as.toStringForDOT()+"\\nsummary";
+      if( shadow ) {
+        strDesc += " shadow";
+      }
+
       hrnSummary = 
         createNewHeapRegionNode( idSummary,    // id or null to generate a new one 
                                  false,        // single object?                
@@ -757,9 +799,17 @@ public class ReachGraph {
   }
 
   // either retrieve or create the needed heap region node
-  protected HeapRegionNode getIthNode( AllocSite as, Integer i ) {
+  protected HeapRegionNode getIthNode( AllocSite as, 
+                                       Integer   i, 
+                                       boolean   shadow ) {
 
-    Integer        idIth  = as.getIthOldest( i );
+    Integer idIth;
+    if( shadow ) {
+      idIth = as.getIthOldestShadow( i );
+    } else {
+      idIth = as.getIthOldest( i );
+    }
+    
     HeapRegionNode hrnIth = id2hrn.get( idIth );
     
     if( hrnIth == null ) {
@@ -774,6 +824,10 @@ public class ReachGraph {
       }
 
       String strDesc = as.toStringForDOT()+"\\n"+i+" oldest";
+      if( shadow ) {
+        strDesc += " shadow";
+      }
+
       hrnIth = createNewHeapRegionNode( idIth,        // id or null to generate a new one 
                                         true,        // single object?                  
                                         false,       // summary?                        
@@ -792,11 +846,16 @@ public class ReachGraph {
   }
 
 
-
   protected void mergeIntoSummary( HeapRegionNode hrn, 
                                    HeapRegionNode hrnSummary ) {
     assert hrnSummary.isNewSummary();
 
+    // assert that these nodes belong to THIS graph
+    assert belongsToThis( hrn );
+    assert belongsToThis( hrnSummary );
+
+    assert hrn != hrnSummary;
+
     // transfer references _from_ hrn over to hrnSummary
     Iterator<RefEdge> itrReferencee = hrn.iteratorToReferencees();
     while( itrReferencee.hasNext() ) {
@@ -813,22 +872,22 @@ public class ReachGraph {
       
       if( edgeSummary == null ) {
        // the merge is trivial, nothing to be done
+        addRefEdge( hrnSummary, hrnReferencee, edgeMerged );
+
       } else {
        // otherwise an edge from the referencer to hrnSummary exists already
        // and the edge referencer->hrn should be merged with it
-       edgeMerged.setBeta( 
-                           Canonical.union( edgeMerged.getBeta(),
-                                            edgeSummary.getBeta() 
-                                            ) 
-                            );
-        edgeMerged.setPreds( 
-                            Canonical.join( edgeMerged.getPreds(),
-                                            edgeSummary.getPreds() 
-                                            )
+       edgeSummary.setBeta( 
+                            Canonical.unionORpreds( edgeMerged.getBeta(),
+                                             edgeSummary.getBeta() 
+                                             ) 
                              );
+        edgeSummary.setPreds( 
+                             Canonical.join( edgeMerged.getPreds(),
+                                             edgeSummary.getPreds() 
+                                             )
+                              );
       }
-
-      addRefEdge( hrnSummary, hrnReferencee, edgeMerged );
     }
 
     // next transfer references _to_ hrn over to hrnSummary
@@ -847,72 +906,81 @@ public class ReachGraph {
 
       if( edgeSummary == null ) {
        // the merge is trivial, nothing to be done
+        addRefEdge( onReferencer, hrnSummary, edgeMerged );
+
       } else {
        // otherwise an edge from the referencer to alpha_S exists already
        // and the edge referencer->alpha_K should be merged with it
-       edgeMerged.setBeta( 
-                           Canonical.union( edgeMerged.getBeta(),
-                                            edgeSummary.getBeta() 
-                                            ) 
-                            );
-        edgeMerged.setPreds( 
-                            Canonical.join( edgeMerged.getPreds(),
-                                            edgeSummary.getPreds() 
-                                            )
+       edgeSummary.setBeta( 
+                            Canonical.unionORpreds( edgeMerged.getBeta(),
+                                             edgeSummary.getBeta() 
+                                             ) 
                              );
+        edgeSummary.setPreds( 
+                             Canonical.join( edgeMerged.getPreds(),
+                                             edgeSummary.getPreds() 
+                                             )
+                              );
       }
-
-      addRefEdge( onReferencer, hrnSummary, edgeMerged );
     }
 
     // then merge hrn reachability into hrnSummary
     hrnSummary.setAlpha( 
-                        Canonical.union( hrnSummary.getAlpha(),
+                        Canonical.unionORpreds( hrnSummary.getAlpha(),
                                          hrn.getAlpha() 
                                          )
                          );
+
+    hrnSummary.setPreds(
+                        Canonical.join( hrnSummary.getPreds(),
+                                        hrn.getPreds()
+                                        )
+                        );
+    
+    // and afterward, this node is gone
+    wipeOut( hrn, true );
   }
 
 
   protected void transferOnto( HeapRegionNode hrnA, 
                                HeapRegionNode hrnB ) {
 
-    // don't allow a heap region from one graph to
-    // get transferred onto a region from another
-    // graph!!  Do the transfer on the equivalent
-    // elements!
-    assert id2hrn.get( hrnA.getID() ) == hrnA;
-    assert id2hrn.get( hrnB.getID() ) == hrnB;
+    assert belongsToThis( hrnA );
+    assert belongsToThis( hrnB );
+    assert hrnA != hrnB;
 
-    // clear references in and out of node b
-    wipeOut( hrnB );
+    // clear references in and out of node b?
+    assert hrnB.isWiped();
 
-    // copy each edge in and out of A to B
+    // copy each: (edge in and out of A) to B
     Iterator<RefEdge> itrReferencee = hrnA.iteratorToReferencees();
     while( itrReferencee.hasNext() ) {
       RefEdge        edge          = itrReferencee.next();
       HeapRegionNode hrnReferencee = edge.getDst();
       RefEdge        edgeNew       = edge.copy();
       edgeNew.setSrc( hrnB );
-      edgeNew.setDst( hrnB );
+      edgeNew.setDst( hrnReferencee );
 
       addRefEdge( hrnB, hrnReferencee, edgeNew );
     }
 
     Iterator<RefEdge> itrReferencer = hrnA.iteratorToReferencers();
     while( itrReferencer.hasNext() ) {
-      RefEdge    edge         = itrReferencer.next();
-      RefSrcNode onReferencer = edge.getSrc();
-      RefEdge    edgeNew      = edge.copy();
-      edgeNew.setDst( hrnB );
+      RefEdge    edge          = itrReferencer.next();
+      RefSrcNode rsnReferencer = edge.getSrc();
+      RefEdge    edgeNew       = edge.copy();
+      edgeNew.setSrc( rsnReferencer );
       edgeNew.setDst( hrnB );
 
-      addRefEdge( onReferencer, hrnB, edgeNew );
+      addRefEdge( rsnReferencer, hrnB, edgeNew );
     }
 
     // replace hrnB reachability and preds with hrnA's
     hrnB.setAlpha( hrnA.getAlpha() );
     hrnB.setPreds( hrnA.getPreds() );
+
+    // after transfer, wipe out source
+    wipeOut( hrnA, true );
   }
 
 
@@ -921,9 +989,19 @@ public class ReachGraph {
   // because the node is still hanging around in the graph, just
   // not mechanically connected or have any reach or predicate
   // information on it anymore--lots of ops can use this
-  protected void wipeOut( HeapRegionNode hrn ) {
+  protected void wipeOut( HeapRegionNode hrn,
+                          boolean        wipeVariableReferences ) {
+
+    assert belongsToThis( hrn );
+
     clearRefEdgesFrom( hrn, null, null, true );
-    clearRefEdgesTo  ( hrn, null, null, true );
+
+    if( wipeVariableReferences ) {
+      clearRefEdgesTo( hrn, null, null, true );
+    } else {
+      clearNonVarRefEdgesTo( hrn );
+    }
+
     hrn.setAlpha( rsetEmpty );
     hrn.setPreds( predsEmpty );
   }
@@ -999,8 +1077,10 @@ public class ReachGraph {
        Iterator<ChangeTuple> itrCprime = C.iterator();
        while( itrCprime.hasNext() ) {
          ChangeTuple c = itrCprime.next();
-         if( edgeF.getBeta().contains( c.getSetToMatch() ) ) {
-           changesToPass = Canonical.union( changesToPass, c );
+         if( edgeF.getBeta().containsIgnorePreds( c.getStateToMatch() ) 
+              != null
+              ) {
+           changesToPass = Canonical.add( changesToPass, c );
          }
        }
 
@@ -1042,7 +1122,7 @@ public class ReachGraph {
       // but this propagation may be only one of many concurrent
       // possible changes, so keep a running union with the node's
       // partially updated new alpha set
-      n.setAlphaNew( Canonical.union( n.getAlphaNew(),
+      n.setAlphaNew( Canonical.unionORpreds( n.getAlphaNew(),
                                       localDelta 
                                       )
                      );
@@ -1079,8 +1159,10 @@ public class ReachGraph {
       Iterator<ChangeTuple> itrC = C.iterator();
       while( itrC.hasNext() ) {
        ChangeTuple c = itrC.next();
-       if( edgeE.getBeta().contains( c.getSetToMatch() ) ) {
-         changesToPass = Canonical.union( changesToPass, c );
+       if( edgeE.getBeta().containsIgnorePreds( c.getStateToMatch() ) 
+            != null
+            ) {
+         changesToPass = Canonical.add( changesToPass, c );
        }
       }
 
@@ -1131,7 +1213,7 @@ public class ReachGraph {
       // but this propagation may be only one of many concurrent
       // possible changes, so keep a running union with the edge's
       // partially updated new beta set
-      e.setBetaNew( Canonical.union( e.getBetaNew(),
+      e.setBetaNew( Canonical.unionORpreds( e.getBetaNew(),
                                      localDelta  
                                      )
                     );
@@ -1141,278 +1223,708 @@ public class ReachGraph {
   }
 
 
+  // 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
+  protected RefEdge
+    getOutOfContextReferenceTo( HeapRegionNode hrn,
+                                TypeDescriptor srcType,
+                                TypeDescriptor refType,
+                                String         refField ) {
+    assert belongsToThis( hrn );
+
+    HeapRegionNode hrnInContext = id2hrn.get( hrn.getID() );
+    if( hrnInContext == null ) {
+      return null;
+    }
+
+    Iterator<RefEdge> refItr = hrnInContext.iteratorToReferencers();
+    while( refItr.hasNext() ) {
+      RefEdge re = refItr.next();
+
+      assert belongsToThis( re.getSrc() );
+      assert belongsToThis( re.getDst() );
+
+      if( !(re.getSrc() instanceof HeapRegionNode) ) {
+        continue;
+      }
+
+      HeapRegionNode hrnSrc = (HeapRegionNode) re.getSrc();
+      if( !hrnSrc.isOutOfContext() ) {
+        continue;
+      }
+      
+      if( srcType == null ) {
+        if( hrnSrc.getType() != null ) {
+          continue;
+        }
+      } else {
+        if( !srcType.equals( hrnSrc.getType() ) ) {
+          continue;
+        }
+      }
+
+      if( !re.typeEquals( refType ) ) {
+        continue;
+      }
+
+      if( !re.fieldEquals( refField ) ) {
+        continue;
+      }
+
+      // tada!  We found it!
+      return re;
+    }
+    
+    return null;
+  }
+
+  // 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,
+                                      Set<ReachTuple> oocTuples
+                                      ) {
+    ReachSet out = ReachSet.factory();
+   
+    Iterator<ReachState> itr = rs.iterator();
+    while( itr.hasNext() ) {
+      ReachState stateCaller = itr.next();
+    
+      ReachState stateCallee = stateCaller;
+
+      Iterator<AllocSite> asItr = allocSites.iterator();
+      while( asItr.hasNext() ) {
+        AllocSite as = asItr.next();
+
+        ReachState stateNew = ReachState.factory();
+        Iterator<ReachTuple> rtItr = stateCallee.iterator();
+        while( rtItr.hasNext() ) {
+          ReachTuple rt = rtItr.next();
+
+          // only translate this tuple if it is
+          // in the out-callee-context bag
+          if( !oocTuples.contains( rt ) ) {
+            stateNew = Canonical.add( stateNew, rt );
+            continue;
+          }
+
+          int age = as.getAgeCategory( rt.getHrnID() );
+          
+          // this is the current mapping, where 0, 1, 2S were allocated
+          // in the current context, 0?, 1? and 2S? were allocated in a
+          // previous context, and we're translating to a future context
+          //
+          // 0    -> 0?
+          // 1    -> 1?
+          // 2S   -> 2S?
+          // 2S*  -> 2S?*
+          //
+          // 0?   -> 2S?
+          // 1?   -> 2S?
+          // 2S?  -> 2S?
+          // 2S?* -> 2S?*
+      
+          if( age == AllocSite.AGE_notInThisSite ) {
+            // things not from the site just go back in
+            stateNew = Canonical.add( stateNew, rt );
+
+          } else if( age == AllocSite.AGE_summary ||
+                     rt.isOutOfContext()
+                     ) {
+            // the in-context summary and all existing out-of-context
+            // stuff all become
+            stateNew = Canonical.add( stateNew,
+                                      ReachTuple.factory( as.getSummary(),
+                                                          true, // multi
+                                                          rt.getArity(),
+                                                          true  // out-of-context
+                                                          )
+                                      );
+          } else {
+            // otherwise everything else just goes to an out-of-context
+            // version, everything else the same
+            Integer I = as.getAge( rt.getHrnID() );
+            assert I != null;
+
+            assert !rt.isMultiObject();
+
+            stateNew = Canonical.add( stateNew,
+                                      ReachTuple.factory( rt.getHrnID(),
+                                                          rt.isMultiObject(),
+                                                          rt.getArity(),
+                                                          true  // out-of-context
+                                                          )
+                                      );        
+          }
+        }
+        
+        stateCallee = stateNew;
+      }
+      
+      // attach the passed in preds
+      stateCallee = Canonical.attach( stateCallee,
+                                      preds );
+
+      out = Canonical.add( out,
+                           stateCallee
+                           );
+
+    }
+    assert out.isCanonical();
+    return out;
+  }
+
+  // used below to convert a ReachSet to its caller-context
+  // equivalent with respect to allocation sites in this graph
+  protected ReachSet 
+    toCallerContext( ReachSet                            rs,
+                     Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied 
+                     ) {
+    ReachSet out = ReachSet.factory();
+
+    Iterator<ReachState> itr = rs.iterator();
+    while( itr.hasNext() ) {
+      ReachState stateCallee = itr.next();
+
+      if( calleeStatesSatisfied.containsKey( stateCallee ) ) {
+
+        // starting from one callee state...
+        ReachSet rsCaller = ReachSet.factory( stateCallee );
+
+        // possibly branch it into many states, which any
+        // allocation site might do, so lots of derived states
+        Iterator<AllocSite> asItr = allocSites.iterator();
+        while( asItr.hasNext() ) {
+          AllocSite as = asItr.next();
+          rsCaller = Canonical.toCallerContext( rsCaller, as );
+        }     
+        
+        // then before adding each derived, now caller-context
+        // states to the output, attach the appropriate pred
+        // based on the source callee state
+        Iterator<ReachState> stateItr = rsCaller.iterator();
+        while( stateItr.hasNext() ) {
+          ReachState stateCaller = stateItr.next();
+          stateCaller = Canonical.attach( stateCaller,
+                                          calleeStatesSatisfied.get( stateCallee )
+                                          );        
+          out = Canonical.add( out,
+                               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 ) {
+    ReachSet out = rs;
+    Iterator<AllocSite> asItr = allocSites.iterator();
+    while( asItr.hasNext() ) {
+      AllocSite as = asItr.next();
+      out = Canonical.unshadow( out, as );
+    }
+    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
   // this reach graph
   public ReachGraph 
-    makeCalleeView( FlatCall            fc,
-                    FlatMethod          fm,
-                    Set<HeapRegionNode> callerNodesCopiedToCallee,
-                    Set<RefEdge>        callerEdgesCopiedToCallee,
-                    boolean             writeDebugDOTs
+    makeCalleeView( FlatCall     fc,
+                    FlatMethod   fmCallee,
+                    Set<Integer> callerNodeIDsCopiedToCallee,
+                    boolean      writeDebugDOTs
                     ) {
 
-    // the callee view is a new graph: DON'T MODIFY
-    // *THIS* graph
-    ReachGraph rg = new ReachGraph();
 
-    // track what parts of this graph have already been
-    // added to callee view, variables not needed.
-    // Note that we need this because when we traverse
-    // this caller graph for each parameter we may find
-    // nodes and edges more than once (which the per-param
-    // "visit" sets won't show) and we only want to create
-    // an element in the new callee view one time
-    //Set callerNodesCopiedToCallee = new HashSet<HeapRegionNode>();
-    //Set callerEdgesCopiedToCallee = new HashSet<RefEdge>();
-
-
-    // a conservative starting point is to take the 
-    // mechanically-reachable-from-arguments graph
-    // as opposed to using reachability information
-    // to prune the graph further
-    for( int i = 0; i < fm.numParameters(); ++i ) {
-
-      // for each parameter index, get the symbol in the
-      // caller view and callee view
-      
-      // argument defined here is the symbol in the caller
-      TempDescriptor tdArg = fc.getArgMatchingParamIndex( fm, i );
+    // first traverse this context to find nodes and edges
+    //  that will be callee-reachable
+    Set<HeapRegionNode> reachableCallerNodes =
+      new HashSet<HeapRegionNode>();
 
-      // parameter defined here is the symbol in the callee
-      TempDescriptor tdParam = fm.getParameter( i );
-
-      // use these two VariableNode objects to translate
-      // between caller and callee--its easy to compare
-      // a HeapRegionNode across callee and caller because
-      // they will have the same heap region ID
-      VariableNode vnCaller = this.getVariableNodeFromTemp( tdArg );
-      VariableNode vnCallee = rg.getVariableNodeFromTemp( tdParam );
-      
-      // now traverse the calleR view using the argument to
-      // build the calleE view which has the parameter symbol
-      Set<RefSrcNode> toVisitInCaller = new HashSet<RefSrcNode>();
-      Set<RefSrcNode> visitedInCaller = new HashSet<RefSrcNode>();
-      toVisitInCaller.add( vnCaller );
+    // caller edges between callee-reachable nodes
+    Set<RefEdge> reachableCallerEdges =
+      new HashSet<RefEdge>();
 
-      while( !toVisitInCaller.isEmpty() ) {
-        RefSrcNode rsnCaller = toVisitInCaller.iterator().next();
-        RefSrcNode rsnCallee;
+    // caller edges from arg vars, and the matching param index
+    // because these become a special edge in callee
+    Hashtable<RefEdge, Integer> reachableCallerArgEdges2paramIndex =
+      new Hashtable<RefEdge, Integer>();
 
-        toVisitInCaller.remove( rsnCaller );
-        visitedInCaller.add( rsnCaller );
-        
-        // FIRST - setup the source end of an edge, and
-        // remember the identifying info of the source
-        // to build predicates
-        TempDescriptor tdSrc    = null;
-        Integer        hrnSrcID = null;
-
-        if( rsnCaller == vnCaller ) {
-          // if the caller node is the param symbol, we
-          // have to do this translation for the callee
-          rsnCallee = vnCallee;
-          tdSrc     = tdArg;
+    // caller edges from local vars or callee-unreachable nodes
+    // (out-of-context sources) to callee-reachable nodes
+    Set<RefEdge> oocCallerEdges =
+      new HashSet<RefEdge>();
 
-        } else {
-          // otherwise the callee-view node is a heap
-          // region with the same ID, that may or may
-          // not have been created already
-          assert rsnCaller instanceof HeapRegionNode;          
 
-          HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller;
-          hrnSrcID = hrnSrcCaller.getID(); 
+    for( int i = 0; i < fmCallee.numParameters(); ++i ) {
 
-          if( !callerNodesCopiedToCallee.contains( rsnCaller ) ) {
-            
-            ExistPred pred = 
-              ExistPred.factory( hrnSrcID, null );
-
-            ExistPredSet preds = 
-              ExistPredSet.factory( pred );
-
-            rsnCallee = 
-              rg.createNewHeapRegionNode( hrnSrcCaller.getID(),
-                                          hrnSrcCaller.isSingleObject(),
-                                          hrnSrcCaller.isNewSummary(),
-                                          hrnSrcCaller.isFlagged(),
-                                          false, // out-of-context?
-                                          hrnSrcCaller.getType(),
-                                          hrnSrcCaller.getAllocSite(),
-                                          /*toShadowTokens( this,*/ hrnSrcCaller.getInherent() /*)*/,
-                                          /*toShadowTokens( this,*/ hrnSrcCaller.getAlpha() /*)*/,
-                                          preds,
-                                          hrnSrcCaller.getDescription()
-                                          );
-            callerNodesCopiedToCallee.add( (HeapRegionNode) rsnCaller );
+      TempDescriptor tdArg = fc.getArgMatchingParamIndex( fmCallee, i );
+      VariableNode vnArgCaller = this.getVariableNodeFromTemp( tdArg );
 
-          } else {
-            rsnCallee = rg.id2hrn.get( hrnSrcID );
-          }
-        }
+      Set<RefSrcNode> toVisitInCaller = new HashSet<RefSrcNode>();
+      Set<RefSrcNode> visitedInCaller = new HashSet<RefSrcNode>();
 
-        // SECOND - go over all edges from that source
+      toVisitInCaller.add( vnArgCaller );
+      
+      while( !toVisitInCaller.isEmpty() ) {
+        RefSrcNode rsnCaller = toVisitInCaller.iterator().next();
+        toVisitInCaller.remove( rsnCaller );
+        visitedInCaller.add( rsnCaller );
 
         Iterator<RefEdge> itrRefEdges = rsnCaller.iteratorToReferencees();
         while( itrRefEdges.hasNext() ) {
           RefEdge        reCaller  = itrRefEdges.next();
           HeapRegionNode hrnCaller = reCaller.getDst();
-          HeapRegionNode hrnCallee;
 
-          // THIRD - setup destination ends of edges
-          Integer hrnDstID = hrnCaller.getID(); 
+          callerNodeIDsCopiedToCallee.add( hrnCaller.getID() );
+          reachableCallerNodes.add( hrnCaller );
 
-          if( !callerNodesCopiedToCallee.contains( hrnCaller ) ) {
-
-            ExistPred pred = 
-              ExistPred.factory( hrnDstID, null );
-
-            ExistPredSet preds = 
-              ExistPredSet.factory( pred );
-            
-            hrnCallee = 
-              rg.createNewHeapRegionNode( hrnCaller.getID(),
-                                          hrnCaller.isSingleObject(),
-                                          hrnCaller.isNewSummary(),
-                                          hrnCaller.isFlagged(),
-                                          false, // out-of-context?
-                                          hrnCaller.getType(),
-                                          hrnCaller.getAllocSite(),
-                                          /*toShadowTokens( this,*/ hrnCaller.getInherent() /*)*/,
-                                          /*toShadowTokens( this,*/ hrnCaller.getAlpha() /*)*/,
-                                          preds,
-                                          hrnCaller.getDescription()
-                                          );
-            callerNodesCopiedToCallee.add( hrnCaller );
+          if( reCaller.getSrc() instanceof HeapRegionNode ) {
+            reachableCallerEdges.add( reCaller );
           } else {
-            hrnCallee = rg.id2hrn.get( hrnDstID );
+            if( rsnCaller.equals( vnArgCaller ) ) {
+              reachableCallerArgEdges2paramIndex.put( reCaller, i );
+            } else {
+              oocCallerEdges.add( reCaller );
+            }
           }
 
-          // FOURTH - copy edge over if needed
-          if( !callerEdgesCopiedToCallee.contains( reCaller ) ) {
-
-            ExistPred pred =
-              ExistPred.factory( tdSrc, 
-                                 hrnSrcID, 
-                                 hrnDstID,
-                                 reCaller.getType(),
-                                 reCaller.getField(),
-                                 null );
-
-            ExistPredSet preds = 
-              ExistPredSet.factory( pred );
-
-            rg.addRefEdge( rsnCallee,
-                           hrnCallee,
-                           new RefEdge( rsnCallee,
-                                        hrnCallee,
-                                        reCaller.getType(),
-                                        reCaller.getField(),
-                                        /*toShadowTokens( this,*/ reCaller.getBeta() /*)*/,
-                                        preds
-                                        )
-                           );              
-            callerEdgesCopiedToCallee.add( reCaller );
-          }
-          
-          // keep traversing nodes reachable from param i
-          // that we haven't visited yet
           if( !visitedInCaller.contains( hrnCaller ) ) {
             toVisitInCaller.add( hrnCaller );
           }
           
-        } // end edge iteration        
+        } // end edge iteration
       } // end visiting heap nodes in caller
     } // end iterating over parameters as starting points
 
 
-    // find the set of edges in this graph with source
-    // out-of-context (not in nodes copied) and have a
-    // destination in context (one of nodes copied) as
-    // a starting point for building out-of-context nodes
-    Iterator<HeapRegionNode> itrInContext =
-      callerNodesCopiedToCallee.iterator();
+    // now collect out-of-context reach tuples and 
+    // more out-of-context edges
+    Set<ReachTuple> oocTuples = new HashSet<ReachTuple>();
+
+    Iterator<Integer> itrInContext = 
+      callerNodeIDsCopiedToCallee.iterator();
     while( itrInContext.hasNext() ) {
-      HeapRegionNode hrnCallerAndInContext = itrInContext.next();
+      Integer        hrnID                 = itrInContext.next();
+      HeapRegionNode hrnCallerAndInContext = id2hrn.get( hrnID );
       
       Iterator<RefEdge> itrMightCross =
         hrnCallerAndInContext.iteratorToReferencers();
       while( itrMightCross.hasNext() ) {
-        RefEdge edgeMightCross = itrMightCross.next();
-
-        // we're only interested in edges with a source
-        // 1) out-of-context and 2) is a heap region
-        if( callerNodesCopiedToCallee.contains( edgeMightCross.getSrc() ) ||
-            !(edgeMightCross.getSrc() instanceof HeapRegionNode)
-            ) { 
-          // then just skip
+        RefEdge edgeMightCross = itrMightCross.next();        
+
+        RefSrcNode rsnCallerAndOutContext =
+          edgeMightCross.getSrc();
+        
+        if( rsnCallerAndOutContext instanceof VariableNode ) {
+          // variables do not have out-of-context reach states,
+          // so jump out now
+          oocCallerEdges.add( edgeMightCross );
           continue;
         }
-
+          
         HeapRegionNode hrnCallerAndOutContext = 
-          (HeapRegionNode) edgeMightCross.getSrc();
+          (HeapRegionNode) rsnCallerAndOutContext;
 
-        // we found a reference that crosses from out-of-context
-        // to in-context, so build a special out-of-context node
-        // for the callee IHM and its reference edge
-        HeapRegionNode hrnCalleeAndOutContext =
-          rg.createNewHeapRegionNode( null,  // ID
-                                      false, // single object?
-                                      false, // new summary?
-                                      false, // flagged?
-                                      true,  // out-of-context?
-                                      hrnCallerAndOutContext.getType(),
-                                      null,  // alloc site, shouldn't be used
-                                      /*toShadowTokens( this,*/ hrnCallerAndOutContext.getAlpha() /*)*/, // inherent
-                                      /*toShadowTokens( this,*/ hrnCallerAndOutContext.getAlpha() /*)*/, // alpha
-                                      predsEmpty,
-                                      "out-of-context"
-                                      );
-       
-        HeapRegionNode hrnCalleeAndInContext = 
-          rg.id2hrn.get( hrnCallerAndInContext.getID() );
+        // is this source node out-of-context?
+        if( callerNodeIDsCopiedToCallee.contains( hrnCallerAndOutContext.getID() ) ) {
+          // no, skip this edge
+          continue;
+        }
+
+        // okay, we got one
+        oocCallerEdges.add( edgeMightCross );
+
+        // add all reach tuples on the node to list
+        // of things that are out-of-context: insight
+        // if this node is reachable from someting that WAS
+        // in-context, then this node should already be in-context
+        Iterator<ReachState> stateItr = hrnCallerAndOutContext.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+
+            oocTuples.add( rt );
+          }
+        }
+      }
+    }
+
+
+    // the callee view is a new graph: DON'T MODIFY *THIS* graph
+    ReachGraph rg = new ReachGraph();
+
+    // add nodes to callee graph
+    Iterator<HeapRegionNode> hrnItr = reachableCallerNodes.iterator();
+    while( hrnItr.hasNext() ) {
+      HeapRegionNode hrnCaller = hrnItr.next();
+
+      assert callerNodeIDsCopiedToCallee.contains( hrnCaller.getID() );
+      assert !rg.id2hrn.containsKey( hrnCaller.getID() );
+            
+      ExistPred    pred  = ExistPred.factory( hrnCaller.getID(), null );
+      ExistPredSet preds = ExistPredSet.factory( pred );
+      
+      rg.createNewHeapRegionNode( hrnCaller.getID(),
+                                  hrnCaller.isSingleObject(),
+                                  hrnCaller.isNewSummary(),
+                                  hrnCaller.isFlagged(),
+                                  false, // out-of-context?
+                                  hrnCaller.getType(),
+                                  hrnCaller.getAllocSite(),
+                                  toCalleeContext( hrnCaller.getInherent(),
+                                                   preds,
+                                                   oocTuples 
+                                                   ),
+                                  toCalleeContext( hrnCaller.getAlpha(),
+                                                   preds,
+                                                   oocTuples 
+                                                   ),
+                                  preds,
+                                  hrnCaller.getDescription()
+                                  );
+    }
+
+    // add param edges to callee graph
+    Iterator argEdges = 
+      reachableCallerArgEdges2paramIndex.entrySet().iterator();
+    while( argEdges.hasNext() ) {
+      Map.Entry me    = (Map.Entry) argEdges.next();
+      RefEdge   reArg = (RefEdge)   me.getKey();
+      Integer   index = (Integer)   me.getValue();
+      
+      TempDescriptor arg = fmCallee.getParameter( index );
+      
+      VariableNode vnCallee = 
+        rg.getVariableNodeFromTemp( arg );
+      
+      HeapRegionNode hrnDstCaller = reArg.getDst();
+      HeapRegionNode hrnDstCallee = rg.id2hrn.get( hrnDstCaller.getID() );
+      assert hrnDstCallee != null;
+      
+      ExistPred pred =
+        ExistPred.factory( arg,
+                           null, 
+                           hrnDstCallee.getID(),
+                           reArg.getType(),
+                           reArg.getField(),
+                           null,
+                           true,  // out-of-callee-context
+                           false  // out-of-caller-context
+                           );
+      
+      ExistPredSet preds = 
+        ExistPredSet.factory( pred );
+      
+      RefEdge reCallee = 
+        new RefEdge( vnCallee,
+                     hrnDstCallee,
+                     reArg.getType(),
+                     reArg.getField(),
+                     toCalleeContext( reArg.getBeta(),
+                                      preds,
+                                      oocTuples
+                                      ),
+                     preds
+                     );
+      
+      rg.addRefEdge( vnCallee,
+                     hrnDstCallee,
+                     reCallee
+                     );      
+    }
+
+    // add in-context edges to callee graph
+    Iterator<RefEdge> reItr = reachableCallerEdges.iterator();
+    while( reItr.hasNext() ) {
+      RefEdge    reCaller  = reItr.next();
+      RefSrcNode rsnCaller = reCaller.getSrc();
+      assert rsnCaller instanceof HeapRegionNode;
+      HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller;
+      HeapRegionNode hrnDstCaller = reCaller.getDst();
+
+      HeapRegionNode hrnSrcCallee = rg.id2hrn.get( hrnSrcCaller.getID() );
+      HeapRegionNode hrnDstCallee = rg.id2hrn.get( hrnDstCaller.getID() );
+      assert hrnSrcCallee != null;
+      assert hrnDstCallee != null;
+
+      ExistPred pred =
+        ExistPred.factory( null, 
+                           hrnSrcCallee.getID(), 
+                           hrnDstCallee.getID(),
+                           reCaller.getType(),
+                           reCaller.getField(),
+                           null,
+                           false, // out-of-callee-context
+                           false  // out-of-caller-context
+                           );
+      
+      ExistPredSet preds = 
+        ExistPredSet.factory( pred );
+      
+      RefEdge reCallee = 
+        new RefEdge( hrnSrcCallee,
+                     hrnDstCallee,
+                     reCaller.getType(),
+                     reCaller.getField(),
+                     toCalleeContext( reCaller.getBeta(),
+                                      preds,
+                                      oocTuples 
+                                      ),
+                     preds
+                     );
+      
+      rg.addRefEdge( hrnSrcCallee,
+                     hrnDstCallee,
+                     reCallee
+                     );        
+    }
+
+    // add out-of-context edges to callee graph
+    reItr = oocCallerEdges.iterator();
+    while( reItr.hasNext() ) {
+      RefEdge        reCaller     = reItr.next();
+      RefSrcNode     rsnCaller    = reCaller.getSrc();
+      HeapRegionNode hrnDstCaller = reCaller.getDst();
+      HeapRegionNode hrnDstCallee = rg.id2hrn.get( hrnDstCaller.getID() );
+      assert hrnDstCallee != null;
+
+      TypeDescriptor oocNodeType;
+      ReachSet       oocReach;
+      TempDescriptor oocPredSrcTemp = null;
+      Integer        oocPredSrcID   = null;
+      boolean        outOfCalleeContext;
+      boolean        outOfCallerContext;
+
+      if( rsnCaller instanceof VariableNode ) {
+        VariableNode vnCaller = (VariableNode) rsnCaller;
+        oocNodeType    = null;
+        oocReach       = rsetEmpty;
+        oocPredSrcTemp = vnCaller.getTempDescriptor();
+        outOfCalleeContext = true;
+        outOfCallerContext = false;
+
+      } else {
+        HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller;
+        assert !callerNodeIDsCopiedToCallee.contains( hrnSrcCaller.getID() );
+        oocNodeType  = hrnSrcCaller.getType();
+        oocReach     = hrnSrcCaller.getAlpha(); 
+        oocPredSrcID = hrnSrcCaller.getID();
+        if( hrnSrcCaller.isOutOfContext() ) {
+          outOfCalleeContext = false;
+          outOfCallerContext = true;
+        } else {
+          outOfCalleeContext = true;
+          outOfCallerContext = false;
+        }
+      }
+
+      ExistPred pred =
+        ExistPred.factory( oocPredSrcTemp, 
+                           oocPredSrcID, 
+                           hrnDstCallee.getID(),
+                           reCaller.getType(),
+                           reCaller.getField(),
+                           null,
+                           outOfCalleeContext,
+                           outOfCallerContext
+                           );
+
+      ExistPredSet preds = 
+        ExistPredSet.factory( pred );
+        
+      RefEdge oocEdgeExisting =
+        rg.getOutOfContextReferenceTo( hrnDstCallee,
+                                       oocNodeType,
+                                       reCaller.getType(),
+                                       reCaller.getField()
+                                       );
+
+      if( oocEdgeExisting == null ) {          
+          // for consistency, map one out-of-context "identifier"
+          // to one heap region node id, otherwise no convergence
+        String oocid = "oocid"+
+          fmCallee+
+          hrnDstCallee.getIDString()+
+          oocNodeType+
+          reCaller.getType()+
+          reCaller.getField();
+          
+        Integer oocHrnID = oocid2hrnid.get( oocid );
+
+        HeapRegionNode hrnCalleeAndOutContext;
+
+        if( oocHrnID == null ) {
+
+          hrnCalleeAndOutContext =
+            rg.createNewHeapRegionNode( null,  // ID
+                                        false, // single object?
+                                        false, // new summary?
+                                        false, // flagged?
+                                        true,  // out-of-context?
+                                        oocNodeType,
+                                        null,  // alloc site, shouldn't be used
+                                        toCalleeContext( oocReach,               
+                                                         preds,
+                                                         oocTuples
+                                                         ),
+                                        toCalleeContext( oocReach,
+                                                         preds,
+                                                         oocTuples
+                                                         ),
+                                        preds,
+                                        "out-of-context"
+                                        );       
+          
+          oocid2hrnid.put( oocid, hrnCalleeAndOutContext.getID() );
+          
+        } else {
+
+          // the mapping already exists, so see if node is there
+          hrnCalleeAndOutContext = rg.id2hrn.get( oocHrnID );
+
+          if( hrnCalleeAndOutContext == null ) {
+            // nope, make it
+            hrnCalleeAndOutContext =
+              rg.createNewHeapRegionNode( oocHrnID,  // ID
+                                          false, // single object?
+                                          false, // new summary?
+                                          false, // flagged?
+                                          true,  // out-of-context?
+                                          oocNodeType,
+                                          null,  // alloc site, shouldn't be used
+                                          toCalleeContext( oocReach,
+                                                           preds,
+                                                           oocTuples
+                                                           ),
+                                          toCalleeContext( oocReach,
+                                                           preds,
+                                                           oocTuples
+                                                           ),
+                                          preds,
+                                          "out-of-context"
+                                          );       
+          } else {
+            // otherwise it is there, so merge reachability
+            hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
+                                                                     toCalleeContext( oocReach,
+                                                                                      preds,
+                                                                                      oocTuples
+                                                                                      )
+                                                                     )
+                                             );
+          }
+        }
 
         rg.addRefEdge( hrnCalleeAndOutContext,
-                       hrnCalleeAndInContext,
+                       hrnDstCallee,
                        new RefEdge( hrnCalleeAndOutContext,
-                                    hrnCalleeAndInContext,
-                                    edgeMightCross.getType(),
-                                    edgeMightCross.getField(),
-                                    /*toShadowTokens( this,*/ edgeMightCross.getBeta() /*)*/,
-                                    predsEmpty
+                                    hrnDstCallee,
+                                    reCaller.getType(),
+                                    reCaller.getField(),
+                                    toCalleeContext( reCaller.getBeta(),
+                                                     preds,
+                                                     oocTuples
+                                                     ),
+                                    preds
                                     )
-                       );                              
-      }
-    }    
+                       );              
+        
+        } else {
+        // the out-of-context edge already exists
+        oocEdgeExisting.setBeta( Canonical.unionORpreds( oocEdgeExisting.getBeta(),
+                                                         toCalleeContext( reCaller.getBeta(),
+                                                                          preds,
+                                                                          oocTuples
+                                                                          )
+                                                  )
+                                 );         
+          
+        oocEdgeExisting.setPreds( Canonical.join( oocEdgeExisting.getPreds(),
+                                                  reCaller.getPreds()
+                                                  )
+                                  );          
+
+        HeapRegionNode hrnCalleeAndOutContext =
+          (HeapRegionNode) oocEdgeExisting.getSrc();
+        hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
+                                                                 toCalleeContext( oocReach,
+                                                                                  preds,
+                                                                                  oocTuples
+                                                                                  )
+                                                                 )
+                                         );
+        
+        
+      }                
+    }
 
 
     if( writeDebugDOTs ) {    
       try {
-        rg.writeGraph( "calleeview", true, false, false, false, true, true );
+        rg.writeGraph( "calleeview", 
+                       resolveMethodDebugDOTwriteLabels,    
+                       resolveMethodDebugDOTselectTemps,    
+                       resolveMethodDebugDOTpruneGarbage,   
+                       resolveMethodDebugDOThideSubsetReach,
+                       resolveMethodDebugDOThideEdgeTaints );
       } catch( IOException e ) {}
     }
 
-
     return rg;
   }  
 
+  private static Hashtable<String, Integer> oocid2hrnid = 
+    new Hashtable<String, Integer>();
+
+
+  // useful since many graphs writes in the method call debug code
+  private static boolean resolveMethodDebugDOTwriteLabels     = true;
+  private static boolean resolveMethodDebugDOTselectTemps     = true;
+  private static boolean resolveMethodDebugDOTpruneGarbage    = true;
+  private static boolean resolveMethodDebugDOThideSubsetReach = false;
+  private static boolean resolveMethodDebugDOThideEdgeTaints  = true;
+
+
+
   public void 
-    resolveMethodCall( FlatCall            fc,        
-                       FlatMethod          fm,        
-                       ReachGraph          rgCallee,
-                       Set<HeapRegionNode> callerNodesCopiedToCallee,
-                       Set<RefEdge>        callerEdgesCopiedToCallee,
-                       boolean             writeDebugDOTs
+    resolveMethodCall( FlatCall     fc,        
+                       FlatMethod   fmCallee,        
+                       ReachGraph   rgCallee,
+                       Set<Integer> callerNodeIDsCopiedToCallee,
+                       boolean      writeDebugDOTs
                        ) {
 
 
     if( writeDebugDOTs ) {
       try {
-        this.writeGraph( "caller", true, false, false, false, true, true, 
-                         callerNodesCopiedToCallee, callerEdgesCopiedToCallee );
-        rgCallee.writeGraph( "callee", true, false, false, false, true, true );
+        rgCallee.writeGraph( "callee", 
+                       resolveMethodDebugDOTwriteLabels,    
+                       resolveMethodDebugDOTselectTemps,    
+                       resolveMethodDebugDOTpruneGarbage,   
+                       resolveMethodDebugDOThideSubsetReach,
+                       resolveMethodDebugDOThideEdgeTaints );
+
+        writeGraph( "caller00In",  
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints,
+                    callerNodeIDsCopiedToCallee );
       } catch( IOException e ) {}
     }
 
@@ -1425,218 +1937,779 @@ public class ReachGraph {
     //    a) bring in nodes
     //    b) bring in callee -> callee edges
     //    c) resolve out-of-context -> callee edges
-    // 4. Global sweep it.
-
+    //    d) assign return value
+    // 4. Collapse shadow nodes down
+    // 5. Global sweep it.
 
 
-    if( writeDebugDOTs ) {
-      System.out.println( "doing call site, edges:"+callerEdgesCopiedToCallee );
-    }
-
 
     // 1. mark what callee elements have satisfied predicates
-    Set<HeapRegionNode> calleeNodesSatisfied =
-      new HashSet<HeapRegionNode>();
+    Hashtable<HeapRegionNode, ExistPredSet> calleeNodesSatisfied =
+      new Hashtable<HeapRegionNode, ExistPredSet>();
     
-    Set<RefEdge>        calleeEdgesSatisfied =
-      new HashSet<RefEdge>();
+    Hashtable<RefEdge, ExistPredSet> calleeEdgesSatisfied =
+      new Hashtable<RefEdge, ExistPredSet>();
+
+    Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied =
+      new Hashtable<ReachState, 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();
       Integer        id        = (Integer)        me.getKey();
       HeapRegionNode hrnCallee = (HeapRegionNode) me.getValue();
-    
-      if( hrnCallee.getPreds().isSatisfiedBy( this,
-                                              callerNodesCopiedToCallee,
-                                              callerEdgesCopiedToCallee
-                                              )
-          ) {
-        calleeNodesSatisfied.add( hrnCallee );
 
+      // if a callee element's predicates are satisfied then a set
+      // of CALLER predicates is returned: they are the predicates
+      // that the callee element moved into the caller context
+      // should have, and it is inefficient to find this again later
+      ExistPredSet predsIfSatis = 
+        hrnCallee.getPreds().isSatisfiedBy( this,
+                                            callerNodeIDsCopiedToCallee
+                                            );
+      if( predsIfSatis != null ) {
+        calleeNodesSatisfied.put( hrnCallee, predsIfSatis );
+      } else {
+        // otherwise don't bother looking at edges to this node
+        continue;
+      }
+      
+      // since the node is coming over, find out which reach
+      // states on it should come over, too
+      Iterator<ReachState> stateItr = hrnCallee.getAlpha().iterator();
+      while( stateItr.hasNext() ) {
+        ReachState stateCallee = stateItr.next();
+
+        predsIfSatis = 
+          stateCallee.getPreds().isSatisfiedBy( this,
+                                                callerNodeIDsCopiedToCallee
+                                                );
+        if( predsIfSatis != null ) {
+          calleeStatesSatisfied.put( stateCallee, predsIfSatis );
+        } 
+      }
+
+      // then look at edges to the node
+      Iterator<RefEdge> reItr = hrnCallee.iteratorToReferencers();
+      while( reItr.hasNext() ) {
+        RefEdge    reCallee  = reItr.next();
+        RefSrcNode rsnCallee = reCallee.getSrc();
+
+        // (caller local variables to in-context heap regions)
+        // 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)
+        // 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;
+        }        
+
+        // 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() ) {          
+
+          assert !calleeEdges2oocCallerSrcMatches.containsKey( reCallee );
+          Set<RefSrcNode> rsnCallers = new HashSet<RefSrcNode>();            
+
+          HeapRegionNode hrnDstCaller = this.id2hrn.get( hrnCallee.getID() );
+          Iterator<RefEdge> reDstItr = hrnDstCaller.iteratorToReferencers();
+          while( reDstItr.hasNext() ) {
+            // the edge and field (either possibly null) must match
+            RefEdge reCaller = reDstItr.next();
+
+            if( !reCaller.typeEquals ( reCallee.getType()  ) ||
+                !reCaller.fieldEquals( reCallee.getField() ) 
+                ) {
+              continue;
+            }
+            
+            RefSrcNode rsnCaller = reCaller.getSrc();
+            if( rsnCaller instanceof VariableNode ) {
+              // a variable node matches an OOC region with null type
+              if( hrnSrcCallee.getType() != null ) {
+                continue;
+              }
+
+            } else {
+              // 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;
+          }
+
+          if( !rsnCallers.isEmpty() ) {
+            calleeEdges2oocCallerSrcMatches.put( reCallee, rsnCallers );
+          }
+        }
+
+        if( hrnSrcCallee.isOutOfContext() &&
+            !matchedOutOfContext ) {
+          continue;
+        }
+        
+        predsIfSatis = 
+          reCallee.getPreds().isSatisfiedBy( this,
+                                             callerNodeIDsCopiedToCallee
+                                             );
+        if( predsIfSatis != null ) {
+          calleeEdgesSatisfied.put( reCallee, predsIfSatis );
+
+          // since the edge is coming over, find out which reach
+          // states on it should come over, too
+          stateItr = reCallee.getBeta().iterator();
+          while( stateItr.hasNext() ) {
+            ReachState stateCallee = stateItr.next();
+            
+            predsIfSatis = 
+              stateCallee.getPreds().isSatisfiedBy( this,
+                                                    callerNodeIDsCopiedToCallee
+                                                    );
+            if( predsIfSatis != null ) {
+              calleeStatesSatisfied.put( stateCallee, predsIfSatis );
+            } 
+          }
+        }        
+      }
+    }
+
+    // test param -> HRN edges, also
+    for( int i = 0; i < fmCallee.numParameters(); ++i ) {
+
+      // parameter defined here is the symbol in the callee
+      TempDescriptor tdParam  = fmCallee.getParameter( i );
+      VariableNode   vnCallee = rgCallee.getVariableNodeFromTemp( tdParam );
+
+      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 );
+
+          // 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
+                                                    );
+            if( predsIfSatis != null ) {
+              calleeStatesSatisfied.put( stateCallee, predsIfSatis );
+            } 
+          }
+
+        }        
+      }
+    }
+
+
+
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller20BeforeWipe", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
+
+
+    // 2. predicates tested, ok to wipe out caller part
+    Iterator<Integer> hrnItr = callerNodeIDsCopiedToCallee.iterator();
+    while( hrnItr.hasNext() ) {
+      Integer        hrnID     = hrnItr.next();
+      HeapRegionNode hrnCaller = id2hrn.get( hrnID );
+      assert hrnCaller != null;
+
+      // when clearing off nodes, also eliminate variable
+      // references
+      wipeOut( hrnCaller, true );
+    }
+
+
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller30BeforeAddingNodes", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
+
+
+    // 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
+    //    some caller element ER.  We bring EE into the caller
+    //    context as ERee with the preds of ER, namely ERp, which
+    //    in the following algorithm is the value in the mapping
+
+    // 3.a) nodes
+    Iterator satisItr = calleeNodesSatisfied.entrySet().iterator();
+    while( satisItr.hasNext() ) {
+      Map.Entry      me        = (Map.Entry)      satisItr.next();
+      HeapRegionNode hrnCallee = (HeapRegionNode) me.getKey();
+      ExistPredSet   preds     = (ExistPredSet)   me.getValue();
+
+      // TODO: I think its true that the current implementation uses
+      // the type of the OOC region and the predicates OF THE EDGE from
+      // it to link everything up in caller context, so that's why we're
+      // skipping this... maybe that's a sillier way to do it?
+      if( hrnCallee.isOutOfContext() ) {
+        continue;
+      }
+
+      AllocSite as = hrnCallee.getAllocSite();  
+      allocSites.add( as );
+
+      Integer hrnIDshadow = as.getShadowIDfromID( hrnCallee.getID() );
+
+      HeapRegionNode hrnCaller = id2hrn.get( hrnIDshadow );
+      if( hrnCaller == null ) {
+        hrnCaller =
+          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
+                                   null,                       // current reach                 
+                                   predsEmpty,                 // predicates
+                                   hrnCallee.getDescription()  // description
+                                   );                                        
+      } else {
+        assert hrnCaller.isWiped();
+      }
+
+      hrnCaller.setAlpha( toCallerContext( hrnCallee.getAlpha(),
+                                           calleeStatesSatisfied 
+                                           )
+                          );
+
+      hrnCaller.setPreds( preds );
+    }
+
+
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller31BeforeAddingEdges", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
+
+
+    // set these up during the next procedure so after
+    // the caller has all of its nodes and edges put
+    // back together we can propagate the callee's
+    // reach changes backwards into the caller graph
+    HashSet<RefEdge> edgesForPropagation = new HashSet<RefEdge>();
+
+    Hashtable<RefEdge, ChangeSet> edgePlannedChanges =
+      new Hashtable<RefEdge, ChangeSet>();
+
+
+    // 3.b) callee -> callee edges AND out-of-context -> callee
+    satisItr = calleeEdgesSatisfied.entrySet().iterator();
+    while( satisItr.hasNext() ) {
+      Map.Entry    me       = (Map.Entry)    satisItr.next();
+      RefEdge      reCallee = (RefEdge)      me.getKey();
+      ExistPredSet preds    = (ExistPredSet) me.getValue();
+
+      HeapRegionNode hrnDstCallee = reCallee.getDst();
+      AllocSite      asDst        = hrnDstCallee.getAllocSite();
+      allocSites.add( asDst );
+
+      Integer hrnIDDstShadow = 
+        asDst.getShadowIDfromID( hrnDstCallee.getID() );
+      
+      HeapRegionNode hrnDstCaller = id2hrn.get( hrnIDDstShadow );
+      assert hrnDstCaller != null;
+      
+      
+      RefSrcNode rsnCallee = reCallee.getSrc();
+
+      Set<RefSrcNode> rsnCallers =
+        new HashSet<RefSrcNode>();
+      
+      Set<RefSrcNode> oocCallers = 
+        calleeEdges2oocCallerSrcMatches.get( reCallee );
+
+      boolean oocEdges = false;
+      
+      if( oocCallers == null ) {
+        // there are no out-of-context matches, so it's
+        // either a param/arg var or one in-context heap region
+        if( rsnCallee instanceof VariableNode ) {
+          // variable -> node in the callee should only
+          // come into the caller if its from a param var
+          VariableNode   vnCallee = (VariableNode) rsnCallee;
+          TempDescriptor tdParam  = vnCallee.getTempDescriptor();
+          TempDescriptor tdArg    = fc.getArgMatchingParam( fmCallee,
+                                                            tdParam );
+          if( tdArg == null ) {
+            // this means the variable isn't a parameter, its local
+            // to the callee so we ignore it in call site transfer
+            // shouldn't this NEVER HAPPEN?
+            assert false;
+          }
+          rsnCallers.add( this.getVariableNodeFromTemp( tdArg ) );
+          oocEdges = true;
+
+        } else {
+          // otherwise source is in context, one region
+          HeapRegionNode hrnSrcCallee = (HeapRegionNode) rsnCallee;
 
-        
-        if( writeDebugDOTs ) {
-          System.out.println( "  node satissfied: "+hrnCallee );
+          // translate an in-context node to shadow
+          AllocSite asSrc = hrnSrcCallee.getAllocSite();
+          allocSites.add( asSrc );
+          
+          Integer hrnIDSrcShadow = 
+            asSrc.getShadowIDfromID( hrnSrcCallee.getID() );
+
+          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
+                                       );                                        
+          }
+          
+          rsnCallers.add( hrnSrcCallerShadow );
         }
 
+      } else {
+        // otherwise we have a set of out-of-context srcs
+        // that should NOT be translated to shadow nodes
+        assert !oocCallers.isEmpty();
+        rsnCallers.addAll( oocCallers );
+        oocEdges = true;
       }
 
-      Iterator<RefEdge> reItr = hrnCallee.iteratorToReferencees();
-      while( reItr.hasNext() ) {
-        RefEdge reCallee = reItr.next();
+      // now make all caller edges we've identified from
+      // this callee edge with a satisfied predicate
+      assert !rsnCallers.isEmpty();
+      Iterator<RefSrcNode> rsnItr = rsnCallers.iterator();
+      while( rsnItr.hasNext() ) {
+        RefSrcNode rsnCaller = rsnItr.next();
         
-        if( reCallee.getPreds().isSatisfiedBy( this,
-                                               callerNodesCopiedToCallee,
-                                               callerEdgesCopiedToCallee
-                                               )
-            ) {
-          calleeEdgesSatisfied.add( reCallee );
-        }        
-      }
-    }
+        RefEdge reCaller = new RefEdge( rsnCaller,
+                                        hrnDstCaller,
+                                        reCallee.getType(),
+                                        reCallee.getField(),
+                                        toCallerContext( reCallee.getBeta(),
+                                                         calleeStatesSatisfied ),
+                                        preds
+                                        );
 
-    // test param -> HRN edges, also
-    for( int i = 0; i < fm.numParameters(); ++i ) {
+        ChangeSet cs = ChangeSet.factory();
+        Iterator<ReachState> rsItr = reCaller.getBeta().iterator();
+        while( rsItr.hasNext() ) {
+          ReachState   state          = rsItr.next();
+          ExistPredSet predsPreCallee = state.getPreds();
 
-      // parameter defined here is the symbol in the callee
-      TempDescriptor tdParam  = fm.getParameter( i );
-      VariableNode   vnCallee = rgCallee.getVariableNodeFromTemp( tdParam );
+          if( state.isEmpty() ) {
+            continue;
+          }
 
-      Iterator<RefEdge> reItr = vnCallee.iteratorToReferencees();
-      while( reItr.hasNext() ) {
-        RefEdge reCallee = reItr.next();
+          Iterator<ExistPred> predItr = predsPreCallee.iterator();
+          while( predItr.hasNext() ) {            
+            ExistPred pred = predItr.next();
+            ReachState old = pred.ne_state;
 
+            if( old == null ) {
+              old = rstateEmpty;
+            }
 
-        if( writeDebugDOTs ) {
-          System.out.println( "  satisfied?: "+reCallee );
+            cs = Canonical.add( cs,
+                                ChangeTuple.factory( old,
+                                                     state
+                                                     )
+                                );
+          }
         }
-
         
-        if( reCallee.getPreds().isSatisfiedBy( this,
-                                               callerNodesCopiedToCallee,
-                                               callerEdgesCopiedToCallee
-                                               )
-            ) {
-          calleeEdgesSatisfied.add( reCallee );
 
-          if( writeDebugDOTs ) {
-            System.out.println( "  satisfied: "+reCallee );
-          }
-        }        
+        // 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()
+                                                )
+                                );
 
-        else 
-          if( writeDebugDOTs ) {
-            System.out.println( "  NOT satisfied: "+reCallee );
+          // for reach propagation
+          if( !cs.isEmpty() ) {
+            edgePlannedChanges.put( 
+                                   edgeExisting, 
+                                   Canonical.union( edgePlannedChanges.get( edgeExisting ),
+                                                    cs
+                                                    ) 
+                                    );
           }
+          
+        } else {                         
+          addRefEdge( rsnCaller, hrnDstCaller, reCaller );     
 
-
+          // for reach propagation
+          if( !cs.isEmpty() ) {
+            edgesForPropagation.add( reCaller );
+            assert !edgePlannedChanges.containsKey( reCaller );
+            edgePlannedChanges.put( reCaller, cs );
+          }
+        }
       }
-
     }
 
 
 
-    // 2. predicates tested, ok to wipe out caller part
-    Iterator<HeapRegionNode> hrnItr = callerNodesCopiedToCallee.iterator();
-    while( hrnItr.hasNext() ) {
-      HeapRegionNode hrnCaller = hrnItr.next();
-      wipeOut( hrnCaller );
 
-      if( writeDebugDOTs ) {
-        System.out.println( "  wiping: "+hrnCaller );
-      }
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller35BeforeAssignReturnValue", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
     }
 
 
-    // 3. callee elements with satisfied preds come in
 
-    // 3.a) nodes
-    hrnItr = calleeNodesSatisfied.iterator();
-    while( hrnItr.hasNext() ) {
-      HeapRegionNode hrnCallee = hrnItr.next();
+    // 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 && !returnTemp.getType().isImmutable() ) {
+
+      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;
+       }       
 
-      if( hrnCallee.isOutOfContext() ) {
-        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
+                                     );                                        
+        } else {
+          assert hrnDstCaller.isWiped();
+        }
 
-      HeapRegionNode hrnCaller = id2hrn.get( hrnCallee.getID() );
-      if( hrnCaller == null ) {
-        hrnCaller =
-          createNewHeapRegionNode( hrnCallee.getID(),          // 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                       
-                                   hrnCallee.getInherent(),    // inherent reach
-                                   null,                       // current reach                 
-                                   predsEmpty,                 // predicates
-                                   hrnCallee.getDescription()  // description
-                                   );                                        
-      }
+        TypeDescriptor tdNewEdge =
+          mostSpecificType( reCallee.getType(),
+                            hrnDstCallee.getType(),
+                            hrnDstCaller.getType()
+                            );       
+
+        RefEdge reCaller = new RefEdge( vnLhsCaller,
+                                        hrnDstCaller,
+                                        tdNewEdge,
+                                        null,
+                                        toCallerContext( reCallee.getBeta(),
+                                                         calleeStatesSatisfied ),
+                                        predsTrue
+                                        );
 
-      if( writeDebugDOTs ) {
-        System.out.println( "  stitching in: "+hrnCaller );
+        addRefEdge( vnLhsCaller, hrnDstCaller, reCaller );
       }
+    }
 
-      // TODO: alpha should be some rewritten version of callee in caller context
-      hrnCaller.setAlpha( rsetEmpty );
 
-      // TODO: predicates should be exact same from caller version that satisfied
-      hrnCaller.setPreds( predsTrue );
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller38propagateReach", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
+
+    // propagate callee reachability changes to the rest
+    // of the caller graph edges
+    HashSet<RefEdge> edgesUpdated = new HashSet<RefEdge>();
+  
+    propagateTokensOverEdges( edgesForPropagation, // source edges
+                              edgePlannedChanges,  // map src edge to change set
+                              edgesUpdated );      // list of updated edges
+    
+    // commit beta' (beta<-betaNew)
+    Iterator<RefEdge> edgeItr = edgesUpdated.iterator();
+    while( edgeItr.hasNext() ) {
+      edgeItr.next().applyBetaNew();
     }
 
-    // 3.b) callee -> callee edges
-    Iterator<RefEdge> reItr = calleeEdgesSatisfied.iterator();
-    while( reItr.hasNext() ) {
-      RefEdge reCallee = reItr.next();
 
-      RefSrcNode rsnCallee = reCallee.getSrc();
-      RefSrcNode rsnCaller;
 
-      if( rsnCallee instanceof VariableNode ) {          
-        VariableNode   vnCallee = (VariableNode) rsnCallee;
-        TempDescriptor tdParam  = vnCallee.getTempDescriptor();
-        TempDescriptor tdArg    = fc.getArgMatchingParam( fm,
-                                                          tdParam );
 
-        if( writeDebugDOTs ) {
-          System.out.println( "  considering: "+rsnCallee );
+
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller40BeforeShadowMerge", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
+    
+
+    // 4) merge shadow nodes so alloc sites are back to k
+    Iterator<AllocSite> asItr = rgCallee.allocSites.iterator();
+    while( asItr.hasNext() ) {
+      // for each allocation site do the following to merge
+      // shadow nodes (newest from callee) with any existing
+      // look for the newest normal and newest shadow "slot"
+      // not being used, transfer normal to shadow.  Keep
+      // doing this until there are no more normal nodes, or
+      // no empty shadow slots: then merge all remaining normal
+      // nodes into the shadow summary.  Finally, convert all
+      // shadow to their normal versions.
+      AllocSite as = asItr.next();
+      int ageNorm = 0;
+      int ageShad = 0;
+      while( ageNorm < allocationDepth &&
+             ageShad < allocationDepth ) {
+
+        // first, are there any normal nodes left?
+        Integer        idNorm  = as.getIthOldest( ageNorm );
+        HeapRegionNode hrnNorm = id2hrn.get( idNorm );
+        if( hrnNorm == null ) {
+          // no, this age of normal node not in the caller graph
+          ageNorm++;
+          continue;
         }
 
-        if( tdArg == null ) {
-          // this means the variable isn't a parameter, its local
-          // to the callee so we ignore it in call site transfer
+        // yes, a normal node exists, is there an empty shadow
+        // "slot" to transfer it onto?
+        HeapRegionNode hrnShad = getIthNode( as, ageShad, true );        
+        if( !hrnShad.isWiped() ) {
+          // no, this age of shadow node is not empty
+          ageShad++;
           continue;
         }
-        
-        rsnCaller = this.getVariableNodeFromTemp( tdArg );
+        // yes, this shadow node is empty
+        transferOnto( hrnNorm, hrnShad );
+        ageNorm++;
+        ageShad++;
+      }
 
-        if( writeDebugDOTs ) {
-          System.out.println( "  stitching in: "+rsnCaller );
+      // now, while there are still normal nodes but no shadow
+      // slots, merge normal nodes into the shadow summary
+      while( ageNorm < allocationDepth ) {
+
+        // first, are there any normal nodes left?
+        Integer        idNorm  = as.getIthOldest( ageNorm );
+        HeapRegionNode hrnNorm = id2hrn.get( idNorm );
+        if( hrnNorm == null ) {
+          // no, this age of normal node not in the caller graph
+          ageNorm++;
+          continue;
         }
-                  
-      } else {
-        HeapRegionNode hrnSrcCallee = (HeapRegionNode) reCallee.getSrc();
-        rsnCaller = id2hrn.get( hrnSrcCallee.getID() );
+
+        // yes, a normal node exists, so get the shadow summary
+        HeapRegionNode summShad = getSummaryNode( as, true );
+        mergeIntoSummary( hrnNorm, summShad );
+        ageNorm++;
+      }
+
+      // if there is a normal summary, merge it into shadow summary
+      Integer        idNorm   = as.getSummary();
+      HeapRegionNode summNorm = id2hrn.get( idNorm );
+      if( summNorm != null ) {
+        HeapRegionNode summShad = getSummaryNode( as, true );
+        mergeIntoSummary( summNorm, summShad );
       }
-            
-      assert rsnCaller != null;
       
-      HeapRegionNode hrnDstCallee = reCallee.getDst();
-      HeapRegionNode hrnDstCaller = id2hrn.get( hrnDstCallee.getID() );
-      assert hrnDstCaller != null;
+      // finally, flip all existing shadow nodes onto the normal
+      for( int i = 0; i < allocationDepth; ++i ) {
+        Integer        idShad  = as.getIthOldestShadow( i );
+        HeapRegionNode hrnShad = id2hrn.get( idShad );
+        if( hrnShad != null ) {
+          // flip it
+          HeapRegionNode hrnNorm = getIthNode( as, i, false );
+          assert hrnNorm.isWiped();
+          transferOnto( hrnShad, hrnNorm );
+        }
+      }
       
-      // TODO: beta rewrites, preds from satisfier in caller
-      RefEdge reCaller = new RefEdge( rsnCaller,
-                                      hrnDstCaller,
-                                      reCallee.getType(),
-                                      reCallee.getField(),
-                                      rsetEmpty,
-                                      predsTrue
-                                      );
-      addRefEdge( rsnCaller, hrnDstCaller, reCaller ); 
+      Integer        idShad   = as.getSummaryShadow();
+      HeapRegionNode summShad = id2hrn.get( idShad );
+      if( summShad != null ) {
+        summNorm = getSummaryNode( as, false );
+        transferOnto( summShad, summNorm );
+      }      
     }
 
-    // 3.c) resolve out-of-context -> callee edges
 
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller45BeforeUnshadow", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
+    
+    
+    Iterator itrAllHRNodes = id2hrn.entrySet().iterator();
+    while( itrAllHRNodes.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      itrAllHRNodes.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+      
+      hrn.setAlpha( unshadow( hrn.getAlpha() ) );
+      
+      Iterator<RefEdge> itrEdges = hrn.iteratorToReferencers();
+      while( itrEdges.hasNext() ) {
+        RefEdge re = itrEdges.next();
+        re.setBeta( unshadow( re.getBeta() ) );
+      }
+    }
     
 
-    // 4.
-    /*
-    globalSweep();
-    */
 
     if( writeDebugDOTs ) {
       try {
-        writeGraph( "callerAfter", 
-                    true, false, false, false, true, true, 
-                    null, null );
+        writeGraph( "caller50BeforeGlobalSweep", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
       } catch( IOException e ) {}
     }
 
+
+    // 5.
+    if( !DISABLE_GLOBAL_SWEEP ) {
+      globalSweep();
+    }
+    
+
+
+    if( writeDebugDOTs ) {
+      try {
+        writeGraph( "caller90AfterTransfer", 
+                    resolveMethodDebugDOTwriteLabels,    
+                    resolveMethodDebugDOTselectTemps,    
+                    resolveMethodDebugDOTpruneGarbage,   
+                    resolveMethodDebugDOThideSubsetReach,
+                    resolveMethodDebugDOThideEdgeTaints );
+      } catch( IOException e ) {}
+    }
   } 
 
   
@@ -1726,7 +2799,7 @@ public class ReachGraph {
         // nodes, so when a node is identified as garbage,
         // actively clear references to and from it so
         // live nodes won't have dangling RefEdge's
-        wipeOut( hrn );
+        wipeOut( hrn, true );
 
         // if we just removed the last node from an allocation
         // site, it should be taken out of the ReachGraph's list
@@ -1763,10 +2836,25 @@ public class ReachGraph {
   public void globalSweep() {
 
     // boldB is part of the phase 1 sweep
-    Hashtable< Integer, Hashtable<RefEdge, ReachSet> > boldB =
+    // it has an in-context table and an out-of-context table
+    Hashtable< Integer, Hashtable<RefEdge, ReachSet> > boldBic =
+      new Hashtable< Integer, Hashtable<RefEdge, ReachSet> >();    
+
+    Hashtable< Integer, Hashtable<RefEdge, ReachSet> > boldBooc =
       new Hashtable< Integer, Hashtable<RefEdge, ReachSet> >();    
 
-    // visit every heap region to initialize alphaNew and calculate boldB
+    // visit every heap region to initialize alphaNew and betaNew,
+    // and make a map of every hrnID to the source nodes it should
+    // propagate forward from.  In-context flagged hrnID's propagate
+    // from only the in-context node they name, but out-of-context
+    // ID's may propagate from several out-of-context nodes
+    Hashtable< Integer, Set<HeapRegionNode> > icID2srcs = 
+      new Hashtable< Integer, Set<HeapRegionNode> >();
+
+    Hashtable< Integer, Set<HeapRegionNode> > oocID2srcs =
+      new Hashtable< Integer, Set<HeapRegionNode> >();
+
+
     Iterator itrHrns = id2hrn.entrySet().iterator();
     while( itrHrns.hasNext() ) {
       Map.Entry      me    = (Map.Entry)      itrHrns.next();
@@ -1783,64 +2871,131 @@ public class ReachGraph {
        assert rsetEmpty.equals( edge.getBetaNew() );
       }      
 
-      // calculate boldB for this flagged node
+      // calculate boldB for this flagged node, or out-of-context node
       if( hrn.isFlagged() ) {
-       
-       Hashtable<RefEdge, ReachSet> boldB_f =
-         new Hashtable<RefEdge, ReachSet>();
-       
-       Set<RefEdge> workSetEdges = new HashSet<RefEdge>();
+        assert !hrn.isOutOfContext();
+        assert !icID2srcs.containsKey( hrn.getID() );
+        Set<HeapRegionNode> srcs = new HashSet<HeapRegionNode>();
+        srcs.add( hrn );
+        icID2srcs.put( hrn.getID(), srcs );
+      }
 
-       // initial boldB_f constraints
-       Iterator<RefEdge> itrRees = hrn.iteratorToReferencees();
-       while( itrRees.hasNext() ) {
-         RefEdge edge = itrRees.next();
+      if( hrn.isOutOfContext() ) {
+       assert !hrn.isFlagged();
 
-         assert !boldB.containsKey( edge );
-         boldB_f.put( edge, edge.getBeta() );
+        Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
 
-         assert !workSetEdges.contains( edge );
-         workSetEdges.add( edge );
-       }       
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+            assert rt.isOutOfContext();
 
-       // enforce the boldB_f constraint at edges until we reach a fixed point
-       while( !workSetEdges.isEmpty() ) {
-         RefEdge edge = workSetEdges.iterator().next();
-         workSetEdges.remove( edge );   
-         
-         Iterator<RefEdge> itrPrime = edge.getDst().iteratorToReferencees();
-         while( itrPrime.hasNext() ) {
-           RefEdge edgePrime = itrPrime.next();            
+            Set<HeapRegionNode> srcs = oocID2srcs.get( rt.getHrnID() );
+            if( srcs == null ) {
+              srcs = new HashSet<HeapRegionNode>();
+            }
+            srcs.add( hrn );
+            oocID2srcs.put( rt.getHrnID(), srcs );
+          }
+        }
+      }
+    }
+
+    // calculate boldB for all hrnIDs identified by the above
+    // node traversal, propagating from every source
+    while( !icID2srcs.isEmpty() || !oocID2srcs.isEmpty() ) {
+
+      Integer             hrnID;
+      Set<HeapRegionNode> srcs;
+      boolean             inContext;
+
+      if( !icID2srcs.isEmpty() ) {
+        Map.Entry me = (Map.Entry) icID2srcs.entrySet().iterator().next();
+        hrnID = (Integer)             me.getKey();
+        srcs  = (Set<HeapRegionNode>) me.getValue();
+        inContext = true;
+        icID2srcs.remove( hrnID );
+
+      } else {
+        assert !oocID2srcs.isEmpty();
+
+        Map.Entry me = (Map.Entry) oocID2srcs.entrySet().iterator().next();
+        hrnID = (Integer)             me.getKey();
+        srcs  = (Set<HeapRegionNode>) me.getValue();
+        inContext = false;
+        oocID2srcs.remove( hrnID );
+      }
+
+
+      Hashtable<RefEdge, ReachSet> boldB_f =
+        new Hashtable<RefEdge, ReachSet>();
+       
+      Set<RefEdge> workSetEdges = new HashSet<RefEdge>();
+
+      Iterator<HeapRegionNode> hrnItr = srcs.iterator();
+      while( hrnItr.hasNext() ) {
+        HeapRegionNode hrn = hrnItr.next();
 
-           ReachSet prevResult   = boldB_f.get( edgePrime );
-           ReachSet intersection = Canonical.intersection( boldB_f.get( edge ),
+        assert workSetEdges.isEmpty();
+        
+        // initial boldB_f constraints
+        Iterator<RefEdge> itrRees = hrn.iteratorToReferencees();
+        while( itrRees.hasNext() ) {
+          RefEdge edge = itrRees.next();
+          
+          assert !boldB_f.containsKey( edge );
+          boldB_f.put( edge, edge.getBeta() );
+          
+          assert !workSetEdges.contains( edge );
+          workSetEdges.add( edge );
+        }              
+      
+        // enforce the boldB_f constraint at edges until we reach a fixed point
+        while( !workSetEdges.isEmpty() ) {
+          RefEdge edge = workSetEdges.iterator().next();
+          workSetEdges.remove( edge );  
+          
+          Iterator<RefEdge> itrPrime = edge.getDst().iteratorToReferencees();
+          while( itrPrime.hasNext() ) {
+            RefEdge edgePrime = itrPrime.next();           
+          
+            ReachSet prevResult   = boldB_f.get( edgePrime );
+            ReachSet intersection = Canonical.intersection( boldB_f.get( edge ),
                                                             edgePrime.getBeta()
                                                             );
-                   
-           if( prevResult == null || 
-               Canonical.union( prevResult,
-                                 intersection ).size() > prevResult.size() ) {
-             
-             if( prevResult == null ) {
-               boldB_f.put( edgePrime, 
-                             Canonical.union( edgePrime.getBeta(),
-                                              intersection 
-                                              )
+          
+            if( prevResult == null || 
+                Canonical.unionORpreds( prevResult,
+                                        intersection ).size() 
+                > prevResult.size() 
+                ) {
+            
+              if( prevResult == null ) {
+                boldB_f.put( edgePrime, 
+                             Canonical.unionORpreds( edgePrime.getBeta(),
+                                                     intersection 
+                                                     )
                              );
-             } else {
-               boldB_f.put( edgePrime, 
-                             Canonical.union( prevResult,
-                                              intersection 
-                                              )
+              } else {
+                boldB_f.put( edgePrime, 
+                             Canonical.unionORpreds( prevResult,
+                                                     intersection 
+                                                     )
                              );
-             }
-             workSetEdges.add( edgePrime );    
-           }
-         }
-       }
-       
-               boldB.put( hrnID, boldB_f );
-      }      
+              }
+              workSetEdges.add( edgePrime );   
+            }
+          }
+        }
+      }
+      
+      if( inContext ) {
+        boldBic.put( hrnID, boldB_f );
+      } else {
+        boldBooc.put( hrnID, boldB_f );
+      }
     }
 
 
@@ -1858,13 +3013,20 @@ public class ReachGraph {
       Integer        hrnID = (Integer)        me.getKey();
       HeapRegionNode hrn   = (HeapRegionNode) me.getValue();
       
-      // create the inherent hrnID from a flagged region
-      // as an exception to removal below
-      ReachTuple rtException = 
-        ReachTuple.factory( hrnID, 
-                            !hrn.isSingleObject(), 
-                            ReachTuple.ARITY_ONE 
-                            );
+      // out-of-context nodes don't participate in the 
+      // global sweep, they serve as sources for the pass
+      // performed above
+      if( hrn.isOutOfContext() ) {
+        continue;
+      }
+
+      // the inherent states of a region are the exception
+      // to removal as the global sweep prunes
+      ReachTuple rtException = ReachTuple.factory( hrnID,
+                                                   !hrn.isSingleObject(),    
+                                                   ReachTuple.ARITY_ONE,
+                                                   false // out-of-context
+                                                   );
 
       ChangeSet cts = ChangeSet.factory();
 
@@ -1887,23 +3049,30 @@ public class ReachGraph {
            }
          }
 
-         // does boldB_ttOld allow this hrnID?
+         // does boldB allow this hrnID?
          boolean foundState = false;
          Iterator<RefEdge> incidentEdgeItr = hrn.iteratorToReferencers();
          while( incidentEdgeItr.hasNext() ) {
            RefEdge incidentEdge = incidentEdgeItr.next();
 
-           // if it isn't allowed, mark for removal
-           Integer idOld = rtOld.getHrnID();
-           assert id2hrn.containsKey( idOld );
-           Hashtable<RefEdge, ReachSet> B = boldB.get( idOld );            
-           ReachSet boldB_ttOld_incident = B.get( incidentEdge );
-           if( boldB_ttOld_incident != null &&
-               boldB_ttOld_incident.contains( stateOld ) ) {
-             foundState = true;
-           }
+            Hashtable<RefEdge, ReachSet> B; 
+            if( rtOld.isOutOfContext() ) {
+              B = boldBooc.get( rtOld.getHrnID() ); 
+            } else {
+              assert id2hrn.containsKey( rtOld.getHrnID() );
+              B = boldBic.get( rtOld.getHrnID() ); 
+            }
+
+            if( B != null ) {            
+              ReachSet boldB_rtOld_incident = B.get( incidentEdge );
+              if( boldB_rtOld_incident != null &&
+                  boldB_rtOld_incident.containsIgnorePreds( stateOld ) != null
+                  ) {
+                foundState = true;
+              }
+            }
          }
-
+          
          if( !foundState ) {
            markedHrnIDs = Canonical.add( markedHrnIDs, rtOld );          
          }
@@ -1911,9 +3080,9 @@ public class ReachGraph {
 
        // if there is nothing marked, just move on
        if( markedHrnIDs.isEmpty() ) {
-         hrn.setAlphaNew( Canonical.union( hrn.getAlphaNew(),
-                                            stateOld
-                                            )
+         hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(),
+                                          stateOld
+                                          )
                            );
          continue;
        }
@@ -1926,19 +3095,19 @@ public class ReachGraph {
          ReachTuple rtOld = rtItr.next();
 
          if( !markedHrnIDs.containsTuple( rtOld ) ) {
-           statePruned = Canonical.union( statePruned, rtOld );
+           statePruned = Canonical.add( statePruned, rtOld );
          }
        }
        assert !stateOld.equals( statePruned );
 
-       hrn.setAlphaNew( Canonical.union( hrn.getAlphaNew(),
-                                          statePruned
-                                          )
+       hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(),
+                                        statePruned
+                                        )
                          );
        ChangeTuple ct = ChangeTuple.factory( stateOld,
                                               statePruned
                                               );
-       cts = Canonical.union( cts, ct );
+       cts = Canonical.add( cts, ct );
       }
 
       // throw change tuple set on all incident edges
@@ -1981,7 +3150,16 @@ public class ReachGraph {
     Iterator<HeapRegionNode> nodeItr = id2hrn.values().iterator();
     while( nodeItr.hasNext() ) {
       HeapRegionNode hrn = nodeItr.next();
-      hrn.applyAlphaNew();
+
+      // as mentioned above, out-of-context nodes only serve
+      // as sources of reach states for the sweep, not part
+      // of the changes
+      if( hrn.isOutOfContext() ) {
+        assert hrn.getAlphaNew().equals( rsetEmpty );
+      } else {
+        hrn.applyAlphaNew();
+      }
+
       Iterator<RefEdge> itrRes = hrn.iteratorToReferencers();
       while( itrRes.hasNext() ) {
        res.add( itrRes.next() );
@@ -2031,13 +3209,16 @@ public class ReachGraph {
                                   edgePrime.getBetaNew() 
                                   );
                    
-       if( Canonical.union( prevResult,
-                             intersection
-                             ).size() > prevResult.size() ) {
+       if( Canonical.unionORpreds( prevResult,
+                                    intersection
+                                    ).size() 
+            > prevResult.size() 
+            ) {
+          
          edge.setBetaNew( 
-                          Canonical.union( prevResult,
-                                           intersection 
-                                           )
+                          Canonical.unionORpreds( prevResult,
+                                                  intersection 
+                                                  )
                            );
          edgeWorkSet.add( edge );
        }       
@@ -2110,18 +3291,15 @@ public class ReachGraph {
        // so make the new reachability set a union of the
        // nodes' reachability sets
        HeapRegionNode hrnB = id2hrn.get( idA );
-       hrnB.setAlpha( Canonical.union( hrnB.getAlpha(),
+       hrnB.setAlpha( Canonical.unionORpreds( hrnB.getAlpha(),
                                         hrnA.getAlpha() 
                                         )
                        );
 
-        // if hrnB is already dirty or hrnA is dirty,
-        // the hrnB should end up dirty: TODO
-        /*
-        if( !hrnA.isClean() ) {
-          hrnB.setIsClean( false );
-        }
-        */
+        hrnB.setPreds( Canonical.join( hrnB.getPreds(),
+                                       hrnA.getPreds()
+                                       )
+                       );
       }
     }
 
@@ -2195,16 +3373,15 @@ public class ReachGraph {
          // just replace this beta set with the union
          assert edgeToMerge != null;
          edgeToMerge.setBeta(
-                              Canonical.union( edgeToMerge.getBeta(),
+                              Canonical.unionORpreds( edgeToMerge.getBeta(),
                                                edgeA.getBeta() 
                                                )
                               );
-          // TODO: what?
-          /*
-         if( !edgeA.isClean() ) {
-           edgeToMerge.setIsClean( false );
-         }
-          */
+          edgeToMerge.setPreds(
+                               Canonical.join( edgeToMerge.getPreds(),
+                                               edgeA.getPreds()
+                                               )
+                               );
        }
       }
     }
@@ -2260,16 +3437,14 @@ public class ReachGraph {
        // so merge their reachability sets
        else {
          // just replace this beta set with the union
-         edgeToMerge.setBeta( Canonical.union( edgeToMerge.getBeta(),
+         edgeToMerge.setBeta( Canonical.unionORpreds( edgeToMerge.getBeta(),
                                                 edgeA.getBeta()
                                                 )
                                );
-          // TODO: what?
-          /*
-         if( !edgeA.isClean() ) {
-           edgeToMerge.setIsClean( false );
-         }
-          */
+          edgeToMerge.setPreds( Canonical.join( edgeToMerge.getPreds(),
+                                                edgeA.getPreds()
+                                                )
+                                );
        }
       }
     }
@@ -2624,7 +3799,6 @@ public class ReachGraph {
                           boolean writeLabels,
                           boolean labelSelect,
                           boolean pruneGarbage,
-                          boolean writeReferencers,
                           boolean hideSubsetReachability,
                           boolean hideEdgeTaints
                           ) throws java.io.IOException {
@@ -2632,22 +3806,18 @@ public class ReachGraph {
                 writeLabels,
                 labelSelect,
                 pruneGarbage,
-                writeReferencers,
                 hideSubsetReachability,
                 hideEdgeTaints,
-                null,
                 null );
   }
 
-  public void writeGraph( String              graphName,
-                          boolean             writeLabels,
-                          boolean             labelSelect,
-                          boolean             pruneGarbage,
-                          boolean             writeReferencers,
-                          boolean             hideSubsetReachability,
-                          boolean             hideEdgeTaints,
-                          Set<HeapRegionNode> callerNodesCopiedToCallee,
-                          Set<RefEdge>        callerEdgesCopiedToCallee
+  public void writeGraph( String       graphName,
+                          boolean      writeLabels,
+                          boolean      labelSelect,
+                          boolean      pruneGarbage,
+                          boolean      hideSubsetReachability,
+                          boolean      hideEdgeTaints,
+                          Set<Integer> callerNodeIDsCopiedToCallee
                           ) throws java.io.IOException {
     
     // remove all non-word characters from the graph name so
@@ -2662,7 +3832,7 @@ public class ReachGraph {
 
     // this is an optional step to form the callee-reachable
     // "cut-out" into a DOT cluster for visualization
-    if( callerNodesCopiedToCallee != null ) {
+    if( callerNodeIDsCopiedToCallee != null ) {
 
       bw.write( "  subgraph cluster0 {\n" );
       bw.write( "    color=blue;\n" );
@@ -2672,7 +3842,7 @@ public class ReachGraph {
         Map.Entry      me  = (Map.Entry)      i.next();
         HeapRegionNode hrn = (HeapRegionNode) me.getValue();      
         
-        if( callerNodesCopiedToCallee.contains( hrn ) ) {
+        if( callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) {
           bw.write( "    "+hrn.toString()+
                     hrn.toStringDOT( hideSubsetReachability )+
                     ";\n" );
@@ -2695,9 +3865,7 @@ public class ReachGraph {
       // only visit nodes worth writing out--for instance
       // not every node at an allocation is referenced
       // (think of it as garbage-collected), etc.
-      if( !pruneGarbage                              ||
-          (hrn.isFlagged() && hrn.getID() > 0)       ||
-          hrn.getDescription().startsWith( "param" ) ||
+      if( !pruneGarbage        ||
           hrn.isOutOfContext()
           ) {
 
@@ -2706,11 +3874,9 @@ public class ReachGraph {
                                    bw,
                                    null,
                                    visited,
-                                   writeReferencers,
                                    hideSubsetReachability,
                                    hideEdgeTaints,
-                                   callerNodesCopiedToCallee,
-                                   callerEdgesCopiedToCallee );
+                                   callerNodeIDsCopiedToCallee );
        }
       }
     }
@@ -2727,10 +3893,10 @@ public class ReachGraph {
         
         if( labelSelect ) {
           String labelStr = vn.getTempDescriptorString();
-          if( labelStr.startsWith("___temp") ||
-              labelStr.startsWith("___dst") ||
-              labelStr.startsWith("___srctmp") ||
-              labelStr.startsWith("___neverused")
+          if( labelStr.startsWith( "___temp" )     ||
+              labelStr.startsWith( "___dst" )      ||
+              labelStr.startsWith( "___srctmp" )   ||
+              labelStr.startsWith( "___neverused" )
               ) {
             continue;
           }
@@ -2741,16 +3907,14 @@ public class ReachGraph {
           RefEdge        edge = heapRegionsItr.next();
           HeapRegionNode hrn  = edge.getDst();
           
-          if( pruneGarbage && !visited.contains( hrn ) ) {
+          if( !visited.contains( hrn ) ) {
             traverseHeapRegionNodes( hrn,
                                      bw,
                                      null,
                                      visited,
-                                     writeReferencers,
                                      hideSubsetReachability,
                                      hideEdgeTaints,
-                                     callerNodesCopiedToCallee,
-                                     callerEdgesCopiedToCallee );
+                                     callerNodeIDsCopiedToCallee );
           }
           
           bw.write( "  "+vn.toString()+
@@ -2769,11 +3933,9 @@ public class ReachGraph {
                                           BufferedWriter      bw,
                                           TempDescriptor      td,
                                           Set<HeapRegionNode> visited,
-                                          boolean             writeReferencers,
                                           boolean             hideSubsetReachability,
                                           boolean             hideEdgeTaints,
-                                          Set<HeapRegionNode> callerNodesCopiedToCallee,
-                                          Set<RefEdge>        callerEdgesCopiedToCallee
+                                          Set<Integer>        callerNodeIDsCopiedToCallee
                                           ) throws java.io.IOException {
 
     if( visited.contains( hrn ) ) {
@@ -2784,8 +3946,8 @@ public class ReachGraph {
     // if we're drawing the callee-view subgraph, only
     // write out the node info if it hasn't already been
     // written
-    if( callerNodesCopiedToCallee == null ||
-        !callerNodesCopiedToCallee.contains( hrn ) 
+    if( callerNodeIDsCopiedToCallee == null ||
+        !callerNodeIDsCopiedToCallee.contains( hrn.getID() ) 
         ) {
       bw.write( "  "+hrn.toString()+
                 hrn.toStringDOT( hideSubsetReachability )+
@@ -2797,13 +3959,29 @@ public class ReachGraph {
       RefEdge        edge     = childRegionsItr.next();
       HeapRegionNode hrnChild = edge.getDst();
 
-      if( callerEdgesCopiedToCallee != null &&
-          callerEdgesCopiedToCallee.contains( hrn ) 
-          ) {
-        bw.write( "  "+hrn.toString()+
-                  " -> "+hrnChild.toString()+
-                  edge.toStringDOT( hideSubsetReachability, ",color=blue" )+
-                  ";\n");
+      if( callerNodeIDsCopiedToCallee != null &&
+          (edge.getSrc() instanceof HeapRegionNode) ) {
+        HeapRegionNode hrnSrc = (HeapRegionNode) edge.getSrc();
+        if( callerNodeIDsCopiedToCallee.contains( hrnSrc.getID()        ) &&
+            callerNodeIDsCopiedToCallee.contains( edge.getDst().getID() )
+            ) {
+          bw.write( "  "+hrn.toString()+
+                    " -> "+hrnChild.toString()+
+                    edge.toStringDOT( hideSubsetReachability, ",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" )+
+                    ";\n");
+        } else {
+          bw.write( "  "+hrn.toString()+
+                    " -> "+hrnChild.toString()+
+                    edge.toStringDOT( hideSubsetReachability, "" )+
+                    ";\n");
+        }
       } else {
         bw.write( "  "+hrn.toString()+
                   " -> "+hrnChild.toString()+
@@ -2815,12 +3993,298 @@ public class ReachGraph {
                                bw,
                                td,
                                visited,
-                               writeReferencers,
                                hideSubsetReachability,
                                hideEdgeTaints,
-                               callerNodesCopiedToCallee,
-                               callerEdgesCopiedToCallee );
+                               callerNodeIDsCopiedToCallee );
     }
   }  
+  
+       public Set<HeapRegionNode> findCommonReachableNodes(HeapRegionNode hrn1,
+                       HeapRegionNode hrn2) {
 
+               Set<HeapRegionNode> reachableNodes1 = new HashSet<HeapRegionNode>();
+               Set<HeapRegionNode> reachableNodes2 = new HashSet<HeapRegionNode>();
+
+               Set<HeapRegionNode> todoNodes1 = new HashSet<HeapRegionNode>();
+               todoNodes1.add(hrn1);
+
+               Set<HeapRegionNode> todoNodes2 = new HashSet<HeapRegionNode>();
+               todoNodes2.add(hrn2);
+
+               // follow links until all reachable nodes have been found
+               while (!todoNodes1.isEmpty()) {
+                       HeapRegionNode hrn = todoNodes1.iterator().next();
+                       todoNodes1.remove(hrn);
+                       reachableNodes1.add(hrn);
+
+                       Iterator<RefEdge> edgeItr = hrn.iteratorToReferencees();
+                       while (edgeItr.hasNext()) {
+                               RefEdge edge = edgeItr.next();
+
+                               if (!reachableNodes1.contains(edge.getDst())) {
+                                       todoNodes1.add(edge.getDst());
+                               }
+                       }
+               }
+
+               while (!todoNodes2.isEmpty()) {
+                       HeapRegionNode hrn = todoNodes2.iterator().next();
+                       todoNodes2.remove(hrn);
+                       reachableNodes2.add(hrn);
+
+                       Iterator<RefEdge> edgeItr = hrn.iteratorToReferencees();
+                       while (edgeItr.hasNext()) {
+                               RefEdge edge = edgeItr.next();
+
+                               if (!reachableNodes2.contains(edge.getDst())) {
+                                       todoNodes2.add(edge.getDst());
+                               }
+                       }
+               }
+
+               Set<HeapRegionNode> intersection =
+                  new HashSet<HeapRegionNode>( reachableNodes1 );
+
+               intersection.retainAll( reachableNodes2 );
+
+               return intersection;
+       }
+        
+       public Set<HeapRegionNode> mayReachSharedObjects(HeapRegionNode hrn1,
+                       HeapRegionNode hrn2) {
+               assert hrn1 != null;
+               assert hrn2 != null;
+
+               // then get the various tokens for these heap regions
+               ReachTuple h1 = ReachTuple.factory(hrn1.getID(),
+                               !hrn1.isSingleObject(), ReachTuple.ARITY_ONE, false);
+
+               int arity;
+               if(hrn1.isSingleObject){
+                       arity=ReachTuple.ARITY_ONE;
+               }else{
+                       arity=ReachTuple.ARITY_ZEROORMORE;
+               }
+               ReachTuple h1star = ReachTuple.factory(hrn1.getID(), !hrn1
+                               .isSingleObject(), arity, false);
+
+               ReachTuple h2 = ReachTuple.factory(hrn2.getID(),
+                               !hrn2.isSingleObject(), ReachTuple.ARITY_ONE, false);
+
+               if(hrn2.isSingleObject){
+                       arity=ReachTuple.ARITY_ONE;
+               }else{
+                       arity=ReachTuple.ARITY_ZEROORMORE;
+               }
+               
+               ReachTuple h2star = ReachTuple.factory(hrn2.getID(), !hrn2
+                               .isSingleObject(), arity, false);
+
+               // then get the merged beta of all out-going edges from these heap
+               // regions
+
+               ReachSet beta1 = ReachSet.factory();
+               Iterator<RefEdge> itrEdge = hrn1.iteratorToReferencees();
+               while (itrEdge.hasNext()) {
+                       RefEdge edge = itrEdge.next();
+                       beta1 = Canonical.unionORpreds(beta1, edge.getBeta());
+               }
+
+               ReachSet beta2 = ReachSet.factory();
+               itrEdge = hrn2.iteratorToReferencees();
+               while (itrEdge.hasNext()) {
+                       RefEdge edge = itrEdge.next();
+                       beta2 = Canonical.unionORpreds(beta2, edge.getBeta());
+               }
+
+               boolean aliasDetected = false;
+
+               // only do this one if they are different tokens
+               if (h1 != h2 && beta1.containsStateWithBoth(h1, h2)) {
+                       aliasDetected = true;
+               }
+//             if (beta1.containsStateWithBoth(h1plus, h2)) {
+//                     aliasDetected = true;
+//             }
+               if (beta1.containsStateWithBoth(h1star, h2)) {
+                       aliasDetected = true;
+               }
+//             if (beta1.containsStateWithBoth(h1, h2plus)) {
+//                     aliasDetected = true;
+//             }
+//             if (beta1.containsStateWithBoth(h1plus, h2plus)) {
+//                     aliasDetected = true;
+//             }
+//             if (beta1.containsStateWithBoth(h1star, h2plus)) {
+//                     aliasDetected = true;
+//             }
+               if (beta1.containsStateWithBoth(h1, h2star)) {
+                       aliasDetected = true;
+               }
+//             if (beta1.containsStateWithBoth(h1plus, h2star)) {
+//                     aliasDetected = true;
+//             }
+               if (beta1.containsStateWithBoth(h1star, h2star)) {
+                       aliasDetected = true;
+               }
+
+               if (h1 != h2 && beta2.containsStateWithBoth(h1, h2)) {
+                       aliasDetected = true;
+               }
+//             if (beta2.containsStateWithBoth(h1plus, h2)) {
+//                     aliasDetected = true;
+//             }
+               if (beta2.containsStateWithBoth(h1star, h2)) {
+                       aliasDetected = true;
+               }
+//             if (beta2.containsStateWithBoth(h1, h2plus)) {
+//                     aliasDetected = true;
+//             }
+//             if (beta2.containsStateWithBoth(h1plus, h2plus)) {
+//                     aliasDetected = true;
+//             }
+//             if (beta2.containsStateWithBoth(h1star, h2plus)) {
+//                     aliasDetected = true;
+//             }
+               if (beta2.containsStateWithBoth(h1, h2star)) {
+                       aliasDetected = true;
+               }
+//             if (beta2.containsStateWithBoth(h1plus, h2star)) {
+//                     aliasDetected = true;
+//             }
+               if (beta2.containsStateWithBoth(h1star, h2star)) {
+                       aliasDetected = true;
+               }
+
+               Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
+               if (aliasDetected) {
+                       common = findCommonReachableNodes(hrn1, hrn2);
+                       if (!(DISABLE_STRONG_UPDATES || DISABLE_GLOBAL_SWEEP)) {
+                               assert !common.isEmpty();
+                       }
+               }
+
+               return common;
+       }
+
+       public Set<HeapRegionNode> mayReachSharedObjects(FlatMethod fm,
+                       Integer paramIndex1, Integer paramIndex2) {
+
+               // get parameter's heap regions
+               TempDescriptor paramTemp1 = fm.getParameter(paramIndex1.intValue());
+               VariableNode argVar1 = getVariableNodeFromTemp(paramTemp1);
+               RefEdge argEdge1 = argVar1.iteratorToReferencees().next();
+               HeapRegionNode hrnParam1 = argEdge1.getDst();
+
+               TempDescriptor paramTemp2 = fm.getParameter(paramIndex2.intValue());
+               VariableNode argVar2 = getVariableNodeFromTemp(paramTemp2);
+               RefEdge argEdge2 = argVar2.iteratorToReferencees().next();
+               HeapRegionNode hrnParam2 = argEdge2.getDst();
+
+               Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
+               common.addAll(mayReachSharedObjects(hrnParam1, hrnParam2));
+
+               return common;
+       }
+
+       public Set<HeapRegionNode> mayReachSharedObjects(FlatMethod fm,
+                       Integer paramIndex, AllocSite as) {
+
+               // get parameter's heap regions
+               TempDescriptor paramTemp = fm.getParameter(paramIndex.intValue());
+               VariableNode argVar = getVariableNodeFromTemp(paramTemp);
+               RefEdge argEdge = argVar.iteratorToReferencees().next();
+               HeapRegionNode hrnParam = argEdge.getDst();
+
+               // get summary node
+               HeapRegionNode hrnSummary=null;
+               if(id2hrn.containsKey(as.getSummary())){
+                       // if summary node doesn't exist, ignore this case
+                       hrnSummary = id2hrn.get(as.getSummary());
+                       assert hrnSummary != null;
+               }
+
+               Set<HeapRegionNode> common  = new HashSet<HeapRegionNode>();
+               if(hrnSummary!=null){
+                       common.addAll( mayReachSharedObjects(hrnParam, hrnSummary) );
+               }
+
+               // check for other nodes
+               for (int i = 0; i < as.getAllocationDepth(); ++i) {
+
+                       assert id2hrn.containsKey(as.getIthOldest(i));
+                       HeapRegionNode hrnIthOldest = id2hrn.get(as.getIthOldest(i));
+                       assert hrnIthOldest != null;
+
+                       common.addAll(mayReachSharedObjects(hrnParam, hrnIthOldest));
+
+               }
+
+               return common;
+       }
+
+       public Set<HeapRegionNode> mayReachSharedObjects(AllocSite as1,
+                       AllocSite as2) {
+
+               // get summary node 1's alpha
+               Integer idSum1 = as1.getSummary();
+               HeapRegionNode hrnSum1=null;
+               if(id2hrn.containsKey(idSum1)){
+                       hrnSum1 = id2hrn.get(idSum1);
+               }
+
+               // get summary node 2's alpha
+               Integer idSum2 = as2.getSummary();
+               HeapRegionNode hrnSum2=null;
+               if(id2hrn.containsKey(idSum2)){
+                       hrnSum2 = id2hrn.get(idSum2);
+               }
+               
+               Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
+               if(hrnSum1!=null && hrnSum2!=null){
+                       common.addAll(mayReachSharedObjects(hrnSum1, hrnSum2));
+               }
+
+               // check sum2 against alloc1 nodes
+               if(hrnSum2!=null){
+               for (int i = 0; i < as1.getAllocationDepth(); ++i) {
+                       Integer idI1 = as1.getIthOldest(i);
+                       assert id2hrn.containsKey(idI1);
+                       HeapRegionNode hrnI1 = id2hrn.get(idI1);
+                       assert hrnI1 != null;
+                       common.addAll(mayReachSharedObjects(hrnI1, hrnSum2));
+               }
+               }
+
+               // check sum1 against alloc2 nodes
+               for (int i = 0; i < as2.getAllocationDepth(); ++i) {
+                       Integer idI2 = as2.getIthOldest(i);
+                       assert id2hrn.containsKey(idI2);
+                       HeapRegionNode hrnI2 = id2hrn.get(idI2);
+                       assert hrnI2 != null;
+
+                       if(hrnSum1!=null){
+                               common.addAll(mayReachSharedObjects(hrnSum1, hrnI2));
+                       }
+
+                       // while we're at it, do an inner loop for alloc2 vs alloc1 nodes
+                       for (int j = 0; j < as1.getAllocationDepth(); ++j) {
+                               Integer idI1 = as1.getIthOldest(j);
+
+                               // if these are the same site, don't look for the same token, no
+                               // alias.
+                               // different tokens of the same site could alias together though
+                               if (idI1.equals(idI2)) {
+                                       continue;
+                               }
+
+                               HeapRegionNode hrnI1 = id2hrn.get(idI1);
+
+                               common.addAll(mayReachSharedObjects(hrnI1, hrnI2));
+                       }
+               }
+
+               return common;
+       }
+  
 }