turn strong updates back on from yesterday testing, add a non-terminating example...
[IRC.git] / Robust / src / Analysis / Disjoint / ReachGraph.java
index ff811bc41268ea246d8d182230f690e10aa171b6..d61a76c7a44afeac3003c9b6a8a6f8bb2f6ef473 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___" );
@@ -18,7 +18,7 @@ public class ReachGraph {
   // some frequently used reachability constants
   protected static final ReachState rstateEmpty        = ReachState.factory();
   protected static final ReachSet   rsetEmpty          = ReachSet.factory();
-  protected static final ReachSet   rsetWithEmptyState = ReachSet.factory( rstateEmpty );
+  protected static final ReachSet   rsetWithEmptyState = Canonical.makePredsTrue(ReachSet.factory( rstateEmpty ));
 
   // predicate constants
   protected static final ExistPred    predTrue   = ExistPred.factory(); // if no args, true
@@ -79,6 +79,8 @@ public class ReachGraph {
     return this.id2hrn.get( hrn.getID() ) == hrn;
   }
 
+  
+
 
 
   // the reason for this method is to have the option
@@ -121,15 +123,17 @@ public class ReachGraph {
     if( inherent == null ) {
       if( markForAnalysis ) {
        inherent = 
-          ReachSet.factory(
-                           ReachState.factory(
-                                              ReachTuple.factory( id,
-                                                                  !isSingleObject,
-                                                                  ReachTuple.ARITY_ONE,
-                                                                  false // out-of-context
-                                                                  )
-                                              )
-                           );
+          Canonical.makePredsTrue(
+                                  ReachSet.factory(
+                                                   ReachState.factory(
+                                                                      ReachTuple.factory( id,
+                                                                                          !isSingleObject,
+                                                                                          ReachTuple.ARITY_ONE,
+                                                                                          false // out-of-context
+                                                                                          )
+                                                                      )
+                                                   )
+                                  );
       } else {
        inherent = rsetWithEmptyState;
       }
@@ -139,11 +143,8 @@ 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,
                                             markForAnalysis,
@@ -293,6 +294,42 @@ public class ReachGraph {
     }
   }
 
+  // this is a common operation in many transfer functions: we want
+  // to add an edge, but if there is already such an edge we should
+  // merge the properties of the existing and the new edges
+  protected void addEdgeOrMergeWithExisting( RefEdge edgeNew ) {
+
+    RefSrcNode src = edgeNew.getSrc();
+    assert belongsToThis( src );
+
+    HeapRegionNode dst = edgeNew.getDst();
+    assert belongsToThis( dst );
+
+    // look to see if an edge with same field exists
+    // and merge with it, otherwise just add the edge
+    RefEdge edgeExisting = src.getReferenceTo( dst, 
+                                               edgeNew.getType(),
+                                               edgeNew.getField() 
+                                               );
+       
+    if( edgeExisting != null ) {
+      edgeExisting.setBeta(
+                           Canonical.unionORpreds( edgeExisting.getBeta(),
+                                                   edgeNew.getBeta()
+                                                   )
+                           );
+      edgeExisting.setPreds(
+                            Canonical.join( edgeExisting.getPreds(),
+                                            edgeNew.getPreds()
+                                            )
+                            );
+       
+    } else {                     
+      addRefEdge( src, dst, edgeNew );
+    }
+  }
+
+
 
   ////////////////////////////////////////////////////
   //
@@ -415,8 +452,8 @@ public class ReachGraph {
                                        Canonical.intersection( betaY, betaHrn ),
                                        predsTrue
                                        );
-       
-       addRefEdge( lnX, hrnHrn, edgeNew );
+
+        addEdgeOrMergeWithExisting( edgeNew );
       }
     }
 
@@ -557,37 +594,20 @@ public class ReachGraph {
                            hrnY.getType()
                            );  
 
-       RefEdge edgeNew = new RefEdge( hrnX,
-                                       hrnY,
-                                       tdNewEdge,
-                                       f.getSymbol(),
-                                       Canonical.pruneBy( edgeY.getBeta(),
-                                                          hrnX.getAlpha() 
-                                                          ),
-                                       predsTrue
-                                       );
+       RefEdge edgeNew = 
+          new RefEdge( hrnX,
+                       hrnY,
+                       tdNewEdge,
+                       f.getSymbol(),
+                       Canonical.makePredsTrue(
+                                               Canonical.pruneBy( edgeY.getBeta(),
+                                                                  hrnX.getAlpha() 
+                                                                  )
+                                               ),
+                       predsTrue
+                       );
 
-       // look to see if an edge with same field exists
-       // and merge with it, otherwise just add the edge
-       RefEdge edgeExisting = hrnX.getReferenceTo( hrnY, 
-                                                    tdNewEdge,
-                                                    f.getSymbol() );
-       
-       if( edgeExisting != null ) {
-         edgeExisting.setBeta(
-                               Canonical.union( edgeExisting.getBeta(),
-                                                edgeNew.getBeta()
-                                                )
-                               );
-          edgeExisting.setPreds(
-                                Canonical.join( edgeExisting.getPreds(),
-                                                edgeNew.getPreds()
-                                                )
-                                );
-       
-        } else {                         
-         addRefEdge( hrnX, hrnY, edgeNew );
-       }
+        addEdgeOrMergeWithExisting( edgeNew );
       }
     }
 
@@ -779,9 +799,6 @@ public class ReachGraph {
       }
 
       String strDesc = as.toStringForDOT()+"\\nsummary";
-      if( shadow ) {
-        strDesc += " shadow";
-      }
 
       hrnSummary = 
         createNewHeapRegionNode( idSummary,    // id or null to generate a new one 
@@ -827,9 +844,6 @@ 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?                  
@@ -881,7 +895,7 @@ public class ReachGraph {
        // otherwise an edge from the referencer to hrnSummary exists already
        // and the edge referencer->hrn should be merged with it
        edgeSummary.setBeta( 
-                            Canonical.union( edgeMerged.getBeta(),
+                            Canonical.unionORpreds( edgeMerged.getBeta(),
                                              edgeSummary.getBeta() 
                                              ) 
                              );
@@ -915,7 +929,7 @@ public class ReachGraph {
        // otherwise an edge from the referencer to alpha_S exists already
        // and the edge referencer->alpha_K should be merged with it
        edgeSummary.setBeta( 
-                            Canonical.union( edgeMerged.getBeta(),
+                            Canonical.unionORpreds( edgeMerged.getBeta(),
                                              edgeSummary.getBeta() 
                                              ) 
                              );
@@ -929,7 +943,7 @@ public class ReachGraph {
 
     // then merge hrn reachability into hrnSummary
     hrnSummary.setAlpha( 
-                        Canonical.union( hrnSummary.getAlpha(),
+                        Canonical.unionORpreds( hrnSummary.getAlpha(),
                                          hrn.getAlpha() 
                                          )
                          );
@@ -1080,8 +1094,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 );
          }
        }
 
@@ -1123,7 +1139,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 
                                       )
                      );
@@ -1160,8 +1176,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 );
        }
       }
 
@@ -1212,7 +1230,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  
                                      )
                     );
