From: jjenista <jjenista> Date: Mon, 15 Mar 2010 22:15:27 +0000 (+0000) Subject: have to test predicates of callee states before admitting to caller, and calculate... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4f663300f6531002e0d76e12ec0bb50fd4a75101;p=IRC.git have to test predicates of callee states before admitting to caller, and calculate what predicate caller version will have --- diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java index e7f01945..8e2b944f 100644 --- a/Robust/src/Analysis/Disjoint/Canonical.java +++ b/Robust/src/Analysis/Disjoint/Canonical.java @@ -989,6 +989,7 @@ abstract public class Canonical { } + public static ReachSet toCallerContext( ReachSet rs, AllocSite as ) { assert rs != null; @@ -1020,6 +1021,7 @@ abstract public class Canonical { op2result.put( op, out ); return out; } + public static ReachSet toCallerContext( ReachState state, AllocSite as ) { diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 470c8607..30e9ddb1 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -1344,13 +1344,45 @@ public class ReachGraph { // used below to convert a ReachSet to its caller-context // equivalent with respect to allocation sites in this graph - protected ReachSet toCallerContext( ReachSet rs ) { - ReachSet out = rs; - Iterator<AllocSite> asItr = allocSites.iterator(); - while( asItr.hasNext() ) { - AllocSite as = asItr.next(); - out = Canonical.toCallerContext( out, as ); + protected ReachSet + toCallerContext( ReachSet rs, + Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied + ) { + ReachSet out = ReachSet.factory(); + + Iterator<ReachState> itr = rs.iterator(); + while( itr.hasNext() ) { + ReachState stateCallee = itr.next(); + + if( calleeStatesSatisfied.containsKey( stateCallee ) ) { + + // starting from one callee state... + ReachSet rsCaller = ReachSet.factory( stateCallee ); + + // possibly branch it into many states, which any + // allocation site might do, so lots of derived states + Iterator<AllocSite> asItr = allocSites.iterator(); + while( asItr.hasNext() ) { + AllocSite as = asItr.next(); + rsCaller = Canonical.toCallerContext( rs, as ); + } + + // then before adding each derived, now caller-context + // states to the output, attach the appropriate pred + // based on the source callee state + Iterator<ReachState> stateItr = rsCaller.iterator(); + while( stateItr.hasNext() ) { + ReachState stateCaller = stateItr.next(); + stateCaller = Canonical.attach( stateCaller, + calleeStatesSatisfied.get( stateCallee ) + ); + out = Canonical.union( out, + stateCaller + ); + } + } } + assert out.isCanonical(); return out; } @@ -1823,6 +1855,9 @@ public class ReachGraph { Hashtable<RefEdge, ExistPredSet> calleeEdgesSatisfied = new Hashtable<RefEdge, ExistPredSet>(); + Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied = + new Hashtable<ReachState, ExistPredSet>(); + Hashtable< RefEdge, Set<RefSrcNode> > calleeEdges2oocCallerSrcMatches = new Hashtable< RefEdge, Set<RefSrcNode> >(); @@ -1846,7 +1881,23 @@ public class ReachGraph { // otherwise don't bother looking at edges to this node continue; } + + // since the node is coming over, find out which reach + // states on it should come over, too + Iterator<ReachState> stateItr = hrnCallee.getAlpha().iterator(); + while( stateItr.hasNext() ) { + ReachState stateCallee = stateItr.next(); + + predsIfSatis = + stateCallee.getPreds().isSatisfiedBy( this, + callerNodeIDsCopiedToCallee + ); + if( predsIfSatis != null ) { + calleeStatesSatisfied.put( stateCallee, predsIfSatis ); + } + } + // then look at edges to the node Iterator<RefEdge> reItr = hrnCallee.iteratorToReferencers(); while( reItr.hasNext() ) { RefEdge reCallee = reItr.next(); @@ -1927,6 +1978,22 @@ public class ReachGraph { ); if( predsIfSatis != null ) { calleeEdgesSatisfied.put( reCallee, predsIfSatis ); + + // since the edge is coming over, find out which reach + // states on it should come over, too + stateItr = reCallee.getBeta().iterator(); + while( stateItr.hasNext() ) { + ReachState stateCallee = stateItr.next(); + + predsIfSatis = + stateCallee.getPreds().isSatisfiedBy( this, + callerNodeIDsCopiedToCallee + ); + if( predsIfSatis != null ) { + calleeStatesSatisfied.put( stateCallee, predsIfSatis ); + } + } + } } @@ -1957,6 +2024,22 @@ public class ReachGraph { ); if( predsIfSatis != null ) { calleeEdgesSatisfied.put( reCallee, predsIfSatis ); + + // since the edge is coming over, find out which reach + // states on it should come over, too + Iterator<ReachState> stateItr = reCallee.getBeta().iterator(); + while( stateItr.hasNext() ) { + ReachState stateCallee = stateItr.next(); + + predsIfSatis = + stateCallee.getPreds().isSatisfiedBy( this, + callerNodeIDsCopiedToCallee + ); + if( predsIfSatis != null ) { + calleeStatesSatisfied.put( stateCallee, predsIfSatis ); + } + } + } } } @@ -2031,7 +2114,8 @@ public class ReachGraph { false, // out-of-context? hrnCallee.getType(), // type hrnCallee.getAllocSite(), // allocation site - toCallerContext( hrnCallee.getInherent() ), // inherent reach + toCallerContext( hrnCallee.getInherent(), + calleeStatesSatisfied ), // inherent reach null, // current reach predsEmpty, // predicates hrnCallee.getDescription() // description @@ -2040,8 +2124,10 @@ public class ReachGraph { assert hrnCaller.isWiped(); } - // TODO: alpha should be some rewritten version of callee in caller context - hrnCaller.setAlpha( toCallerContext( hrnCallee.getAlpha() ) ); + hrnCaller.setAlpha( toCallerContext( hrnCallee.getAlpha(), + calleeStatesSatisfied + ) + ); hrnCaller.setPreds( preds ); } @@ -2124,8 +2210,10 @@ public class ReachGraph { false, // out-of-context? hrnSrcCallee.getType(), // type hrnSrcCallee.getAllocSite(), // allocation site - toCallerContext( hrnSrcCallee.getInherent() ), // inherent reach - toCallerContext( hrnSrcCallee.getAlpha() ), // current reach + toCallerContext( hrnSrcCallee.getInherent(), + calleeStatesSatisfied ), // inherent reach + toCallerContext( hrnSrcCallee.getAlpha(), + calleeStatesSatisfied ), // current reach predsEmpty, // predicates hrnSrcCallee.getDescription() // description ); @@ -2153,7 +2241,8 @@ public class ReachGraph { hrnDstCaller, reCallee.getType(), reCallee.getField(), - toCallerContext( reCallee.getBeta() ), + toCallerContext( reCallee.getBeta(), + calleeStatesSatisfied ), preds ); @@ -2235,8 +2324,10 @@ public class ReachGraph { false, // out-of-context? hrnDstCallee.getType(), // type hrnDstCallee.getAllocSite(), // allocation site - toCallerContext( hrnDstCallee.getInherent() ), // inherent reach - toCallerContext( hrnDstCallee.getAlpha() ), // current reach + toCallerContext( hrnDstCallee.getInherent(), + calleeStatesSatisfied ), // inherent reach + toCallerContext( hrnDstCallee.getAlpha(), + calleeStatesSatisfied ), // current reach predsTrue, // predicates hrnDstCallee.getDescription() // description ); @@ -2254,7 +2345,8 @@ public class ReachGraph { hrnDstCaller, tdNewEdge, null, - toCallerContext( reCallee.getBeta() ), + toCallerContext( reCallee.getBeta(), + calleeStatesSatisfied ), predsTrue );