From a4e8e0a1b2d129c1b41ad32a474fd4957500840b Mon Sep 17 00:00:00 2001 From: jjenista Date: Thu, 4 Feb 2010 23:57:11 +0000 Subject: [PATCH] implementing --- .../Analysis/Disjoint/DisjointAnalysis.java | 36 ++++- .../src/Analysis/Disjoint/ExistPredEdge.java | 21 ++- .../src/Analysis/Disjoint/ExistPredNode.java | 2 +- .../src/Analysis/Disjoint/ExistPredSet.java | 20 ++- .../src/Analysis/Disjoint/ExistPredTrue.java | 23 +++ .../src/Analysis/Disjoint/HeapRegionNode.java | 57 ++++--- Robust/src/Analysis/Disjoint/ReachGraph.java | 151 ++++++++++-------- Robust/src/Analysis/Disjoint/ReachSet.java | 2 +- Robust/src/Analysis/Disjoint/RefEdge.java | 48 ++---- Robust/src/IR/State.java | 1 + Robust/src/Main/Main.java | 9 ++ .../Tests/disjoint/predicateTest1/makefile | 2 +- .../Tests/disjoint/predicateTest2/makefile | 27 ++++ .../Tests/disjoint/predicateTest2/test.java | 31 ++++ 14 files changed, 285 insertions(+), 145 deletions(-) create mode 100644 Robust/src/Analysis/Disjoint/ExistPredTrue.java create mode 100644 Robust/src/Tests/disjoint/predicateTest2/makefile create mode 100644 Robust/src/Tests/disjoint/predicateTest2/test.java diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index 94c9de6e..dc431cc2 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -201,7 +201,11 @@ public class DisjointAnalysis { if( writeFinalDOTs && !writeAllIncrementalDOTs ) { writeFinalGraphs(); - } + } + + if( state.DISJOINTWRITEIHMS ) { + writeFinalIHMs(); + } if( state.DISJOINTALIASFILE != null ) { if( state.TASK ) { @@ -660,7 +664,7 @@ public class DisjointAnalysis { ReachGraph rg = (ReachGraph) me.getValue(); try { - rg.writeGraph( d+"COMPLETE", + rg.writeGraph( "COMPLETE"+d, true, // write labels (variables) true, // selectively hide intermediate temp vars true, // prune unreachable heap regions @@ -670,8 +674,36 @@ public class DisjointAnalysis { } catch( IOException e ) {} } } + + private void writeFinalIHMs() { + Iterator d2IHMsItr = mapDescriptorToIHMcontributions.entrySet().iterator(); + while( d2IHMsItr.hasNext() ) { + Map.Entry me1 = (Map.Entry) d2IHMsItr.next(); + Descriptor d = (Descriptor) me1.getKey(); + Hashtable IHMs = (Hashtable) me1.getValue(); + + Iterator fc2rgItr = IHMs.entrySet().iterator(); + while( fc2rgItr.hasNext() ) { + Map.Entry me2 = (Map.Entry) fc2rgItr.next(); + FlatCall fc = (FlatCall) me2.getKey(); + ReachGraph rg = (ReachGraph) me2.getValue(); + + try { + rg.writeGraph( "IHMPARTFOR"+d+"FROM"+fc, + true, // write labels (variables) + true, // selectively hide intermediate temp vars + true, // prune unreachable heap regions + false, // show back edges to confirm graph validity + true, // hide subset reachability states + true ); // hide edge taints + } catch( IOException e ) {} + } + } + } + + // return just the allocation site associated with one FlatNew node protected AllocSite getAllocSiteFromFlatNewPRIVATE( FlatNew fnew ) { diff --git a/Robust/src/Analysis/Disjoint/ExistPredEdge.java b/Robust/src/Analysis/Disjoint/ExistPredEdge.java index ffe598dc..ee0f188e 100644 --- a/Robust/src/Analysis/Disjoint/ExistPredEdge.java +++ b/Robust/src/Analysis/Disjoint/ExistPredEdge.java @@ -10,7 +10,7 @@ import java.io.*; // The reach state may be null--if not the predicate is // satisfied when the edge exists AND it has the state. -public class ExistPredEdge extends Canonical { +public class ExistPredEdge extends ExistPred { // the source of an edge is *either* a variable // node or a heap region node @@ -35,10 +35,13 @@ public class ExistPredEdge extends Canonical { String field, ReachState state ) { - assert (vnSrc == null) || (hrnSrcID == null); + assert (tdSrc == null) || (hrnSrcID == null); assert hrnDstID != null; assert type != null; - assert field != null; + + // fields can be null when the edge is from + // a variable node to a heap region! + // assert field != null; this.tdSrc = tdSrc; this.hrnSrcID = hrnSrcID; @@ -132,8 +135,14 @@ public class ExistPredEdge extends Canonical { return false; } - if( !field.equals( epn.field ) ) { - return false; + if( field == null ) { + if( epn.field != null ) { + return false; + } + } else { + if( !field.equals( epn.field ) ) { + return false; + } } // ReachState objects are cannonical @@ -155,7 +164,7 @@ public class ExistPredEdge extends Canonical { hash += hrnSrcID.hashCode()*11; } - hash += hrnDst.hashCode(); + hash += hrnDstID.hashCode(); if( state != null ) { hash += state.hashCode(); diff --git a/Robust/src/Analysis/Disjoint/ExistPredNode.java b/Robust/src/Analysis/Disjoint/ExistPredNode.java index 6ef0a6e9..4a2d610a 100644 --- a/Robust/src/Analysis/Disjoint/ExistPredNode.java +++ b/Robust/src/Analysis/Disjoint/ExistPredNode.java @@ -10,7 +10,7 @@ import java.io.*; // The reach state may be null--if not the predicate is // satisfied when the edge exists AND it has the state. -public class ExistPredNode extends Canonical { +public class ExistPredNode extends ExistPred { protected Integer hrnID; protected ReachState state; diff --git a/Robust/src/Analysis/Disjoint/ExistPredSet.java b/Robust/src/Analysis/Disjoint/ExistPredSet.java index a538ef0d..75d0dfe8 100644 --- a/Robust/src/Analysis/Disjoint/ExistPredSet.java +++ b/Robust/src/Analysis/Disjoint/ExistPredSet.java @@ -17,6 +17,12 @@ public class ExistPredSet extends Canonical { preds = new HashSet(); } + public ExistPredSet( ExistPred ep ) { + preds = new HashSet(); + preds.add( ep ); + } + + public ExistPredSet makeCanonical() { return (ExistPredSet) ExistPredSet.makeCanonical( this ); } @@ -26,16 +32,24 @@ public class ExistPredSet extends Canonical { preds.add( pred ); } + + public ExistPredSet join( ExistPredSet eps ) { + this.preds.addAll( eps.preds ); + return this; + } + + public boolean isSatisfiedBy( ReachGraph rg ) { Iterator predItr = preds.iterator(); while( predItr.hasNext() ) { - if( !predItr.next().isSatisfiedBy( rg ) ) { - return false; + if( predItr.next().isSatisfiedBy( rg ) ) { + return true; } } - return true; + return false; } + public String toString() { String s = "P["; Iterator predItr = preds.iterator(); diff --git a/Robust/src/Analysis/Disjoint/ExistPredTrue.java b/Robust/src/Analysis/Disjoint/ExistPredTrue.java new file mode 100644 index 00000000..69812847 --- /dev/null +++ b/Robust/src/Analysis/Disjoint/ExistPredTrue.java @@ -0,0 +1,23 @@ +package Analysis.Disjoint; + +import IR.*; +import IR.Flat.*; +import java.util.*; +import java.io.*; + +// these existence predicates on elements of +// a callee graph allow a caller to prune the +// pieces of the graph that don't apply when +// predicates are not satisfied in the +// caller's context + +public class ExistPredTrue extends ExistPred { + + public boolean isSatisfiedBy( ReachGraph rg ) { + return true; + } + + public String toString() { + return "t"; + } +} diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java index 0d014b21..3aba2390 100644 --- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java +++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java @@ -12,10 +12,6 @@ public class HeapRegionNode extends RefSrcNode { protected boolean isFlagged; protected boolean isNewSummary; - // clean means that the node existed - // before the current analysis context - protected boolean isClean; - // special nodes that represent heap parts // outside of the current method context protected boolean isOutOfContext; @@ -49,7 +45,6 @@ public class HeapRegionNode extends RefSrcNode { boolean isSingleObject, boolean isFlagged, boolean isNewSummary, - boolean isClean, boolean isOutOfContext, TypeDescriptor type, AllocSite allocSite, @@ -63,7 +58,6 @@ public class HeapRegionNode extends RefSrcNode { this.isSingleObject = isSingleObject; this.isFlagged = isFlagged; this.isNewSummary = isNewSummary; - this.isClean = isClean; this.isOutOfContext = isOutOfContext; this.type = type; this.allocSite = allocSite; @@ -81,7 +75,6 @@ public class HeapRegionNode extends RefSrcNode { isSingleObject, isFlagged, isNewSummary, - isClean, isOutOfContext, type, allocSite, @@ -125,7 +118,6 @@ public class HeapRegionNode extends RefSrcNode { assert isSingleObject == hrn.isSingleObject(); assert isFlagged == hrn.isFlagged(); assert isNewSummary == hrn.isNewSummary(); - assert isClean == hrn.isClean(); assert isOutOfContext == hrn.isOutOfContext(); assert description.equals( hrn.getDescription() ); @@ -153,14 +145,6 @@ public class HeapRegionNode extends RefSrcNode { return isOutOfContext; } - public boolean isClean() { - return isClean; - } - - public void setIsClean( boolean isClean ) { - this.isClean = isClean; - } - public Iterator iteratorToReferencers() { return referencers.iterator(); @@ -246,6 +230,15 @@ public class HeapRegionNode extends RefSrcNode { } + public ExistPredSet getPreds() { + return preds; + } + + public void setPreds( ExistPredSet preds ) { + this.preds = preds; + } + + public String getIDString() { String s; @@ -258,19 +251,33 @@ public class HeapRegionNode extends RefSrcNode { return s; } - public String getAlphaString( boolean hideSubsetReachability ) { - return alpha.toStringEscapeNewline( hideSubsetReachability ); - } + public String getDescription() { + return description; + } + + public String toStringDOT( boolean hideSubsetReach ) { + String attributes = ""; + + if( isSingleObject ) { + attributes += "shape=box"; + } else { + attributes += "shape=Msquare"; + } - public String getPredString() { - return preds.toString(); + if( isFlagged ) { + attributes += ",style=filled,fillcolor=lightgrey"; + } + + return new String( "["+attributes+ + ",label=\"ID"+getIDString()+"\\n"+ + type.toPrettyString()+"\\n"+ + description+"\\n"+ + alpha.toStringEscNewline( hideSubsetReach )+"\\n"+ + preds+"\"]" + ); } public String toString() { return "HRN"+getIDString(); } - - public String getDescription() { - return description; - } } diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 7775e642..3fc32666 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -21,7 +21,9 @@ public class ReachGraph { protected static final ReachSet rsetWithEmptyState = new ReachSet( rstateEmpty ).makeCanonical(); // predicate constants - protected static final ExistPredSet predsEmpty = new ExistPredSet().makeCanonical(); + protected static final ExistPredTrue predTrue = new ExistPredTrue(); + protected static final ExistPredSet predsEmpty = new ExistPredSet().makeCanonical(); + protected static final ExistPredSet predsTrue = new ExistPredSet( predTrue ).makeCanonical(); // from DisjointAnalysis for convenience @@ -71,7 +73,6 @@ public class ReachGraph { boolean isSingleObject, boolean isNewSummary, boolean isFlagged, - boolean isClean, boolean isOutOfContext, TypeDescriptor type, AllocSite allocSite, @@ -117,7 +118,7 @@ public class ReachGraph { } if( preds == null ) { - // TODO: do this right? + // TODO: do this right? For out-of-context nodes? preds = new ExistPredSet().makeCanonical(); } @@ -125,7 +126,6 @@ public class ReachGraph { isSingleObject, markForAnalysis, isNewSummary, - isClean, isOutOfContext, typeToUse, allocSite, @@ -361,9 +361,8 @@ public class ReachGraph { hrnHrn, tdNewEdge, null, - false, betaY.intersection( betaHrn ), - predsEmpty + predsTrue ); addRefEdge( lnX, hrnHrn, edgeNew ); @@ -509,9 +508,8 @@ public class ReachGraph { hrnY, tdNewEdge, f.getSymbol(), - false, edgeY.getBeta().pruneBy( hrnX.getAlpha() ), - predsEmpty + predsTrue ); // look to see if an edge with same field exists @@ -524,9 +522,9 @@ public class ReachGraph { edgeExisting.setBeta( edgeExisting.getBeta().union( edgeNew.getBeta() ) ); - // we touched this edge in the current context - // so dirty it - edgeExisting.setIsClean( false ); + edgeExisting.setPreds( + edgeExisting.getPreds().join( edgeNew.getPreds() ) + ); } else { addRefEdge( hrnX, hrnY, edgeNew ); @@ -595,9 +593,8 @@ public class ReachGraph { hrnNewest, // dest type, // type null, // field name - false, // is initial param hrnNewest.getAlpha(), // beta - predsEmpty // predicates + predsTrue // predicates ); addRefEdge( lnX, hrnNewest, edgeNew ); @@ -689,7 +686,9 @@ public class ReachGraph { // after tokens have been aged, reset newest node's reachability + // and a brand new node has a "true" predicate hrn0.setAlpha( hrn0.getInherent() ); + hrn0.setPreds( predsTrue ); } @@ -722,7 +721,6 @@ public class ReachGraph { false, // single object? true, // summary? hasFlags, // flagged? - false, // clean? false, // out-of-context? as.getType(), // type as, // allocation site @@ -740,7 +738,6 @@ public class ReachGraph { true, // single object? false, // summary? hasFlags, // flagged? - false, // clean? false, // out-of-context? as.getType(), // type as, // allocation site @@ -778,7 +775,6 @@ public class ReachGraph { false, // single object? true, // summary? hasFlags, // flagged? - false, // clean? false, // out-of-context? as.getType(), // type as, // allocation site @@ -796,7 +792,6 @@ public class ReachGraph { true, // single object? false, // summary? hasFlags, // flagged? - false, // clean? false, // out-of-context? as.getType(), // type as, // allocation site @@ -836,6 +831,7 @@ public class ReachGraph { // otherwise an edge from the referencer to hrnSummary exists already // and the edge referencer->hrn should be merged with it edgeMerged.setBeta( edgeMerged.getBeta().union( edgeSummary.getBeta() ) ); + edgeMerged.setPreds( edgeMerged.getPreds().join( edgeSummary.getPreds() ) ); } addRefEdge( hrnSummary, hrnReferencee, edgeMerged ); @@ -861,6 +857,7 @@ public class ReachGraph { // otherwise an edge from the referencer to alpha_S exists already // and the edge referencer->alpha_K should be merged with it edgeMerged.setBeta( edgeMerged.getBeta().union( edgeSummary.getBeta() ) ); + edgeMerged.setPreds( edgeMerged.getPreds().join( edgeSummary.getPreds() ) ); } addRefEdge( onReferencer, hrnSummary, edgeMerged ); @@ -899,8 +896,9 @@ public class ReachGraph { addRefEdge( onReferencer, hrnB, edgeNew ); } - // replace hrnB reachability with hrnA's + // replace hrnB reachability and preds with hrnA's hrnB.setAlpha( hrnA.getAlpha() ); + hrnB.setPreds( hrnA.getPreds() ); } @@ -1122,8 +1120,8 @@ public class ReachGraph { VariableNode vnCaller = this.getVariableNodeFromTemp( tdArg ); VariableNode vnCallee = rg.getVariableNodeFromTemp( tdParam ); - // now traverse the caller view using the argument to - // build the callee view which has the parameter symbol + // now traverse the calleR view using the argument to + // build the calleE view which has the parameter symbol Set toVisitInCaller = new HashSet(); Set visitedInCaller = new HashSet(); toVisitInCaller.add( vnCaller ); @@ -1135,38 +1133,51 @@ public class ReachGraph { toVisitInCaller.remove( rsnCaller ); visitedInCaller.add( rsnCaller ); - // FIRST - setup the source end of an edge + // FIRST - setup the source end of an edge, and + // remember the identifying info of the source + // to build predicates + TempDescriptor tdSrc = null; + Integer hrnSrcID = null; if( rsnCaller == vnCaller ) { // if the caller node is the param symbol, we // have to do this translation for the callee rsnCallee = vnCallee; + tdSrc = tdArg; + } else { // otherwise the callee-view node is a heap // region with the same ID, that may or may // not have been created already assert rsnCaller instanceof HeapRegionNode; - HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller; + HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller; hrnSrcID = hrnSrcCaller.getID(); if( !callerNodesCopiedToCallee.contains( rsnCaller ) ) { + + ExistPredNode pred = + new ExistPredNode( hrnSrcID, null ); + + ExistPredSet preds = new ExistPredSet(); + preds.add( pred ); + rsnCallee = rg.createNewHeapRegionNode( hrnSrcCaller.getID(), hrnSrcCaller.isSingleObject(), hrnSrcCaller.isNewSummary(), hrnSrcCaller.isFlagged(), - true, // clean? false, // out-of-context? hrnSrcCaller.getType(), hrnSrcCaller.getAllocSite(), toShadowTokens( this, hrnSrcCaller.getInherent() ), toShadowTokens( this, hrnSrcCaller.getAlpha() ), - predsEmpty, + preds, hrnSrcCaller.getDescription() ); callerNodesCopiedToCallee.add( rsnCaller ); + } else { - rsnCallee = rg.id2hrn.get( hrnSrcCaller.getID() ); + rsnCallee = rg.id2hrn.get( hrnSrcID ); } } @@ -1179,38 +1190,56 @@ public class ReachGraph { HeapRegionNode hrnCallee; // THIRD - setup destination ends of edges + Integer hrnDstID = hrnCaller.getID(); if( !callerNodesCopiedToCallee.contains( hrnCaller ) ) { + + ExistPredNode pred = + new ExistPredNode( hrnDstID, null ); + + ExistPredSet preds = new ExistPredSet(); + preds.add( pred ); + hrnCallee = rg.createNewHeapRegionNode( hrnCaller.getID(), hrnCaller.isSingleObject(), hrnCaller.isNewSummary(), hrnCaller.isFlagged(), - true, // clean? false, // out-of-context? hrnCaller.getType(), hrnCaller.getAllocSite(), toShadowTokens( this, hrnCaller.getInherent() ), toShadowTokens( this, hrnCaller.getAlpha() ), - predsEmpty, + preds, hrnCaller.getDescription() ); callerNodesCopiedToCallee.add( hrnCaller ); } else { - hrnCallee = rg.id2hrn.get( hrnCaller.getID() ); + hrnCallee = rg.id2hrn.get( hrnDstID ); } // FOURTH - copy edge over if needed if( !callerEdgesCopiedToCallee.contains( reCaller ) ) { + + ExistPredEdge pred = + new ExistPredEdge( tdSrc, + hrnSrcID, + hrnDstID, + reCaller.getType(), + reCaller.getField(), + null ); + + ExistPredSet preds = new ExistPredSet(); + preds.add( pred ); + rg.addRefEdge( rsnCallee, hrnCallee, new RefEdge( rsnCallee, hrnCallee, reCaller.getType(), reCaller.getField(), - true, // clean? toShadowTokens( this, reCaller.getBeta() ), - predsEmpty + preds ) ); callerEdgesCopiedToCallee.add( reCaller ); @@ -1261,7 +1290,6 @@ public class ReachGraph { false, // single object? false, // new summary? false, // flagged? - true, // clean? true, // out-of-context? hrnCallerAndOutContext.getType(), null, // alloc site, shouldn't be used @@ -1280,7 +1308,6 @@ public class ReachGraph { hrnCalleeAndInContext, edgeMightCross.getType(), edgeMightCross.getField(), - true, // clean? toShadowTokens( this, edgeMightCross.getBeta() ), predsEmpty ) @@ -1293,7 +1320,7 @@ public class ReachGraph { rg.writeGraph( "calleeview", true, true, true, false, true, true ); } catch( IOException e ) {} - if( fc.getMethod().getSymbol().equals( "f1" ) ) { + if( fc.getMethod().getSymbol().equals( "addSomething" ) ) { System.exit( 0 ); } @@ -1738,10 +1765,12 @@ public class ReachGraph { hrnB.setAlpha( hrnB.getAlpha().union( hrnA.getAlpha() ) ); // if hrnB is already dirty or hrnA is dirty, - // the hrnB should end up dirty + // the hrnB should end up dirty: TODO + /* if( !hrnA.isClean() ) { hrnB.setIsClean( false ); } + */ } } @@ -1817,9 +1846,12 @@ public class ReachGraph { edgeToMerge.setBeta( edgeToMerge.getBeta().union( edgeA.getBeta() ) ); + // TODO: what? + /* if( !edgeA.isClean() ) { edgeToMerge.setIsClean( false ); } + */ } } } @@ -1878,9 +1910,12 @@ public class ReachGraph { edgeToMerge.setBeta( edgeToMerge.getBeta().union( edgeA.getBeta() ) ); + // TODO: what? + /* if( !edgeA.isClean() ) { edgeToMerge.setIsClean( false ); } + */ } } } @@ -2299,8 +2334,6 @@ public class ReachGraph { continue; } } - - //bw.write(" "+vn.toString() + ";\n"); Iterator heapRegionsItr = vn.iteratorToReferencees(); while( heapRegionsItr.hasNext() ) { @@ -2317,10 +2350,10 @@ public class ReachGraph { hideEdgeTaints ); } - bw.write( " " + vn.toString() + - " -> " + hrn.toString() + - "[label=\"" + edge.toGraphEdgeString( hideSubsetReachability ) + - "\",decorate];\n" ); + bw.write( " "+vn.toString()+ + " -> "+hrn.toString()+ + edge.toStringDOT( hideSubsetReachability )+ + ";\n" ); } } } @@ -2343,43 +2376,19 @@ public class ReachGraph { } visited.add( hrn ); - String attributes = "["; - - if( hrn.isSingleObject() ) { - attributes += "shape=box"; - } else { - attributes += "shape=Msquare"; - } - - if( hrn.isFlagged() ) { - attributes += ",style=filled,fillcolor=lightgrey"; - } - - attributes += ",label=\"ID" + - hrn.getID() + - "\\n"; - - if( hrn.getType() != null ) { - attributes += hrn.getType().toPrettyString()+"\\n"; - } - - attributes += hrn.getDescription()+ - "\\n"+hrn.getAlphaString( hideSubsetReachability )+ - "\\n"+hrn.getPredString()+ - "\"]"; - - bw.write( " "+hrn.toString()+attributes+";\n" ); - + bw.write( " "+hrn.toString()+ + hrn.toStringDOT( hideSubsetReachability )+ + ";\n" ); Iterator childRegionsItr = hrn.iteratorToReferencees(); while( childRegionsItr.hasNext() ) { RefEdge edge = childRegionsItr.next(); HeapRegionNode hrnChild = edge.getDst(); - bw.write( " " +hrn.toString()+ - " -> " +hrnChild.toString()+ - "[label=\""+edge.toGraphEdgeString( hideSubsetReachability )+ - "\",decorate];\n"); + bw.write( " "+hrn.toString()+ + " -> "+hrnChild.toString()+ + edge.toStringDOT( hideSubsetReachability )+ + ";\n"); traverseHeapRegionNodes( hrnChild, bw, diff --git a/Robust/src/Analysis/Disjoint/ReachSet.java b/Robust/src/Analysis/Disjoint/ReachSet.java index 7cfced63..e6275335 100644 --- a/Robust/src/Analysis/Disjoint/ReachSet.java +++ b/Robust/src/Analysis/Disjoint/ReachSet.java @@ -486,7 +486,7 @@ public class ReachSet extends Canonical { } - public String toStringEscapeNewline( boolean hideSubsetReachability ) { + public String toStringEscNewline( boolean hideSubsetReachability ) { String s = "["; Iterator i = this.iterator(); diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java index 72bd42cc..3c186eda 100644 --- a/Robust/src/Analysis/Disjoint/RefEdge.java +++ b/Robust/src/Analysis/Disjoint/RefEdge.java @@ -13,10 +13,6 @@ public class RefEdge { // edge models a variable reference protected String field; - // clean means that the reference existed - // before the current analysis context - protected boolean isClean; - protected ReachSet beta; protected ReachSet betaNew; @@ -34,7 +30,6 @@ public class RefEdge { HeapRegionNode dst, TypeDescriptor type, String field, - boolean isClean, ReachSet beta, ExistPredSet preds ) { assert type != null; @@ -43,7 +38,6 @@ public class RefEdge { this.dst = dst; this.type = type; this.field = field; - this.isClean = isClean; if( preds != null ) { this.preds = preds; @@ -69,7 +63,6 @@ public class RefEdge { dst, type, field, - isClean, beta, preds ); return copy; @@ -102,8 +95,6 @@ public class RefEdge { return false; } - assert isClean == edge.isClean; - return true; } @@ -195,15 +186,6 @@ public class RefEdge { } - public boolean isClean() { - return isClean; - } - - public void setIsClean( boolean isClean ) { - this.isClean = isClean; - } - - public ReachSet getBeta() { return beta; } @@ -230,29 +212,25 @@ public class RefEdge { } - public String toGraphEdgeString( boolean hideSubsetReachability ) { - String edgeLabel = ""; - - if( type != null ) { - edgeLabel += type.toPrettyString() + "\\n"; - } + public ExistPredSet getPreds() { + return preds; + } - if( field != null ) { - edgeLabel += field + "\\n"; - } + public void setPreds( ExistPredSet preds ) { + this.preds = preds; + } - if( isClean ) { - edgeLabel += "*clean*\\n"; - } - edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability ) + - "\\n" + preds.toString(); - - return edgeLabel; + public String toStringDOT( boolean hideSubsetReach ) { + return new String( "[label=\""+ + type.toPrettyString()+"\\n"+ + field+"\\n"+ + beta.toStringEscNewline( hideSubsetReach )+"\\n"+ + preds.toString()+"\",decorate]" + ); } public String toString() { - assert type != null; return new String( "("+src+ "->"+type.toPrettyString()+ " "+field+ diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java index 5d618735..004e5612 100644 --- a/Robust/src/IR/State.java +++ b/Robust/src/IR/State.java @@ -73,6 +73,7 @@ public class State { public int DISJOINTALLOCDEPTH=3; public boolean DISJOINTWRITEDOTS=false; public boolean DISJOINTWRITEALL=false; + public boolean DISJOINTWRITEIHMS=false; public String DISJOINTALIASFILE=null; public boolean DISJOINTALIASTAB=false; public int DISJOINTDEBUGCALLCOUNT=0; diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java index 748c0027..d51883f4 100644 --- a/Robust/src/Main/Main.java +++ b/Robust/src/Main/Main.java @@ -165,10 +165,13 @@ public class Main { } else if (option.equals("-owndebugcallcount")) { state.OWNERSHIPDEBUGCALLCOUNT=Integer.parseInt(args[++i]); } + else if (option.equals("-disjoint")) state.DISJOINT=true; + else if (option.equals("-disjoint-k")) { state.DISJOINTALLOCDEPTH=Integer.parseInt(args[++i]); + } else if (option.equals("-disjoint-write-dots")) { state.DISJOINTWRITEDOTS = true; String arg = args[++i]; @@ -179,6 +182,10 @@ public class Main { } else { throw new Error("disjoint-write-dots requires argument "); } + + } else if (option.equals("-disjoint-write-ihms")) { + state.DISJOINTWRITEIHMS = true; + } else if (option.equals("-disjoint-alias-file")) { state.DISJOINTALIASFILE = args[++i]; String arg = args[++i]; @@ -189,11 +196,13 @@ public class Main { } else { throw new Error("disjoint-alias-file requires arguments "); } + } else if (option.equals("-disjoint-debug-callsite")) { state.DISJOINTDEBUGCALLEE=args[++i]; state.DISJOINTDEBUGCALLER=args[++i]; state.DISJOINTDEBUGCALLCOUNT=Integer.parseInt(args[++i]); } + else if (option.equals("-optional")) state.OPTIONAL=true; else if (option.equals("-optimize")) diff --git a/Robust/src/Tests/disjoint/predicateTest1/makefile b/Robust/src/Tests/disjoint/predicateTest1/makefile index dcb012af..8dcb226e 100644 --- a/Robust/src/Tests/disjoint/predicateTest1/makefile +++ b/Robust/src/Tests/disjoint/predicateTest1/makefile @@ -3,7 +3,7 @@ PROGRAM=test SOURCE_FILES=$(PROGRAM).java BUILDSCRIPT=~/research/Robust/src/buildscript -BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -disjoint-write-dots final -disjoint-alias-file aliases.txt normal -enable-assertions +BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -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/predicateTest2/makefile b/Robust/src/Tests/disjoint/predicateTest2/makefile new file mode 100644 index 00000000..8dcb226e --- /dev/null +++ b/Robust/src/Tests/disjoint/predicateTest2/makefile @@ -0,0 +1,27 @@ +PROGRAM=test + +SOURCE_FILES=$(PROGRAM).java + +BUILDSCRIPT=~/research/Robust/src/buildscript +BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 1 -disjoint-write-dots final -disjoint-write-ihms -disjoint-alias-file aliases.txt normal -enable-assertions + +all: $(PROGRAM).bin + +view: PNGs + eog *.png & + +PNGs: DOTs + d2p *COMPLETE*.dot + +DOTs: $(PROGRAM).bin + +$(PROGRAM).bin: $(SOURCE_FILES) + $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES) + +clean: + rm -f $(PROGRAM).bin + rm -fr tmpbuilddirectory + rm -f *~ + rm -f *.dot + rm -f *.png + rm -f aliases.txt diff --git a/Robust/src/Tests/disjoint/predicateTest2/test.java b/Robust/src/Tests/disjoint/predicateTest2/test.java new file mode 100644 index 00000000..28d5be3c --- /dev/null +++ b/Robust/src/Tests/disjoint/predicateTest2/test.java @@ -0,0 +1,31 @@ +public class Foo { + public Foo() {} + public Bar b; +} + +public class Bar { + public Bar() {} +} + +public class Test { + static public void main( String[] args ) { + + Foo f1 = new Foo(); + addSomething( f1 ); + + Foo f2 = new Foo(); + addSomething( f2 ); + } + + public static void addSomething( Foo f ) { + addBar( f ); + } + + public static void addBar( Foo g ) { + if( true ) { + g.b = new Bar(); + } else { + g.b = new Bar(); + } + } +} -- 2.34.1