@@ -1280,12 +1298,156 @@ public class ReachGraph {
 
   // used below to convert a ReachSet to its callee-context
   // equivalent with respect to allocation sites in this graph
-  protected ReachSet toCalleeContext( ReachSet rs ) {
+  protected ReachSet toCalleeContext( ReachSet      rs,
+                                      ExistPredSet  preds,
+                                      Set<HrnIdOoc> oocHrnIdOoc2callee
+                                      ) {
+    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
+          HrnIdOoc hio = new HrnIdOoc( rt.getHrnID(),
+                                       rt.isOutOfContext()
+                                       );
+          if( !oocHrnIdOoc2callee.contains( hio ) ) {
+            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.toCalleeContext( out, as );
+      out = Canonical.unshadow( out, as );
     }
     assert out.isCanonical();
     return out;
@@ -1303,190 +1465,75 @@ public class ReachGraph {
                     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
+    // first traverse this context to find nodes and edges
+    //  that will be callee-reachable
+    Set<HeapRegionNode> reachableCallerNodes =
+      new HashSet<HeapRegionNode>();
+
+    // caller edges between callee-reachable nodes
+    Set<RefEdge> reachableCallerEdges =
+      new HashSet<RefEdge>();
+
+    // 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>();
+
+    // caller edges from local vars or callee-unreachable nodes
+    // (out-of-context sources) to callee-reachable nodes
+    Set<RefEdge> oocCallerEdges =
+      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 < fmCallee.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( fmCallee, i );
+      VariableNode vnArgCaller = this.getVariableNodeFromTemp( tdArg );
 
-      // parameter defined here is the symbol in the callee
-      TempDescriptor tdParam = fmCallee.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 );
 
+      toVisitInCaller.add( vnArgCaller );
+      
       while( !toVisitInCaller.isEmpty() ) {
         RefSrcNode rsnCaller = toVisitInCaller.iterator().next();
-        RefSrcNode rsnCallee;
-
         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;
-
-        } 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(); 
-
-          if( !callerNodeIDsCopiedToCallee.contains( hrnSrcID ) ) {
-            
-            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(),
-                                          toCalleeContext( hrnSrcCaller.getInherent() ),
-                                          toCalleeContext( hrnSrcCaller.getAlpha() ),
-                                          preds,
-                                          hrnSrcCaller.getDescription()
-                                          );
-
-            callerNodeIDsCopiedToCallee.add( hrnSrcID );
-
-          } else {
-            rsnCallee = rg.id2hrn.get( hrnSrcID );
-          }
-        }
-
-        // SECOND - go over all edges from that source
 
         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(); 
-
-          if( !callerNodeIDsCopiedToCallee.contains( hrnDstID ) ) {
-
-            ExistPred pred = 
-              ExistPred.factory( hrnDstID, null );
-
-            ExistPredSet preds = 
-              ExistPredSet.factory( pred );
-            
-            hrnCallee = 
-              rg.createNewHeapRegionNode( hrnDstID,
-                                          hrnCaller.isSingleObject(),
-                                          hrnCaller.isNewSummary(),
-                                          hrnCaller.isFlagged(),
-                                          false, // out-of-context?
-                                          hrnCaller.getType(),
-                                          hrnCaller.getAllocSite(),
-                                          toCalleeContext( hrnCaller.getInherent() ),
-                                          toCalleeContext( hrnCaller.getAlpha() ),
-                                          preds,
-                                          hrnCaller.getDescription()
-                                          );
 
-            callerNodeIDsCopiedToCallee.add( hrnDstID );
+          callerNodeIDsCopiedToCallee.add( hrnCaller.getID() );
+          reachableCallerNodes.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
-          RefEdge reCallee = rsnCallee.getReferenceTo( hrnCallee,
-                                                       reCaller.getType(),
-                                                       reCaller.getField()
-                                                       );
-          if( reCallee == null ) {
-
-            ExistPred pred =
-              ExistPred.factory( tdSrc, 
-                                 hrnSrcID, 
-                                 hrnDstID,
-                                 reCaller.getType(),
-                                 reCaller.getField(),
-                                 null,
-                                 rsnCaller instanceof VariableNode ); // out-of-context
-
-            ExistPredSet preds = 
-              ExistPredSet.factory( pred );
-
-            rg.addRefEdge( rsnCallee,
-                           hrnCallee,
-                           new RefEdge( rsnCallee,
-                                        hrnCallee,
-                                        reCaller.getType(),
-                                        reCaller.getField(),
-                                        toCalleeContext( reCaller.getBeta() ),
-                                        preds
-                                        )
-                           );              
-          }
-          
-          // 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<Integer> itrInContext =
+    // now collect out-of-callee-context IDs and 
+    // map them to whether the ID is out of the caller
+    // context as well
+    Set<HrnIdOoc> oocHrnIdOoc2callee = new HashSet<HrnIdOoc>();
+
+    Iterator<Integer> itrInContext = 
       callerNodeIDsCopiedToCallee.iterator();
     while( itrInContext.hasNext() ) {
       Integer        hrnID                 = itrInContext.next();
@@ -1500,150 +1547,366 @@ public class ReachGraph {
         RefSrcNode rsnCallerAndOutContext =
           edgeMightCross.getSrc();
         
-        TypeDescriptor oocNodeType;
-        ReachSet       oocReach;
+        if( rsnCallerAndOutContext instanceof VariableNode ) {
+          // variables do not have out-of-context reach states,
+          // so jump out now
+          oocCallerEdges.add( edgeMightCross );
+          continue;
+        }
+          
+        HeapRegionNode hrnCallerAndOutContext = 
+          (HeapRegionNode) rsnCallerAndOutContext;
 
-        TempDescriptor oocPredSrcTemp = null;
-        Integer        oocPredSrcID   = null;
+        // is this source node out-of-context?
+        if( callerNodeIDsCopiedToCallee.contains( hrnCallerAndOutContext.getID() ) ) {
+          // no, skip this edge
+          continue;
+        }
 
-        if( rsnCallerAndOutContext instanceof VariableNode ) {
-          // variables are always out-of-context
-          oocNodeType = null;
-          oocReach    = rsetEmpty;
-          oocPredSrcTemp = 
-            ((VariableNode)rsnCallerAndOutContext).getTempDescriptor();
+        // okay, we got one
+        oocCallerEdges.add( edgeMightCross );
 
-        } else {
-          
-          HeapRegionNode hrnCallerAndOutContext = 
-            (HeapRegionNode) rsnCallerAndOutContext;
+        // 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();
 
-          // is this source node out-of-context?
-          if( callerNodeIDsCopiedToCallee.contains( hrnCallerAndOutContext.getID() ) ) {
-            // no, skip this edge
-            continue;
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+
+            oocHrnIdOoc2callee.add( new HrnIdOoc( rt.getHrnID(),
+                                                  rt.isOutOfContext()
+                                                  )
+                                    );
           }
+        }
+      }
+    }
 
-          oocNodeType  = hrnCallerAndOutContext.getType();
-          oocReach     = hrnCallerAndOutContext.getAlpha(); 
-          oocPredSrcID = hrnCallerAndOutContext.getID();
-        }        
+    // the callee view is a new graph: DON'T MODIFY *THIS* graph
+    ReachGraph rg = new ReachGraph();
 
-        // if we're here we've found an out-of-context edge
+    // 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,
+                                                   oocHrnIdOoc2callee 
+                                                   ),
+                                  toCalleeContext( hrnCaller.getAlpha(),
+                                                   preds,
+                                                   oocHrnIdOoc2callee 
+                                                   ),
+                                  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,
+                                      oocHrnIdOoc2callee
+                                      ),
+                     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,
+                                      oocHrnIdOoc2callee 
+                                      ),
+                     preds
+                     );
+      
+      rg.addRefEdge( hrnSrcCallee,
+                     hrnDstCallee,
+                     reCallee
+                     );        
+    }
 
-        ExistPred pred =
-          ExistPred.factory( oocPredSrcTemp, 
-                             oocPredSrcID, 
-                             hrnID,
-                             edgeMightCross.getType(),
-                             edgeMightCross.getField(),
-                             null,
-                             true ); // out-of-context
+    // 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;
 
