// 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 );
// 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;
--- /dev/null
+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;
+ }
+}
--- /dev/null
+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;
+ }
+}
public class ExistPredSet extends Canonical {
- private HashSet<ExistPred> preds;
+ protected Set<ExistPred> preds;
+
+ public ExistPredSet() {
+ preds = new HashSet<ExistPred>();
+ }
+
+ public ExistPredSet makeCanonical() {
+ return (ExistPredSet) ExistPredSet.makeCanonical( this );
+ }
+
+
+ public void add( ExistPred pred ) {
+ preds.add( pred );
+ }
+
+ public boolean isSatisfiedBy( ReachGraph rg ) {
+ Iterator<ExistPred> predItr = preds.iterator();
+ while( predItr.hasNext() ) {
+ if( !predItr.next().isSatisfiedBy( rg ) ) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public String toString() {
+ String s = "P[";
+ Iterator<ExistPred> predItr = preds.iterator();
+ while( predItr.hasNext() ) {
+ ExistPred pred = predItr.next();
+ s += pred.toString();
+ if( predItr.hasNext() ) {
+ s += " && ";
+ }
+ }
+ s += "]";
+ return s;
+ }
- public
}
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,
AllocSite allocSite,
ReachSet inherent,
ReachSet alpha,
+ ExistPredSet preds,
String description
) {
this.allocSite = allocSite;
this.inherent = inherent;
this.alpha = alpha;
+ this.preds = preds;
this.description = description;
referencers = new HashSet<RefEdge>();
allocSite,
inherent,
alpha,
+ preds,
description );
}
}
- 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 );
}
return alpha.toStringEscapeNewline( hideSubsetReachability );
}
+ public String getPredString() {
+ return preds.toString();
+ }
+
public String toString() {
return "HRN"+getIDString();
}
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;
AllocSite allocSite,
ReachSet inherent,
ReachSet alpha,
+ ExistPredSet preds,
String description
) {
if( alpha == null ) {
alpha = inherent;
}
+
+ if( preds == null ) {
+ // TODO: do this right?
+ preds = new ExistPredSet().makeCanonical();
+ }
HeapRegionNode hrn = new HeapRegionNode( id,
isSingleObject,
allocSite,
inherent,
alpha,
+ preds,
description );
id2hrn.put( id, hrn );
return hrn;
tdNewEdge,
null,
false,
- betaY.intersection( betaHrn )
+ betaY.intersection( betaHrn ),
+ predsEmpty
);
addRefEdge( lnX, hrnHrn, edgeNew );
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
type, // type
null, // field name
false, // is initial param
- hrnNewest.getAlpha() // beta
+ hrnNewest.getAlpha(), // beta
+ predsEmpty // predicates
);
addRefEdge( lnX, hrnNewest, edgeNew );
as, // allocation site
null, // inherent reach
null, // current reach
+ predsEmpty, // predicates
strDesc // description
);
as, // allocation site
null, // inherent reach
null, // current reach
+ predsEmpty, // predicates
strDesc // description
);
}
as, // allocation site
null, // inherent reach
null, // current reach
+ predsEmpty, // predicates
strDesc // description
);
as.getType(), // type
as, // allocation site
null, // inherent reach
- null, // current reach
+ null, // current reach
+ predsEmpty, // predicates
strDesc // description
);
}
hrnSrcCaller.getAllocSite(),
toShadowTokens( this, hrnSrcCaller.getInherent() ),
toShadowTokens( this, hrnSrcCaller.getAlpha() ),
+ predsEmpty,
hrnSrcCaller.getDescription()
);
callerNodesCopiedToCallee.add( rsnCaller );
hrnCaller.getAllocSite(),
toShadowTokens( this, hrnCaller.getInherent() ),
toShadowTokens( this, hrnCaller.getAlpha() ),
+ predsEmpty,
hrnCaller.getDescription()
);
callerNodesCopiedToCallee.add( hrnCaller );
reCaller.getType(),
reCaller.getField(),
true, // clean?
- toShadowTokens( this, reCaller.getBeta() )
+ toShadowTokens( this, reCaller.getBeta() ),
+ predsEmpty
)
);
callerEdgesCopiedToCallee.add( reCaller );
null, // alloc site, shouldn't be used
toShadowTokens( this, hrnCallerAndOutContext.getAlpha() ), // inherent
toShadowTokens( this, hrnCallerAndOutContext.getAlpha() ), // alpha
+ predsEmpty,
"out-of-context"
);
edgeMightCross.getType(),
edgeMightCross.getField(),
true, // clean?
- toShadowTokens( this, edgeMightCross.getBeta() )
+ toShadowTokens( this, edgeMightCross.getBeta() ),
+ predsEmpty
)
);
}
hrnCallee.getAllocSite(),
unShadowTokens( rgCallee, hrnCallee.getInherent() ),
unShadowTokens( rgCallee, hrnCallee.getAlpha() ),
+ predsEmpty,
hrnCallee.getDescription()
);
}
HeapRegionNode hrnB = rgB.id2hrn.get( idA );
- if( !hrnA.equalsIncludingAlpha( hrnB ) ) {
+ if( !hrnA.equalsIncludingAlphaAndPreds( hrnB ) ) {
return false;
}
}
// 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;
}
}
}
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" );
" -> " +hrnChild.toString()+
"[label=\""+edge.toGraphEdgeString( hideSubsetReachability )+
"\",decorate];\n");
-
+
traverseHeapRegionNodes( hrnChild,
bw,
td,
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;
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 {
dst,
type,
field,
- isClean,
- beta );
+ isClean,
+ beta,
+ preds );
return copy;
}
}
- 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;
edgeLabel += "*clean*\\n";
}
- edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability );
+ edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability ) +
+ "\\n" + preds.toString();
return edgeLabel;
}
--- /dev/null
+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
--- /dev/null
+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 );
+ }
+}
projects / IRC.git / commitdiff