add option to graph visualization that supresses reachability subsets, for improved...

diff --git a/Robust/src/Analysis/OwnershipAnalysis/HeapRegionNode.java b/Robust/src/Analysis/OwnershipAnalysis/HeapRegionNode.java
index d245970c326a035962a5081242e436a95eb76ae0..71db77b17c8892d6726f33fcfa9a54d7dae66072 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/HeapRegionNode.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/HeapRegionNode.java
@@ -209,8 +209,8 @@ public class HeapRegionNode extends OwnershipNode {
     return s;
   }
 
-  public String getAlphaString() {
-    return alpha.toStringEscapeNewline();
+  public String getAlphaString( boolean hideSubsetReachability ) {
+    return alpha.toStringEscapeNewline(hideSubsetReachability);
   }
 
   public String toString() {

diff --git a/Robust/src/Analysis/OwnershipAnalysis/OwnershipAnalysis.java b/Robust/src/Analysis/OwnershipAnalysis/OwnershipAnalysis.java
index 4f1c4d9f402393de2cb8b171dc13cfdab29dc15c..19e5f5f89f657be4bdac8b70a829a9879e81ac37 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/OwnershipAnalysis.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/OwnershipAnalysis.java
@@ -1015,7 +1015,7 @@ public class OwnershipAnalysis {
       }
       Integer n = mapMethodContextToNumUpdates.get(mc);
       try {
-       og.writeGraph(mc, n, true, true, true, false, false);
+       og.writeGraph(mc, n, true, true, true, false, false, true);
       } catch( IOException e ) {}
       mapMethodContextToNumUpdates.put(mc, n + 1);
     }
@@ -1048,6 +1048,7 @@ public class OwnershipAnalysis {
     // boolean pruneGarbage,
     // boolean writeReferencers
     // boolean writeParamMappings
+    // boolean hideSubsetReachability
 
     Set entrySet = mapMethodContextToCompleteOwnershipGraph.entrySet();
     Iterator itr = entrySet.iterator();
@@ -1057,7 +1058,7 @@ public class OwnershipAnalysis {
       OwnershipGraph og = (OwnershipGraph) me.getValue();
 
       try {
-       og.writeGraph(mc, true, true, true, false, false);
+       og.writeGraph(mc, true, true, true, false, false, true);
       } catch( IOException e ) {}    
     }
   }

diff --git a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
index 5b7dc3cf8c1b1edf696114e9263d4c836f16ec1f..8aa559caa5cccabea0a47761ffbb53a0df9ef3ec 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
@@ -4489,6 +4489,25 @@ public class OwnershipGraph {
                );
   }
 
+  public void writeGraph(MethodContext mc,
+                         boolean writeLabels,
+                         boolean labelSelect,
+                         boolean pruneGarbage,
+                         boolean writeReferencers,
+                         boolean writeParamMappings,
+                         boolean hideSubsetReachability
+                         ) throws java.io.IOException {
+
+    writeGraph(mc+"COMPLETE",
+               writeLabels,
+               labelSelect,
+               pruneGarbage,
+               writeReferencers,
+               writeParamMappings,
+               hideSubsetReachability
+               );
+  }
+
   public void writeGraph(MethodContext mc,
                          Integer numUpdate,
                          boolean writeLabels,
@@ -4498,14 +4517,32 @@ public class OwnershipGraph {
                          boolean writeParamMappings
                          ) throws java.io.IOException {
 
+    writeGraph(mc+"COMPLETE"+String.format("%05d", numUpdate),
+               writeLabels,
+               labelSelect,
+               pruneGarbage,
+               writeReferencers,
+               writeParamMappings
+               );
+  }
 
+  public void writeGraph(MethodContext mc,
+                         Integer numUpdate,
+                         boolean writeLabels,
+                         boolean labelSelect,
+                         boolean pruneGarbage,
+                         boolean writeReferencers,
+                         boolean writeParamMappings,
+                         boolean hideSubsetReachability
+                         ) throws java.io.IOException {
 
     writeGraph(mc+"COMPLETE"+String.format("%05d", numUpdate),
                writeLabels,
                labelSelect,
                pruneGarbage,
                writeReferencers,
-               writeParamMappings
+               writeParamMappings,
+               hideSubsetReachability
                );
   }
 
@@ -4516,6 +4553,24 @@ public class OwnershipGraph {
                          boolean writeReferencers,
                          boolean writeParamMappings
                          ) throws java.io.IOException {
+    writeGraph(graphName,
+               writeLabels,
+               labelSelect,
+               pruneGarbage,
+               writeReferencers,
+               writeParamMappings,
+               false
+               );
+  }
+
+  public void writeGraph(String graphName,
+                         boolean writeLabels,
+                         boolean labelSelect,
+                         boolean pruneGarbage,
+                         boolean writeReferencers,
+                         boolean writeParamMappings,
+                         boolean hideSubsetReachability
+                         ) throws java.io.IOException {
 
     // remove all non-word characters from the graph name so
     // the filename and identifier in dot don't cause errors
@@ -4544,7 +4599,8 @@ public class OwnershipGraph {
                                  bw,
                                  null,
                                  visited,
-                                 writeReferencers);
+                                 writeReferencers,
+                                  hideSubsetReachability);
        }
       }
     }
