some subtle reach state bug fixes uncovered by labyrinth benchmark, the benchmark...

diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java
index ff47436fa1e24238d8080fb6c6c621dfa1524bb1..74faebb6e18448a3f254579cd9a53d1858577875 100644 (file)
--- a/Robust/src/Analysis/Disjoint/Canonical.java
+++ b/Robust/src/Analysis/Disjoint/Canonical.java
@@ -297,6 +297,35 @@ abstract public class Canonical {
     return out;
   }
 
+
+  public static ReachState addUpArity( ReachState rs,
+                                       ReachTuple rt ) {
+    assert rs != null;
+    assert rt != null;
+
+    CanonicalOp op = 
+      new CanonicalOp( CanonicalOp.REACHSTATE_ADDUPARITY_REACHTUPLE,
+                       rs, 
+                       rt );
+    
+    Canonical result = op2result.get( op );
+    if( result != null ) {
+      return (ReachState) result;
+    }
+
+    // otherwise, no cached result...
+    ReachState out;
+
+    // the reason for this add is that we are aware a tuple
+    // with the same hrnID might already be in the state, so
+    // if it is we should combine properly
+    ReachState rtOnly = ReachState.factory( rt );
+    out = Canonical.unionUpArity( rs, rtOnly );
+    
+    op2result.put( op, out );
+    return out;
+  }
+
   
   public static ReachState remove( ReachState rs, ReachTuple rt ) {
     assert rs != null;
@@ -976,7 +1005,7 @@ abstract public class Canonical {
 
       if( age == AllocSite.AGE_notInThisSite ) {
         // things not from the site just go back in
-       baseState = Canonical.add( baseState, rt );
+       baseState = Canonical.addUpArity( baseState, rt );
 
       } else if( age == AllocSite.AGE_summary ) {
 
@@ -985,20 +1014,22 @@ abstract public class Canonical {
           // arity, if ARITY-ONE we'll branch the base state after the loop
           if( rt.getArity() == ReachTuple.ARITY_ZEROORMORE ) {
             // add two overly conservative symbols to reach state (PUNTING)
-            baseState = Canonical.add( baseState,
-                                       ReachTuple.factory( as.getSummary(),
-                                                           true, // multi
-                                                           ReachTuple.ARITY_ZEROORMORE,
-                                                           false // out-of-context
-                                                           )
-                                         );            
-            baseState = Canonical.add( baseState,
-                                       ReachTuple.factory( as.getSummary(),
-                                                           true, // multi
-                                                           ReachTuple.ARITY_ZEROORMORE,
-                                                           true  // out-of-context
-                                                           )
-                                       );            
+
+            baseState = Canonical.addUpArity( baseState,
+                                              ReachTuple.factory( as.getSummary(),
+                                                                  true, // multi
+                                                                  ReachTuple.ARITY_ZEROORMORE,
+                                                                  false // out-of-context
+                                                                  )
+                                              );            
+
+            baseState = Canonical.addUpArity( baseState,
+                                              ReachTuple.factory( as.getSummary(),
+                                                                  true, // multi
+                                                                  ReachTuple.ARITY_ZEROORMORE,
+                                                                  true  // out-of-context
+                                                                  )
+                                              );            
           } else {
             assert rt.getArity() == ReachTuple.ARITY_ONE;
             found2Sooc = true;
@@ -1006,13 +1037,13 @@ abstract public class Canonical {
 
         } else {
           // the in-context just becomes shadow
-          baseState = Canonical.add( baseState,
-                                     ReachTuple.factory( as.getSummaryShadow(),
-                                                         true, // multi
-                                                         rt.getArity(),
-                                                         false  // out-of-context
-                                                         )
-                                     );
+          baseState = Canonical.addUpArity( baseState,
+                                            ReachTuple.factory( as.getSummaryShadow(),
+                                                                true, // multi
+                                                                rt.getArity(),
+                                                                false  // out-of-context
+                                                                )
+                                            );
         }
 
 
@@ -1025,23 +1056,23 @@ abstract public class Canonical {
 
         if( rt.isOutOfContext() ) {
           // becomes the in-context version
-          baseState = Canonical.add( baseState,
-                                     ReachTuple.factory( rt.getHrnID(),
-                                                         false, // multi
-                                                         ReachTuple.ARITY_ONE,
-                                                         false  // out-of-context
-                                                         )
-                                     );          
+          baseState = Canonical.addUpArity( baseState,
+                                            ReachTuple.factory( rt.getHrnID(),
+                                                                false, // multi
+                                                                ReachTuple.ARITY_ONE,
+                                                                false  // out-of-context
+                                                                )
+                                            );          
 
         } else {
           // otherwise the ith symbol becomes shadowed
-          baseState = Canonical.add( baseState,
-                                     ReachTuple.factory( -rt.getHrnID(),
-                                                         false, // multi
-                                                         ReachTuple.ARITY_ONE,
-                                                         false  // out-of-context
-                                                         )
-                                     );        
+          baseState = Canonical.addUpArity( baseState,
+                                            ReachTuple.factory( -rt.getHrnID(),
+                                                                false, // multi
+                                                                ReachTuple.ARITY_ONE,
+                                                                false  // out-of-context
+                                                                )
+                                            );        
         }
       }
     }
@@ -1052,34 +1083,34 @@ abstract public class Canonical {
       // make a branch with every possibility of the one-to-many
       // mapping for 2S? appended to the baseState
       out = Canonical.add( out,
-                           Canonical.add( baseState,
-                                          ReachTuple.factory( as.getSummary(),
-                                                              true, // multi
-                                                              ReachTuple.ARITY_ONE,
-                                                              false  // out-of-context
-                                                              )
-                                          )
+                           Canonical.addUpArity( baseState,
+                                                 ReachTuple.factory( as.getSummary(),
+                                                                     true, // multi
+                                                                     ReachTuple.ARITY_ONE,
+                                                                     false  // out-of-context
+                                                                     )
+                                                 )
                            );
 
       out = Canonical.add( out,
-                           Canonical.add( baseState,
-                                          ReachTuple.factory( as.getSummary(),
-                                                              true, // multi
-                                                              ReachTuple.ARITY_ONE,
-                                                              true  // out-of-context
-                                                              )
-                                          )
+                           Canonical.addUpArity( baseState,
+                                                 ReachTuple.factory( as.getSummary(),
+                                                                     true, // multi
+                                                                     ReachTuple.ARITY_ONE,
+                                                                     true  // out-of-context
+                                                                     )
+                                                 )
                            );      
 
       for( int i = 0; i < as.getAllocationDepth(); ++i ) {
         out = Canonical.add( out,
-                             Canonical.add( baseState,
-                                            ReachTuple.factory( as.getIthOldest( i ),
-                                                                false, // multi
-                                                                ReachTuple.ARITY_ONE,
-                                                                true  // out-of-context
-                                                                )
-                                            )
+                             Canonical.addUpArity( baseState,
+                                                   ReachTuple.factory( as.getIthOldest( i ),
+                                                                       false, // multi
+                                                                       ReachTuple.ARITY_ONE,
+                                                                       true  // out-of-context
+                                                                       )
+                                                   )
                              );
       }
 
@@ -1163,19 +1194,19 @@ abstract public class Canonical {
       
       if( age == AllocSite.SHADOWAGE_notInThisSite ) {
         // things not from the site just go back in
-       out = Canonical.add( out, rt );
+       out = Canonical.addUpArity( out, rt );
 
       } else {
         assert !rt.isOutOfContext();
 
         // otherwise unshadow it
-        out = Canonical.add( out,
-                             ReachTuple.factory( -rt.getHrnID(),
-                                                 rt.isMultiObject(),
-                                                 rt.getArity(),
-                                                 false
-                                                 )
-                             );
+        out = Canonical.addUpArity( out,
+                                    ReachTuple.factory( -rt.getHrnID(),
+                                                        rt.isMultiObject(),
+                                                        rt.getArity(),
+                                                        false
+                                                        )
+                                    );
       }
     }
 

diff --git a/Robust/src/Analysis/Disjoint/CanonicalOp.java b/Robust/src/Analysis/Disjoint/CanonicalOp.java
index 7de780c60cc2d833cd030ce0bc92dc2eb8138c53..64761bc5b038180e593188e9373d0f6c5d5286ad 100644 (file)
--- a/Robust/src/Analysis/Disjoint/CanonicalOp.java
+++ b/Robust/src/Analysis/Disjoint/CanonicalOp.java
@@ -12,6 +12,7 @@ public class CanonicalOp {
   public static final int REACHSTATE_UNION_REACHSTATE          = 0x5678;
   public static final int REACHSTATE_ADD_REACHTUPLE            = 0x32b6;
   public static final int REACHSTATE_UNIONUPARITY_REACHSTATE   = 0x9152;
+  public static final int REACHSTATE_ADDUPARITY_REACHTUPLE     = 0x0a34;
   public static final int REACHSTATE_REMOVE_REACHTUPLE         = 0x8173;
   public static final int REACHSTATE_AGETUPLESFROM_ALLOCSITE   = 0x4f65;
   public static final int REACHSET_UNIONORPREDS_REACHSET       = 0x2131;

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 10617e110624c2e45b791329b25215d7c594de4a..51f83fe0e9c73485ad8ec250e10cf206f45242fb 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -1268,8 +1268,8 @@ public class ReachGraph {
       // possible changes, so keep a running union with the edge's
       // partially updated new beta set
       e.setBetaNew( Canonical.unionORpreds( e.getBetaNew(),
-                                     localDelta  
-                                     )
+                                            localDelta  
+                                            )
                     );
       
       edgesWithNewBeta.add( e );
@@ -1462,7 +1462,7 @@ public class ReachGraph {
                                        rt.isOutOfContext()
                                        );
           if( !oocHrnIdOoc2callee.contains( hio ) ) {
-            stateNew = Canonical.add( stateNew, rt );
+            stateNew = Canonical.addUpArity( stateNew, rt );
             continue;
           }
 
@@ -1484,20 +1484,20 @@ public class ReachGraph {
       
           if( age == AllocSite.AGE_notInThisSite ) {
             // things not from the site just go back in
-            stateNew = Canonical.add( stateNew, rt );
+            stateNew = Canonical.addUpArity( stateNew, rt );
 
           } else if( age == AllocSite.AGE_summary ||
                      rt.isOutOfContext()
                      ) {
-            // the in-context summary and all existing out-of-context
-            // stuff all become
-            stateNew = Canonical.add( stateNew,
-                                      ReachTuple.factory( as.getSummary(),
-                                                          true, // multi
-                                                          rt.getArity(),
-                                                          true  // out-of-context
-                                                          )
-                                      );
+            
+            stateNew = Canonical.addUpArity( stateNew,
+                                             ReachTuple.factory( as.getSummary(),
+                                                                 true, // multi
+                                                                 rt.getArity(),
+                                                                 true  // out-of-context
+                                                                 )
+                                             );
+            
           } else {
             // otherwise everything else just goes to an out-of-context
             // version, everything else the same
@@ -1506,13 +1506,13 @@ public class ReachGraph {
 
             assert !rt.isMultiObject();
 
-            stateNew = Canonical.add( stateNew,
-                                      ReachTuple.factory( rt.getHrnID(),
-                                                          rt.isMultiObject(),
-                                                          rt.getArity(),
-                                                          true  // out-of-context
-                                                          )
-                                      );        
+            stateNew = Canonical.addUpArity( stateNew,
+                                             ReachTuple.factory( rt.getHrnID(),
+                                                                 rt.isMultiObject(), // multi
+                                                                 rt.getArity(),
+                                                                 true  // out-of-context
+                                                                 )
+                                             );
           }
         }
         
@@ -3384,7 +3384,7 @@ public class ReachGraph {
          }
           
          if( !foundState ) {
-           markedHrnIDs = Canonical.add( markedHrnIDs, rtOld );          
+           markedHrnIDs = Canonical.addUpArity( markedHrnIDs, rtOld );   
          }
        }
 
@@ -3405,7 +3405,7 @@ public class ReachGraph {
          ReachTuple rtOld = rtItr.next();
 
          if( !markedHrnIDs.containsTuple( rtOld ) ) {
-           statePruned = Canonical.add( statePruned, rtOld );
+           statePruned = Canonical.addUpArity( statePruned, rtOld );
          }
        }
        assert !stateOld.equals( statePruned );