implementing

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index 94c9de6ed50090525795eedb71d0bc4395a9fd5a..dc431cc2a71b6e31929f5296a4dc7ed42f8e5b81 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -201,7 +201,11 @@ public class DisjointAnalysis {
 
     if( writeFinalDOTs && !writeAllIncrementalDOTs ) {
       writeFinalGraphs();      
-    }  
+    }
+
+    if( state.DISJOINTWRITEIHMS ) {
+      writeFinalIHMs();
+    }
 
     if( state.DISJOINTALIASFILE != null ) {
       if( state.TASK ) {
@@ -660,7 +664,7 @@ public class DisjointAnalysis {
       ReachGraph rg = (ReachGraph) me.getValue();
 
       try {        
-       rg.writeGraph( d+"COMPLETE",
+       rg.writeGraph( "COMPLETE"+d,
                        true,   // write labels (variables)
                        true,   // selectively hide intermediate temp vars
                        true,   // prune unreachable heap regions
@@ -670,8 +674,36 @@ public class DisjointAnalysis {
       } catch( IOException e ) {}    
     }
   }
+
+  private void writeFinalIHMs() {
+    Iterator d2IHMsItr = mapDescriptorToIHMcontributions.entrySet().iterator();
+    while( d2IHMsItr.hasNext() ) {
+      Map.Entry                        me1 = (Map.Entry)                       d2IHMsItr.next();
+      Descriptor                         d = (Descriptor)                      me1.getKey();
+      Hashtable<FlatCall, ReachGraph> IHMs = (Hashtable<FlatCall, ReachGraph>) me1.getValue();
+
+      Iterator fc2rgItr = IHMs.entrySet().iterator();
+      while( fc2rgItr.hasNext() ) {
+        Map.Entry  me2 = (Map.Entry)  fc2rgItr.next();
+        FlatCall   fc  = (FlatCall)   me2.getKey();
+        ReachGraph rg  = (ReachGraph) me2.getValue();
+                
+        try {        
+          rg.writeGraph( "IHMPARTFOR"+d+"FROM"+fc,
+                         true,   // write labels (variables)
+                         true,   // selectively hide intermediate temp vars
+                         true,   // prune unreachable heap regions
+                         false,  // show back edges to confirm graph validity
+                         true,   // hide subset reachability states
+                         true ); // hide edge taints
+        } catch( IOException e ) {}    
+      }
+    }
+  }
    
 
+
+
   // return just the allocation site associated with one FlatNew node
   protected AllocSite getAllocSiteFromFlatNewPRIVATE( FlatNew fnew ) {
 

diff --git a/Robust/src/Analysis/Disjoint/ExistPredEdge.java b/Robust/src/Analysis/Disjoint/ExistPredEdge.java
index ffe598dc2de63c62be74db28a569376f200859ae..ee0f188ee016646f12f66a776c38b4a7a0116922 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ExistPredEdge.java
+++ b/Robust/src/Analysis/Disjoint/ExistPredEdge.java
@@ -10,7 +10,7 @@ import java.io.*;
 // The reach state may be null--if not the predicate is
 // satisfied when the edge exists AND it has the state.
 
-public class ExistPredEdge extends Canonical {  
+public class ExistPredEdge extends ExistPred {  
 
   // the source of an edge is *either* a variable
   // node or a heap region node
@@ -35,10 +35,13 @@ public class ExistPredEdge extends Canonical {
                         String         field,
                         ReachState     state ) {
 
-    assert (vnSrc == null) || (hrnSrcID == null);
+    assert (tdSrc == null) || (hrnSrcID == null);
     assert hrnDstID != null;
     assert type     != null;
-    assert field    != null;
+
+    // fields can be null when the edge is from
+    // a variable node to a heap region!
+    // assert field    != null;
 
     this.tdSrc    = tdSrc;
     this.hrnSrcID = hrnSrcID;
@@ -132,8 +135,14 @@ public class ExistPredEdge extends Canonical {
       return false;
     }
 
-    if( !field.equals( epn.field ) ) {
-      return false;
+    if( field == null ) {
+      if( epn.field != null ) {
+        return false;
+      }
+    } else {
+      if( !field.equals( epn.field ) ) {
+        return false;
+      }
     }
 
     // ReachState objects are cannonical
@@ -155,7 +164,7 @@ public class ExistPredEdge extends Canonical {
       hash += hrnSrcID.hashCode()*11;
     }
 
-    hash += hrnDst.hashCode();
+    hash += hrnDstID.hashCode();
 
     if( state != null ) {
       hash += state.hashCode();

diff --git a/Robust/src/Analysis/Disjoint/ExistPredNode.java b/Robust/src/Analysis/Disjoint/ExistPredNode.java
index 6ef0a6e9cd2b7370840db90908a40942fa2e4eb4..4a2d610a5e1381e2283d509761fe5b518d9a3896 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ExistPredNode.java
+++ b/Robust/src/Analysis/Disjoint/ExistPredNode.java
@@ -10,7 +10,7 @@ import java.io.*;
 // The reach state may be null--if not the predicate is
 // satisfied when the edge exists AND it has the state.
 
-public class ExistPredNode extends Canonical {  
+public class ExistPredNode extends ExistPred {  
 
   protected Integer    hrnID;
   protected ReachState state;

diff --git a/Robust/src/Analysis/Disjoint/ExistPredSet.java b/Robust/src/Analysis/Disjoint/ExistPredSet.java
index a538ef0df240f2de8bdc2514aa88d3c0d6cfecff..75d0dfe8f02f44efc4100aaf96337183ebc2c2a7 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ExistPredSet.java
+++ b/Robust/src/Analysis/Disjoint/ExistPredSet.java
@@ -17,6 +17,12 @@ public class ExistPredSet extends Canonical {
     preds = new HashSet<ExistPred>();
   }
 
+  public ExistPredSet( ExistPred ep ) {
+    preds = new HashSet<ExistPred>();
+    preds.add( ep );
+  }
+
+
   public ExistPredSet makeCanonical() {
     return (ExistPredSet) ExistPredSet.makeCanonical( this );
   }
@@ -26,16 +32,24 @@ public class ExistPredSet extends Canonical {
     preds.add( pred );
   }
 
+
+  public ExistPredSet join( ExistPredSet eps ) {
+    this.preds.addAll( eps.preds );
+    return this;
+  }
+
+
   public boolean isSatisfiedBy( ReachGraph rg ) {
     Iterator<ExistPred> predItr = preds.iterator();
     while( predItr.hasNext() ) {
-      if( !predItr.next().isSatisfiedBy( rg ) ) {
-        return false;
+      if( predItr.next().isSatisfiedBy( rg ) ) {
+        return true;
       }
     }
-    return true;
+    return false;
   }
 
+
   public String toString() {
     String s = "P[";
     Iterator<ExistPred> predItr = preds.iterator();

diff --git a/Robust/src/Analysis/Disjoint/ExistPredTrue.java b/Robust/src/Analysis/Disjoint/ExistPredTrue.java
new file mode 100644 (file)
index 0000000..6981284
--- /dev/null
+++ b/Robust/src/Analysis/Disjoint/ExistPredTrue.java
@@ -0,0 +1,23 @@
+package Analysis.Disjoint;
+
+import IR.*;
+import IR.Flat.*;
+import java.util.*;
+import java.io.*;
+
+// these existence predicates on elements of
+// a callee graph allow a caller to prune the
+// pieces of the graph that don't apply when
+// predicates are not satisfied in the
+// caller's context
+
+public class ExistPredTrue extends ExistPred {  
+
+  public boolean isSatisfiedBy( ReachGraph rg ) {    
+    return true;
+  }
+
+  public String toString() {
+    return "t";
+  }
+}

diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java
index 0d014b21192183e82153542d28ca7c93cebcc358..3aba239073d277ff913ca9d6b815bacef44e018c 100644 (file)
--- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java
+++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java
@@ -12,10 +12,6 @@ public class HeapRegionNode extends RefSrcNode {
   protected boolean isFlagged;
   protected boolean isNewSummary;
 
-  // clean means that the node existed
-  // before the current analysis context
-  protected boolean isClean;  
-
   // special nodes that represent heap parts
   // outside of the current method context
   protected boolean isOutOfContext;
@@ -49,7 +45,6 @@ public class HeapRegionNode extends RefSrcNode {
                          boolean        isSingleObject,
                          boolean        isFlagged,
                          boolean        isNewSummary,
-                         boolean        isClean,
                          boolean        isOutOfContext,
                          TypeDescriptor type,
                          AllocSite      allocSite,
@@ -63,7 +58,6 @@ public class HeapRegionNode extends RefSrcNode {
     this.isSingleObject = isSingleObject;
     this.isFlagged      = isFlagged;
     this.isNewSummary   = isNewSummary;
-    this.isClean        = isClean;
     this.isOutOfContext = isOutOfContext;
     this.type           = type;
     this.allocSite      = allocSite;
@@ -81,7 +75,6 @@ public class HeapRegionNode extends RefSrcNode {
                                isSingleObject,
                                isFlagged,
                                isNewSummary,
-                               isClean,
                                isOutOfContext,
                                type,
                                allocSite,
@@ -125,7 +118,6 @@ public class HeapRegionNode extends RefSrcNode {
     assert isSingleObject == hrn.isSingleObject();
     assert isFlagged      == hrn.isFlagged();
     assert isNewSummary   == hrn.isNewSummary();
-    assert isClean        == hrn.isClean();
     assert isOutOfContext == hrn.isOutOfContext();
     assert description.equals( hrn.getDescription() );
 
@@ -153,14 +145,6 @@ public class HeapRegionNode extends RefSrcNode {
     return isOutOfContext;
   }
 
-  public boolean isClean() {
-    return isClean;
-  }
-
-  public void setIsClean( boolean isClean ) {
-    this.isClean = isClean;
-  }
-
 
   public Iterator<RefEdge> iteratorToReferencers() {
     return referencers.iterator();
@@ -246,6 +230,15 @@ public class HeapRegionNode extends RefSrcNode {
   }
 
 
+  public ExistPredSet getPreds() {
+    return preds;
+  }
+
+  public void setPreds( ExistPredSet preds ) {
+    this.preds = preds;
+  }
+
+
   public String getIDString() {
     String s;
 
@@ -258,19 +251,33 @@ public class HeapRegionNode extends RefSrcNode {
     return s;
   }
 
-  public String getAlphaString( boolean hideSubsetReachability ) {
-    return alpha.toStringEscapeNewline( hideSubsetReachability );
-  }
+  public String getDescription() {
+    return description;
+  }  
+
+  public String toStringDOT( boolean hideSubsetReach ) {
+    String attributes = "";
+    
+    if( isSingleObject ) {
+      attributes += "shape=box";
+    } else {
+      attributes += "shape=Msquare";
+    }
 
-  public String getPredString() {
-    return preds.toString();
+    if( isFlagged ) {
+      attributes += ",style=filled,fillcolor=lightgrey";
+    }
+
+    return new String( "["+attributes+
+                       ",label=\"ID"+getIDString()+"\\n"+
+                       type.toPrettyString()+"\\n"+
+                       description+"\\n"+
+                       alpha.toStringEscNewline( hideSubsetReach )+"\\n"+
+                       preds+"\"]"
+                       );
   }
 
   public String toString() {
     return "HRN"+getIDString();
   }
-
-  public String getDescription() {
-    return description;
-  }  
 }

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 7775e64250136ac409f20c930bbf2e242a8d07cb..3fc326665ddf2e8ca30550391d59b72e94d3dbee 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -21,7 +21,9 @@ public class ReachGraph {
   protected static final ReachSet   rsetWithEmptyState = new ReachSet( rstateEmpty ).makeCanonical();
 
   // predicate constants
-  protected static final ExistPredSet predsEmpty = new ExistPredSet().makeCanonical();
+  protected static final ExistPredTrue predTrue   = new ExistPredTrue();
+  protected static final ExistPredSet  predsEmpty = new ExistPredSet().makeCanonical();
+  protected static final ExistPredSet  predsTrue  = new ExistPredSet( predTrue ).makeCanonical();
 
 
   // from DisjointAnalysis for convenience
@@ -71,7 +73,6 @@ public class ReachGraph {
                             boolean        isSingleObject,
                             boolean        isNewSummary,
                             boolean        isFlagged,
-                             boolean        isClean,
                              boolean        isOutOfContext,
                             TypeDescriptor type,
                             AllocSite      allocSite,
@@ -117,7 +118,7 @@ public class ReachGraph {
     }
 
     if( preds == null ) {
-      // TODO: do this right?
+      // TODO: do this right?  For out-of-context nodes?
       preds = new ExistPredSet().makeCanonical();
     }
     
@@ -125,7 +126,6 @@ public class ReachGraph {
                                             isSingleObject,
                                             markForAnalysis,
                                             isNewSummary,
-                                             isClean,
                                              isOutOfContext,
                                             typeToUse,
                                             allocSite,
@@ -361,9 +361,8 @@ public class ReachGraph {
                                        hrnHrn,
                                        tdNewEdge,
                                        null,
-                                       false,
                                        betaY.intersection( betaHrn ),
-                                       predsEmpty
+                                       predsTrue
                                        );
        
        addRefEdge( lnX, hrnHrn, edgeNew );     
@@ -509,9 +508,8 @@ public class ReachGraph {
                                        hrnY,
                                        tdNewEdge,
                                        f.getSymbol(),
-                                       false,
                                        edgeY.getBeta().pruneBy( hrnX.getAlpha() ),
-                                       predsEmpty
+                                       predsTrue
                                        );
 
        // look to see if an edge with same field exists
@@ -524,9 +522,9 @@ public class ReachGraph {
          edgeExisting.setBeta(
                               edgeExisting.getBeta().union( edgeNew.getBeta() )
                                );
-         // we touched this edge in the current context
-          // so dirty it
-         edgeExisting.setIsClean( false );
+          edgeExisting.setPreds(
+                                edgeExisting.getPreds().join( edgeNew.getPreds() )
+                                );
        
         } else {                         
          addRefEdge( hrnX, hrnY, edgeNew );
@@ -595,9 +593,8 @@ public class ReachGraph {
                    hrnNewest,            // dest
                    type,                 // type
                    null,                 // field name
-                   false,                // is initial param
                    hrnNewest.getAlpha(), // beta
-                   predsEmpty            // predicates
+                   predsTrue             // predicates
                    );
 
     addRefEdge( lnX, hrnNewest, edgeNew );
@@ -689,7 +686,9 @@ public class ReachGraph {
 
 
     // after tokens have been aged, reset newest node's reachability
+    // and a brand new node has a "true" predicate
     hrn0.setAlpha( hrn0.getInherent() );
+    hrn0.setPreds( predsTrue );
   }
 
 
@@ -722,7 +721,6 @@ public class ReachGraph {
                                  false,        // single object?                
                                  true,         // summary?      
                                  hasFlags,     // flagged?
-                                 false,        // clean?
                                  false,        // out-of-context?
                                  as.getType(), // type                          
                                  as,           // allocation site                       
@@ -740,7 +738,6 @@ public class ReachGraph {
                                  true,        // single object?                         
                                  false,               // summary?                       
                                  hasFlags,     // flagged?                      
-                                 false,        // clean?
                                  false,        // out-of-context?
                                  as.getType(), // type                          
                                  as,          // allocation site                        
@@ -778,7 +775,6 @@ public class ReachGraph {
                                  false,           // single object?                     
                                  true,           // summary?                    
                                  hasFlags,        // flagged?                              
-                                 false,           // clean?
                                  false,           // out-of-context?
                                  as.getType(),    // type                               
                                  as,             // allocation site                     
@@ -796,7 +792,6 @@ public class ReachGraph {
                                  true,        // single object?                         
                                  false,               // summary?                       
                                  hasFlags,     // flagged?     
-                                 false,        // clean?
                                  false,        // out-of-context?
                                  as.getType(), // type                          
                                  as,          // allocation site                        
@@ -836,6 +831,7 @@ public class ReachGraph {
        // otherwise an edge from the referencer to hrnSummary exists already
        // and the edge referencer->hrn should be merged with it
        edgeMerged.setBeta( edgeMerged.getBeta().union( edgeSummary.getBeta() ) );
+        edgeMerged.setPreds( edgeMerged.getPreds().join( edgeSummary.getPreds() ) );
       }
 
       addRefEdge( hrnSummary, hrnReferencee, edgeMerged );
@@ -861,6 +857,7 @@ public class ReachGraph {
        // otherwise an edge from the referencer to alpha_S exists already
        // and the edge referencer->alpha_K should be merged with it
        edgeMerged.setBeta( edgeMerged.getBeta().union( edgeSummary.getBeta() ) );
+        edgeMerged.setPreds( edgeMerged.getPreds().join( edgeSummary.getPreds() ) );
       }
 
       addRefEdge( onReferencer, hrnSummary, edgeMerged );
@@ -899,8 +896,9 @@ public class ReachGraph {
       addRefEdge( onReferencer, hrnB, edgeNew );
     }
 
-    // replace hrnB reachability with hrnA's
+    // replace hrnB reachability and preds with hrnA's
     hrnB.setAlpha( hrnA.getAlpha() );
+    hrnB.setPreds( hrnA.getPreds() );
   }
 
 
@@ -1122,8 +1120,8 @@ public class ReachGraph {
       VariableNode vnCaller = this.getVariableNodeFromTemp( tdArg );
       VariableNode vnCallee = rg.getVariableNodeFromTemp( tdParam );
       
-      // now traverse the caller view using the argument to
-      // build the callee view which has the parameter symbol
+      // now traverse the calleR view using the argument to
+      // build the calleE view which has the parameter symbol
       Set<RefSrcNode> toVisitInCaller = new HashSet<RefSrcNode>();
       Set<RefSrcNode> visitedInCaller = new HashSet<RefSrcNode>();
       toVisitInCaller.add( vnCaller );
@@ -1135,38 +1133,51 @@ public class ReachGraph {
         toVisitInCaller.remove( rsnCaller );
         visitedInCaller.add( rsnCaller );
         
-        // FIRST - setup the source end of an edge
+        // FIRST - setup the source end of an edge, and
+        // remember the identifying info of the source
+        // to build predicates
+        TempDescriptor tdSrc    = null;
+        Integer        hrnSrcID = null;
 
         if( rsnCaller == vnCaller ) {
           // if the caller node is the param symbol, we
           // have to do this translation for the callee
           rsnCallee = vnCallee;
+          tdSrc     = tdArg;
+
         } else {
           // otherwise the callee-view node is a heap
           // region with the same ID, that may or may
           // not have been created already
           assert rsnCaller instanceof HeapRegionNode;          
 
-          HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller;          
+          HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller;                   hrnSrcID = hrnSrcCaller.getID(); 
 
           if( !callerNodesCopiedToCallee.contains( rsnCaller ) ) {
+            
+            ExistPredNode pred = 
+              new ExistPredNode( hrnSrcID, null );
+
+            ExistPredSet preds = new ExistPredSet();
+            preds.add( pred );
+
             rsnCallee = 
               rg.createNewHeapRegionNode( hrnSrcCaller.getID(),
                                           hrnSrcCaller.isSingleObject(),
                                           hrnSrcCaller.isNewSummary(),
                                           hrnSrcCaller.isFlagged(),
-                                          true,  // clean?
                                           false, // out-of-context?
                                           hrnSrcCaller.getType(),
                                           hrnSrcCaller.getAllocSite(),
                                           toShadowTokens( this, hrnSrcCaller.getInherent() ),
                                           toShadowTokens( this, hrnSrcCaller.getAlpha() ),
-                                          predsEmpty,
+                                          preds,
                                           hrnSrcCaller.getDescription()
                                           );
             callerNodesCopiedToCallee.add( rsnCaller );
+
           } else {
-            rsnCallee = rg.id2hrn.get( hrnSrcCaller.getID() );
+            rsnCallee = rg.id2hrn.get( hrnSrcID );
           }
         }
 
@@ -1179,38 +1190,56 @@ public class ReachGraph {
           HeapRegionNode hrnCallee;
 
           // THIRD - setup destination ends of edges
+          Integer hrnDstID = hrnCaller.getID(); 
 
           if( !callerNodesCopiedToCallee.contains( hrnCaller ) ) {
+
+            ExistPredNode pred = 
+              new ExistPredNode( hrnDstID, null );
+
+            ExistPredSet preds = new ExistPredSet();
+            preds.add( pred );
+            
             hrnCallee = 
               rg.createNewHeapRegionNode( hrnCaller.getID(),
                                           hrnCaller.isSingleObject(),
                                           hrnCaller.isNewSummary(),
                                           hrnCaller.isFlagged(),
-                                          true,  // clean?
                                           false, // out-of-context?
                                           hrnCaller.getType(),
                                           hrnCaller.getAllocSite(),
                                           toShadowTokens( this, hrnCaller.getInherent() ),
                                           toShadowTokens( this, hrnCaller.getAlpha() ),
-                                          predsEmpty,
+                                          preds,
                                           hrnCaller.getDescription()
                                           );
             callerNodesCopiedToCallee.add( hrnCaller );
           } else {
-            hrnCallee = rg.id2hrn.get( hrnCaller.getID() );
+            hrnCallee = rg.id2hrn.get( hrnDstID );
           }
 
           // FOURTH - copy edge over if needed
           if( !callerEdgesCopiedToCallee.contains( reCaller ) ) {
+
+            ExistPredEdge pred =
+              new ExistPredEdge( tdSrc, 
+                                 hrnSrcID, 
+                                 hrnDstID,
+                                 reCaller.getType(),
+                                 reCaller.getField(),
+                                 null );
+
+            ExistPredSet preds = new ExistPredSet();
+            preds.add( pred );
+
             rg.addRefEdge( rsnCallee,
                            hrnCallee,
                            new RefEdge( rsnCallee,
                                         hrnCallee,
                                         reCaller.getType(),
                                         reCaller.getField(),
-                                        true, // clean?
                                         toShadowTokens( this, reCaller.getBeta() ),
-                                        predsEmpty
+                                        preds
                                         )
                            );              
             callerEdgesCopiedToCallee.add( reCaller );
@@ -1261,7 +1290,6 @@ public class ReachGraph {
                                       false, // single object?
                                       false, // new summary?
                                       false, // flagged?
-                                      true,  // clean?
                                       true,  // out-of-context?
                                       hrnCallerAndOutContext.getType(),
                                       null,  // alloc site, shouldn't be used
@@ -1280,7 +1308,6 @@ public class ReachGraph {
                                     hrnCalleeAndInContext,
                                     edgeMightCross.getType(),
                                     edgeMightCross.getField(),
-                                    true, // clean?
                                     toShadowTokens( this, edgeMightCross.getBeta() ),
                                     predsEmpty
                                     )
@@ -1293,7 +1320,7 @@ public class ReachGraph {
       rg.writeGraph( "calleeview", true, true, true, false, true, true );
     } catch( IOException e ) {}
 
-    if( fc.getMethod().getSymbol().equals( "f1" ) ) {
+    if( fc.getMethod().getSymbol().equals( "addSomething" ) ) {
       System.exit( 0 );
     }
 
@@ -1738,10 +1765,12 @@ public class ReachGraph {
        hrnB.setAlpha( hrnB.getAlpha().union( hrnA.getAlpha() ) );
 
         // if hrnB is already dirty or hrnA is dirty,
-        // the hrnB should end up dirty
+        // the hrnB should end up dirty: TODO
+        /*
         if( !hrnA.isClean() ) {
           hrnB.setIsClean( false );
         }
+        */
       }
     }
 
@@ -1817,9 +1846,12 @@ public class ReachGraph {
          edgeToMerge.setBeta(
            edgeToMerge.getBeta().union( edgeA.getBeta() )
            );
+          // TODO: what?
+          /*
          if( !edgeA.isClean() ) {
            edgeToMerge.setIsClean( false );
          }
+          */
        }
       }
     }
@@ -1878,9 +1910,12 @@ public class ReachGraph {
          edgeToMerge.setBeta(
            edgeToMerge.getBeta().union( edgeA.getBeta() )
            );
+          // TODO: what?
+          /*
          if( !edgeA.isClean() ) {
            edgeToMerge.setIsClean( false );
          }
+          */
        }
       }
     }
@@ -2299,8 +2334,6 @@ public class ReachGraph {
             continue;
           }
         }
-
-        //bw.write("  "+vn.toString() + ";\n");
         
         Iterator<RefEdge> heapRegionsItr = vn.iteratorToReferencees();
         while( heapRegionsItr.hasNext() ) {
@@ -2317,10 +2350,10 @@ public class ReachGraph {
                                      hideEdgeTaints );
           }
           
-          bw.write( "  "        + vn.toString() +
-                    " -> "      + hrn.toString() +
-                    "[label=\"" + edge.toGraphEdgeString( hideSubsetReachability ) +
-                    "\",decorate];\n" );
+          bw.write( "  "+vn.toString()+
+                    " -> "+hrn.toString()+
+                    edge.toStringDOT( hideSubsetReachability )+
+                    ";\n" );
         }
       }
     }
@@ -2343,43 +2376,19 @@ public class ReachGraph {
     }
     visited.add( hrn );
 
-    String attributes = "[";
-
-    if( hrn.isSingleObject() ) {
-      attributes += "shape=box";
-    } else {
-      attributes += "shape=Msquare";
-    }
-
-    if( hrn.isFlagged() ) {
-      attributes += ",style=filled,fillcolor=lightgrey";
-    }
-
-    attributes += ",label=\"ID" +
-      hrn.getID() +
-      "\\n";
-
-    if( hrn.getType() != null ) {
-      attributes += hrn.getType().toPrettyString()+"\\n";
-    }
-       
-    attributes += hrn.getDescription()+
-      "\\n"+hrn.getAlphaString( hideSubsetReachability )+      
-      "\\n"+hrn.getPredString()+
-      "\"]";
-
-    bw.write( "  "+hrn.toString()+attributes+";\n" );
-
+    bw.write( "  "+hrn.toString()+
+              hrn.toStringDOT( hideSubsetReachability )+
+              ";\n" );
 
     Iterator<RefEdge> childRegionsItr = hrn.iteratorToReferencees();
     while( childRegionsItr.hasNext() ) {
       RefEdge        edge     = childRegionsItr.next();
       HeapRegionNode hrnChild = edge.getDst();
 
-      bw.write( "  "       +hrn.toString()+
-                " -> "     +hrnChild.toString()+
-                "[label=\""+edge.toGraphEdgeString( hideSubsetReachability )+
-                "\",decorate];\n");
+      bw.write( "  "+hrn.toString()+
+                " -> "+hrnChild.toString()+
+                edge.toStringDOT( hideSubsetReachability )+
+                ";\n");
       
       traverseHeapRegionNodes( hrnChild,
                                bw,

diff --git a/Robust/src/Analysis/Disjoint/ReachSet.java b/Robust/src/Analysis/Disjoint/ReachSet.java
index 7cfced63f0f6484d5e3dc23d17fe5f3c7cdedc07..e62753358892b284b7d14ad69cb949ec14cc09f6 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachSet.java
+++ b/Robust/src/Analysis/Disjoint/ReachSet.java
@@ -486,7 +486,7 @@ public class ReachSet extends Canonical {
   }
 
 
-  public String toStringEscapeNewline( boolean hideSubsetReachability ) {
+  public String toStringEscNewline( boolean hideSubsetReachability ) {
     String s = "[";
 
     Iterator<ReachState> i = this.iterator();

diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java
index 72bd42ccd3e85749e6152c5a629e876df33f3a99..3c186eda5868e4348aebd7879a3b133a03b7005a 100644 (file)
--- a/Robust/src/Analysis/Disjoint/RefEdge.java
+++ b/Robust/src/Analysis/Disjoint/RefEdge.java
@@ -13,10 +13,6 @@ public class RefEdge {
   // edge models a variable reference
   protected String field;
 
-  // clean means that the reference existed
-  // before the current analysis context
-  protected boolean isClean;
-
   protected ReachSet beta;
   protected ReachSet betaNew;
 
@@ -34,7 +30,6 @@ public class RefEdge {
                   HeapRegionNode dst,
                   TypeDescriptor type,
                   String         field,
-                  boolean        isClean,
                   ReachSet       beta,
                   ExistPredSet   preds ) {
     assert type != null;
@@ -43,7 +38,6 @@ public class RefEdge {
     this.dst     = dst;
     this.type    = type;
     this.field   = field;
-    this.isClean = isClean;
 
     if( preds != null ) {
       this.preds = preds;
@@ -69,7 +63,6 @@ public class RefEdge {
                                 dst,
                                 type,
                                 field,
-                                isClean,                               
                                 beta,
                                 preds );
     return copy;
@@ -102,8 +95,6 @@ public class RefEdge {
       return false;
     }
 
-    assert isClean == edge.isClean;
-
     return true;
   }
 
@@ -195,15 +186,6 @@ public class RefEdge {
   }
 
 
-  public boolean isClean() {
-    return isClean;
-  }
-
-  public void setIsClean( boolean isClean ) {
-    this.isClean = isClean;
-  }
-
-
   public ReachSet getBeta() {
     return beta;
   }
@@ -230,29 +212,25 @@ public class RefEdge {
   }
 
 
-  public String toGraphEdgeString( boolean hideSubsetReachability ) {
-    String edgeLabel = "";
-
-    if( type != null ) {
-      edgeLabel += type.toPrettyString() + "\\n";
-    }
+  public ExistPredSet getPreds() {
+    return preds;
+  }
 
-    if( field != null ) {
-      edgeLabel += field + "\\n";
-    }
+  public void setPreds( ExistPredSet preds ) {
+    this.preds = preds;
+  }
 
-    if( isClean ) {
-      edgeLabel += "*clean*\\n";
-    }
 
-    edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability ) +
-      "\\n" + preds.toString();
-      
-    return edgeLabel;
+  public String toStringDOT( boolean hideSubsetReach ) {
+    return new String( "[label=\""+
+                       type.toPrettyString()+"\\n"+
+                       field+"\\n"+
+                       beta.toStringEscNewline( hideSubsetReach )+"\\n"+
+                       preds.toString()+"\",decorate]"
+                       );
   }
 
   public String toString() {
-    assert type != null;
     return new String( "("+src+
                        "->"+type.toPrettyString()+
                        " "+field+

diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java
index 5d618735f07b24a738d049dd1bfcfe35bdbe30ef..004e56120f8725a9a7e5d497d970c8d90257e993 100644 (file)
--- a/Robust/src/IR/State.java
+++ b/Robust/src/IR/State.java
@@ -73,6 +73,7 @@ public class State {
   public int DISJOINTALLOCDEPTH=3;
   public boolean DISJOINTWRITEDOTS=false;
   public boolean DISJOINTWRITEALL=false;
+  public boolean DISJOINTWRITEIHMS=false;
   public String DISJOINTALIASFILE=null;
   public boolean DISJOINTALIASTAB=false;
   public int DISJOINTDEBUGCALLCOUNT=0;

diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index 748c0027fa06bdfcf33a21ecfae53e671574d0e8..d51883f4703d2441d07efccdbeab78efc4ce50e6 100644 (file)
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -165,10 +165,13 @@ public class Main {
       } else if (option.equals("-owndebugcallcount")) {
        state.OWNERSHIPDEBUGCALLCOUNT=Integer.parseInt(args[++i]);
       }
+
       else if (option.equals("-disjoint"))
        state.DISJOINT=true;
+
       else if (option.equals("-disjoint-k")) {
        state.DISJOINTALLOCDEPTH=Integer.parseInt(args[++i]);
+
       } else if (option.equals("-disjoint-write-dots")) {
        state.DISJOINTWRITEDOTS = true;
         String arg = args[++i];
@@ -179,6 +182,10 @@ public class Main {
         } else {
           throw new Error("disjoint-write-dots requires argument <all/final>");
         }
+
+      } else if (option.equals("-disjoint-write-ihms")) {
+       state.DISJOINTWRITEIHMS = true;
+
       } else if (option.equals("-disjoint-alias-file")) {
        state.DISJOINTALIASFILE = args[++i];
         String arg = args[++i];
@@ -189,11 +196,13 @@ public class Main {
         } else {
           throw new Error("disjoint-alias-file requires arguments <filename> <normal/tabbed>");
         }
+
       } else if (option.equals("-disjoint-debug-callsite")) {
        state.DISJOINTDEBUGCALLEE=args[++i];
        state.DISJOINTDEBUGCALLER=args[++i];
        state.DISJOINTDEBUGCALLCOUNT=Integer.parseInt(args[++i]);
       }
+
       else if (option.equals("-optional"))
        state.OPTIONAL=true;
       else if (option.equals("-optimize"))

diff --git a/Robust/src/Tests/disjoint/predicateTest1/makefile b/Robust/src/Tests/disjoint/predicateTest1/makefile
index dcb012af1b6a6059828d47e82d39a4d0a3891d1d..8dcb226e20a0c5a7fa9dad51955c983c85785a81 100644 (file)
--- a/Robust/src/Tests/disjoint/predicateTest1/makefile
+++ b/Robust/src/Tests/disjoint/predicateTest1/makefile
@@ -3,7 +3,7 @@ PROGRAM=test
 SOURCE_FILES=$(PROGRAM).java
 
 BUILDSCRIPT=~/research/Robust/src/buildscript
-BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -disjoint-write-dots final -disjoint-alias-file aliases.txt normal -enable-assertions
+BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -disjoint-write-dots final -disjoint-write-ihms -disjoint-alias-file aliases.txt normal -enable-assertions
 
 all: $(PROGRAM).bin
 

diff --git a/Robust/src/Tests/disjoint/predicateTest2/makefile b/Robust/src/Tests/disjoint/predicateTest2/makefile
new file mode 100644 (file)
index 0000000..8dcb226
--- /dev/null
+++ b/Robust/src/Tests/disjoint/predicateTest2/makefile
@@ -0,0 +1,27 @@
+PROGRAM=test
+
+SOURCE_FILES=$(PROGRAM).java
+
+BUILDSCRIPT=~/research/Robust/src/buildscript
+BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -disjoint-write-dots final -disjoint-write-ihms -disjoint-alias-file aliases.txt normal -enable-assertions
+
+all: $(PROGRAM).bin
+
+view: PNGs
+       eog *.png &
+
+PNGs: DOTs
+       d2p *COMPLETE*.dot
+
+DOTs: $(PROGRAM).bin
+
+$(PROGRAM).bin: $(SOURCE_FILES)
+       $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
+
+clean:
+       rm -f  $(PROGRAM).bin
+       rm -fr tmpbuilddirectory
+       rm -f  *~
+       rm -f  *.dot
+       rm -f  *.png
+       rm -f  aliases.txt

diff --git a/Robust/src/Tests/disjoint/predicateTest2/test.java b/Robust/src/Tests/disjoint/predicateTest2/test.java
new file mode 100644 (file)
index 0000000..28d5be3
--- /dev/null
+++ b/Robust/src/Tests/disjoint/predicateTest2/test.java
@@ -0,0 +1,31 @@
+public class Foo {
+  public Foo() {}
+  public Bar b;
+}
+
+public class Bar {
+  public Bar() {}
+}
+
+public class Test {
+  static public void main( String[] args ) {
+
+    Foo f1 = new Foo();
+    addSomething( f1 );
+
+    Foo f2 = new Foo();
+    addSomething( f2 );
+  }   
+
+  public static void addSomething( Foo f ) {
+    addBar( f );
+  }
+
+  public static void addBar( Foo g ) {
+    if( true ) {
+      g.b = new Bar();
+    } else {
+      g.b = new Bar();
+    }
+  }
+}