From e455fec2607fd94bb99bc831089ef314a01cf060 Mon Sep 17 00:00:00 2001 From: jjenista Date: Wed, 26 May 2010 22:21:57 +0000 Subject: [PATCH] porting effects analysis to new disjoint analysis --- Robust/src/Analysis/Disjoint/AllocSite.java | 15 +- .../Analysis/Disjoint/DisjointAnalysis.java | 77 ++++++---- .../src/Analysis/Disjoint/HeapRegionNode.java | 33 ++-- Robust/src/Analysis/Disjoint/ReachGraph.java | 141 ++++++++++++++---- Robust/src/Analysis/Disjoint/ReachSet.java | 27 +++- Robust/src/Analysis/Disjoint/RefEdge.java | 92 ++++++++++-- .../Tests/disjoint/predicateTest3/makefile | 7 - Robust/src/Tests/disjoint/simple/test.java | 6 +- 8 files changed, 293 insertions(+), 105 deletions(-) diff --git a/Robust/src/Analysis/Disjoint/AllocSite.java b/Robust/src/Analysis/Disjoint/AllocSite.java index d5020158..7edca4a0 100644 --- a/Robust/src/Analysis/Disjoint/AllocSite.java +++ b/Robust/src/Analysis/Disjoint/AllocSite.java @@ -48,11 +48,13 @@ public class AllocSite extends Canonical { public static AllocSite factory( int allocationDepth, FlatNew flatNew, - String disjointId + String disjointId, + boolean markAsFlagged ) { AllocSite out = new AllocSite( allocationDepth, flatNew, - disjointId ); + disjointId, + markAsFlagged ); out = (AllocSite) Canonical.makeCanonical( out ); return out; } @@ -60,7 +62,8 @@ public class AllocSite extends Canonical { protected AllocSite( int allocationDepth, FlatNew flatNew, - String disjointId + String disjointId, + boolean markAsFlagged ) { assert allocationDepth >= 1; @@ -74,6 +77,9 @@ public class AllocSite extends Canonical { // 1) we have a non-null disjointID (a named flagged site) // OR // 2) the type is a class with Bamboo-parameter flags + // OR + // 3) a client wants to programmatically flag this site, + // such as the OoOJava method effects analysis this.isFlagged = false; if( disjointId != null ) { @@ -83,6 +89,9 @@ public class AllocSite extends Canonical { flatNew.getType().getClassDesc().hasFlags() ) { this.isFlagged = true; + + } else if( markAsFlagged ) { + this.isFlagged = true; } diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index 7834bd77..f9a23098 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -1347,11 +1347,13 @@ public class DisjointAnalysis { ReachGraph rg = (ReachGraph) me.getValue(); rg.writeGraph( "COMPLETE"+d, - true, // write labels (variables) - true, // selectively hide intermediate temp vars - true, // prune unreachable heap regions - true, // hide subset reachability states - true ); // hide edge taints + true, // write labels (variables) + true, // selectively hide intermediate temp vars + true, // prune unreachable heap regions + false, // hide reachability altogether + true, // hide subset reachability states + true, // hide predicates + false ); // hide edge taints } } @@ -1371,8 +1373,10 @@ public class DisjointAnalysis { rg.writeGraph( "IHMPARTFOR"+d+"FROM"+fc2enclosing.get( fc )+fc, true, // write labels (variables) true, // selectively hide intermediate temp vars + true, // hide reachability altogether true, // prune unreachable heap regions - true, // hide subset reachability states + true, // hide subset reachability states + false, // hide predicates true ); // hide edge taints } } @@ -1390,8 +1394,10 @@ public class DisjointAnalysis { true, // write labels (variables) true, // selectively hide intermediate temp vars true, // prune unreachable heap regions - true, // hide subset reachability states - true ); // hide edge taints + false, // hide all reachability + true, // hide subset reachability states + true, // hide predicates + false );// hide edge taints } } @@ -1418,8 +1424,10 @@ public class DisjointAnalysis { true, // write labels (variables) true, // selectively hide intermediate temp vars true, // prune unreachable heap regions - true, // hide subset reachability states - true ); // hide edge taints + false, // hide all reachability + true, // hide subset reachability states + false, // hide predicates + false); // hide edge taints mapDescriptorToNumUpdates.put( d, n + 1 ); } @@ -1433,7 +1441,8 @@ public class DisjointAnalysis { if( !mapFlatNewToAllocSite.containsKey( fnew ) ) { AllocSite as = AllocSite.factory( allocationDepth, fnew, - fnew.getDisjointId() + fnew.getDisjointId(), + false ); // the newest nodes are single objects @@ -1713,7 +1722,8 @@ public class DisjointAnalysis { // create allocation site AllocSite as = AllocSite.factory( allocationDepth, flatNew, - flatNew.getDisjointId() + flatNew.getDisjointId(), + false ); for (int i = 0; i < allocationDepth; ++i) { Integer id = generateUniqueHeapRegionNodeID(); @@ -1785,12 +1795,14 @@ private Set getFieldSetTobeAnalyzed(TypeDescriptor typeDesc){ if(prevNode==null){ // make a new reference between new summary node and source - RefEdge edgeToSummary = new RefEdge(srcHRN, // source + RefEdge edgeToSummary = new RefEdge(srcHRN, // source hrnSummary, // dest typeDesc, // type fd.getSymbol(), // field name alpha, // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, + null ); rg.addRefEdge(srcHRN, hrnSummary, edgeToSummary); @@ -1803,7 +1815,9 @@ private Set getFieldSetTobeAnalyzed(TypeDescriptor typeDesc){ typeDesc, // type arrayElementFieldName, // field name alpha, // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, + null ); rg.addRefEdge(prevNode, hrnSummary, edgeToSummary); @@ -1840,19 +1854,23 @@ private Set getFieldSetTobeAnalyzed(TypeDescriptor typeDesc){ typeDesc, // type arrayElementFieldName, // field name alpha, // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, + null ); rg.addRefEdge(prevNode, hrnSummary, edgeToSummary); prevNode=hrnSummary; }else{ - HeapRegionNode hrnSummary=mapToExistingNode.get(typeDesc); + HeapRegionNode hrnSummary=mapToExistingNode.get(typeDesc); if(prevNode.getReferenceTo(hrnSummary, typeDesc, arrayElementFieldName)==null){ RefEdge edgeToSummary = new RefEdge(prevNode, // source hrnSummary, // dest typeDesc, // type arrayElementFieldName, // field name alpha, // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, + null ); rg.addRefEdge(prevNode, hrnSummary, edgeToSummary); } @@ -1894,7 +1912,9 @@ private ReachGraph createInitialTaskReachGraph(FlatMethod fm) { taskDesc.getParamType(idx), // type null, // field name hrnNewest.getAlpha(), // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, + null ); rg.addRefEdge(lnX, hrnNewest, edgeNew); @@ -1964,7 +1984,8 @@ private ReachGraph createInitialTaskReachGraph(FlatMethod fm) { type, // type fd.getSymbol(), // field name hrnNewest.getAlpha(), // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, null ); rg.addRefEdge(srcHRN, hrnSummary, edgeToSummary); @@ -2005,7 +2026,9 @@ private ReachGraph createInitialTaskReachGraph(FlatMethod fm) { fd.getType(), // type fd.getSymbol(), // field name srcHRN.getAlpha(), // beta - ExistPredSet.factory(rg.predTrue) // predicates + ExistPredSet.factory(rg.predTrue), // predicates + null, + null ); rg.addRefEdge(srcHRN, hrnDst, edgeToSummary); @@ -2196,11 +2219,13 @@ getFlaggedAllocationSitesReachableFromTaskPRIVATE(TaskDescriptor td) { graphName = graphName + fn; } rg.writeGraph( graphName, - true, // write labels (variables) - true, // selectively hide intermediate temp vars - true, // prune unreachable heap regions - true, // hide subset reachability states - true );// hide edge taints + true, // write labels (variables) + true, // selectively hide intermediate temp vars + true, // prune unreachable heap regions + false, // hide reachability + true, // hide subset reachability states + true, // hide predicates + false );// hide edge taints } } diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java index 1a2cab1d..41c877cb 100644 --- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java +++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java @@ -117,12 +117,6 @@ public class HeapRegionNode extends RefSrcNode { } assert isSingleObject == hrn.isSingleObject(); - - if( isFlagged != hrn.isFlagged ) { - System.out.println( this.toStringDOT(true)+"\ndoesn't match\n"+hrn.toStringDOT(true) ); - //throw new Exception("flagged regions don't match"); - } - assert isFlagged == hrn.isFlagged(); assert isNewSummary == hrn.isNewSummary(); assert isOutOfContext == hrn.isOutOfContext(); @@ -296,8 +290,9 @@ public class HeapRegionNode extends RefSrcNode { return description; } - public String toStringDOT( boolean hideSubsetReach ) { - + public String toStringDOT( boolean hideReach, + boolean hideSubsetReach, + boolean hidePreds ) { String attributes = ""; if( isSingleObject ) { @@ -317,13 +312,21 @@ public class HeapRegionNode extends RefSrcNode { typeStr = type.toPrettyString(); } - return new String( "["+attributes+ - ",label=\"ID"+getIDString()+"\\n"+ - typeStr+"\\n"+ - description+"\\n"+ - alpha.toStringEscNewline( hideSubsetReach )+"\\n"+ - preds.toStringEscNewline()+"\"]" - ); + String s = + "["+attributes+ + ",label=\"ID"+getIDString()+"\\n"+ + typeStr+"\\n"+ + description; + + if( !hideReach ) { + s += "\\n"+alpha.toStringEscNewline( hideSubsetReach ); + } + + if( !hidePreds ) { + s += "\\n"+preds.toStringEscNewline(); + } + + return s+"\"]"; } public String toString() { diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 105af437..7fbab6f0 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -456,7 +456,9 @@ public class ReachGraph { tdNewEdge, null, Canonical.intersection( betaY, betaHrn ), - predsTrue + predsTrue, + null, + null ); addEdgeOrMergeWithExisting( edgeNew ); @@ -610,7 +612,9 @@ public class ReachGraph { hrnX.getAlpha() ) ), - predsTrue + predsTrue, + null, + null ); addEdgeOrMergeWithExisting( edgeNew ); @@ -679,7 +683,8 @@ public class ReachGraph { type, // type null, // field name hrnNewest.getAlpha(), // beta - predsTrue // predicates + predsTrue, // predicates + null, null ); addRefEdge( lnX, hrnNewest, edgeNew ); @@ -1647,7 +1652,8 @@ public class ReachGraph { preds, oocHrnIdOoc2callee ), - preds + preds, + null, null ); rg.addRefEdge( vnCallee, @@ -1693,7 +1699,8 @@ public class ReachGraph { preds, oocHrnIdOoc2callee ), - preds + preds, + null, null ); rg.addRefEdge( hrnSrcCallee, @@ -1849,7 +1856,8 @@ public class ReachGraph { preds, oocHrnIdOoc2callee ), - preds + preds, + null, null ) ); @@ -1888,8 +1896,10 @@ public class ReachGraph { rg.writeGraph( debugGraphPrefix+"calleeview", resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, - resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -1904,7 +1914,9 @@ public class ReachGraph { private static boolean resolveMethodDebugDOTwriteLabels = true; private static boolean resolveMethodDebugDOTselectTemps = true; private static boolean resolveMethodDebugDOTpruneGarbage = true; + private static boolean resolveMethodDebugDOThideReach = true; private static boolean resolveMethodDebugDOThideSubsetReach = true; + private static boolean resolveMethodDebugDOThidePreds = true; private static boolean resolveMethodDebugDOThideEdgeTaints = true; static String debugGraphPrefix; @@ -1934,14 +1946,18 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); writeGraph( debugGraphPrefix+"caller00In", resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints, callerNodeIDsCopiedToCallee ); } @@ -2183,7 +2199,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2219,7 +2237,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2289,7 +2309,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2398,7 +2420,8 @@ public class ReachGraph { reCallee.getField(), toCallerContext( reCallee.getBeta(), calleeStatesSatisfied ), - preds + preds, + null, null ); ChangeSet cs = ChangeSet.factory(); @@ -2482,7 +2505,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2511,7 +2536,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2614,7 +2641,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2641,7 +2670,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } @@ -2657,7 +2688,9 @@ public class ReachGraph { resolveMethodDebugDOTwriteLabels, resolveMethodDebugDOTselectTemps, resolveMethodDebugDOTpruneGarbage, + resolveMethodDebugDOThideReach, resolveMethodDebugDOThideSubsetReach, + resolveMethodDebugDOThidePreds, resolveMethodDebugDOThideEdgeTaints ); } } @@ -3990,12 +4023,14 @@ public class ReachGraph { // the default signature for quick-and-dirty debugging public void writeGraph( String graphName ) { writeGraph( graphName, - true, // write labels - true, // label select - true, // prune garbage - true, // hide subset reachability - true, // hide edge taints - null // in-context boundary + true, // write labels + true, // label select + true, // prune garbage + false, // hide reachability + true, // hide subset reachability + true, // hide predicates + true, // hide edge taints + null // in-context boundary ); } @@ -4003,14 +4038,18 @@ public class ReachGraph { boolean writeLabels, boolean labelSelect, boolean pruneGarbage, + boolean hideReachability, boolean hideSubsetReachability, + boolean hidePredicates, boolean hideEdgeTaints ) { writeGraph( graphName, writeLabels, labelSelect, pruneGarbage, + hideReachability, hideSubsetReachability, + hidePredicates, hideEdgeTaints, null ); } @@ -4019,7 +4058,9 @@ public class ReachGraph { boolean writeLabels, boolean labelSelect, boolean pruneGarbage, + boolean hideReachability, boolean hideSubsetReachability, + boolean hidePredicates, boolean hideEdgeTaints, Set callerNodeIDsCopiedToCallee ) { @@ -4048,10 +4089,12 @@ public class ReachGraph { HeapRegionNode hrn = (HeapRegionNode) me.getValue(); if( callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) { - bw.write( " "+hrn.toString()+ - hrn.toStringDOT( hideSubsetReachability )+ - ";\n" ); - + bw.write( " "+ + hrn.toString()+ + hrn.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates )+ + ";\n" ); } } @@ -4080,7 +4123,9 @@ public class ReachGraph { bw, null, visited, + hideReachability, hideSubsetReachability, + hidePredicates, hideEdgeTaints, callerNodeIDsCopiedToCallee ); } @@ -4118,14 +4163,20 @@ public class ReachGraph { bw, null, visited, + hideReachability, hideSubsetReachability, + hidePredicates, hideEdgeTaints, callerNodeIDsCopiedToCallee ); } bw.write( " "+vn.toString()+ " -> "+hrn.toString()+ - edge.toStringDOT( hideSubsetReachability, "" )+ + edge.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates, + hideEdgeTaints, + "" )+ ";\n" ); } } @@ -4139,14 +4190,17 @@ public class ReachGraph { } } - protected void traverseHeapRegionNodes( HeapRegionNode hrn, - BufferedWriter bw, - TempDescriptor td, - Set visited, - boolean hideSubsetReachability, - boolean hideEdgeTaints, - Set callerNodeIDsCopiedToCallee - ) throws java.io.IOException { + protected void + traverseHeapRegionNodes( HeapRegionNode hrn, + BufferedWriter bw, + TempDescriptor td, + Set visited, + boolean hideReachability, + boolean hideSubsetReachability, + boolean hidePredicates, + boolean hideEdgeTaints, + Set callerNodeIDsCopiedToCallee + ) throws java.io.IOException { if( visited.contains( hrn ) ) { return; @@ -4159,8 +4213,11 @@ public class ReachGraph { if( callerNodeIDsCopiedToCallee == null || !callerNodeIDsCopiedToCallee.contains( hrn.getID() ) ) { - bw.write( " "+hrn.toString()+ - hrn.toStringDOT( hideSubsetReachability )+ + bw.write( " "+ + hrn.toString()+ + hrn.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates )+ ";\n" ); } @@ -4177,25 +4234,41 @@ public class ReachGraph { ) { bw.write( " "+hrn.toString()+ " -> "+hrnChild.toString()+ - edge.toStringDOT( hideSubsetReachability, ",color=blue" )+ + edge.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates, + hideEdgeTaints, + ",color=blue" )+ ";\n"); } else if( !callerNodeIDsCopiedToCallee.contains( hrnSrc.getID() ) && callerNodeIDsCopiedToCallee.contains( edge.getDst().getID() ) ) { bw.write( " "+hrn.toString()+ " -> "+hrnChild.toString()+ - edge.toStringDOT( hideSubsetReachability, ",color=blue,style=dashed" )+ + edge.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates, + hideEdgeTaints, + ",color=blue,style=dashed" )+ ";\n"); } else { bw.write( " "+hrn.toString()+ " -> "+hrnChild.toString()+ - edge.toStringDOT( hideSubsetReachability, "" )+ + edge.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates, + hideEdgeTaints, + "" )+ ";\n"); } } else { bw.write( " "+hrn.toString()+ " -> "+hrnChild.toString()+ - edge.toStringDOT( hideSubsetReachability, "" )+ + edge.toStringDOT( hideReachability, + hideSubsetReachability, + hidePredicates, + hideEdgeTaints, + "" )+ ";\n"); } @@ -4203,7 +4276,9 @@ public class ReachGraph { bw, td, visited, + hideReachability, hideSubsetReachability, + hidePredicates, hideEdgeTaints, callerNodeIDsCopiedToCallee ); } diff --git a/Robust/src/Analysis/Disjoint/ReachSet.java b/Robust/src/Analysis/Disjoint/ReachSet.java index e299f71a..ea2ca6d8 100644 --- a/Robust/src/Analysis/Disjoint/ReachSet.java +++ b/Robust/src/Analysis/Disjoint/ReachSet.java @@ -208,18 +208,31 @@ public class ReachSet extends Canonical { } public String toString( boolean hideSubsetReachability ) { + + ReachSet toPrint = this; + + if( hideSubsetReachability ) { + // make a new reach set with subset states removed + toPrint = ReachSet.factory(); + + Iterator i = this.iterator(); + while( i.hasNext() ) { + ReachState state = i.next(); + + if( containsStrictSuperSet( state ) ) { + continue; + } + + toPrint = Canonical.add( toPrint, state ); + } + } + String s = "["; - Iterator i = this.iterator(); + Iterator i = toPrint.iterator(); while( i.hasNext() ) { ReachState state = i.next(); - // skip this if there is a superset already - if( hideSubsetReachability && - containsStrictSuperSet( state ) ) { - continue; - } - s += state; if( i.hasNext() ) { s += "\n"; diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java index 8d8e09b0..54f6f5ab 100644 --- a/Robust/src/Analysis/Disjoint/RefEdge.java +++ b/Robust/src/Analysis/Disjoint/RefEdge.java @@ -25,13 +25,25 @@ public class RefEdge { // do not factor into edge comparisons protected ExistPredSet preds; + // taint sets indicate which heap roots have + // 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; + public RefEdge( RefSrcNode src, HeapRegionNode dst, TypeDescriptor type, String field, ReachSet beta, - ExistPredSet preds ) { + ExistPredSet preds, + TaintSet paramTaints, + TaintSet rblockTaints ) { + + assert src != null; + assert dst != null; assert type != null; this.src = src; @@ -42,7 +54,6 @@ public class RefEdge { if( preds != null ) { this.preds = preds; } else { - // TODO: do this right? this.preds = ExistPredSet.factory(); } @@ -55,6 +66,18 @@ public class RefEdge { // when edges are not undergoing an operation that // is changing beta info, betaNew is always empty betaNew = ReachSet.factory(); + + if( paramTaints != null ) { + this.paramTaints = paramTaints; + } else { + this.paramTaints = TaintSet.factory(); + } + + if( rblockTaints != null ) { + this.rblockTaints = rblockTaints; + } else { + this.rblockTaints = TaintSet.factory(); + } } @@ -64,7 +87,9 @@ public class RefEdge { type, field, beta, - preds ); + preds, + paramTaints, + rblockTaints ); return copy; } @@ -102,10 +127,13 @@ public class RefEdge { // 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 - public boolean equalsIncludingBetaAndPreds( RefEdge edge ) { + // AND EDGE TAINTS! + public boolean equalsIncludingBetaPredsTaints( RefEdge edge ) { return equals( edge ) && beta.equals( edge.beta ) && - preds.equals( edge.preds ); + preds.equals( edge.preds ) && + paramTaints.equals( edge.paramTaints ) && + rblockTaints.equals( edge.rblockTaints ); } public boolean equalsPreds( RefEdge edge ) { @@ -113,6 +141,15 @@ public class RefEdge { } + // this method SPECIFICALLY does not use the + // beta/preds/taints in the hash code--it uses + // the same fields as normal equals. Again, + // there are two meanings of equality for edges, + // one is "this edge is the same edge object" like when + // deciding if an edge is already in a set, which + // is represented by this hashcode. The other + // meaning is "this edge equals an edge from another + // graph that is abstractly the same edge" public int hashCode() { int hash = 0; @@ -220,15 +257,44 @@ public class RefEdge { } - public String toStringDOT( boolean hideSubsetReach, + public TaintSet getParamTaints() { + return paramTaints; + } + + public TaintSet getRblockTaints() { + return rblockTaints; + } + + + + public String toStringDOT( boolean hideReach, + boolean hideSubsetReach, + boolean hidePreds, + boolean hideEdgeTaints, String otherAttributes ) { - return new String( "[label=\""+ - type.toPrettyString()+"\\n"+ - field+"\\n"+ - beta.toStringEscNewline( hideSubsetReach )+"\\n"+ - preds.toStringEscNewline()+"\",decorate"+ - otherAttributes+"]" - ); + String s = + "[label=\""+ + type.toPrettyString()+"\\n"+ + field; + if( !hideReach ) { + s += "\\n"+beta.toStringEscNewline( hideSubsetReach ); + } + + if( !hidePreds ) { + s += "\\n"+preds.toStringEscNewline(); + } + + if( !hideEdgeTaints ) { + if( !paramTaints.isEmpty() ) { + s += "\\npt: "+paramTaints.toString(); + } + + if( !rblockTaints.isEmpty() ) { + s += "\\nrt: "+rblockTaints.toString(); + } + } + + return s+"\",decorate"+otherAttributes+"]"; } public String toString() { diff --git a/Robust/src/Tests/disjoint/predicateTest3/makefile b/Robust/src/Tests/disjoint/predicateTest3/makefile index fa33ee55..ac171076 100644 --- a/Robust/src/Tests/disjoint/predicateTest3/makefile +++ b/Robust/src/Tests/disjoint/predicateTest3/makefile @@ -4,13 +4,6 @@ SOURCE_FILES=$(PROGRAM).java BUILDSCRIPT=~/research/Robust/src/buildscript -#DEBUGFLAGS= -disjoint-debug-callsite Bar addSomething 1 -#DEBUGFLAGS= -disjoint-debug-callsite Foo main 1 -#DEBUGFLAGS= -disjoint-debug-callsite main analysisEntryMethod 1 -DEBUGFLAGS= -disjoint-debug-callsite addSomething main 100 -#DEBUGFLAGS= -disjoint-debug-callsite addBar addSomething 1 -#DEBUGFLAGS= -disjoint-debug-callsite Bar addBar 1 - BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 2 -disjoint-write-dots final -disjoint-write-ihms -disjoint-alias-file aliases.txt normal -enable-assertions all: $(PROGRAM).bin diff --git a/Robust/src/Tests/disjoint/simple/test.java b/Robust/src/Tests/disjoint/simple/test.java index c0f6cc7f..a9ced8b4 100644 --- a/Robust/src/Tests/disjoint/simple/test.java +++ b/Robust/src/Tests/disjoint/simple/test.java @@ -7,8 +7,12 @@ public class Test { static public void main( String[] args ) { Foo a = disjoint A new Foo(); Foo b = disjoint B new Foo(); + f0( a, b ); + } + + static public void f0( Foo a, Foo b ) { a.f = b; - f1( b ); + f1( b ); } static public void f1( Foo c ) { -- 2.34.1