lots of untested code, but compiles, for attaching preds to reach states

diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java
index 23c39bb630f1bf8f3e7d7dacb22af131b40a4740..e7f01945a347012c393a6d6040e1596525f9cb70 100644 (file)
--- a/Robust/src/Analysis/Disjoint/Canonical.java
+++ b/Robust/src/Analysis/Disjoint/Canonical.java
@@ -151,6 +151,35 @@ abstract public class Canonical {
   }
 
 
+  public static ReachState attach( ReachState   rs,
+                                   ExistPredSet preds ) {
+    assert rs    != null;
+    assert preds != null;
+    assert rs.isCanonical();
+    assert preds.isCanonical();
+
+    CanonicalOp op = 
+      new CanonicalOp( CanonicalOp.REACHSTATE_ATTACH_EXISTPREDSET,
+                       rs, 
+                       preds );
+    
+    Canonical result = op2result.get( op );
+    if( result != null ) {
+      return (ReachState) result;
+    }
+    
+    // otherwise, no cached result...
+    ReachState out = new ReachState();
+    out.reachTuples.addAll( rs.reachTuples );
+    out.preds = Canonical.join( rs.preds,
+                                preds );
+
+    out = (ReachState) makeCanonical( out );
+    op2result.put( op, out );
+    return out;
+  }
+
+
   public static ReachState union( ReachState rs1,
                                   ReachState rs2 ) {
     assert rs1 != null;
@@ -172,6 +201,9 @@ abstract public class Canonical {
     ReachState out = new ReachState();
     out.reachTuples.addAll( rs1.reachTuples );
     out.reachTuples.addAll( rs2.reachTuples );
+    out.preds = Canonical.join( rs1.getPreds(),
+                                rs2.getPreds()
+                                );
 
     out = (ReachState) makeCanonical( out );
     op2result.put( op, out );
@@ -198,6 +230,7 @@ abstract public class Canonical {
     ReachState out = new ReachState();
     out.reachTuples.addAll( rs.reachTuples );
     out.reachTuples.add( rt );
+    out.preds = rs.preds;
 
     out = (ReachState) makeCanonical( out );
     op2result.put( op, out );
@@ -248,6 +281,10 @@ abstract public class Canonical {
        out.reachTuples.add( rto );
       }
     }
+
+    out.preds = Canonical.join( rs1.getPreds(),
+                                rs2.getPreds()
+                                );
     
     out = (ReachState) makeCanonical( out );
     op2result.put( op, out );
@@ -276,6 +313,7 @@ abstract public class Canonical {
     ReachState out = new ReachState();
     out.reachTuples.addAll( rs.reachTuples );
     out.reachTuples.remove( rt );
+    out.preds = rs.preds;
 
     out = (ReachState) makeCanonical( out );
     op2result.put( op, out );
@@ -375,6 +413,8 @@ abstract public class Canonical {
                            );
     }
 
+    out.preds = rs.preds;
+
     out = (ReachState) makeCanonical( out );
     op2result.put( op, out );
     return out;
@@ -832,7 +872,7 @@ abstract public class Canonical {
   }
 
 
-
+  /*
   public static ReachSet toCalleeContext( ReachSet  rs,
                                           AllocSite as ) {
     assert rs != null;
@@ -864,6 +904,7 @@ abstract public class Canonical {
     op2result.put( op, out );
     return out;
   }
+  */
 
   public static ReachState toCalleeContext( ReachState state,
                                             AllocSite  as ) {
@@ -938,6 +979,10 @@ abstract public class Canonical {
       }
     }
 
+    out = Canonical.attach( out,
+                            state.getPreds()
+                            );
+
     assert out.isCanonical();
     op2result.put( op, out );
     return out;
@@ -1223,6 +1268,10 @@ abstract public class Canonical {
       }
     }
 
+    out = Canonical.attach( out,
+                            state.getPreds()
+                            );
+
     assert out.isCanonical();
     op2result.put( op, out );
     return out;

diff --git a/Robust/src/Analysis/Disjoint/CanonicalOp.java b/Robust/src/Analysis/Disjoint/CanonicalOp.java
index 7f5dd6cf208bdb2b95da28fb3e3a6cb6dd71013b..14ca4bc155fcb34555b6b0f492ebfc1c09252a2a 100644 (file)
--- a/Robust/src/Analysis/Disjoint/CanonicalOp.java
+++ b/Robust/src/Analysis/Disjoint/CanonicalOp.java
@@ -9,6 +9,7 @@ package Analysis.Disjoint;
 public class CanonicalOp {
 
   public static final int REACHTUPLE_UNIONARITY_REACHTUPLE     = 0x1a34;
+  public static final int REACHSTATE_ATTACH_EXISTPREDSET       = 0x8358;
   public static final int REACHSTATE_UNION_REACHSTATE          = 0x5678;
   public static final int REACHSTATE_UNION_REACHTUPLE          = 0x32b6;
   public static final int REACHSTATE_UNIONUPARITY_REACHSTATE   = 0x9152;

diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java
index 6b46ab5ea306c4d68e3eb4f3cb50bb4889043a39..ec60aaafc0ec20f009d05bdb116c5c641981fd2a 100644 (file)
--- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java
+++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java
@@ -36,8 +36,7 @@ public class HeapRegionNode extends RefSrcNode {
 
   // existence predicates must be true in a caller
   // context for this node to transfer from this
-  // callee to that context--NOTE, existence predicates
-  // do not factor into node comparisons
+  // callee to that context
   protected ExistPredSet preds;
 
 

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index c8a63bf03994ff02662ed54c936a018b01273158..470c86076a5a32ab06c40cbd24f94b9d839ac392 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -1280,12 +1280,63 @@ public class ReachGraph {
 
   // used below to convert a ReachSet to its callee-context
   // equivalent with respect to allocation sites in this graph
-  protected ReachSet toCalleeContext( ReachSet rs ) {
-    ReachSet out = rs;
-    Iterator<AllocSite> asItr = allocSites.iterator();
-    while( asItr.hasNext() ) {
-      AllocSite as = asItr.next();
-      out = Canonical.toCalleeContext( out, as );
+  protected ReachSet toCalleeContext( ReachSet       rs,
+                                      Integer        hrnID,
+                                      TempDescriptor tdSrc,
+                                      Integer        hrnSrcID,
+                                      Integer        hrnDstID,
+                                      TypeDescriptor type,
+                                      String         field,
+                                      boolean        outOfContext
+                                      ) {
+    ReachSet out = ReachSet.factory();
+   
+    Iterator<ReachState> itr = rs.iterator();
+    while( itr.hasNext() ) {
+      ReachState stateCaller = itr.next();
+    
+      ReachState stateCallee = stateCaller;
+
+      Iterator<AllocSite> asItr = allocSites.iterator();
+      while( asItr.hasNext() ) {
+        AllocSite as = asItr.next();
+
+        stateCallee = Canonical.toCalleeContext( stateCallee, as );
+      }
+
+      ExistPredSet preds;
+
+      if( outOfContext ) {
+        preds = predsEmpty;
+      } else {
+        ExistPred pred;
+        if( hrnID != null ) {
+          assert tdSrc    == null;
+          assert hrnSrcID == null;
+          assert hrnDstID == null;
+          pred = ExistPred.factory( hrnID, 
+                                    stateCaller );
+        } else {
+          assert tdSrc != null || hrnSrcID != null;
+          assert hrnDstID != null;
+          pred = ExistPred.factory( tdSrc,
+                                    hrnSrcID,
+                                    hrnDstID,
+                                    type,
+                                    field,
+                                    stateCaller,
+                                    false );
+        }
+        preds = ExistPredSet.factory( pred );
+      }
+      
+      stateCallee = Canonical.attach( stateCallee,
+                                      preds );
+
+      out = Canonical.add( out,
+                           stateCallee
+                           );
+
     }
     assert out.isCanonical();
     return out;
@@ -1414,8 +1465,14 @@ public class ReachGraph {
                                           false, // out-of-context?
                                           hrnSrcCaller.getType(),
                                           hrnSrcCaller.getAllocSite(),
-                                          toCalleeContext( hrnSrcCaller.getInherent() ),
-                                          toCalleeContext( hrnSrcCaller.getAlpha() ),
+                                          toCalleeContext( hrnSrcCaller.getInherent(),   // in state
+                                                           hrnSrcCaller.getID(),         // node pred
+                                                           null, null, null, null, null, // edge pred
+                                                           false ),                      // ooc pred
+                                          toCalleeContext( hrnSrcCaller.getAlpha(),      // in state
+                                                           hrnSrcCaller.getID(),         // node pred
+                                                           null, null, null, null, null, // edge pred
+                                                           false ),                      // ooc pred
                                           preds,
                                           hrnSrcCaller.getDescription()
                                           );
@@ -1454,8 +1511,14 @@ public class ReachGraph {
                                           false, // out-of-context?
                                           hrnCaller.getType(),
                                           hrnCaller.getAllocSite(),
-                                          toCalleeContext( hrnCaller.getInherent() ),
-                                          toCalleeContext( hrnCaller.getAlpha() ),
+                                          toCalleeContext( hrnCaller.getInherent(),      // in state
+                                                           hrnDstID,                     // node pred
+                                                           null, null, null, null, null, // edge pred
+                                                           false ),                      // ooc pred
+                                          toCalleeContext( hrnCaller.getAlpha(),         // in state
+                                                           hrnDstID,                     // node pred
+                                                           null, null, null, null, null, // edge pred
+                                                           false ),                      // ooc pred
                                           preds,
                                           hrnCaller.getDescription()
                                           );
@@ -1491,7 +1554,14 @@ public class ReachGraph {
                                         hrnCallee,
                                         reCaller.getType(),
                                         reCaller.getField(),
-                                        toCalleeContext( reCaller.getBeta() ),
+                                        toCalleeContext( reCaller.getBeta(),  // in state
+                                                         null,                // node pred
+                                                         tdSrc,               // edge pred
+                                                         hrnSrcID,            // edge pred
+                                                         hrnDstID,            // edge pred
+                                                         reCaller.getType(),  // edge pred
+                                                         reCaller.getField(), // edge pred
+                                                         false ),             // ooc pred
                                         preds
                                         )
                            );              
@@ -1608,8 +1678,16 @@ public class ReachGraph {
                                           true,  // out-of-context?
                                           oocNodeType,
                                           null,  // alloc site, shouldn't be used
-                                          toCalleeContext( oocReach ), // inherent
-                                          toCalleeContext( oocReach ), // alpha
+                                          toCalleeContext( oocReach,                     // in state
+                                                           null,                         // node pred
+                                                           null, null, null, null, null, // edge pred
+                                                           true                          // ooc pred
+                                                           ), // inherent
+                                          toCalleeContext( oocReach,                     // in state
+                                                           null,                         // node pred
+                                                           null, null, null, null, null, // edge pred
+                                                           true                          // ooc pred
+                                                           ), // alpha
                                           preds,
                                           "out-of-context"
                                           );       
@@ -1631,8 +1709,16 @@ public class ReachGraph {
                                             true,  // out-of-context?
                                             oocNodeType,
                                             null,  // alloc site, shouldn't be used
-                                            toCalleeContext( oocReach ), // inherent
-                                            toCalleeContext( oocReach ), // alpha
+                                            toCalleeContext( oocReach,                     // in state
+                                                             null,                         // node pred
+                                                             null, null, null, null, null, // edge pred
+                                                             true                          // ooc pred
+                                                             ), // inherent
+                                            toCalleeContext( oocReach,                     // in state
+                                                             null,                         // node pred
+                                                             null, null, null, null, null, // edge pred
+                                                             true                          // ooc pred
+                                                             ), // alpha
                                             preds,
                                             "out-of-context"
                                             );       
@@ -1645,7 +1731,15 @@ public class ReachGraph {
                                       hrnCalleeAndInContext,
                                       edgeMightCross.getType(),
                                       edgeMightCross.getField(),
-                                      toCalleeContext( edgeMightCross.getBeta() ),
+                                      toCalleeContext( edgeMightCross.getBeta(),      // in state
+                                                       null,                          // node pred
+                                                       oocPredSrcTemp,                // edge pred
+                                                       oocPredSrcID,                  // edge pred
+                                                       hrnCallerAndInContext.getID(), // edge pred
+                                                       edgeMightCross.getType(),      // edge pred
+                                                       edgeMightCross.getField(),     // edge pred
+                                                       false                          // ooc pred
+                                                       ),
                                       preds
                                       )
                          );              
@@ -1653,10 +1747,18 @@ public class ReachGraph {
         } else {
           // the out-of-context edge already exists
           oocEdgeExisting.setBeta( Canonical.union( oocEdgeExisting.getBeta(),
-                                                    toCalleeContext( edgeMightCross.getBeta() )
+                                                    toCalleeContext( edgeMightCross.getBeta(),      // in state
+                                                                     null,                          // node pred
+                                                                     oocPredSrcTemp,                // edge pred
+                                                                     oocPredSrcID,                  // edge pred
+                                                                     hrnCallerAndInContext.getID(), // edge pred
+                                                                     edgeMightCross.getType(),      // edge pred
+                                                                     edgeMightCross.getField(),     // edge pred
+                                                                     false                          // ooc pred
+                                                                     )
                                                     )
                                    );         
- 
+          
           oocEdgeExisting.setPreds( Canonical.join( oocEdgeExisting.getPreds(),
                                                     edgeMightCross.getPreds()
                                                     )

diff --git a/Robust/src/Analysis/Disjoint/ReachState.java b/Robust/src/Analysis/Disjoint/ReachState.java
index aa17556174d13a003eeae3be635f8267e7b4d7dd..732054a36e7b48508acf4288affa1c4f9b01310e 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachState.java
+++ b/Robust/src/Analysis/Disjoint/ReachState.java
@@ -31,6 +31,11 @@ public class ReachState extends Canonical {
 
   protected HashSet<ReachTuple> reachTuples;
 
+  // existance predicates must be true in a caller
+  // context for this node to transfer from this
+  // callee to that context
+  protected ExistPredSet preds;
+
 
   public static ReachState factory() {
     ReachState out = new ReachState();
@@ -49,6 +54,7 @@ public class ReachState extends Canonical {
 
   protected ReachState() {
     reachTuples = new HashSet<ReachTuple>();
+    preds       = ExistPredSet.factory();
   }
 
 
@@ -88,6 +94,9 @@ public class ReachState extends Canonical {
     return null;
   }
 
+  public ExistPredSet getPreds() {
+    return preds;
+  }
 
 
   public boolean equals( Object o ) {
@@ -100,16 +109,18 @@ public class ReachState extends Canonical {
     }
 
     ReachState rs = (ReachState) o;
-    return reachTuples.equals( rs.reachTuples );
+    return 
+      reachTuples.equals( rs.reachTuples ) &&
+      preds.equals( rs.preds );
   }
 
 
   public int hashCodeSpecific() {
-    return reachTuples.hashCode();
+    return reachTuples.hashCode() ^ preds.hashCode();
   }
 
 
   public String toString() {
-    return reachTuples.toString();
+    return reachTuples+":"+preds;
   }
 }