more implementation

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index ffec0c9b9830dd27f2d733a42ffe7b12405bbe0e..d85979c1d36209f9dd95d7693e8e4ca035aa3983 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -565,7 +565,7 @@ public class DisjointAnalysis {
         }
       }
 
-      // now that we've got that taken care of, go ahead and update
+      // now that we've taken care of that, go ahead and update
       // the reach graph for this FlatCall node by whatever callee
       // result we do have
       

diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java
index 9817c5f3ce62291c42213554cfc998975c76ba5c..f190fae09245f1929ec9ce20e621761d7c76ca37 100644 (file)
--- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java
+++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java
@@ -12,12 +12,23 @@ 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;  
+
   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;
 
@@ -28,8 +39,10 @@ public class HeapRegionNode extends RefSrcNode {
                          boolean        isSingleObject,
                          boolean        isFlagged,
                          boolean        isNewSummary,
+                         boolean        isClean,
                          TypeDescriptor type,
                          AllocSite      allocSite,
+                         ReachSet       inherent,
                          ReachSet       alpha,
                          String         description
                          ) {
@@ -37,8 +50,10 @@ public class HeapRegionNode extends RefSrcNode {
     this.isSingleObject = isSingleObject;
     this.isFlagged      = isFlagged;
     this.isNewSummary   = isNewSummary;
+    this.isClean        = isClean;
     this.type           = type;
     this.allocSite      = allocSite;
+    this.inherent       = inherent;
     this.alpha          = alpha;
     this.description    = description;
 
@@ -51,8 +66,10 @@ public class HeapRegionNode extends RefSrcNode {
                                isSingleObject,
                                isFlagged,
                                isNewSummary,
+                               isClean,
                                type,
                                allocSite,
+                               inherent,
                                alpha,
                                description );
   }
@@ -86,6 +103,7 @@ public class HeapRegionNode extends RefSrcNode {
     assert isSingleObject == hrn.isSingleObject();
     assert isFlagged      == hrn.isFlagged();
     assert isNewSummary   == hrn.isNewSummary();
+    assert isClean        == hrn.isClean();
     assert description.equals( hrn.getDescription() );
 
     return true;
@@ -108,6 +126,14 @@ public class HeapRegionNode extends RefSrcNode {
     return isNewSummary;
   }
 
+  public boolean isClean() {
+    return isClean();
+  }
+
+  public void setIsClean( boolean isClean ) {
+    this.isClean = isClean;
+  }
+
 
   public Iterator<RefEdge> iteratorToReferencers() {
     return referencers.iterator();
@@ -165,6 +191,11 @@ public class HeapRegionNode extends RefSrcNode {
     return allocSite;
   }
 
+  
+  public ReachSet getInherent() {
+    return inherent;
+  }
+  
   public ReachSet getAlpha() {
     return alpha;
   }
@@ -209,7 +240,6 @@ public class HeapRegionNode extends RefSrcNode {
   }
 
   public String getDescription() {
-    //return new String(description);
     return description;
   }  
 }

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 068c5a963a53bced7f1b7ebc9933e2f27ae89bd0..97b99a95391109c59aba9fa9a92079343941b96c 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -76,8 +76,10 @@ public class ReachGraph {
                             boolean isSingleObject,
                             boolean isNewSummary,
                             boolean isFlagged,
+                             boolean isClean,
                             TypeDescriptor type,
                             AllocSite allocSite,
+                             ReachSet inherent,
                             ReachSet alpha,
                             String description
                              ) {
@@ -100,25 +102,31 @@ public class ReachGraph {
       id = DisjointAnalysis.generateUniqueHeapRegionNodeID();
     }
 
-    if( alpha == null ) {
+    if( inherent == null ) {
       if( markForAnalysis ) {
-       alpha = new ReachSet(
-                            new ReachTuple( id,
-                                            !isSingleObject,
-                                            ReachTuple.ARITY_ONE
-                                            ).makeCanonical()
-                            ).makeCanonical();
+       inherent = new ReachSet(
+                                new ReachTuple( id,
+                                                !isSingleObject,
+                                                ReachTuple.ARITY_ONE
+                                                ).makeCanonical()
+                                ).makeCanonical();
       } else {
-       alpha = rsetWithEmptyState;
+       inherent = rsetWithEmptyState;
       }
     }
+
+    if( alpha == null ) {
+      alpha = inherent;
+    }
     
     HeapRegionNode hrn = new HeapRegionNode( id,
                                             isSingleObject,
                                             markForAnalysis,
                                             isNewSummary,
+                                             isClean,
                                             typeToUse,
                                             allocSite,
+                                             inherent,
                                             alpha,
                                             description );
     id2hrn.put( id, hrn );
@@ -532,9 +540,9 @@ public class ReachGraph {
          edgeExisting.setBeta(
                               edgeExisting.getBeta().union( edgeNew.getBeta() )
                                );
-         // a new edge here cannot be reflexive, so existing will
-         // always be also not reflexive anymore
-         edgeExisting.setIsInitialParam( false );
+         // we touched this edge in the current context
+          // so dirty it
+         edgeExisting.setIsClean( false );
        
         } else {                         
          addRefEdge( hrnX, hrnY, edgeNew );
@@ -741,9 +749,11 @@ public class ReachGraph {
                                  false,        // single object?                
                                  true,         // summary?      
                                  hasFlags,     // flagged?
+                                 false,        // dirty?
                                  as.getType(), // type                          
                                  as,           // allocation site                       
-                                 null,         // reachability set                 
+                                 null,         // inherent reach
+                                 null,         // current reach                 
                                  strDesc       // description
                                  );
                                  
@@ -755,9 +765,11 @@ public class ReachGraph {
                                  true,        // single object?                         
                                  false,               // summary?                       
                                  hasFlags,     // flagged?                      
+                                 false,        // dirty?
                                  as.getType(), // type                          
                                  as,          // allocation site                        
-                                 null,        // reachability set                 
+                                 null,         // inherent reach
+                                 null,        // current reach
                                  strDesc       // description
                                  );
       }
@@ -789,9 +801,11 @@ public class ReachGraph {
                                  false,           // single object?                     
                                  true,           // summary?                    
                                  hasFlags,        // flagged?                              
+                                 false,           // dirty?
                                  as.getType(),    // type                               
                                  as,             // allocation site                     
-                                 null,           // reachability set                 
+                                 null,            // inherent reach
+                                 null,           // current reach
                                  strDesc          // description
                                  );
 
@@ -802,10 +816,12 @@ public class ReachGraph {
        createNewHeapRegionNode( idShadowIth,  // id or null to generate a new one 
                                  true,        // single object?                         
                                  false,               // summary?                       
-                                 hasFlags,     // flagged?                     
+                                 hasFlags,     // flagged?     
+                                 false,        // dirty?
                                  as.getType(), // type                          
                                  as,          // allocation site                        
-                                 null,        // reachability set                 
+                                 null,         // inherent reach
+                                 null,        // current reach                 
                                  strDesc       // description
                                  );
       }
@@ -2943,6 +2959,12 @@ public class ReachGraph {
        // nodes' reachability sets
        HeapRegionNode hrnB = id2hrn.get( idA );
        hrnB.setAlpha( hrnB.getAlpha().union( hrnA.getAlpha() ) );
+
+        // if hrnB is already dirty or hrnA is dirty,
+        // the hrnB should end up dirty
+        if( !hrnA.isClean() ) {
+          hrnB.setIsClean( false );
+        }
       }
     }
 
@@ -3018,8 +3040,8 @@ public class ReachGraph {
          edgeToMerge.setBeta(
            edgeToMerge.getBeta().union( edgeA.getBeta() )
            );
-         if( !edgeA.isInitialParam() ) {
-           edgeToMerge.setIsInitialParam( false );
+         if( !edgeA.isClean() ) {
+           edgeToMerge.setIsClean( false );
          }
        }
       }
@@ -3079,8 +3101,8 @@ public class ReachGraph {
          edgeToMerge.setBeta(
            edgeToMerge.getBeta().union( edgeA.getBeta() )
            );
-         if( !edgeA.isInitialParam() ) {
-           edgeToMerge.setIsInitialParam( false );
+         if( !edgeA.isClean() ) {
+           edgeToMerge.setIsClean( false );
          }
        }
       }
@@ -3400,8 +3422,10 @@ public class ReachGraph {
                                           hrnSrcCaller.isSingleObject(),
                                           hrnSrcCaller.isNewSummary(),
                                           hrnSrcCaller.isFlagged(),
+                                          true, // clean
                                           hrnSrcCaller.getType(),
                                           hrnSrcCaller.getAllocSite(),
+                                          hrnSrcCaller.getInherent(),
                                           hrnSrcCaller.getAlpha(),
                                           hrnSrcCaller.getDescription()
                                           );
@@ -3427,8 +3451,10 @@ public class ReachGraph {
                                           hrnCaller.isSingleObject(),
                                           hrnCaller.isNewSummary(),
                                           hrnCaller.isFlagged(),
+                                          true, // clean
                                           hrnCaller.getType(),
                                           hrnCaller.getAllocSite(),
+                                          hrnCaller.getInherent(),
                                           hrnCaller.getAlpha(),
                                           hrnCaller.getDescription()
                                           );

diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java
index 9134f33b345fb22481787cca85ff6b968d0364f1..30c7a6116d7dc8239ce195b089a0e6005fdf8011 100644 (file)
--- a/Robust/src/Analysis/Disjoint/RefEdge.java
+++ b/Robust/src/Analysis/Disjoint/RefEdge.java
@@ -13,7 +13,9 @@ public class RefEdge {
   // edge models a variable reference
   protected String field;
 
-  protected boolean isInitialParam;
+  // clean means that the reference existed
+  // before the current analysis context
+  protected boolean isClean;
 
   protected ReachSet beta;
   protected ReachSet betaNew;
@@ -26,15 +28,15 @@ public class RefEdge {
                   HeapRegionNode dst,
                   TypeDescriptor type,
                   String         field,
-                  boolean        isInitialParam,
+                  boolean        isClean,
                   ReachSet       beta ) {
     assert type != null;
 
-    this.src             = src;
-    this.dst             = dst;
-    this.type            = type;
-    this.field           = field;
-    this.isInitialParam  = isInitialParam;
+    this.src     = src;
+    this.dst     = dst;
+    this.type    = type;
+    this.field   = field;
+    this.isClean = isClean;
 
     if( beta != null ) {
       this.beta = beta;
@@ -53,7 +55,7 @@ public class RefEdge {
                                 dst,
                                 type,
                                 field,
-                                isInitialParam,
+                                isClean,
                                 beta );
     return copy;
   }
@@ -85,6 +87,8 @@ public class RefEdge {
       return false;
     }
 
+    assert isClean == edge.isClean;
+
     return true;
   }
 
@@ -167,12 +171,12 @@ public class RefEdge {
   }
 
 
-  public boolean isInitialParam() {
-    return isInitialParam;
+  public boolean isClean() {
+    return isClean;
   }
 
-  public void setIsInitialParam( boolean isInitialParam ) {
-    this.isInitialParam = isInitialParam;
+  public void setIsClean( boolean isClean ) {
+    this.isClean = isClean;
   }
 
 
@@ -213,8 +217,8 @@ public class RefEdge {
       edgeLabel += field + "\\n";
     }
 
-    if( isInitialParam ) {
-      edgeLabel += "*init*\\n";
+    if( isClean ) {
+      edgeLabel += "*clean*\\n";
     }
 
     edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability );

diff --git a/Robust/src/Tests/disjoint/simple/test.java b/Robust/src/Tests/disjoint/simple/test.java
index 4a89947a1b4deacda58d517bd52dca4b16b5497b..c6b136c4872212da17f813063167ffc1a692853b 100644 (file)
--- a/Robust/src/Tests/disjoint/simple/test.java
+++ b/Robust/src/Tests/disjoint/simple/test.java
@@ -6,10 +6,12 @@ public class Foo {
 public class Test {
   static public void main( String[] args ) {
     Foo a = new Foo();
-    a.f = new Foo();
     f1( a );
   }
    
   static public void f1( Foo b ) {
+    Foo c = new Foo();
+    b.f = c;
+    f1( c );
   }
 }