enforce strict monotonicity for initial method contexts and back edges as defined...

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index 81eeb49602710240b3a7f4cbd3e96f159865b90c..152ddd8090cefe6a3a4692946075d8ab34c3fe10 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -410,6 +410,20 @@ public class DisjointAnalysis {
   protected Hashtable< Descriptor, Hashtable< FlatCall, ReachGraph > >
     mapDescriptorToIHMcontributions;
 
+  // additionally, keep a mapping from descriptors to the
+  // merged in-coming initial context, because we want this
+  // initial context to be STRICTLY MONOTONIC
+  protected Hashtable<Descriptor, ReachGraph>
+    mapDescriptorToInitialContext;
+
+  // make the result for back edges analysis-wide STRICTLY
+  // MONOTONIC as well, but notice we use FlatNode as the
+  // key for this map: in case we want to consider other
+  // nodes as back edge's in future implementations
+  protected Hashtable<FlatNode, ReachGraph>
+    mapBackEdgeToMonotone;
+  
+
   public static final String arrayElementFieldName = "___element_";
   static protected Hashtable<TypeDescriptor, FieldDescriptor>
     mapTypeToArrayField;
@@ -454,6 +468,12 @@ public class DisjointAnalysis {
     mapDescriptorToIHMcontributions =
       new Hashtable< Descriptor, Hashtable< FlatCall, ReachGraph > >();
 
+    mapDescriptorToInitialContext =
+      new Hashtable<Descriptor, ReachGraph>();    
+
+    mapBackEdgeToMonotone =
+      new Hashtable<FlatNode, ReachGraph>();
+
     mapHrnIdToAllocSite =
       new Hashtable<Integer, AllocSite>();
 
@@ -888,14 +908,17 @@ public class DisjointAnalysis {
 
         assert fc.getMethod().equals( d );
 
-        // some call sites are in same method context though,
-        // and all of them should be merged together first,
-        // then heaps from different contexts should be merged
-        // THIS ASSUMES DIFFERENT CONTEXTS NEED SPECIAL CONSIDERATION!
-        // such as, do allocation sites need to be aged?
-
-        rg.merge_diffMethodContext( rgContrib );
+        rg.merge( rgContrib );
       }
+
+      // additionally, we are enforcing STRICT MONOTONICITY for the
+      // method's initial context, so grow the context by whatever
+      // the previously computed context was, and put the most
+      // up-to-date context back in the map
+      ReachGraph rgPrevContext = mapDescriptorToInitialContext.get( d );
+      rg.merge( rgPrevContext );      
+      mapDescriptorToInitialContext.put( d, rg );
+
     } break;
       
     case FKind.FlatOpNode:
@@ -1109,6 +1132,13 @@ public class DisjointAnalysis {
     //rg.abstractGarbageCollect();
     //rg.globalSweep();
 
+
+    // back edges are strictly monotonic
+    if( pm.isBackEdge( fn ) ) {
+      ReachGraph rgPrevResult = mapBackEdgeToMonotone.get( fn );
+      rg.merge( rgPrevResult );
+      mapBackEdgeToMonotone.put( fn, rg );
+    }
     
     // at this point rg should be the correct update
     // by an above transfer function, or untouched if

diff --git a/Robust/src/Analysis/Disjoint/PointerMethod.java b/Robust/src/Analysis/Disjoint/PointerMethod.java
index 1062c1635698285f41c62f4a5396cc6226f4b387..372a0fcac1a829ec8db9b2a1ff283c5684cef092 100644 (file)
--- a/Robust/src/Analysis/Disjoint/PointerMethod.java
+++ b/Robust/src/Analysis/Disjoint/PointerMethod.java
@@ -80,6 +80,10 @@ public class PointerMethod {
     return prevmap.get(fn).get(i);
   }
 
+  public boolean isBackEdge(FlatNode fn) {
+    return fn.kind() == FKind.FlatBackEdge;
+  }
+
   public boolean analysisCares(FlatNode fn) {
     switch(fn.kind()) {
     case FKind.FlatMethod:
@@ -90,6 +94,7 @@ public class PointerMethod {
     case FKind.FlatNew:
     case FKind.FlatCall:
     case FKind.FlatReturnNode:
+    case FKind.FlatBackEdge:
       return true;
     case FKind.FlatCastNode:
       FlatCastNode fcn=(FlatCastNode)fn;

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index d61a76c7a44afeac3003c9b6a8a6f8bb2f6ef473..3645338efa767b43e96fd1a3ab2c78c870c483e3 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -3374,23 +3374,6 @@ public class ReachGraph {
 
 
 
-  ////////////////////////////////////////////////////
-  // high-level merge operations
-  ////////////////////////////////////////////////////
-  public void merge_sameMethodContext( ReachGraph rg ) {
-    // when merging two graphs that abstract the heap
-    // of the same method context, we just call the
-    // basic merge operation
-    merge( rg );
-  }
-
-  public void merge_diffMethodContext( ReachGraph rg ) {
-    // when merging graphs for abstract heaps in
-    // different method contexts we should:
-    // 1) age the allocation sites?
-    merge( rg );
-  }
-
   ////////////////////////////////////////////////////
   // in merge() and equals() methods the suffix A
   // represents the passed in graph and the suffix