From: jjenista Date: Fri, 4 Mar 2011 23:10:03 +0000 (+0000) Subject: extend taints for a new mode in DFJ that helps build the state machine traversers X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6be7554a5efe98821649c3ff5ffcfcf2d815ea13;p=IRC.git extend taints for a new mode in DFJ that helps build the state machine traversers --- diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java index 291f424c..456b9dfe 100644 --- a/Robust/src/Analysis/Disjoint/Canonical.java +++ b/Robust/src/Analysis/Disjoint/Canonical.java @@ -1533,6 +1533,7 @@ abstract public class Canonical { t.stallSite, t.var, t.allocSite, + t.fnDefined, preds ); diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index ffe9f072..81ea411e 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -688,6 +688,8 @@ public class DisjointAnalysis { // set some static configuration for ReachGraphs ReachGraph.allocationDepth = allocationDepth; ReachGraph.typeUtil = typeUtil; + ReachGraph.state = state; + ReachGraph.debugCallSiteVisitStartCapture = state.DISJOINTDEBUGCALLVISITTOSTART; @@ -1135,7 +1137,7 @@ public class DisjointAnalysis { true, // hide reachability altogether false, // hide subset reachability states true, // hide predicates - true ); // hide edge taints + false ); // hide edge taints } break; diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index a8d8b605..d296bf24 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -29,6 +29,7 @@ public class ReachGraph { // 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 @@ -1286,32 +1287,46 @@ public class ReachGraph { 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 ) { @@ -1325,6 +1340,7 @@ public class ReachGraph { stallSite, var, re.getDst().getAllocSite(), + whereDefined, preds ); @@ -1695,6 +1711,7 @@ public class ReachGraph { tCallee.stallSite, tCallee.var, tCallee.allocSite, + tCallee.fnDefined, ExistPredSet.factory() ), calleeTaintsSatisfied.get( tCallee ) ); diff --git a/Robust/src/Analysis/Disjoint/SMFEState.java b/Robust/src/Analysis/Disjoint/SMFEState.java new file mode 100644 index 00000000..f427cd99 --- /dev/null +++ b/Robust/src/Analysis/Disjoint/SMFEState.java @@ -0,0 +1,117 @@ +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 effects; + + // the given effect allows a transition to a + // set of new states + protected Hashtable< Effect, Set > e2states; + + + public SMFEState( FlatNode id ) { + this.id = id; + effects = new HashSet(); + e2states = new Hashtable< Effect, Set >(); + } + + 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 states = e2states.get( effect ); + if( states == null ) { + states = new HashSet(); + } + 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 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 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; + } +} diff --git a/Robust/src/Analysis/Disjoint/StateMachineForEffects.java b/Robust/src/Analysis/Disjoint/StateMachineForEffects.java new file mode 100644 index 00000000..0becddb8 --- /dev/null +++ b/Robust/src/Analysis/Disjoint/StateMachineForEffects.java @@ -0,0 +1,82 @@ +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 fn2state; + + protected SMFEState initialState; + + + public StateMachineForEffects( FlatNode fnInitial ) { + fn2state = new Hashtable(); + + 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 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 ); + } + } + +} diff --git a/Robust/src/Analysis/Disjoint/Taint.java b/Robust/src/Analysis/Disjoint/Taint.java index fc87353b..a6a38e9a 100644 --- a/Robust/src/Analysis/Disjoint/Taint.java +++ b/Robust/src/Analysis/Disjoint/Taint.java @@ -44,16 +44,25 @@ public class Taint extends Canonical { 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; } @@ -61,8 +70,9 @@ public class Taint extends Canonical { 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; } @@ -71,8 +81,9 @@ public class Taint extends Canonical { 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; } @@ -81,6 +92,7 @@ public class Taint extends Canonical { FlatNode stallSite, TempDescriptor v, AllocSite as, + FlatNode fnDefined, ExistPredSet eps ) { assert (sese == null && stallSite != null) || @@ -94,6 +106,7 @@ public class Taint extends Canonical { this.stallSite = stallSite; this.var = v; this.allocSite = as; + this.fnDefined = fnDefined; this.preds = eps; } @@ -102,6 +115,7 @@ public class Taint extends Canonical { t.stallSite, t.var, t.allocSite, + t.fnDefined, t.preds ); } @@ -129,6 +143,10 @@ public class Taint extends Canonical { return allocSite; } + public FlatNode getWhereDefined() { + return fnDefined; + } + public ExistPredSet getPreds() { return preds; } @@ -167,9 +185,17 @@ public class Taint extends Canonical { 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 ); } @@ -186,6 +212,10 @@ public class Taint extends Canonical { hash = hash ^ stallSite.hashCode(); } + if( fnDefined != null ) { + hash = hash ^ fnDefined.hashCode(); + } + return hash; } @@ -199,10 +229,16 @@ public class Taint extends Canonical { s = stallSite.toString(); } + String f = ""; + if( fnDefined != null ) { + f += ", "+fnDefined; + } + return "("+s+ "-"+var+ ", "+allocSite.toStringBrief()+ + f+ "):"+preds; } } diff --git a/Robust/src/Analysis/Disjoint/TaintSet.java b/Robust/src/Analysis/Disjoint/TaintSet.java index 49319c50..4fda15a0 100644 --- a/Robust/src/Analysis/Disjoint/TaintSet.java +++ b/Robust/src/Analysis/Disjoint/TaintSet.java @@ -61,6 +61,7 @@ public class TaintSet extends Canonical { t.stallSite, t.var, t.allocSite, + t.fnDefined, preds ); out.taints.add( tOut ); }