run ooojava and rcrpointer that print out effects and annotate them with the source...
[IRC.git] / Robust / src / Analysis / Disjoint / HeapRegionNode.java
index ac729a20b1adc343e130935fbcc2615415d47bb3..ed7e101f577551fbc69fdcc195549ad005410467 100644 (file)
@@ -3,6 +3,7 @@ package Analysis.Disjoint;
 import IR.*;
 import IR.Flat.*;
 import java.util.*;
+import java.io.*;
 
 public class HeapRegionNode extends RefSrcNode {
 
@@ -10,60 +11,77 @@ public class HeapRegionNode extends RefSrcNode {
 
   protected boolean isSingleObject;
   protected boolean isFlagged;
-  protected boolean isParameter;
   protected boolean isNewSummary;
 
+  // special nodes that represent heap parts
+  // outside of the current method context
+  protected boolean isOutOfContext;
+
   protected HashSet<RefEdge> referencers;
 
   protected TypeDescriptor type;
 
   protected AllocSite allocSite;
 
+  // some reachability states are inherent
+  // to a node by its definition
+  protected ReachSet inherent;
+
+  // use alpha for the current reach states
+  // and alphaNew during iterative calculations
+  // to update alpha
   protected ReachSet alpha;
   protected ReachSet alphaNew;
 
   protected String description;
-  
-  protected String globalIdentifier;
 
+  // existence predicates must be true in a caller
+  // context for this node to transfer from this
+  // callee to that context
+  protected ExistPredSet preds;
 
 
   public HeapRegionNode(Integer id,
                         boolean isSingleObject,
                         boolean isFlagged,
-                       boolean isParameter,
                         boolean isNewSummary,
-                       TypeDescriptor type,
+                        boolean isOutOfContext,
+                        TypeDescriptor type,
                         AllocSite allocSite,
+                        ReachSet inherent,
                         ReachSet alpha,
-                        String description,
-                        String globalIdentifier) {
-    this.id = id;
+                        ExistPredSet preds,
+                        String description
+                        ) {
+
+    this.id             = id;
     this.isSingleObject = isSingleObject;
     this.isFlagged      = isFlagged;
-    this.isParameter    = isParameter;
     this.isNewSummary   = isNewSummary;
+    this.isOutOfContext = isOutOfContext;
     this.type           = type;
     this.allocSite      = allocSite;
+    this.inherent       = inherent;
     this.alpha          = alpha;
+    this.preds          = preds;
     this.description    = description;
-    this.globalIdentifier = globalIdentifier;
 
     referencers = new HashSet<RefEdge>();
-    alphaNew    = new ReachSet().makeCanonical();
+    alphaNew    = ReachSet.factory();
   }
 
   public HeapRegionNode copy() {
     return new HeapRegionNode(id,
                               isSingleObject,
                               isFlagged,
-                             isParameter,
                               isNewSummary,
-                             type,
+                              isOutOfContext,
+                              type,
                               allocSite,
+                              inherent,
                               alpha,
-                              description,
-                              globalIdentifier);
+                              preds,
+                              description);
   }
 
 
@@ -72,8 +90,14 @@ public class HeapRegionNode extends RefSrcNode {
   }
 
 
-  public boolean equalsIncludingAlpha(HeapRegionNode hrn) {
-    return equals(hrn) && alpha.equals(hrn.alpha);
+  // alpha and preds contribute towards reaching the
+  // fixed point, so use this method to determine if
+  // a node is "equal" to some previous visit, basically
+  public boolean equalsIncludingAlphaAndPreds(HeapRegionNode hrn) {
+
+    return equals(hrn) &&
+           alpha.equals(hrn.alpha) &&
+           preds.equals(hrn.preds);
   }
 
 
@@ -82,7 +106,7 @@ public class HeapRegionNode extends RefSrcNode {
       return false;
     }
 
-    if( !( o instanceof HeapRegionNode) ) {
+    if( !(o instanceof HeapRegionNode) ) {
       return false;
     }
 
@@ -94,9 +118,9 @@ public class HeapRegionNode extends RefSrcNode {
 
     assert isSingleObject == hrn.isSingleObject();
     assert isFlagged      == hrn.isFlagged();
-    assert isParameter    == hrn.isParameter();
     assert isNewSummary   == hrn.isNewSummary();
-    assert description.equals(hrn.getDescription() );
+    assert isOutOfContext == hrn.isOutOfContext();
+    //assert description.equals( hrn.getDescription() );
 
     return true;
   }
@@ -114,14 +138,13 @@ public class HeapRegionNode extends RefSrcNode {
     return isFlagged;
   }
 
-  public boolean isParameter() {
-    return isParameter;
-  }
-
   public boolean isNewSummary() {
     return isNewSummary;
   }
 
+  public boolean isOutOfContext() {
+    return isOutOfContext;
+  }
 
 
   public Iterator<RefEdge> iteratorToReferencers() {
@@ -138,6 +161,15 @@ public class HeapRegionNode extends RefSrcNode {
   }
 
 
+  // in other words, this node is not functionally
+  // part of the graph (anymore)
+  public boolean isWiped() {
+    return
+      getNumReferencers() == 0 &&
+      getNumReferencees() == 0;
+  }
+
+
   public void addReferencer(RefEdge edge) {
     assert edge != null;
 
@@ -151,18 +183,21 @@ public class HeapRegionNode extends RefSrcNode {
     referencers.remove(edge);
   }
 
-  public RefEdge getReferenceFrom(RefSrcNode on,
-                                        TypeDescriptor type,
-                                       String field) {
-    assert on != null;
+  public RefEdge getReferenceFrom(RefSrcNode rsn,
+                                  TypeDescriptor type,
+                                  String field
+                                  ) {
+    assert rsn != null;
 
     Iterator<RefEdge> itrEdge = referencers.iterator();
     while( itrEdge.hasNext() ) {
       RefEdge edge = itrEdge.next();
-      if( edge.getSrc().equals(on) &&
-         edge.typeEquals(type) &&
-          edge.fieldEquals(field) ) {
-       return edge;
+
+      if( edge.getSrc().equals(rsn) &&
+          edge.typeEquals(type)     &&
+          edge.fieldEquals(field)
+          ) {
+        return edge;
       }
     }
 
@@ -172,21 +207,25 @@ public class HeapRegionNode extends RefSrcNode {
 
   public TypeDescriptor getType() {
     return type;
-  }  
+  }
 
   public AllocSite getAllocSite() {
     return allocSite;
   }
 
 
-  public void setAlpha(ReachSet alpha) {
-    this.alpha = alpha;
+  public ReachSet getInherent() {
+    return inherent;
   }
 
   public ReachSet getAlpha() {
     return alpha;
   }
 
+  public void setAlpha(ReachSet alpha) {
+    this.alpha = alpha;
+  }
+
   public ReachSet getAlphaNew() {
     return alphaNew;
   }
@@ -198,7 +237,40 @@ public class HeapRegionNode extends RefSrcNode {
   public void applyAlphaNew() {
     assert alphaNew != null;
     alpha = alphaNew;
-    alphaNew = new ReachSet().makeCanonical();
+    alphaNew = ReachSet.factory();
+  }
+
+
+  public ExistPredSet getPreds() {
+    return preds;
+  }
+
+  public void setPreds(ExistPredSet preds) {
+    this.preds = preds;
+  }
+
+
+  // use this method to assert that an out-of-context
+  // heap region node has only out-of-context symbols
+  // in its reachability
+  public boolean reachHasOnlyOOC() {
+    assert isOutOfContext;
+
+    Iterator<ReachState> stateItr = alpha.iterator();
+    while( stateItr.hasNext() ) {
+      ReachState state = stateItr.next();
+
+      Iterator<ReachTuple> rtItr = state.iterator();
+      while( rtItr.hasNext() ) {
+        ReachTuple rt = rtItr.next();
+
+        if( !rt.isOutOfContext() ) {
+          return false;
+        }
+      }
+    }
+
+    return true;
   }
 
 
@@ -214,21 +286,50 @@ public class HeapRegionNode extends RefSrcNode {
     return s;
   }
 
-  public String getAlphaString( boolean hideSubsetReachability ) {
-    return alpha.toStringEscapeNewline(hideSubsetReachability);
+  public String getDescription() {
+    return description;
   }
 
-  public String toString() {
-    return "HRN"+getIDString();
-  }
+  public String toStringDOT(boolean hideReach,
+                            boolean hideSubsetReach,
+                            boolean hidePreds) {
+    String attributes = "";
 
-  // WHY WHY WHY WHY WHY WHY?!
-  public String getDescription() {
-    return new String(description);
-    //return new String( description+" ID "+getIDString() );
+    if( isSingleObject ) {
+      attributes += "shape=box";
+    } else {
+      attributes += "shape=Msquare";
+    }
+
+    if( isFlagged ) {
+      attributes += ",style=filled,fillcolor=lightgrey";
+    }
+
+    String typeStr;
+    if( type == null ) {
+      typeStr = "null";
+    } else {
+      typeStr = type.toPrettyString();
+    }
+
+    String s =
+      "["+attributes+
+      ",label=\"ID"+getIDString()+"\\n"+
+      typeStr+"\\n"+
+      description;
+
+    if( !hideReach ) {
+      s += "\\n"+alpha.toStringEscNewline(hideSubsetReach);
+    }
+
+    if( !hidePreds ) {
+      s += "\\n"+preds.toStringEscNewline();
+    }
+
+    return s+"\"]";
   }
-  
-  public String getGloballyUniqueIdentifier(){
-         return globalIdentifier;
+
+  public String toString() {
+    return "HRN"+getIDString();
   }
 }