-        ExistPredSet preds = 
-          ExistPredSet.factory( pred );
+      } 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
+                           );
 
-        HeapRegionNode hrnCalleeAndInContext = 
-          rg.id2hrn.get( hrnCallerAndInContext.getID() );
+      ExistPredSet preds = 
+        ExistPredSet.factory( pred );
         
-        RefEdge oocEdgeExisting =
-          rg.getOutOfContextReferenceTo( hrnCalleeAndInContext,
-                                         oocNodeType,
-                                         edgeMightCross.getType(),
-                                         edgeMightCross.getField()
-                                         );
+      RefEdge oocEdgeExisting =
+        rg.getOutOfContextReferenceTo( hrnDstCallee,
+                                       oocNodeType,
+                                       reCaller.getType(),
+                                       reCaller.getField()
+                                       );
 
-        if( oocEdgeExisting == null ) {
-          // 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
-          
+      if( oocEdgeExisting == null ) {          
           // for consistency, map one out-of-context "identifier"
           // to one heap region node id, otherwise no convergence
-          String oocid = "oocid"+
-            fmCallee+
-            hrnCalleeAndInContext.getIDString()+
-            oocNodeType+
-            edgeMightCross.getType()+
-            edgeMightCross.getField();
+        String oocid = "oocid"+
+          fmCallee+
+          hrnDstCallee.getIDString()+
+          oocNodeType+
+          reCaller.getType()+
+          reCaller.getField();
           
-          Integer oocHrnID = oocid2hrnid.get( oocid );
-
-          HeapRegionNode hrnCalleeAndOutContext;
+        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,
+                                                         oocHrnIdOoc2callee
+                                                         ),
+                                        toCalleeContext( oocReach,
+                                                         preds,
+                                                         oocHrnIdOoc2callee
+                                                         ),
+                                        preds,
+                                        "out-of-context"
+                                        );       
+          
+          oocid2hrnid.put( oocid, hrnCalleeAndOutContext.getID() );
+          
+        } else {
 
-          if( oocHrnID == null ) {
+          // the mapping already exists, so see if node is there
+          hrnCalleeAndOutContext = rg.id2hrn.get( oocHrnID );
 
+          if( hrnCalleeAndOutContext == null ) {
+            // nope, make it
             hrnCalleeAndOutContext =
-              rg.createNewHeapRegionNode( null,  // ID
+              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 ), // inherent
-                                          toCalleeContext( oocReach ), // alpha
+                                          toCalleeContext( oocReach,
+                                                           preds,
+                                                           oocHrnIdOoc2callee
+                                                           ),
+                                          toCalleeContext( oocReach,
+                                                           preds,
+                                                           oocHrnIdOoc2callee
+                                                           ),
                                           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 ), // inherent
-                                            toCalleeContext( oocReach ), // alpha
-                                            preds,
-                                            "out-of-context"
-                                            );       
-            }
+            // otherwise it is there, so merge reachability
+            hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
+                                                                     toCalleeContext( oocReach,
+                                                                                      preds,
+                                                                                      oocHrnIdOoc2callee
+                                                                                      )
+                                                                     )
+                                             );
           }
+        }
 
