stable, still partial method calls

diff --git a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
index d44a06cff3383f5dc0a2f13c59ff62ddc804a4a0..7c9575a07aeb446f492cdf4c110aebf2304fcb62 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
@@ -1001,6 +1001,8 @@ public class OwnershipGraph {
     }
 
 
+    HashSet<HeapRegionNode> nodesWithNewAlpha = new HashSet<HeapRegionNode>();
+
     Iterator lnArgItr = paramIndex2ln.entrySet().iterator();
     while( lnArgItr.hasNext() ) {
       Map.Entry me      = (Map.Entry) lnArgItr.next();
@@ -1040,74 +1042,27 @@ public class OwnershipGraph {
       while( hrnItr.hasNext() ) {
        HeapRegionNode hrn = hrnItr.next();
 
-       rewriteCallerNodeAlpha( index,
+       rewriteCallerNodeAlpha( fm.numParameters(),
+                               index,
                                hrn,
                                paramIndex2rewriteH,
                                paramIndex2rewriteD,
                                paramIndex2paramToken,
-                               paramTokenStar2paramIndex );
+                               paramIndex2paramTokenStar );
+
+       nodesWithNewAlpha.add( hrn );
       }
     }    
     
 
+    // commit changes to alpha
+    Iterator<HeapRegionNode> nodeItr = nodesWithNewAlpha.iterator();
+    while( nodeItr.hasNext() ) {
+      nodeItr.next().applyAlphaNew();
+    }
 
 
 
-    /*
-    // make a change set to translate callee tokens into caller tokens
-    ChangeTupleSet C = new ChangeTupleSet().makeCanonical();
-
-    for( int i = 0; i < fm.numParameters(); ++i ) {
-      
-      Integer paramIndex = new Integer( i );
-      
-      System.out.println( "In method "+fm+ " on param "+paramIndex );
-      
-      assert ogCallee.paramIndex2id.containsKey( paramIndex );
-      Integer idParam = ogCallee.paramIndex2id.get( paramIndex );
-      
-      assert ogCallee.id2hrn.containsKey( idParam );
-      HeapRegionNode hrnParam = ogCallee.id2hrn.get( idParam );
-      assert hrnParam != null;
-      
-      TokenTupleSet calleeTokenToMatch =
-       new TokenTupleSet( new TokenTuple( hrnParam ) ).makeCanonical();
-      
-      
-      // now depending on whether the callee is static or not
-      // we need to account for a "this" argument in order to
-      // find the matching argument in the caller context
-      TempDescriptor argTemp;
-      if( isStatic ) {
-       argTemp = fc.getArg( paramIndex );
-      } else {
-       if( paramIndex == 0 ) {
-         argTemp = fc.getThis();
-       } else {
-         argTemp = fc.getArg( paramIndex - 1 );
-       }
-      }
-      
-      LabelNode argLabel = getLabelNodeFromTemp( argTemp );
-      Iterator argHeapRegionsItr = argLabel.setIteratorToReferencedRegions();
-      while( argHeapRegionsItr.hasNext() ) {
-       Map.Entry meArg                = (Map.Entry)               argHeapRegionsItr.next();
-       HeapRegionNode argHeapRegion   = (HeapRegionNode)          meArg.getKey();
-       ReferenceEdgeProperties repArg = (ReferenceEdgeProperties) meArg.getValue();
-       
-       Iterator<TokenTupleSet> ttsItr = repArg.getBeta().iterator();
-       while( ttsItr.hasNext() ) {
-         TokenTupleSet callerTokensToReplace = ttsItr.next();
-         
-         ChangeTuple ct = new ChangeTuple( calleeTokenToMatch,
-                                           callerTokensToReplace ).makeCanonical();
-         
-         C = C.union( ct );
-       }
-      }
-    }
-    */
-
     /*
     System.out.println( "Applying method call "+fm );
     System.out.println( "  Change: "+C );
@@ -1186,12 +1141,13 @@ public class OwnershipGraph {
   }
 
 
-  private void rewriteCallerNodeAlpha( Integer paramIndex, 
+  private void rewriteCallerNodeAlpha( int numParameters, 
+                                      Integer paramIndex, 
                                       HeapRegionNode hrn,
                                       Hashtable<Integer, ReachabilitySet> paramIndex2rewriteH,
                                       Hashtable<Integer, ReachabilitySet> paramIndex2rewriteD,
                                       Hashtable<Integer, TokenTuple> paramIndex2paramToken,
-                                      Hashtable<TokenTuple, Integer> paramTokenStar2paramIndex ) {
+                                      Hashtable<Integer, TokenTuple> paramIndex2paramTokenStar ) {
    
     ReachabilitySet rules = paramIndex2rewriteH.get( paramIndex );
     assert rules != null;
@@ -1199,20 +1155,88 @@ public class OwnershipGraph {
     TokenTuple tokenToRewrite = paramIndex2paramToken.get( paramIndex );
     assert tokenToRewrite != null;
 
-    ReachabilitySet r0 = new ReachabilitySet().makeCanonical();
-    
+    ReachabilitySet r0 = new ReachabilitySet().makeCanonical();    
     Iterator<TokenTupleSet> ttsItr = rules.iterator();
     while( ttsItr.hasNext() ) {
       TokenTupleSet tts = ttsItr.next();
-      r0 = r0.union( tts.rewrite( tokenToRewrite, hrn.getAlpha() ) );
+      r0 = r0.union( tts.simpleRewriteToken( tokenToRewrite, hrn.getAlpha() ) );
     }
     
-    //ReachabilitySet r1 = D( r0 );
+    ReachabilitySet r1 = new ReachabilitySet().makeCanonical();
+    ttsItr = r0.iterator();
+    while( ttsItr.hasNext() ) {
+      TokenTupleSet tts = ttsItr.next();
+      r1 = r1.union( rewriteDpass( numParameters,
+                                  paramIndex,
+                                  tts,
+                                  paramIndex2rewriteD,
+                                  paramIndex2paramToken,
+                                  paramIndex2paramTokenStar ) );
+    }    
 
-    hrn.setAlphaNew( r0 );
+    hrn.setAlphaNew( r1 );
   }
 
 
+  private ReachabilitySet rewriteDpass( int numParameters, 
+                                       Integer paramIndex,
+                                       TokenTupleSet ttsIn,
+                                       Hashtable<Integer, ReachabilitySet> paramIndex2rewriteD,
+                                       Hashtable<Integer, TokenTuple> paramIndex2paramToken,
+                                       Hashtable<Integer, TokenTuple> paramIndex2paramTokenStar ) {
+
+    ReachabilitySet rsOut = new ReachabilitySet().makeCanonical();
+
+    boolean rewritten = false;
+
+    for( int j = 0; j < numParameters; ++j ) {
+      Integer paramIndexJ = new Integer( j );
+      ReachabilitySet D_j = paramIndex2rewriteD.get( paramIndexJ );
+      assert D_j != null;
+      
+      if( paramIndexJ != paramIndex ) {
+       TokenTuple tokenToRewriteJ = paramIndex2paramToken.get( paramIndexJ );
+       assert tokenToRewriteJ != null;
+       if( ttsIn.containsTuple( tokenToRewriteJ ) ) {
+         ReachabilitySet r = ttsIn.exhaustiveRewriteToken( tokenToRewriteJ, D_j );
+         Iterator<TokenTupleSet> ttsItr = r.iterator();
+         while( ttsItr.hasNext() ) {
+           TokenTupleSet tts = ttsItr.next();
+           rsOut = rsOut.union( rewriteDpass( numParameters,
+                                              paramIndex,
+                                              tts,
+                                              paramIndex2rewriteD,
+                                              paramIndex2paramToken,
+                                              paramIndex2paramTokenStar ) );
+           rewritten = true;
+         }      
+       }
+      }
+      
+      TokenTuple tokenStarToRewriteJ = paramIndex2paramTokenStar.get( paramIndexJ );
+      assert tokenStarToRewriteJ != null;              
+      if( ttsIn.containsTuple( tokenStarToRewriteJ ) ) {
+       ReachabilitySet r = ttsIn.exhaustiveRewriteToken( tokenStarToRewriteJ, D_j );
+       Iterator<TokenTupleSet> ttsItr = r.iterator();
+       while( ttsItr.hasNext() ) {
+         TokenTupleSet tts = ttsItr.next();
+         rsOut = rsOut.union( rewriteDpass( numParameters,
+                                            paramIndex,
+                                            tts,
+                                            paramIndex2rewriteD,
+                                            paramIndex2paramToken,
+                                            paramIndex2paramTokenStar ) );
+         rewritten = true;
+       }
+      }
+    }
+
+    if( !rewritten ) {
+      rsOut = rsOut.union( ttsIn );
+    }
+    
+    return rsOut;
+  }
 
 
   /*

diff --git a/Robust/src/Analysis/OwnershipAnalysis/TokenTupleSet.java b/Robust/src/Analysis/OwnershipAnalysis/TokenTupleSet.java
index cda83d8adf84703a904585e13ac91c60b173792b..69b954a8a1bf45e5527d36d2027e55efbf26500c 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/TokenTupleSet.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/TokenTupleSet.java
@@ -181,13 +181,13 @@ public class TokenTupleSet extends Canonical {
   }
 
 
-  public ReachabilitySet rewrite( TokenTuple tokenToRewrite,
-                                 ReachabilitySet replacements ) {
+  public ReachabilitySet simpleRewriteToken( TokenTuple tokenToRewrite,
+                                            ReachabilitySet replacements ) {
     
     ReachabilitySet rsOut = new ReachabilitySet().makeCanonical();
 
     if( !tokenTuples.contains( tokenToRewrite ) ) {
-      rsOut.add( this );
+      rsOut = rsOut.add( this );
 
     } else {
       TokenTupleSet ttsMinusToken = new TokenTupleSet( this );
@@ -200,7 +200,7 @@ public class TokenTupleSet extends Canonical {
        replaced.tokenTuples.addAll( ttsMinusToken.tokenTuples );
        replaced.tokenTuples.addAll( replacement.tokenTuples );
        replaced = replaced.makeCanonical();
-       rsOut.add( replaced );
+       rsOut = rsOut.add( replaced );
       }
     }
 
@@ -208,6 +208,35 @@ public class TokenTupleSet extends Canonical {
   }
 
 
+  public ReachabilitySet exhaustiveRewriteToken( TokenTuple tokenToRewrite,
+                                                ReachabilitySet replacements ) {
+    
+    ReachabilitySet rsOut = new ReachabilitySet().makeCanonical();
+
+    /*
+    if( !tokenTuples.contains( tokenToRewrite ) ) {
+      rsOut = rsOut.add( this );
+
+    } else {
+      TokenTupleSet ttsMinusToken = new TokenTupleSet( this );
+      ttsMinusToken.tokenTuples.remove( tokenToRewrite );
+
+      Iterator<TokenTupleSet> replaceItr = replacements.iterator();
+      while( replaceItr.hasNext() ) {
+       TokenTupleSet replacement = replaceItr.next();
+       TokenTupleSet replaced = new TokenTupleSet();
+       replaced.tokenTuples.addAll( ttsMinusToken.tokenTuples );
+       replaced.tokenTuples.addAll( replacement.tokenTuples );
+       replaced = replaced.makeCanonical();
+       rsOut = rsOut.add( replaced );
+      }
+    }
+    */
+
+    return rsOut;
+  }
+
+
   public String toString() {
     return tokenTuples.toString();
   }

