From: jjenista Date: Fri, 19 Feb 2010 01:05:18 +0000 (+0000) Subject: big update--bringing implementation of new analysis into focus X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7704d7fae6615fc1ecb725ceef059c208d4a1ff2;p=IRC.git big update--bringing implementation of new analysis into focus --- diff --git a/Robust/src/Analysis/Disjoint/AccessPath.java b/Robust/src/Analysis/Disjoint/AccessPath.java deleted file mode 100644 index 4adc1261..00000000 --- a/Robust/src/Analysis/Disjoint/AccessPath.java +++ /dev/null @@ -1,57 +0,0 @@ -package Analysis.Disjoint; - -import IR.*; -import IR.Flat.*; -import java.util.*; - -// An access path is relevant in a callee method to -// a caller's heap. When mapping edges from a callee -// into the caller, if the caller's heap does not have -// any matching access paths, then the edge could not -// exist in that context and is ignored. - -public class AccessPath { - - public AccessPath() { - } - - public boolean equals( Object o ) { - if( o == null ) { - return false; - } - - if( !(o instanceof AccessPath) ) { - return false; - } - - return true; - /* - VariableSourceToken vst = (VariableSourceToken) o; - - // the reference vars have no bearing on equality - return sese.equals( vst.sese ) && - addrVar.equals( vst.addrVar ) && - seseAge.equals( vst.seseAge ); - */ - } - - public int hashCode() { - // the reference vars have no bearing on hashCode - return 1; //(sese.hashCode() << 3) * (addrVar.hashCode() << 4) ^ seseAge.intValue(); - } - - public String toString() { - return "ap"; - } - - public String toStringForDOT() { - /* - if( disjointId != null ) { - return "disjoint "+disjointId+"\\n"+toString()+"\\n"+getType().toPrettyString(); - } else { - return toString()+"\\n"+getType().toPrettyString(); - } - */ - return "do"; - } -} diff --git a/Robust/src/Analysis/Disjoint/AllocSite.java b/Robust/src/Analysis/Disjoint/AllocSite.java index ba857de5..617a27d6 100644 --- a/Robust/src/Analysis/Disjoint/AllocSite.java +++ b/Robust/src/Analysis/Disjoint/AllocSite.java @@ -5,13 +5,13 @@ import IR.Flat.*; import java.util.*; // allocation sites are independent of any particular -// ownership graph, unlike most of the other elements -// of the ownership analysis. An allocation site is +// reachability graph, unlike most of the other elements +// of the reachability analysis. An allocation site is // simply a collection of heap region identifiers that // are associated with a single allocation site in the // program under analysis. -// So two different ownership graphs may incorporate +// So two different reachability graphs may incorporate // nodes that represent the memory from one allocation // site. In this case there are two different sets of // HeapRegionNode objects, but they have the same @@ -19,7 +19,11 @@ import java.util.*; // object associated with the FlatNew node that gives // the graphs the identifiers in question. -public class AllocSite { +// note that an allocsite extends Canonical because they +// are Canonical, but specifically so an AllocSite can +// be an operand to a CanonicalOp + +public class AllocSite extends Canonical { static protected int uniqueIDcount = 0; @@ -66,7 +70,6 @@ public class AllocSite { return new Integer( uniqueIDcount ); } - public String getDisjointAnalysisId() { return disjointId; } @@ -189,6 +192,7 @@ public class AllocSite { return null; } + public String toString() { if( disjointId == null ) { return "allocSite"+id; @@ -223,6 +227,11 @@ public class AllocSite { s += "summary("+summary+")"; return s; } + + + public int hashCodeSpecific() { + return id; + } public void setFlag( boolean flag ) { this.flag = flag; diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java index 8e15a526..c5abe974 100644 --- a/Robust/src/Analysis/Disjoint/Canonical.java +++ b/Robust/src/Analysis/Disjoint/Canonical.java @@ -5,23 +5,798 @@ import IR.Flat.*; import java.util.*; import java.io.*; -public class Canonical { +abstract public class Canonical { - private static Hashtable canon = new Hashtable(); + private static int canonicalCount = 1; + + // the canon of objects + private static Hashtable + canon = new Hashtable(); + - int canonicalvalue; - private static int canonicalcount = 1; public static Canonical makeCanonical( Canonical c ) { - if( canon.containsKey(c) ) { - return canon.get(c); + if( canon.containsKey( c ) ) { + return canon.get( c ); } - c.canonicalvalue=canonicalcount++; - canon.put(c, c); + c.canonicalValue = canonicalCount; + ++canonicalCount; + canon.put( c, c ); return c; } - static Hashtable unionhash=new Hashtable(); - static Hashtable interhash=new Hashtable(); - static Hashtable lookuphash=new Hashtable(); + + // any Canonical with value still 0 is NOT CANONICAL! + private int canonicalValue = 0; + + public boolean isCanonical() { + return canonicalValue != 0; + } + + public int getCanonicalValue() { + assert isCanonical(); + return canonicalValue; + } + + + // canonical objects should never be modified + // and therefore have changing hash codes, so + // use a standard canonical hash code method to + // enforce this, and define a specific hash code + // method each specific subclass should implement + abstract public int hashCodeSpecific(); + + private boolean hasHash = false; + private int oldHash; + final public int hashCode() { + int hash = hashCodeSpecific(); + + if( hasHash ) { + if( oldHash != hash ) { + throw new Error( "A CANONICAL HASH CHANGED" ); + } + } else { + hasHash = true; + oldHash = hash; + } + + return hash; + } + + + + + // mapping of a non-trivial operation to its result + private static Hashtable + op2result = new Hashtable(); + + + + /////////////////////////////////////////////////////////// + // + // Everything below are static methods that implement + // "mutating" operations on Canonical objects by returning + // the canonical result. If the op is non-trivial the + // canonical result is hashed by its defining CononicalOp + // + /////////////////////////////////////////////////////////// + + + // not weighty, don't bother with caching + public static ReachTuple unionArity( ReachTuple rt1, + ReachTuple rt2 ) { + assert rt1 != null; + assert rt2 != null; + assert rt1.isCanonical(); + assert rt2.isCanonical(); + assert rt1.hrnID == rt2.hrnID; + assert rt1.isMultiObject == rt2.isMultiObject; + + ReachTuple out; + + if( rt1.isMultiObject ) { + // on two non-ZERO arity multi regions, union arity is always + // ZERO-OR-MORE + out = ReachTuple.factory( rt1.hrnID, + true, + ReachTuple.ARITY_ZEROORMORE ); + + } else { + // a single object region can only be ARITY_ONE (or zero by + // being absent) + assert rt1.arity == ReachTuple.ARITY_ONE; + out = rt1; + } + + assert out.isCanonical(); + return out; + } + + // not weighty, no caching + public static ReachTuple changeHrnIDTo( ReachTuple rt, + Integer hrnIDToChangeTo ) { + assert rt != null; + assert hrnIDToChangeTo != null; + + ReachTuple out = ReachTuple.factory( hrnIDToChangeTo, + rt.isMultiObject, + rt.arity + ); + assert out.isCanonical(); + return out; + } + + + public 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 = ReachState.factory(); + out.reachTuples.addAll( rs1.reachTuples ); + out.reachTuples.addAll( rs2.reachTuples ); + + 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 ) { + assert rs != null; + assert rt != null; + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSTATE_UNION_REACHTUPLE, + rs, + rt ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachState) result; + } + + // otherwise, no cached result... + ReachState out = ReachState.factory(); + out.reachTuples.addAll( rs.reachTuples ); + out.reachTuples.add( rt ); + + out = (ReachState) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ReachState unionUpArity( ReachState rs1, + ReachState rs2 ) { + assert rs1 != null; + assert rs2 != null; + assert rs1.isCanonical(); + assert rs2.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSTATE_UNIONUPARITY_REACHSTATE, + rs1, + rs2 ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachState) result; + } + + // otherwise, no cached result... + ReachState out = ReachState.factory(); + + Iterator rtItr = rs1.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rt1 = rtItr.next(); + ReachTuple rt2 = rs2.containsHrnID( rt1.getHrnID() ); + + if( rt2 != null ) { + out.reachTuples.add( unionArity( rt1, rt2 ) ); + } else { + out.reachTuples.add( rt1 ); + } + } + + rtItr = rs2.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rt2 = rtItr.next(); + ReachTuple rto = out.containsHrnID( rt2.getHrnID() ); + + if( rto == null ) { + out.reachTuples.add( rto ); + } + } + + out = (ReachState) makeCanonical( out ); + op2result.put( op, out ); + 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; + assert rt != null; + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSTATE_REMOVE_REACHTUPLE, + rs, + rt ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachState) result; + } + + // otherwise, no cached result... + ReachState out = ReachState.factory(); + out.reachTuples.addAll( rs.reachTuples ); + out.reachTuples.remove( rt ); + + out = (ReachState) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ReachState ageTuplesFrom( ReachState rs, + AllocSite as ) { + assert rs != null; + assert as != null; + assert rs.isCanonical(); + assert as.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSTATE_AGETUPLESFROM_ALLOCSITE, + rs, + as ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachState) result; + } + + // otherwise, no cached result... + ReachState out = ReachState.factory(); + + ReachTuple rtSummary = null; + ReachTuple rtOldest = null; + + Iterator rtItr = rs.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rt = rtItr.next(); + Integer hrnID = rt.getHrnID(); + int age = as.getAgeCategory( hrnID ); + + // hrnIDs not associated with + // the site should be left alone + if( age == AllocSite.AGE_notInThisSite ) { + out.reachTuples.add( rt ); + + } else if( age == AllocSite.AGE_summary ) { + // remember the summary tuple, but don't add it + // we may combine it with the oldest tuple + rtSummary = rt; + + } else if( age == AllocSite.AGE_oldest ) { + // found an oldest hrnID, again just remember + // for later + rtOldest = rt; + + } else { + assert age == AllocSite.AGE_in_I; + + Integer I = as.getAge( hrnID ); + assert I != null; + + // otherwise, we change this hrnID to the + // next older hrnID + Integer hrnIDToChangeTo = as.getIthOldest( I + 1 ); + ReachTuple rtAged = + Canonical.changeHrnIDTo( rt, hrnIDToChangeTo ); + out.reachTuples.add( rtAged ); + } + } + + // there are four cases to consider here + // 1. we found a summary tuple and no oldest tuple + // Here we just pass the summary unchanged + // 2. we found an oldest tuple, no summary + // Make a new, arity-one summary tuple + // 3. we found both a summary and an oldest + // Merge them by arity + // 4. (not handled) we found neither, do nothing + if( rtSummary != null && rtOldest == null ) { + out.reachTuples.add( rtSummary ); + + } else if( rtSummary == null && rtOldest != null ) { + out.reachTuples.add( ReachTuple.factory( as.getSummary(), + true, + rtOldest.getArity() + ) + ); + + } else if( rtSummary != null && rtOldest != null ) { + out.reachTuples.add( Canonical.unionArity( rtSummary, + ReachTuple.factory( as.getSummary(), + true, + rtOldest.getArity() + ) + ) + ); + } + + out = (ReachState) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + + public static ReachSet union( ReachSet rs1, + ReachSet rs2 ) { + assert rs1 != null; + assert rs2 != null; + assert rs1.isCanonical(); + assert rs2.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_UNION_REACHSET, + rs1, + rs2 ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + 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 ) { + + assert rs != null; + assert state != null; + assert rs.isCanonical(); + assert state.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_UNION_REACHSTATE, + rs, + state ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + 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; + assert rs2 != null; + assert rs1.isCanonical(); + assert rs2.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_INTERSECTION_REACHSET, + rs1, + rs2 ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + Iterator itr = rs1.iterator(); + while( itr.hasNext() ) { + ReachState state = (ReachState) itr.next(); + if( rs2.reachStates.contains( state ) ) { + out.reachStates.add( state ); + } + } + + out = (ReachSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ReachSet add( ReachSet rs, + ReachState state ) { + return union( rs, state ); + } + + public static ReachSet remove( ReachSet rs, + ReachState state ) { + assert rs != null; + assert state != null; + assert rs.isCanonical(); + assert state.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_REMOVE_REACHSTATE, + rs, + state ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + out.reachStates.addAll( rs.reachStates ); + out.reachStates.remove( state ); + + out = (ReachSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ReachSet applyChangeSet( ReachSet rs, + ChangeSet cs, + boolean keepSourceState ) { + assert rs != null; + assert cs != null; + assert rs.isCanonical(); + assert cs.isCanonical(); + + // this primitive operand stuff is just a way to + // ensure distinct inputs to a CanonicalOp + int primOperand; + if( keepSourceState ) { + primOperand = 0x1f; + } else { + primOperand = 0x2b; + } + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_APPLY_CHANGESET, + rs, + cs, + primOperand ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + + Iterator stateItr = rs.iterator(); + while( stateItr.hasNext() ) { + ReachState state = stateItr.next(); + + boolean changeFound = false; + + Iterator ctItr = cs.iterator(); + while( ctItr.hasNext() ) { + ChangeTuple ct = ctItr.next(); + + if( state.equals( ct.getSetToMatch() ) ) { + out.reachStates.add( ct.getSetToAdd() ); + changeFound = true; + } + } + + if( keepSourceState || !changeFound ) { + out.reachStates.add( state ); + } + } + + out = (ReachSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ChangeSet unionUpArityToChangeSet( ReachSet rsO, + ReachSet rsR ) { + assert rsO != null; + assert rsR != null; + assert rsO.isCanonical(); + assert rsR.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_UNIONTOCHANGESET_REACHSET, + rsO, + rsR ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ChangeSet) result; + } + + // otherwise, no cached result... + ChangeSet out = ChangeSet.factory(); + + Iterator itrO = rsO.iterator(); + while( itrO.hasNext() ) { + ReachState o = itrO.next(); + + Iterator itrR = rsR.iterator(); + while( itrR.hasNext() ) { + ReachState r = itrR.next(); + + ReachState theUnion = ReachState.factory(); + + Iterator itrRelement = r.iterator(); + while( itrRelement.hasNext() ) { + ReachTuple rtR = itrRelement.next(); + ReachTuple rtO = o.containsHrnID( rtR.getHrnID() ); + + if( rtO != null ) { + theUnion = Canonical.union( theUnion, + Canonical.unionArity( rtR, + rtO + ) + ); + } else { + theUnion = Canonical.union( theUnion, + rtR + ); + } + } + + Iterator itrOelement = o.iterator(); + while( itrOelement.hasNext() ) { + ReachTuple rtO = itrOelement.next(); + ReachTuple rtR = theUnion.containsHrnID( rtO.getHrnID() ); + + if( rtR == null ) { + theUnion = Canonical.union( theUnion, + rtO + ); + } + } + + if( !theUnion.isEmpty() ) { + out = + Canonical.union( out, + ChangeSet.factory( + ChangeTuple.factory( o, theUnion ) + ) + ); + } + } + } + + out = (ChangeSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ReachSet ageTuplesFrom( ReachSet rs, + AllocSite as ) { + assert rs != null; + assert as != null; + assert rs.isCanonical(); + assert as.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_AGETUPLESFROM_ALLOCSITE, + rs, + as ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + + Iterator itrS = rs.iterator(); + while( itrS.hasNext() ) { + ReachState state = itrS.next(); + out.reachStates.add( Canonical.ageTuplesFrom( state, as ) ); + } + + out = (ReachSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ReachSet pruneBy( ReachSet rsO, + ReachSet rsP ) { + assert rsO != null; + assert rsP != null; + assert rsO.isCanonical(); + assert rsP.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.REACHSET_PRUNEBY_REACHSET, + rsO, + rsP ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ReachSet) result; + } + + // otherwise, no cached result... + ReachSet out = ReachSet.factory(); + + Iterator itrO = rsO.iterator(); + while( itrO.hasNext() ) { + ReachState stateO = itrO.next(); + + boolean subsetExists = false; + + Iterator itrP = rsP.iterator(); + while( itrP.hasNext() && !subsetExists ) { + ReachState stateP = itrP.next(); + + if( stateP.isSubset( stateO ) ) { + subsetExists = true; + } + } + + if( subsetExists ) { + out.reachStates.add( stateO ); + } + } + + out = (ReachSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + public static ChangeSet union( ChangeSet cs1, + ChangeSet cs2 ) { + assert cs1 != null; + assert cs2 != null; + assert cs1.isCanonical(); + assert cs2.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.CHANGESET_UNION_CHANGESET, + cs1, + cs2 ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ChangeSet) result; + } + + // otherwise, no cached result... + ChangeSet out = ChangeSet.factory(); + out.changeTuples.addAll( cs1.changeTuples ); + out.changeTuples.addAll( cs2.changeTuples ); + + out = (ChangeSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + public static ChangeSet union( ChangeSet cs, + ChangeTuple ct ) { + assert cs != null; + assert ct != null; + assert cs.isCanonical(); + assert ct.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.CHANGESET_UNION_CHANGETUPLE, + cs, + ct ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ChangeSet) result; + } + + // otherwise, no cached result... + ChangeSet out = ChangeSet.factory(); + out.changeTuples.addAll( cs.changeTuples ); + out.changeTuples.add( ct ); + + out = (ChangeSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + + + public static ExistPredSet join( ExistPredSet eps1, + ExistPredSet eps2 ) { + + assert eps1 != null; + assert eps2 != null; + assert eps1.isCanonical(); + assert eps2.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.EXISTPREDSET_JOIN_EXISTPREDSET, + eps1, + eps2 ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ExistPredSet) result; + } + + // otherwise, no cached result... + ExistPredSet out = ExistPredSet.factory(); + out.preds.addAll( eps1.preds ); + out.preds.addAll( eps2.preds ); + + out = (ExistPredSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + public static ExistPredSet add( ExistPredSet eps, + ExistPred ep ) { + + + assert eps != null; + assert ep != null; + assert eps.isCanonical(); + assert ep.isCanonical(); + + CanonicalOp op = + new CanonicalOp( CanonicalOp.EXISTPREDSET_ADD_EXISTPRED, + eps, + ep ); + + Canonical result = op2result.get( op ); + if( result != null ) { + return (ExistPredSet) result; + } + + // otherwise, no cached result... + ExistPredSet out = ExistPredSet.factory(); + out.preds.addAll( eps.preds ); + out.preds.add( ep ); + + out = (ExistPredSet) makeCanonical( out ); + op2result.put( op, out ); + return out; + } + + } diff --git a/Robust/src/Analysis/Disjoint/CanonicalOp.java b/Robust/src/Analysis/Disjoint/CanonicalOp.java new file mode 100644 index 00000000..6cccb4b5 --- /dev/null +++ b/Robust/src/Analysis/Disjoint/CanonicalOp.java @@ -0,0 +1,72 @@ +package Analysis.Disjoint; + +// a CanonicalOperation defines an operation on +// Canonical objects. The Canonical class maps +// an op to its result, so when you ask the +// Canonical static methods to do an op that is +// non-trivial, it will generate one of these +// first and do a result look-up +public class CanonicalOp { + + public static final int REACHTUPLE_UNIONARITY_REACHTUPLE = 0x1a34; + public static final int REACHSTATE_UNION_REACHSTATE = 0x5678; + public static final int REACHSTATE_UNION_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_INTERSECTION_REACHSET = 0x3361; + public static final int REACHSET_REMOVE_REACHSTATE = 0x9391; + public static final int REACHSET_APPLY_CHANGESET = 0x1d55; + public static final int REACHSET_UNIONTOCHANGESET_REACHSET = 0x46a9; + public static final int REACHSET_AGETUPLESFROM_ALLOCSITE = 0x22bb; + public static final int REACHSET_PRUNEBY_REACHSET = 0xd774; + public static final int CHANGESET_UNION_CHANGESET = 0x53b3; + public static final int CHANGESET_UNION_CHANGETUPLE = 0x9ee4; + public static final int EXISTPREDSET_JOIN_EXISTPREDSET = 0x8a21; + public static final int EXISTPREDSET_ADD_EXISTPRED = 0xba5f; + public static final int PRIM_OP_UNUSED = 0xef01; + + protected int opCode; + protected Canonical operand1; + protected Canonical operand2; + protected int operand3; + + public CanonicalOp( int opc, + Canonical op1, + Canonical op2 ) { + this( opc, op1, op2, PRIM_OP_UNUSED ); + } + + public CanonicalOp( int opc, + Canonical op1, + Canonical op2, + int op3 ) { + assert op1.isCanonical(); + assert op2.isCanonical(); + opCode = opc; + operand1 = op1; + operand2 = op2; + operand3 = op3; + } + + public int hashCode() { + return opCode ^ + (operand1.getCanonicalValue() << 2) ^ + (operand2.getCanonicalValue() << 1) ^ + (operand3 << 3); + } + + public boolean equals( Object o ) { + if( o == null ) { + return false; + } + + CanonicalOp co = (CanonicalOp) o; + return opCode == co.opCode && + (operand1.getCanonicalValue() == co.operand1.getCanonicalValue()) && + (operand2.getCanonicalValue() == co.operand2.getCanonicalValue()) && + operand3 == co.operand3; + } +} diff --git a/Robust/src/Analysis/Disjoint/ChangeSet.java b/Robust/src/Analysis/Disjoint/ChangeSet.java index cc110894..a9f36e82 100644 --- a/Robust/src/Analysis/Disjoint/ChangeSet.java +++ b/Robust/src/Analysis/Disjoint/ChangeSet.java @@ -5,29 +5,48 @@ import IR.Flat.*; import java.util.*; import java.io.*; +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// public class ChangeSet extends Canonical { - private HashSet changeTuples; + protected HashSet changeTuples; - public ChangeSet() { - changeTuples = new HashSet(); - } - - public ChangeSet(ChangeTuple ct) { - this(); - changeTuples.add(ct); + public static ChangeSet factory() { + ChangeSet out = new ChangeSet(); + out = (ChangeSet) Canonical.makeCanonical( out ); + return out; } - public ChangeSet(ChangeSet cts) { - changeTuples = (HashSet)cts.changeTuples.clone(); - } + public static ChangeSet factory( ChangeTuple ct ) { + assert ct != null; + assert ct.isCanonical(); + ChangeSet out = new ChangeSet(); + out.changeTuples.add( ct ); + out = (ChangeSet) Canonical.makeCanonical( out ); + return out; + } - public ChangeSet makeCanonical() { - return (ChangeSet) Canonical.makeCanonical(this); + private ChangeSet() { + changeTuples = new HashSet(); } - public Iterator iterator() { + public Iterator iterator() { return changeTuples.iterator(); } @@ -35,29 +54,13 @@ public class ChangeSet extends Canonical { return changeTuples.size(); } - public ChangeSet union(ChangeSet ctsIn) { - assert ctsIn != null; - - ChangeSet ctsOut = new ChangeSet(this); - ctsOut.changeTuples.addAll(ctsIn.changeTuples); - return ctsOut.makeCanonical(); - } - - public ChangeSet union(ChangeTuple ctIn) { - assert ctIn != null; - - ChangeSet ctsOut = new ChangeSet(this); - ctsOut.changeTuples.add(ctIn); - return ctsOut.makeCanonical(); - } - public boolean isEmpty() { return changeTuples.isEmpty(); } - public boolean isSubset(ChangeSet ctsIn) { + public boolean isSubset( ChangeSet ctsIn ) { assert ctsIn != null; - return ctsIn.changeTuples.containsAll(this.changeTuples); + return ctsIn.changeTuples.containsAll( this.changeTuples ); } @@ -71,26 +74,13 @@ public class ChangeSet extends Canonical { } ChangeSet cts = (ChangeSet) o; - return changeTuples.equals(cts.changeTuples); + assert this.isCanonical(); + assert cts.isCanonical(); + return this == cts; } - private boolean oldHashSet = false; - private int oldHash = 0; - public int hashCode() { - int currentHash = changeTuples.hashCode(); - - if( oldHashSet == false ) { - oldHash = currentHash; - oldHashSet = true; - } else { - if( oldHash != currentHash ) { - System.out.println("IF YOU SEE THIS A CANONICAL ChangeSet CHANGED"); - Integer x = null; - x.toString(); - } - } - - return currentHash; + public int hashCodeSpecific() { + return changeTuples.hashCode(); } diff --git a/Robust/src/Analysis/Disjoint/ChangeTuple.java b/Robust/src/Analysis/Disjoint/ChangeTuple.java index 8a91b609..b579c16a 100644 --- a/Robust/src/Analysis/Disjoint/ChangeTuple.java +++ b/Robust/src/Analysis/Disjoint/ChangeTuple.java @@ -5,71 +5,76 @@ import IR.Flat.*; import java.util.*; import java.io.*; - -// a change touple is a pair that indicates if the +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// + +// a change tuple is a pair that indicates if the // first ReachState is found in a ReachSet, // then the second ReachState should be added -// THIS CLASS IS IMMUTABLE! - public class ChangeTuple extends Canonical { - private ReachState toMatch; - private ReachState toAdd; + protected ReachState toMatch; + protected ReachState toAdd; + + public static ChangeTuple factory( ReachState toMatch, + ReachState toAdd ) { + ChangeTuple out = new ChangeTuple( toMatch, + toAdd ); + out = (ChangeTuple) Canonical.makeCanonical( out ); + return out; + } - public ChangeTuple(ReachState toMatch, - ReachState toAdd) { + private ChangeTuple( ReachState toMatch, + ReachState toAdd ) { this.toMatch = toMatch; this.toAdd = toAdd; } - public ChangeTuple makeCanonical() { - return (ChangeTuple) Canonical.makeCanonical(this); - } - public ReachState getSetToMatch() { return toMatch; } public ReachState getSetToAdd() { return toAdd; } + - - public boolean equals(Object o) { + public boolean equals( Object o ) { if( o == null ) { return false; } - + if( !(o instanceof ChangeTuple) ) { return false; } ChangeTuple ct = (ChangeTuple) o; - - return toMatch.equals(ct.getSetToMatch() ) && - toAdd.equals(ct.getSetToAdd() ); + assert this.isCanonical(); + assert ct.isCanonical(); + return this == ct; } - private boolean oldHashSet = false; - private int oldHash = 0; - public int hashCode() { - int currentHash = toMatch.hashCode() + toAdd.hashCode()*3; - - if( oldHashSet == false ) { - oldHash = currentHash; - oldHashSet = true; - } else { - if( oldHash != currentHash ) { - System.out.println("IF YOU SEE THIS A CANONICAL ChangeTuple CHANGED"); - Integer x = null; - x.toString(); - } - } - - return currentHash; + public int hashCodeSpecific() { + return + toMatch.hashCode() ^ + toAdd.hashCode()*3; } - public String toString() { return new String("("+toMatch+" -> "+toAdd+")"); } diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index 914b1092..656610ec 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -717,7 +717,11 @@ public class DisjointAnalysis { if( !mapFlatNewToAllocSite.containsKey( fnew ) ) { AllocSite as = - new AllocSite( allocationDepth, fnew, fnew.getDisjointId() ); + (AllocSite) Canonical.makeCanonical( new AllocSite( allocationDepth, + fnew, + fnew.getDisjointId() + ) + ); // the newest nodes are single objects for( int i = 0; i < allocationDepth; ++i ) { diff --git a/Robust/src/Analysis/Disjoint/ExistPred.java b/Robust/src/Analysis/Disjoint/ExistPred.java index c71b31bd..2c1f56b7 100644 --- a/Robust/src/Analysis/Disjoint/ExistPred.java +++ b/Robust/src/Analysis/Disjoint/ExistPred.java @@ -5,19 +5,375 @@ import IR.Flat.*; import java.util.*; import java.io.*; -// these existence predicates on elements of -// a callee graph allow a caller to prune the -// pieces of the graph that don't apply when -// predicates are not satisfied in the -// caller's context +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// -abstract public class ExistPred extends Canonical { +// Existence predicates in the callee final-result +// graph are relevant on the caller's callee-reachable +// graph parts. Any callee result elements with +// predicates not satisfied in the caller are not +// mapped in the call site transfer function - public ExistPred makeCanonical() { - return (ExistPred) Canonical.makeCanonical( this ); +public class ExistPred extends Canonical { + + // there are several types of predicates, note that + // there are not subclasses of the ExistPred class + // because they must be Canonical, no multiple inheritence + + // types: true, node, edge + public static final int TYPE_TRUE = 0xa501; + public static final int TYPE_NODE = 0x02fd; + public static final int TYPE_EDGE = 0x414b; + protected int predType; + + // true predicates always evaluate to true + + // A node existence predicate is satisfied if the heap + // region ID defining a node is part of the given graph + // The reach state may be null--if not the predicate is + // satisfied when the edge exists AND it has the state. + protected Integer n_hrnID; + protected ReachState ne_state; + + // An edge existence predicate is satisfied if the elements + // defining an edge are part of the given graph. + // The reach state may be null--if not the predicate is + // satisfied when the edge exists AND it has the state. + // the source of an edge is *either* a variable + // node or a heap region node + protected TempDescriptor e_tdSrc; + protected Integer e_hrnSrcID; + + // dst is always a heap region + protected Integer e_hrnDstID; + + // a reference has a field name and type + protected TypeDescriptor e_type; + protected String e_field; + + // edge uses same ReachState ne_state as node type above + + + // to make the true predicate + public static ExistPred factory() { + ExistPred out = new ExistPred(); + out = (ExistPred) Canonical.makeCanonical( out ); + return out; + } + + private ExistPred() { + this.predType = TYPE_TRUE; + } + + // node predicates + public static ExistPred factory( Integer hrnID, + ReachState state ) { + ExistPred out = new ExistPred( hrnID, state ); + out = (ExistPred) Canonical.makeCanonical( out ); + return out; + } + + private ExistPred( Integer hrnID, + ReachState state ) { + assert hrnID != null; + this.n_hrnID = hrnID; + this.ne_state = state; + this.predType = TYPE_NODE; + } + + // edge predicates + public static ExistPred factory( TempDescriptor tdSrc, + Integer hrnSrcID, + Integer hrnDstID, + TypeDescriptor type, + String field, + ReachState state ) { + ExistPred out = new ExistPred( tdSrc, + hrnSrcID, + hrnDstID, + type, + field, + state ); + out = (ExistPred) Canonical.makeCanonical( out ); + return out; + } + + private ExistPred( TempDescriptor tdSrc, + Integer hrnSrcID, + Integer hrnDstID, + TypeDescriptor type, + String field, + ReachState state ) { + + assert (tdSrc == null) || (hrnSrcID == null); + assert hrnDstID != null; + assert type != null; + + // fields can be null when the edge is from + // a variable node to a heap region! + // assert field != null; + + this.e_tdSrc = tdSrc; + this.e_hrnSrcID = hrnSrcID; + this.e_hrnDstID = hrnDstID; + this.e_type = type; + this.e_field = field; + this.ne_state = state; + this.predType = TYPE_EDGE; + } + + + public boolean isSatisfiedBy( ReachGraph rg ) { + if( predType == TYPE_TRUE ) { + return true; + } + + if( predType == TYPE_NODE ) { + // first find node + HeapRegionNode hrn = rg.id2hrn.get( n_hrnID ); + if( hrn == null ) { + return false; + } + + // when the state is null it is not part of the + // predicate, so we've already satisfied + if( ne_state == null ) { + return true; + } + + // otherwise look for state too + // TODO: contains OR containsSuperSet OR containsWithZeroes?? + return hrn.getAlpha().contains( ne_state ); + } + + if( predType == TYPE_EDGE ) { + // first establish whether the source of the + // reference edge exists + VariableNode vnSrc = rg.td2vn.get( e_tdSrc ); + HeapRegionNode hrnSrc = rg.id2hrn.get( e_hrnSrcID ); + assert (vnSrc == null) || (hrnSrc == null); + + // the source is not present in graph + if( vnSrc == null && hrnSrc == null ) { + return false; + } + + RefSrcNode rsn; + if( vnSrc != null ) { + rsn = vnSrc; + } else { + rsn = hrnSrc; + } + + // is the destination present? + HeapRegionNode hrnDst = rg.id2hrn.get( e_hrnDstID ); + if( hrnDst == null ) { + return false; + } + + // is there an edge between them with the given + // type and field? + // TODO: type OR a subtype? + RefEdge edge = rsn.getReferenceTo( hrnDst, + e_type, + e_field ); + if( edge == null ) { + return false; + } + + // when state is null it is not part of the predicate + // so we've satisfied the edge existence + if( ne_state == null ) { + return true; + } + + // otherwise look for state too + // TODO: contains OR containsSuperSet OR containsWithZeroes?? + return hrnDst.getAlpha().contains( ne_state ); + } + + throw new Error( "Unknown predicate type" ); + } + + + public boolean equals( Object o ) { + if( o == null ) { + return false; + } + + if( !(o instanceof ExistPred) ) { + return false; + } + + ExistPred pred = (ExistPred) o; + assert this.isCanonical(); + assert pred.isCanonical(); + return this == pred; + } + /* + public boolean equals( Object o ) { + if( o == null ) { + return false; + } + + if( !(o instanceof ExistPredNode) ) { + return false; + } + + ExistPredNode epn = (ExistPredNode) o; + + if( !hrnID.equals( epn.hrnID ) ) { + return false; + } + + // ReachState objects are canonical + return state == epn.state; + } + + public boolean equals( Object o ) { + if( o == null ) { + return false; + } + + if( !(o instanceof ExistPredEdge) ) { + return false; + } + + ExistPredEdge epn = (ExistPredEdge) o; + + this.tdSrc = tdSrc; + this.hrnSrcID = hrnSrcID; + this.hrnDstID = hrnDstID; + this.type = type; + this.field = field; + this.state = state; + + if( tdSrc == null && epn.tdSrc != null ) { + return false; + } else if( !tdSrc.equals( epn.tdSrc ) ) { + return false; + } + + if( hrnSrcID == null && epn.hrnSrcID != null ) { + return false; + } else if( !hrnSrcID.equals( epn.hrnSrcID ) ) { + return false; + } + + if( !hrnDstID.equals( epn.hrnDstID ) ) { + return false; + } + + if( !type.equals( epn.type ) ) { + return false; + } + + if( field == null ) { + if( epn.field != null ) { + return false; + } + } else { + if( !field.equals( epn.field ) ) { + return false; + } + } + + // ReachState objects are cannonical + return state == epn.state; + } + */ + + + public int hashCodeSpecific() { + if( predType == TYPE_TRUE ) { + return 1; + } + + if( predType == TYPE_NODE ) { + int hash = n_hrnID.intValue()*17; + + if( ne_state != null ) { + hash += ne_state.hashCode(); + } + + return hash; + } + + if( predType == TYPE_EDGE ) { + int hash = 0; + + hash += e_type.hashCode()*17; + + if( e_field != null ) { + hash += e_field.hashCode()*7; + } + + if( e_tdSrc != null ) { + hash += e_tdSrc.hashCode()*11; + } else { + hash += e_hrnSrcID.hashCode()*11; + } + + hash += e_hrnDstID.hashCode(); + + if( ne_state != null ) { + hash += ne_state.hashCode(); + } + + return hash; + } + + throw new Error( "Unknown predicate type" ); } - public boolean isSatisfiedBy( ReachGraph rg ) { - return true; + + public String toString() { + if( predType == TYPE_TRUE ) { + return "t"; + } + + if( predType == TYPE_NODE ) { + String s = n_hrnID.toString(); + if( ne_state != null ) { + s += "w"+ne_state; + } + return s; + } + + if( predType == TYPE_EDGE ) { + String s = "("; + + if( e_tdSrc != null ) { + s += e_tdSrc.toString(); + } else { + s += e_hrnSrcID.toString(); + } + + s += "-->"+e_hrnDstID+")"; + + if( ne_state != null ) { + s += "w"+ne_state; + } + + return s; + } + + throw new Error( "Unknown predicate type" ); } + } diff --git a/Robust/src/Analysis/Disjoint/ExistPredEdge.java b/Robust/src/Analysis/Disjoint/ExistPredEdge.java deleted file mode 100644 index ee0f188e..00000000 --- a/Robust/src/Analysis/Disjoint/ExistPredEdge.java +++ /dev/null @@ -1,194 +0,0 @@ -package Analysis.Disjoint; - -import IR.*; -import IR.Flat.*; -import java.util.*; -import java.io.*; - -// A edge existence predicate is satisfied if the elements -// defining an edge are part of the given graph. -// The reach state may be null--if not the predicate is -// satisfied when the edge exists AND it has the state. - -public class ExistPredEdge extends ExistPred { - - // the source of an edge is *either* a variable - // node or a heap region node - protected TempDescriptor tdSrc; - protected Integer hrnSrcID; - - // dst is always a heap region - protected Integer hrnDstID; - - // a reference has a field name and type - protected TypeDescriptor type; - protected String field; - - // state can be null - protected ReachState state; - - - public ExistPredEdge( TempDescriptor tdSrc, - Integer hrnSrcID, - Integer hrnDstID, - TypeDescriptor type, - String field, - ReachState state ) { - - assert (tdSrc == null) || (hrnSrcID == null); - assert hrnDstID != null; - assert type != null; - - // fields can be null when the edge is from - // a variable node to a heap region! - // assert field != null; - - this.tdSrc = tdSrc; - this.hrnSrcID = hrnSrcID; - this.hrnDstID = hrnDstID; - this.type = type; - this.field = field; - this.state = state; - } - - public boolean isSatisfiedBy( ReachGraph rg ) { - - // first establish whether the source of the - // reference edge exists - VariableNode vnSrc = rg.td2vn.get( tdSrc ); - HeapRegionNode hrnSrc = rg.id2hrn.get( hrnSrcID ); - assert (vnSrc == null) || (hrnSrc == null); - - // the source is not present in graph - if( vnSrc == null && hrnSrc == null ) { - return false; - } - - RefSrcNode rsn; - if( vnSrc != null ) { - rsn = vnSrc; - } else { - rsn = hrnSrc; - } - - // is the destination present? - HeapRegionNode hrnDst = rg.id2hrn.get( hrnDstID ); - if( hrnDst == null ) { - return false; - } - - // is there an edge between them with the given - // type and field? - // TODO: type OR a subtype? - RefEdge edge = rsn.getReferenceTo( hrnDst, type, field ); - if( edge == null ) { - return false; - } - - // when state is null it is not part of the predicate - // so we've satisfied the edge existence - if( state == null ) { - return true; - } - - // otherwise look for state too - // TODO: contains OR containsSuperSet OR containsWithZeroes?? - return hrnDst.getAlpha().contains( state ); - } - - - public boolean equals( Object o ) { - if( o == null ) { - return false; - } - - if( !(o instanceof ExistPredEdge) ) { - return false; - } - - ExistPredEdge epn = (ExistPredEdge) o; - - this.tdSrc = tdSrc; - this.hrnSrcID = hrnSrcID; - this.hrnDstID = hrnDstID; - this.type = type; - this.field = field; - this.state = state; - - if( tdSrc == null && epn.tdSrc != null ) { - return false; - } else if( !tdSrc.equals( epn.tdSrc ) ) { - return false; - } - - if( hrnSrcID == null && epn.hrnSrcID != null ) { - return false; - } else if( !hrnSrcID.equals( epn.hrnSrcID ) ) { - return false; - } - - if( !hrnDstID.equals( epn.hrnDstID ) ) { - return false; - } - - if( !type.equals( epn.type ) ) { - return false; - } - - if( field == null ) { - if( epn.field != null ) { - return false; - } - } else { - if( !field.equals( epn.field ) ) { - return false; - } - } - - // ReachState objects are cannonical - return state == epn.state; - } - - public int hashCode() { - int hash = 0; - - hash += type.hashCode()*17; - - if( field != null ) { - hash += field.hashCode()*7; - } - - if( tdSrc != null ) { - hash += tdSrc.hashCode()*11; - } else { - hash += hrnSrcID.hashCode()*11; - } - - hash += hrnDstID.hashCode(); - - if( state != null ) { - hash += state.hashCode(); - } - - return hash; - } - - - public String toString() { - String s = "("; - - if( tdSrc != null ) { - s += tdSrc.toString(); - } else { - s += hrnSrcID.toString(); - } - - s += "-->"+hrnDstID+")"; - - if( state != null ) { - s += "w"+state; - } - - return s; - } -} diff --git a/Robust/src/Analysis/Disjoint/ExistPredNode.java b/Robust/src/Analysis/Disjoint/ExistPredNode.java deleted file mode 100644 index 4a2d610a..00000000 --- a/Robust/src/Analysis/Disjoint/ExistPredNode.java +++ /dev/null @@ -1,83 +0,0 @@ -package Analysis.Disjoint; - -import IR.*; -import IR.Flat.*; -import java.util.*; -import java.io.*; - -// A node existence predicate is satisfied if the heap -// region ID defining a node is part of the given graph -// The reach state may be null--if not the predicate is -// satisfied when the edge exists AND it has the state. - -public class ExistPredNode extends ExistPred { - - protected Integer hrnID; - protected ReachState state; - - public ExistPredNode( Integer hrnID, ReachState state ) { - assert hrnID != null; - - this.hrnID = hrnID; - this.state = state; - } - - - public boolean isSatisfiedBy( ReachGraph rg ) { - - // first find node - HeapRegionNode hrn = rg.id2hrn.get( hrnID ); - if( hrn == null ) { - return false; - } - - // when the state is null it is not part of the - // predicate, so we've already satisfied - if( state == null ) { - return true; - } - - // otherwise look for state too - // TODO: contains OR containsSuperSet OR containsWithZeroes?? - return hrn.getAlpha().contains( state ); - } - - - public boolean equals( Object o ) { - if( o == null ) { - return false; - } - - if( !(o instanceof ExistPredNode) ) { - return false; - } - - ExistPredNode epn = (ExistPredNode) o; - - if( !hrnID.equals( epn.hrnID ) ) { - return false; - } - - // ReachState objects are canonical - return state == epn.state; - } - - public int hashCode() { - int hash = hrnID.intValue()*17; - - if( state != null ) { - hash += state.hashCode(); - } - - return hash; - } - - - public String toString() { - String s = hrnID.toString(); - if( state != null ) { - s += "w"+state; - } - return s; - } -} diff --git a/Robust/src/Analysis/Disjoint/ExistPredSet.java b/Robust/src/Analysis/Disjoint/ExistPredSet.java index c6ef5c3e..9f2fc31b 100644 --- a/Robust/src/Analysis/Disjoint/ExistPredSet.java +++ b/Robust/src/Analysis/Disjoint/ExistPredSet.java @@ -5,6 +5,24 @@ import IR.Flat.*; import java.util.*; import java.io.*; +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// + // a set of existence predicates that are // OR'ed terms, if any predicate is true // then the set evaluates to true @@ -13,29 +31,22 @@ public class ExistPredSet extends Canonical { protected Set preds; - public ExistPredSet() { - preds = new HashSet(); - } - - public ExistPredSet( ExistPred ep ) { - preds = new HashSet(); - preds.add( ep ); + + public static ExistPredSet factory() { + ExistPredSet out = new ExistPredSet(); + out = (ExistPredSet) Canonical.makeCanonical( out ); + return out; } - - public ExistPredSet makeCanonical() { - return (ExistPredSet) ExistPredSet.makeCanonical( this ); - } - - - public void add( ExistPred pred ) { - preds.add( pred ); + public static ExistPredSet factory( ExistPred pred ) { + ExistPredSet out = new ExistPredSet(); + out.preds.add( pred ); + out = (ExistPredSet) Canonical.makeCanonical( out ); + return out; } - - public ExistPredSet join( ExistPredSet eps ) { - this.preds.addAll( eps.preds ); - return this; + private ExistPredSet() { + preds = new HashSet(); } @@ -50,12 +61,27 @@ public class ExistPredSet extends Canonical { } - public boolean equals( Object o ) { - return true; + if( o == null ) { + return false; + } + + if( !(o instanceof ExistPredSet) ) { + return false; + } + + ExistPredSet eps = (ExistPredSet) o; + assert this.isCanonical(); + assert eps.isCanonical(); + return this == eps; } + public int hashCodeSpecific() { + return preds.hashCode(); + } + + public String toString() { String s = "P["; Iterator predItr = preds.iterator(); @@ -63,7 +89,7 @@ public class ExistPredSet extends Canonical { ExistPred pred = predItr.next(); s += pred.toString(); if( predItr.hasNext() ) { - s += " && "; + s += " || "; } } s += "]"; diff --git a/Robust/src/Analysis/Disjoint/ExistPredTrue.java b/Robust/src/Analysis/Disjoint/ExistPredTrue.java deleted file mode 100644 index 69812847..00000000 --- a/Robust/src/Analysis/Disjoint/ExistPredTrue.java +++ /dev/null @@ -1,23 +0,0 @@ -package Analysis.Disjoint; - -import IR.*; -import IR.Flat.*; -import java.util.*; -import java.io.*; - -// these existence predicates on elements of -// a callee graph allow a caller to prune the -// pieces of the graph that don't apply when -// predicates are not satisfied in the -// caller's context - -public class ExistPredTrue extends ExistPred { - - public boolean isSatisfiedBy( ReachGraph rg ) { - return true; - } - - public String toString() { - return "t"; - } -} diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java index 3aba2390..0b190fc6 100644 --- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java +++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java @@ -67,7 +67,7 @@ public class HeapRegionNode extends RefSrcNode { this.description = description; referencers = new HashSet(); - alphaNew = new ReachSet().makeCanonical(); + alphaNew = ReachSet.factory(); } public HeapRegionNode copy() { @@ -226,7 +226,7 @@ public class HeapRegionNode extends RefSrcNode { public void applyAlphaNew() { assert alphaNew != null; alpha = alphaNew; - alphaNew = new ReachSet().makeCanonical(); + alphaNew = ReachSet.factory(); } @@ -243,7 +243,7 @@ public class HeapRegionNode extends RefSrcNode { String s; if( id < 0 ) { - s = "minus" + new Integer(-id).toString(); + s = "minus" + new Integer( -id ).toString(); } else { s = id.toString(); } diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 53a7886f..aaaf3156 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -16,14 +16,14 @@ public class ReachGraph { protected static final TempDescriptor tdReturn = new TempDescriptor( "_Return___" ); // some frequently used reachability constants - protected static final ReachState rstateEmpty = new ReachState().makeCanonical(); - protected static final ReachSet rsetEmpty = new ReachSet().makeCanonical(); - protected static final ReachSet rsetWithEmptyState = new ReachSet( rstateEmpty ).makeCanonical(); + protected static final ReachState rstateEmpty = ReachState.factory(); + protected static final ReachSet rsetEmpty = ReachSet.factory(); + protected static final ReachSet rsetWithEmptyState = ReachSet.factory( rstateEmpty ); // predicate constants - protected static final ExistPredTrue predTrue = new ExistPredTrue(); - protected static final ExistPredSet predsEmpty = new ExistPredSet().makeCanonical(); - protected static final ExistPredSet predsTrue = new ExistPredSet( predTrue ).makeCanonical(); + protected static final ExistPred predTrue = ExistPred.factory(); // if no args, true + protected static final ExistPredSet predsEmpty = ExistPredSet.factory(); + protected static final ExistPredSet predsTrue = ExistPredSet.factory( predTrue ); // from DisjointAnalysis for convenience @@ -102,12 +102,15 @@ public class ReachGraph { if( inherent == null ) { if( markForAnalysis ) { - inherent = new ReachSet( - new ReachTuple( id, - !isSingleObject, - ReachTuple.ARITY_ONE - ).makeCanonical() - ).makeCanonical(); + inherent = + ReachSet.factory( + ReachState.factory( + ReachTuple.factory( id, + !isSingleObject, + ReachTuple.ARITY_ONE + ) + ) + ); } else { inherent = rsetWithEmptyState; } @@ -119,7 +122,7 @@ public class ReachGraph { if( preds == null ) { // TODO: do this right? For out-of-context nodes? - preds = new ExistPredSet().makeCanonical(); + preds = ExistPredSet.factory(); } HeapRegionNode hrn = new HeapRegionNode( id, @@ -361,7 +364,7 @@ public class ReachGraph { hrnHrn, tdNewEdge, null, - betaY.intersection( betaHrn ), + Canonical.intersection( betaY, betaHrn ), predsTrue ); @@ -428,7 +431,9 @@ public class ReachGraph { RefEdge edgeX = itrXhrn.next(); HeapRegionNode hrnX = edgeX.getDst(); ReachSet betaX = edgeX.getBeta(); - ReachSet R = hrnX.getAlpha().intersection( edgeX.getBeta() ); + ReachSet R = Canonical.intersection( hrnX.getAlpha(), + edgeX.getBeta() + ); Iterator itrYhrn = lnY.iteratorToReferencees(); while( itrYhrn.hasNext() ) { @@ -444,11 +449,11 @@ public class ReachGraph { // propagate tokens over nodes starting from hrnSrc, and it will // take care of propagating back up edges from any touched nodes - ChangeSet Cy = O.unionUpArityToChangeSet( R ); + ChangeSet Cy = Canonical.unionUpArityToChangeSet( O, R ); propagateTokensOverNodes( hrnY, Cy, nodesWithNewAlpha, edgesWithNewBeta ); // then propagate back just up the edges from hrn - ChangeSet Cx = R.unionUpArityToChangeSet(O); + ChangeSet Cx = Canonical.unionUpArityToChangeSet( R, O ); HashSet todoEdges = new HashSet(); Hashtable edgePlannedChanges = @@ -508,7 +513,9 @@ public class ReachGraph { hrnY, tdNewEdge, f.getSymbol(), - edgeY.getBeta().pruneBy( hrnX.getAlpha() ), + Canonical.pruneBy( edgeY.getBeta(), + hrnX.getAlpha() + ), predsTrue ); @@ -520,10 +527,14 @@ public class ReachGraph { if( edgeExisting != null ) { edgeExisting.setBeta( - edgeExisting.getBeta().union( edgeNew.getBeta() ) + Canonical.union( edgeExisting.getBeta(), + edgeNew.getBeta() + ) ); edgeExisting.setPreds( - edgeExisting.getPreds().join( edgeNew.getPreds() ) + Canonical.join( edgeExisting.getPreds(), + edgeNew.getPreds() + ) ); } else { @@ -678,7 +689,7 @@ public class ReachGraph { Iterator itrEdges = ln.iteratorToReferencees(); while( itrEdges.hasNext() ) { - ageTokens(as, itrEdges.next() ); + ageTuplesFrom( as, itrEdges.next() ); } } @@ -687,11 +698,11 @@ public class ReachGraph { Map.Entry me = (Map.Entry) itrAllHRNodes.next(); HeapRegionNode hrnToAge = (HeapRegionNode) me.getValue(); - ageTokens( as, hrnToAge ); + ageTuplesFrom( as, hrnToAge ); Iterator itrEdges = hrnToAge.iteratorToReferencees(); while( itrEdges.hasNext() ) { - ageTokens( as, itrEdges.next() ); + ageTuplesFrom( as, itrEdges.next() ); } } @@ -775,59 +786,6 @@ public class ReachGraph { } - protected HeapRegionNode getShadowSummaryNode( AllocSite as ) { - - Integer idShadowSummary = as.getSummaryShadow(); - HeapRegionNode hrnShadowSummary = id2hrn.get( idShadowSummary ); - - if( hrnShadowSummary == null ) { - - boolean hasFlags = false; - if( as.getType().isClass() ) { - hasFlags = as.getType().getClassDesc().hasFlags(); - } - - if( as.getFlag() ){ - hasFlags = as.getFlag(); - } - - String strDesc = as+"\\n"+as.getType()+"\\nshadowSum"; - hrnShadowSummary = - createNewHeapRegionNode( idShadowSummary, // id or null to generate a new one - false, // single object? - true, // summary? - hasFlags, // flagged? - false, // out-of-context? - as.getType(), // type - as, // allocation site - null, // inherent reach - null, // current reach - predsEmpty, // predicates - strDesc // description - ); - - for( int i = 0; i < as.getAllocationDepth(); ++i ) { - Integer idShadowIth = as.getIthOldestShadow( i ); - assert !id2hrn.containsKey( idShadowIth ); - strDesc = as+"\\n"+as.getType()+"\\n"+i+" shadow"; - createNewHeapRegionNode( idShadowIth, // id or null to generate a new one - true, // single object? - false, // summary? - hasFlags, // flagged? - false, // out-of-context? - as.getType(), // type - as, // allocation site - null, // inherent reach - null, // current reach - predsEmpty, // predicates - strDesc // description - ); - } - } - - return hrnShadowSummary; - } - protected void mergeIntoSummary( HeapRegionNode hrn, HeapRegionNode hrnSummary ) { @@ -852,8 +810,16 @@ public class ReachGraph { } else { // otherwise an edge from the referencer to hrnSummary exists already // and the edge referencer->hrn should be merged with it - edgeMerged.setBeta( edgeMerged.getBeta().union( edgeSummary.getBeta() ) ); - edgeMerged.setPreds( edgeMerged.getPreds().join( edgeSummary.getPreds() ) ); + edgeMerged.setBeta( + Canonical.union( edgeMerged.getBeta(), + edgeSummary.getBeta() + ) + ); + edgeMerged.setPreds( + Canonical.join( edgeMerged.getPreds(), + edgeSummary.getPreds() + ) + ); } addRefEdge( hrnSummary, hrnReferencee, edgeMerged ); @@ -878,15 +844,27 @@ public class ReachGraph { } else { // otherwise an edge from the referencer to alpha_S exists already // and the edge referencer->alpha_K should be merged with it - edgeMerged.setBeta( edgeMerged.getBeta().union( edgeSummary.getBeta() ) ); - edgeMerged.setPreds( edgeMerged.getPreds().join( edgeSummary.getPreds() ) ); + edgeMerged.setBeta( + Canonical.union( edgeMerged.getBeta(), + edgeSummary.getBeta() + ) + ); + edgeMerged.setPreds( + Canonical.join( edgeMerged.getPreds(), + edgeSummary.getPreds() + ) + ); } addRefEdge( onReferencer, hrnSummary, edgeMerged ); } // then merge hrn reachability into hrnSummary - hrnSummary.setAlpha( hrnSummary.getAlpha().union( hrn.getAlpha() ) ); + hrnSummary.setAlpha( + Canonical.union( hrnSummary.getAlpha(), + hrn.getAlpha() + ) + ); } @@ -924,32 +902,39 @@ public class ReachGraph { } - protected void ageTokens( AllocSite as, RefEdge edge ) { - edge.setBeta( edge.getBeta().ageTokens( as ) ); + protected void ageTuplesFrom( AllocSite as, RefEdge edge ) { + edge.setBeta( + Canonical.ageTuplesFrom( edge.getBeta(), + as + ) + ); } - protected void ageTokens( AllocSite as, HeapRegionNode hrn ) { - hrn.setAlpha( hrn.getAlpha().ageTokens( as ) ); + protected void ageTuplesFrom( AllocSite as, HeapRegionNode hrn ) { + hrn.setAlpha( + Canonical.ageTuplesFrom( hrn.getAlpha(), + as + ) + ); } - protected void propagateTokensOverNodes( - HeapRegionNode nPrime, - ChangeSet c0, - HashSet nodesWithNewAlpha, - HashSet edgesWithNewBeta ) { + protected void propagateTokensOverNodes( HeapRegionNode nPrime, + ChangeSet c0, + HashSet nodesWithNewAlpha, + HashSet edgesWithNewBeta ) { HashSet todoNodes = new HashSet(); - todoNodes.add(nPrime); - + todoNodes.add( nPrime ); + HashSet todoEdges = new HashSet(); - + Hashtable nodePlannedChanges = new Hashtable(); - nodePlannedChanges.put(nPrime, c0); + nodePlannedChanges.put( nPrime, c0 ); Hashtable edgePlannedChanges = new Hashtable(); @@ -957,51 +942,61 @@ public class ReachGraph { // first propagate change sets everywhere they can go while( !todoNodes.isEmpty() ) { HeapRegionNode n = todoNodes.iterator().next(); - ChangeSet C = nodePlannedChanges.get(n); + ChangeSet C = nodePlannedChanges.get( n ); Iterator referItr = n.iteratorToReferencers(); while( referItr.hasNext() ) { RefEdge edge = referItr.next(); - todoEdges.add(edge); + todoEdges.add( edge ); - if( !edgePlannedChanges.containsKey(edge) ) { - edgePlannedChanges.put(edge, new ChangeSet().makeCanonical() ); + if( !edgePlannedChanges.containsKey( edge ) ) { + edgePlannedChanges.put( edge, + ChangeSet.factory() + ); } - edgePlannedChanges.put(edge, edgePlannedChanges.get(edge).union(C) ); + edgePlannedChanges.put( edge, + Canonical.union( edgePlannedChanges.get( edge ), + C + ) + ); } Iterator refeeItr = n.iteratorToReferencees(); while( refeeItr.hasNext() ) { - RefEdge edgeF = refeeItr.next(); + RefEdge edgeF = refeeItr.next(); HeapRegionNode m = edgeF.getDst(); - ChangeSet changesToPass = new ChangeSet().makeCanonical(); + ChangeSet changesToPass = ChangeSet.factory(); Iterator itrCprime = C.iterator(); while( itrCprime.hasNext() ) { ChangeTuple c = itrCprime.next(); if( edgeF.getBeta().contains( c.getSetToMatch() ) ) { - changesToPass = changesToPass.union(c); + changesToPass = Canonical.union( changesToPass, c ); } } if( !changesToPass.isEmpty() ) { - if( !nodePlannedChanges.containsKey(m) ) { - nodePlannedChanges.put(m, new ChangeSet().makeCanonical() ); + if( !nodePlannedChanges.containsKey( m ) ) { + nodePlannedChanges.put( m, ChangeSet.factory() ); } - ChangeSet currentChanges = nodePlannedChanges.get(m); + ChangeSet currentChanges = nodePlannedChanges.get( m ); - if( !changesToPass.isSubset(currentChanges) ) { + if( !changesToPass.isSubset( currentChanges ) ) { - nodePlannedChanges.put(m, currentChanges.union(changesToPass) ); - todoNodes.add(m); + nodePlannedChanges.put( m, + Canonical.union( currentChanges, + changesToPass + ) + ); + todoNodes.add( m ); } } } - todoNodes.remove(n); + todoNodes.remove( n ); } // then apply all of the changes for each node at once @@ -1009,68 +1004,83 @@ public class ReachGraph { while( itrMap.hasNext() ) { Map.Entry me = (Map.Entry) itrMap.next(); HeapRegionNode n = (HeapRegionNode) me.getKey(); - ChangeSet C = (ChangeSet) me.getValue(); + ChangeSet C = (ChangeSet) me.getValue(); // this propagation step is with respect to one change, // so we capture the full change from the old alpha: - ReachSet localDelta = n.getAlpha().applyChangeSet( C, true ); - + ReachSet localDelta = Canonical.applyChangeSet( n.getAlpha(), + C, + true + ); // 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( n.getAlphaNew().union( localDelta ) ); + n.setAlphaNew( Canonical.union( n.getAlphaNew(), + localDelta + ) + ); nodesWithNewAlpha.add( n ); } - propagateTokensOverEdges(todoEdges, edgePlannedChanges, edgesWithNewBeta); + propagateTokensOverEdges( todoEdges, + edgePlannedChanges, + edgesWithNewBeta + ); } - protected void propagateTokensOverEdges( - HashSet todoEdges, - Hashtable edgePlannedChanges, - HashSet edgesWithNewBeta ) { - + protected void propagateTokensOverEdges( HashSet todoEdges, + Hashtable edgePlannedChanges, + HashSet edgesWithNewBeta ) { + // first propagate all change tuples everywhere they can go while( !todoEdges.isEmpty() ) { RefEdge edgeE = todoEdges.iterator().next(); - todoEdges.remove(edgeE); + todoEdges.remove( edgeE ); - if( !edgePlannedChanges.containsKey(edgeE) ) { - edgePlannedChanges.put(edgeE, new ChangeSet().makeCanonical() ); + if( !edgePlannedChanges.containsKey( edgeE ) ) { + edgePlannedChanges.put( edgeE, + ChangeSet.factory() + ); } - ChangeSet C = edgePlannedChanges.get(edgeE); + ChangeSet C = edgePlannedChanges.get( edgeE ); - ChangeSet changesToPass = new ChangeSet().makeCanonical(); + ChangeSet changesToPass = ChangeSet.factory(); Iterator itrC = C.iterator(); while( itrC.hasNext() ) { ChangeTuple c = itrC.next(); if( edgeE.getBeta().contains( c.getSetToMatch() ) ) { - changesToPass = changesToPass.union(c); + changesToPass = Canonical.union( changesToPass, c ); } } - RefSrcNode onSrc = edgeE.getSrc(); + RefSrcNode rsn = edgeE.getSrc(); - if( !changesToPass.isEmpty() && onSrc instanceof HeapRegionNode ) { - HeapRegionNode n = (HeapRegionNode) onSrc; + if( !changesToPass.isEmpty() && rsn instanceof HeapRegionNode ) { + HeapRegionNode n = (HeapRegionNode) rsn; Iterator referItr = n.iteratorToReferencers(); while( referItr.hasNext() ) { RefEdge edgeF = referItr.next(); - if( !edgePlannedChanges.containsKey(edgeF) ) { - edgePlannedChanges.put(edgeF, new ChangeSet().makeCanonical() ); + if( !edgePlannedChanges.containsKey( edgeF ) ) { + edgePlannedChanges.put( edgeF, + ChangeSet.factory() + ); } - ChangeSet currentChanges = edgePlannedChanges.get(edgeF); + ChangeSet currentChanges = edgePlannedChanges.get( edgeF ); - if( !changesToPass.isSubset(currentChanges) ) { - todoEdges.add(edgeF); - edgePlannedChanges.put(edgeF, currentChanges.union(changesToPass) ); + if( !changesToPass.isSubset( currentChanges ) ) { + todoEdges.add( edgeF ); + edgePlannedChanges.put( edgeF, + Canonical.union( currentChanges, + changesToPass + ) + ); } } } @@ -1079,18 +1089,25 @@ public class ReachGraph { // then apply all of the changes for each edge at once Iterator itrMap = edgePlannedChanges.entrySet().iterator(); while( itrMap.hasNext() ) { - Map.Entry me = (Map.Entry) itrMap.next(); - RefEdge e = (RefEdge) me.getKey(); + Map.Entry me = (Map.Entry) itrMap.next(); + RefEdge e = (RefEdge) me.getKey(); ChangeSet C = (ChangeSet) me.getValue(); // this propagation step is with respect to one change, // so we capture the full change from the old beta: - ReachSet localDelta = e.getBeta().applyChangeSet( C, true ); + ReachSet localDelta = + Canonical.applyChangeSet( e.getBeta(), + C, + true + ); // 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( e.getBetaNew().union( localDelta ) ); + e.setBetaNew( Canonical.union( e.getBetaNew(), + localDelta + ) + ); edgesWithNewBeta.add( e ); } @@ -1173,15 +1190,16 @@ public class ReachGraph { // not have been created already assert rsnCaller instanceof HeapRegionNode; - HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller; hrnSrcID = hrnSrcCaller.getID(); + HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller; + hrnSrcID = hrnSrcCaller.getID(); if( !callerNodesCopiedToCallee.contains( rsnCaller ) ) { - ExistPredNode pred = - new ExistPredNode( hrnSrcID, null ); + ExistPred pred = + ExistPred.factory( hrnSrcID, null ); - ExistPredSet preds = new ExistPredSet(); - preds.add( pred ); + ExistPredSet preds = + ExistPredSet.factory( pred ); rsnCallee = rg.createNewHeapRegionNode( hrnSrcCaller.getID(), @@ -1191,8 +1209,8 @@ public class ReachGraph { false, // out-of-context? hrnSrcCaller.getType(), hrnSrcCaller.getAllocSite(), - toShadowTokens( this, hrnSrcCaller.getInherent() ), - toShadowTokens( this, hrnSrcCaller.getAlpha() ), + /*toShadowTokens( this,*/ hrnSrcCaller.getInherent() /*)*/, + /*toShadowTokens( this,*/ hrnSrcCaller.getAlpha() /*)*/, preds, hrnSrcCaller.getDescription() ); @@ -1216,11 +1234,11 @@ public class ReachGraph { if( !callerNodesCopiedToCallee.contains( hrnCaller ) ) { - ExistPredNode pred = - new ExistPredNode( hrnDstID, null ); + ExistPred pred = + ExistPred.factory( hrnDstID, null ); - ExistPredSet preds = new ExistPredSet(); - preds.add( pred ); + ExistPredSet preds = + ExistPredSet.factory( pred ); hrnCallee = rg.createNewHeapRegionNode( hrnCaller.getID(), @@ -1230,8 +1248,8 @@ public class ReachGraph { false, // out-of-context? hrnCaller.getType(), hrnCaller.getAllocSite(), - toShadowTokens( this, hrnCaller.getInherent() ), - toShadowTokens( this, hrnCaller.getAlpha() ), + /*toShadowTokens( this,*/ hrnCaller.getInherent() /*)*/, + /*toShadowTokens( this,*/ hrnCaller.getAlpha() /*)*/, preds, hrnCaller.getDescription() ); @@ -1243,16 +1261,16 @@ public class ReachGraph { // FOURTH - copy edge over if needed if( !callerEdgesCopiedToCallee.contains( reCaller ) ) { - ExistPredEdge pred = - new ExistPredEdge( tdSrc, + ExistPred pred = + ExistPred.factory( tdSrc, hrnSrcID, hrnDstID, reCaller.getType(), reCaller.getField(), null ); - ExistPredSet preds = new ExistPredSet(); - preds.add( pred ); + ExistPredSet preds = + ExistPredSet.factory( pred ); rg.addRefEdge( rsnCallee, hrnCallee, @@ -1260,7 +1278,7 @@ public class ReachGraph { hrnCallee, reCaller.getType(), reCaller.getField(), - toShadowTokens( this, reCaller.getBeta() ), + /*toShadowTokens( this,*/ reCaller.getBeta() /*)*/, preds ) ); @@ -1302,7 +1320,7 @@ public class ReachGraph { } HeapRegionNode hrnCallerAndOutContext = - (HeapRegionNode)edgeMightCross.getSrc(); + (HeapRegionNode) edgeMightCross.getSrc(); // we found a reference that crosses from out-of-context // to in-context, so build a special out-of-context node @@ -1315,8 +1333,8 @@ public class ReachGraph { true, // out-of-context? hrnCallerAndOutContext.getType(), null, // alloc site, shouldn't be used - toShadowTokens( this, hrnCallerAndOutContext.getAlpha() ), // inherent - toShadowTokens( this, hrnCallerAndOutContext.getAlpha() ), // alpha + /*toShadowTokens( this,*/ hrnCallerAndOutContext.getAlpha() /*)*/, // inherent + /*toShadowTokens( this,*/ hrnCallerAndOutContext.getAlpha() /*)*/, // alpha predsEmpty, "out-of-context" ); @@ -1330,7 +1348,7 @@ public class ReachGraph { hrnCalleeAndInContext, edgeMightCross.getType(), edgeMightCross.getField(), - toShadowTokens( this, edgeMightCross.getBeta() ), + /*toShadowTokens( this,*/ edgeMightCross.getBeta() /*)*/, predsEmpty ) ); @@ -1433,33 +1451,6 @@ public class ReachGraph { } - protected void unshadowTokens( AllocSite as, - RefEdge edge - ) { - edge.setBeta( edge.getBeta().unshadowTokens( as ) ); - } - - protected void unshadowTokens( AllocSite as, - HeapRegionNode hrn - ) { - hrn.setAlpha( hrn.getAlpha().unshadowTokens( as ) ); - } - - - private ReachSet toShadowTokens( ReachGraph rg, - ReachSet rsIn - ) { - ReachSet rsOut = new ReachSet( rsIn ).makeCanonical(); - - Iterator allocItr = rg.allocSites.iterator(); - while( allocItr.hasNext() ) { - AllocSite as = allocItr.next(); - rsOut = rsOut.toShadowTokens( as ); - } - - return rsOut.makeCanonical(); - } - //////////////////////////////////////////////////// // @@ -1588,12 +1579,11 @@ public class ReachGraph { new Hashtable< Integer, Hashtable >(); // visit every heap region to initialize alphaNew and calculate boldB - Set hrns = id2hrn.entrySet(); - Iterator itrHrns = hrns.iterator(); + Iterator itrHrns = id2hrn.entrySet().iterator(); while( itrHrns.hasNext() ) { - Map.Entry me = (Map.Entry)itrHrns.next(); - Integer token = (Integer) me.getKey(); - HeapRegionNode hrn = (HeapRegionNode) me.getValue(); + Map.Entry me = (Map.Entry) itrHrns.next(); + Integer hrnID = (Integer) me.getKey(); + HeapRegionNode hrn = (HeapRegionNode) me.getValue(); // assert that this node and incoming edges have clean alphaNew // and betaNew sets, respectively @@ -1635,111 +1625,132 @@ public class ReachGraph { RefEdge edgePrime = itrPrime.next(); ReachSet prevResult = boldB_f.get( edgePrime ); - ReachSet intersection = boldB_f.get( edge ).intersection( edgePrime.getBeta() ); + ReachSet intersection = Canonical.intersection( boldB_f.get( edge ), + edgePrime.getBeta() + ); if( prevResult == null || - prevResult.union( intersection ).size() > prevResult.size() ) { + Canonical.union( prevResult, + intersection ).size() > prevResult.size() ) { if( prevResult == null ) { - boldB_f.put( edgePrime, edgePrime.getBeta().union( intersection ) ); + boldB_f.put( edgePrime, + Canonical.union( edgePrime.getBeta(), + intersection + ) + ); } else { - boldB_f.put( edgePrime, prevResult .union( intersection ) ); + boldB_f.put( edgePrime, + Canonical.union( prevResult, + intersection + ) + ); } workSetEdges.add( edgePrime ); } } } - boldB.put( token, boldB_f ); + boldB.put( hrnID, boldB_f ); } } - // use boldB to prune tokens from alpha states that are impossible + // use boldB to prune hrnIDs from alpha states that are impossible // and propagate the differences backwards across edges HashSet edgesForPropagation = new HashSet(); Hashtable edgePlannedChanges = new Hashtable(); - hrns = id2hrn.entrySet(); - itrHrns = hrns.iterator(); - while( itrHrns.hasNext() ) { - Map.Entry me = (Map.Entry)itrHrns.next(); - Integer token = (Integer) me.getKey(); - HeapRegionNode hrn = (HeapRegionNode) me.getValue(); - // never remove the identity token from a flagged region - // because it is trivially satisfied - ReachTuple ttException = new ReachTuple( token, - !hrn.isSingleObject(), - ReachTuple.ARITY_ONE ).makeCanonical(); + itrHrns = id2hrn.entrySet().iterator(); + while( itrHrns.hasNext() ) { + Map.Entry me = (Map.Entry) itrHrns.next(); + Integer hrnID = (Integer) me.getKey(); + HeapRegionNode hrn = (HeapRegionNode) me.getValue(); + + // create the inherent hrnID from a flagged region + // as an exception to removal below + ReachTuple rtException = + ReachTuple.factory( hrnID, + !hrn.isSingleObject(), + ReachTuple.ARITY_ONE + ); - ChangeSet cts = new ChangeSet().makeCanonical(); + ChangeSet cts = ChangeSet.factory(); - // mark tokens for removal + // mark hrnIDs for removal Iterator stateItr = hrn.getAlpha().iterator(); while( stateItr.hasNext() ) { - ReachState ttsOld = stateItr.next(); + ReachState stateOld = stateItr.next(); - ReachState markedTokens = new ReachState().makeCanonical(); + ReachState markedHrnIDs = ReachState.factory(); - Iterator ttItr = ttsOld.iterator(); - while( ttItr.hasNext() ) { - ReachTuple ttOld = ttItr.next(); + Iterator rtItr = stateOld.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rtOld = rtItr.next(); - // never remove the identity token from a flagged region + // never remove the inherent hrnID from a flagged region // because it is trivially satisfied if( hrn.isFlagged() ) { - if( ttOld == ttException ) { + if( rtOld == rtException ) { continue; } } - // does boldB_ttOld allow this token? + // does boldB_ttOld allow this hrnID? boolean foundState = false; Iterator incidentEdgeItr = hrn.iteratorToReferencers(); while( incidentEdgeItr.hasNext() ) { RefEdge incidentEdge = incidentEdgeItr.next(); // if it isn't allowed, mark for removal - Integer idOld = ttOld.getToken(); + Integer idOld = rtOld.getHrnID(); assert id2hrn.containsKey( idOld ); Hashtable B = boldB.get( idOld ); - ReachSet boldB_ttOld_incident = B.get( incidentEdge );// B is NULL! + ReachSet boldB_ttOld_incident = B.get( incidentEdge ); if( boldB_ttOld_incident != null && - boldB_ttOld_incident.contains( ttsOld ) ) { + boldB_ttOld_incident.contains( stateOld ) ) { foundState = true; } } if( !foundState ) { - markedTokens = markedTokens.add( ttOld ); + markedHrnIDs = Canonical.add( markedHrnIDs, rtOld ); } } // if there is nothing marked, just move on - if( markedTokens.isEmpty() ) { - hrn.setAlphaNew( hrn.getAlphaNew().union( ttsOld ) ); + if( markedHrnIDs.isEmpty() ) { + hrn.setAlphaNew( Canonical.union( hrn.getAlphaNew(), + stateOld + ) + ); continue; } - // remove all marked tokens and establish a change set that should + // remove all marked hrnIDs and establish a change set that should // propagate backwards over edges from this node - ReachState ttsPruned = new ReachState().makeCanonical(); - ttItr = ttsOld.iterator(); - while( ttItr.hasNext() ) { - ReachTuple ttOld = ttItr.next(); + ReachState statePruned = ReachState.factory(); + rtItr = stateOld.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rtOld = rtItr.next(); - if( !markedTokens.containsTuple( ttOld ) ) { - ttsPruned = ttsPruned.union( ttOld ); + if( !markedHrnIDs.containsTuple( rtOld ) ) { + statePruned = Canonical.union( statePruned, rtOld ); } } - assert !ttsOld.equals( ttsPruned ); + assert !stateOld.equals( statePruned ); - hrn.setAlphaNew( hrn.getAlphaNew().union( ttsPruned ) ); - ChangeTuple ct = new ChangeTuple( ttsOld, ttsPruned ).makeCanonical(); - cts = cts.union( ct ); + hrn.setAlphaNew( Canonical.union( hrn.getAlphaNew(), + statePruned + ) + ); + ChangeTuple ct = ChangeTuple.factory( stateOld, + statePruned + ); + cts = Canonical.union( cts, ct ); } // throw change tuple set on all incident edges @@ -1754,9 +1765,11 @@ public class ReachGraph { edgePlannedChanges.put( incidentEdge, cts ); } else { edgePlannedChanges.put( - incidentEdge, - edgePlannedChanges.get( incidentEdge ).union( cts ) - ); + incidentEdge, + Canonical.union( edgePlannedChanges.get( incidentEdge ), + cts + ) + ); } } } @@ -1791,8 +1804,8 @@ public class ReachGraph { // 2nd phase Iterator edgeItr = res.iterator(); while( edgeItr.hasNext() ) { - RefEdge edge = edgeItr.next(); - HeapRegionNode hrn = edge.getDst(); + RefEdge edge = edgeItr.next(); + HeapRegionNode hrn = edge.getDst(); // commit results of last phase if( edgesUpdated.contains( edge ) ) { @@ -1800,7 +1813,10 @@ public class ReachGraph { } // compute intial condition of 2nd phase - edge.setBetaNew( edge.getBeta().intersection( hrn.getAlpha() ) ); + edge.setBetaNew( Canonical.intersection( edge.getBeta(), + hrn.getAlpha() + ) + ); } // every edge in the graph is the initial workset @@ -1809,11 +1825,11 @@ public class ReachGraph { RefEdge edgePrime = edgeWorkSet.iterator().next(); edgeWorkSet.remove( edgePrime ); - RefSrcNode on = edgePrime.getSrc(); - if( !(on instanceof HeapRegionNode) ) { + RefSrcNode rsn = edgePrime.getSrc(); + if( !(rsn instanceof HeapRegionNode) ) { continue; } - HeapRegionNode hrn = (HeapRegionNode) on; + HeapRegionNode hrn = (HeapRegionNode) rsn; Iterator itrEdge = hrn.iteratorToReferencers(); while( itrEdge.hasNext() ) { @@ -1822,10 +1838,19 @@ public class ReachGraph { ReachSet prevResult = edge.getBetaNew(); assert prevResult != null; - ReachSet intersection = edge.getBeta().intersection( edgePrime.getBetaNew() ); + ReachSet intersection = + Canonical.intersection( edge.getBeta(), + edgePrime.getBetaNew() + ); - if( prevResult.union( intersection ).size() > prevResult.size() ) { - edge.setBetaNew( prevResult.union( intersection ) ); + if( Canonical.union( prevResult, + intersection + ).size() > prevResult.size() ) { + edge.setBetaNew( + Canonical.union( prevResult, + intersection + ) + ); edgeWorkSet.add( edge ); } } @@ -1897,7 +1922,10 @@ public class ReachGraph { // so make the new reachability set a union of the // nodes' reachability sets HeapRegionNode hrnB = id2hrn.get( idA ); - hrnB.setAlpha( hrnB.getAlpha().union( hrnA.getAlpha() ) ); + hrnB.setAlpha( Canonical.union( hrnB.getAlpha(), + hrnA.getAlpha() + ) + ); // if hrnB is already dirty or hrnA is dirty, // the hrnB should end up dirty: TODO @@ -1979,8 +2007,10 @@ public class ReachGraph { // just replace this beta set with the union assert edgeToMerge != null; edgeToMerge.setBeta( - edgeToMerge.getBeta().union( edgeA.getBeta() ) - ); + Canonical.union( edgeToMerge.getBeta(), + edgeA.getBeta() + ) + ); // TODO: what? /* if( !edgeA.isClean() ) { @@ -2042,9 +2072,10 @@ public class ReachGraph { // so merge their reachability sets else { // just replace this beta set with the union - edgeToMerge.setBeta( - edgeToMerge.getBeta().union( edgeA.getBeta() ) - ); + edgeToMerge.setBeta( Canonical.union( edgeToMerge.getBeta(), + edgeA.getBeta() + ) + ); // TODO: what? /* if( !edgeA.isClean() ) { diff --git a/Robust/src/Analysis/Disjoint/ReachOperation.java b/Robust/src/Analysis/Disjoint/ReachOperation.java deleted file mode 100644 index e2d46fb4..00000000 --- a/Robust/src/Analysis/Disjoint/ReachOperation.java +++ /dev/null @@ -1,23 +0,0 @@ -package Analysis.Disjoint; - -public class ReachOperation { - Canonical a; - Canonical b; - public Canonical c; - - public ReachOperation(Canonical a, Canonical b) { - assert a.canonicalvalue!=0; - assert b.canonicalvalue!=0; - this.a=a; - this.b=b; - } - - public int hashCode() { - return a.canonicalvalue^(b.canonicalvalue<<1); - } - public boolean equals(Object o) { - ReachOperation ro=(ReachOperation)o; - return ro.a.canonicalvalue==a.canonicalvalue&& - ro.b.canonicalvalue==b.canonicalvalue; - } -} \ No newline at end of file diff --git a/Robust/src/Analysis/Disjoint/ReachSet.java b/Robust/src/Analysis/Disjoint/ReachSet.java index e6275335..0c40a3f1 100644 --- a/Robust/src/Analysis/Disjoint/ReachSet.java +++ b/Robust/src/Analysis/Disjoint/ReachSet.java @@ -5,484 +5,167 @@ import IR.Flat.*; import java.util.*; import java.io.*; +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// + +// a reach set is a set of reach states public class ReachSet extends Canonical { - private HashSet possibleReachabilities; + protected HashSet reachStates; - public ReachSet() { - possibleReachabilities = new HashSet(); - } - - public ReachSet(ReachState tts) { - this(); - assert tts != null; - possibleReachabilities.add(tts); - } - public ReachSet(ReachTuple tt) { - // can't assert before calling this(), it will - // do the checking though - this( new ReachState(tt).makeCanonical() ); + public static ReachSet factory() { + ReachSet out = new ReachSet(); + out = (ReachSet) Canonical.makeCanonical( out ); + return out; } - public ReachSet(HashSet possibleReachabilities) { - assert possibleReachabilities != null; - this.possibleReachabilities = possibleReachabilities; + public static ReachSet factory( ReachState state ) { + assert state != null; + assert state.isCanonical(); + ReachSet out = new ReachSet(); + out.reachStates.add( state ); + out = (ReachSet) Canonical.makeCanonical( out ); + return out; } - public ReachSet(ReachSet rs) { - assert rs != null; - // okay to clone, ReachSet should be canonical - possibleReachabilities = (HashSet)rs.possibleReachabilities.clone(); + private ReachSet() { + reachStates = new HashSet(); } - public ReachSet makeCanonical() { - return (ReachSet) ReachSet.makeCanonical(this); - } - public Iterator iterator() { - return possibleReachabilities.iterator(); + return reachStates.iterator(); } - public int size() { - return possibleReachabilities.size(); + return reachStates.size(); } public boolean isEmpty() { - return possibleReachabilities.isEmpty(); + return reachStates.isEmpty(); } - public boolean contains(ReachState tts) { - assert tts != null; - return possibleReachabilities.contains(tts); + public boolean contains( ReachState state ) { + assert state != null; + return reachStates.contains( state ); } - public boolean containsWithZeroes(ReachState tts) { - assert tts != null; + /* + public boolean containsWithZeroes( ReachState state ) { + assert state != null; - if( possibleReachabilities.contains(tts) ) { + if( reachStates.contains( state ) ) { return true; } - Iterator itr = iterator(); + Iterator itr = iterator(); while( itr.hasNext() ) { - ReachState ttsThis = (ReachState) itr.next(); - if( ttsThis.containsWithZeroes(tts) ) { + ReachState stateThis = itr.next(); + if( stateThis.containsWithZeroes( state ) ) { return true; } } - + return false; } + */ - - public boolean containsSuperSet(ReachState tts) { - return containsSuperSet( tts, false ); + public boolean containsSuperSet( ReachState state ) { + return containsSuperSet( state, false ); } - public boolean containsStrictSuperSet(ReachState tts) { - return containsSuperSet( tts, true ); + public boolean containsStrictSuperSet( ReachState state ) { + return containsSuperSet( state, true ); } - public boolean containsSuperSet(ReachState tts, boolean strict) { - assert tts != null; + public boolean containsSuperSet( ReachState state, + boolean strict ) { + assert state != null; - if( !strict && possibleReachabilities.contains(tts) ) { + if( !strict && reachStates.contains( state ) ) { return true; } - Iterator itr = iterator(); + Iterator itr = iterator(); while( itr.hasNext() ) { - ReachState ttsThis = (ReachState) itr.next(); + ReachState stateThis = itr.next(); if( strict ) { - if( !tts.equals(ttsThis) && tts.isSubset(ttsThis) ) { + if( !state.equals( stateThis ) && + state.isSubset( stateThis ) ) { return true; } } else { - if( tts.isSubset(ttsThis) ) { + if( state.isSubset( stateThis ) ) { return true; } } } - + return false; } - public boolean containsTuple(ReachTuple tt) { - Iterator itr = iterator(); + public boolean containsTuple( ReachTuple rt ) { + Iterator itr = iterator(); while( itr.hasNext() ) { - ReachState tts = (ReachState) itr.next(); - if( tts.containsTuple(tt) ) { + ReachState state = itr.next(); + if( state.containsTuple( rt ) ) { return true; } } return false; } - public boolean containsTupleSetWithBoth(ReachTuple tt1, ReachTuple tt2) { - Iterator itr = iterator(); + public boolean containsStateWithBoth( ReachTuple rt1, + ReachTuple rt2 ) { + Iterator itr = iterator(); while( itr.hasNext() ) { - ReachState tts = (ReachState) itr.next(); - if( tts.containsTuple(tt1) && tts.containsTuple(tt2) ) { + ReachState state = itr.next(); + if( state.containsTuple( rt1 ) && + state.containsTuple( rt2 ) ) { return true; } } return false; } - public static ReachSet factory(ReachState tts) { - CanonicalWrapper cw=new CanonicalWrapper(tts); - if (lookuphash.containsKey(cw)) - return (ReachSet)lookuphash.get(cw).b; - ReachSet rs=new ReachSet(tts); - rs=rs.makeCanonical(); - cw.b=rs; - lookuphash.put(cw,cw); - return rs; - } - - public ReachSet union(ReachState ttsIn) { - ReachOperation ro=new ReachOperation(this, ttsIn); - if (unionhash.containsKey(ro)) { - return (ReachSet) unionhash.get(ro).c; - } else { - ReachSet rsOut = new ReachSet(this); - rsOut.possibleReachabilities.add(ttsIn); - ro.c=rsOut=rsOut.makeCanonical(); - unionhash.put(ro,ro); - return rsOut; - } - } - - - public ReachSet union(ReachSet rsIn) { - // assert rsIn != null; - - // assert can.containsKey(this); - // assert can.containsKey(rsIn); - - ReachOperation ro=new ReachOperation(this, rsIn); - if (unionhash.containsKey(ro)) - return (ReachSet) unionhash.get(ro).c; - else { - ReachSet rsOut = new ReachSet(this); - rsOut.possibleReachabilities.addAll(rsIn.possibleReachabilities); - ro.c=rsOut=rsOut.makeCanonical(); - unionhash.put(ro, ro); - return rsOut; - } - } - - public ReachSet intersection(ReachSet rsIn) { - // assert rsIn != null; - - // assert can.containsKey(this); - // assert can.containsKey(rsIn); - - ReachOperation ro=new ReachOperation(this, rsIn); - if (interhash.containsKey(ro)) - return (ReachSet) interhash.get(ro).c; - else { - ReachSet rsOut = new ReachSet(); - Iterator i = this.iterator(); - while( i.hasNext() ) { - ReachState tts = (ReachState) i.next(); - if( rsIn.possibleReachabilities.contains(tts) ) { - rsOut.possibleReachabilities.add(tts); - } - } - ro.c=rsOut=rsOut.makeCanonical(); - interhash.put(ro,ro); - return rsOut; - } - } - - - public ReachSet add(ReachState tts) { - assert tts != null; - return union(tts); - } - - public ReachSet remove(ReachState tts) { - assert tts != null; - ReachSet rsOut = new ReachSet(this); - assert rsOut.possibleReachabilities.remove(tts); - return rsOut.makeCanonical(); - } - - public ReachSet removeTokenAIfTokenB(ReachTuple ttA, - ReachTuple ttB) { - assert ttA != null; - assert ttB != null; - ReachSet rsOut = new ReachSet(); - - Iterator i = this.iterator(); - while( i.hasNext() ) { - ReachState tts = (ReachState) i.next(); - if( tts.containsTuple( ttB ) ) { - rsOut.possibleReachabilities.add( tts.remove(ttA) ); - } else { - rsOut.possibleReachabilities.add( tts ); - } - } - - return rsOut.makeCanonical(); - } - - - public ReachSet applyChangeSet(ChangeSet C, boolean keepSourceState) { - assert C != null; - - ReachSet rsOut = new ReachSet(); - - Iterator i = this.iterator(); - while( i.hasNext() ) { - ReachState tts = (ReachState) i.next(); - - boolean changeFound = false; - - Iterator itrC = C.iterator(); - while( itrC.hasNext() ) { - ChangeTuple c = itrC.next(); - - if( tts.equals( c.getSetToMatch() ) ) { - rsOut.possibleReachabilities.add( c.getSetToAdd() ); - changeFound = true; - } - } - - if( keepSourceState || !changeFound ) { - rsOut.possibleReachabilities.add( tts ); - } - } - - return rsOut.makeCanonical(); - } - - - public ChangeSet unionUpArityToChangeSet(ReachSet rsIn) { - assert rsIn != null; - - ChangeSet ctsOut = new ChangeSet(); - - Iterator itrO = this.iterator(); - while( itrO.hasNext() ) { - ReachState o = (ReachState) itrO.next(); - - Iterator itrR = rsIn.iterator(); - while( itrR.hasNext() ) { - ReachState r = (ReachState) itrR.next(); - - ReachState theUnion = new ReachState().makeCanonical(); - - Iterator itrRelement = r.iterator(); - while( itrRelement.hasNext() ) { - ReachTuple ttR = (ReachTuple) itrRelement.next(); - ReachTuple ttO = o.containsToken(ttR.getToken() ); - - if( ttO != null ) { - theUnion = theUnion.union((new ReachState(ttR.unionArity(ttO)).makeCanonical() ) ); - } else { - theUnion = theUnion.union((new ReachState(ttR)).makeCanonical() ); - } - } - - Iterator itrOelement = o.iterator(); - while( itrOelement.hasNext() ) { - ReachTuple ttO = (ReachTuple) itrOelement.next(); - ReachTuple ttR = theUnion.containsToken(ttO.getToken() ); - - if( ttR == null ) { - theUnion = theUnion.union(new ReachState(ttO).makeCanonical() ); - } - } - - if( !theUnion.isEmpty() ) { - ctsOut = ctsOut.union((new ChangeSet(new ChangeTuple(o, theUnion) )).makeCanonical() ); - } - } - } - - return ctsOut.makeCanonical(); - } - - public ReachSet ageTokens(AllocSite as) { - assert as != null; - - ReachSet rsOut = new ReachSet(); - - Iterator itrS = this.iterator(); - while( itrS.hasNext() ) { - ReachState tts = (ReachState) itrS.next(); - rsOut.possibleReachabilities.add(tts.ageTokens(as) ); - } - - return rsOut.makeCanonical(); - } - - - public ReachSet unshadowTokens(AllocSite as) { - assert as != null; - - ReachSet rsOut = new ReachSet(); - - Iterator itrS = this.iterator(); - while( itrS.hasNext() ) { - ReachState tts = (ReachState) itrS.next(); - rsOut.possibleReachabilities.add(tts.unshadowTokens(as) ); - } - - return rsOut.makeCanonical(); - } - - - public ReachSet toShadowTokens(AllocSite as) { - assert as != null; - - ReachSet rsOut = new ReachSet(); - - Iterator itrS = this.iterator(); - while( itrS.hasNext() ) { - ReachState tts = (ReachState) itrS.next(); - rsOut.possibleReachabilities.add(tts.toShadowTokens(as) ); - } - - return rsOut.makeCanonical(); - } - - - public ReachSet pruneBy(ReachSet rsIn) { - assert rsIn != null; - - ReachSet rsOut = new ReachSet(); - - Iterator itrB = this.iterator(); - while( itrB.hasNext() ) { - ReachState ttsB = (ReachState) itrB.next(); - - boolean subsetExists = false; - - Iterator itrA = rsIn.iterator(); - while( itrA.hasNext() && !subsetExists ) { - ReachState ttsA = (ReachState) itrA.next(); - - if( ttsA.isSubset(ttsB) ) { - subsetExists = true; - } - } - - if( subsetExists ) { - rsOut.possibleReachabilities.add(ttsB); - } - } - - return rsOut.makeCanonical(); - } - - - public ReachSet exhaustiveArityCombinations() { - ReachSet rsOut = (new ReachSet()).makeCanonical(); - - int numDimensions = this.possibleReachabilities.size(); - - if( numDimensions > 3 ) { - // for problems that are too big, punt and use less - // precise arity for reachability information - ReachState ttsImprecise = new ReachState().makeCanonical(); - - Iterator itrThis = this.iterator(); - while( itrThis.hasNext() ) { - ReachState ttsUnit = itrThis.next(); - ttsImprecise = ttsImprecise.unionUpArity(ttsUnit.makeArityZeroOrMore() ); - } - - //rsOut = this.union( ttsImprecise ); - rsOut = rsOut.union(ttsImprecise); - return rsOut; - } - - // add an extra digit to detect termination - int[] digits = new int[numDimensions+1]; - - int minArity = 0; - int maxArity = 2; - - // start with the minimum possible coordinate - for( int i = 0; i < numDimensions+1; ++i ) { - digits[i] = minArity; - } - - // and stop when the highest-ordered axis rolls above the minimum - while( digits[numDimensions] == minArity ) { - - // spit out a "coordinate" made from these digits - ReachState ttsCoordinate = new ReachState().makeCanonical(); - Iterator ttsItr = this.iterator(); - for( int i = 0; i < numDimensions; ++i ) { - assert ttsItr.hasNext(); - ReachState ttsUnit = ttsItr.next(); - for( int j = 0; j < digits[i]; ++j ) { - ttsCoordinate = ttsCoordinate.unionUpArity(ttsUnit); - } - } - rsOut = rsOut.add(ttsCoordinate.makeCanonical() ); - - // increment - for( int i = 0; i < numDimensions+1; ++i ) { - digits[i]++; - - if( digits[i] > maxArity ) { - // this axis reached its max, so roll it back to min and increment next higher digit - digits[i] = minArity; - - } else { - // this axis did not reach its max so we just enumerated a new unique coordinate, stop - break; - } - } - } - - return rsOut.makeCanonical(); - } - - - public boolean equals(Object o) { + public boolean equals( Object o ) { if( o == null ) { return false; } - + if( !(o instanceof ReachSet) ) { return false; } ReachSet rs = (ReachSet) o; - return possibleReachabilities.equals(rs.possibleReachabilities); + assert this.isCanonical(); + assert rs.isCanonical(); + return this == rs; } - private boolean oldHashSet = false; - private int oldHash = 0; - public int hashCode() { - int currentHash = possibleReachabilities.hashCode(); - - if( oldHashSet == false ) { - oldHash = currentHash; - oldHashSet = true; - } else { - if( oldHash != currentHash ) { - System.out.println("IF YOU SEE THIS A CANONICAL ReachSet CHANGED"); - Integer x = null; - x.toString(); - } - } - - return currentHash; + public int hashCodeSpecific() { + return reachStates.hashCode(); } @@ -491,15 +174,15 @@ public class ReachSet extends Canonical { Iterator i = this.iterator(); while( i.hasNext() ) { - ReachState tts = i.next(); + ReachState state = i.next(); // skip this if there is a superset already if( hideSubsetReachability && - containsStrictSuperSet( tts ) ) { + containsStrictSuperSet( state ) ) { continue; } - s += tts; + s += state; if( i.hasNext() ) { s += "\\n"; } @@ -519,15 +202,15 @@ public class ReachSet extends Canonical { Iterator i = this.iterator(); while( i.hasNext() ) { - ReachState tts = i.next(); + ReachState state = i.next(); // skip this if there is a superset already if( hideSubsetReachability && - containsStrictSuperSet( tts ) ) { + containsStrictSuperSet( state ) ) { continue; } - s += tts; + s += state; if( i.hasNext() ) { s += "\n"; } diff --git a/Robust/src/Analysis/Disjoint/ReachState.java b/Robust/src/Analysis/Disjoint/ReachState.java index 587917f7..b1d96659 100644 --- a/Robust/src/Analysis/Disjoint/ReachState.java +++ b/Robust/src/Analysis/Disjoint/ReachState.java @@ -5,161 +5,89 @@ import IR.Flat.*; import java.util.*; import java.io.*; +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// + +// a reach state is a set of reach tuples +// such that any heap region ID in a tuple +// appears at most once in the state public class ReachState extends Canonical { - private HashSet tokenTuples; + protected HashSet reachTuples; - public ReachState() { - tokenTuples = new HashSet(); + public static ReachState factory() { + ReachState out = new ReachState(); + out = (ReachState) Canonical.makeCanonical( out ); + return out; } - public ReachState(ReachTuple tt) { - this(); - assert tt != null; - tokenTuples.add(tt); + public static ReachState factory( ReachTuple rt ) { + assert rt != null; + assert rt.isCanonical(); + ReachState out = new ReachState(); + out.reachTuples.add( rt ); + out = (ReachState) Canonical.makeCanonical( out ); + return out; } - public ReachState(ReachState tts) { - assert tts != null; - // okay to clone, ReachTuple and ReachState should be canonical - tokenTuples = (HashSet)tts.tokenTuples.clone(); + private ReachState() { + reachTuples = new HashSet(); } - public ReachState makeCanonical() { - return (ReachState) Canonical.makeCanonical(this); - } - public Iterator iterator() { - return tokenTuples.iterator(); + return reachTuples.iterator(); } public boolean isEmpty() { - return tokenTuples.isEmpty(); - } - - public boolean isSubset(ReachState ttsIn) { - assert ttsIn != null; - return ttsIn.tokenTuples.containsAll(this.tokenTuples); - } - - public boolean containsTuple(ReachTuple tt) { - assert tt != null; - return tokenTuples.contains(tt); - } - - public boolean containsBoth(ReachTuple tt1, ReachTuple tt2) { - return containsTuple(tt1) && containsTuple(tt2); - } - - public boolean containsWithZeroes(ReachState tts) { - assert tts != null; - - // first establish that every token tuple from tts is - // also in this set - Iterator ttItrIn = tts.iterator(); - while( ttItrIn.hasNext() ) { - ReachTuple ttIn = ttItrIn.next(); - ReachTuple ttThis = this.containsToken(ttIn.getToken() ); - - if( ttThis == null ) { - return false; - } - } - - // then establish that anything in this set that is - // not in tts is a zero-arity token tuple, which is okay - Iterator ttItrThis = this.iterator(); - while( ttItrThis.hasNext() ) { - ReachTuple ttThis = ttItrThis.next(); - ReachTuple ttIn = tts.containsToken(ttThis.getToken() ); - - if( ttIn == null && - ttThis.getArity() != ReachTuple.ARITY_ZEROORMORE ) { - return false; - } - } - - // if so this set contains tts with zeroes - return true; + return reachTuples.isEmpty(); } - public ReachState union(ReachTuple ttIn) { - assert ttIn != null; - ReachOperation ro=new ReachOperation(this, ttIn); - if (unionhash.containsKey(ro)) - return (ReachState) unionhash.get(ro).c; - else { - ReachState ttsOut = new ReachState(this); - ttsOut.tokenTuples.add(ttIn); - ro.c=ttsOut=ttsOut.makeCanonical(); - unionhash.put(ro,ro); - return ttsOut; - } + public boolean isSubset( ReachState rsIn ) { + assert rsIn != null; + return rsIn.reachTuples.containsAll( this.reachTuples ); } - public ReachState union(ReachState ttsIn) { - assert ttsIn != null; - ReachOperation ro=new ReachOperation(this, ttsIn); - if (unionhash.containsKey(ro)) { - return (ReachState) unionhash.get(ro).c; - } else { - ReachState ttsOut = new ReachState(this); - ttsOut.tokenTuples.addAll(ttsIn.tokenTuples); - ro.c=ttsOut=ttsOut.makeCanonical(); - unionhash.put(ro,ro); - return ttsOut; - } + public boolean containsTuple( ReachTuple rt ) { + assert rt != null; + return reachTuples.contains( rt ); } - - public ReachState unionUpArity(ReachState ttsIn) { - assert ttsIn != null; - ReachState ttsOut = new ReachState(); - - Iterator ttItr = this.iterator(); - while( ttItr.hasNext() ) { - ReachTuple ttThis = ttItr.next(); - ReachTuple ttIn = ttsIn.containsToken(ttThis.getToken() ); - - if( ttIn != null ) { - ttsOut.tokenTuples.add(ttThis.unionArity(ttIn) ); - } else { - ttsOut.tokenTuples.add(ttThis); - } - } - - ttItr = ttsIn.iterator(); - while( ttItr.hasNext() ) { - ReachTuple ttIn = ttItr.next(); - ReachTuple ttThis = ttsOut.containsToken(ttIn.getToken() ); - - if( ttThis == null ) { - ttsOut.tokenTuples.add(ttIn); + // this should be a hash table so we can do this by key + public ReachTuple containsHrnID( Integer hrnID ) { + assert hrnID != null; + + Iterator rtItr = reachTuples.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rt = rtItr.next(); + if( hrnID.equals( rt.getHrnID() ) ) { + return rt; } } - - return ttsOut.makeCanonical(); - } - - - public ReachState add(ReachTuple tt) { - assert tt != null; - return this.union(tt); + + return null; } - public ReachState remove(ReachTuple tt) { - assert tt != null; - ReachState ttsOut = new ReachState(this); - ttsOut.tokenTuples.remove(tt); - return ttsOut.makeCanonical(); - } - - public boolean equals(Object o) { + public boolean equals( Object o ) { if( o == null ) { return false; } @@ -168,275 +96,19 @@ public class ReachState extends Canonical { return false; } - ReachState tts = (ReachState) o; - return tokenTuples.equals(tts.tokenTuples); - } - - boolean hashcodecomputed=false; - int ourhashcode=0; - - - public int hashCode() { - if (hashcodecomputed) - return ourhashcode; - else { - ourhashcode=tokenTuples.hashCode(); - hashcodecomputed=true; - return ourhashcode; - } - } - - - // this should be a hash table so we can do this by key - public ReachTuple containsToken(Integer token) { - assert token != null; - - Iterator itr = tokenTuples.iterator(); - while( itr.hasNext() ) { - ReachTuple tt = (ReachTuple) itr.next(); - if( token.equals(tt.getToken() ) ) { - return tt; - } - } - return null; - } - - - public ReachState ageTokens(AllocSite as) { - assert as != null; - - ReachState ttsOut = new ReachState(); - - ReachTuple ttSummary = null; - ReachTuple ttOldest = null; - - Iterator itrT = this.iterator(); - while( itrT.hasNext() ) { - ReachTuple tt = (ReachTuple) itrT.next(); - - Integer token = tt.getToken(); - int age = as.getAgeCategory(token); - - // tokens not associated with - // the site should be left alone - if( age == AllocSite.AGE_notInThisSite ) { - ttsOut.tokenTuples.add(tt); - - } else if( age == AllocSite.AGE_summary ) { - // remember the summary tuple, but don't add it - // we may combine it with the oldest tuple - ttSummary = tt; - - } else if( age == AllocSite.AGE_oldest ) { - // found an oldest token, again just remember - // for later - ttOldest = tt; - - } else { - assert age == AllocSite.AGE_in_I; - - Integer I = as.getAge(token); - assert I != null; - - // otherwise, we change this token to the - // next older token - Integer tokenToChangeTo = as.getIthOldest(I + 1); - ReachTuple ttAged = tt.changeTokenTo(tokenToChangeTo); - ttsOut.tokenTuples.add(ttAged); - } - } - - // there are four cases to consider here - // 1. we found a summary tuple and no oldest tuple - // Here we just pass the summary unchanged - // 2. we found an oldest tuple, no summary - // Make a new, arity-one summary tuple - // 3. we found both a summary and an oldest - // Merge them by arity - // 4. (not handled) we found neither, do nothing - if ( ttSummary != null && ttOldest == null ) { - ttsOut.tokenTuples.add(ttSummary); - - } else if( ttSummary == null && ttOldest != null ) { - ttsOut.tokenTuples.add(new ReachTuple(as.getSummary(), - true, - ttOldest.getArity() - ).makeCanonical() - ); - - } else if( ttSummary != null && ttOldest != null ) { - ttsOut.tokenTuples.add(ttSummary.unionArity(new ReachTuple(as.getSummary(), - true, - ttOldest.getArity() - ).makeCanonical() - ) - ); - } - - return ttsOut.makeCanonical(); - } - - - public ReachState unshadowTokens(AllocSite as) { - assert as != null; - - ReachState ttsOut = new ReachState(); - - ReachTuple ttSummary = null; - ReachTuple ttShadowSummary = null; - - Iterator itrT = this.iterator(); - while( itrT.hasNext() ) { - ReachTuple tt = (ReachTuple) itrT.next(); - - Integer token = tt.getToken(); - int shadowAge = as.getShadowAgeCategory(token); - - if( shadowAge == AllocSite.AGE_summary ) { - // remember the summary tuple, but don't add it - // we may combine it with the oldest tuple - ttSummary = tt; - - } else if( shadowAge == AllocSite.SHADOWAGE_notInThisSite ) { - ttsOut.tokenTuples.add(tt); - - } else if( shadowAge == AllocSite.SHADOWAGE_summary ) { - // found the shadow summary token, again just remember - // for later - ttShadowSummary = tt; - - } else if( shadowAge == AllocSite.SHADOWAGE_oldest ) { - Integer tokenToChangeTo = as.getOldest(); - ReachTuple ttNormal = tt.changeTokenTo(tokenToChangeTo); - ttsOut.tokenTuples.add(ttNormal); - - } else { - assert shadowAge == AllocSite.SHADOWAGE_in_I; - - Integer I = as.getShadowAge(token); - assert I != null; - - Integer tokenToChangeTo = as.getIthOldest(-I); - ReachTuple ttNormal = tt.changeTokenTo(tokenToChangeTo); - ttsOut.tokenTuples.add(ttNormal); - } - } - - if ( ttSummary != null && ttShadowSummary == null ) { - ttsOut.tokenTuples.add(ttSummary); - - } else if( ttSummary == null && ttShadowSummary != null ) { - ttsOut.tokenTuples.add(new ReachTuple(as.getSummary(), - true, - ttShadowSummary.getArity() - ).makeCanonical() - ); - - } else if( ttSummary != null && ttShadowSummary != null ) { - ttsOut.tokenTuples.add(ttSummary.unionArity(new ReachTuple(as.getSummary(), - true, - ttShadowSummary.getArity() - ).makeCanonical() - ) - ); - } - - return ttsOut.makeCanonical(); - } - - - public ReachState toShadowTokens(AllocSite as) { - assert as != null; - - ReachState ttsOut = new ReachState().makeCanonical(); - - Iterator itrT = this.iterator(); - while( itrT.hasNext() ) { - ReachTuple tt = (ReachTuple) itrT.next(); - - Integer token = tt.getToken(); - int age = as.getAgeCategory(token); - - // summary tokens and tokens not associated with - // the site should be left alone - if( age == AllocSite.AGE_notInThisSite ) { - ttsOut = ttsOut.union(tt); - - } else if( age == AllocSite.AGE_summary ) { - ttsOut = ttsOut.union(tt.changeTokenTo(as.getSummaryShadow() )); - - } else if( age == AllocSite.AGE_oldest ) { - ttsOut = ttsOut.union(tt.changeTokenTo(as.getOldestShadow() )); - - } else { - assert age == AllocSite.AGE_in_I; - - Integer I = as.getAge(token); - assert I != null; - - ttsOut = ttsOut.union(tt.changeTokenTo(as.getIthOldestShadow(I) )); - } - } - - return ttsOut.makeCanonical(); + ReachState rs = (ReachState) o; + assert this.isCanonical(); + assert rs.isCanonical(); + return this == rs; } - public ReachSet rewriteToken(ReachTuple tokenToRewrite, - ReachSet replacements, - boolean makeChangeSet, - Hashtable > forChangeSet) { - - ReachSet rsOut = new ReachSet().makeCanonical(); - - if( !tokenTuples.contains(tokenToRewrite) ) { - rsOut = rsOut.add(this); - - } else { - ReachState ttsMinusToken = new ReachState(this); - ttsMinusToken.tokenTuples.remove(tokenToRewrite); - - Iterator replaceItr = replacements.iterator(); - while( replaceItr.hasNext() ) { - ReachState replacement = replaceItr.next(); - ReachState replaced = new ReachState(ttsMinusToken).makeCanonical(); - replaced = replaced.unionUpArity(replacement); - rsOut = rsOut.add(replaced); - - if( makeChangeSet ) { - assert forChangeSet != null; - - if( forChangeSet.get(this) == null ) { - forChangeSet.put(this, new HashSet() ); - } - - forChangeSet.get(this).add(replaced); - } - } - } - - return rsOut.makeCanonical(); + public int hashCodeSpecific() { + return reachTuples.hashCode(); } - public ReachState makeArityZeroOrMore() { - ReachState ttsOut = new ReachState().makeCanonical(); - - Iterator itrThis = this.iterator(); - while( itrThis.hasNext() ) { - ReachTuple tt = itrThis.next(); - - ttsOut = ttsOut.union(new ReachTuple(tt.getToken(), - tt.isMultiObject(), - ReachTuple.ARITY_ZEROORMORE - ).makeCanonical() - ); - } - - return ttsOut.makeCanonical(); - } - public String toString() { - return tokenTuples.toString(); + return reachTuples.toString(); } } diff --git a/Robust/src/Analysis/Disjoint/ReachTuple.java b/Robust/src/Analysis/Disjoint/ReachTuple.java index 9d9962d7..bfa3e1ab 100644 --- a/Robust/src/Analysis/Disjoint/ReachTuple.java +++ b/Robust/src/Analysis/Disjoint/ReachTuple.java @@ -5,61 +5,79 @@ import IR.Flat.*; import java.util.*; import java.io.*; - -// a token touple is a pair that indicates a +/////////////////////////////////////////// +// IMPORTANT +// This class is an immutable Canonical, so +// +// 0) construct them with a factory pattern +// to ensure only canonical versions escape +// +// 1) any operation that modifies a Canonical +// is a static method in the Canonical class +// +// 2) operations that just read this object +// should be defined here +// +// 3) every Canonical subclass hashCode should +// throw an error if the hash ever changes +// +/////////////////////////////////////////// + +// a reach touple is a pair that indicates a // heap region node and an arity -// THIS CLASS IS IMMUTABLE! - public class ReachTuple extends Canonical { - private Integer token; - private boolean isMultiObject; + // defined by the source heap region + protected Integer hrnID; + protected boolean isMultiObject; + // arity of reachability paths from the + // given heap region public static final int ARITY_ZEROORMORE = 0; public static final int ARITY_ONE = 1; public static final int ARITY_ONEORMORE = 2; - private int arity; - + protected int arity; - public ReachTuple(HeapRegionNode hrn) { - assert hrn != null; - token = hrn.getID(); - isMultiObject = !hrn.isSingleObject(); - arity = ARITY_ONE; - fixStuff(); + public static ReachTuple factory( Integer hrnID, + boolean isMultiObject, + int arity ) { + ReachTuple out = new ReachTuple( hrnID, + isMultiObject, + arity ); + out = (ReachTuple) Canonical.makeCanonical( out ); + return out; + } + + public static ReachTuple factory( HeapRegionNode hrn ) { + ReachTuple out = new ReachTuple( hrn.getID(), + !hrn.isSingleObject(), + ARITY_ONE ); + out = (ReachTuple) Canonical.makeCanonical( out ); + return out; } - public ReachTuple(Integer token, - boolean isMultiObject, - int arity) { - assert token != null; + private ReachTuple( Integer hrnID, + boolean isMultiObject, + int arity ) { + assert hrnID != null; - this.token = token; + this.hrnID = hrnID; this.isMultiObject = isMultiObject; this.arity = arity; - fixStuff(); - } - private void fixStuff() { - //This is an evil hack...we should fix this stuff elsewhere... - if (!isMultiObject) { - arity=ARITY_ONE; - } else { - if (arity==ARITY_ONEORMORE) - arity=ARITY_ZEROORMORE; - } - } - - - public ReachTuple makeCanonical() { - return (ReachTuple) Canonical.makeCanonical(this); + // just make sure this stuff is true now + // that analysis doesn't use ONEORMORE + assert arity != ARITY_ONEORMORE; + if( !isMultiObject ) { + assert arity == ARITY_ONE; + } } - public Integer getToken() { - return token; + public Integer getHrnID() { + return hrnID; } public boolean isMultiObject() { @@ -71,42 +89,7 @@ public class ReachTuple extends Canonical { } - public ReachTuple unionArity(ReachTuple tt) { - assert tt != null; - assert token == tt.token; - assert isMultiObject == tt.isMultiObject; - - if( isMultiObject ) { - // for multiple objects only zero-or-mores combined are still zero-or-more - // when two tokens are present (absence of a token is arity=zero and is - // handled outside of this method) - if( arity == ARITY_ZEROORMORE && tt.arity == ARITY_ZEROORMORE ) { - return new ReachTuple(token, true, ARITY_ZEROORMORE).makeCanonical(); - } else { - return new ReachTuple(token, true, ARITY_ONEORMORE).makeCanonical(); - } - - } else { - // a single object region's token can only have ZEROORMORE or ONE - if( arity == ARITY_ZEROORMORE && tt.arity == ARITY_ZEROORMORE ) { - return new ReachTuple(token, false, ARITY_ZEROORMORE).makeCanonical(); - } else { - return new ReachTuple(token, false, ARITY_ONE).makeCanonical(); - } - } - } - - - public ReachTuple changeTokenTo(Integer tokenToChangeTo) { - assert tokenToChangeTo != null; - - return new ReachTuple(tokenToChangeTo, - isMultiObject, - arity).makeCanonical(); - } - - - public boolean equals(Object o) { + public boolean equals( Object o ) { if( o == null ) { return false; } @@ -115,19 +98,19 @@ public class ReachTuple extends Canonical { return false; } - ReachTuple tt = (ReachTuple) o; - - return token.equals(tt.getToken() ) && - arity == tt.getArity(); + ReachTuple rt = (ReachTuple) o; + assert this.isCanonical(); + assert rt.isCanonical(); + return this == rt; } - public int hashCode() { - return (token.intValue() << 2) ^ arity; + public int hashCodeSpecific() { + return (hrnID.intValue() << 2) ^ arity; } public String toString() { - String s = token.toString(); + String s = hrnID.toString(); if( isMultiObject ) { s += "M"; diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java index 3c186eda..ddb3fa04 100644 --- a/Robust/src/Analysis/Disjoint/RefEdge.java +++ b/Robust/src/Analysis/Disjoint/RefEdge.java @@ -43,18 +43,18 @@ public class RefEdge { this.preds = preds; } else { // TODO: do this right? - this.preds = new ExistPredSet().makeCanonical(); + this.preds = ExistPredSet.factory(); } if( beta != null ) { this.beta = beta; } else { - this.beta = new ReachSet().makeCanonical(); + this.beta = ReachSet.factory(); } // when edges are not undergoing an operation that // is changing beta info, betaNew is always empty - betaNew = new ReachSet().makeCanonical(); + betaNew = ReachSet.factory(); } @@ -206,9 +206,8 @@ public class RefEdge { public void applyBetaNew() { assert betaNew != null; - beta = betaNew; - betaNew = new ReachSet().makeCanonical(); + betaNew = ReachSet.factory(); }