t.stallSite,
t.var,
t.allocSite,
+ t.fnDefined,
preds
);
// set some static configuration for ReachGraphs
ReachGraph.allocationDepth = allocationDepth;
ReachGraph.typeUtil = typeUtil;
+ ReachGraph.state = state;
+
ReachGraph.debugCallSiteVisitStartCapture
= state.DISJOINTDEBUGCALLVISITTOSTART;
true, // hide reachability altogether
false, // hide subset reachability states
true, // hide predicates
- true ); // hide edge taints
+ false ); // hide edge taints
} break;
// from DisjointAnalysis for convenience
protected static int allocationDepth = -1;
protected static TypeUtil typeUtil = null;
+ protected static State state = null;
// variable and heap region nodes indexed by unique ID
while( isvItr.hasNext() ) {
TempDescriptor isv = isvItr.next();
+ // use this where defined flatnode to support RCR/DFJ
+ FlatNode whereDefined = null;
+ if( state.RCR ) {
+ whereDefined = sese;
+ }
+
// in-set var taints should NOT propagate back into callers
// so give it FALSE(EMPTY) predicates
taintTemp( sese,
null,
isv,
+ whereDefined,
predsEmpty
- );
-
+ );
}
}
public void taintStallSite( FlatNode stallSite,
TempDescriptor var ) {
+
+ // use this where defined flatnode to support RCR/DFJ
+ FlatNode whereDefined = null;
+ if( state.RCR ) {
+ whereDefined = stallSite;
+ }
// stall site taint should propagate back into callers
// so give it TRUE predicates
- taintTemp( null,
- stallSite,
- var,
- predsTrue
- );
+ taintTemp( null,
+ stallSite,
+ var,
+ whereDefined,
+ predsTrue
+ );
}
protected void taintTemp( FlatSESEEnterNode sese,
FlatNode stallSite,
TempDescriptor var,
+ FlatNode whereDefined,
ExistPredSet preds
) {
stallSite,
var,
re.getDst().getAllocSite(),
+ whereDefined,
preds
);
tCallee.stallSite,
tCallee.var,
tCallee.allocSite,
+ tCallee.fnDefined,
ExistPredSet.factory() ),
calleeTaintsSatisfied.get( tCallee )
);
--- /dev/null
+package Analysis.Disjoint;
+
+import java.util.*;
+import java.io.*;
+
+import IR.*;
+import IR.Flat.*;
+
+//////////////////////////////////////////////
+//
+// SMFEState is part of a
+// (S)tate (M)achine (F)or (E)ffects.
+//
+// StateMachineForEffects describes an intial
+// state and the effect transtions a DFJ
+// traverser should make from the current state
+// when searching for possible runtime conflicts.
+//
+//////////////////////////////////////////////
+
+public class SMFEState {
+
+ // uniquely identifies this state
+ protected FlatNode id;
+
+ // all possible effects in this state
+ protected Set<Effect> effects;
+
+ // the given effect allows a transition to a
+ // set of new states
+ protected Hashtable< Effect, Set<SMFEState> > e2states;
+
+
+ public SMFEState( FlatNode id ) {
+ this.id = id;
+ effects = new HashSet<Effect>();
+ e2states = new Hashtable< Effect, Set<SMFEState> >();
+ }
+
+ public void addEffect( Effect e ) {
+ effects.add( e );
+ }
+
+ // the given effect allows the transition to the new state
+ public void addTransition( Effect effect,
+ SMFEState stateTo
+ ) {
+
+ Set<SMFEState> states = e2states.get( effect );
+ if( states == null ) {
+ states = new HashSet<SMFEState>();
+ }
+ states.add( stateTo );
+ }
+
+ public FlatNode getID() {
+ return id;
+ }
+
+
+ public boolean equals( Object o ) {
+ if( o == null ) {
+ return false;
+ }
+
+ if( !(o instanceof SMFEState) ) {
+ return false;
+ }
+
+ SMFEState state = (SMFEState) o;
+
+ return id.equals( state.id );
+ }
+
+ public int hashCode() {
+ return id.hashCode();
+ }
+
+
+ public String toStringDOT() {
+
+ // first create the state as a node in DOT graph
+ String s = " "+id.nodeid+
+ "[shape=box,label=\"";
+
+ if( effects.size() == 1 ) {
+ s += effects.iterator().next().toString();
+
+ } else if( effects.size() > 1 ) {
+
+ Iterator<Effect> eItr = effects.iterator();
+ while( eItr.hasNext() ) {
+ Effect e = eItr.next();
+ s += e.toString();
+
+ if( eItr.hasNext() ) {
+ s += "\\n";
+ }
+ }
+ }
+
+ s += "\"];";
+
+ // then each transition is an edge
+ Iterator<Effect> eItr = e2states.entrySet().iterator();
+ while( eItr.hasNext() ) {
+ Effect e = eItr.next();
+ SMFEState state = e2states.get( e );
+
+ s += "\n "+
+ id.nodeid+" -> "+state.id.nodeid+
+ "[label=\""+e+"\"];"
+ }
+
+ return s;
+ }
+}
--- /dev/null
+package Analysis.Disjoint;
+
+import java.util.*;
+import java.io.*;
+
+import IR.*;
+import IR.Flat.*;
+
+//////////////////////////////////////////////
+//
+// StateMachineForEffects describes an intial
+// state and the effect transtions a DFJ
+// traverser should make from the current state
+// when searching for possible runtime conflicts.
+//
+//////////////////////////////////////////////
+
+public class StateMachineForEffects {
+
+ // states in the machine are uniquely identified
+ // by a flat node (program point)
+ protected Hashtable<FlatNode, SMFEState> fn2state;
+
+ protected SMFEState initialState;
+
+
+ public StateMachineForEffects( FlatNode fnInitial ) {
+ fn2state = new Hashtable<FlatNode, SMFEState>();
+
+ initialState = getState( fnInitial );
+ }
+
+ public void addTransition( FlatNode fnFrom,
+ FlatNode fnTo,
+ Effect e ) {
+
+ assert fn2state.containsKey( fnFrom );
+ SMFEState stateFrom = getState( fnFrom );
+ SMFEState stateTo = getState( fnTo );
+
+ stateFrom.addTransition( e, stateTo );
+ }
+
+ public SMFEState getIntialState() {
+ return initialState;
+ }
+
+
+ protected SMFEState getState( FlatNode fn ) {
+ SMFEState state = fn2state.get( fn );
+ if( state == null ) {
+ state = new SMFEState();
+ }
+ return state;
+ }
+
+
+ public void writeAsDOT() {
+ String graphName = initialState.getID().toString();
+ graphName = graphName.replaceAll( "[\\W]", "" );
+
+ try {
+ BufferedWriter bw =
+ new BufferedWriter( new FileWriter( graphName+".dot" ) );
+
+ bw.write( "digraph "+graphName+" {\n" );
+
+ Iterator<Effect> fnItr = fn2state.entrySet().iterator();
+ while( fnItr.hasNext() ) {
+ SMFEState state = fn2state.get( fnItr.next() );
+ bw.write( state.toStringDOT()+"\n" );
+ }
+
+ bw.write( "}\n" );
+ bw.close();
+
+ } catch( IOException e ) {
+ throw new Error( "Error writing out DOT graph "+graphName );
+ }
+ }
+
+}
protected TempDescriptor var;
protected AllocSite allocSite;
+ // taints have a new, possibly null element which is
+ // the FlatNode at which the tainted reference was
+ // defined, which currently supports DFJ but doesn't
+ // hinder other analysis modes
+ protected FlatNode fnDefined;
+
// existance predicates must be true in a caller
// context for this taint's effects to transfer from this
// callee to that context
protected ExistPredSet preds;
+
+
public static Taint factory( FlatSESEEnterNode sese,
TempDescriptor insetVar,
AllocSite as,
+ FlatNode whereDefined,
ExistPredSet eps ) {
- Taint out = new Taint( sese, null, insetVar, as, eps );
+ Taint out = new Taint( sese, null, insetVar, as, whereDefined, eps );
out = (Taint) Canonical.makeCanonical( out );
return out;
}
public static Taint factory( FlatNode stallSite,
TempDescriptor var,
AllocSite as,
+ FlatNode whereDefined,
ExistPredSet eps ) {
- Taint out = new Taint( null, stallSite, var, as, eps );
+ Taint out = new Taint( null, stallSite, var, as, whereDefined, eps );
out = (Taint) Canonical.makeCanonical( out );
return out;
}
FlatNode stallSite,
TempDescriptor var,
AllocSite as,
+ FlatNode whereDefined,
ExistPredSet eps ) {
- Taint out = new Taint( sese, stallSite, var, as, eps );
+ Taint out = new Taint( sese, stallSite, var, as, whereDefined, eps );
out = (Taint) Canonical.makeCanonical( out );
return out;
}
FlatNode stallSite,
TempDescriptor v,
AllocSite as,
+ FlatNode fnDefined,
ExistPredSet eps ) {
assert
(sese == null && stallSite != null) ||
this.stallSite = stallSite;
this.var = v;
this.allocSite = as;
+ this.fnDefined = fnDefined;
this.preds = eps;
}
t.stallSite,
t.var,
t.allocSite,
+ t.fnDefined,
t.preds );
}
return allocSite;
}
+ public FlatNode getWhereDefined() {
+ return fnDefined;
+ }
+
public ExistPredSet getPreds() {
return preds;
}
stallSiteEqual = stallSite.equals( t.stallSite );
}
+ boolean fnDefinedEqual;
+ if( fnDefined == null ) {
+ fnDefinedEqual = (t.fnDefined == null);
+ } else {
+ fnDefinedEqual = fnDefined.equals( t.fnDefined );
+ }
+
return
seseEqual &&
stallSiteEqual &&
+ fnDefinedEqual &&
var .equals( t.var ) &&
allocSite.equals( t.allocSite );
}
hash = hash ^ stallSite.hashCode();
}
+ if( fnDefined != null ) {
+ hash = hash ^ fnDefined.hashCode();
+ }
+
return hash;
}
s = stallSite.toString();
}
+ String f = "";
+ if( fnDefined != null ) {
+ f += ", "+fnDefined;
+ }
+
return
"("+s+
"-"+var+
", "+allocSite.toStringBrief()+
+ f+
"):"+preds;
}
}
t.stallSite,
t.var,
t.allocSite,
+ t.fnDefined,
preds );
out.taints.add( tOut );
}
projects / IRC.git / commitdiff