going to start with just enough definite reach analysis to do a simple example

diff --git a/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java b/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
index 5fec38af0d380f2b9a4b010fb5f168c8c1c3fbeb..f22da374f78d6c9a4b298679567bbd10ccd76cd6 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
@@ -49,9 +49,10 @@ public class DefiniteReachAnalysis {
   public void store( FlatNode fn, 
                      TempDescriptor  x,
                      FieldDescriptor f,
-                     TempDescriptor  y ) {
+                     TempDescriptor  y,
+                    Set<EdgeKey> edgeKeysRemoved ) {
     DefiniteReachState state = makeIn( fn );
-    state.store( x, f, y );
+    state.store( x, f, y, edgeKeysRemoved );
     fn2state.put( fn, state ); 
   }
 
@@ -62,15 +63,16 @@ public class DefiniteReachAnalysis {
     fn2state.put( fn, state ); 
   }
 
-  // x is the return value, x = foo(...);
   public void methodCall( FlatNode fn, 
-                          TempDescriptor x ) {
+                          TempDescriptor retVal ) {
     DefiniteReachState state = makeIn( fn );
-    state.methodCall( x );
+    state.methodCall( retVal );
     fn2state.put( fn, state ); 
   }
 
 
+
+
   public void writeState( FlatNode fn, String outputName ) {
     DefiniteReachState state = makeIn( fn );
     try {

diff --git a/Robust/src/Analysis/Disjoint/DefiniteReachState.java b/Robust/src/Analysis/Disjoint/DefiniteReachState.java
index 8b64181cdc1a5e6a6725c8e206fbd5e81b9282af..43a20d2767a6251e91f566bb360bdd5b5c153b64 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DefiniteReachState.java
+++ b/Robust/src/Analysis/Disjoint/DefiniteReachState.java
@@ -11,21 +11,26 @@ public class DefiniteReachState {
 
   // R
   //
-  // Maps variables and an edge (x, y, e) to an unused value when the
+  // Maps two variables to an edge (x, y, e) to an unused value when the
   // object of x is already reachable from the object of y, and the
   // set of edges conservatively gives the path.
   // NOTE: Use EdgeKey instead of edges because this analysis's
   // scope is beyond the scope of a single reach graph.
-
+  private static MultiViewMapBuilder<Object> RBuilder;
+  private static BitSet viewR0;
+  private static BitSet viewR1;
+  private static BitSet viewR01;
+  private MultiViewMap<Object> R;
 
   // Rs
+  //
   // Tracks whether the analysis must know the definite reachability
   // information of a given variable.
-  private enum DefReachKnown {
-    UNKNOWN,
-    KNOWN,
-  }
-  private Map<TempDescriptor, DefReachKnown> Rs;
+  //private enum DefReachKnown {
+  //  UNKNOWN,
+  //  KNOWN,
+  //}
+  //private Map<TempDescriptor, DefReachKnown> Rs;
   
   
   // Fu (upstream)
@@ -33,10 +38,10 @@ public class DefiniteReachState {
   // Maps a variable that points to object o0 to the
   // set of variables that point to objects o1...oN
   // that have a reference to o0.
-  private static MultiViewMapBuilder<Object> FuBuilder;
-  private static BitSet viewFu0;
-  private static BitSet viewFu1;
-  private MultiViewMap<Object> Fu;
+  //private static MultiViewMapBuilder<Object> FuBuilder;
+  //private static BitSet viewFu0;
+  //private static BitSet viewFu1;
+  //private MultiViewMap<Object> Fu;
 
 
   // Fd (downstream)
@@ -46,20 +51,32 @@ public class DefiniteReachState {
 
   // for MultiViewMaps that don't need to use the value,
   // always map to this dummy
-  private static Object dummy = new Integer( -1234 );
+  private static Object dummy = new Integer( -12345 );
 
 
   // call before instantiating this class
   static public void initBuilders() {
-    FuBuilder =
+    RBuilder =
       new MultiViewMapBuilder<Object>( new Class[] {
                                          TempDescriptor.class,
-                                         DefReachFuVal.class},
+                                         TempDescriptor.class,
+                                         EdgeKey.class },
                                        new JoinOpNop() );
-    viewFu0 = FuBuilder.addPartialView( 0 );
-    viewFu1 = FuBuilder.addPartialView( 1 );
-    FuBuilder.setCheckTypes( true );
-    FuBuilder.setCheckConsistency( true );
+    viewR0  = RBuilder.addPartialView( 0 );
+    viewR1  = RBuilder.addPartialView( 1 );
+    viewR01 = RBuilder.addPartialView( 0, 1 );
+    RBuilder.setCheckTypes( true );
+    RBuilder.setCheckConsistency( true );
+
+    //FuBuilder =
+    //  new MultiViewMapBuilder<Object>( new Class[] {
+    //                                     TempDescriptor.class,
+    //                                     DefReachFuVal.class},
+    //                                   new JoinOpNop() );
+    //viewFu0 = FuBuilder.addPartialView( 0 );
+    //viewFu1 = FuBuilder.addPartialView( 1 );
+    //FuBuilder.setCheckTypes( true );
+    //FuBuilder.setCheckConsistency( true );
   }
 
 
@@ -67,8 +84,8 @@ public class DefiniteReachState {
 
 
   public DefiniteReachState() {
-    Rs = new HashMap<TempDescriptor, DefReachKnown>();
-    Fu = FuBuilder.build();
+    //Rs = new HashMap<TempDescriptor, DefReachKnown>();
+    //Fu = FuBuilder.build();
   }
 
 
@@ -77,12 +94,12 @@ public class DefiniteReachState {
     // R' := {}
     // R.clear();
 
-    Rs.clear();
-    for( TempDescriptor p : parameters ) {
-      Rs.put( p, DefReachKnown.UNKNOWN );
-    }
-
-    Fu = FuBuilder.build();
+    //Rs.clear();
+    //for( TempDescriptor p : parameters ) {
+    //  Rs.put( p, DefReachKnown.UNKNOWN );
+    //}
+    //
+    //Fu = FuBuilder.build();
   }
 
   public void copy(TempDescriptor x,
@@ -99,32 +116,32 @@ public class DefiniteReachState {
     // for each <z,y>->e: R'.put(<z,x>, e);
 
     // Rs' := (Rs - <x,*>) U {<x,v> | <y,v> in Rs}
-    DefReachKnown valRs = Rs.get( y );
-    assert( valRs != null );
-    Rs.put( x, valRs );
+    //DefReachKnown valRs = Rs.get( y );
+    //assert( valRs != null );
+    //Rs.put( x, valRs );
 
     // Fu' := (Fu - <x, *> - <*, x>) U
     //        {<x,v> | <y,v> in Fu} U
     //        {<v,x> | <v,y> in Fu} U
     //        {<z, unknown> | <z,<x>> in Fu}
-    Fu.remove( viewFu0, MultiKey.factory( x ) );
-    Fu.remove( viewFu1, MultiKey.factory( x ) );
-    for( MultiKey key : Fu.get( viewFu0, MultiKey.factory( y ) ).keySet() ) {
-      DefReachFuVal val = (DefReachFuVal) key.get( 1 );
-      Fu.put( MultiKey.factory( x, val ), dummy );
-    }
-    for( MultiKey key : Fu.get( viewFu1, MultiKey.factory( y ) ).keySet() ) {
-      TempDescriptor v = (TempDescriptor) key.get( 0 );
-      Fu.put( MultiKey.factory( v, DefReachFuVal.factory( x ) ), dummy );
-    }
-    for( MultiKey key : 
-           Fu.get( viewFu1, 
-                   MultiKey.factory( DefReachFuVal.factory( DefReachFuVal.Val.UNKNOWN ) )
-                   ).keySet() 
-         ) {
-      TempDescriptor z = (TempDescriptor) key.get( 0 );
-      Fu.put( MultiKey.factory( z, DefReachFuVal.factory( x ) ), dummy );      
-    }
+    //Fu.remove( viewFu0, MultiKey.factory( x ) );
+    //Fu.remove( viewFu1, MultiKey.factory( x ) );
+    //for( MultiKey key : Fu.get( viewFu0, MultiKey.factory( y ) ).keySet() ) {
+    //  DefReachFuVal val = (DefReachFuVal) key.get( 1 );
+    //  Fu.put( MultiKey.factory( x, val ), dummy );
+    //}
+    //for( MultiKey key : Fu.get( viewFu1, MultiKey.factory( y ) ).keySet() ) {
+    //  TempDescriptor v = (TempDescriptor) key.get( 0 );
+    //  Fu.put( MultiKey.factory( v, DefReachFuVal.factory( x ) ), dummy );
+    //}
+    //for( MultiKey key : 
+    //       Fu.get( viewFu1, 
+    //               MultiKey.factory( DefReachFuVal.factory( DefReachFuVal.Val.UNKNOWN ) )
+    //               ).keySet() 
+    //     ) {
+    //  TempDescriptor z = (TempDescriptor) key.get( 0 );
+    //  Fu.put( MultiKey.factory( z, DefReachFuVal.factory( x ) ), dummy );      
+    //}
   }
 
   public void load(TempDescriptor x,
@@ -142,12 +159,13 @@ public class DefiniteReachState {
     // for each <y,z>->e: R'.put(<x,z>, eee!Ue);
 
     // Rs' := (Rs - <x,*>) U {<x, unknown>}
-    Rs.put( x, DefReachKnown.UNKNOWN );
+    //Rs.put( x, DefReachKnown.UNKNOWN );
   }
 
   public void store(TempDescriptor x,
                    FieldDescriptor f,
-                   TempDescriptor y) {
+                   TempDescriptor y,
+                   Set<EdgeKey> edgeKeysRemoved) {
     // 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)}
@@ -165,7 +183,7 @@ public class DefiniteReachState {
     // R'.remove(view1, x);
 
     // Rs' := (Rs - <x,*>) U {<x, new>}
-    Rs.put( x, DefReachKnown.KNOWN );
+    //Rs.put( x, DefReachKnown.KNOWN );
     
   }
 
@@ -177,14 +195,14 @@ public class DefiniteReachState {
     // R'.remove(view1, x);
 
     // Rs' := (Rs - <x,*>) U {<x, unknown>}
-    Rs.put( x, DefReachKnown.UNKNOWN );
+    //Rs.put( x, DefReachKnown.UNKNOWN );
   }
 
   public void merge( DefiniteReachState that ) {
     // R' := <x,y>->e iff its in all incoming edges
 
     // Rs' := <x, new> iff in all incoming edges, otherwie <x, unknown>
-    mergeRs( that );
+    //mergeRs( that );
   }
 
 
@@ -200,19 +218,19 @@ public class DefiniteReachState {
   //  before there is a sensical answer.  I think...
   private void mergeRs( DefiniteReachState that ) {
     // merge "that" into "this" and leave "that" unchanged
-    Set<TempDescriptor> allVars = new HashSet<TempDescriptor>();
-    allVars.addAll( this.Rs.keySet() );
-    allVars.addAll( that.Rs.keySet() );
-    for( TempDescriptor x : allVars ) {
-      DefReachKnown vThis = this.Rs.get( x );
-      DefReachKnown vThat = that.Rs.get( x );
-      if( vThis != null && vThis.equals( DefReachKnown.KNOWN ) &&
-          vThat != null && vThat.equals( DefReachKnown.KNOWN ) ) {
-        this.Rs.put( x, DefReachKnown.KNOWN );
-      } else {
-        this.Rs.put( x, DefReachKnown.UNKNOWN );
-      }
-    }
+    //Set<TempDescriptor> allVars = new HashSet<TempDescriptor>();
+    //allVars.addAll( this.Rs.keySet() );
+    //allVars.addAll( that.Rs.keySet() );
+    //for( TempDescriptor x : allVars ) {
+    //  DefReachKnown vThis = this.Rs.get( x );
+    //  DefReachKnown vThat = that.Rs.get( x );
+    //  if( vThis != null && vThis.equals( DefReachKnown.KNOWN ) &&
+    //      vThat != null && vThat.equals( DefReachKnown.KNOWN ) ) {
+    //    this.Rs.put( x, DefReachKnown.KNOWN );
+    //  } else {
+    //    this.Rs.put( x, DefReachKnown.UNKNOWN );
+    //  }
+    //}
   }
 
 
@@ -243,10 +261,10 @@ public class DefiniteReachState {
 
   public String toString() {
     StringBuilder s = new StringBuilder( "R_s = {" );
-    for( TempDescriptor x : Rs.keySet() ) {
-      s.append( "  "+x+"->"+Rs.get( x ) );
-    }
-    s.append( "}" );
+    //for( TempDescriptor x : Rs.keySet() ) {
+    //  s.append( "  "+x+"->"+Rs.get( x ) );
+    //}
+    //s.append( "}" );
     return s.toString();
   }
 }

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index 3c5e29e3411d88a636c49228a0c77978eb6ded95..00f0735f648b9a0d5e476f1046fd7b5fe0c0b639 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -1302,6 +1302,8 @@ public class DisjointAnalysis implements HeapAnalysis {
     FlatSESEEnterNode sese;
     FlatSESEExitNode fsexn;
 
+    Set<EdgeKey> edgeKeysRemoved;
+
     //Stores the flatnode's reach graph at enter
     ReachGraph rgOnEnter = new ReachGraph();
     rgOnEnter.merge(rg);
@@ -1478,6 +1480,11 @@ public class DisjointAnalysis implements HeapAnalysis {
 
       boolean strongUpdate = false;
 
+      edgeKeysRemoved = null;
+      if( doDefiniteReachAnalysis ) {
+        edgeKeysRemoved = new HashSet<EdgeKey>();
+      }
+
       // before transfer func, possibly inject
       // stall-site taints
       if( doEffectsAnalysis && fmContaining != fmAnalysisEntry ) {
@@ -1501,10 +1508,10 @@ public class DisjointAnalysis implements HeapAnalysis {
 
       if( shouldAnalysisTrack(fld.getType() ) ) {
         // transfer func
-        strongUpdate = rg.assignTempXFieldFEqualToTempY(lhs, fld, rhs, fn);
+        strongUpdate = rg.assignTempXFieldFEqualToTempY(lhs, fld, rhs, fn, edgeKeysRemoved);
 
         if( doDefiniteReachAnalysis ) {
-          definiteReachAnalysis.store( fn, lhs, fld, rhs );
+          definiteReachAnalysis.store( fn, lhs, fld, rhs, edgeKeysRemoved );
         }
       }
 
@@ -1562,13 +1569,18 @@ public class DisjointAnalysis implements HeapAnalysis {
 
       lhs = fsen.getDst();
       rhs = fsen.getSrc();
-
+      
       assert lhs.getType() != null;
       assert lhs.getType().isArray();
 
       tdElement = lhs.getType().dereference();
       fdElement = getArrayField(tdElement);
 
+      edgeKeysRemoved = null;
+      if( doDefiniteReachAnalysis ) {
+        edgeKeysRemoved = new HashSet<EdgeKey>();
+      }
+
       // before transfer func, possibly inject
       // stall-site taints
       if( doEffectsAnalysis && fmContaining != fmAnalysisEntry ) {
@@ -1594,11 +1606,11 @@ 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);
+          rg.assignTempXFieldFEqualToTempY(lhs, fdElement, rhs, fn, edgeKeysRemoved);
         }
 
         if( doDefiniteReachAnalysis ) {
-          definiteReachAnalysis.store( fn, lhs, fdElement, rhs );
+          definiteReachAnalysis.store( fn, lhs, fdElement, rhs, edgeKeysRemoved );
         }
       }
 

diff --git a/Robust/src/Analysis/Disjoint/EdgeKey.java b/Robust/src/Analysis/Disjoint/EdgeKey.java
index 64617e90dd2e80130077bc5a8bc64d42b03228b3..f4282bcc5436df6808dac4e3a4cc49d00893ee11 100644 (file)
--- a/Robust/src/Analysis/Disjoint/EdgeKey.java
+++ b/Robust/src/Analysis/Disjoint/EdgeKey.java
@@ -1,3 +1,8 @@
+package Analysis.Disjoint;
+
+import IR.*;
+
+
 public class EdgeKey {
   private Integer srcId;
   private Integer dstId;

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 3e5a043358d8eee448c7f3d32fd2df2d36059a70..02037c79c7adff9105f6c4d6392358945bf337e2 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,7 +425,8 @@ public class ReachGraph {
     assignTempXFieldFEqualToTempY( x,
                                    fdStringBytesField,
                                    tdStrLiteralBytes,
-                                   null );
+                                   null,
+                                   null);
   }
 
 
@@ -561,7 +581,8 @@ public class ReachGraph {
   public boolean assignTempXFieldFEqualToTempY(TempDescriptor x,
                                                FieldDescriptor f,
                                                TempDescriptor y,
-                                               FlatNode currentProgramPoint
+                                               FlatNode currentProgramPoint,
+                                               Set<EdgeKey> edgeKeysRemoved
                                                ) {
 
     VariableNode lnX = getVariableNodeFromTemp(x);
@@ -594,11 +615,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;
           }