improved debug graph capture
[IRC.git] / Robust / src / Analysis / Disjoint / ReachGraph.java
index aea243daafe62530823018e75f5a46e687160210..9adbdad45f44a89554b5a4ba24adb7aacd4462ef 100644 (file)
@@ -139,10 +139,7 @@ public class ReachGraph {
       alpha = inherent;
     }
 
-    if( preds == null ) {
-      // TODO: do this right?  For out-of-context nodes?
-      preds = ExistPredSet.factory();
-    }
+    assert preds != null;
     
     HeapRegionNode hrn = new HeapRegionNode( id,
                                             isSingleObject,
@@ -293,6 +290,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 +448,8 @@ public class ReachGraph {
                                        Canonical.intersection( betaY, betaHrn ),
                                        predsTrue
                                        );
-       
-       addRefEdge( lnX, hrnHrn, edgeNew );
+
+        addEdgeOrMergeWithExisting( edgeNew );
       }
     }
 
@@ -567,27 +600,7 @@ public class ReachGraph {
                                        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.unionORpreds( edgeExisting.getBeta(),
-                                                edgeNew.getBeta()
-                                                )
-                               );
-          edgeExisting.setPreds(
-                                Canonical.join( edgeExisting.getPreds(),
-                                                edgeNew.getPreds()
-                                                )
-                                );
-       
-        } else {                         
-         addRefEdge( hrnX, hrnY, edgeNew );
-       }
+        addEdgeOrMergeWithExisting( edgeNew );
       }
     }
 
@@ -779,9 +792,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 +837,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?                  
@@ -1284,15 +1291,9 @@ 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( Set<ReachTuple> oocTuples,
-                                      ReachSet        rs,
-                                      Integer         hrnID,
-                                      TempDescriptor  tdSrc,
-                                      Integer         hrnSrcID,
-                                      Integer         hrnDstID,
-                                      TypeDescriptor  type,
-                                      String          field,
-                                      boolean         outOfContext
+  protected ReachSet toCalleeContext( ReachSet      rs,
+                                      ExistPredSet  preds,
+                                      Set<HrnIdOoc> oocHrnIdOoc2callee
                                       ) {
     ReachSet out = ReachSet.factory();
    
@@ -1311,8 +1312,12 @@ public class ReachGraph {
         while( rtItr.hasNext() ) {
           ReachTuple rt = rtItr.next();
 
-          // only translate this tuple if it is in the out-context bag
-          if( !oocTuples.contains( rt ) ) {
+          // 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;
           }
@@ -1369,34 +1374,8 @@ public class ReachGraph {
         
         stateCallee = stateNew;
       }
-
-
-      ExistPredSet preds;
-
-      if( outOfContext ) {
-        preds = predsEmpty;
-      } else {
-        ExistPred pred;
-        if( hrnID != null ) {
-          assert tdSrc    == null;
-          assert hrnSrcID == null;
-          assert hrnDstID == null;
-          pred = ExistPred.factory( hrnID, 
-                                    stateCaller );
-        } else {
-          assert tdSrc != null || hrnSrcID != null;
-          assert hrnDstID != null;
-          pred = ExistPred.factory( tdSrc,
-                                    hrnSrcID,
-                                    hrnDstID,
-                                    type,
-                                    field,
-                                    stateCaller,
-                                    false );
-        }
-        preds = ExistPredSet.factory( pred );
-      }
       
+      // attach the passed in preds
       stateCallee = Canonical.attach( stateCallee,
                                       preds );
 
@@ -1444,10 +1423,10 @@ public class ReachGraph {
                                           calleeStatesSatisfied.get( stateCallee )
                                           );        
           out = Canonical.add( out,
-                                 stateCaller
-                                 );
+                               stateCaller
+                               );
         }
-      }
+      } 
     }    
 
     assert out.isCanonical();
@@ -1542,9 +1521,10 @@ public class ReachGraph {
     } // end iterating over parameters as starting points
 
 
-    // now collect out-of-context reach tuples and 
-    // more out-of-context edges
-    Set<ReachTuple> oocTuples = new HashSet<ReachTuple>();
+    // 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();
@@ -1591,13 +1571,15 @@ public class ReachGraph {
           while( rtItr.hasNext() ) {
             ReachTuple rt = rtItr.next();
 
-            oocTuples.add( rt );
+            oocHrnIdOoc2callee.add( new HrnIdOoc( rt.getHrnID(),
+                                                  rt.isOutOfContext()
+                                                  )
+                                    );
           }
         }
       }
     }
 
-
     // the callee view is a new graph: DON'T MODIFY *THIS* graph
     ReachGraph rg = new ReachGraph();
 