@@ -4599,12 +4655,13 @@ public class OwnershipGraph {
                                    bw,
                                    null,
                                    visited,
-                                   writeReferencers);
+                                   writeReferencers,
+                                    hideSubsetReachability);
          }
 
          bw.write("  "        + ln.toString() +
                   " -> "      + hrn.toString() +
-                  "[label=\"" + edge.toGraphEdgeString() +
+                  "[label=\"" + edge.toGraphEdgeString(hideSubsetReachability) +
                   "\",decorate];\n");
        }
       }
@@ -4620,7 +4677,8 @@ public class OwnershipGraph {
                                          BufferedWriter bw,
                                          TempDescriptor td,
                                          HashSet<HeapRegionNode> visited,
-                                         boolean writeReferencers
+                                         boolean writeReferencers,
+                                         boolean hideSubsetReachability
                                          ) throws java.io.IOException {
 
     if( visited.contains(hrn) ) {
@@ -4653,7 +4711,7 @@ public class OwnershipGraph {
        
       attributes += hrn.getDescription() +
                    "\\n"                +
-                    hrn.getAlphaString() +
+                    hrn.getAlphaString(hideSubsetReachability) +
                     "\"]";
 
       bw.write("  " + hrn.toString() + attributes + ";\n");
@@ -4690,7 +4748,7 @@ public class OwnershipGraph {
       case VISIT_HRN_WRITE_FULL:
        bw.write("  "        + hrn.toString() +
                 " -> "      + hrnChild.toString() +
-                "[label=\"" + edge.toGraphEdgeString() +
+                "[label=\"" + edge.toGraphEdgeString(hideSubsetReachability) +
                 "\",decorate];\n");
        break;
       }
@@ -4700,7 +4758,8 @@ public class OwnershipGraph {
                               bw,
                               td,
                               visited,
-                              writeReferencers);
+                              writeReferencers,
+                              hideSubsetReachability);
     }
   }
   

diff --git a/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java b/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java
index acee806800aff4793f8ab251e6038074be93cca4..f4fabab620e83c526de754dee23304cff839a485 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java
@@ -78,18 +78,33 @@ public class ReachabilitySet extends Canonical {
     return false;    
   }
 
