Not the most elegant fix, but out-of-context nodes can be uniquely identified by...

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index c3480b74da4f146abf60d9f8f9dca5f481dcc40c..9c838529793d1ede550eab976735b41edd2a1f4e 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -1503,19 +1503,52 @@ public class ReachGraph {
           // we found a reference that crosses from out-of-context
           // to in-context, so build a special out-of-context node
           // for the callee IHM and its reference edge
-          HeapRegionNode hrnCalleeAndOutContext =
-            rg.createNewHeapRegionNode( null,  // ID
-                                        false, // single object?
-                                        false, // new summary?
-                                        false, // flagged?
-                                        true,  // out-of-context?
-                                        oocNodeType,
-                                        null,  // alloc site, shouldn't be used
-                                        /*toShadowTokens( this,*/ oocReach  /*)*/, // inherent
-                                        /*toShadowTokens( this,*/ oocReach /*)*/, // alpha
-                                        predsEmpty,
-                                        "out-of-context"
-                                        );       
+          
+          // for consistency, map one out-of-context "identifier"
+          // to one heap region node id, otherwise no convergence
+          String oocid = "oocid"+
+            hrnCalleeAndInContext.getIDString()+
+            oocNodeType+
+            edgeMightCross.getType()+
+            edgeMightCross.getField();
+          
+          Integer oocHrnID = oocid2hrnid.get( oocid );
+
+          HeapRegionNode hrnCalleeAndOutContext;
+
+          if( oocHrnID == null ) {
+
+            hrnCalleeAndOutContext =
+              rg.createNewHeapRegionNode( null,  // ID
+                                          false, // single object?
+                                          false, // new summary?
+                                          false, // flagged?
+                                          true,  // out-of-context?
+                                          oocNodeType,
+                                          null,  // alloc site, shouldn't be used
+                                          /*toShadowTokens( this,*/ oocReach  /*)*/, // inherent
+                                          /*toShadowTokens( this,*/ oocReach /*)*/, // alpha
+                                          predsEmpty,
+                                          "out-of-context"
+                                          );       
+
+            oocid2hrnid.put( oocid, hrnCalleeAndOutContext.getID() );
+
+          } else {
+            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
+                                          /*toShadowTokens( this,*/ oocReach  /*)*/, // inherent
+                                          /*toShadowTokens( this,*/ oocReach /*)*/, // alpha
+                                          predsEmpty,
+                                          "out-of-context"
+                                          );       
+          }
 
           rg.addRefEdge( hrnCalleeAndOutContext,
                          hrnCalleeAndInContext,
@@ -1547,6 +1580,9 @@ public class ReachGraph {
     return rg;
   }  
 
+  private static Hashtable<String, Integer> oocid2hrnid = 
+    new Hashtable<String, Integer>();
+
 
 
   public void