@@ -1619,16 +1601,14 @@ public class ReachGraph {
                                   false, // out-of-context?
                                   hrnCaller.getType(),
                                   hrnCaller.getAllocSite(),
-                                  toCalleeContext( oocTuples,
-                                                   hrnCaller.getInherent(),      // in state
-                                                   hrnCaller.getID(),            // node pred
-                                                   null, null, null, null, null, // edge pred
-                                                   false ),                      // ooc pred
-                                  toCalleeContext( oocTuples,
-                                                   hrnCaller.getAlpha(),         // in state
-                                                   hrnCaller.getID(),            // node pred
-                                                   null, null, null, null, null, // edge pred
-                                                   false ),                      // ooc pred
+                                  toCalleeContext( hrnCaller.getInherent(),
+                                                   preds,
+                                                   oocHrnIdOoc2callee 
+                                                   ),
+                                  toCalleeContext( hrnCaller.getAlpha(),
+                                                   preds,
+                                                   oocHrnIdOoc2callee 
+                                                   ),
                                   preds,
                                   hrnCaller.getDescription()
                                   );
@@ -1658,7 +1638,9 @@ public class ReachGraph {
                            reArg.getType(),
                            reArg.getField(),
                            null,
-                           false ); // out-of-context
+                           true,  // out-of-callee-context
+                           false  // out-of-caller-context
+                           );
       
       ExistPredSet preds = 
         ExistPredSet.factory( pred );
@@ -1668,15 +1650,10 @@ public class ReachGraph {
                      hrnDstCallee,
                      reArg.getType(),
                      reArg.getField(),
-                     toCalleeContext( oocTuples,
-                                      reArg.getBeta(),      // in state
-                                      null,                 // node pred
-                                      arg,                  // edge pred
-                                      null,                 // edge pred
-                                      hrnDstCallee.getID(), // edge pred
-                                      reArg.getType(),      // edge pred
-                                      reArg.getField(),     // edge pred
-                                      false ),              // ooc pred
+                     toCalleeContext( reArg.getBeta(),
+                                      preds,
+                                      oocHrnIdOoc2callee
+                                      ),
                      preds
                      );
       
@@ -1707,7 +1684,9 @@ public class ReachGraph {
                            reCaller.getType(),
                            reCaller.getField(),
                            null,
-                           false ); // out-of-context
+                           false, // out-of-callee-context
+                           false  // out-of-caller-context
+                           );
       
       ExistPredSet preds = 
         ExistPredSet.factory( pred );
@@ -1717,15 +1696,10 @@ public class ReachGraph {
                      hrnDstCallee,
                      reCaller.getType(),
                      reCaller.getField(),
-                     toCalleeContext( oocTuples,
-                                      reCaller.getBeta(),   // in state
-                                      null,                 // node pred
-                                      null,                 // edge pred
-                                      hrnSrcCallee.getID(), // edge pred
-                                      hrnDstCallee.getID(), // edge pred
-                                      reCaller.getType(),   // edge pred
-                                      reCaller.getField(),  // edge pred
-                                      false ),              // ooc pred
+                     toCalleeContext( reCaller.getBeta(),
+                                      preds,
+                                      oocHrnIdOoc2callee 
+                                      ),
                      preds
                      );
       
@@ -1748,19 +1722,30 @@ public class ReachGraph {
       ReachSet       oocReach;
       TempDescriptor oocPredSrcTemp = null;
       Integer        oocPredSrcID   = null;
+      boolean        outOfCalleeContext;
+      boolean        outOfCallerContext;
 
       if( rsnCaller instanceof VariableNode ) {
         VariableNode vnCaller = (VariableNode) rsnCaller;
         oocNodeType    = null;
         oocReach       = rsetEmpty;
         oocPredSrcTemp = vnCaller.getTempDescriptor();
+        outOfCalleeContext = true;
+        outOfCallerContext = false;
 
       } else {
         HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller;
         assert !callerNodeIDsCopiedToCallee.contains( hrnSrcCaller.getID() );
         oocNodeType  = hrnSrcCaller.getType();
         oocReach     = hrnSrcCaller.getAlpha(); 
-        oocPredSrcID = hrnSrcCaller.getID();        
+        oocPredSrcID = hrnSrcCaller.getID();
+        if( hrnSrcCaller.isOutOfContext() ) {
+          outOfCalleeContext = false;
+          outOfCallerContext = true;
+        } else {
+          outOfCalleeContext = true;
+          outOfCallerContext = false;
+        }
       }
 
       ExistPred pred =
@@ -1770,7 +1755,9 @@ public class ReachGraph {
                            reCaller.getType(),
                            reCaller.getField(),
                            null,
-                           true ); // out-of-context
+                           outOfCalleeContext,
+                           outOfCallerContext
+                           );
 
       ExistPredSet preds = 
         ExistPredSet.factory( pred );
