Added hooks for global sweep and made sure that strong update logic without effecting...

diff --git a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
index a4fa3272508cd3a2e0310c9eb63afa9c5e8e78d7..cd46e70888af017ae340a798f48d33044c8759c4 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
@@ -462,46 +462,45 @@ public class OwnershipGraph {
          sourceBetaForNewEdge = edgeY.getBeta();
        }
 
-       // create the actual reference edge hrnX.f -> hrnY
+       // prepare the new reference edge hrnX.f -> hrnY
        ReferenceEdge edgeNew = new ReferenceEdge(hrnX,
                                                  hrnY,
                                                  f,
                                                  false,
                                                  sourceBetaForNewEdge.pruneBy(hrnX.getAlpha() )
                                                  );
-       addReferenceEdge(hrnX, hrnY, edgeNew);
-
-       /*
-          if( f != null ) {
-           // we can do a strong update here if one of two cases holds
-           // SAVE FOR LATER, WITHOUT STILL CORRECT
-           if( (hrnX.getNumReferencers() == 1)                           ||
-               ( lnX.getNumReferencees() == 1 && hrnX.isSingleObject() )
-             ) {
-               clearReferenceEdgesFrom( hrnX, f, false );
-           }
-
-           addReferenceEdge( hrnX, hrnY, edgeNew );
 
-          } else {
-           // if the field is null, or "any" field, then
-           // look to see if an any field already exists
-           // and merge with it, otherwise just add the edge
-           ReferenceEdge edgeExisting = hrnX.getReferenceTo( hrnY, f );
+       // we can do a strong update here if one of two cases holds     
+       boolean strongUpdate = false;
+       if( f != null &&
+           (   (hrnX.getNumReferencers() == 1)                           ||
+               ( lnX.getNumReferencees() == 1 && hrnX.isSingleObject() )
+           )
+         ) {
+         strongUpdate = true;
+         //clearReferenceEdgesFrom( hrnX, f, false );
+       }
 
-           if( edgeExisting != null ) {
-               edgeExisting.setBetaNew(
-                 edgeExisting.getBetaNew().union( edgeNew.getBeta() )
-                                      );
-               // a new edge here cannot be reflexive, so existing will
-               // always be also not reflexive anymore
-               edgeExisting.setIsInitialParamReflexive( false );
+       // look to see if an edge with same field exists
+       // and merge with it, otherwise just add the edge
+       ReferenceEdge edgeExisting = hrnX.getReferenceTo( hrnY, f );
+         
+       if( edgeExisting != null ) {
+         edgeExisting.setBetaNew(
+                                 edgeExisting.getBetaNew().union( edgeNew.getBeta() )
+                                 );
+         // a new edge here cannot be reflexive, so existing will
+         // always be also not reflexive anymore
+         edgeExisting.setIsInitialParamReflexive( false );
+       } else {
+         addReferenceEdge( hrnX, hrnY, edgeNew );
+       }
 
-           } else {
-               addReferenceEdge( hrnX, hrnY, edgeNew );
-           }
-          }
-        */
+       // if it was a strong update, make sure to improve
+       // reachability with a global sweep
+       if( strongUpdate ) {
+         globalSweep();
+       }       
       }
     }
 
@@ -1501,6 +1500,10 @@ public class OwnershipGraph {
        }
       }
     }
+
+    // last thing in the entire method call is to do a global sweep
+    // and try to clean up a little bit
+    globalSweep();
   }
 
 
@@ -1798,6 +1801,20 @@ public class OwnershipGraph {
 
 
 
+  ////////////////////////////////////////////////////
+  //
+  //  This global sweep is an optional step to prune
+  //  reachability sets that are not internally
+  //  consistent with the global graph.  It should be
+  //  invoked after strong updates or method calls.
+  //
+  ////////////////////////////////////////////////////
+  protected void globalSweep() {
+    
+  }  
+
+
+
   ////////////////////////////////////////////////////
   // in merge() and equals() methods the suffix A
   // represents the passed in graph and the suffix
@@ -2239,7 +2256,6 @@ public class OwnershipGraph {
     return id2paramIndex.size() == og.id2paramIndex.size();
   }
 
-
   public boolean hasPotentialAlias(Integer paramIndex1, Integer paramIndex2) {
 
     // get parameter's heap region