From e97f941bdb954537ea57983c5dade2411f27da09 Mon Sep 17 00:00:00 2001
From: jjenista <jjenista>
Date: Wed, 31 Mar 2010 17:21:08 +0000
Subject: [PATCH] enforce strict monotonicity for initial method contexts and
 back edges as defined by the PointerMethod, which allow the nonterminating
 test cases to converge now.  Still gotta test on the wider benchmark suite...

---
 .../Analysis/Disjoint/DisjointAnalysis.java   | 44 ++++++++++++++++---
 .../src/Analysis/Disjoint/PointerMethod.java  |  5 +++
 Robust/src/Analysis/Disjoint/ReachGraph.java  | 17 -------
 3 files changed, 42 insertions(+), 24 deletions(-)

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index 81eeb496..152ddd80 100644
--- 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 1062c163..372a0fca 100644
--- 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 d61a76c7..3645338e 100644
--- 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
-- 
2.34.1