@@ -1806,18 +1793,14 @@ public class ReachGraph {
                                         true,  // out-of-context?
                                         oocNodeType,
                                         null,  // alloc site, shouldn't be used
-                                        toCalleeContext( oocTuples, 
-                                                         oocReach,                     // in state
-                                                         null,                         // node pred
-                                                         null, null, null, null, null, // edge pred
-                                                         true                          // ooc pred
-                                                         ), // inherent
-                                        toCalleeContext( oocTuples,
-                                                         oocReach,                     // in state
-                                                         null,                         // node pred
-                                                         null, null, null, null, null, // edge pred
-                                                         true                          // ooc pred
-                                                         ), // alpha
+                                        toCalleeContext( oocReach,               
+                                                         preds,
+                                                         oocHrnIdOoc2callee
+                                                         ),
+                                        toCalleeContext( oocReach,
+                                                         preds,
+                                                         oocHrnIdOoc2callee
+                                                         ),
                                         preds,
                                         "out-of-context"
                                         );       
@@ -1839,39 +1822,41 @@ public class ReachGraph {
                                           true,  // out-of-context?
                                           oocNodeType,
                                           null,  // alloc site, shouldn't be used
-                                          toCalleeContext( oocTuples,
-                                                           oocReach,                     // in state
-                                                           null,                         // node pred
-                                                           null, null, null, null, null, // edge pred
-                                                           true                          // ooc pred
-                                                           ), // inherent
-                                          toCalleeContext( oocTuples,
-                                                           oocReach,                     // in state
-                                                           null,                         // node pred
-                                                           null, null, null, null, null, // edge pred
-                                                           true                          // ooc pred
-                                                           ), // alpha
+                                          toCalleeContext( oocReach,
+                                                           preds,
+                                                           oocHrnIdOoc2callee
+                                                           ),
+                                          toCalleeContext( oocReach,
+                                                           preds,
+                                                           oocHrnIdOoc2callee
+                                                           ),
                                           preds,
                                           "out-of-context"
                                           );       
+
+          } else {
+            // otherwise it is there, so merge reachability
+            hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
+                                                                     toCalleeContext( oocReach,
+                                                                                      preds,
+                                                                                      oocHrnIdOoc2callee
+                                                                                      )
+                                                                     )
+                                             );
           }
         }
 
