- public static ReachState makePredsTrue( ReachState rs ) {
+ public static ReachState changePredsTo( ReachState rs,
+ ExistPredSet preds ) {
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,
+ new CanonicalOp( CanonicalOp.REACHSTATE_CHANGEPREDSTO_EXISTPREDSET,
rs,
- ReachState.factory() );
+ preds );
Canonical result = op2result.get( op );
if( result != null ) {
// just remake state with the true predicate attached
out.reachTuples.addAll( rs.reachTuples );
- out.preds = ExistPredSet.factory( ExistPred.factory() );
+ out.preds = preds;
out = (ReachState) makeCanonical( out );
op2result.put( op, out );
}
- public static ReachSet makePredsTrue( ReachSet rs ) {
+ public static ReachSet changePredsTo( ReachSet rs,
+ ExistPredSet preds ) {
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,
+ new CanonicalOp( CanonicalOp.REACHSET_CHANGEPREDSTO_EXISTPREDSET,
rs,
- ReachSet.factory() );
+ preds );
Canonical result = op2result.get( op );
if( result != null ) {
while( itr.hasNext() ) {
ReachState state = itr.next();
out = Canonical.add( out,
- Canonical.makePredsTrue( state )
+ Canonical.changePredsTo( state,
+ preds
+ )
);
}
}
- public static Taint changePredsTo( Taint t, ExistPredSet preds ) {
+ public static Taint changePredsTo( Taint t,
+ ExistPredSet preds ) {
assert t != null;
assert t.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.TAINT_CHANGEPREDSTO,
+ new CanonicalOp( CanonicalOp.TAINT_CHANGEPREDSTO_EXISTPREDSET,
t,
- t );
+ preds );
Canonical result = op2result.get( op );
if( result != null ) {
}
- public static TaintSet changePredsTo( TaintSet ts, ExistPredSet preds ) {
+ public static TaintSet changePredsTo( TaintSet ts,
+ ExistPredSet preds ) {
assert ts != null;
assert ts.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.TAINTSET_CHANGEPREDSTO,
+ new CanonicalOp( CanonicalOp.TAINTSET_CHANGEPREDSTO_EXISTPREDSET,
ts,
- ts );
+ preds );
Canonical result = op2result.get( op );
if( result != null ) {
public static final int REACHSTATE_TOCALLERCONTEXT_ALLOCSITE = 0xb2b1;
public static final int REACHSET_UNSHADOW_ALLOCSITE = 0x1049;
public static final int REACHSTATE_UNSHADOW_ALLOCSITE = 0x08ef;
- public static final int REACHSTATE_MAKEPREDSTRUE = 0x0b9c;
- public static final int REACHSET_MAKEPREDSTRUE = 0xdead;
+ public static final int REACHSTATE_CHANGEPREDSTO_EXISTPREDSET= 0x0b9c;
+ public static final int REACHSET_CHANGEPREDSTO_EXISTPREDSET = 0xdead;
public static final int TAINT_ATTACH_EXISTPREDSET = 0xcce2;
public static final int TAINTSET_ADD_TAINT = 0xcd17;
public static final int TAINTSET_UNION_TAINTSET = 0xa835;
public static final int TAINTSET_UNIONORPREDS_TAINTSET = 0x204f;
- public static final int TAINT_CHANGEPREDSTO = 0x3ab4;
- public static final int TAINTSET_CHANGEPREDSTO = 0x2ff1;
+ public static final int TAINT_CHANGEPREDSTO_EXISTPREDSET = 0x3ab4;
+ public static final int TAINTSET_CHANGEPREDSTO_EXISTPREDSET = 0x2ff1;
protected int opCode;
protected Canonical operand1;
protected TypeDescriptor e_type;
protected String e_field;
-
+ // if the taint is non-null then the predicate
+ // is true only if the edge exists AND has the
+ // taint--ONLY ONE of the ne_state or e_taint
+ // may be non-null for an edge predicate
+ protected Taint e_taint;
e_hrnDstID = null;
e_type = null;
e_field = null;
+ e_taint = null;
e_srcOutCalleeContext = false;
e_srcOutCallerContext = false;
}
e_hrnDstID = null;
e_type = null;
e_field = null;
+ e_taint = null;
e_srcOutCalleeContext = false;
e_srcOutCallerContext = false;
}
TypeDescriptor type,
String field,
ReachState state,
+ Taint taint,
boolean srcOutCalleeContext,
boolean srcOutCallerContext ) {
type,
field,
state,
+ taint,
srcOutCalleeContext,
srcOutCallerContext );
TypeDescriptor type,
String field,
ReachState state,
+ Taint taint,
boolean srcOutCalleeContext,
boolean srcOutCallerContext ) {
assert (tdSrc == null) || (hrnSrcID == null);
assert hrnDstID != null;
assert type != null;
+ assert (state == null) || (taint == null);
// fields can be null when the edge is from
// a variable node to a heap region!
- // assert field != null;
this.e_srcOutCalleeContext = srcOutCalleeContext;
this.e_srcOutCallerContext = srcOutCallerContext;
this.e_hrnSrcID = hrnSrcID;
this.e_hrnDstID = hrnDstID;
this.e_type = type;
- this.e_field = field;
+ this.e_field = field;
this.ne_state = state;
+ this.e_taint = taint;
this.predType = TYPE_EDGE;
n_hrnID = null;
}
+ // for node or edge, check inputs
+ public static ExistPred factory( Integer hrnID,
+ TempDescriptor tdSrc,
+ Integer hrnSrcID,
+ Integer hrnDstID,
+ TypeDescriptor type,
+ String field,
+ ReachState state,
+ Taint taint,
+ boolean srcOutCalleeContext,
+ boolean srcOutCallerContext ) {
+ ExistPred out;
+
+ if( hrnID != null ) {
+ out = new ExistPred( hrnID, state );
+
+ } else {
+ out = new ExistPred( tdSrc,
+ hrnSrcID,
+ hrnDstID,
+ type,
+ field,
+ state,
+ taint,
+ srcOutCalleeContext,
+ srcOutCallerContext );
+ }
+
+ out = (ExistPred) Canonical.makeCanonical( out );
+ return out;
+ }
+
+
+
// only consider the subest of the caller elements that
// are reachable by callee when testing predicates--if THIS
return null;
}
- // when the state is null it is not part of the
- // predicate, so we've already satisfied
+ // when the state is null we're done!
if( ne_state == null ) {
return hrn.getPreds();
- }
- // otherwise look for state too
- // TODO: contains OR containsSuperSet OR containsWithZeroes??
- if( hrn.getAlpha().containsIgnorePreds( ne_state )
- == null ) {
- return hrn.getPreds();
+ } else {
+ // otherwise look for state too
+
+ // TODO: contains OR containsSuperSet OR containsWithZeroes??
+ ReachState stateCaller = hrn.getAlpha().containsIgnorePreds( ne_state );
+
+ if( stateCaller == null ) {
+ return null;
+
+ } else {
+ // it was here, return the predicates on the state!!
+ return stateCaller.getPreds();
+ }
}
- return null;
+ // unreachable program point!
}
if( predType == TYPE_EDGE ) {
return null;
}
- // only check state as part of the predicate if it
- // is non-null
- if( ne_state != null &&
- // TODO: contains OR containsSuperSet OR containsWithZeroes??
- hrnDst.getAlpha().containsIgnorePreds( ne_state ) != null
- ) {
- return null;
+ // when the state and taint are null we're done!
+ if( ne_state == null &&
+ e_taint == null ) {
+ return edge.getPreds();
+
+ } else if( ne_state != null ) {
+ // otherwise look for state too
+
+ // TODO: contains OR containsSuperSet OR containsWithZeroes??
+ ReachState stateCaller = edge.getBeta().containsIgnorePreds( ne_state );
+
+ if( stateCaller == null ) {
+ return null;
+
+ } else {
+ // it was here, return the predicates on the state!!
+ return stateCaller.getPreds();
+ }
+
+ } else {
+ // otherwise look for taint
+
+ Taint tCaller = edge.getTaints().containsIgnorePreds( e_taint );
+
+ if( tCaller == null ) {
+ return null;
+
+ } else {
+ // it was here, return the predicates on the taint!!
+ return tCaller.getPreds();
+ }
}
-
- // predicate satisfied
- return edge.getPreds();
+
+ // unreachable program point!
}
throw new Error( "Unknown predicate type" );
return false;
}
+ if( e_taint == null ) {
+ if( pred.e_taint != null ) {
+ return false;
+ }
+ } else if( !e_taint.equals( pred.e_taint ) ) {
+ return false;
+ }
+
return true;
}
if( ne_state != null ) {
hash ^= ne_state.hashCode();
}
-
+
+ if( e_taint != null ) {
+ hash ^= e_taint.hashCode();
+ }
+
return hash;
}
s += "w"+ne_state;
}
+ if( e_taint != null ) {
+ s += "w"+e_taint;
+ }
+
return s;
}
// a special out-of-scope temp
protected static final TempDescriptor tdReturn = new TempDescriptor( "_Return___" );
-
- // some frequently used reachability constants
- protected static final ReachState rstateEmpty = ReachState.factory();
- protected static final ReachSet rsetEmpty = ReachSet.factory();
- protected static final ReachSet rsetWithEmptyState = Canonical.makePredsTrue(ReachSet.factory( rstateEmpty ));
// predicate constants
public static final ExistPred predTrue = ExistPred.factory(); // if no args, true
public static final ExistPredSet predsEmpty = ExistPredSet.factory();
public static final ExistPredSet predsTrue = ExistPredSet.factory( predTrue );
-
+
+ // some frequently used reachability constants
+ protected static final ReachState rstateEmpty = ReachState.factory();
+ protected static final ReachSet rsetEmpty = ReachSet.factory();
+ protected static final ReachSet rsetWithEmptyState = Canonical.changePredsTo( ReachSet.factory( rstateEmpty ),
+ predsTrue );
// from DisjointAnalysis for convenience
protected static int allocationDepth = -1;
if( inherent == null ) {
if( markForAnalysis ) {
inherent =
- Canonical.makePredsTrue(
+ Canonical.changePredsTo(
ReachSet.factory(
ReachState.factory(
ReachTuple.factory( id,
false // out-of-context
)
)
- )
+ ),
+ predsTrue
);
} else {
inherent = rsetWithEmptyState;
hrnY,
tdNewEdge,
f.getSymbol(),
- Canonical.makePredsTrue(
+ Canonical.changePredsTo(
Canonical.pruneBy( edgeY.getBeta(),
hrnX.getAlpha()
- )
+ ),
+ predsTrue
),
predsTrue,
Canonical.changePredsTo( edgeY.getTaints(),
// used below to convert a ReachSet to its callee-context
// equivalent with respect to allocation sites in this graph
protected ReachSet toCalleeContext( ReachSet rs,
- ExistPredSet preds,
+ ExistPredSet predsNodeOrEdge,
Set<HrnIdOoc> oocHrnIdOoc2callee
) {
ReachSet out = ReachSet.factory();
stateCallee = stateNew;
}
- // attach the passed in preds
- stateCallee = Canonical.attach( stateCallee,
- preds );
+ // make a predicate of the caller graph element
+ // and the caller state we just converted
+ ExistPredSet predsWithState = ExistPredSet.factory();
+
+ Iterator<ExistPred> predItr = predsNodeOrEdge.iterator();
+ while( predItr.hasNext() ) {
+ ExistPred predNodeOrEdge = predItr.next();
+
+ predsWithState =
+ Canonical.add( predsWithState,
+ ExistPred.factory( predNodeOrEdge.n_hrnID,
+ predNodeOrEdge.e_tdSrc,
+ predNodeOrEdge.e_hrnSrcID,
+ predNodeOrEdge.e_hrnDstID,
+ predNodeOrEdge.e_type,
+ predNodeOrEdge.e_field,
+ stateCallee,
+ null,
+ predNodeOrEdge.e_srcOutCalleeContext,
+ predNodeOrEdge.e_srcOutCallerContext
+ )
+ );
+ }
+ stateCallee = Canonical.changePredsTo( stateCallee,
+ predsWithState );
+
out = Canonical.add( out,
stateCallee
- );
-
+ );
}
assert out.isCanonical();
return out;
}
+ // convert a caller taint set into a callee taint set
+ protected TaintSet
+ toCalleeContext( TaintSet ts,
+ ExistPredSet predsEdge ) {
+
+ TaintSet out = TaintSet.factory();
+
+ // the idea is easy, the taint identifier itself doesn't
+ // change at all, but the predicates should be tautology:
+ // start with the preds passed in from the caller edge
+ // that host the taints, and alter them to have the taint
+ // added, just becoming more specific than edge predicate alone
+
+ Iterator<Taint> itr = ts.iterator();
+ while( itr.hasNext() ) {
+ Taint tCaller = itr.next();
+
+ ExistPredSet predsWithTaint = ExistPredSet.factory();
+
+ Iterator<ExistPred> predItr = predsEdge.iterator();
+ while( predItr.hasNext() ) {
+ ExistPred predEdge = predItr.next();
+
+ predsWithTaint =
+ Canonical.add( predsWithTaint,
+ ExistPred.factory( predEdge.e_tdSrc,
+ predEdge.e_hrnSrcID,
+ predEdge.e_hrnDstID,
+ predEdge.e_type,
+ predEdge.e_field,
+ null,
+ tCaller,
+ predEdge.e_srcOutCalleeContext,
+ predEdge.e_srcOutCallerContext
+ )
+ );
+ }
+
+ Taint tCallee = Canonical.changePredsTo( tCaller,
+ predsWithTaint );
+
+ out = Canonical.add( out,
+ tCallee
+ );
+ }
+
+ assert out.isCanonical();
+ return out;
+ }
+
+
// used below to convert a TaintSet to its caller-context
// equivalent, just eliminate Taints with bad preds
protected TaintSet
),
toCalleeContext( hrnCaller.getAlpha(),
preds,
- oocHrnIdOoc2callee
+ oocHrnIdOoc2callee
),
preds,
hrnCaller.getDescription()
hrnDstCallee.getID(),
reArg.getType(),
reArg.getField(),
- null,
+ null, // state
+ null, // taint
true, // out-of-callee-context
false // out-of-caller-context
);
ExistPredSet preds =
ExistPredSet.factory( pred );
-
- TaintSet taints = TaintSet.factory( reArg.getTaints(),
- preds
- );
RefEdge reCallee =
new RefEdge( vnCallee,
oocHrnIdOoc2callee
),
preds,
- taints
+ toCalleeContext( reArg.getTaints(),
+ preds )
);
rg.addRefEdge( vnCallee,
hrnDstCallee.getID(),
reCaller.getType(),
reCaller.getField(),
- null,
+ null, // state
+ null, // taint
false, // out-of-callee-context
false // out-of-caller-context
);
reCaller.getType(),
reCaller.getField(),
null,
+ null,
outOfCalleeContext,
outOfCallerContext
);
oocHrnIdOoc2callee
),
preds,
- Canonical.changePredsTo( reCaller.getTaints(),
- preds )
+ toCalleeContext( reCaller.getTaints(),
+ preds )
)
);
)
);
+ oocEdgeExisting.setTaints( Canonical.unionORpreds( oocEdgeExisting.getTaints(),
+ toCalleeContext( reCaller.getTaints(),
+ preds
+ )
+ )
+ );
+
HeapRegionNode hrnCalleeAndOutContext =
(HeapRegionNode) oocEdgeExisting.getSrc();
hrnCalleeAndOutContext.setAlpha( Canonical.unionORpreds( hrnCalleeAndOutContext.getAlpha(),
BUILDSCRIPT=~/research/Robust/src/buildscript
BSFLAGS= -mainclass Test -justanalyze -ooojava -disjoint -disjoint-k 1 -enable-assertions
-DEBUGFLAGS= -disjoint-write-dots final -disjoint-write-initial-contexts -disjoint-write-ihms # -disjoint-debug-snap-method main 0 10 true
+DEBUGFLAGS= -disjoint-write-dots final -disjoint-write-initial-contexts -disjoint-write-ihms -disjoint-debug-snap-method main 0 10 true
all: $(PROGRAM).bin
projects / IRC.git / commitdiff