return out;
}
+
+
+ public static ReachState makePredsTrue( ReachState rs ) {
+ assert rs != null;
+ assert rs.isCanonical();
+
+ // ops require two canonicals, in this case always supply
+ // the empty reach state as the second, it's never used,
+ // but makes the hashing happy
+ CanonicalOp op =
+ new CanonicalOp( CanonicalOp.REACHSTATE_MAKEPREDSTRUE,
+ rs,
+ ReachState.factory() );
+
+ Canonical result = op2result.get( op );
+ if( result != null ) {
+ return (ReachState) result;
+ }
+
+ // otherwise, no cached result...
+ ReachState out = new ReachState();
+
+ // just remake state with the true predicate attached
+ out.reachTuples.addAll( rs.reachTuples );
+ out.preds = ExistPredSet.factory( ExistPred.factory() );
+
+ out = (ReachState) makeCanonical( out );
+ op2result.put( op, out );
+ return out;
+ }
+
+
+ public static ReachSet makePredsTrue( ReachSet rs ) {
+ assert rs != null;
+ assert rs.isCanonical();
+
+ // ops require two canonicals, in this case always supply
+ // the empty reach set as the second, it's never used,
+ // but makes the hashing happy
+ CanonicalOp op =
+ new CanonicalOp( CanonicalOp.REACHSET_MAKEPREDSTRUE,
+ rs,
+ ReachSet.factory() );
+
+ Canonical result = op2result.get( op );
+ if( result != null ) {
+ return (ReachSet) result;
+ }
+
+ // otherwise, no cached result...
+ ReachSet out = ReachSet.factory();
+ Iterator<ReachState> itr = rs.iterator();
+ while( itr.hasNext() ) {
+ ReachState state = itr.next();
+ out = Canonical.add( out,
+ Canonical.makePredsTrue( state )
+ );
+ }
+
+ out = (ReachSet) makeCanonical( out );
+ op2result.put( op, out );
+ return out;
+ }
+
}
rg.writeGraph( "IHMPARTFOR"+d+"FROM"+fc,
true, // write labels (variables)
- false, // selectively hide intermediate temp vars
- false, // prune unreachable heap regions
+ true, // selectively hide intermediate temp vars
+ true, // prune unreachable heap regions
false, // hide subset reachability states
true ); // hide edge taints
}
rg.writeGraph( d+"COMPLETE"+String.format( "%05d", n ),
true, // write labels (variables)
true, // selectively hide intermediate temp vars
- false, // prune unreachable heap regions
+ true, // prune unreachable heap regions
false, // hide subset reachability states
true ); // hide edge taints
}
-private HeapRegionNode createMultiDeimensionalArrayHRN(ReachGraph rg, AllocSite alloc, HeapRegionNode srcHRN, FieldDescriptor fd, Hashtable<HeapRegionNode, HeapRegionNode> map, Hashtable<TypeDescriptor, HeapRegionNode> mapToExistingNode ){
+ private HeapRegionNode createMultiDeimensionalArrayHRN(ReachGraph rg, AllocSite alloc, HeapRegionNode srcHRN, FieldDescriptor fd, Hashtable<HeapRegionNode, HeapRegionNode> map, Hashtable<TypeDescriptor, HeapRegionNode> mapToExistingNode, ReachSet alpha ){
int dimCount=fd.getType().getArrayCount();
HeapRegionNode prevNode=null;
as.getType(), // type
as, // allocation site
null, // inherent reach
- null, // current reach
- ExistPredSet.factory(), // predicates
+ alpha, // current reach
+ ExistPredSet.factory(rg.predTrue), // predicates
tempDesc.toString() // description
);
rg.id2hrn.put(as.getSummary(),hrnSummary);
hrnSummary, // dest
typeDesc, // type
fd.getSymbol(), // field name
- srcHRN.getAlpha(), // beta
+ alpha, // beta
ExistPredSet.factory(rg.predTrue) // predicates
);
hrnSummary, // dest
typeDesc, // type
arrayElementFieldName, // field name
- srcHRN.getAlpha(), // beta
+ alpha, // beta
ExistPredSet.factory(rg.predTrue) // predicates
);
typeDesc, // type
as, // allocation site
null, // inherent reach
- null, // current reach
- ExistPredSet.factory(), // predicates
+ alpha, // current reach
+ ExistPredSet.factory(rg.predTrue), // predicates
tempDesc.toString() // description
);
rg.id2hrn.put(as.getSummary(),hrnSummary);
hrnSummary, // dest
typeDesc, // type
arrayElementFieldName, // field name
- null, // beta
+ alpha, // beta
ExistPredSet.factory(rg.predTrue) // predicates
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
hrnSummary, // dest
typeDesc, // type
arrayElementFieldName, // field name
- null, // beta
+ alpha, // beta
ExistPredSet.factory(rg.predTrue) // predicates
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
HeapRegionNode hrnSummary;
if(allocType.isArray() && allocType.getArrayCount()>0){
- hrnSummary=createMultiDeimensionalArrayHRN(rg,allocSite,srcHRN,fd,mapToFirstDimensionArrayNode,mapTypeToExistingSummaryNode);
+ hrnSummary=createMultiDeimensionalArrayHRN(rg,allocSite,srcHRN,fd,mapToFirstDimensionArrayNode,mapTypeToExistingSummaryNode,hrnNewest.getAlpha());
}else{
hrnSummary =
rg.createNewHeapRegionNode(allocSite.getSummary(), // id or null to generate a new one
allocSite.getType(), // type
allocSite, // allocation site
null, // inherent reach
- srcHRN.getAlpha(), // current reach
- ExistPredSet.factory(), // predicates
+ hrnNewest.getAlpha(), // current reach
+ ExistPredSet.factory(rg.predTrue), // predicates
strDesc // description
);
rg.id2hrn.put(allocSite.getSummary(),hrnSummary);
hrnSummary, // dest
type, // type
fd.getSymbol(), // field name
- srcHRN.getAlpha(), // beta
+ hrnNewest.getAlpha(), // beta
ExistPredSet.factory(rg.predTrue) // predicates
);
rg.writeGraph( graphName,
true, // write labels (variables)
true, // selectively hide intermediate temp vars
- false, // prune unreachable heap regions
+ true, // prune unreachable heap regions
false, // hide subset reachability states
true );// hide edge taints
}
if( inherent == null ) {
if( markForAnalysis ) {
inherent =
- ReachSet.factory(
- ReachState.factory(
- ReachTuple.factory( id,
- !isSingleObject,
- ReachTuple.ARITY_ONE,
- false // out-of-context
- )
- )
- );
+ Canonical.makePredsTrue(
+ ReachSet.factory(
+ ReachState.factory(
+ ReachTuple.factory( id,
+ !isSingleObject,
+ ReachTuple.ARITY_ONE,
+ false // out-of-context
+ )
+ )
+ )
+ );
} else {
inherent = rsetWithEmptyState;
}
hrnY.getType()
);
- RefEdge edgeNew = new RefEdge( hrnX,
- hrnY,
- tdNewEdge,
- f.getSymbol(),
- Canonical.pruneBy( edgeY.getBeta(),
- hrnX.getAlpha()
- ),
- predsTrue
- );
+ RefEdge edgeNew =
+ new RefEdge( hrnX,
+ hrnY,
+ tdNewEdge,
+ f.getSymbol(),
+ Canonical.makePredsTrue(
+ Canonical.pruneBy( edgeY.getBeta(),
+ hrnX.getAlpha()
+ )
+ ),
+ predsTrue
+ );
addEdgeOrMergeWithExisting( edgeNew );
}
if( writeDebugDOTs ) {
- rg.writeGraph( "calleeview",
+ debugGraphPrefix = String.format( "call%02d", debugCallSiteVisits );
+ rg.writeGraph( debugGraphPrefix+"calleeview",
resolveMethodDebugDOTwriteLabels,
resolveMethodDebugDOTselectTemps,
resolveMethodDebugDOTpruneGarbage,
// useful since many graphs writes in the method call debug code
private static boolean resolveMethodDebugDOTwriteLabels = true;
private static boolean resolveMethodDebugDOTselectTemps = true;
- private static boolean resolveMethodDebugDOTpruneGarbage = false;
+ private static boolean resolveMethodDebugDOTpruneGarbage = true;
private static boolean resolveMethodDebugDOThideSubsetReach = false;
private static boolean resolveMethodDebugDOThideEdgeTaints = true;