+        assert hrnCalleeAndOutContext.reachHasOnlyOOC();
+
         rg.addRefEdge( hrnCalleeAndOutContext,
                        hrnDstCallee,
                        new RefEdge( hrnCalleeAndOutContext,
                                     hrnDstCallee,
                                     reCaller.getType(),
                                     reCaller.getField(),
-                                    toCalleeContext( oocTuples,
-                                                     reCaller.getBeta(),   // in state
-                                                     null,                 // node pred
-                                                     oocPredSrcTemp,       // edge pred
-                                                     oocPredSrcID,         // edge pred
-                                                     hrnDstCaller.getID(), // edge pred
-                                                     reCaller.getType(),   // edge pred
-                                                     reCaller.getField(),  // edge pred
-                                                     false                 // ooc pred
+                                    toCalleeContext( reCaller.getBeta(),
+                                                     preds,
+                                                     oocHrnIdOoc2callee
                                                      ),
                                     preds
                                     )
@@ -1880,37 +1865,40 @@ public class ReachGraph {
         } else {
         // the out-of-context edge already exists
         oocEdgeExisting.setBeta( Canonical.unionORpreds( oocEdgeExisting.getBeta(),
-                                                  toCalleeContext( oocTuples,
-                                                                   reCaller.getBeta(),   // in state
-                                                                   null,                 // node pred
-                                                                   oocPredSrcTemp,       // edge pred
-                                                                   oocPredSrcID,         // edge pred
-                                                                   hrnDstCaller.getID(), // edge pred
-                                                                   reCaller.getType(),   // edge pred
-                                                                   reCaller.getField(),  // edge pred
-                                                                   false                 // ooc pred
-                                                                   )
+                                                         toCalleeContext( reCaller.getBeta(),
+                                                                          preds,
+                                                                          oocHrnIdOoc2callee
+                                                                          )
                                                   )
                                  );         
           
         oocEdgeExisting.setPreds( Canonical.join( oocEdgeExisting.getPreds(),
-                                                  reCaller.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", 
-                       resolveMethodDebugDOTwriteLabels,    
-                       resolveMethodDebugDOTselectTemps,    
-                       resolveMethodDebugDOTpruneGarbage,   
-                       resolveMethodDebugDOThideSubsetReach,
-                       resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      rg.writeGraph( "calleeview", 
+                     resolveMethodDebugDOTwriteLabels,    
+                     resolveMethodDebugDOTselectTemps,    
+                     resolveMethodDebugDOTpruneGarbage,   
+                     resolveMethodDebugDOThideSubsetReach,
+                     resolveMethodDebugDOThideEdgeTaints );      
     }
 
     return rg;
@@ -1927,7 +1915,9 @@ public class ReachGraph {
   private static boolean resolveMethodDebugDOThideSubsetReach = false;
   private static boolean resolveMethodDebugDOThideEdgeTaints  = true;
 
-
+  static String debugGraphPrefix;
+  static int debugCallSiteVisitsUntilExit = 0;
+  
 
   public void 
     resolveMethodCall( FlatCall     fc,        
@@ -1937,24 +1927,23 @@ public class ReachGraph {
                        boolean      writeDebugDOTs
                        ) {
 
-
     if( writeDebugDOTs ) {
-      try {
-        rgCallee.writeGraph( "callee", 
-                       resolveMethodDebugDOTwriteLabels,    
-                       resolveMethodDebugDOTselectTemps,    
-                       resolveMethodDebugDOTpruneGarbage,   
-                       resolveMethodDebugDOThideSubsetReach,
-                       resolveMethodDebugDOThideEdgeTaints );
-
-        writeGraph( "caller00In",  
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints,
-                    callerNodeIDsCopiedToCallee );
-      } catch( IOException e ) {}
+      debugGraphPrefix = String.format( "call%02d", debugCallSiteVisitsUntilExit );
+      
+      rgCallee.writeGraph( debugGraphPrefix+"callee", 
+                           resolveMethodDebugDOTwriteLabels,    
+                           resolveMethodDebugDOTselectTemps,    
+                           resolveMethodDebugDOTpruneGarbage,   
+                           resolveMethodDebugDOThideSubsetReach,
+                           resolveMethodDebugDOThideEdgeTaints );
+      
+      writeGraph( debugGraphPrefix+"caller00In",  
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints,
+                  callerNodeIDsCopiedToCallee );
     }
 
 
@@ -1971,7 +1960,6 @@ public class ReachGraph {
     // 5. Global sweep it.
 
 
-
     // 1. mark what callee elements have satisfied predicates
     Hashtable<HeapRegionNode, ExistPredSet> calleeNodesSatisfied =
       new Hashtable<HeapRegionNode, ExistPredSet>();
@@ -1999,6 +1987,7 @@ public class ReachGraph {
         hrnCallee.getPreds().isSatisfiedBy( this,
                                             callerNodeIDsCopiedToCallee
                                             );
+
       if( predsIfSatis != null ) {
         calleeNodesSatisfied.put( hrnCallee, predsIfSatis );
       } else {
@@ -2047,9 +2036,15 @@ public class ReachGraph {
         if( hrnSrcCallee.isOutOfContext() ) {          
 
           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
@@ -2063,6 +2058,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;
@@ -2100,6 +2096,7 @@ public class ReachGraph {
           reCallee.getPreds().isSatisfiedBy( this,
                                              callerNodeIDsCopiedToCallee
                                              );
+
         if( predsIfSatis != null ) {
           calleeEdgesSatisfied.put( reCallee, predsIfSatis );
 
@@ -2117,9 +2114,7 @@ public class ReachGraph {
               calleeStatesSatisfied.put( stateCallee, predsIfSatis );
             } 
           }
-
         }        
-
       }
     }
 
@@ -2127,8 +2122,14 @@ public class ReachGraph {
     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 );
+      TempDescriptor tdParam = fmCallee.getParameter( i );
+
+      if( !DisjointAnalysis.shouldAnalysisTrack( tdParam.getType() ) ) {
+        // skip primitive/immutable parameters
+        continue;
+      }
+
+      VariableNode vnCallee = rgCallee.getVariableNodeFromTemp( tdParam );
 
       Iterator<RefEdge> reItr = vnCallee.iteratorToReferencees();
       while( reItr.hasNext() ) {
@@ -2172,14 +2173,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller20BeforeWipe", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller20BeforeWipe", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -2198,14 +2197,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller30BeforeAddingNodes", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller30BeforeAddingNodes", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -2267,14 +2264,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller31BeforeAddingEdges", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller31BeforeAddingEdges", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -2314,7 +2309,6 @@ public class ReachGraph {
       Set<RefSrcNode> oocCallers = 
         calleeEdges2oocCallerSrcMatches.get( reCallee );
 
-      boolean oocEdges = false;
       
       if( oocCallers == null ) {
         // there are no out-of-context matches, so it's
@@ -2332,8 +2326,8 @@ public class ReachGraph {
             // shouldn't this NEVER HAPPEN?
             assert false;
           }
+
           rsnCallers.add( this.getVariableNodeFromTemp( tdArg ) );
-          oocEdges = true;
 
         } else {
           // otherwise source is in context, one region
@@ -2375,7 +2369,6 @@ public class ReachGraph {
         // that should NOT be translated to shadow nodes
         assert !oocCallers.isEmpty();
         rsnCallers.addAll( oocCallers );
-        oocEdges = true;
       }
 
       // now make all caller edges we've identified from
@@ -2421,6 +2414,7 @@ public class ReachGraph {
           }
         }
         
+
         // look to see if an edge with same field exists
         // and merge with it, otherwise just add the edge
         RefEdge edgeExisting = rsnCaller.getReferenceTo( hrnDstCaller,
@@ -2441,11 +2435,14 @@ public class ReachGraph {
 
           // for reach propagation
           if( !cs.isEmpty() ) {
-            edgePlannedChanges.put( 
-                                   edgeExisting, 
-                                   Canonical.union( edgePlannedChanges.get( edgeExisting ),
-                                                    cs
-                                                    ) 
+            ChangeSet csExisting = edgePlannedChanges.get( edgeExisting );
+            if( csExisting == null ) {
+              csExisting = ChangeSet.factory();
+            }
+            edgePlannedChanges.put( edgeExisting, 
+                                    Canonical.union( csExisting,
+                                                     cs
+                                                     ) 
                                     );
           }
           
@@ -2467,14 +2464,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller35BeforeAssignReturnValue", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller35BeforeAssignReturnValue", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -2485,7 +2480,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 );
@@ -2527,8 +2524,6 @@ public class ReachGraph {
                                      predsTrue,                     // predicates
                                      hrnDstCallee.getDescription()  // description
                                      );                                        
-        } else {
-          assert hrnDstCaller.isWiped();
         }
 
         TypeDescriptor tdNewEdge =
@@ -2553,14 +2548,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller38propagateReach", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller38propagateReach", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
     // propagate callee reachability changes to the rest
@@ -2583,14 +2576,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller40BeforeShadowMerge", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller40BeforeShadowMerge", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
     
 
@@ -2684,14 +2675,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller45BeforeUnshadow", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller45BeforeUnshadow", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
     
     
@@ -2712,14 +2701,12 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller50BeforeGlobalSweep", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller50BeforeGlobalSweep", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
     }
 
 
@@ -2731,14 +2718,18 @@ public class ReachGraph {
 
 
     if( writeDebugDOTs ) {
-      try {
-        writeGraph( "caller90AfterTransfer", 
-                    resolveMethodDebugDOTwriteLabels,    
-                    resolveMethodDebugDOTselectTemps,    
-                    resolveMethodDebugDOTpruneGarbage,   
-                    resolveMethodDebugDOThideSubsetReach,
-                    resolveMethodDebugDOThideEdgeTaints );
-      } catch( IOException e ) {}
+      writeGraph( debugGraphPrefix+"caller90AfterTransfer", 
+                  resolveMethodDebugDOTwriteLabels,    
+                  resolveMethodDebugDOTselectTemps,    
+                  resolveMethodDebugDOTpruneGarbage,   
+                  resolveMethodDebugDOThideSubsetReach,
+                  resolveMethodDebugDOThideEdgeTaints );
+
+      --debugCallSiteVisitsUntilExit;
+      if( debugCallSiteVisitsUntilExit <= 0 ) {
+        System.out.println( "!!! Exiting after requested visits to call site. !!!" );
+        System.exit( 0 );
+      }
     }
   } 
 
@@ -2901,10 +2892,13 @@ public class ReachGraph {
        assert rsetEmpty.equals( edge.getBetaNew() );
       }      
 
-      // calculate boldB for this flagged node, or out-of-context node
+      // make a mapping of IDs to heap regions they propagate from
       if( hrn.isFlagged() ) {
         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 );
@@ -2913,6 +2907,13 @@ public class ReachGraph {
       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();
@@ -3089,6 +3090,14 @@ public class ReachGraph {
             if( rtOld.isOutOfContext() ) {
               B = boldBooc.get( rtOld.getHrnID() ); 
             } else {
+
+
+              if( !id2hrn.containsKey( rtOld.getHrnID() ) ) {
+                System.out.println( "\nLooking for "+rtOld );
+                writeGraph( "dbgz" );
+              }
+
+
               assert id2hrn.containsKey( rtOld.getHrnID() );
               B = boldBic.get( rtOld.getHrnID() ); 
             }
@@ -3096,7 +3105,8 @@ public class ReachGraph {
             if( B != null ) {            
               ReachSet boldB_rtOld_incident = B.get( incidentEdge );
               if( boldB_rtOld_incident != null &&
-                  boldB_rtOld_incident.contains( stateOld ) ) {
+                  boldB_rtOld_incident.containsIgnorePreds( stateOld ) != null
+                  ) {
                 foundState = true;
               }
             }
@@ -3179,7 +3189,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() );
@@ -3475,6 +3494,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
@@ -3488,18 +3511,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;
     }
 
@@ -3546,7 +3581,6 @@ public class ReachGraph {
     
     return true;
   }
-  
 
   protected boolean areVariableNodesEqual( ReachGraph rg ) {
 
@@ -3815,13 +3849,25 @@ 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 hideSubsetReachability,
                           boolean hideEdgeTaints
-                          ) throws java.io.IOException {
+                          ) {
     writeGraph( graphName,
                 writeLabels,
                 labelSelect,
@@ -3838,94 +3884,57 @@ public class ReachGraph {
                           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]", "" );
 
-    // this is an optional step to form the callee-reachable
-    // "cut-out" into a DOT cluster for visualization
-    if( callerNodeIDsCopiedToCallee != null ) {
+      BufferedWriter bw = 
+        new BufferedWriter( new FileWriter( graphName+".dot" ) );
 
-      bw.write( "  subgraph cluster0 {\n" );
-      bw.write( "    color=blue;\n" );
+      bw.write( "digraph "+graphName+" {\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.isOutOfContext()
-          ) {
-
-       if( !visited.contains( hrn ) ) {
-         traverseHeapRegionNodes( hrn,
-                                   bw,
-                                   null,
-                                   visited,
-                                   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( !visited.contains( hrn ) ) {
             traverseHeapRegionNodes( hrn,
@@ -3936,17 +3945,59 @@ public class ReachGraph {
                                      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,
@@ -4019,272 +4070,347 @@ public class ReachGraph {
     }
   }  
   
-       public Set<HeapRegionNode> findCommonReachableNodes(HeapRegionNode hrn1,
-                       HeapRegionNode hrn2) {
 
-               Set<HeapRegionNode> reachableNodes1 = new HashSet<HeapRegionNode>();
-               Set<HeapRegionNode> reachableNodes2 = new HashSet<HeapRegionNode>();
 
-               Set<HeapRegionNode> todoNodes1 = new HashSet<HeapRegionNode>();
-               todoNodes1.add(hrn1);
 
-               Set<HeapRegionNode> todoNodes2 = new HashSet<HeapRegionNode>();
-               todoNodes2.add(hrn2);
 
-               // follow links until all reachable nodes have been found
-               while (!todoNodes1.isEmpty()) {
-                       HeapRegionNode hrn = todoNodes1.iterator().next();
-                       todoNodes1.remove(hrn);
-                       reachableNodes1.add(hrn);
+  public Set<HeapRegionNode> findCommonReachableNodes( ReachSet proofOfSharing ) {
 
-                       Iterator<RefEdge> edgeItr = hrn.iteratorToReferencees();
-                       while (edgeItr.hasNext()) {
-                               RefEdge edge = edgeItr.next();
+    Set<HeapRegionNode> exhibitProofState =
+      new HashSet<HeapRegionNode>();
 
-                               if (!reachableNodes1.contains(edge.getDst())) {
-                                       todoNodes1.add(edge.getDst());
-                               }
-                       }
-               }
+    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;
+  }
 
-               while (!todoNodes2.isEmpty()) {
-                       HeapRegionNode hrn = todoNodes2.iterator().next();
-                       todoNodes2.remove(hrn);
-                       reachableNodes2.add(hrn);
+        
+  public Set<HeapRegionNode> mayReachSharedObjects(HeapRegionNode hrn1,
+                                                   HeapRegionNode hrn2) {
+    assert hrn1 != null;
+    assert hrn2 != null;
 
-                       Iterator<RefEdge> edgeItr = hrn.iteratorToReferencees();
-                       while (edgeItr.hasNext()) {
-                               RefEdge edge = edgeItr.next();
+    assert !hrn1.isOutOfContext();
+    assert !hrn2.isOutOfContext();
 
-                               if (!reachableNodes2.contains(edge.getDst())) {
-                                       todoNodes2.add(edge.getDst());
-                               }
-                       }
-               }
+    assert belongsToThis( hrn1 );
+    assert belongsToThis( hrn2 );
 
-               Set<HeapRegionNode> intersection =
-                  new HashSet<HeapRegionNode>( reachableNodes1 );
+    assert !hrn1.getID().equals( hrn2.getID() );
 
-               intersection.retainAll( reachableNodes2 );
 
-               return intersection;
-       }
+    // 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 );
+    }
 
-       public Set<HeapRegionNode> mayReachSharedObjects(HeapRegionNode hrn1,
-                       HeapRegionNode hrn2) {
-               assert hrn1 != null;
-               assert hrn2 != null;
-
-               // then get the various tokens for these heap regions
-               ReachTuple h1 = ReachTuple.factory(hrn1.getID(),
-                               !hrn1.isSingleObject(), ReachTuple.ARITY_ONE, false);
-
-               ReachTuple h1plus = ReachTuple.factory(hrn1.getID(), !hrn1
-                               .isSingleObject(), ReachTuple.ARITY_ONEORMORE, false);
-
-               ReachTuple h1star = ReachTuple.factory(hrn1.getID(), !hrn1
-                               .isSingleObject(), ReachTuple.ARITY_ZEROORMORE, false);
-
-               ReachTuple h2 = ReachTuple.factory(hrn2.getID(),
-                               !hrn2.isSingleObject(), ReachTuple.ARITY_ONE, false);
-
-               ReachTuple h2plus = ReachTuple.factory(hrn2.getID(), !hrn2
-                               .isSingleObject(), ReachTuple.ARITY_ONEORMORE, false);
-
-               ReachTuple 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());
-               }
-
-               boolean aliasDetected = false;
-
-               // only do this one if they are different tokens
-               if (h1 != h2 && beta1.containsStateWithBoth(h1, h2)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1plus, h2)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1star, h2)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1, h2plus)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1plus, h2plus)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1star, h2plus)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1, h2star)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1plus, h2star)) {
-                       aliasDetected = true;
-               }
-               if (beta1.containsStateWithBoth(h1star, h2star)) {
-                       aliasDetected = true;
-               }
-
-               if (h1 != h2 && beta2.containsStateWithBoth(h1, h2)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1plus, h2)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1star, h2)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1, h2plus)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1plus, h2plus)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1star, h2plus)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1, h2star)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1plus, h2star)) {
-                       aliasDetected = true;
-               }
-               if (beta2.containsStateWithBoth(h1star, h2star)) {
-                       aliasDetected = true;
-               }
-
-               Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
-               if (aliasDetected) {
-                       common = findCommonReachableNodes(hrn1, hrn2);
-                       if (!(DISABLE_STRONG_UPDATES || DISABLE_GLOBAL_SWEEP)) {
-                               assert !common.isEmpty();
-                       }
-               }
-
-               return common;
-       }
+    // then get the merged beta of all out-going edges from these heap
+    // regions
 
-       public Set<HeapRegionNode> mayReachSharedObjects(FlatMethod fm,
-                       Integer paramIndex1, Integer paramIndex2) {
+    ReachSet beta1 = ReachSet.factory();
+    Iterator<RefEdge> itrEdge = hrn1.iteratorToReferencees();
+    while (itrEdge.hasNext()) {
+      RefEdge edge = itrEdge.next();
+      beta1 = Canonical.unionORpreds(beta1, edge.getBeta());
+    }
 
-               // get parameter's heap regions
-               TempDescriptor paramTemp1 = fm.getParameter(paramIndex1.intValue());
-               VariableNode argVar1 = getVariableNodeFromTemp(paramTemp1);
-               RefEdge argEdge1 = argVar1.iteratorToReferencees().next();
-               HeapRegionNode hrnParam1 = argEdge1.getDst();
+    ReachSet beta2 = ReachSet.factory();
+    itrEdge = hrn2.iteratorToReferencees();
+    while (itrEdge.hasNext()) {
+      RefEdge edge = itrEdge.next();
+      beta2 = Canonical.unionORpreds(beta2, edge.getBeta());
+    }
 
-               TempDescriptor paramTemp2 = fm.getParameter(paramIndex2.intValue());
-               VariableNode argVar2 = getVariableNodeFromTemp(paramTemp2);
-               RefEdge argEdge2 = argVar2.iteratorToReferencees().next();
-               HeapRegionNode hrnParam2 = argEdge2.getDst();
+    ReachSet proofOfSharing = ReachSet.factory();
 
-               Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
-               common.addAll(mayReachSharedObjects(hrnParam1, hrnParam2));
+    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 )
+                                );      
+    }
 
-               return common;
-       }
+    if( !hrn2.isSingleObject() ) {    
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta1.getStatesWithBoth( h1, h2star )
+                                );
+      proofOfSharing = 
+        Canonical.unionORpreds( proofOfSharing,
+                                beta2.getStatesWithBoth( h1, h2star )
+                                );
+    }
 
-       public Set<HeapRegionNode> mayReachSharedObjects(FlatMethod fm,
-                       Integer paramIndex, AllocSite as) {
+    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();
+      }
+    }
 