-          rg.addRefEdge( hrnCalleeAndOutContext,
-                         hrnCalleeAndInContext,
-                         new RefEdge( hrnCalleeAndOutContext,
-                                      hrnCalleeAndInContext,
-                                      edgeMightCross.getType(),
-                                      edgeMightCross.getField(),
-                                      toCalleeContext( edgeMightCross.getBeta() ),
-                                      preds
-                                      )
-                         );              
-
+        assert hrnCalleeAndOutContext.reachHasOnlyOOC();
+
+        rg.addRefEdge( hrnCalleeAndOutContext,
+                       hrnDstCallee,
+                       new RefEdge( hrnCalleeAndOutContext,
+                                    hrnDstCallee,
+                                    reCaller.getType(),
+                                    reCaller.getField(),
+                                    toCalleeContext( reCaller.getBeta(),
+                                                     preds,
+                                                     oocHrnIdOoc2callee
+                                                     ),
+                                    preds
+                                    )
+                       );              
+        
         } else {
-          // the out-of-context edge already exists
-          oocEdgeExisting.setBeta( Canonical.union( oocEdgeExisting.getBeta(),
-                                                    toCalleeContext( edgeMightCross.getBeta() )
-                                                    )
-                                   );         
-          oocEdgeExisting.setPreds( Canonical.join( oocEdgeExisting.getPreds(),
-                                                    edgeMightCross.getPreds()
-                                                    )
-                                    );          
+        // the out-of-context edge already exists
+        oocEdgeExisting.setBeta( Canonical.unionORpreds( oocEdgeExisting.getBeta(),
+                                                         toCalleeContext( reCaller.getBeta(),
+                                                                          preds,
+                                                                          oocHrnIdOoc2callee
+                                                                          )
+                                                  )
+                                 );         
           
-        }                
-      }
-    }    
+        oocEdgeExisting.setPreds( Canonical.join( oocEdgeExisting.getPreds(),
+                                                  preds
+                                                  )
+                                  );          
+
+        HeapRegionNode hrnCalleeAndOutContext =
+          (HeapRegionNode) oocEdgeExisting.getSrc();
+        hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
+                                                                 toCalleeContext( oocReach,
+                                                                                  preds,
+                                                                                  oocHrnIdOoc2callee
+                                                                                  )
+                                                                 )
+                                         );
+        
+        assert hrnCalleeAndOutContext.reachHasOnlyOOC();
+      }                
+    }
+
 
     if( writeDebugDOTs ) {    
-      try {
-        rg.writeGraph( "calleeview", true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      debugGraphPrefix = String.format( "call%02d", debugCallSiteVisits );
+      rg.writeGraph( debugGraphPrefix+"calleeview", 
+                     resolveMethodDebugDOTwriteLabels,    
+                     resolveMethodDebugDOTselectTemps,    
+                     resolveMethodDebugDOTpruneGarbage,   
+                     resolveMethodDebugDOThideSubsetReach,
+                     resolveMethodDebugDOThideEdgeTaints );      
     }
 
     return rg;
@@ -1653,6 +1916,17 @@ public class ReachGraph {
     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;
+
+  static String debugGraphPrefix;
+  static int debugCallSiteVisits = 0;
+  static int debugCallSiteVisitsUntilExit = 0;
+  
 
   public void 
     resolveMethodCall( FlatCall     fc,        
@@ -1662,18 +1936,32 @@ public class ReachGraph {
                        boolean      writeDebugDOTs
                        ) {
 
-
     if( writeDebugDOTs ) {
-      try {
-        rgCallee.writeGraph( "callee", 
-                             true, false, false, false, true, true );
-        writeGraph( "caller00In", 
-                    true, false, false, false, true, true, 
-                    callerNodeIDsCopiedToCallee );
-      } catch( IOException e ) {}
+      System.out.println( "  Writing out visit "+
+                          debugCallSiteVisits+
+                          " to debug call site" );
+
+      debugGraphPrefix = String.format( "call%02d", 
+                                        debugCallSiteVisits );
+      
+      rgCallee.writeGraph( debugGraphPrefix+"callee", 
+                           resolveMethodDebugDOTwriteLabels,    
+                           resolveMethodDebugDOTselectTemps,    
+                           resolveMethodDebugDOTpruneGarbage,   
+                           resolveMethodDebugDOThideSubsetReach,
+                           resolveMethodDebugDOThideEdgeTaints );
+      
+      writeGraph( debugGraphPrefix+"caller00In",  
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints,
+                  callerNodeIDsCopiedToCallee );
     }
 
 
+
     // method call transfer function steps:
     // 1. Use current callee-reachable heap (CRH) to test callee 
     //    predicates and mark what will be coming in.
@@ -1687,7 +1975,6 @@ public class ReachGraph {
     // 5. Global sweep it.
 
 
-
     // 1. mark what callee elements have satisfied predicates
     Hashtable<HeapRegionNode, ExistPredSet> calleeNodesSatisfied =
       new Hashtable<HeapRegionNode, ExistPredSet>();
@@ -1695,6 +1982,9 @@ public class ReachGraph {
     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> >();
 
@@ -1712,13 +2002,30 @@ public class ReachGraph {
         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();
@@ -1741,12 +2048,32 @@ public class ReachGraph {
         HeapRegionNode hrnSrcCallee = (HeapRegionNode) rsnCallee;
         boolean matchedOutOfContext = false;
 
-        if( hrnSrcCallee.isOutOfContext() ) {          
+        if( !hrnSrcCallee.isOutOfContext() ) {          
+
+          predsIfSatis = 
+            hrnSrcCallee.getPreds().isSatisfiedBy( this,
+                                                   callerNodeIDsCopiedToCallee
+                                                   );          
+          if( predsIfSatis != null ) {
+            calleeNodesSatisfied.put( hrnSrcCallee, predsIfSatis );
+          } else {
+            // otherwise forget this edge
+            continue;
+          }          
+      
+        } else {
+          // hrnSrcCallee is out-of-context
 
           assert !calleeEdges2oocCallerSrcMatches.containsKey( reCallee );
+
           Set<RefSrcNode> rsnCallers = new HashSet<RefSrcNode>();            
 
+          // is the target node in the caller?
           HeapRegionNode hrnDstCaller = this.id2hrn.get( hrnCallee.getID() );
+          if( hrnDstCaller == null ) {
+            continue;
+          }          
+
           Iterator<RefEdge> reDstItr = hrnDstCaller.iteratorToReferencers();
           while( reDstItr.hasNext() ) {
             // the edge and field (either possibly null) must match
@@ -1760,6 +2087,7 @@ public class ReachGraph {
             
             RefSrcNode rsnCaller = reCaller.getSrc();
             if( rsnCaller instanceof VariableNode ) {
+
               // a variable node matches an OOC region with null type
               if( hrnSrcCallee.getType() != null ) {
                 continue;
@@ -1797,50 +2125,35 @@ public class ReachGraph {
           reCallee.getPreds().isSatisfiedBy( this,
                                              callerNodeIDsCopiedToCallee
                                              );
-        if( predsIfSatis != null ) {
-          calleeEdgesSatisfied.put( reCallee, 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
+          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", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller20BeforeWipe", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -1859,13 +2172,17 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller30BeforeAddingNodes", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller30BeforeAddingNodes", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
+
+
     // 3. callee elements with satisfied preds come in, note that
     //    the mapping of elements satisfied to preds is like this:
     //    A callee element EE has preds EEp that are satisfied by
@@ -1903,7 +2220,8 @@ public class ReachGraph {
                                    false,                      // out-of-context?
                                    hrnCallee.getType(),        // type                          
                                    hrnCallee.getAllocSite(),   // allocation site                       
-                                   hrnCallee.getInherent(),    // inherent reach
+                                   toCallerContext( hrnCallee.getInherent(),
+                                                    calleeStatesSatisfied  ),    // inherent reach
                                    null,                       // current reach                 
                                    predsEmpty,                 // predicates
                                    hrnCallee.getDescription()  // description
@@ -1912,22 +2230,38 @@ public class ReachGraph {
         assert hrnCaller.isWiped();
       }
 
-      // TODO: alpha should be some rewritten version of callee in caller context
-      hrnCaller.setAlpha( hrnCallee.getAlpha() );
+      hrnCaller.setAlpha( toCallerContext( hrnCallee.getAlpha(),
+                                           calleeStatesSatisfied 
+                                           )
+                          );
 
       hrnCaller.setPreds( preds );
     }
 
 
 
+
+
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller31BeforeAddingEdges", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller31BeforeAddingEdges", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
+    // 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() ) {
@@ -1953,6 +2287,14 @@ public class ReachGraph {
       
       Set<RefSrcNode> oocCallers = 
         calleeEdges2oocCallerSrcMatches.get( reCallee );
+
+      if( rsnCallee instanceof HeapRegionNode ) {
+        HeapRegionNode hrnCalleeSrc = (HeapRegionNode) rsnCallee;
+        if( hrnCalleeSrc.isOutOfContext() ) {
+          assert oocCallers != null;
+        }
+      }
+
       
       if( oocCallers == null ) {
         // there are no out-of-context matches, so it's
@@ -1969,12 +2311,13 @@ public class ReachGraph {
             // to the callee so we ignore it in call site transfer
             // shouldn't this NEVER HAPPEN?
             assert false;
-            //continue;
           }
+
           rsnCallers.add( this.getVariableNodeFromTemp( tdArg ) );
 
         } else {
           // otherwise source is in context, one region
+          
           HeapRegionNode hrnSrcCallee = (HeapRegionNode) rsnCallee;
 
           // translate an in-context node to shadow
@@ -1987,21 +2330,7 @@ public class ReachGraph {
           HeapRegionNode hrnSrcCallerShadow =
             this.id2hrn.get( hrnIDSrcShadow );
           
-          if( hrnSrcCallerShadow == null ) {
-            hrnSrcCallerShadow =
-              createNewHeapRegionNode( hrnIDSrcShadow,                // id or null to generate a new one 
-                                       hrnSrcCallee.isSingleObject(), // single object?                 
-                                       hrnSrcCallee.isNewSummary(),   // summary?       
-                                       hrnSrcCallee.isFlagged(),      // flagged?
-                                       false,                         // out-of-context?
-                                       hrnSrcCallee.getType(),        // type                           
-                                       hrnSrcCallee.getAllocSite(),   // allocation site                        
-                                       hrnSrcCallee.getInherent(),    // inherent reach
-                                       hrnSrcCallee.getAlpha(),       // current reach                 
-                                       predsEmpty,                    // predicates
-                                       hrnSrcCallee.getDescription()  // description
-                                       );                                        
-          }
+          assert hrnSrcCallerShadow != null;        
           
           rsnCallers.add( hrnSrcCallerShadow );
         }
@@ -2020,25 +2349,53 @@ public class ReachGraph {
       while( rsnItr.hasNext() ) {
         RefSrcNode rsnCaller = rsnItr.next();
         
-        // TODO: beta rewrites
         RefEdge reCaller = new RefEdge( rsnCaller,
                                         hrnDstCaller,
                                         reCallee.getType(),
                                         reCallee.getField(),
-                                        reCallee.getBeta(),
+                                        toCallerContext( reCallee.getBeta(),
+                                                         calleeStatesSatisfied ),
                                         preds
                                         );
-        
-        // 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.union( edgeExisting.getBeta(),
-                                                reCaller.getBeta()
+
+        ChangeSet cs = ChangeSet.factory();
+        Iterator<ReachState> rsItr = reCaller.getBeta().iterator();
+        while( rsItr.hasNext() ) {
+          ReachState   state          = rsItr.next();
+          ExistPredSet predsPreCallee = state.getPreds();
+
+          if( state.isEmpty() ) {
+            continue;
+          }
+
+          Iterator<ExistPred> predItr = predsPreCallee.iterator();
+          while( predItr.hasNext() ) {            
+            ExistPred pred = predItr.next();
+            ReachState old = pred.ne_state;
+
+            if( old == null ) {
+              old = rstateEmpty;
+            }
+
+            cs = Canonical.add( cs,
+                                ChangeTuple.factory( old,
+                                                     state
+                                                     )
+                                );
+          }
+        }
+        
+
+        // 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(
@@ -2046,9 +2403,29 @@ public class ReachGraph {
                                                 reCaller.getPreds()
                                                 )
                                 );
+
+          // for reach propagation
+          if( !cs.isEmpty() ) {
+            ChangeSet csExisting = edgePlannedChanges.get( edgeExisting );
+            if( csExisting == null ) {
+              csExisting = ChangeSet.factory();
+            }
+            edgePlannedChanges.put( edgeExisting, 
+                                    Canonical.union( csExisting,
+                                                     cs
+                                                     ) 
+                                    );
+          }
           
         } else {                         
           addRefEdge( rsnCaller, hrnDstCaller, reCaller );     
+
+          // for reach propagation
+          if( !cs.isEmpty() ) {
+            edgesForPropagation.add( reCaller );
+            assert !edgePlannedChanges.containsKey( reCaller );
+            edgePlannedChanges.put( reCaller, cs );
+          }
         }
       }
     }
@@ -2056,12 +2433,13 @@ public class ReachGraph {
 
 
 
-
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller35BeforeAssignReturnValue", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller35BeforeAssignReturnValue", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -2072,7 +2450,9 @@ public class ReachGraph {
     
     // 3.d) handle return value assignment if needed
     TempDescriptor returnTemp = fc.getReturnTemp();
-    if( returnTemp != null && !returnTemp.getType().isImmutable() ) {
+    if( returnTemp != null && 
+        DisjointAnalysis.shouldAnalysisTrack( returnTemp.getType() ) 
+        ) {
 
       VariableNode vnLhsCaller = getVariableNodeFromTemp( returnTemp );
       clearRefEdgesFrom( vnLhsCaller, null, null, true );
@@ -2107,13 +2487,13 @@ public class ReachGraph {
                                      false,                         // out-of-context?
                                      hrnDstCallee.getType(),        // type                             
                                      hrnDstCallee.getAllocSite(),   // allocation site                  
-                                     hrnDstCallee.getInherent(),    // inherent reach
-                                     hrnDstCallee.getAlpha(),       // current reach                 
+                                     toCallerContext( hrnDstCallee.getInherent(),
+                                                      calleeStatesSatisfied  ),    // inherent reach
+                                     toCallerContext( hrnDstCallee.getAlpha(),
+                                                      calleeStatesSatisfied  ),    // current reach                 
                                      predsTrue,                     // predicates
                                      hrnDstCallee.getDescription()  // description
                                      );                                        
-        } else {
-          assert hrnDstCaller.isWiped();
         }
 
         TypeDescriptor tdNewEdge =
@@ -2126,7 +2506,8 @@ public class ReachGraph {
                                         hrnDstCaller,
                                         tdNewEdge,
                                         null,
-                                        reCallee.getBeta(),
+                                        toCallerContext( reCallee.getBeta(),
+                                                         calleeStatesSatisfied ),
                                         predsTrue
                                         );
 
@@ -2137,10 +2518,41 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller40BeforeShadowMerge", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller38propagateReach", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
+    }
+
+    // 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();
+    }
+
+
+
+
+
+
+
+    if( writeDebugDOTs ) {
+      writeGraph( debugGraphPrefix+"caller40BeforeShadowMerge", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
     
 
@@ -2233,24 +2645,69 @@ public class ReachGraph {
     }
 
 
+
+
+
+
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller50BeforeGlobalSweep", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller45BeforeUnshadow", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
+    }
+    
+    
+    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() ) );
+      }
+    }
+    
+
+
+
+    if( writeDebugDOTs ) {
+      writeGraph( debugGraphPrefix+"caller50BeforeGlobalSweep", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
     // 5.
-    globalSweep();
+    if( !DISABLE_GLOBAL_SWEEP ) {
+      globalSweep();
+    }
     
 
 
+
+
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller90AfterTransfer", 
-                    true, false, false, false, true, true );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller90AfterTransfer", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
+
+      ++debugCallSiteVisits;
+      if( debugCallSiteVisits >= debugCallSiteVisitsUntilExit ) {
+        System.out.println( "!!! Exiting after requested visits to call site. !!!" );
+        System.exit( 0 );
+      }
     }
   } 
 
@@ -2378,10 +2835,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();
@@ -2398,64 +2870,141 @@ public class ReachGraph {
        assert rsetEmpty.equals( edge.getBetaNew() );
       }      
 
-      // calculate boldB for this flagged node
+      // make a mapping of IDs to heap regions they propagate from
       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() );
+
+        // in-context flagged node IDs simply propagate from the
+        // node they name
+        Set<HeapRegionNode> srcs = new HashSet<HeapRegionNode>();
+        srcs.add( hrn );
+        icID2srcs.put( hrn.getID(), srcs );
+      }
+
+      if( hrn.isOutOfContext() ) {
+       assert !hrn.isFlagged();
+
+        // the reachability states on an out-of-context
+        // node are not really important (combinations of
+        // IDs or arity)--what matters is that the states
+        // specify which nodes this out-of-context node
+        // stands in for.  For example, if the state [17?, 19*]
+        // appears on the ooc node, it may serve as a source
+        // for node 17? and a source for node 19.
+        Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+            assert rt.isOutOfContext();
+
+            Set<HeapRegionNode> srcs = oocID2srcs.get( rt.getHrnID() );
+            if( srcs == null ) {
+              srcs = new HashSet<HeapRegionNode>();
+            }
+            srcs.add( hrn );
+            oocID2srcs.put( rt.getHrnID(), srcs );
+          }
+        }
+      }
+    }
 
-       // initial boldB_f constraints
-       Iterator<RefEdge> itrRees = hrn.iteratorToReferencees();
-       while( itrRees.hasNext() ) {
-         RefEdge edge = itrRees.next();
+    // calculate boldB for all hrnIDs identified by the above
+    // node traversal, propagating from every source
+    while( !icID2srcs.isEmpty() || !oocID2srcs.isEmpty() ) {
 
-         assert !boldB.containsKey( edge );
-         boldB_f.put( edge, edge.getBeta() );
+      Integer             hrnID;
+      Set<HeapRegionNode> srcs;
+      boolean             inContext;
 
-         assert !workSetEdges.contains( edge );
-         workSetEdges.add( edge );
-       }       
+      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 );
 
-       // 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();            
+      } 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 );
+      }
     }
 
 
@@ -2473,14 +3022,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,
-                            false // out-of-context
-                            );
+      // 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();
 
@@ -2503,23 +3058,35 @@ 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 {
 
+              if( !id2hrn.containsKey( rtOld.getHrnID() ) ) {
+                // let symbols not in the graph get pruned
+                break;
+              }
+
+              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 );          
          }
@@ -2527,9 +3094,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;
        }
@@ -2542,19 +3109,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
@@ -2597,7 +3164,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() );
@@ -2647,13 +3223,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 );
        }       
