protected Hashtable<Descriptor, ReachGraph>
mapDescriptorToInitialContext;
+ // mapping of current partial results for a given node. Note that
+ // to reanalyze a method we discard all partial results because a
+ // null reach graph indicates the node needs to be visited on the
+ // way to the fixed point.
+ // The reason for a persistent mapping is so after the analysis we
+ // can ask for the graph of any node at the fixed point, but this
+ // option is only enabled with a compiler flag.
+ protected Hashtable<FlatNode, ReachGraph> mapFlatNodeToReachGraphPersist;
+ protected Hashtable<FlatNode, ReachGraph> mapFlatNodeToReachGraph;
+
+
// make the result for back edges analysis-wide STRICTLY
// MONOTONIC as well, but notice we use FlatNode as the
// key for this map: in case we want to consider other
mapDescriptorToInitialContext =
new Hashtable<Descriptor, ReachGraph>();
+ mapFlatNodeToReachGraphPersist =
+ new Hashtable<FlatNode, ReachGraph>();
+
mapBackEdgeToMonotone =
new Hashtable<FlatNode, ReachGraph>();
writeFinalGraphs();
}
- if( state.DISJOINTWRITEIHMS && !suppressOutput ) {
+ if( state.DISJOINTWRITEIHMS ) {
writeFinalIHMs();
}
- if( state.DISJOINTWRITEINITCONTEXTS && !suppressOutput ) {
+ if( state.DISJOINTWRITEINITCONTEXTS ) {
writeInitialContexts();
}
+ if( state.DISJOINT_WRITE_ALL_NODE_FINAL_GRAPHS ) {
+ writeFinalGraphsForEveryNode();
+ }
+
if( state.DISJOINTALIASFILE != null && !suppressOutput ) {
if( state.TASK ) {
writeAllSharing(state.DISJOINTALIASFILE, treport, justtime, state.DISJOINTALIASTAB, state.lines);
flatNodesToVisitQ.add(fm);
}
- // mapping of current partial results
- Hashtable<FlatNode, ReachGraph> mapFlatNodeToReachGraph =
+ // start a new mapping of partial results
+ mapFlatNodeToReachGraph =
new Hashtable<FlatNode, ReachGraph>();
// the set of return nodes partial results that will be combined as
if( !rg.equals(rgPrev) ) {
mapFlatNodeToReachGraph.put(fn, rg);
+ // we don't necessarily want to keep the reach graph for every
+ // node in the program unless a client or the user wants it
+ if( state.DISJOINT_WRITE_ALL_NODE_FINAL_GRAPHS ) {
+ mapFlatNodeToReachGraphPersist.put(fn, rg);
+ }
+
for( int i = 0; i < pm.numNext(fn); i++ ) {
FlatNode nn = pm.getNext(fn, i);
// states after the flat method returns
ReachGraph completeGraph = new ReachGraph();
+ if( setReturns.isEmpty() ) {
+ System.out.println( "d = "+d );
+
+ }
assert !setReturns.isEmpty();
Iterator retItr = setReturns.iterator();
while( retItr.hasNext() ) {
if( doEffectsAnalysis && fmContaining != fmAnalysisEntry ) {
if(rblockRel.isPotentialStallSite(fn)) {
// x gets status of y
-// if(!rg.isAccessible(rhs)){
if(!accessible.isAccessible(fn, rhs)) {
rg.makeInaccessible(lhs);
}
if( doEffectsAnalysis && fmContaining != fmAnalysisEntry ) {
if(rblockRel.isPotentialStallSite(fn)) {
// x gets status of y
-// if(!rg.isAccessible(rhs)){
if(!accessible.isAccessible(fn,rhs)) {
rg.makeInaccessible(lhs);
}
if(rblockRel.isPotentialStallSite(fn)) {
// x=y.f, stall y if not accessible
// contributes read effects on stall site of y
-// if(!rg.isAccessible(rhs)) {
if(!accessible.isAccessible(fn,rhs)) {
rg.taintStallSite(fn, rhs);
}
if(rblockRel.isPotentialStallSite(fn)) {
// x.y=f , stall x and y if they are not accessible
// also contribute write effects on stall site of x
-// if(!rg.isAccessible(lhs)) {
if(!accessible.isAccessible(fn,lhs)) {
rg.taintStallSite(fn, lhs);
}
-// if(!rg.isAccessible(rhs)) {
if(!accessible.isAccessible(fn,rhs)) {
rg.taintStallSite(fn, rhs);
}
// x=y.f, stall y if not accessible
// contributes read effects on stall site of y
// after this, x and y are accessbile.
-// if(!rg.isAccessible(rhs)) {
if(!accessible.isAccessible(fn,rhs)) {
rg.taintStallSite(fn, rhs);
}
if(rblockRel.isPotentialStallSite(fn)) {
// x.y=f , stall x and y if they are not accessible
// also contribute write effects on stall site of x
-// if(!rg.isAccessible(lhs)) {
if(!accessible.isAccessible(fn,lhs)) {
rg.taintStallSite(fn, lhs);
}
-// if(!rg.isAccessible(rhs)) {
if(!accessible.isAccessible(fn,rhs)) {
rg.taintStallSite(fn, rhs);
}
FlatMethod fmCallee = state.getMethodFlat(mdCallee);
+
+
+
+
+
+
// the transformation for a call site should update the
// current heap abstraction with any effects from the callee,
// before transfer, do effects analysis support
if( doEffectsAnalysis && fmContaining != fmAnalysisEntry ) {
-// if(!rg.isAccessible(rhs)){
if(!accessible.isAccessible(fn,rhs)) {
rg.makeInaccessible(ReachGraph.tdReturn);
}
}
}
+ private void writeFinalGraphsForEveryNode() {
+ Set entrySet = mapFlatNodeToReachGraphPersist.entrySet();
+ Iterator itr = entrySet.iterator();
+ while( itr.hasNext() ) {
+ Map.Entry me = (Map.Entry) itr.next();
+ FlatNode fn = (FlatNode) me.getKey();
+ ReachGraph rg = (ReachGraph) me.getValue();
+
+ rg.writeGraph("NODEFINAL"+fn,
+ true, // write labels (variables)
+ false, // selectively hide intermediate temp vars
+ true, // prune unreachable heap regions
+ true, // hide all reachability
+ true, // hide subset reachability states
+ true, // hide predicates
+ true); // hide edge taints
+ }
+ }
+
protected ReachGraph getPartial(Descriptor d) {
return mapDescriptorToCompleteReachGraph.get(d);
return rgAtEnter.canPointTo( x );
}
-
-
- public Set<Alloc> canPointToAfter( TempDescriptor x,
- FlatNode programPoint ) {
-
- ReachGraph rgAtExit = fn2rgAtExit.get( programPoint );
- if( rgAtExit == null ) {
- return null;
- }
-
- return rgAtExit.canPointTo( x );
- }
public Hashtable< Alloc, Set<Alloc> > canPointToAt( TempDescriptor x,
return rgAtEnter.canPointTo( x, arrayElementFieldName, x.getType().dereference() );
}
+
+
+ public Set<Alloc> canPointToAfter( TempDescriptor x,
+ FlatNode programPoint ) {
+
+ ReachGraph rgAtExit = fn2rgAtExit.get( programPoint );
+
+ if( rgAtExit == null ) {
+ return null;
+ }
+
+ return rgAtExit.canPointTo( x );
+ }
+
+
+ public Hashtable< Alloc, Set<Alloc> > canPointToAfter( TempDescriptor x,
+ FieldDescriptor f,
+ FlatNode programPoint ) {
+
+ ReachGraph rgAtExit = fn2rgAtExit.get( programPoint );
+ if( rgAtExit == null ) {
+ return null;
+ }
+
+ return rgAtExit.canPointTo( x, f.getSymbol(), f.getType() );
+ }
+
+
+ public Hashtable< Alloc, Set<Alloc> > canPointToAfterElement( TempDescriptor x,
+ FlatNode programPoint ) {
+
+ ReachGraph rgAtExit = fn2rgAtExit.get( programPoint );
+ if( rgAtExit == null ) {
+ return null;
+ }
+
+ assert x.getType() != null;
+ assert x.getType().isArray();
+
+ return rgAtExit.canPointTo( x, arrayElementFieldName, x.getType().dereference() );
+ }
}
// predicate is satisfied, return the predicate set of the
// element that satisfied it, or null for false
public ExistPredSet isSatisfiedBy(ReachGraph rg,
- Set<Integer> calleeReachableNodes
+ Set<Integer> calleeReachableNodes,
+ Set<RefSrcNode> callerSrcMatches
) {
if( predType == TYPE_TRUE ) {
return ExistPredSet.factory(ExistPred.factory() );
}
if( predType == TYPE_NODE ) {
-
// first find node
HeapRegionNode hrn = rg.id2hrn.get(n_hrnID);
if( hrn == null ) {
// when the state and taint are null we're done!
if( ne_state == null &&
e_taint == null ) {
+
+ if( callerSrcMatches != null ) {
+ callerSrcMatches.add( rsn );
+ }
+
return edge.getPreds();
+
} else if( ne_state != null ) {
// otherwise look for state too
} else {
// it was here, return the predicates on the taint!!
+ if( callerSrcMatches != null ) {
+ callerSrcMatches.add( rsn );
+ }
+
return tCaller.getPreds();
}
}
+ // if this pred is an edge type pred, then given
+ // a reach graph, find the element of the graph that
+ // may exist and represents the source of the edge
+ public RefSrcNode getEdgeSource( ReachGraph rg ) {
+ if( predType != TYPE_EDGE ) {
+ return null;
+ }
+
+ if( e_tdSrc != null ) {
+ // variable node is the source, look for it in the graph
+ return rg.getVariableNodeNoMutation( e_tdSrc );
+ }
+
+ // otherwise a heap region node is the source, look for it
+ assert e_hrnDstID != null;
+ return rg.id2hrn.get( e_hrnDstID );
+ }
+
+
+
public boolean equalsSpecific(Object o) {
if( o == null ) {
return false;
// only consider the subest of the caller elements that
// are reachable by callee when testing predicates
public ExistPredSet isSatisfiedBy(ReachGraph rg,
- Set<Integer> calleeReachableNodes
+ Set<Integer> calleeReachableNodes,
+ Set<RefSrcNode> callerSrcMatches
) {
ExistPredSet predsOut = null;
while( predItr.hasNext() ) {
ExistPredSet predsFromSatisfier =
predItr.next().isSatisfiedBy(rg,
- calleeReachableNodes);
+ calleeReachableNodes,
+ callerSrcMatches);
if( predsFromSatisfier != null ) {
if( predsOut == null ) {
}
+ // this method returns the source node of any
+ // edge predicates in the set for the given graph
+ public Set<RefSrcNode> getEdgeSources( ReachGraph rg ) {
+ Set<RefSrcNode> out = new HashSet<RefSrcNode>();
+
+ for( ExistPred pred: preds ) {
+ RefSrcNode rsn = pred.getEdgeSource( rg );
+ if( rsn != null ) {
+ out.add( rsn );
+ }
+ }
+
+ return out;
+ }
+
+
+
public boolean isEmpty() {
return preds.isEmpty();
}
public Set<Alloc> canPointToAt( TempDescriptor x,
FlatNode programPoint );
- public Set<Alloc> canPointToAfter( TempDescriptor x,
- FlatNode programPoint );
-
public Hashtable< Alloc, Set<Alloc> > canPointToAt( TempDescriptor x,
FieldDescriptor f,
FlatNode programPoint );
public Hashtable< Alloc, Set<Alloc> > canPointToAtElement( TempDescriptor x, // x[i]
FlatNode programPoint );
+
+ public Set<Alloc> canPointToAfter( TempDescriptor x,
+ FlatNode programPoint );
+
+ public Hashtable< Alloc, Set<Alloc> > canPointToAfter( TempDescriptor x,
+ FieldDescriptor f,
+ FlatNode programPoint );
+
+ public Hashtable< Alloc, Set<Alloc> > canPointToAfterElement( TempDescriptor x, // x[i]
+ FlatNode programPoint );
}
private static boolean resolveMethodDebugDOTpruneGarbage = true;
private static boolean resolveMethodDebugDOThideReach = true;
private static boolean resolveMethodDebugDOThideSubsetReach = true;
- private static boolean resolveMethodDebugDOThidePreds = true;
- private static boolean resolveMethodDebugDOThideEdgeTaints = false;
+ private static boolean resolveMethodDebugDOThidePreds = false;
+ private static boolean resolveMethodDebugDOThideEdgeTaints = true;
static String debugGraphPrefix;
static int debugCallSiteVisitCounter;
new Hashtable< RefEdge, Set<RefSrcNode> >();
+
Iterator meItr = rgCallee.id2hrn.entrySet().iterator();
while( meItr.hasNext() ) {
Map.Entry me = (Map.Entry)meItr.next();
// should have, and it is inefficient to find this again later
ExistPredSet predsIfSatis =
hrnCallee.getPreds().isSatisfiedBy(this,
- callerNodeIDsCopiedToCallee
- );
+ callerNodeIDsCopiedToCallee,
+ null);
if( predsIfSatis != null ) {
calleeNodesSatisfied.put(hrnCallee, predsIfSatis);
predsIfSatis =
stateCallee.getPreds().isSatisfiedBy(this,
- callerNodeIDsCopiedToCallee
- );
+ callerNodeIDsCopiedToCallee,
+ null);
if( predsIfSatis != null ) {
Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied =
predsIfSatis =
hrnSrcCallee.getPreds().isSatisfiedBy(this,
- callerNodeIDsCopiedToCallee
- );
+ callerNodeIDsCopiedToCallee,
+ null);
if( predsIfSatis != null ) {
calleeNodesSatisfied.put(hrnSrcCallee, predsIfSatis);
} else {
} else {
// hrnSrcCallee is out-of-context
-
assert !calleeEdges2oocCallerSrcMatches.containsKey(reCallee);
Set<RefSrcNode> rsnCallers = new HashSet<RefSrcNode>();
- // is the target node in the caller?
- HeapRegionNode hrnDstCaller = this.id2hrn.get(hrnCallee.getID() );
- if( hrnDstCaller == null ) {
- continue;
- }
-
- Iterator<RefEdge> reDstItr = hrnDstCaller.iteratorToReferencers();
- while( reDstItr.hasNext() ) {
- // the edge and field (either possibly null) must match
- RefEdge reCaller = reDstItr.next();
-
- if( !reCaller.typeEquals(reCallee.getType() ) ||
- !reCaller.fieldEquals(reCallee.getField() )
- ) {
- continue;
- }
-
- RefSrcNode rsnCaller = reCaller.getSrc();
- if( rsnCaller instanceof VariableNode ) {
-
- // a variable node matches an OOC region with null type
- if( hrnSrcCallee.getType() != null ) {
- continue;
- }
-
- } else {
- // otherwise types should match
- HeapRegionNode hrnCallerSrc = (HeapRegionNode) rsnCaller;
- if( hrnSrcCallee.getType() == null ) {
- if( hrnCallerSrc.getType() != null ) {
- continue;
- }
- } else {
- if( !hrnSrcCallee.getType().equals(hrnCallerSrc.getType() ) ) {
- continue;
- }
- }
- }
-
- rsnCallers.add(rsnCaller);
- matchedOutOfContext = true;
- }
+ // use the isSatisfiedBy with a non-null callers set to capture
+ // nodes in the caller that match the predicates
+ reCallee.getPreds().isSatisfiedBy( this,
+ callerNodeIDsCopiedToCallee,
+ rsnCallers );
if( !rsnCallers.isEmpty() ) {
+ matchedOutOfContext = true;
calleeEdges2oocCallerSrcMatches.put(reCallee, rsnCallers);
}
}
predsIfSatis =
reCallee.getPreds().isSatisfiedBy(this,
- callerNodeIDsCopiedToCallee
- );
+ callerNodeIDsCopiedToCallee,
+ null);
+
if( predsIfSatis != null ) {
calleeEdgesSatisfied.put(reCallee, predsIfSatis);
predsIfSatis =
stateCallee.getPreds().isSatisfiedBy(this,
- callerNodeIDsCopiedToCallee
- );
+ callerNodeIDsCopiedToCallee,
+ null);
if( predsIfSatis != null ) {
Hashtable<ReachState, ExistPredSet> calleeStatesSatisfied =
predsIfSatis =
tCallee.getPreds().isSatisfiedBy(this,
- callerNodeIDsCopiedToCallee
- );
+ callerNodeIDsCopiedToCallee,
+ null);
if( predsIfSatis != null ) {
Hashtable<Taint, ExistPredSet> calleeTaintsSatisfied =
//System.out.println( "*** Asking if A is no smaller than B ***" );
-
Iterator iA = rgA.id2hrn.entrySet().iterator();
while( iA.hasNext() ) {
Map.Entry meA = (Map.Entry)iA.next();
System.out.println(" regions smaller");
return false;
}
-
- //HeapRegionNode hrnB = rgB.id2hrn.get( idA );
- /* NOT EQUALS, NO SMALLER THAN!
- if( !hrnA.equalsIncludingAlphaAndPreds( hrnB ) ) {
- System.out.println( " regions smaller" );
- return false;
- }
- */
}
// this works just fine, no smaller than
System.out.println(" edges smaller:");
return false;
}
-
- // REMEMBER, IS NO SMALLER THAN
- /*
- System.out.println( " edges smaller" );
- return false;
- }
- */
-
}
}
return null;
}
- public Set<Alloc> canPointToAfter( TempDescriptor x,
- FlatNode programPoint ) {
- return null;
- }
-
public Hashtable< Alloc, Set<Alloc> > canPointToAt( TempDescriptor x,
FieldDescriptor f,
FlatNode programPoint ) {
FlatNode programPoint ) {
return null;
}
+
+ public Set<Alloc> canPointToAfter( TempDescriptor x,
+ FlatNode programPoint ) {
+ return null;
+ }
+
+ public Hashtable< Alloc, Set<Alloc> > canPointToAfter( TempDescriptor x,
+ FieldDescriptor f,
+ FlatNode programPoint ) {
+ return null;
+ }
+
+ public Hashtable< Alloc, Set<Alloc> > canPointToAfterElement( TempDescriptor x, // x[i]
+ FlatNode programPoint ) {
+ return null;
+ }
}
# -disjoint-debug-snap-method Remove 10 3 true
DISJOINTDEBUG= -disjoint -disjoint-k 1 -enable-assertions
+# -disjoint-write-dots final \
+# -flatirusermethods \
+# -disjoint-debug-callsite System.println Barneshut.run 1 1000 true \
+# -disjoint-debug-snap-method Barneshut.run 1 1000 false
+# -disjoint-debug-snap-method String.indexOf 1 1000 true
+# -disjoint-debug-callsite String.concat2 FileInputStream.readLine 1 1000 true \
+# -disjoint-debug-snap-method String.concat2 1 1000 true
+# -disjoint-debug-snap-method FileInputStream.readLine 1 1000 true
+# -disjoint-write-all-node-graphs
+#
+# -justanalyze \
# -disjoint-debug-callsite String.toString String.valueOf 1 1000 true \
-# -disjoint-debug-snap-method String.toString 1 1000 true \
# -disjoint-write-initial-contexts \
-# -disjoint-write-dots final
# -disjoint-debug-scheduling \
# -disjoint-write-ihms
-# -flatirusermethods
-# -justanalyze
# -disjoint-desire-determinism
# -disjoint-debug-callsite Demand.add Lateral.compute 1 1000 true
# -disjoint-debug-snap-method ComputeCenterOfMass 6 2 true
public class BCXPointsToCheckVRuntime implements BuildCodeExtension {
+ protected State state;
protected BuildCode buildCode;
protected TypeUtil typeUtil;
protected HeapAnalysis heapAnalysis;
protected ClassDescriptor cdObject;
+ protected TypeDescriptor stringType;
- public BCXPointsToCheckVRuntime( BuildCode buildCode,
+ private boolean DEBUG = false;
+
+
+
+ public BCXPointsToCheckVRuntime( State state,
+ BuildCode buildCode,
TypeUtil typeUtil,
HeapAnalysis heapAnalysis ) {
+ this.state = state;
this.buildCode = buildCode;
this.typeUtil = typeUtil;
this.heapAnalysis = heapAnalysis;
+
+ ClassDescriptor cdString = typeUtil.getClass( typeUtil.StringClass );
+ assert cdString != null;
+ stringType = new TypeDescriptor( cdString );
}
TempDescriptor td = fm.getParameter( i );
TypeDescriptor type = td.getType();
if( type.isPtr() ) {
+ output.println( "// Generating points-to checks for method params" );
+
genAssertRuntimePtrVsHeapResults( output,
fm,
td,
heapAnalysis.canPointToAfter( td, fm )
);
+
+ output.println( "// end method params" );
+
+ if( DEBUG ) {
+ System.out.println( "\nGenerating code for "+fm );
+ System.out.println( " arg "+td+" can point to "+heapAnalysis.canPointToAfter( td, fm ) );
+ }
}
}
}
FieldDescriptor fld;
TempDescriptor idx;
TypeDescriptor type;
+ TempDescriptor arg;
+ TempDescriptor ret;
+
+ // for PRE-NODE checks, only look at pointers we are reading from because
+ // pointers about to be set may be undefined and don't pass runtime checks nicely
+
switch( fn.kind() ) {
+ /*
+ case FKind.FlatLiteralNode: {
+ FlatLiteralNode fln = (FlatLiteralNode) fn;
+
+ if( fln.getType().equals( stringType ) ) {
+ lhs = fln.getDst();
+
+ output.println( "// Generating points-to checks for pre-node string literal" );
+
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ lhs,
+ heapAnalysis.canPointToAt( lhs, fn )
+ );
+
+ output.println( "// end pre-node string literal" );
+
+
+ if( DEBUG ) {
+ System.out.println( " before "+fn );
+ System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAt( lhs, fn ) );
+ }
+ }
+ } break;
+ */
+
case FKind.FlatOpNode: {
FlatOpNode fon = (FlatOpNode) fn;
if( fon.getOp().getOp() == Operation.ASSIGN ) {
type = lhs.getType();
if( type.isPtr() ) {
- genAssertRuntimePtrVsHeapResults( output,
- fm,
- lhs,
- heapAnalysis.canPointToAt( lhs, fn )
- );
+
+ output.println( "// Generating points-to checks for pre-node op assign" );
+
+
+ //genAssertRuntimePtrVsHeapResults( output,
+ // fm,
+ // lhs,
+ // heapAnalysis.canPointToAt( lhs, fn )
+ // );
genAssertRuntimePtrVsHeapResults( output,
fm,
rhs,
heapAnalysis.canPointToAt( rhs, fn )
);
+
+ output.println( "// end pre-node op assign" );
+
+
+ if( DEBUG ) {
+ System.out.println( " before "+fn );
+ //System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAt( lhs, fn ) );
+ System.out.println( " "+rhs+" can point to "+heapAnalysis.canPointToAt( rhs, fn ) );
+ }
}
}
} break;
type = fcn.getType();
if( type.isPtr() ) {
- genAssertRuntimePtrVsHeapResults( output,
- fm,
- lhs,
- heapAnalysis.canPointToAt( lhs, fn )
- );
+
+ output.println( "// Generating points-to checks for pre-node cast" );
+
+ //genAssertRuntimePtrVsHeapResults( output,
+ // fm,
+ // lhs,
+ // heapAnalysis.canPointToAt( lhs, fn )
+ // );
genAssertRuntimePtrVsHeapResults( output,
fm,
rhs,
heapAnalysis.canPointToAt( rhs, fn )
);
+
+ output.println( "// end pre-node cast" );
+
+
+ if( DEBUG ) {
+ System.out.println( " before "+fn );
+ //System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAt( lhs, fn ) );
+ System.out.println( " "+rhs+" can point to "+heapAnalysis.canPointToAt( rhs, fn ) );
+ }
}
} break;
type = lhs.getType();
if( type.isPtr() ) {
- genAssertRuntimePtrVsHeapResults( output,
- fm,
- lhs,
- heapAnalysis.canPointToAt( lhs, fn )
- );
+
+ output.println( "// Generating points-to checks for pre-node field" );
+
+ //genAssertRuntimePtrVsHeapResults( output,
+ // fm,
+ // lhs,
+ // heapAnalysis.canPointToAt( lhs, fn )
+ // );
genAssertRuntimePtrVsHeapResults( output,
fm,
null,
heapAnalysis.canPointToAt( rhs, fld, fn )
);
+
+ output.println( "// end pre-node field" );
+
+
+ if( DEBUG ) {
+ System.out.println( " before "+fn );
+ //System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAt( lhs, fn ) );
+ System.out.println( " "+rhs+" can point to "+heapAnalysis.canPointToAt( rhs, fn ) );
+ System.out.println( " "+rhs+"."+fld+" can point to "+heapAnalysis.canPointToAt( rhs, fld, fn ) );
+ }
}
} break;
type = lhs.getType();
if( type.isPtr() ) {
- genAssertRuntimePtrVsHeapResults( output,
- fm,
- lhs,
- heapAnalysis.canPointToAt( lhs, fn )
- );
+
+ output.println( "// Generating points-to checks for pre-node element" );
+
+ //genAssertRuntimePtrVsHeapResults( output,
+ // fm,
+ // lhs,
+ // heapAnalysis.canPointToAt( lhs, fn )
+ // );
genAssertRuntimePtrVsHeapResults( output,
fm,
idx,
heapAnalysis.canPointToAtElement( rhs, fn )
);
+
+ output.println( "// end pre-node element" );
+
+
+ if( DEBUG ) {
+ System.out.println( " before "+fn );
+ //System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAt( lhs, fn ) );
+ System.out.println( " "+rhs+" can point to "+heapAnalysis.canPointToAt( rhs, fn ) );
+ System.out.println( " "+rhs+"["+idx+"] can point to "+heapAnalysis.canPointToAtElement( rhs, fn ) );
+ }
}
} break;
-
- }
+
+ case FKind.FlatCall: {
+ FlatCall fc = (FlatCall) fn;
+ //ret = fc.getReturnTemp();
+
+ FlatMethod fmCallee = state.getMethodFlat( fc.getMethod() );
+
+ boolean somethingChecked = false;
+
+ output.println( "// Generating points-to checks for pre-node call" );
+
+ for( int i = 0; i < fmCallee.numParameters(); ++i ) {
+ arg = fc.getArgMatchingParamIndex( fmCallee, i );
+ type = arg.getType();
+ if( type.isPtr() ) {
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ arg,
+ heapAnalysis.canPointToAt( arg, fn )
+ );
+ somethingChecked = true;
+ }
+ }
+
+ //if( ret != null ) {
+ // type = ret.getType();
+ // if( type.isPtr() ) {
+ // genAssertRuntimePtrVsHeapResults( output,
+ // fm,
+ // ret,
+ // heapAnalysis.canPointToAt( ret, fn )
+ // );
+ // somethingChecked = true;
+ // }
+ //}
+
+ output.println( "// end pre-node call" );
+
+ if( DEBUG && somethingChecked ) {
+
+ System.out.println( " before "+fn+":" );
+
+ for( int i = 0; i < fmCallee.numParameters(); ++i ) {
+ arg = fc.getArgMatchingParamIndex( fmCallee, i );
+ type = arg.getType();
+ if( type.isPtr() ) {
+ System.out.println( " arg "+arg+" can point to "+heapAnalysis.canPointToAt( arg, fn ) );
+ }
+ }
+
+ //if( ret != null ) {
+ // type = ret.getType();
+ // if( type.isPtr() ) {
+ // System.out.println( " return temp "+ret+" can point to "+heapAnalysis.canPointToAt( ret, fn ) );
+ // }
+ //}
+
+ }
+ } break;
+ }
}
+
public void additionalCodePostNode(FlatMethod fm,
FlatNode fn,
PrintWriter output) {
+
+ TempDescriptor lhs;
+ TempDescriptor rhs;
+ FieldDescriptor fld;
+ TempDescriptor idx;
+ TypeDescriptor type;
+ TempDescriptor arg;
+ TempDescriptor ret;
+
+
+
switch( fn.kind() ) {
+
+
+ case FKind.FlatLiteralNode: {
+ FlatLiteralNode fln = (FlatLiteralNode) fn;
+
+ if( fln.getType().equals( stringType ) ) {
+ lhs = fln.getDst();
+
+ output.println( "// Generating points-to checks for post-node string literal" );
+
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ lhs,
+ heapAnalysis.canPointToAfter( lhs, fn )
+ );
+
+ output.println( "// end post-node string literal" );
+
+
+ if( DEBUG ) {
+ System.out.println( " after "+fn );
+ System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAfter( lhs, fn ) );
+ }
+ }
+ } break;
+
+
+ case FKind.FlatOpNode: {
+ FlatOpNode fon = (FlatOpNode) fn;
+ if( fon.getOp().getOp() == Operation.ASSIGN ) {
+ lhs = fon.getDest();
+
+ type = lhs.getType();
+ if( type.isPtr() ) {
+
+ output.println( "// Generating points-to checks for post-node op assign" );
+
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ lhs,
+ heapAnalysis.canPointToAfter( lhs, fn )
+ );
+
+ output.println( "// end post-node op assign" );
+
+
+ if( DEBUG ) {
+ System.out.println( " after "+fn );
+ System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAfter( lhs, fn ) );
+ }
+ }
+ }
+ } break;
+
+
+ case FKind.FlatCastNode: {
+ FlatCastNode fcn = (FlatCastNode) fn;
+ lhs = fcn.getDst();
+
+ type = fcn.getType();
+ if( type.isPtr() ) {
+
+ output.println( "// Generating points-to checks for post-node cast" );
+
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ lhs,
+ heapAnalysis.canPointToAfter( lhs, fn )
+ );
+
+ output.println( "// end post-node cast" );
+
+
+ if( DEBUG ) {
+ System.out.println( " after "+fn );
+ System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAfter( lhs, fn ) );
+ }
+ }
+ } break;
+
+
+ case FKind.FlatFieldNode: {
+ FlatFieldNode ffn = (FlatFieldNode) fn;
+ lhs = ffn.getDst();
+
+ type = lhs.getType();
+ if( type.isPtr() ) {
+
+ output.println( "// Generating points-to checks for post-node field" );
+
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ lhs,
+ heapAnalysis.canPointToAfter( lhs, fn )
+ );
+
+ output.println( "// end post-node field" );
+
+
+ if( DEBUG ) {
+ System.out.println( " after "+fn );
+ System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAfter( lhs, fn ) );
+ }
+ }
+ } break;
+
+
+ case FKind.FlatElementNode: {
+ FlatElementNode fen = (FlatElementNode) fn;
+ lhs = fen.getDst();
+
+ type = lhs.getType();
+ if( type.isPtr() ) {
+
+ output.println( "// Generating points-to checks for post-node element" );
+
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ lhs,
+ heapAnalysis.canPointToAfter( lhs, fn )
+ );
+
+ output.println( "// end post-node element" );
+
+
+ if( DEBUG ) {
+ System.out.println( " after "+fn );
+ System.out.println( " "+lhs+" can point to "+heapAnalysis.canPointToAfter( lhs, fn ) );
+ }
+ }
+ } break;
+
+
case FKind.FlatCall: {
- FlatCall fc = (FlatCall) fn;
- TempDescriptor td = fc.getReturnTemp();
-
- if( td != null ) {
- TypeDescriptor type = td.getType();
+ FlatCall fc = (FlatCall) fn;
+ ret = fc.getReturnTemp();
+
+ FlatMethod fmCallee = state.getMethodFlat( fc.getMethod() );
+
+ boolean somethingChecked = false;
+
+ output.println( "// Generating points-to checks for post-node call" );
+
+ for( int i = 0; i < fmCallee.numParameters(); ++i ) {
+ arg = fc.getArgMatchingParamIndex( fmCallee, i );
+ type = arg.getType();
if( type.isPtr() ) {
genAssertRuntimePtrVsHeapResults( output,
fm,
- td,
- heapAnalysis.canPointToAfter( td, fn )
+ arg,
+ heapAnalysis.canPointToAfter( arg, fn )
);
+ somethingChecked = true;
+ }
+ }
+
+ if( ret != null ) {
+ type = ret.getType();
+ if( type.isPtr() ) {
+ genAssertRuntimePtrVsHeapResults( output,
+ fm,
+ ret,
+ heapAnalysis.canPointToAfter( ret, fn )
+ );
+ somethingChecked = true;
+ }
+ }
+
+ output.println( "// end post-node call" );
+
+ if( DEBUG && somethingChecked ) {
+
+ System.out.println( " after "+fn+":" );
+
+ for( int i = 0; i < fmCallee.numParameters(); ++i ) {
+ arg = fc.getArgMatchingParamIndex( fmCallee, i );
+ type = arg.getType();
+ if( type.isPtr() ) {
+ System.out.println( " arg "+arg+" can point to "+heapAnalysis.canPointToAfter( arg, fn ) );
+ }
+ }
+
+ if( ret != null ) {
+ type = ret.getType();
+ if( type.isPtr() ) {
+ System.out.println( " return temp "+ret+" can point to "+heapAnalysis.canPointToAfter( ret, fn ) );
+ }
}
+
}
} break;
}
public boolean DISJOINTDEBUGSCHEDULING=false;
+ public boolean DISJOINT_WRITE_ALL_NODE_FINAL_GRAPHS=false;
public boolean POINTSTO_CHECK_V_RUNTIME=false;
} else if (option.equals("-disjoint-write-ihms")) {
state.DISJOINTWRITEIHMS = true;
+ } else if (option.equals("-disjoint-write-all-node-graphs")) {
+ state.DISJOINT_WRITE_ALL_NODE_FINAL_GRAPHS = true;
+
} else if (option.equals("-disjoint-alias-file")) {
state.DISJOINTALIASFILE = args[++i];
String arg = args[++i];
if( state.POINTSTO_CHECK_V_RUNTIME &&
heapAnalysis != null ) {
- BCXPointsToCheckVRuntime bcx = new BCXPointsToCheckVRuntime( bc, tu, heapAnalysis );
+ BCXPointsToCheckVRuntime bcx = new BCXPointsToCheckVRuntime( state, bc, tu, heapAnalysis );
bc.registerExtension( bcx );
}