-               // get parameter's heap regions
-               TempDescriptor paramTemp = fm.getParameter(paramIndex.intValue());
-               VariableNode argVar = getVariableNodeFromTemp(paramTemp);
-               RefEdge argEdge = argVar.iteratorToReferencees().next();
-               HeapRegionNode hrnParam = argEdge.getDst();
+    return common;
+  }
 
-               // get summary node
-               assert id2hrn.containsKey(as.getSummary());
-               HeapRegionNode hrnSummary = id2hrn.get(as.getSummary());
-               assert hrnSummary != null;
+  // 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 );
 
-               Set<HeapRegionNode> common = mayReachSharedObjects(hrnParam, hrnSummary);
+    ReachTuple hstar =  
+      ReachTuple.factory( hrn.getID(), 
+                          true,    // multi
+                          ReachTuple.ARITY_ZEROORMORE,
+                          false ); // ooc    
 
-               // check for other nodes
-               for (int i = 0; i < as.getAllocationDepth(); ++i) {
+    // then get the merged beta of all out-going edges from 
+    // this heap region
 
-                       assert id2hrn.containsKey(as.getIthOldest(i));
-                       HeapRegionNode hrnIthOldest = id2hrn.get(as.getIthOldest(i));
-                       assert hrnIthOldest != null;
+    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();
 
-                       common = mayReachSharedObjects(hrnParam, hrnIthOldest);
+    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;
+  }
 