@@ -2668,6 +3247,132 @@ public class ReachGraph {
   }  
 
 
+  // a useful assertion for debugging:
+  // every in-context tuple on any edge or
+  // any node should name a node that is
+  // part of the graph
+  public boolean inContextTuplesInGraph() {
+
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      {
+        Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+          
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+            
+            if( !rt.isOutOfContext() ) {
+              if( !id2hrn.containsKey( rt.getHrnID() ) ) {
+                System.out.println( rt.getHrnID()+" is missing" );
+                return false;
+              }
+            }
+          }
+        }
+      }
+
+      Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+      while( edgeItr.hasNext() ) {
+        RefEdge edge = edgeItr.next();
+
+        Iterator<ReachState> stateItr = edge.getBeta().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+        
+          Iterator<ReachTuple> rtItr = state.iterator();
+          while( rtItr.hasNext() ) {
+            ReachTuple rt = rtItr.next();
+            
+            if( !rt.isOutOfContext() ) {
+              if( !id2hrn.containsKey( rt.getHrnID() ) ) {
+                System.out.println( rt.getHrnID()+" is missing" );
+                return false;
+              }
+            }
+          }
+        }
+      }
+    }
+
+    return true;
+  }
+
+
+  // another useful assertion for debugging
+  public boolean noEmptyReachSetsInGraph() {
+    
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      if( !hrn.isOutOfContext() && 
+          !hrn.isWiped()        &&
+          hrn.getAlpha().isEmpty() 
+          ) {
+        System.out.println( "!!! "+hrn+" has an empty ReachSet !!!" );
+        return false;
+      }
+
+      Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+      while( edgeItr.hasNext() ) {
+        RefEdge edge = edgeItr.next();
+
+        if( edge.getBeta().isEmpty() ) {
+          System.out.println( "!!! "+edge+" has an empty ReachSet !!!" );
+          return false;
+        }
+      }
+    }
+    
+    return true;
+  }
+
+
+  public boolean everyReachStateWTrue() {
+
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry)      hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+      {
+        Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+          
+          if( !state.getPreds().equals( predsTrue ) ) {
+            return false;
+          }
+        }
+      }
+
+      Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+      while( edgeItr.hasNext() ) {
+        RefEdge edge = edgeItr.next();
+
+        Iterator<ReachState> stateItr = edge.getBeta().iterator();
+        while( stateItr.hasNext() ) {
+          ReachState state = stateItr.next();
+
+          if( !state.getPreds().equals( predsTrue ) ) {
+            return false;
+          }
+        }
+      }
+    }
+
+    return true;
+  }
+  
+
+
 
   ////////////////////////////////////////////////////
   // high-level merge operations
