From cc4bee76a0da6f1c469a476614473f27e195c389 Mon Sep 17 00:00:00 2001 From: jjenista Date: Wed, 6 Jan 2010 19:25:29 +0000 Subject: [PATCH] more implementation --- .../Analysis/Disjoint/DisjointAnalysis.java | 2 +- .../src/Analysis/Disjoint/HeapRegionNode.java | 32 ++++++++- Robust/src/Analysis/Disjoint/ReachGraph.java | 66 +++++++++++++------ Robust/src/Analysis/Disjoint/RefEdge.java | 32 +++++---- Robust/src/Tests/disjoint/simple/test.java | 4 +- 5 files changed, 99 insertions(+), 37 deletions(-) diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java index ffec0c9b..d85979c1 100644 --- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java +++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java @@ -565,7 +565,7 @@ public class DisjointAnalysis { } } - // now that we've got that taken care of, go ahead and update + // now that we've taken care of that, go ahead and update // the reach graph for this FlatCall node by whatever callee // result we do have diff --git a/Robust/src/Analysis/Disjoint/HeapRegionNode.java b/Robust/src/Analysis/Disjoint/HeapRegionNode.java index 9817c5f3..f190fae0 100644 --- a/Robust/src/Analysis/Disjoint/HeapRegionNode.java +++ b/Robust/src/Analysis/Disjoint/HeapRegionNode.java @@ -12,12 +12,23 @@ 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; + protected HashSet referencers; protected TypeDescriptor type; protected AllocSite allocSite; + // some reachability states are inherent + // to a node by its definition + protected ReachSet inherent; + + // use alpha for the current reach states + // and alphaNew during iterative calculations + // to update alpha protected ReachSet alpha; protected ReachSet alphaNew; @@ -28,8 +39,10 @@ public class HeapRegionNode extends RefSrcNode { boolean isSingleObject, boolean isFlagged, boolean isNewSummary, + boolean isClean, TypeDescriptor type, AllocSite allocSite, + ReachSet inherent, ReachSet alpha, String description ) { @@ -37,8 +50,10 @@ public class HeapRegionNode extends RefSrcNode { this.isSingleObject = isSingleObject; this.isFlagged = isFlagged; this.isNewSummary = isNewSummary; + this.isClean = isClean; this.type = type; this.allocSite = allocSite; + this.inherent = inherent; this.alpha = alpha; this.description = description; @@ -51,8 +66,10 @@ public class HeapRegionNode extends RefSrcNode { isSingleObject, isFlagged, isNewSummary, + isClean, type, allocSite, + inherent, alpha, description ); } @@ -86,6 +103,7 @@ public class HeapRegionNode extends RefSrcNode { assert isSingleObject == hrn.isSingleObject(); assert isFlagged == hrn.isFlagged(); assert isNewSummary == hrn.isNewSummary(); + assert isClean == hrn.isClean(); assert description.equals( hrn.getDescription() ); return true; @@ -108,6 +126,14 @@ public class HeapRegionNode extends RefSrcNode { return isNewSummary; } + public boolean isClean() { + return isClean(); + } + + public void setIsClean( boolean isClean ) { + this.isClean = isClean; + } + public Iterator iteratorToReferencers() { return referencers.iterator(); @@ -165,6 +191,11 @@ public class HeapRegionNode extends RefSrcNode { return allocSite; } + + public ReachSet getInherent() { + return inherent; + } + public ReachSet getAlpha() { return alpha; } @@ -209,7 +240,6 @@ public class HeapRegionNode extends RefSrcNode { } public String getDescription() { - //return new String(description); return description; } } diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 068c5a96..97b99a95 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -76,8 +76,10 @@ public class ReachGraph { boolean isSingleObject, boolean isNewSummary, boolean isFlagged, + boolean isClean, TypeDescriptor type, AllocSite allocSite, + ReachSet inherent, ReachSet alpha, String description ) { @@ -100,25 +102,31 @@ public class ReachGraph { id = DisjointAnalysis.generateUniqueHeapRegionNodeID(); } - if( alpha == null ) { + if( inherent == null ) { if( markForAnalysis ) { - alpha = new ReachSet( - new ReachTuple( id, - !isSingleObject, - ReachTuple.ARITY_ONE - ).makeCanonical() - ).makeCanonical(); + inherent = new ReachSet( + new ReachTuple( id, + !isSingleObject, + ReachTuple.ARITY_ONE + ).makeCanonical() + ).makeCanonical(); } else { - alpha = rsetWithEmptyState; + inherent = rsetWithEmptyState; } } + + if( alpha == null ) { + alpha = inherent; + } HeapRegionNode hrn = new HeapRegionNode( id, isSingleObject, markForAnalysis, isNewSummary, + isClean, typeToUse, allocSite, + inherent, alpha, description ); id2hrn.put( id, hrn ); @@ -532,9 +540,9 @@ public class ReachGraph { edgeExisting.setBeta( edgeExisting.getBeta().union( edgeNew.getBeta() ) ); - // a new edge here cannot be reflexive, so existing will - // always be also not reflexive anymore - edgeExisting.setIsInitialParam( false ); + // we touched this edge in the current context + // so dirty it + edgeExisting.setIsClean( false ); } else { addRefEdge( hrnX, hrnY, edgeNew ); @@ -741,9 +749,11 @@ public class ReachGraph { false, // single object? true, // summary? hasFlags, // flagged? + false, // dirty? as.getType(), // type as, // allocation site - null, // reachability set + null, // inherent reach + null, // current reach strDesc // description ); @@ -755,9 +765,11 @@ public class ReachGraph { true, // single object? false, // summary? hasFlags, // flagged? + false, // dirty? as.getType(), // type as, // allocation site - null, // reachability set + null, // inherent reach + null, // current reach strDesc // description ); } @@ -789,9 +801,11 @@ public class ReachGraph { false, // single object? true, // summary? hasFlags, // flagged? + false, // dirty? as.getType(), // type as, // allocation site - null, // reachability set + null, // inherent reach + null, // current reach strDesc // description ); @@ -802,10 +816,12 @@ public class ReachGraph { createNewHeapRegionNode( idShadowIth, // id or null to generate a new one true, // single object? false, // summary? - hasFlags, // flagged? + hasFlags, // flagged? + false, // dirty? as.getType(), // type as, // allocation site - null, // reachability set + null, // inherent reach + null, // current reach strDesc // description ); } @@ -2943,6 +2959,12 @@ public class ReachGraph { // nodes' reachability sets HeapRegionNode hrnB = id2hrn.get( idA ); hrnB.setAlpha( hrnB.getAlpha().union( hrnA.getAlpha() ) ); + + // if hrnB is already dirty or hrnA is dirty, + // the hrnB should end up dirty + if( !hrnA.isClean() ) { + hrnB.setIsClean( false ); + } } } @@ -3018,8 +3040,8 @@ public class ReachGraph { edgeToMerge.setBeta( edgeToMerge.getBeta().union( edgeA.getBeta() ) ); - if( !edgeA.isInitialParam() ) { - edgeToMerge.setIsInitialParam( false ); + if( !edgeA.isClean() ) { + edgeToMerge.setIsClean( false ); } } } @@ -3079,8 +3101,8 @@ public class ReachGraph { edgeToMerge.setBeta( edgeToMerge.getBeta().union( edgeA.getBeta() ) ); - if( !edgeA.isInitialParam() ) { - edgeToMerge.setIsInitialParam( false ); + if( !edgeA.isClean() ) { + edgeToMerge.setIsClean( false ); } } } @@ -3400,8 +3422,10 @@ public class ReachGraph { hrnSrcCaller.isSingleObject(), hrnSrcCaller.isNewSummary(), hrnSrcCaller.isFlagged(), + true, // clean hrnSrcCaller.getType(), hrnSrcCaller.getAllocSite(), + hrnSrcCaller.getInherent(), hrnSrcCaller.getAlpha(), hrnSrcCaller.getDescription() ); @@ -3427,8 +3451,10 @@ public class ReachGraph { hrnCaller.isSingleObject(), hrnCaller.isNewSummary(), hrnCaller.isFlagged(), + true, // clean hrnCaller.getType(), hrnCaller.getAllocSite(), + hrnCaller.getInherent(), hrnCaller.getAlpha(), hrnCaller.getDescription() ); diff --git a/Robust/src/Analysis/Disjoint/RefEdge.java b/Robust/src/Analysis/Disjoint/RefEdge.java index 9134f33b..30c7a611 100644 --- a/Robust/src/Analysis/Disjoint/RefEdge.java +++ b/Robust/src/Analysis/Disjoint/RefEdge.java @@ -13,7 +13,9 @@ public class RefEdge { // edge models a variable reference protected String field; - protected boolean isInitialParam; + // clean means that the reference existed + // before the current analysis context + protected boolean isClean; protected ReachSet beta; protected ReachSet betaNew; @@ -26,15 +28,15 @@ public class RefEdge { HeapRegionNode dst, TypeDescriptor type, String field, - boolean isInitialParam, + boolean isClean, ReachSet beta ) { assert type != null; - this.src = src; - this.dst = dst; - this.type = type; - this.field = field; - this.isInitialParam = isInitialParam; + this.src = src; + this.dst = dst; + this.type = type; + this.field = field; + this.isClean = isClean; if( beta != null ) { this.beta = beta; @@ -53,7 +55,7 @@ public class RefEdge { dst, type, field, - isInitialParam, + isClean, beta ); return copy; } @@ -85,6 +87,8 @@ public class RefEdge { return false; } + assert isClean == edge.isClean; + return true; } @@ -167,12 +171,12 @@ public class RefEdge { } - public boolean isInitialParam() { - return isInitialParam; + public boolean isClean() { + return isClean; } - public void setIsInitialParam( boolean isInitialParam ) { - this.isInitialParam = isInitialParam; + public void setIsClean( boolean isClean ) { + this.isClean = isClean; } @@ -213,8 +217,8 @@ public class RefEdge { edgeLabel += field + "\\n"; } - if( isInitialParam ) { - edgeLabel += "*init*\\n"; + if( isClean ) { + edgeLabel += "*clean*\\n"; } edgeLabel += beta.toStringEscapeNewline( hideSubsetReachability ); diff --git a/Robust/src/Tests/disjoint/simple/test.java b/Robust/src/Tests/disjoint/simple/test.java index 4a89947a..c6b136c4 100644 --- a/Robust/src/Tests/disjoint/simple/test.java +++ b/Robust/src/Tests/disjoint/simple/test.java @@ -6,10 +6,12 @@ public class Foo { public class Test { static public void main( String[] args ) { Foo a = new Foo(); - a.f = new Foo(); f1( a ); } static public void f1( Foo b ) { + Foo c = new Foo(); + b.f = c; + f1( c ); } } -- 2.34.1