From 282eafd47fce761f4a82a754ba49ccd84ece95ae Mon Sep 17 00:00:00 2001 From: jjenista Date: Fri, 19 Mar 2010 21:28:39 +0000 Subject: [PATCH] make sure change sets ignore predicates hanging off reach states and alter reach set intersection to ignore predicates, and have a preference of taking preds from the first reach set argument so client algorithms can indicate preference --- Robust/src/Analysis/Disjoint/Canonical.java | 42 +++++++----- Robust/src/Analysis/Disjoint/ChangeTuple.java | 19 ++++-- .../src/Analysis/Disjoint/ExistPredSet.java | 5 ++ Robust/src/Analysis/Disjoint/ReachGraph.java | 67 +++++++++++-------- 4 files changed, 83 insertions(+), 50 deletions(-) diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java index c74bad4d..7f380b58 100644 --- a/Robust/src/Analysis/Disjoint/Canonical.java +++ b/Robust/src/Analysis/Disjoint/Canonical.java @@ -173,7 +173,7 @@ abstract public class Canonical { out.reachTuples.addAll( rs.reachTuples ); out.preds = Canonical.join( rs.preds, preds ); - + out = (ReachState) makeCanonical( out ); op2result.put( op, out ); return out; @@ -451,6 +451,13 @@ abstract public class Canonical { } + // NOTE: when taking the intersection of two reach sets it + // is possible for a reach state to be in both sets, but + // have different predicates. Conceptully the best new + // predicate is an AND of the source predicates, but to + // avoid eploding states we'll take an overapproximation + // by preferring the predicates from the state in the FIRST + // set, so order of arguments matters public static ReachSet intersection( ReachSet rs1, ReachSet rs2 ) { assert rs1 != null; @@ -472,9 +479,12 @@ abstract public class Canonical { ReachSet out = new ReachSet(); Iterator itr = rs1.iterator(); while( itr.hasNext() ) { - ReachState state = (ReachState) itr.next(); - if( rs2.reachStates.contains( state ) ) { - out.reachStates.add( state ); + ReachState state1 = (ReachState) itr.next(); + ReachState state2 = rs2.containsIgnorePreds( state1 ); + if( state2 != null ) { + // prefer the predicates on state1, an overapproximation + // of state1 preds AND state2 preds + out.reachStates.add( state1 ); } } @@ -552,7 +562,7 @@ abstract public class Canonical { Iterator stateItr = rs.iterator(); while( stateItr.hasNext() ) { - ReachState state = stateItr.next(); + ReachState stateOrig = stateItr.next(); boolean changeFound = false; @@ -560,14 +570,19 @@ abstract public class Canonical { while( ctItr.hasNext() ) { ChangeTuple ct = ctItr.next(); - if( state.equals( ct.getSetToMatch() ) ) { - out.reachStates.add( ct.getSetToAdd() ); + if( stateOrig.equalsIgnorePreds( ct.getStateToMatch() ) ) { + // use the new state, but the original predicates + ReachState stateNew = + ReachState.factory( ct.getStateToAdd().reachTuples, + stateOrig.preds + ); + out.reachStates.add( stateNew ); changeFound = true; } } if( keepSourceState || !changeFound ) { - out.reachStates.add( state ); + out.reachStates.add( stateOrig ); } } @@ -761,8 +776,8 @@ abstract public class Canonical { return out; } - public static ChangeSet union( ChangeSet cs, - ChangeTuple ct ) { + public static ChangeSet add( ChangeSet cs, + ChangeTuple ct ) { assert cs != null; assert ct != null; assert cs.isCanonical(); @@ -1171,13 +1186,6 @@ abstract public class Canonical { } - - - - - - - public static ReachSet unshadow( ReachSet rs, AllocSite as ) { assert rs != null; diff --git a/Robust/src/Analysis/Disjoint/ChangeTuple.java b/Robust/src/Analysis/Disjoint/ChangeTuple.java index 01bff33b..99bf8326 100644 --- a/Robust/src/Analysis/Disjoint/ChangeTuple.java +++ b/Robust/src/Analysis/Disjoint/ChangeTuple.java @@ -34,8 +34,19 @@ public class ChangeTuple extends Canonical public static ChangeTuple factory( ReachState toMatch, ReachState toAdd ) { - ChangeTuple out = new ChangeTuple( toMatch, - toAdd ); + // we don't care about the predicates hanging on + // change tuple states, so always set them to empty + // to ensure change tuple sets work out + ReachState toMatchNoPreds = + ReachState.factory( toMatch.reachTuples, + ExistPredSet.factory() + ); + ReachState toAddNoPreds = + ReachState.factory( toAdd.reachTuples, + ExistPredSet.factory() + ); + ChangeTuple out = new ChangeTuple( toMatchNoPreds, + toAddNoPreds ); out = (ChangeTuple) Canonical.makeCanonical( out ); return out; } @@ -46,10 +57,10 @@ public class ChangeTuple extends Canonical this.toAdd = toAdd; } - public ReachState getSetToMatch() { + public ReachState getStateToMatch() { return toMatch; } - public ReachState getSetToAdd() { + public ReachState getStateToAdd() { return toAdd; } diff --git a/Robust/src/Analysis/Disjoint/ExistPredSet.java b/Robust/src/Analysis/Disjoint/ExistPredSet.java index 48d9afff..c026624a 100644 --- a/Robust/src/Analysis/Disjoint/ExistPredSet.java +++ b/Robust/src/Analysis/Disjoint/ExistPredSet.java @@ -49,6 +49,11 @@ public class ExistPredSet extends Canonical { preds = new HashSet(); } + + public Iterator iterator() { + return preds.iterator(); + } + // only consider the subest of the caller elements that // are reachable by callee when testing predicates diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index f6deaab2..778c9387 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -1080,8 +1080,10 @@ public class ReachGraph { Iterator itrCprime = C.iterator(); while( itrCprime.hasNext() ) { ChangeTuple c = itrCprime.next(); - if( edgeF.getBeta().contains( c.getSetToMatch() ) ) { - changesToPass = Canonical.union( changesToPass, c ); + if( edgeF.getBeta().containsIgnorePreds( c.getStateToMatch() ) + != null + ) { + changesToPass = Canonical.add( changesToPass, c ); } } @@ -1160,8 +1162,10 @@ public class ReachGraph { Iterator itrC = C.iterator(); while( itrC.hasNext() ) { ChangeTuple c = itrC.next(); - if( edgeE.getBeta().contains( c.getSetToMatch() ) ) { - changesToPass = Canonical.union( changesToPass, c ); + if( edgeE.getBeta().containsIgnorePreds( c.getStateToMatch() ) + != null + ) { + changesToPass = Canonical.add( changesToPass, c ); } } @@ -2384,28 +2388,28 @@ public class ReachGraph { ChangeSet cs = ChangeSet.factory(); Iterator rsItr = reCaller.getBeta().iterator(); while( rsItr.hasNext() ) { - ReachState state = rsItr.next(); - ExistPredSet preds2 = state.getPreds(); - assert preds2.preds.size() == 1; + ReachState state = rsItr.next(); + ExistPredSet predsPreCallee = state.getPreds(); if( state.isEmpty() ) { continue; } - ExistPred pred = preds2.preds.iterator().next(); - ReachState old = pred.ne_state; - - if( old == null ) { - old = rstateEmpty; - } + Iterator predItr = predsPreCallee.iterator(); + while( predItr.hasNext() ) { + ExistPred pred = predItr.next(); + ReachState old = pred.ne_state; - assert old != null; + if( old == null ) { + old = rstateEmpty; + } - cs = Canonical.union( cs, + cs = Canonical.add( cs, ChangeTuple.factory( old, state ) ); + } } // look to see if an edge with same field exists @@ -2985,19 +2989,21 @@ public class ReachGraph { if( prevResult == null || Canonical.unionORpreds( prevResult, - intersection ).size() > prevResult.size() ) { + intersection ).size() + > prevResult.size() + ) { if( prevResult == null ) { boldB_f.put( edgePrime, Canonical.unionORpreds( edgePrime.getBeta(), - intersection - ) + intersection + ) ); } else { boldB_f.put( edgePrime, Canonical.unionORpreds( prevResult, - intersection - ) + intersection + ) ); } workSetEdges.add( edgePrime ); @@ -3095,8 +3101,8 @@ public class ReachGraph { // if there is nothing marked, just move on if( markedHrnIDs.isEmpty() ) { hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(), - stateOld - ) + stateOld + ) ); continue; } @@ -3115,13 +3121,13 @@ public class ReachGraph { assert !stateOld.equals( statePruned ); hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(), - statePruned - ) + statePruned + ) ); ChangeTuple ct = ChangeTuple.factory( stateOld, statePruned ); - cts = Canonical.union( cts, ct ); + cts = Canonical.add( cts, ct ); } // throw change tuple set on all incident edges @@ -3216,7 +3222,10 @@ public class ReachGraph { if( Canonical.unionORpreds( prevResult, intersection - ).size() > prevResult.size() ) { + ).size() + > prevResult.size() + ) { + edge.setBetaNew( Canonical.unionORpreds( prevResult, intersection @@ -4044,10 +4053,10 @@ public class ReachGraph { } } - Set intersection = new HashSet( - reachableNodes1); + Set intersection = + new HashSet( reachableNodes1 ); - intersection.retainAll(reachableNodes2); + intersection.retainAll( reachableNodes2 ); return intersection; } -- 2.34.1