def reach coming along

[IRC.git] / Robust / src / Analysis / Disjoint / ReachGraph.java

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 7a9e9f023f640389cd2eb4cf9fdaac10cc1f0589..d231593bfdbac6bfa5007405bb5e8f641464c697 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -257,11 +257,21 @@ public class ReachGraph {
     referencee.removeReferencer(edge);
   }
 
-  // return whether at least one edge was removed
+
   protected boolean clearRefEdgesFrom(RefSrcNode referencer,
                                       TypeDescriptor type,
                                       String field,
                                       boolean removeAll) {
+    return clearRefEdgesFrom( referencer, type, field, removeAll, null, null );
+  }
+
+  // return whether at least one edge was removed
+  protected boolean clearRefEdgesFrom(RefSrcNode referencer,
+                                      TypeDescriptor type,
+                                      String field,
+                                      boolean removeAll,
+                                      Set<EdgeKey> edgeKeysRemoved,
+                                      FieldDescriptor fd) {
     assert referencer != null;
 
     boolean atLeastOneEdgeRemoved = false;
@@ -279,6 +289,15 @@ public class ReachGraph {
 
         HeapRegionNode referencee = edge.getDst();
 
+        if( edgeKeysRemoved != null ) {
+          assert fd != null;
+          assert referencer instanceof HeapRegionNode;
+          edgeKeysRemoved.add( new EdgeKey( ((HeapRegionNode)referencer).getID(), 
+                                            referencee.getID(),
+                                            fd )
+                                );
+        }
+
         removeRefEdge(referencer,
                       referencee,
                       edge.getType(),
@@ -406,6 +425,8 @@ public class ReachGraph {
     assignTempXFieldFEqualToTempY( x,
                                    fdStringBytesField,
                                    tdStrLiteralBytes,
+                                   null,
+                                   null,
                                    null );
   }
 
@@ -474,7 +495,8 @@ public class ReachGraph {
   public void assignTempXEqualToTempYFieldF(TempDescriptor x,
                                             TempDescriptor y,
                                             FieldDescriptor f,
-                                            FlatNode currentProgramPoint
+                                            FlatNode currentProgramPoint,
+                                            Set<EdgeKey> edgeKeysForLoad
                                             ) {
 
     VariableNode lnX = getVariableNodeFromTemp(x);
@@ -513,6 +535,16 @@ public class ReachGraph {
           continue;
         }
 
+        // for definite reach analysis only
+        if( edgeKeysForLoad != null ) {
+          assert f != null;
+          edgeKeysForLoad.add( new EdgeKey( hrnY.getID(), 
+                                            hrnHrn.getID(),
+                                            f )
+                               );
+        }
+
+
         TypeDescriptor tdNewEdge =
           mostSpecificType(edgeHrn.getType(),
                            hrnHrn.getType()
@@ -561,7 +593,9 @@ public class ReachGraph {
   public boolean assignTempXFieldFEqualToTempY(TempDescriptor x,
                                                FieldDescriptor f,
                                                TempDescriptor y,
-                                               FlatNode currentProgramPoint
+                                               FlatNode currentProgramPoint,
+                                               Set<EdgeKey> edgeKeysRemoved,
+                                               Set<EdgeKey> edgeKeysAdded
                                                ) {
 
     VariableNode lnX = getVariableNodeFromTemp(x);
@@ -594,11 +628,12 @@ public class ReachGraph {
         if( !DISABLE_STRONG_UPDATES ) {
           strongUpdateCond = true;
 
-          boolean atLeastOne =
-            clearRefEdgesFrom(hrnX,
-                              f.getType(),
-                              f.getSymbol(),
-                              false);
+          boolean atLeastOne = clearRefEdgesFrom(hrnX,
+                                                 f.getType(),
+                                                 f.getSymbol(),
+                                                 false,
+                                                 edgeKeysRemoved,
+                                                 f);          
           if( atLeastOne ) {
             edgeRemovedByStrongUpdate = true;
           }
@@ -683,6 +718,15 @@ public class ReachGraph {
           continue;
         }
 
+        // for definite reach analysis only
+        if( edgeKeysAdded != null ) {
+          assert f != null;
+          edgeKeysAdded.add( new EdgeKey( hrnX.getID(),
+                                          hrnY.getID(),
+                                          f )
+                             );
+        }
+
         // prepare the new reference edge hrnX.f -> hrnY
         TypeDescriptor tdNewEdge =
           mostSpecificType(y.getType(),
@@ -1584,7 +1628,7 @@ public class ReachGraph {
                                           predNodeOrEdge.e_hrnDstID,
                                           predNodeOrEdge.e_type,
                                           predNodeOrEdge.e_field,
-                                          stateCallee,
+                                          stateCaller,
                                           null,
                                           predNodeOrEdge.e_srcOutCalleeContext,
                                           predNodeOrEdge.e_srcOutCallerContext
@@ -2256,7 +2300,6 @@ 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;
@@ -3951,7 +3994,7 @@ public class ReachGraph {
 
 
 
-  static boolean dbgEquals = false;
+  static public boolean dbgEquals = false;
 
 
   // it is necessary in the equals() member functions
@@ -4177,9 +4220,7 @@ public class ReachGraph {
 
           // there is an edge in the right place with the right field,
           // but do they have the same attributes?
-          if( edgeA.getBeta().equals(edgeB.getBeta() ) &&
-              edgeA.equalsPreds(edgeB)
-              ) {
+          if( edgeA.equalsIncludingBetaPredsTaints( edgeB ) ) {
             edgeFound = true;
           }
         }