diff --git a/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java b/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java
index 73256c19d2adfea5e4f11dc1f4fd47d5466134d7..088fd08486284d8032cfa31f3108353212a2f208 100644 (file)
--- a/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java
+++ b/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java
@@ -44,6 +44,7 @@ public class Foo {
 
     public Foo x;
     public Foo y;
+    public Foo z;
 
     /*
     public void ruinSomeFoos( Foo a, Foo b ) {
@@ -61,6 +62,85 @@ public class Foo {
        p1.x = f2;
     }
     */
+
+  static public void m1_( Foo p0 ) {
+    Foo g0 = new Foo();
+    Foo g1 = new Foo();
+
+    g0.x = p0;
+    p0.x = g1;
+  }
+
+  static public void m2_( Foo p0 ) {
+    Foo g0 = new Foo();
+
+    g0.x = p0;
+    g0.y = p0;
+  }
+
+  static public void m3_( Foo p0 ) {
+    Foo g0 = new Foo();
+
+    p0.x = g0;
+    p0.y = g0;
+  }
+
+  static public void m4_( Foo p0 ) {
+    p0.x = p0;
+  }
+
+  static public void m5_( Foo p0 ) {
+    Foo g0 = new Foo();
+    p0.x = g0;
+    g0.x = p0;
+  }
+
+  static public void m6_( Foo p0, Foo p1 ) {
+    Foo g0 = new Foo();
+    Foo g1 = new Foo();
+    Foo g2 = new Foo();
+    Foo g3 = new Foo();
+
+    g0.x = p0;
+    p0.x = g1;
+
+    g2.x = p1;
+    p1.x = g3;
+
+    p0.y = p1;
+  }
+
+  static public void m7_( Foo p0, Foo p1 ) {
+    Foo g0 = new Foo();
+    Foo g1 = new Foo();
+    Foo g2 = new Foo();
+    Foo g3 = new Foo();
+
+    g0.x = p0;
+    p0.x = g1;
+
+    g2.x = p1;
+    p1.x = g3;
+
+    p0.y = p1;
+    p0.z = p1;
+  }
+
+  static public void m8_( Foo p0, Foo p1 ) {
+    Foo g0 = new Foo();
+    Foo g1 = new Foo();
+    Foo g2 = new Foo();
+    Foo g3 = new Foo();
+
+    g0.x = p0;
+    p0.x = g1;
+
+    g2.x = p1;
+    p1.x = g3;
+
+    p0.y = p1;
+    p1.y = p0;
+  }
 }
 
 
