public static AllocSite factory( int allocationDepth,
FlatNew flatNew,
- String disjointId
+ String disjointId,
+ boolean markAsFlagged
) {
AllocSite out = new AllocSite( allocationDepth,
flatNew,
- disjointId );
+ disjointId,
+ markAsFlagged );
out = (AllocSite) Canonical.makeCanonical( out );
return out;
}
protected AllocSite( int allocationDepth,
FlatNew flatNew,
- String disjointId
+ String disjointId,
+ boolean markAsFlagged
) {
assert allocationDepth >= 1;
// 1) we have a non-null disjointID (a named flagged site)
// OR
// 2) the type is a class with Bamboo-parameter flags
+ // OR
+ // 3) a client wants to programmatically flag this site,
+ // such as the OoOJava method effects analysis
this.isFlagged = false;
if( disjointId != null ) {
flatNew.getType().getClassDesc().hasFlags()
) {
this.isFlagged = true;
+
+ } else if( markAsFlagged ) {
+ this.isFlagged = true;
}
ReachGraph rg = (ReachGraph) me.getValue();
rg.writeGraph( "COMPLETE"+d,
- true, // write labels (variables)
- true, // selectively hide intermediate temp vars
- true, // prune unreachable heap regions
- true, // hide subset reachability states
- true ); // hide edge taints
+ true, // write labels (variables)
+ true, // selectively hide intermediate temp vars
+ true, // prune unreachable heap regions
+ false, // hide reachability altogether
+ true, // hide subset reachability states
+ true, // hide predicates
+ false ); // hide edge taints
}
}
rg.writeGraph( "IHMPARTFOR"+d+"FROM"+fc2enclosing.get( fc )+fc,
true, // write labels (variables)
true, // selectively hide intermediate temp vars
+ true, // hide reachability altogether
true, // prune unreachable heap regions
- true, // hide subset reachability states
+ true, // hide subset reachability states
+ false, // hide predicates
true ); // hide edge taints
}
}
true, // write labels (variables)
true, // selectively hide intermediate temp vars
true, // prune unreachable heap regions
- true, // hide subset reachability states
- true ); // hide edge taints
+ false, // hide all reachability
+ true, // hide subset reachability states
+ true, // hide predicates
+ false );// hide edge taints
}
}
true, // write labels (variables)
true, // selectively hide intermediate temp vars
true, // prune unreachable heap regions
- true, // hide subset reachability states
- true ); // hide edge taints
+ false, // hide all reachability
+ true, // hide subset reachability states
+ false, // hide predicates
+ false); // hide edge taints
mapDescriptorToNumUpdates.put( d, n + 1 );
}
if( !mapFlatNewToAllocSite.containsKey( fnew ) ) {
AllocSite as = AllocSite.factory( allocationDepth,
fnew,
- fnew.getDisjointId()
+ fnew.getDisjointId(),
+ false
);
// the newest nodes are single objects
// create allocation site
AllocSite as = AllocSite.factory( allocationDepth,
flatNew,
- flatNew.getDisjointId()
+ flatNew.getDisjointId(),
+ false
);
for (int i = 0; i < allocationDepth; ++i) {
Integer id = generateUniqueHeapRegionNodeID();
if(prevNode==null){
// make a new reference between new summary node and source
- RefEdge edgeToSummary = new RefEdge(srcHRN, // source
+ RefEdge edgeToSummary = new RefEdge(srcHRN, // source
hrnSummary, // dest
typeDesc, // type
fd.getSymbol(), // field name
alpha, // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null,
+ null
);
rg.addRefEdge(srcHRN, hrnSummary, edgeToSummary);
typeDesc, // type
arrayElementFieldName, // field name
alpha, // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null,
+ null
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
typeDesc, // type
arrayElementFieldName, // field name
alpha, // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null,
+ null
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
prevNode=hrnSummary;
}else{
- HeapRegionNode hrnSummary=mapToExistingNode.get(typeDesc);
+ HeapRegionNode hrnSummary=mapToExistingNode.get(typeDesc);
if(prevNode.getReferenceTo(hrnSummary, typeDesc, arrayElementFieldName)==null){
RefEdge edgeToSummary = new RefEdge(prevNode, // source
hrnSummary, // dest
typeDesc, // type
arrayElementFieldName, // field name
alpha, // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null,
+ null
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
}
taskDesc.getParamType(idx), // type
null, // field name
hrnNewest.getAlpha(), // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null,
+ null
);
rg.addRefEdge(lnX, hrnNewest, edgeNew);
type, // type
fd.getSymbol(), // field name
hrnNewest.getAlpha(), // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null, null
);
rg.addRefEdge(srcHRN, hrnSummary, edgeToSummary);
fd.getType(), // type
fd.getSymbol(), // field name
srcHRN.getAlpha(), // beta
- ExistPredSet.factory(rg.predTrue) // predicates
+ ExistPredSet.factory(rg.predTrue), // predicates
+ null,
+ null
);
rg.addRefEdge(srcHRN, hrnDst, edgeToSummary);
graphName = graphName + fn;
}
rg.writeGraph( graphName,
- true, // write labels (variables)
- true, // selectively hide intermediate temp vars
- true, // prune unreachable heap regions
- true, // hide subset reachability states
- true );// hide edge taints
+ true, // write labels (variables)
+ true, // selectively hide intermediate temp vars
+ true, // prune unreachable heap regions
+ false, // hide reachability
+ true, // hide subset reachability states
+ true, // hide predicates
+ false );// hide edge taints
}
}
}
assert isSingleObject == hrn.isSingleObject();
-
- if( isFlagged != hrn.isFlagged ) {
- System.out.println( this.toStringDOT(true)+"\ndoesn't match\n"+hrn.toStringDOT(true) );
- //throw new Exception("flagged regions don't match");
- }
-
assert isFlagged == hrn.isFlagged();
assert isNewSummary == hrn.isNewSummary();
assert isOutOfContext == hrn.isOutOfContext();
return description;
}
- public String toStringDOT( boolean hideSubsetReach ) {
-
+ public String toStringDOT( boolean hideReach,
+ boolean hideSubsetReach,
+ boolean hidePreds ) {
String attributes = "";
if( isSingleObject ) {
typeStr = type.toPrettyString();
}
- return new String( "["+attributes+
- ",label=\"ID"+getIDString()+"\\n"+
- typeStr+"\\n"+
- description+"\\n"+
- alpha.toStringEscNewline( hideSubsetReach )+"\\n"+
- preds.toStringEscNewline()+"\"]"
- );
+ String s =
+ "["+attributes+
+ ",label=\"ID"+getIDString()+"\\n"+
+ typeStr+"\\n"+
+ description;
+
+ if( !hideReach ) {
+ s += "\\n"+alpha.toStringEscNewline( hideSubsetReach );
+ }
+
+ if( !hidePreds ) {
+ s += "\\n"+preds.toStringEscNewline();
+ }
+
+ return s+"\"]";
}
public String toString() {
tdNewEdge,
null,
Canonical.intersection( betaY, betaHrn ),
- predsTrue
+ predsTrue,
+ null,
+ null
);
addEdgeOrMergeWithExisting( edgeNew );
hrnX.getAlpha()
)
),
- predsTrue
+ predsTrue,
+ null,
+ null
);
addEdgeOrMergeWithExisting( edgeNew );
type, // type
null, // field name
hrnNewest.getAlpha(), // beta
- predsTrue // predicates
+ predsTrue, // predicates
+ null, null
);
addRefEdge( lnX, hrnNewest, edgeNew );
preds,
oocHrnIdOoc2callee
),
- preds
+ preds,
+ null, null
);
rg.addRefEdge( vnCallee,
preds,
oocHrnIdOoc2callee
),
- preds
+ preds,
+ null, null
);
rg.addRefEdge( hrnSrcCallee,
preds,
oocHrnIdOoc2callee
),
- preds
+ preds,
+ null, null
)
);
rg.writeGraph( debugGraphPrefix+"calleeview",
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
- resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
private static boolean resolveMethodDebugDOTwriteLabels = true;
private static boolean resolveMethodDebugDOTselectTemps = true;
private static boolean resolveMethodDebugDOTpruneGarbage = true;
+ private static boolean resolveMethodDebugDOThideReach = true;
private static boolean resolveMethodDebugDOThideSubsetReach = true;
+ private static boolean resolveMethodDebugDOThidePreds = true;
private static boolean resolveMethodDebugDOThideEdgeTaints = true;
static String debugGraphPrefix;
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
writeGraph( debugGraphPrefix+"caller00In",
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints,
callerNodeIDsCopiedToCallee );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
reCallee.getField(),
toCallerContext( reCallee.getBeta(),
calleeStatesSatisfied ),
- preds
+ preds,
+ null, null
);
ChangeSet cs = ChangeSet.factory();
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
+ resolveMethodDebugDOThideReach,
resolveMethodDebugDOThideSubsetReach,
+ resolveMethodDebugDOThidePreds,
resolveMethodDebugDOThideEdgeTaints );
}
}
// the default signature for quick-and-dirty debugging
public void writeGraph( String graphName ) {
writeGraph( graphName,
- true, // write labels
- true, // label select
- true, // prune garbage
- true, // hide subset reachability
- true, // hide edge taints
- null // in-context boundary
+ true, // write labels
+ true, // label select
+ true, // prune garbage
+ false, // hide reachability
+ true, // hide subset reachability
+ true, // hide predicates
+ true, // hide edge taints
+ null // in-context boundary
);
}
boolean writeLabels,
boolean labelSelect,
boolean pruneGarbage,
+ boolean hideReachability,
boolean hideSubsetReachability,
+ boolean hidePredicates,
boolean hideEdgeTaints
) {
writeGraph( graphName,
writeLabels,
labelSelect,
pruneGarbage,
+ hideReachability,
hideSubsetReachability,
+ hidePredicates,
hideEdgeTaints,
null );
}
boolean writeLabels,
boolean labelSelect,
boolean pruneGarbage,
+ boolean hideReachability,
boolean hideSubsetReachability,
+ boolean hidePredicates,
boolean hideEdgeTaints,
Set<Integer> callerNodeIDsCopiedToCallee
) {
HeapRegionNode hrn = (HeapRegionNode) me.getValue();
if( callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) {
- bw.write( " "+hrn.toString()+
- hrn.toStringDOT( hideSubsetReachability )+
- ";\n" );
-
+ bw.write( " "+
+ hrn.toString()+
+ hrn.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates )+
+ ";\n" );
}
}
bw,
null,
visited,
+ hideReachability,
hideSubsetReachability,
+ hidePredicates,
hideEdgeTaints,
callerNodeIDsCopiedToCallee );
}
bw,
null,
visited,
+ hideReachability,
hideSubsetReachability,
+ hidePredicates,
hideEdgeTaints,
callerNodeIDsCopiedToCallee );
}
bw.write( " "+vn.toString()+
" -> "+hrn.toString()+
- edge.toStringDOT( hideSubsetReachability, "" )+
+ edge.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates,
+ hideEdgeTaints,
+ "" )+
";\n" );
}
}
}
}
- protected void traverseHeapRegionNodes( HeapRegionNode hrn,
- BufferedWriter bw,
- TempDescriptor td,
- Set<HeapRegionNode> visited,
- boolean hideSubsetReachability,
- boolean hideEdgeTaints,
- Set<Integer> callerNodeIDsCopiedToCallee
- ) throws java.io.IOException {
+ protected void
+ traverseHeapRegionNodes( HeapRegionNode hrn,
+ BufferedWriter bw,
+ TempDescriptor td,
+ Set<HeapRegionNode> visited,
+ boolean hideReachability,
+ boolean hideSubsetReachability,
+ boolean hidePredicates,
+ boolean hideEdgeTaints,
+ Set<Integer> callerNodeIDsCopiedToCallee
+ ) throws java.io.IOException {
if( visited.contains( hrn ) ) {
return;
if( callerNodeIDsCopiedToCallee == null ||
!callerNodeIDsCopiedToCallee.contains( hrn.getID() )
) {
- bw.write( " "+hrn.toString()+
- hrn.toStringDOT( hideSubsetReachability )+
+ bw.write( " "+
+ hrn.toString()+
+ hrn.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates )+
";\n" );
}
) {
bw.write( " "+hrn.toString()+
" -> "+hrnChild.toString()+
- edge.toStringDOT( hideSubsetReachability, ",color=blue" )+
+ edge.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates,
+ hideEdgeTaints,
+ ",color=blue" )+
";\n");
} else if( !callerNodeIDsCopiedToCallee.contains( hrnSrc.getID() ) &&
callerNodeIDsCopiedToCallee.contains( edge.getDst().getID() )
) {
bw.write( " "+hrn.toString()+
" -> "+hrnChild.toString()+
- edge.toStringDOT( hideSubsetReachability, ",color=blue,style=dashed" )+
+ edge.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates,
+ hideEdgeTaints,
+ ",color=blue,style=dashed" )+
";\n");
} else {
bw.write( " "+hrn.toString()+
" -> "+hrnChild.toString()+
- edge.toStringDOT( hideSubsetReachability, "" )+
+ edge.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates,
+ hideEdgeTaints,
+ "" )+
";\n");
}
} else {
bw.write( " "+hrn.toString()+
" -> "+hrnChild.toString()+
- edge.toStringDOT( hideSubsetReachability, "" )+
+ edge.toStringDOT( hideReachability,
+ hideSubsetReachability,
+ hidePredicates,
+ hideEdgeTaints,
+ "" )+
";\n");
}
bw,
td,
visited,
+ hideReachability,
hideSubsetReachability,
+ hidePredicates,
hideEdgeTaints,
callerNodeIDsCopiedToCallee );
}
}
public String toString( boolean hideSubsetReachability ) {
+
+ ReachSet toPrint = this;
+
+ if( hideSubsetReachability ) {
+ // make a new reach set with subset states removed
+ toPrint = ReachSet.factory();
+
+ Iterator<ReachState> i = this.iterator();
+ while( i.hasNext() ) {
+ ReachState state = i.next();
+
+ if( containsStrictSuperSet( state ) ) {
+ continue;
+ }
+
+ toPrint = Canonical.add( toPrint, state );
+ }
+ }
+
String s = "[";
- Iterator<ReachState> i = this.iterator();
+ Iterator<ReachState> i = toPrint.iterator();
while( i.hasNext() ) {
ReachState state = i.next();
- // skip this if there is a superset already
- if( hideSubsetReachability &&
- containsStrictSuperSet( state ) ) {
- continue;
- }
-
s += state;
if( i.hasNext() ) {
s += "\n";
// do not factor into edge comparisons
protected ExistPredSet preds;
+ // taint sets indicate which heap roots have
+ // tainted this edge-->meaning which heap roots
+ // code must have had access to in order to
+ // read or write through this edge
+ protected TaintSet paramTaints;
+ protected TaintSet rblockTaints;
+
public RefEdge( RefSrcNode src,
HeapRegionNode dst,
TypeDescriptor type,
String field,
ReachSet beta,
- ExistPredSet preds ) {
+ ExistPredSet preds,
+ TaintSet paramTaints,
+ TaintSet rblockTaints ) {
+
+ assert src != null;
+ assert dst != null;
assert type != null;
this.src = src;
if( preds != null ) {
this.preds = preds;
} else {
- // TODO: do this right?
this.preds = ExistPredSet.factory();
}
// when edges are not undergoing an operation that
// is changing beta info, betaNew is always empty
betaNew = ReachSet.factory();
+
+ if( paramTaints != null ) {
+ this.paramTaints = paramTaints;
+ } else {
+ this.paramTaints = TaintSet.factory();
+ }
+
+ if( rblockTaints != null ) {
+ this.rblockTaints = rblockTaints;
+ } else {
+ this.rblockTaints = TaintSet.factory();
+ }
}
type,
field,
beta,
- preds );
+ preds,
+ paramTaints,
+ rblockTaints );
return copy;
}
// 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 ) {
+ // AND EDGE TAINTS!
+ public boolean equalsIncludingBetaPredsTaints( RefEdge edge ) {
return equals( edge ) &&
beta.equals( edge.beta ) &&
- preds.equals( edge.preds );
+ preds.equals( edge.preds ) &&
+ paramTaints.equals( edge.paramTaints ) &&
+ rblockTaints.equals( edge.rblockTaints );
}
public boolean equalsPreds( RefEdge edge ) {
}
+ // this method SPECIFICALLY does not use the
+ // beta/preds/taints in the hash code--it uses
+ // the same fields as normal equals. Again,
+ // there are two meanings of equality for edges,
+ // one is "this edge is the same edge object" like when
+ // deciding if an edge is already in a set, which
+ // is represented by this hashcode. The other
+ // meaning is "this edge equals an edge from another
+ // graph that is abstractly the same edge"
public int hashCode() {
int hash = 0;
}
- public String toStringDOT( boolean hideSubsetReach,
+ public TaintSet getParamTaints() {
+ return paramTaints;
+ }
+
+ public TaintSet getRblockTaints() {
+ return rblockTaints;
+ }
+
+
+
+ public String toStringDOT( boolean hideReach,
+ boolean hideSubsetReach,
+ boolean hidePreds,
+ boolean hideEdgeTaints,
String otherAttributes ) {
- return new String( "[label=\""+
- type.toPrettyString()+"\\n"+
- field+"\\n"+
- beta.toStringEscNewline( hideSubsetReach )+"\\n"+
- preds.toStringEscNewline()+"\",decorate"+
- otherAttributes+"]"
- );
+ String s =
+ "[label=\""+
+ type.toPrettyString()+"\\n"+
+ field;
+ if( !hideReach ) {
+ s += "\\n"+beta.toStringEscNewline( hideSubsetReach );
+ }
+
+ if( !hidePreds ) {
+ s += "\\n"+preds.toStringEscNewline();
+ }
+
+ if( !hideEdgeTaints ) {
+ if( !paramTaints.isEmpty() ) {
+ s += "\\npt: "+paramTaints.toString();
+ }
+
+ if( !rblockTaints.isEmpty() ) {
+ s += "\\nrt: "+rblockTaints.toString();
+ }
+ }
+
+ return s+"\",decorate"+otherAttributes+"]";
}
public String toString() {
BUILDSCRIPT=~/research/Robust/src/buildscript
-#DEBUGFLAGS= -disjoint-debug-callsite Bar addSomething 1
-#DEBUGFLAGS= -disjoint-debug-callsite Foo main 1
-#DEBUGFLAGS= -disjoint-debug-callsite main analysisEntryMethod 1
-DEBUGFLAGS= -disjoint-debug-callsite addSomething main 100
-#DEBUGFLAGS= -disjoint-debug-callsite addBar addSomething 1
-#DEBUGFLAGS= -disjoint-debug-callsite Bar addBar 1
-
BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 2 -disjoint-write-dots final -disjoint-write-ihms -disjoint-alias-file aliases.txt normal -enable-assertions
all: $(PROGRAM).bin
static public void main( String[] args ) {
Foo a = disjoint A new Foo();
Foo b = disjoint B new Foo();
+ f0( a, b );
+ }
+
+ static public void f0( Foo a, Foo b ) {
a.f = b;
- f1( b );
+ f1( b );
}
static public void f1( Foo c ) {
projects / IRC.git / commitdiff