From: jjenista Date: Tue, 16 Mar 2010 00:32:31 +0000 (+0000) Subject: updating the global sweep and some related code--this currently bombs, only update... X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=3886c642471aa68f44503cd6ec57ca9f46de4731;p=IRC.git updating the global sweep and some related code--this currently bombs, only update if you must, it will compile though --- diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 30e9ddb1..07552410 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -10,7 +10,7 @@ public class ReachGraph { // use to disable improvements for comparison protected static final boolean DISABLE_STRONG_UPDATES = false; - protected static final boolean DISABLE_GLOBAL_SWEEP = true; + protected static final boolean DISABLE_GLOBAL_SWEEP = false; // a special out-of-scope temp protected static final TempDescriptor tdReturn = new TempDescriptor( "_Return___" ); @@ -2486,7 +2486,9 @@ public class ReachGraph { // 5. - globalSweep(); + if( !DISABLE_GLOBAL_SWEEP ) { + globalSweep(); + } @@ -2622,10 +2624,25 @@ public class ReachGraph { public void globalSweep() { // boldB is part of the phase 1 sweep - Hashtable< Integer, Hashtable > boldB = + // it has an in-context table and an out-of-context table + Hashtable< Integer, Hashtable > boldBic = + new Hashtable< Integer, Hashtable >(); + + Hashtable< Integer, Hashtable > boldBooc = new Hashtable< Integer, Hashtable >(); - // visit every heap region to initialize alphaNew and calculate boldB + // visit every heap region to initialize alphaNew and betaNew, + // and make a map of every hrnID to the source nodes it should + // propagate forward from. In-context flagged hrnID's propagate + // from only the in-context node they name, but out-of-context + // ID's may propagate from several out-of-context nodes + Hashtable< Integer, Set > icID2srcs = + new Hashtable< Integer, Set >(); + + Hashtable< Integer, Set > oocID2srcs = + new Hashtable< Integer, Set >(); + + Iterator itrHrns = id2hrn.entrySet().iterator(); while( itrHrns.hasNext() ) { Map.Entry me = (Map.Entry) itrHrns.next(); @@ -2642,64 +2659,129 @@ public class ReachGraph { assert rsetEmpty.equals( edge.getBetaNew() ); } - // calculate boldB for this flagged node + // calculate boldB for this flagged node, or out-of-context node if( hrn.isFlagged() ) { - - Hashtable boldB_f = - new Hashtable(); - - Set workSetEdges = new HashSet(); + assert !hrn.isOutOfContext(); + assert !icID2srcs.containsKey( hrn.getID() ); + Set srcs = new HashSet(); + srcs.add( hrn ); + icID2srcs.put( hrn.getID(), srcs ); + } - // initial boldB_f constraints - Iterator itrRees = hrn.iteratorToReferencees(); - while( itrRees.hasNext() ) { - RefEdge edge = itrRees.next(); + if( hrn.isOutOfContext() ) { + assert !hrn.isFlagged(); - assert !boldB.containsKey( edge ); - boldB_f.put( edge, edge.getBeta() ); + Iterator stateItr = hrn.getAlpha().iterator(); + while( stateItr.hasNext() ) { + ReachState state = stateItr.next(); - assert !workSetEdges.contains( edge ); - workSetEdges.add( edge ); - } + Iterator rtItr = state.iterator(); + while( rtItr.hasNext() ) { + ReachTuple rt = rtItr.next(); + assert rt.isOutOfContext(); - // enforce the boldB_f constraint at edges until we reach a fixed point - while( !workSetEdges.isEmpty() ) { - RefEdge edge = workSetEdges.iterator().next(); - workSetEdges.remove( edge ); - - Iterator itrPrime = edge.getDst().iteratorToReferencees(); - while( itrPrime.hasNext() ) { - RefEdge edgePrime = itrPrime.next(); + Set srcs = oocID2srcs.get( rt.getHrnID() ); + if( srcs == null ) { + srcs = new HashSet(); + } + srcs.add( hrn ); + oocID2srcs.put( rt.getHrnID(), srcs ); + } + } + } + } + + // calculate boldB for all hrnIDs identified by the above + // node traversal, propagating from every source + while( !icID2srcs.isEmpty() || !oocID2srcs.isEmpty() ) { + + Integer hrnID; + Set srcs; + boolean inContext; + + if( !icID2srcs.isEmpty() ) { + Map.Entry me = (Map.Entry) icID2srcs.entrySet().iterator().next(); + hrnID = (Integer) me.getKey(); + srcs = (Set) me.getValue(); + inContext = true; + icID2srcs.remove( hrnID ); + + } else { + assert !oocID2srcs.isEmpty(); + + Map.Entry me = (Map.Entry) oocID2srcs.entrySet().iterator().next(); + hrnID = (Integer) me.getKey(); + srcs = (Set) me.getValue(); + inContext = false; + oocID2srcs.remove( hrnID ); + } + + + Hashtable boldB_f = + new Hashtable(); + + Set workSetEdges = new HashSet(); - ReachSet prevResult = boldB_f.get( edgePrime ); - ReachSet intersection = Canonical.intersection( boldB_f.get( edge ), + Iterator hrnItr = srcs.iterator(); + while( hrnItr.hasNext() ) { + HeapRegionNode hrn = hrnItr.next(); + + assert workSetEdges.isEmpty(); + + // initial boldB_f constraints + Iterator itrRees = hrn.iteratorToReferencees(); + while( itrRees.hasNext() ) { + RefEdge edge = itrRees.next(); + + assert !boldB_f.containsKey( edge ); + boldB_f.put( edge, edge.getBeta() ); + + assert !workSetEdges.contains( edge ); + workSetEdges.add( edge ); + } + + // enforce the boldB_f constraint at edges until we reach a fixed point + while( !workSetEdges.isEmpty() ) { + RefEdge edge = workSetEdges.iterator().next(); + workSetEdges.remove( edge ); + + Iterator itrPrime = edge.getDst().iteratorToReferencees(); + while( itrPrime.hasNext() ) { + RefEdge edgePrime = itrPrime.next(); + + ReachSet prevResult = boldB_f.get( edgePrime ); + ReachSet intersection = Canonical.intersection( boldB_f.get( edge ), edgePrime.getBeta() ); - - if( prevResult == null || - Canonical.union( prevResult, + + if( prevResult == null || + Canonical.union( prevResult, intersection ).size() > prevResult.size() ) { - - if( prevResult == null ) { - boldB_f.put( edgePrime, + + if( prevResult == null ) { + boldB_f.put( edgePrime, Canonical.union( edgePrime.getBeta(), intersection ) ); - } else { - boldB_f.put( edgePrime, + } else { + boldB_f.put( edgePrime, Canonical.union( prevResult, intersection ) ); - } - workSetEdges.add( edgePrime ); - } - } - } - - boldB.put( hrnID, boldB_f ); - } + } + workSetEdges.add( edgePrime ); + } + } + } + } + + if( inContext ) { + boldBic.put( hrnID, boldB_f ); + } else { + boldBooc.put( hrnID, boldB_f ); + } } @@ -2717,14 +2799,20 @@ public class ReachGraph { 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, - false // out-of-context - ); + // out-of-context nodes don't participate in the + // global sweep, they serve as sources for the pass + // performed above + if( hrn.isOutOfContext() ) { + continue; + } + + // the inherent states of a region are the exception + // to removal as the global sweep prunes + ReachTuple rtException = ReachTuple.factory( hrnID, + !hrn.isSingleObject(), + ReachTuple.ARITY_ONE, + false // out-of-context + ); ChangeSet cts = ChangeSet.factory(); @@ -2747,23 +2835,27 @@ public class ReachGraph { } } - // does boldB_ttOld allow this hrnID? + // does boldB 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 = rtOld.getHrnID(); - assert id2hrn.containsKey( idOld ); - Hashtable B = boldB.get( idOld ); - ReachSet boldB_ttOld_incident = B.get( incidentEdge ); - if( boldB_ttOld_incident != null && - boldB_ttOld_incident.contains( stateOld ) ) { + Hashtable B; + if( rtOld.isOutOfContext() ) { + B = boldBooc.get( rtOld.getHrnID() ); + } else { + assert id2hrn.containsKey( rtOld.getHrnID() ); + B = boldBic.get( rtOld.getHrnID() ); + } + + ReachSet boldB_rtOld_incident = B.get( incidentEdge ); + if( boldB_rtOld_incident != null && + boldB_rtOld_incident.contains( stateOld ) ) { foundState = true; } } - + if( !foundState ) { markedHrnIDs = Canonical.add( markedHrnIDs, rtOld ); } diff --git a/Robust/src/Analysis/Disjoint/ReachState.java b/Robust/src/Analysis/Disjoint/ReachState.java index 732054a3..21fc2811 100644 --- a/Robust/src/Analysis/Disjoint/ReachState.java +++ b/Robust/src/Analysis/Disjoint/ReachState.java @@ -121,6 +121,10 @@ public class ReachState extends Canonical { public String toString() { + return reachTuples.toString(); + } + + public String toStringPreds() { return reachTuples+":"+preds; } } diff --git a/Robust/src/Tests/disjoint/predicateTest3/test.java b/Robust/src/Tests/disjoint/predicateTest3/test.java index f8b640b9..00c84f4e 100644 --- a/Robust/src/Tests/disjoint/predicateTest3/test.java +++ b/Robust/src/Tests/disjoint/predicateTest3/test.java @@ -7,7 +7,9 @@ public class Test { static public void main( String[] args ) { Foo top = disjoint inMain new Foo(); - addSomething( top ); + Foo bot = new Foo(); + top.f = bot; + addSomething( bot ); } public static void addSomething( Foo x ) {