From: jjenista Date: Fri, 19 Mar 2010 19:21:10 +0000 (+0000) Subject: make sure straight union of reach states or reach sets is never done, reach tuples... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0ddc61c243785e40b5b8cb9000244e7b52608513;p=IRC.git make sure straight union of reach states or reach sets is never done, reach tuples in states with same id should merge arity values, and reach states with same state but different preds should become one state with preds ORed --- diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java index 7918033f..c74bad4d 100644 --- a/Robust/src/Analysis/Disjoint/Canonical.java +++ b/Robust/src/Analysis/Disjoint/Canonical.java @@ -104,8 +104,8 @@ abstract public class Canonical { // not weighty, don't bother with caching - public static ReachTuple unionArity( ReachTuple rt1, - ReachTuple rt2 ) { + public static ReachTuple unionUpArity( ReachTuple rt1, + ReachTuple rt2 ) { assert rt1 != null; assert rt2 != null; assert rt1.isCanonical(); @@ -180,44 +180,18 @@ abstract public class Canonical { } - public static ReachState union( ReachState rs1, - ReachState rs2 ) { - assert rs1 != null; - assert rs2 != null; - assert rs1.isCanonical(); - assert rs2.isCanonical(); - - CanonicalOp op = - new CanonicalOp( CanonicalOp.REACHSTATE_UNION_REACHSTATE, - rs1, - rs2 ); - - Canonical result = op2result.get( op ); - if( result != null ) { - return (ReachState) result; - } - - // otherwise, no cached result... - ReachState out = new ReachState(); - out.reachTuples.addAll( rs1.reachTuples ); - out.reachTuples.addAll( rs2.reachTuples ); - out.preds = Canonical.join( rs1.getPreds(), - rs2.getPreds() - ); - - out = (ReachState) makeCanonical( out ); - op2result.put( op, out ); - return out; - } - - // this is just a convenience version of above - public static ReachState union( ReachState rs, - ReachTuple rt ) { + public static ReachState add( ReachState rs, + ReachTuple rt ) { assert rs != null; assert rt != null; + // this is only safe if we are certain the new tuple's + // ID doesn't already appear in the reach state + assert rs.containsHrnID( rt.getHrnID(), + rt.isOutOfContext() ) == null; + CanonicalOp op = - new CanonicalOp( CanonicalOp.REACHSTATE_UNION_REACHTUPLE, + new CanonicalOp( CanonicalOp.REACHSTATE_ADD_REACHTUPLE, rs, rt ); @@ -258,6 +232,8 @@ abstract public class Canonical { // otherwise, no cached result... ReachState out = new ReachState(); + // first add everything from 1, and if it is + // also in 2 take the union of the tuple arities Iterator rtItr = rs1.iterator(); while( rtItr.hasNext() ) { ReachTuple rt1 = rtItr.next(); @@ -265,20 +241,21 @@ abstract public class Canonical { rt1.isOutOfContext() ); if( rt2 != null ) { - out.reachTuples.add( unionArity( rt1, rt2 ) ); + out.reachTuples.add( unionUpArity( rt1, rt2 ) ); } else { out.reachTuples.add( rt1 ); } } + // then add everything in 2 that wasn't in 1 rtItr = rs2.iterator(); while( rtItr.hasNext() ) { ReachTuple rt2 = rtItr.next(); - ReachTuple rto = out.containsHrnID( rt2.getHrnID(), + ReachTuple rt1 = rs1.containsHrnID( rt2.getHrnID(), rt2.isOutOfContext() ); - if( rto == null ) { - out.reachTuples.add( rto ); + if( rt1 == null ) { + out.reachTuples.add( rt2 ); } } @@ -291,9 +268,6 @@ abstract public class Canonical { return out; } - public static ReachState add( ReachState rs, ReachTuple rt ) { - return union( rs, rt ); - } public static ReachState remove( ReachState rs, ReachTuple rt ) { assert rs != null; @@ -403,13 +377,13 @@ abstract public class Canonical { ); } else if( rtSummary != null && rtOldest != null ) { - out.reachTuples.add( Canonical.unionArity( rtSummary, - ReachTuple.factory( as.getSummary(), - true, // muli - rtOldest.getArity(), - false // out-of-context - ) - ) + out.reachTuples.add( Canonical.unionUpArity( rtSummary, + ReachTuple.factory( as.getSummary(), + true, // muli + rtOldest.getArity(), + false // out-of-context + ) + ) ); } @@ -422,15 +396,15 @@ abstract public class Canonical { - public static ReachSet union( ReachSet rs1, - ReachSet rs2 ) { + public static ReachSet unionORpreds( ReachSet rs1, + ReachSet rs2 ) { assert rs1 != null; assert rs2 != null; assert rs1.isCanonical(); assert rs2.isCanonical(); CanonicalOp op = - new CanonicalOp( CanonicalOp.REACHSET_UNION_REACHSET, + new CanonicalOp( CanonicalOp.REACHSET_UNIONORPREDS_REACHSET, rs1, rs2 ); @@ -441,42 +415,42 @@ abstract public class Canonical { // otherwise, no cached result... ReachSet out = new ReachSet(); - out.reachStates.addAll( rs1.reachStates ); - out.reachStates.addAll( rs2.reachStates ); - out = (ReachSet) makeCanonical( out ); - op2result.put( op, out ); - return out; - } - - public static ReachSet union( ReachSet rs, - ReachState state ) { + // first add everything from 1, and if it was also in 2 + // take the OR of the predicates + Iterator stateItr = rs1.iterator(); + while( stateItr.hasNext() ) { + ReachState state1 = stateItr.next(); + ReachState state2 = rs2.containsIgnorePreds( state1 ); + + if( state2 != null ) { + out.reachStates.add( ReachState.factory( state1.reachTuples, + Canonical.join( state1.preds, + state2.preds + ) + ) ); + } else { + out.reachStates.add( state1 ); + } + } - assert rs != null; - assert state != null; - assert rs.isCanonical(); - assert state.isCanonical(); + // then add everything in 2 that wasn't in 1 + stateItr = rs2.iterator(); + while( stateItr.hasNext() ) { + ReachState state2 = stateItr.next(); + ReachState state1 = rs1.containsIgnorePreds( state2 ); - CanonicalOp op = - new CanonicalOp( CanonicalOp.REACHSET_UNION_REACHSTATE, - rs, - state ); - - Canonical result = op2result.get( op ); - if( result != null ) { - return (ReachSet) result; + if( state1 == null ) { + out.reachStates.add( state2 ); + } } - // otherwise, no cached result... - ReachSet out = new ReachSet(); - out.reachStates.addAll( rs.reachStates ); - out.reachStates.add( state ); - out = (ReachSet) makeCanonical( out ); op2result.put( op, out ); return out; } + public static ReachSet intersection( ReachSet rs1, ReachSet rs2 ) { assert rs1 != null; @@ -512,7 +486,9 @@ abstract public class Canonical { public static ReachSet add( ReachSet rs, ReachState state ) { - return union( rs, state ); + return unionORpreds( rs, + ReachSet.factory( state ) + ); } public static ReachSet remove( ReachSet rs, @@ -638,15 +614,15 @@ abstract public class Canonical { rtR.isOutOfContext() ); if( rtO != null ) { - theUnion = Canonical.union( theUnion, - Canonical.unionArity( rtR, + theUnion = Canonical.add( theUnion, + Canonical.unionUpArity( rtR, rtO ) - ); + ); } else { - theUnion = Canonical.union( theUnion, - rtR - ); + theUnion = Canonical.add( theUnion, + rtR + ); } } @@ -657,9 +633,9 @@ abstract public class Canonical { rtO.isOutOfContext() ); if( rtR == null ) { - theUnion = Canonical.union( theUnion, - rtO - ); + theUnion = Canonical.add( theUnion, + rtO + ); } } @@ -1013,9 +989,9 @@ abstract public class Canonical { Iterator itr = rs.iterator(); while( itr.hasNext() ) { ReachState state = itr.next(); - out = Canonical.union( out, - Canonical.toCallerContext( state, as ) - ); + out = Canonical.unionORpreds( out, + Canonical.toCallerContext( state, as ) + ); } assert out.isCanonical(); @@ -1075,7 +1051,7 @@ abstract public class Canonical { if( age == AllocSite.AGE_notInThisSite ) { // things not from the site just go back in - baseState = Canonical.union( baseState, rt ); + baseState = Canonical.add( baseState, rt ); } else if( age == AllocSite.AGE_summary ) { @@ -1084,20 +1060,20 @@ 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.union( baseState, - ReachTuple.factory( as.getSummary(), - true, // multi - ReachTuple.ARITY_ZEROORMORE, - false // out-of-context - ) - ); - baseState = Canonical.union( baseState, - ReachTuple.factory( as.getSummary(), - true, // multi - ReachTuple.ARITY_ZEROORMORE, - true // out-of-context - ) + 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 + ) + ); } else { assert rt.getArity() == ReachTuple.ARITY_ONE; found2Sooc = true; @@ -1105,13 +1081,13 @@ abstract public class Canonical { } else { // the in-context just becomes shadow - baseState = Canonical.union( baseState, - ReachTuple.factory( as.getSummaryShadow(), - true, // multi - rt.getArity(), - false // out-of-context - ) - ); + baseState = Canonical.add( baseState, + ReachTuple.factory( as.getSummaryShadow(), + true, // multi + rt.getArity(), + false // out-of-context + ) + ); } @@ -1124,23 +1100,23 @@ abstract public class Canonical { if( rt.isOutOfContext() ) { // becomes the in-context version - baseState = Canonical.union( baseState, - ReachTuple.factory( rt.getHrnID(), - false, // multi - ReachTuple.ARITY_ONE, - false // out-of-context - ) - ); + baseState = Canonical.add( baseState, + ReachTuple.factory( rt.getHrnID(), + false, // multi + ReachTuple.ARITY_ONE, + false // out-of-context + ) + ); } else { // otherwise the ith symbol becomes shadowed - baseState = Canonical.union( baseState, - ReachTuple.factory( -rt.getHrnID(), - false, // multi - ReachTuple.ARITY_ONE, - false // out-of-context - ) - ); + baseState = Canonical.add( baseState, + ReachTuple.factory( -rt.getHrnID(), + false, // multi + ReachTuple.ARITY_ONE, + false // out-of-context + ) + ); } } } @@ -1150,42 +1126,42 @@ abstract public class Canonical { if( found2Sooc ) { // make a branch with every possibility of the one-to-many // mapping for 2S? appended to the baseState - out = Canonical.union( out, - Canonical.union( 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, + false // out-of-context + ) + ) + ); - out = Canonical.union( out, - Canonical.union( baseState, - ReachTuple.factory( as.getSummary(), - true, // multi - ReachTuple.ARITY_ONE, - true // out-of-context - ) - ) - ); + out = Canonical.add( out, + Canonical.add( baseState, + ReachTuple.factory( as.getSummary(), + true, // multi + ReachTuple.ARITY_ONE, + true // out-of-context + ) + ) + ); for( int i = 0; i < as.getAllocationDepth(); ++i ) { - out = Canonical.union( out, - Canonical.union( baseState, - ReachTuple.factory( as.getIthOldest( i ), - false, // multi - ReachTuple.ARITY_ONE, - true // out-of-context - ) - ) - ); + out = Canonical.add( out, + Canonical.add( baseState, + ReachTuple.factory( as.getIthOldest( i ), + false, // multi + ReachTuple.ARITY_ONE, + true // out-of-context + ) + ) + ); } } else { // just use current baseState - out = Canonical.union( out, - baseState ); + out = Canonical.add( out, + baseState ); } @@ -1269,19 +1245,19 @@ abstract public class Canonical { if( age == AllocSite.SHADOWAGE_notInThisSite ) { // things not from the site just go back in - out = Canonical.union( out, rt ); + out = Canonical.add( out, rt ); } else { assert !rt.isOutOfContext(); // otherwise unshadow it - out = Canonical.union( out, - ReachTuple.factory( -rt.getHrnID(), - rt.isMultiObject(), - rt.getArity(), - false - ) - ); + out = Canonical.add( 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 14ca4bc1..73caa309 100644 --- a/Robust/src/Analysis/Disjoint/CanonicalOp.java +++ b/Robust/src/Analysis/Disjoint/CanonicalOp.java @@ -8,15 +8,13 @@ package Analysis.Disjoint; // first and do a result look-up public class CanonicalOp { - public static final int REACHTUPLE_UNIONARITY_REACHTUPLE = 0x1a34; public static final int REACHSTATE_ATTACH_EXISTPREDSET = 0x8358; public static final int REACHSTATE_UNION_REACHSTATE = 0x5678; - public static final int REACHSTATE_UNION_REACHTUPLE = 0x32b6; + public static final int REACHSTATE_ADD_REACHTUPLE = 0x32b6; public static final int REACHSTATE_UNIONUPARITY_REACHSTATE = 0x9152; public static final int REACHSTATE_REMOVE_REACHTUPLE = 0x8173; public static final int REACHSTATE_AGETUPLESFROM_ALLOCSITE = 0x4f65; - public static final int REACHSET_UNION_REACHSET = 0x2131; - public static final int REACHSET_UNION_REACHSTATE = 0xe3c8; + public static final int REACHSET_UNIONORPREDS_REACHSET = 0x2131; public static final int REACHSET_INTERSECTION_REACHSET = 0x3361; public static final int REACHSET_REMOVE_REACHSTATE = 0x9391; public static final int REACHSET_APPLY_CHANGESET = 0x1d55; diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index d1b5bab5..f6deaab2 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -575,7 +575,7 @@ public class ReachGraph { if( edgeExisting != null ) { edgeExisting.setBeta( - Canonical.union( edgeExisting.getBeta(), + Canonical.unionORpreds( edgeExisting.getBeta(), edgeNew.getBeta() ) ); @@ -881,7 +881,7 @@ public class ReachGraph { // otherwise an edge from the referencer to hrnSummary exists already // and the edge referencer->hrn should be merged with it edgeSummary.setBeta( - Canonical.union( edgeMerged.getBeta(), + Canonical.unionORpreds( edgeMerged.getBeta(), edgeSummary.getBeta() ) ); @@ -915,7 +915,7 @@ public class ReachGraph { // otherwise an edge from the referencer to alpha_S exists already // and the edge referencer->alpha_K should be merged with it edgeSummary.setBeta( - Canonical.union( edgeMerged.getBeta(), + Canonical.unionORpreds( edgeMerged.getBeta(), edgeSummary.getBeta() ) ); @@ -929,7 +929,7 @@ public class ReachGraph { // then merge hrn reachability into hrnSummary hrnSummary.setAlpha( - Canonical.union( hrnSummary.getAlpha(), + Canonical.unionORpreds( hrnSummary.getAlpha(), hrn.getAlpha() ) ); @@ -1123,7 +1123,7 @@ public class ReachGraph { // but this propagation may be only one of many concurrent // possible changes, so keep a running union with the node's // partially updated new alpha set - n.setAlphaNew( Canonical.union( n.getAlphaNew(), + n.setAlphaNew( Canonical.unionORpreds( n.getAlphaNew(), localDelta ) ); @@ -1212,7 +1212,7 @@ public class ReachGraph { // but this propagation may be only one of many concurrent // possible changes, so keep a running union with the edge's // partially updated new beta set - e.setBetaNew( Canonical.union( e.getBetaNew(), + e.setBetaNew( Canonical.unionORpreds( e.getBetaNew(), localDelta ) ); @@ -1309,7 +1309,7 @@ public class ReachGraph { // only translate this tuple if it is in the out-context bag if( !oocTuples.contains( rt ) ) { - stateNew = Canonical.union( stateNew, rt ); + stateNew = Canonical.add( stateNew, rt ); continue; } @@ -1331,20 +1331,20 @@ public class ReachGraph { if( age == AllocSite.AGE_notInThisSite ) { // things not from the site just go back in - stateNew = Canonical.union( stateNew, rt ); + stateNew = Canonical.add( 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.union( stateNew, - ReachTuple.factory( as.getSummary(), - true, // multi - rt.getArity(), - true // out-of-context - ) - ); + stateNew = Canonical.add( 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 @@ -1353,13 +1353,13 @@ public class ReachGraph { assert !rt.isMultiObject(); - stateNew = Canonical.union( stateNew, - ReachTuple.factory( rt.getHrnID(), - rt.isMultiObject(), - rt.getArity(), - true // out-of-context - ) - ); + stateNew = Canonical.add( stateNew, + ReachTuple.factory( rt.getHrnID(), + rt.isMultiObject(), + rt.getArity(), + true // out-of-context + ) + ); } } @@ -1439,7 +1439,7 @@ public class ReachGraph { stateCaller = Canonical.attach( stateCaller, calleeStatesSatisfied.get( stateCallee ) ); - out = Canonical.union( out, + out = Canonical.add( out, stateCaller ); } @@ -1875,7 +1875,7 @@ public class ReachGraph { } else { // the out-of-context edge already exists - oocEdgeExisting.setBeta( Canonical.union( oocEdgeExisting.getBeta(), + oocEdgeExisting.setBeta( Canonical.unionORpreds( oocEdgeExisting.getBeta(), toCalleeContext( oocTuples, reCaller.getBeta(), // in state null, // node pred @@ -2416,7 +2416,7 @@ public class ReachGraph { ); if( edgeExisting != null ) { edgeExisting.setBeta( - Canonical.union( edgeExisting.getBeta(), + Canonical.unionORpreds( edgeExisting.getBeta(), reCaller.getBeta() ) ); @@ -2984,18 +2984,18 @@ public class ReachGraph { ); if( prevResult == null || - Canonical.union( prevResult, + Canonical.unionORpreds( prevResult, intersection ).size() > prevResult.size() ) { if( prevResult == null ) { boldB_f.put( edgePrime, - Canonical.union( edgePrime.getBeta(), + Canonical.unionORpreds( edgePrime.getBeta(), intersection ) ); } else { boldB_f.put( edgePrime, - Canonical.union( prevResult, + Canonical.unionORpreds( prevResult, intersection ) ); @@ -3094,7 +3094,7 @@ public class ReachGraph { // if there is nothing marked, just move on if( markedHrnIDs.isEmpty() ) { - hrn.setAlphaNew( Canonical.union( hrn.getAlphaNew(), + hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(), stateOld ) ); @@ -3109,12 +3109,12 @@ public class ReachGraph { ReachTuple rtOld = rtItr.next(); if( !markedHrnIDs.containsTuple( rtOld ) ) { - statePruned = Canonical.union( statePruned, rtOld ); + statePruned = Canonical.add( statePruned, rtOld ); } } assert !stateOld.equals( statePruned ); - hrn.setAlphaNew( Canonical.union( hrn.getAlphaNew(), + hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(), statePruned ) ); @@ -3214,13 +3214,13 @@ public class ReachGraph { edgePrime.getBetaNew() ); - if( Canonical.union( prevResult, - intersection - ).size() > prevResult.size() ) { + if( Canonical.unionORpreds( prevResult, + intersection + ).size() > prevResult.size() ) { edge.setBetaNew( - Canonical.union( prevResult, - intersection - ) + Canonical.unionORpreds( prevResult, + intersection + ) ); edgeWorkSet.add( edge ); } @@ -3293,7 +3293,7 @@ public class ReachGraph { // so make the new reachability set a union of the // nodes' reachability sets HeapRegionNode hrnB = id2hrn.get( idA ); - hrnB.setAlpha( Canonical.union( hrnB.getAlpha(), + hrnB.setAlpha( Canonical.unionORpreds( hrnB.getAlpha(), hrnA.getAlpha() ) ); @@ -3375,7 +3375,7 @@ public class ReachGraph { // just replace this beta set with the union assert edgeToMerge != null; edgeToMerge.setBeta( - Canonical.union( edgeToMerge.getBeta(), + Canonical.unionORpreds( edgeToMerge.getBeta(), edgeA.getBeta() ) ); @@ -3439,7 +3439,7 @@ public class ReachGraph { // so merge their reachability sets else { // just replace this beta set with the union - edgeToMerge.setBeta( Canonical.union( edgeToMerge.getBeta(), + edgeToMerge.setBeta( Canonical.unionORpreds( edgeToMerge.getBeta(), edgeA.getBeta() ) ); @@ -4083,14 +4083,14 @@ public class ReachGraph { Iterator itrEdge = hrn1.iteratorToReferencees(); while (itrEdge.hasNext()) { RefEdge edge = itrEdge.next(); - beta1 = Canonical.union(beta1, edge.getBeta()); + beta1 = Canonical.unionORpreds(beta1, edge.getBeta()); } ReachSet beta2 = ReachSet.factory(); itrEdge = hrn2.iteratorToReferencees(); while (itrEdge.hasNext()) { RefEdge edge = itrEdge.next(); - beta2 = Canonical.union(beta2, edge.getBeta()); + beta2 = Canonical.unionORpreds(beta2, edge.getBeta()); } boolean aliasDetected = false; diff --git a/Robust/src/Analysis/Disjoint/ReachSet.java b/Robust/src/Analysis/Disjoint/ReachSet.java index 62f60df3..49417732 100644 --- a/Robust/src/Analysis/Disjoint/ReachSet.java +++ b/Robust/src/Analysis/Disjoint/ReachSet.java @@ -67,6 +67,21 @@ public class ReachSet extends Canonical { return reachStates.contains( state ); } + // this should be a hash table so we can do this by key + public ReachState containsIgnorePreds( ReachState state ) { + assert state != null; + + Iterator stateItr = this.reachStates.iterator(); + while( stateItr.hasNext() ) { + ReachState stateThis = stateItr.next(); + if( stateThis.equalsIgnorePreds( state ) ) { + return stateThis; + } + } + + return null; + } + /* public boolean containsWithZeroes( ReachState state ) { assert state != null; @@ -146,6 +161,23 @@ public class ReachSet extends Canonical { return false; } + // used to assert each state in the set is + // unique + public boolean containsNoDuplicates() { + Vector v = new Vector( reachStates ); + for( int i = 0; i < v.size(); ++i ) { + ReachState s1 = v.get( i ); + for( int j = i+1; j < v.size(); ++j ) { + ReachState s2 = v.get( j ); + if( s1.equals( s2 ) ) { + assert s1.isCanonical(); + assert s2.isCanonical(); + return false; + } + } + } + return true; + } public boolean equals( Object o ) { diff --git a/Robust/src/Analysis/Disjoint/ReachState.java b/Robust/src/Analysis/Disjoint/ReachState.java index 21fc2811..a1052a6f 100644 --- a/Robust/src/Analysis/Disjoint/ReachState.java +++ b/Robust/src/Analysis/Disjoint/ReachState.java @@ -52,6 +52,19 @@ public class ReachState extends Canonical { return out; } + public static ReachState factory( HashSet reachTuples, + ExistPredSet preds + ) { + assert reachTuples != null; + assert preds != null; + assert preds.isCanonical(); + ReachState out = new ReachState(); + out.reachTuples.addAll( reachTuples ); + out.preds = preds; + out = (ReachState) Canonical.makeCanonical( out ); + return out; + } + protected ReachState() { reachTuples = new HashSet(); preds = ExistPredSet.factory(); @@ -116,10 +129,28 @@ public class ReachState extends Canonical { public int hashCodeSpecific() { - return reachTuples.hashCode() ^ preds.hashCode(); + return + reachTuples.hashCode() ^ + preds.hashCode(); + } + + + public boolean equalsIgnorePreds( Object o ) { + if( o == null ) { + return false; + } + + if( !(o instanceof ReachState) ) { + return false; + } + + ReachState rs = (ReachState) o; + return + reachTuples.equals( rs.reachTuples ); } + public String toString() { return reachTuples.toString(); }