return "allocSite "+disjointId+" ("+id+")";
}
+ public String toStringBrief() {
+ return id.toString();
+ }
+
public String toStringVerbose() {
if( disjointId == null ) {
return "allocSite"+id+" "+
fd.getSymbol(), // field name
alpha, // beta
ExistPredSet.factory(rg.predTrue), // predicates
- null,
null
);
arrayElementFieldName, // field name
alpha, // beta
ExistPredSet.factory(rg.predTrue), // predicates
- null,
null
);
arrayElementFieldName, // field name
alpha, // beta
ExistPredSet.factory(rg.predTrue), // predicates
- null,
null
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
arrayElementFieldName, // field name
alpha, // beta
ExistPredSet.factory(rg.predTrue), // predicates
- null,
null
);
rg.addRefEdge(prevNode, hrnSummary, edgeToSummary);
null, // field name
hrnNewest.getAlpha(), // beta
ExistPredSet.factory(rg.predTrue), // predicates
- null,
null
);
rg.addRefEdge(lnX, hrnNewest, edgeNew);
fd.getSymbol(), // field name
hrnNewest.getAlpha(), // beta
ExistPredSet.factory(rg.predTrue), // predicates
- null, null
+ null
);
rg.addRefEdge(srcHRN, hrnSummary, edgeToSummary);
fd.getType(), // type
fd.getSymbol(), // field name
srcHRN.getAlpha(), // beta
- ExistPredSet.factory(rg.predTrue), // predicates
- null,
+ ExistPredSet.factory(rg.predTrue), // predicates
null
);
rg.addRefEdge(srcHRN, hrnDst, edgeToSummary);
null,
Canonical.intersection( betaY, betaHrn ),
predsTrue,
- null,
null
);
)
),
predsTrue,
- null,
null
);
null, // field name
hrnNewest.getAlpha(), // beta
predsTrue, // predicates
- null, null
+ null
);
addRefEdge( lnX, hrnNewest, edgeNew );
ExistPredSet preds =
ExistPredSet.factory( pred );
- //Taint paramTaint =
- // Taint.factory( 0, null, null, );
+ Taint paramTaint =
+ Taint.factory( index,
+ null,
+ null,
+ hrnDstCallee.getAllocSite()
+ );
- TaintSet paramTaints =
- //TaintSet.factory( paramTaint );
- TaintSet.factory();
+ TaintSet taints =
+ TaintSet.factory( paramTaint );
RefEdge reCallee =
new RefEdge( vnCallee,
oocHrnIdOoc2callee
),
preds,
- paramTaints,
- null
+ taints
);
rg.addRefEdge( vnCallee,
oocHrnIdOoc2callee
),
preds,
- null, null
+ null
);
rg.addRefEdge( hrnSrcCallee,
oocHrnIdOoc2callee
),
preds,
- null, null
+ null
)
);
toCallerContext( reCallee.getBeta(),
calleeStatesSatisfied ),
preds,
- null, null
+ null
);
ChangeSet cs = ChangeSet.factory();
edgeA.getPreds()
)
);
- edgeToMerge.setParamTaints(
- Canonical.union( edgeToMerge.getParamTaints(),
- edgeA.getParamTaints()
- )
- );
- edgeToMerge.setRblockTaints(
- Canonical.union( edgeToMerge.getRblockTaints(),
- edgeA.getRblockTaints()
- )
- );
+ edgeToMerge.setTaints(
+ Canonical.union( edgeToMerge.getTaints(),
+ edgeA.getTaints()
+ )
+ );
}
}
}
edgeA.getPreds()
)
);
- edgeToMerge.setParamTaints(
- Canonical.union( edgeToMerge.getParamTaints(),
- edgeA.getParamTaints()
- )
- );
- edgeToMerge.setRblockTaints(
- Canonical.union( edgeToMerge.getRblockTaints(),
- edgeA.getRblockTaints()
- )
- );
+ edgeToMerge.setTaints(
+ Canonical.union( edgeToMerge.getTaints(),
+ edgeA.getTaints()
+ )
+ );
}
}
}
protected HashSet<ReachTuple> reachTuples;
// existance predicates must be true in a caller
- // context for this node to transfer from this
+ // context for this state to transfer from this
// callee to that context
protected ExistPredSet preds;
// tainted this edge-->meaning which heap roots
// code must have had access to in order to
// read or write through this edge
- protected TaintSet paramTaints;
- protected TaintSet rblockTaints;
+ protected TaintSet taints;
public RefEdge( RefSrcNode src,
String field,
ReachSet beta,
ExistPredSet preds,
- TaintSet paramTaints,
- TaintSet rblockTaints ) {
+ TaintSet taints ) {
assert src != null;
assert dst != null;
// is changing beta info, betaNew is always empty
betaNew = ReachSet.factory();
- if( paramTaints != null ) {
- this.paramTaints = paramTaints;
+ if( taints != null ) {
+ this.taints = taints;
} else {
- this.paramTaints = TaintSet.factory();
- }
-
- if( rblockTaints != null ) {
- this.rblockTaints = rblockTaints;
- } else {
- this.rblockTaints = TaintSet.factory();
+ this.taints = TaintSet.factory();
}
}
field,
beta,
preds,
- paramTaints,
- rblockTaints );
+ taints );
return copy;
}
// beta and preds contribute towards reaching the
// fixed point, so use this method to determine if
// an edge is "equal" to some previous visit, basically
- // AND EDGE TAINTS!
+ // and taints!
public boolean equalsIncludingBetaPredsTaints( RefEdge edge ) {
return equals( edge ) &&
beta.equals( edge.beta ) &&
preds.equals( edge.preds ) &&
- paramTaints.equals( edge.paramTaints ) &&
- rblockTaints.equals( edge.rblockTaints );
+ taints.equals( edge.taints );
}
public boolean equalsPreds( RefEdge edge ) {
}
- public TaintSet getParamTaints() {
- return paramTaints;
- }
-
- public void setParamTaints( TaintSet taints ) {
- this.paramTaints = taints;
- }
-
- public TaintSet getRblockTaints() {
- return rblockTaints;
+ public TaintSet getTaints() {
+ return taints;
}
- public void setRblockTaints( TaintSet taints ) {
- this.rblockTaints = taints;
+ public void setTaints( TaintSet taints ) {
+ this.taints = taints;
}
-
public String toStringDOT( boolean hideReach,
}
if( !hideEdgeTaints ) {
- if( !paramTaints.isEmpty() ) {
- s += "\\npt: "+paramTaints.toString();
- }
-
- if( !rblockTaints.isEmpty() ) {
- s += "\\nrt: "+rblockTaints.toString();
+ if( !taints.isEmpty() ) {
+ s += "\\nt: "+taints.toString();
}
}
}
public String toString() {
- return "";
+ String s = "(";
+
+ if( paramIndex != null ) {
+ s += "param"+paramIndex;
+ } else {
+ s += sese.toPrettyString()+"-"+insetVar;
+ }
+
+ return s+", "+allocSite.toStringBrief()+")";
}
}
--- /dev/null
+PROGRAM=test
+
+SOURCE_FILES=$(PROGRAM).java
+
+BUILDSCRIPT=~/research/Robust/src/buildscript
+
+
+BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 2 -disjoint-write-dots final -enable-assertions
+
+all: $(PROGRAM).bin
+
+view: PNGs
+ eog *.png &
+
+PNGs: DOTs
+ d2p *COMPLETE*.dot
+
+DOTs: $(PROGRAM).bin
+
+$(PROGRAM).bin: $(SOURCE_FILES)
+ $(BUILDSCRIPT) $(BSFLAGS) $(DEBUGFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
+
+clean:
+ rm -f $(PROGRAM).bin
+ rm -fr tmpbuilddirectory
+ rm -f *~
+ rm -f *.dot
+ rm -f *.png
+ rm -f aliases.txt
--- /dev/null
+public class Foo {
+ public Foo() {}
+ public Foo f;
+}
+
+public class Test {
+
+ static public void main( String[] args ) {
+
+ Foo f = new Foo();
+
+ Foo g = doStuff( f );
+ }
+
+ static Foo doStuff( Foo m ) {
+
+ Foo n = new Foo();
+ return n;
+ }
+}