From deb696523b17714935a17fa0c6e3401e9914774c Mon Sep 17 00:00:00 2001 From: jjenista Date: Tue, 2 Feb 2010 20:08:01 +0000 Subject: [PATCH] implementing --- .../Analysis/Disjoint/DisjointAnalysis.java | 2 +- Robust/src/Analysis/Disjoint/ExistPred.java | 6 +- .../src/Analysis/Disjoint/ExistPredEdge.java | 185 ++++++++++++++++++ .../src/Analysis/Disjoint/ExistPredNode.java | 83 ++++++++ .../src/Analysis/Disjoint/ExistPredSet.java | 40 +++- .../src/Analysis/Disjoint/HeapRegionNode.java | 22 ++- Robust/src/Analysis/Disjoint/ReachGraph.java | 54 +++-- Robust/src/Analysis/Disjoint/RefEdge.java | 39 +++- .../Tests/disjoint/predicateTest1/makefile | 27 +++ .../Tests/disjoint/predicateTest1/test.java | 77 ++++++++ 10 files changed, 507 insertions(+), 28 deletions(-) create mode 100644 Robust/src/Analysis/Disjoint/ExistPredEdge.java create mode 100644 Robust/src/Analysis/Disjoint/ExistPredNode.java create mode 100644 Robust/src/Tests/disjoint/predicateTest1/makefile create mode 100644 Robust/src/Tests/disjoint/predicateTest1/test.java diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index b29e15d6..94c9de6e 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -588,7 +588,7 @@ public class DisjointAnalysis { // calculate the heap this call site can reach--note this is // not used for the current call site transform, we are // grabbing this heap model for future analysis of the callees, - // of if different results emerge we will return to this site + // so if different results emerge we will return to this site ReachGraph heapForThisCall_old = getIHMcontribution( mdCallee, fc ); diff --git a/Robust/src/Analysis/Disjoint/ExistPred.java b/Robust/src/Analysis/Disjoint/ExistPred.java index 689e5084..c71b31bd 100644 --- a/Robust/src/Analysis/Disjoint/ExistPred.java +++ b/Robust/src/Analysis/Disjoint/ExistPred.java @@ -11,9 +11,11 @@ import java.io.*; // predicates are not satisfied in the // caller's context -public class ExistPred extends Canonical { +abstract public class ExistPred extends Canonical { - + public ExistPred makeCanonical() { + return (ExistPred) Canonical.makeCanonical( this ); + } public boolean isSatisfiedBy( ReachGraph rg ) { return true; diff --git a/Robust/src/Analysis/Disjoint/ExistPredEdge.java b/Robust/src/Analysis/Disjoint/ExistPredEdge.java new file mode 100644 index 00000000..ffe598dc --- /dev/null +++ b/Robust/src/Analysis/Disjoint/ExistPredEdge.java @@ -0,0 +1,185 @@ +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 Canonical { + + // 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 (vnSrc == null) || (hrnSrcID == null); + assert hrnDstID != null; + assert type != null; + 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.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 += hrnDst.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 new file mode 100644 index 00000000..6ef0a6e9 --- /dev/null +++ b/Robust/src/Analysis/Disjoint/ExistPredNode.java @@ -0,0 +1,83 @@ +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 Canonical { + + 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 29ab305e..a538ef0d 100644 --- a/Robust/src/Analysis/Disjoint/ExistPredSet.java +++ b/Robust/src/Analysis/Disjoint/ExistPredSet.java @@ -11,7 +11,43 @@ import java.io.*; public class ExistPredSet extends Canonical { - private HashSet preds; + protected Set preds; + + public ExistPredSet() { + preds = new HashSet(); + } + + public ExistPredSet makeCanonical() { + return (ExistPredSet) ExistPredSet.makeCanonical( this ); + } + + + public void add( ExistPred pred ) { + preds.add( pred ); + } + + public boolean isSatisfiedBy( ReachGraph rg ) { + Iterator predItr = preds.iterator(); + while( predItr.hasNext() ) { + if( !predItr.next().isSatisfiedBy( rg ) ) { + return false; + } + } + return true; + } + + public String toString() { + String s = "P["; + Iterator predItr = preds.iterator(); + while( predItr.hasNext() ) { + ExistPred pred = predItr.next(); + s += pred.toString(); + if( predItr.hasNext() ) { + s += " && "; + } + } + s += "]"; + return s; + } - public } diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java index 5213aa6b..0d014b21 100644 --- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java +++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java @@ -38,6 +38,12 @@ public class HeapRegionNode extends RefSrcNode { protected String description; + // existence predicates must be true in a caller + // context for this node to transfer from this + // callee to that context--NOTE, existence predicates + // do not factor into node comparisons + protected ExistPredSet preds; + public HeapRegionNode( Integer id, boolean isSingleObject, @@ -49,6 +55,7 @@ public class HeapRegionNode extends RefSrcNode { AllocSite allocSite, ReachSet inherent, ReachSet alpha, + ExistPredSet preds, String description ) { @@ -62,6 +69,7 @@ public class HeapRegionNode extends RefSrcNode { this.allocSite = allocSite; this.inherent = inherent; this.alpha = alpha; + this.preds = preds; this.description = description; referencers = new HashSet(); @@ -79,6 +87,7 @@ public class HeapRegionNode extends RefSrcNode { allocSite, inherent, alpha, + preds, description ); } @@ -88,8 +97,13 @@ public class HeapRegionNode extends RefSrcNode { } - public boolean equalsIncludingAlpha( HeapRegionNode hrn ) { - return equals( hrn ) && alpha.equals( hrn.alpha ); + // alpha and preds contribute towards reaching the + // fixed point, so use this method to determine if + // a node is "equal" to some previous visit, basically + public boolean equalsIncludingAlphaAndPreds( HeapRegionNode hrn ) { + return equals( hrn ) && + alpha.equals( hrn.alpha ) && + preds.equals( hrn.preds ); } @@ -248,6 +262,10 @@ public class HeapRegionNode extends RefSrcNode { return alpha.toStringEscapeNewline( hideSubsetReachability ); } + public String getPredString() { + return preds.toString(); + } + public String toString() { return "HRN"+getIDString(); } diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 5f688e4a..7775e642 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -20,6 +20,10 @@ public class ReachGraph { protected static final ReachSet rsetEmpty = new ReachSet().makeCanonical(); protected static final ReachSet rsetWithEmptyState = new ReachSet( rstateEmpty ).makeCanonical(); + // predicate constants + protected static final ExistPredSet predsEmpty = new ExistPredSet().makeCanonical(); + + // from DisjointAnalysis for convenience protected static int allocationDepth = -1; protected static TypeUtil typeUtil = null; @@ -73,6 +77,7 @@ public class ReachGraph { AllocSite allocSite, ReachSet inherent, ReachSet alpha, + ExistPredSet preds, String description ) { @@ -110,6 +115,11 @@ public class ReachGraph { if( alpha == null ) { alpha = inherent; } + + if( preds == null ) { + // TODO: do this right? + preds = new ExistPredSet().makeCanonical(); + } HeapRegionNode hrn = new HeapRegionNode( id, isSingleObject, @@ -121,6 +131,7 @@ public class ReachGraph { allocSite, inherent, alpha, + preds, description ); id2hrn.put( id, hrn ); return hrn; @@ -351,7 +362,8 @@ public class ReachGraph { tdNewEdge, null, false, - betaY.intersection( betaHrn ) + betaY.intersection( betaHrn ), + predsEmpty ); addRefEdge( lnX, hrnHrn, edgeNew ); @@ -498,7 +510,8 @@ public class ReachGraph { tdNewEdge, f.getSymbol(), false, - edgeY.getBeta().pruneBy( hrnX.getAlpha() ) + edgeY.getBeta().pruneBy( hrnX.getAlpha() ), + predsEmpty ); // look to see if an edge with same field exists @@ -583,7 +596,8 @@ public class ReachGraph { type, // type null, // field name false, // is initial param - hrnNewest.getAlpha() // beta + hrnNewest.getAlpha(), // beta + predsEmpty // predicates ); addRefEdge( lnX, hrnNewest, edgeNew ); @@ -714,6 +728,7 @@ public class ReachGraph { as, // allocation site null, // inherent reach null, // current reach + predsEmpty, // predicates strDesc // description ); @@ -731,6 +746,7 @@ public class ReachGraph { as, // allocation site null, // inherent reach null, // current reach + predsEmpty, // predicates strDesc // description ); } @@ -768,6 +784,7 @@ public class ReachGraph { as, // allocation site null, // inherent reach null, // current reach + predsEmpty, // predicates strDesc // description ); @@ -784,7 +801,8 @@ public class ReachGraph { as.getType(), // type as, // allocation site null, // inherent reach - null, // current reach + null, // current reach + predsEmpty, // predicates strDesc // description ); } @@ -1143,6 +1161,7 @@ public class ReachGraph { hrnSrcCaller.getAllocSite(), toShadowTokens( this, hrnSrcCaller.getInherent() ), toShadowTokens( this, hrnSrcCaller.getAlpha() ), + predsEmpty, hrnSrcCaller.getDescription() ); callerNodesCopiedToCallee.add( rsnCaller ); @@ -1173,6 +1192,7 @@ public class ReachGraph { hrnCaller.getAllocSite(), toShadowTokens( this, hrnCaller.getInherent() ), toShadowTokens( this, hrnCaller.getAlpha() ), + predsEmpty, hrnCaller.getDescription() ); callerNodesCopiedToCallee.add( hrnCaller ); @@ -1189,7 +1209,8 @@ public class ReachGraph { reCaller.getType(), reCaller.getField(), true, // clean? - toShadowTokens( this, reCaller.getBeta() ) + toShadowTokens( this, reCaller.getBeta() ), + predsEmpty ) ); callerEdgesCopiedToCallee.add( reCaller ); @@ -1246,6 +1267,7 @@ public class ReachGraph { null, // alloc site, shouldn't be used toShadowTokens( this, hrnCallerAndOutContext.getAlpha() ), // inherent toShadowTokens( this, hrnCallerAndOutContext.getAlpha() ), // alpha + predsEmpty, "out-of-context" ); @@ -1259,7 +1281,8 @@ public class ReachGraph { edgeMightCross.getType(), edgeMightCross.getField(), true, // clean? - toShadowTokens( this, edgeMightCross.getBeta() ) + toShadowTokens( this, edgeMightCross.getBeta() ), + predsEmpty ) ); } @@ -1325,6 +1348,7 @@ public class ReachGraph { hrnCallee.getAllocSite(), unShadowTokens( rgCallee, hrnCallee.getInherent() ), unShadowTokens( rgCallee, hrnCallee.getAlpha() ), + predsEmpty, hrnCallee.getDescription() ); @@ -1931,7 +1955,7 @@ public class ReachGraph { } HeapRegionNode hrnB = rgB.id2hrn.get( idA ); - if( !hrnA.equalsIncludingAlpha( hrnB ) ) { + if( !hrnA.equalsIncludingAlphaAndPreds( hrnB ) ) { return false; } } @@ -2071,7 +2095,9 @@ public class ReachGraph { // there is an edge in the right place with the right field, // but do they have the same attributes? - if( edgeA.getBeta().equals( edgeB.getBeta() ) ) { + if( edgeA.getBeta().equals( edgeB.getBeta() ) && + edgeA.equalsPreds( edgeB ) + ) { edgeFound = true; } } @@ -2330,16 +2356,16 @@ public class ReachGraph { } attributes += ",label=\"ID" + - hrn.getID() + + hrn.getID() + "\\n"; if( hrn.getType() != null ) { - attributes += hrn.getType().toPrettyString() + "\\n"; + attributes += hrn.getType().toPrettyString()+"\\n"; } - attributes += hrn.getDescription() + - "\\n" + - hrn.getAlphaString( hideSubsetReachability ) + + attributes += hrn.getDescription()+ + "\\n"+hrn.getAlphaString( hideSubsetReachability )+ + "\\n"+hrn.getPredString()+ "\"]"; bw.write( " "+hrn.toString()+attributes+";\n" ); @@ -2354,7 +2380,7 @@ public class ReachGraph { " -> " +hrnChild.toString()+ "[label=\""+edge.toGraphEdgeString( hideSubsetReachability )+ "\",decorate];\n"); - + traverseHeapRegionNodes( hrnChild, bw, td, diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java index 30c7a611..72bd42cc 100644 --- a/Robust/src/Analysis/Disjoint/RefEdge.java +++ b/Robust/src/Analysis/Disjoint/RefEdge.java @@ -23,13 +23,20 @@ public class RefEdge { protected RefSrcNode src; protected HeapRegionNode dst; + // existence predicates must be true in a caller + // context for this edge to transfer from this + // callee to that context--NOTE, existence predicates + // do not factor into edge comparisons + protected ExistPredSet preds; + public RefEdge( RefSrcNode src, HeapRegionNode dst, TypeDescriptor type, String field, boolean isClean, - ReachSet beta ) { + ReachSet beta, + ExistPredSet preds ) { assert type != null; this.src = src; @@ -38,6 +45,13 @@ public class RefEdge { this.field = field; this.isClean = isClean; + if( preds != null ) { + this.preds = preds; + } else { + // TODO: do this right? + this.preds = new ExistPredSet().makeCanonical(); + } + if( beta != null ) { this.beta = beta; } else { @@ -55,8 +69,9 @@ public class RefEdge { dst, type, field, - isClean, - beta ); + isClean, + beta, + preds ); return copy; } @@ -93,10 +108,19 @@ public class RefEdge { } - public boolean equalsIncludingBeta( RefEdge edge ) { - return equals( edge ) && beta.equals( edge.beta ); + // beta and preds contribute towards reaching the + // fixed point, so use this method to determine if + // an edge is "equal" to some previous visit, basically + public boolean equalsIncludingBetaAndPreds( RefEdge edge ) { + return equals( edge ) && + beta.equals( edge.beta ) && + preds.equals( edge.preds ); } - + + public boolean equalsPreds( RefEdge edge ) { + return preds.equals( edge.preds ); + } + public int hashCode() { int hash = 0; @@ -221,7 +245,8 @@ public class RefEdge { edgeLabel += "*clean*\\n"; } - edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability ); + edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability ) + + "\\n" + preds.toString(); return edgeLabel; } diff --git a/Robust/src/Tests/disjoint/predicateTest1/makefile b/Robust/src/Tests/disjoint/predicateTest1/makefile new file mode 100644 index 00000000..dcb012af --- /dev/null +++ b/Robust/src/Tests/disjoint/predicateTest1/makefile @@ -0,0 +1,27 @@ +PROGRAM=test + +SOURCE_FILES=$(PROGRAM).java + +BUILDSCRIPT=~/research/Robust/src/buildscript +BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -disjoint-write-dots final -disjoint-alias-file aliases.txt normal -enable-assertions + +all: $(PROGRAM).bin + +view: PNGs + eog *.png & + +PNGs: DOTs + d2p *COMPLETE*.dot + +DOTs: $(PROGRAM).bin + +$(PROGRAM).bin: $(SOURCE_FILES) + $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES) + +clean: + rm -f $(PROGRAM).bin + rm -fr tmpbuilddirectory + rm -f *~ + rm -f *.dot + rm -f *.png + rm -f aliases.txt diff --git a/Robust/src/Tests/disjoint/predicateTest1/test.java b/Robust/src/Tests/disjoint/predicateTest1/test.java new file mode 100644 index 00000000..c49595d9 --- /dev/null +++ b/Robust/src/Tests/disjoint/predicateTest1/test.java @@ -0,0 +1,77 @@ +public class Foo { + public Foo() {} + public Bar b; +} + +public class Foo1 extends Foo { + public Foo1() {} +} + +public class Foo2 extends Foo { + public Foo2() {} +} + +public class Bar { + public Bar() {} +} + +public class Bar1 extends Bar { + public Bar1() {} +} + +public class Bar2 extends Bar { + public Bar2() {} +} + +/////////////////////////////////////// +// +// These classes define a virtual +// method addBar() that will, depending +// the dispatch, allocate a Bar from +// one of two allocation sites +// +/////////////////////////////////////// +public class DoodadBase { + public DoodadBase() {} + + public void addBar( Foo f ) {} +} + +public class Doodad1 extends DoodadBase { + public Doodad1() {} + + public void addBar( Foo f ) { + f.b = new Bar1(); + } +} + +public class Doodad2 extends DoodadBase { + public Doodad2() {} + + public void addBar( Foo f ) { + f.b = new Bar2(); + } +} + + +////////////////////////////////////// +// +// Now set up two call sites, one that +// invokes one virtual, and another for +// other, and verify that predicates +// can sort out the conservative merge +// of virtual results by call site +// +////////////////////////////////////// +public class Test { + static public void main( String[] args ) { + + DoodadBase d1 = new Doodad1(); + Foo f1 = new Foo1(); + d1.addBar( f1 ); + + DoodadBase d2 = new Doodad2(); + Foo f2 = new Foo2(); + d2.addBar( f2 ); + } +} -- 2.34.1