def reach coming along

diff --git a/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java b/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
index 0ebfbdd2a8340f2d82c397a08d32336bf9414231..6477a8f5269afa572b5ae7082d9014494b70ca44 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
@@ -51,9 +51,10 @@ public class DefiniteReachAnalysis {
                      TempDescriptor  x,
                      FieldDescriptor f,
                      TempDescriptor  y,
-                    Set<EdgeKey> edgeKeysRemoved ) {
+                     Set<EdgeKey> edgeKeysRemoved,
+                     Set<EdgeKey> edgeKeysAdded ) {
     DefiniteReachState state = makeIn( fn );
-    state.store( x, f, y, edgeKeysRemoved );
+    state.store( x, f, y, edgeKeysRemoved, edgeKeysAdded );
     fn2state.put( fn, state ); 
   }
 

diff --git a/Robust/src/Analysis/Disjoint/DefiniteReachState.java b/Robust/src/Analysis/Disjoint/DefiniteReachState.java
index 710a6954bbd2c4abce0bb3ea06b32bc1796d011e..8006656b7dc65f0a41b102f6441566c93833e767 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DefiniteReachState.java
+++ b/Robust/src/Analysis/Disjoint/DefiniteReachState.java
@@ -135,6 +135,7 @@ public class DefiniteReachState {
                     TempDescriptor y,
                     FieldDescriptor f,
                     Set<EdgeKey> edgeKeysForLoad ) {
+
     loadR( x, y, f, edgeKeysForLoad );
     // Rs' := (Rs - <x,*>) U {<x, unknown>}
     //Rs.put( x, DefReachKnown.UNKNOWN );
@@ -143,8 +144,10 @@ public class DefiniteReachState {
   public void store( TempDescriptor x,
                      FieldDescriptor f,
                      TempDescriptor y,
-                     Set<EdgeKey> edgeKeysRemoved ) {
-    storeR( x, f, y, edgeKeysRemoved );
+                     Set<EdgeKey> edgeKeysRemoved,
+                     Set<EdgeKey> edgeKeysAdded ) {
+
+    storeR( x, f, y, edgeKeysRemoved, edgeKeysAdded );
     // Rs' := Rs
   }
 
@@ -246,7 +249,8 @@ public class DefiniteReachState {
   public void storeR( TempDescriptor x,
                       FieldDescriptor f,
                       TempDescriptor y,
-                      Set<EdgeKey> edgeKeysRemoved ) {
+                      Set<EdgeKey> edgeKeysRemoved,
+                      Set<EdgeKey> edgeKeysAdded ) {
     // I think this should be if there is ANY <w,z>->e' IN Eremove, then kill all <w,z>
     // R' := (R - {<w,z>->e | <w,z>->e in R, A<w,z>->e' in R, e' notin Eremove}) U
     //       {<y,x>->e | e in E(x) x {f} x E(y)}

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index 176bba262f46ed95596e58d7afdffc2f4b92ee1b..6bde8d8d5f297dbe1207538ee5b84ec6b253213f 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -1304,6 +1304,7 @@ public class DisjointAnalysis implements HeapAnalysis {
 
     Set<EdgeKey> edgeKeysForLoad;
     Set<EdgeKey> edgeKeysRemoved;
+    Set<EdgeKey> edgeKeysAdded;
 
     //Stores the flatnode's reach graph at enter
     ReachGraph rgOnEnter = new ReachGraph();
@@ -1487,8 +1488,10 @@ public class DisjointAnalysis implements HeapAnalysis {
       boolean strongUpdate = false;
 
       edgeKeysRemoved = null;
+      edgeKeysAdded   = null;
       if( doDefiniteReachAnalysis ) {
         edgeKeysRemoved = new HashSet<EdgeKey>();
+        edgeKeysAdded   = new HashSet<EdgeKey>();
       }
 
       // before transfer func, possibly inject
@@ -1514,10 +1517,19 @@ public class DisjointAnalysis implements HeapAnalysis {
 
       if( shouldAnalysisTrack(fld.getType() ) ) {
         // transfer func
-        strongUpdate = rg.assignTempXFieldFEqualToTempY(lhs, fld, rhs, fn, edgeKeysRemoved);
-
+        strongUpdate = rg.assignTempXFieldFEqualToTempY( lhs, 
+                                                         fld, 
+                                                         rhs, 
+                                                         fn, 
+                                                         edgeKeysRemoved,
+                                                         edgeKeysAdded );
         if( doDefiniteReachAnalysis ) {
-          definiteReachAnalysis.store( fn, lhs, fld, rhs, edgeKeysRemoved );
+          definiteReachAnalysis.store( fn, 
+                                       lhs,
+                                       fld,
+                                       rhs,
+                                       edgeKeysRemoved,
+                                       edgeKeysAdded );
         }
       }
 
@@ -1588,8 +1600,10 @@ public class DisjointAnalysis implements HeapAnalysis {
       fdElement = getArrayField(tdElement);
 
       edgeKeysRemoved = null;
+      edgeKeysAdded   = null;
       if( doDefiniteReachAnalysis ) {
         edgeKeysRemoved = new HashSet<EdgeKey>();
+        edgeKeysAdded   = new HashSet<EdgeKey>();
       }
 
       // before transfer func, possibly inject
@@ -1617,11 +1631,21 @@ public class DisjointAnalysis implements HeapAnalysis {
         // transfer func, BUT
         // skip this node if it cannot create new reachability paths
         if( !arrayReferencees.doesNotCreateNewReaching(fsen) ) {
-          rg.assignTempXFieldFEqualToTempY(lhs, fdElement, rhs, fn, edgeKeysRemoved);
+          rg.assignTempXFieldFEqualToTempY( lhs, 
+                                            fdElement, 
+                                            rhs, 
+                                            fn, 
+                                            edgeKeysRemoved,
+                                            edgeKeysAdded );
         }
 
         if( doDefiniteReachAnalysis ) {
-          definiteReachAnalysis.store( fn, lhs, fdElement, rhs, edgeKeysRemoved );
+          definiteReachAnalysis.store( fn,
+                                       lhs,
+                                       fdElement, 
+                                       rhs, 
+                                       edgeKeysRemoved,
+                                       edgeKeysAdded );
         }
       }
 

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 8d5038c07b003a2422f785bfe3b4b66f60b24d43..d231593bfdbac6bfa5007405bb5e8f641464c697 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -426,7 +426,8 @@ public class ReachGraph {
                                    fdStringBytesField,
                                    tdStrLiteralBytes,
                                    null,
-                                   null);
+                                   null,
+                                   null );
   }
 
 
@@ -593,7 +594,8 @@ public class ReachGraph {
                                                FieldDescriptor f,
                                                TempDescriptor y,
                                                FlatNode currentProgramPoint,
-                                               Set<EdgeKey> edgeKeysRemoved
+                                               Set<EdgeKey> edgeKeysRemoved,
+                                               Set<EdgeKey> edgeKeysAdded
                                                ) {
 
     VariableNode lnX = getVariableNodeFromTemp(x);
@@ -716,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(),