+
   public boolean containsSuperSet(TokenTupleSet tts) {
+    return containsSuperSet( tts, false );
+  }
+
+  public boolean containsStrictSuperSet(TokenTupleSet tts) {
+    return containsSuperSet( tts, true );
+  }
+
+  public boolean containsSuperSet(TokenTupleSet tts, boolean strict) {
     assert tts != null;
 
-    if( possibleReachabilities.contains(tts) ) {
+    if( !strict && possibleReachabilities.contains(tts) ) {
       return true;
     }
 
     Iterator itr = iterator();
     while( itr.hasNext() ) {
       TokenTupleSet ttsThis = (TokenTupleSet) itr.next();
-      if( tts.isSubset(ttsThis) ) {
-       return true;
+      if( strict ) {
+        if( !tts.equals(ttsThis) && tts.isSubset(ttsThis) ) {
+          return true;
+        }
+      } else {
+        if( tts.isSubset(ttsThis) ) {
+          return true;
+        }
       }
     }
 
@@ -471,12 +486,20 @@ public class ReachabilitySet extends Canonical {
   }
 
 
-  public String toStringEscapeNewline() {
+  public String toStringEscapeNewline( boolean hideSubsetReachability ) {
     String s = "[";
 
-    Iterator i = this.iterator();
+    Iterator<TokenTupleSet> i = this.iterator();
     while( i.hasNext() ) {
-      s += i.next();
+      TokenTupleSet tts = i.next();
+
+      // skip this if there is a superset already
+      if( hideSubsetReachability &&
+          containsStrictSuperSet( tts ) ) {
+        continue;
+      }
+
+      s += tts;
       if( i.hasNext() ) {
        s += "\\n";
       }
@@ -485,13 +508,26 @@ public class ReachabilitySet extends Canonical {
     s += "]";
     return s;
   }
+  
 
   public String toString() {
+    return toString( false );
+  }
+
+  public String toString( boolean hideSubsetReachability ) {
     String s = "[";
 
-    Iterator i = this.iterator();
+    Iterator<TokenTupleSet> i = this.iterator();
     while( i.hasNext() ) {
-      s += i.next();
+      TokenTupleSet tts = i.next();
+
+      // skip this if there is a superset already
+      if( hideSubsetReachability &&
+          containsStrictSuperSet( tts ) ) {
+        continue;
+      }
+
+      s += tts;
       if( i.hasNext() ) {
        s += "\n";
       }

diff --git a/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdge.java b/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdge.java
index 4cf3814f3d7accc91b511b2ab80c1f8aaf36c552..28d5d4925c391e7fa0bd91de6f6263beb163db42 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdge.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdge.java
@@ -208,7 +208,7 @@ public class ReferenceEdge {
   }
 
 
-  public String toGraphEdgeString() {
+  public String toGraphEdgeString( boolean hideSubsetReachability ) {
     String edgeLabel = "";
 
     if( type != null ) {
@@ -225,7 +225,7 @@ public class ReferenceEdge {
     
     edgeLabel+="*taint*="+Integer.toBinaryString(taintIdentifier)+"\\n";
 
-    edgeLabel += beta.toStringEscapeNewline();
+    edgeLabel += beta.toStringEscapeNewline(hideSubsetReachability);
 
     return edgeLabel;
   }

diff --git a/Robust/src/Tests/OwnershipAnalysisTest/versusShape/test.java b/Robust/src/Tests/OwnershipAnalysisTest/versusShape/test.java
index b30fe514a1849a2b1f54edfa04fbbc2a7547bc88..166f063d671e18f6524677a2a8a7e6ce9afce02f 100644 (file)
--- a/Robust/src/Tests/OwnershipAnalysisTest/versusShape/test.java
+++ b/Robust/src/Tests/OwnershipAnalysisTest/versusShape/test.java
@@ -1,16 +1,18 @@
+/*
 public class SparseGraph {
   Node head;
-  public SparseGraph() {
-    head = null;
+  public SparseGraph( Node n ) {
+    head = n;
   }
 }
 
 public class DenseGraph {
   Node head;
-  public DenseGraph() {
-    head = null;
+  public DenseGraph( Node n ) {
+    head = n;
   }
 }
+*/
 
 public class Node {
   public int value;
@@ -26,15 +28,52 @@ public class Test {
 
   static public void main( String[] args ) {
     HashSet sSet = new HashSet();
-    HashSet dSet = new HashSet();
+    //HashSet dSet = new HashSet();
     for( int i = 0; i < 100; ++i ) {
-      SparseGraph sNew = disjoint sparse new SparseGraph();
-      DenseGraph  dNew = disjoint dense  new DenseGraph();
+      /*
+      SparseGraph sNew = disjoint sparse new SparseGraph( new Node( 3*i ) );
+      DenseGraph  dNew = disjoint dense  new DenseGraph ( new Node( 2*i ) );
       sSet.add( sNew );
       dSet.add( dNew );
       SparseGraph s = (SparseGraph) sSet.iterator().next();
       DenseGraph  d = (DenseGraph)  dSet.iterator().next();
-      
+      process(  );
+      */
+
+
+      Node sNew = disjoint sparse new Node( 3*i );
+      //Node dNew = disjoint dense  new Node( 2*i );
+      sSet.add( sNew );
+      //dSet.add( dNew );
+      Node s = (Node) sSet.iterator().next();
+      //Node d = (Node) dSet.iterator().next();
+      growSparseAndDense( s /*, d*/ );
+    }
+  }
+
+  static public void growSparseAndDense( Node s /*, Node d*/ ) {
+    
+    Node sOld = s;
+    for( int j = 0; j < 2; ++j ) {
+      if( !sOld.nodes.isEmpty() ) {
+        sOld = (Node) sOld.nodes.iterator().next();
+      }
+    }
+    Node sNew = new Node( 4/**d.value*/ );
+    sOld.nodes.add( sNew );
+  
+
+    /*
+    Node dOld = d;
+    for( int j = 0; j < 2; ++j ) {
+      if( !dOld.nodes.isEmpty() ) {
+        dOld = (Node) dOld.nodes.iterator().next();
+      }
     }
+    Node dNew1 = new Node( 5*s.value );
+    Node dNew2 = new Node( 6*s.value );
+    dOld.nodes.add( dNew1 );
+    dOld.nodes.add( dNew2 );
+    */
   }
 }