@@ -2726,18 +3431,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()
+                                       )
+                       );
       }
     }
 
@@ -2811,16 +3513,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()
+                                               )
+                               );
        }
       }
     }
@@ -2876,16 +3577,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()
+                                                )
+                                );
        }
       }
     }
@@ -2896,6 +3595,10 @@ public class ReachGraph {
   }
 
 
+
+  static boolean dbgEquals = false;
+
+
   // it is necessary in the equals() member functions
   // to "check both ways" when comparing the data
   // structures of two graphs.  For instance, if all
@@ -2909,18 +3612,30 @@ public class ReachGraph {
   public boolean equals( ReachGraph rg ) {
 
     if( rg == null ) {
+      if( dbgEquals ) {
+        System.out.println( "rg is null" );
+      }
       return false;
     }
     
     if( !areHeapRegionNodesEqual( rg ) ) {
+      if( dbgEquals ) {
+        System.out.println( "hrn not equal" );
+      }
       return false;
     }
 
     if( !areVariableNodesEqual( rg ) ) {
+      if( dbgEquals ) {
+        System.out.println( "vars not equal" );
+      }
       return false;
     }
 
     if( !areRefEdgesEqual( rg ) ) {
+      if( dbgEquals ) {
+        System.out.println( "edges not equal" );
+      }
       return false;
     }
 
@@ -2967,7 +3682,6 @@ public class ReachGraph {
     
     return true;
   }
-  
 
   protected boolean areVariableNodesEqual( ReachGraph rg ) {
 
@@ -3004,6 +3718,10 @@ public class ReachGraph {
       return false;
     }
 
+    if( !areallREinAandBequal( rg, this ) ) {
+      return false;
+    }    
+
     return true;
   }
 
@@ -3117,6 +3835,94 @@ public class ReachGraph {
   }
 
 
+  // can be used to assert monotonicity
+  static public boolean isNoSmallerThan( ReachGraph rgA, 
+                                         ReachGraph rgB ) {
+
+    //System.out.println( "*** Asking if A is no smaller than B ***" );
+
+
+    Iterator iA = rgA.id2hrn.entrySet().iterator();
+    while( iA.hasNext() ) {
+      Map.Entry      meA  = (Map.Entry)      iA.next();
+      Integer        idA  = (Integer)        meA.getKey();
+      HeapRegionNode hrnA = (HeapRegionNode) meA.getValue();
+
+      if( !rgB.id2hrn.containsKey( idA ) ) {
+        System.out.println( "  regions smaller" );
+       return false;
+      }
+
+      //HeapRegionNode hrnB = rgB.id2hrn.get( idA );
+      /* NOT EQUALS, NO SMALLER THAN!
+      if( !hrnA.equalsIncludingAlphaAndPreds( hrnB ) ) {
+        System.out.println( "  regions smaller" );
+       return false;
+      }
+      */
+    }
+    
+    // this works just fine, no smaller than
+    if( !areallVNinAalsoinBandequal( rgA, rgB ) ) {
+      System.out.println( "  vars smaller:" );
+      System.out.println( "    A:"+rgA.td2vn.keySet() );
+      System.out.println( "    B:"+rgB.td2vn.keySet() );
+      return false;
+    }
+
+
+    iA = rgA.id2hrn.entrySet().iterator();
+    while( iA.hasNext() ) {
+      Map.Entry      meA  = (Map.Entry)      iA.next();
+      Integer        idA  = (Integer)        meA.getKey();
+      HeapRegionNode hrnA = (HeapRegionNode) meA.getValue();
+
+      Iterator<RefEdge> reItr = hrnA.iteratorToReferencers();
+      while( reItr.hasNext() ) {
+        RefEdge    edgeA = reItr.next();
+        RefSrcNode rsnA  = edgeA.getSrc();
+
+        // we already checked that nodes were present
+        HeapRegionNode hrnB = rgB.id2hrn.get( hrnA.getID() );
+        assert hrnB != null;
+
+        RefSrcNode rsnB;
+        if( rsnA instanceof VariableNode ) {
+          VariableNode vnA = (VariableNode) rsnA;
+          rsnB = rgB.td2vn.get( vnA.getTempDescriptor() );
+
+        } else {
+          HeapRegionNode hrnSrcA = (HeapRegionNode) rsnA;
+          rsnB = rgB.id2hrn.get( hrnSrcA.getID() );
+        }
+        assert rsnB != null;
+
+        RefEdge edgeB = rsnB.getReferenceTo( hrnB,
+                                             edgeA.getType(),
+                                             edgeA.getField()
+                                             );
+        if( edgeB == null ) {
+          System.out.println( "  edges smaller:" );          
+          return false;
+        }        
+
+        // REMEMBER, IS NO SMALLER THAN
+        /*
+          System.out.println( "  edges smaller" );
+          return false;
+          }
+        */
+
+      }
+    }
+
+    
+    return true;
+  }
+
+
+
+
 
   // this analysis no longer has the "match anything"
   // type which was represented by null
@@ -3236,19 +4042,29 @@ public class ReachGraph {
   
 
 
+  // the default signature for quick-and-dirty debugging
+  public void writeGraph( String graphName ) {
+    writeGraph( graphName,
+                true, // write labels
+                true, // label select
+                true, // prune garbage
+                true, // hide subset reachability
+                true, // hide edge taints
+                null  // in-context boundary
+                );
+  }
+
   public void writeGraph( String  graphName,
                           boolean writeLabels,
                           boolean labelSelect,
                           boolean pruneGarbage,
-                          boolean writeReferencers,
                           boolean hideSubsetReachability,
                           boolean hideEdgeTaints
-                          ) throws java.io.IOException {
+                          ) {
     writeGraph( graphName,
                 writeLabels,
                 labelSelect,
                 pruneGarbage,
-                writeReferencers,
                 hideSubsetReachability,
                 hideEdgeTaints,
                 null );
@@ -3258,130 +4074,129 @@ public class ReachGraph {
                           boolean      writeLabels,
                           boolean      labelSelect,
                           boolean      pruneGarbage,
-                          boolean      writeReferencers,
                           boolean      hideSubsetReachability,
                           boolean      hideEdgeTaints,
                           Set<Integer> callerNodeIDsCopiedToCallee
-                          ) throws java.io.IOException {
+                          ) {
     
-    // remove all non-word characters from the graph name so
-    // the filename and identifier in dot don't cause errors
-    graphName = graphName.replaceAll( "[\\W]", "" );
-
-    BufferedWriter bw = 
-      new BufferedWriter( new FileWriter( graphName+".dot" ) );
-
-    bw.write( "digraph "+graphName+" {\n" );
+    try {
+      // remove all non-word characters from the graph name so
+      // the filename and identifier in dot don't cause errors
+      graphName = graphName.replaceAll( "[\\W]", "" );
 
+      BufferedWriter bw = 
+        new BufferedWriter( new FileWriter( graphName+".dot" ) );
 
-    // this is an optional step to form the callee-reachable
-    // "cut-out" into a DOT cluster for visualization
-    if( callerNodeIDsCopiedToCallee != null ) {
+      bw.write( "digraph "+graphName+" {\n" );
 
-      bw.write( "  subgraph cluster0 {\n" );
-      bw.write( "    color=blue;\n" );
-
-      Iterator i = id2hrn.entrySet().iterator();
-      while( i.hasNext() ) {
-        Map.Entry      me  = (Map.Entry)      i.next();
-        HeapRegionNode hrn = (HeapRegionNode) me.getValue();      
+      
+      // this is an optional step to form the callee-reachable
+      // "cut-out" into a DOT cluster for visualization
+      if( callerNodeIDsCopiedToCallee != null ) {
         
-        if( callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) {
-          bw.write( "    "+hrn.toString()+
-                    hrn.toStringDOT( hideSubsetReachability )+
-                    ";\n" );
+        bw.write( "  subgraph cluster0 {\n" );
+        bw.write( "    color=blue;\n" );
+      
+        Iterator i = id2hrn.entrySet().iterator();
+        while( i.hasNext() ) {
+          Map.Entry      me  = (Map.Entry)      i.next();
+          HeapRegionNode hrn = (HeapRegionNode) me.getValue();      
           
+          if( callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) {
+            bw.write( "    "+hrn.toString()+
+                      hrn.toStringDOT( hideSubsetReachability )+
+                      ";\n" );
+            
+          }
         }
+        
+        bw.write( "  }\n" );
       }
-
-      bw.write( "  }\n" );
-    }
-
-
-    Set<HeapRegionNode> visited = new HashSet<HeapRegionNode>();
-
-    // then visit every heap region node    
-    Iterator i = id2hrn.entrySet().iterator();
-    while( i.hasNext() ) {
-      Map.Entry      me  = (Map.Entry)      i.next();
-      HeapRegionNode hrn = (HeapRegionNode) me.getValue();      
-
-      // 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" ) ||
-          hrn.isOutOfContext()
-          ) {
-
-       if( !visited.contains( hrn ) ) {
-         traverseHeapRegionNodes( hrn,
-                                   bw,
-                                   null,
-                                   visited,
-                                   writeReferencers,
-                                   hideSubsetReachability,
-                                   hideEdgeTaints,
-                                   callerNodeIDsCopiedToCallee );
-       }
-      }
-    }
-
-    bw.write( "  graphTitle[label=\""+graphName+"\",shape=box];\n" );
-  
-
-    // then visit every label node, useful for debugging
-    if( writeLabels ) {
-      i = td2vn.entrySet().iterator();
+      
+      
+      Set<HeapRegionNode> visited = new HashSet<HeapRegionNode>();
+      
+      // then visit every heap region node    
+      Iterator i = id2hrn.entrySet().iterator();
       while( i.hasNext() ) {
-        Map.Entry    me = (Map.Entry)    i.next();
-        VariableNode vn = (VariableNode) me.getValue();
-        
-        if( labelSelect ) {
-          String labelStr = vn.getTempDescriptorString();
-          if( labelStr.startsWith("___temp") ||
-              labelStr.startsWith("___dst") ||
-              labelStr.startsWith("___srctmp") ||
-              labelStr.startsWith("___neverused")
-              ) {
-            continue;
-          }
-        }
+        Map.Entry      me  = (Map.Entry)      i.next();
+        HeapRegionNode hrn = (HeapRegionNode) me.getValue();      
         
-        Iterator<RefEdge> heapRegionsItr = vn.iteratorToReferencees();
-        while( heapRegionsItr.hasNext() ) {
-          RefEdge        edge = heapRegionsItr.next();
-          HeapRegionNode hrn  = edge.getDst();
+        // 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.isOutOfContext()
+            ) {
           
-          if( pruneGarbage && !visited.contains( hrn ) ) {
+          if( !visited.contains( hrn ) ) {
             traverseHeapRegionNodes( hrn,
                                      bw,
                                      null,
                                      visited,
-                                     writeReferencers,
                                      hideSubsetReachability,
                                      hideEdgeTaints,
                                      callerNodeIDsCopiedToCallee );
           }
+        }
+      }
+      
+      bw.write( "  graphTitle[label=\""+graphName+"\",shape=box];\n" );
+      
+      
+      // then visit every label node, useful for debugging
+      if( writeLabels ) {
+        i = td2vn.entrySet().iterator();
+        while( i.hasNext() ) {
+          Map.Entry    me = (Map.Entry)    i.next();
+          VariableNode vn = (VariableNode) me.getValue();
           
-          bw.write( "  "+vn.toString()+
-                    " -> "+hrn.toString()+
-                    edge.toStringDOT( hideSubsetReachability, "" )+
-                    ";\n" );
+          if( labelSelect ) {
+            String labelStr = vn.getTempDescriptorString();
+            if( labelStr.startsWith( "___temp" )     ||
+                labelStr.startsWith( "___dst" )      ||
+                labelStr.startsWith( "___srctmp" )   ||
+                labelStr.startsWith( "___neverused" )
+                ) {
+              continue;
+            }
+          }
+          
+          Iterator<RefEdge> heapRegionsItr = vn.iteratorToReferencees();
+          while( heapRegionsItr.hasNext() ) {
+            RefEdge        edge = heapRegionsItr.next();
+            HeapRegionNode hrn  = edge.getDst();
+          
+            if( !visited.contains( hrn ) ) {
+              traverseHeapRegionNodes( hrn,
+                                       bw,
+                                       null,
+                                       visited,
+                                       hideSubsetReachability,
+                                       hideEdgeTaints,
+                                       callerNodeIDsCopiedToCallee );
+            }
+          
+            bw.write( "  "+vn.toString()+
+                      " -> "+hrn.toString()+
+                      edge.toStringDOT( hideSubsetReachability, "" )+
+                      ";\n" );
+          }
         }
       }
-    }
     
-    bw.write( "}\n" );
-    bw.close();
+      bw.write( "}\n" );
+      bw.close();
+
+    } catch( IOException e ) {
+      throw new Error( "Error writing out DOT graph "+graphName );
+    }
   }
 
   protected void traverseHeapRegionNodes( HeapRegionNode      hrn,
                                           BufferedWriter      bw,
                                           TempDescriptor      td,
                                           Set<HeapRegionNode> visited,
-                                          boolean             writeReferencers,
                                           boolean             hideSubsetReachability,
                                           boolean             hideEdgeTaints,
                                           Set<Integer>        callerNodeIDsCopiedToCallee
@@ -3442,11 +4257,353 @@ public class ReachGraph {
                                bw,
                                td,
                                visited,
-                               writeReferencers,
                                hideSubsetReachability,
                                hideEdgeTaints,
                                callerNodeIDsCopiedToCallee );
     }
   }  
+  
 
+
+
+
+  public Set<HeapRegionNode> findCommonReachableNodes( ReachSet proofOfSharing ) {
+
+    Set<HeapRegionNode> exhibitProofState =
+      new HashSet<HeapRegionNode>();
+
+    Iterator hrnItr = id2hrn.entrySet().iterator();
+    while( hrnItr.hasNext() ) {
+      Map.Entry      me  = (Map.Entry) hrnItr.next();
+      HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+      
+      ReachSet intersection =
+        Canonical.intersection( proofOfSharing,
+                                hrn.getAlpha()
+                                );
+      if( !intersection.isEmpty() ) {
+        assert !hrn.isOutOfContext();
+        exhibitProofState.add( hrn );
+      }
+    }
+    
+    return exhibitProofState;
+  }
+
+        
+  public Set<HeapRegionNode> mayReachSharedObjects(HeapRegionNode hrn1,
+                                                   HeapRegionNode hrn2) {
+    assert hrn1 != null;
+    assert hrn2 != null;
+
+    assert !hrn1.isOutOfContext();
+    assert !hrn2.isOutOfContext();
+
+    assert belongsToThis( hrn1 );
+    assert belongsToThis( hrn2 );
+
+    assert !hrn1.getID().equals( hrn2.getID() );
+
+
+    // then get the various tokens for these heap regions
+    ReachTuple h1 = 
+      ReachTuple.factory( hrn1.getID(),
+                          !hrn1.isSingleObject(), // multi?
+                          ReachTuple.ARITY_ONE, 
+                          false );                // ooc?
+    
+    ReachTuple h1star = null;
+    if( !hrn1.isSingleObject() ) {
+      h1star = 
+        ReachTuple.factory( hrn1.getID(), 
+                            !hrn1.isSingleObject(), 
+                            ReachTuple.ARITY_ZEROORMORE,
+                            false );
+    }
+    
+    ReachTuple h2 = 
+      ReachTuple.factory( hrn2.getID(),
+                          !hrn2.isSingleObject(),
+                          ReachTuple.ARITY_ONE,
+                          false );
+
+    ReachTuple h2star = null;
+    if( !hrn2.isSingleObject() ) {    
+      h2star =
+        ReachTuple.factory( hrn2.getID(), 
+                            !hrn2.isSingleObject(),
+                            ReachTuple.ARITY_ZEROORMORE,
+                            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());
+    }
+
+    ReachSet proofOfSharing = ReachSet.factory();
+
+    proofOfSharing = 
+      Canonical.unionORpreds( proofOfSharing,
+                              beta1.getStatesWithBoth( h1, h2 )
+                              );
+    proofOfSharing = 
+      Canonical.unionORpreds( proofOfSharing,
+                              beta2.getStatesWithBoth( h1, h2 )
+                              );
+    
+    if( !hrn1.isSingleObject() ) {    
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta1.getStatesWithBoth( h1star, h2 )
+                                );
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta2.getStatesWithBoth( h1star, h2 )
+                                );      
+    }
+
+    if( !hrn2.isSingleObject() ) {    
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta1.getStatesWithBoth( h1, h2star )
+                                );
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta2.getStatesWithBoth( h1, h2star )
+                                );
+    }
+
+    if( !hrn1.isSingleObject() &&
+        !hrn2.isSingleObject()
+        ) {    
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta1.getStatesWithBoth( h1star, h2star )
+                                );
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta2.getStatesWithBoth( h1star, h2star )
+                                );
+    }
+    
+    Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
+    if( !proofOfSharing.isEmpty() ) {
+      common = findCommonReachableNodes( proofOfSharing );
+      if( !DISABLE_STRONG_UPDATES &&
+          !DISABLE_GLOBAL_SWEEP
+          ) {        
+        assert !common.isEmpty();
+      }
+    }
+
+    return common;
+  }
+
+  // this version of the above method checks whether there is sharing
+  // among the objects in a summary node
+  public Set<HeapRegionNode> mayReachSharedObjects(HeapRegionNode hrn) {
+    assert hrn != null;
+    assert hrn.isNewSummary();
+    assert !hrn.isOutOfContext();
+    assert belongsToThis( hrn );
+
+    ReachTuple hstar =  
+      ReachTuple.factory( hrn.getID(), 
+                          true,    // multi
+                          ReachTuple.ARITY_ZEROORMORE,
+                          false ); // ooc    
+
+    // then get the merged beta of all out-going edges from 
+    // this heap region
+
+    ReachSet beta = ReachSet.factory();
+    Iterator<RefEdge> itrEdge = hrn.iteratorToReferencees();
+    while (itrEdge.hasNext()) {
+      RefEdge edge = itrEdge.next();
+      beta = Canonical.unionORpreds(beta, edge.getBeta());
+    }
+    
+    ReachSet proofOfSharing = ReachSet.factory();
+
+    proofOfSharing = 
+      Canonical.unionORpreds( proofOfSharing,
+                              beta.getStatesWithBoth( hstar, hstar )
+                              );
+    
+    Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
+    if( !proofOfSharing.isEmpty() ) {
+      common = findCommonReachableNodes( proofOfSharing );
+      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());
+    assert this.hasVariable( paramTemp1 );
+    VariableNode paramVar1 = getVariableNodeFromTemp(paramTemp1);
+
+
+    if( !(paramVar1.getNumReferencees() == 1) ) {
+      System.out.println( "\n  fm="+fm+"\n  param="+paramTemp1 );
+      writeGraph( "whatup" );
+    }
+
+
+    assert paramVar1.getNumReferencees() == 1;
+    RefEdge paramEdge1 = paramVar1.iteratorToReferencees().next();
+    HeapRegionNode hrnParam1 = paramEdge1.getDst();
+
+    TempDescriptor paramTemp2 = fm.getParameter(paramIndex2.intValue());
+    assert this.hasVariable( paramTemp2 );
+    VariableNode paramVar2 = getVariableNodeFromTemp(paramTemp2);
+
+    if( !(paramVar2.getNumReferencees() == 1) ) {
+      System.out.println( "\n  fm="+fm+"\n  param="+paramTemp2 );
+      writeGraph( "whatup" );
+    }
+
+    assert paramVar2.getNumReferencees() == 1;
+    RefEdge paramEdge2 = paramVar2.iteratorToReferencees().next();
+    HeapRegionNode hrnParam2 = paramEdge2.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());
+    assert this.hasVariable( paramTemp );
+    VariableNode paramVar = getVariableNodeFromTemp(paramTemp);
+    assert paramVar.getNumReferencees() == 1;
+    RefEdge paramEdge = paramVar.iteratorToReferencees().next();
+    HeapRegionNode hrnParam = paramEdge.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 && hrnSum1!=hrnSum2){
+      common.addAll(mayReachSharedObjects(hrnSum1, hrnSum2));
+    }
+
+    if(hrnSum1!=null){
+      // ask if objects from this summary share among each other
+      common.addAll(mayReachSharedObjects(hrnSum1));
+    }
+
+    // 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));
+      }
+
+      // also ask if objects from this summary share among each other
+      common.addAll(mayReachSharedObjects(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;
+  }  
 }