@@ -116,7 +196,7 @@ task NewObjectC( Foo a{ f }, Foo b{ f } ) {
 }
 */
 
-
+/*
 task forMethod( Foo p0{ f } ) {
 
     Foo a0;
@@ -136,7 +216,7 @@ task forMethod( Foo p0{ f } ) {
 
     taskexit( p0{ !f } );
 }
-
+*/
 
 
 /*
@@ -263,3 +343,229 @@ task methodTest( Foo p0{ f } ) {
     taskexit( p0{ !f } );
 }
 */
+
+
+task methodTest01_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo.m1_( a0after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest02_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo.m2_( a0after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest03_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo.m3_( a0after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest04_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo.m4_( a0after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest05_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo.m5_( a0after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest06_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo a1before = new Foo();
+  if( false ) {
+    a1before.x = new Foo();
+  } else {
+    a1before.x = new Foo();
+  }
+
+  Foo a1after = new Foo();
+  if( false ) {
+    a1after.x = new Foo();
+  } else {
+    a1after.x = new Foo();
+  }
+
+  Foo.m6_( a0after, a1after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest07_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo a1before = new Foo();
+  if( false ) {
+    a1before.x = new Foo();
+  } else {
+    a1before.x = new Foo();
+  }
+
+  Foo a1after = new Foo();
+  if( false ) {
+    a1after.x = new Foo();
+  } else {
+    a1after.x = new Foo();
+  }
+
+  Foo.m7_( a0after, a1after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}
+
+
+task methodTest08_( Foo p0{ f }, Foo p1{ f } ) {
+
+  Foo a0before = new Foo();
+  if( false ) {
+    a0before.x = new Foo();
+  } else {
+    a0before.x = new Foo();
+  }
+
+  Foo a0after = new Foo();
+  if( false ) {
+    a0after.x = new Foo();
+  } else {
+    a0after.x = new Foo();
+  }
+
+  Foo a1before = new Foo();
+  if( false ) {
+    a1before.x = new Foo();
+  } else {
+    a1before.x = new Foo();
+  }
+
+  Foo a1after = new Foo();
+  if( false ) {
+    a1after.x = new Foo();
+  } else {
+    a1after.x = new Foo();
+  }
+
+  Foo.m8_( a0after, a1after );
+
+
+  taskexit( p0{ !f }, p1{ !f } );
+}