-               }
 
-               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);
+
 
-       public Set<HeapRegionNode> mayReachSharedObjects(AllocSite as1,
-                       AllocSite as2) {
+    if( !(paramVar1.getNumReferencees() == 1) ) {
+      System.out.println( "\n  fm="+fm+"\n  param="+paramTemp1 );
+      writeGraph( "whatup" );
+    }
 
-               // get summary node 1's alpha
-               Integer idSum1 = as1.getSummary();
-               assert id2hrn.containsKey(idSum1);
-               HeapRegionNode hrnSum1 = id2hrn.get(idSum1);
-               assert hrnSum1 != null;
 
-               // get summary node 2's alpha
-               Integer idSum2 = as2.getSummary();
-               assert id2hrn.containsKey(idSum2);
-               HeapRegionNode hrnSum2 = id2hrn.get(idSum2);
-               assert hrnSum2 != null;
+    assert paramVar1.getNumReferencees() == 1;
+    RefEdge paramEdge1 = paramVar1.iteratorToReferencees().next();
+    HeapRegionNode hrnParam1 = paramEdge1.getDst();
 
-               Set<HeapRegionNode> common = mayReachSharedObjects(hrnSum1, hrnSum2);
+    TempDescriptor paramTemp2 = fm.getParameter(paramIndex2.intValue());
+    assert this.hasVariable( paramTemp2 );
+    VariableNode paramVar2 = getVariableNodeFromTemp(paramTemp2);
 
-               // check sum2 against alloc1 nodes
-               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;
+    if( !(paramVar2.getNumReferencees() == 1) ) {
+      System.out.println( "\n  fm="+fm+"\n  param="+paramTemp2 );
+      writeGraph( "whatup" );
+    }
 
-                       common.addAll(mayReachSharedObjects(hrnI1, hrnSum2));
-               }
+    assert paramVar2.getNumReferencees() == 1;
+    RefEdge paramEdge2 = paramVar2.iteratorToReferencees().next();
+    HeapRegionNode hrnParam2 = paramEdge2.getDst();
 
-               // 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;
+    Set<HeapRegionNode> common = new HashSet<HeapRegionNode>();
+    common.addAll(mayReachSharedObjects(hrnParam1, hrnParam2));
 
-                       common.addAll(mayReachSharedObjects(hrnSum1, hrnI2));
+    return common;
+  }
 
-                       // 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);
+  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;
+    }
 
-                               // 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;
-                               }
+    Set<HeapRegionNode> common  = new HashSet<HeapRegionNode>();
+    if(hrnSummary!=null){
+      common.addAll( mayReachSharedObjects(hrnParam, hrnSummary) );
+    }
 
-                               HeapRegionNode hrnI1 = id2hrn.get(idI1);
+    // check for other nodes
+    for (int i = 0; i < as.getAllocationDepth(); ++i) {
 
-                               common.addAll(mayReachSharedObjects(hrnI1, hrnI2));
-                       }
-               }
+      assert id2hrn.containsKey(as.getIthOldest(i));
+      HeapRegionNode hrnIthOldest = id2hrn.get(as.getIthOldest(i));
+      assert hrnIthOldest != null;
 
-               return common;
-       }
-  
+      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;
+  }  
 }