From 9f4bc2d218f90f104da228c439373fd2aa2454f6 Mon Sep 17 00:00:00 2001 From: jjenista Date: Mon, 22 Mar 2010 02:56:57 +0000 Subject: [PATCH] fixed problem by differentiating between an element that is out of the callee context, and an element that is also out of the caller context as well, results looking better but reachability states aren't propagating over more than one context --- Robust/src/Analysis/Disjoint/ExistPred.java | 75 ++++--- Robust/src/Analysis/Disjoint/ReachGraph.java | 193 ++++++------------ .../Tests/disjoint/predicateTest3/test.java | 2 +- 3 files changed, 109 insertions(+), 161 deletions(-) diff --git a/Robust/src/Analysis/Disjoint/ExistPred.java b/Robust/src/Analysis/Disjoint/ExistPred.java index 1bd58318..1e00baab 100644 --- a/Robust/src/Analysis/Disjoint/ExistPred.java +++ b/Robust/src/Analysis/Disjoint/ExistPred.java @@ -56,11 +56,16 @@ public class ExistPred extends Canonical { // satisfied when the edge exists AND it has the state. // the source of an edge is *either* a variable // node or a heap region node - protected boolean e_srcOutContext; - protected TempDescriptor e_tdSrc; protected Integer e_hrnSrcID; + // the source of an edge might be out of the callee + // context but in the caller graph, a normal caller + // heap region or variable, OR it might be out of the + // caller context ALSO: an ooc node in the caller + protected boolean e_srcOutCalleeContext; + protected boolean e_srcOutCallerContext; + // dst is always a heap region protected Integer e_hrnDstID; @@ -87,7 +92,8 @@ public class ExistPred extends Canonical { e_hrnDstID = null; e_type = null; e_field = null; - e_srcOutContext = false; + e_srcOutCalleeContext = false; + e_srcOutCallerContext = false; } // node predicates @@ -111,7 +117,8 @@ public class ExistPred extends Canonical { e_hrnDstID = null; e_type = null; e_field = null; - e_srcOutContext = false; + e_srcOutCalleeContext = false; + e_srcOutCallerContext = false; } // edge predicates @@ -121,7 +128,8 @@ public class ExistPred extends Canonical { TypeDescriptor type, String field, ReachState state, - boolean srcOutContext ) { + boolean srcOutCalleeContext, + boolean srcOutCallerContext ) { ExistPred out = new ExistPred( tdSrc, hrnSrcID, @@ -129,7 +137,8 @@ public class ExistPred extends Canonical { type, field, state, - srcOutContext ); + srcOutCalleeContext, + srcOutCallerContext ); out = (ExistPred) Canonical.makeCanonical( out ); return out; @@ -141,7 +150,8 @@ public class ExistPred extends Canonical { TypeDescriptor type, String field, ReachState state, - boolean srcOutContext ) { + boolean srcOutCalleeContext, + boolean srcOutCallerContext ) { assert (tdSrc == null) || (hrnSrcID == null); assert hrnDstID != null; @@ -150,7 +160,9 @@ public class ExistPred extends Canonical { // fields can be null when the edge is from // a variable node to a heap region! // assert field != null; - this.e_srcOutContext = srcOutContext; + + this.e_srcOutCalleeContext = srcOutCalleeContext; + this.e_srcOutCallerContext = srcOutCallerContext; this.e_tdSrc = tdSrc; this.e_hrnSrcID = hrnSrcID; @@ -214,10 +226,6 @@ public class ExistPred extends Canonical { hrnSrc = rg.id2hrn.get( e_hrnSrcID ); } assert (vnSrc == null) || (hrnSrc == null); - - - System.out.println( " checking if src in graph" ); - // the source is not present in graph if( vnSrc == null && hrnSrc == null ) { @@ -227,12 +235,24 @@ public class ExistPred extends Canonical { RefSrcNode rsn; if( vnSrc != null ) { rsn = vnSrc; - } else { + assert e_srcOutCalleeContext; + assert !e_srcOutCallerContext; + } else { - System.out.println( " doing this thing, reachable nodes: "+calleeReachableNodes ); + if( e_srcOutCalleeContext ) { + assert !e_srcOutCallerContext; + if( calleeReachableNodes.contains( e_hrnSrcID ) ) { + return null; + } + } else { + if( !calleeReachableNodes.contains( e_hrnSrcID ) ) { + return null; + } + } - if( e_srcOutContext ) { + if( e_srcOutCallerContext ) { + assert !e_srcOutCalleeContext; if( !hrnSrc.isOutOfContext() ) { return null; } @@ -245,11 +265,6 @@ public class ExistPred extends Canonical { rsn = hrnSrc; } - - - System.out.println( " checking if dst in graph" ); - - // is the destination present? HeapRegionNode hrnDst = rg.id2hrn.get( e_hrnDstID ); if( hrnDst == null ) { @@ -260,11 +275,6 @@ public class ExistPred extends Canonical { return null; } - - - System.out.println( " checking if edge/type/field matches" ); - - // is there an edge between them with the given // type and field? // TODO: type OR a subtype? @@ -281,10 +291,6 @@ public class ExistPred extends Canonical { return edge.getPreds(); } - - System.out.println( " state not null, checking for existence" ); - - // otherwise look for state too // TODO: contains OR containsSuperSet OR containsWithZeroes?? if( hrnDst.getAlpha().containsIgnorePreds( ne_state ) @@ -373,7 +379,8 @@ public class ExistPred extends Canonical { // if the identifiers match, this should // always match - assert e_srcOutContext == pred.e_srcOutContext; + assert e_srcOutCalleeContext == pred.e_srcOutCalleeContext; + assert e_srcOutCallerContext == pred.e_srcOutCallerContext; return true; } @@ -444,8 +451,12 @@ public class ExistPred extends Canonical { s += e_hrnSrcID.toString(); } - if( e_srcOutContext ) { - s += "(ooc)"; + if( e_srcOutCalleeContext ) { + s += "(ooCLEEc)"; + } + + if( e_srcOutCallerContext ) { + s += "(ooCLERc)"; } s += "-->"+e_hrnDstID+")"; diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java index 661c43b9..9c8c8f88 100644 --- a/Robust/src/Analysis/Disjoint/ReachGraph.java +++ b/Robust/src/Analysis/Disjoint/ReachGraph.java @@ -1284,15 +1284,9 @@ public class ReachGraph { // used below to convert a ReachSet to its callee-context // equivalent with respect to allocation sites in this graph - protected ReachSet toCalleeContext( Set oocTuples, - ReachSet rs, - Integer hrnID, - TempDescriptor tdSrc, - Integer hrnSrcID, - Integer hrnDstID, - TypeDescriptor type, - String field, - boolean outOfContext + protected ReachSet toCalleeContext( ReachSet rs, + ExistPredSet preds, + Set oocTuples ) { ReachSet out = ReachSet.factory(); @@ -1311,7 +1305,8 @@ public class ReachGraph { while( rtItr.hasNext() ) { ReachTuple rt = rtItr.next(); - // only translate this tuple if it is in the out-context bag + // only translate this tuple if it is + // in the out-callee-context bag if( !oocTuples.contains( rt ) ) { stateNew = Canonical.add( stateNew, rt ); continue; @@ -1369,34 +1364,8 @@ public class ReachGraph { stateCallee = stateNew; } - - - ExistPredSet preds; - - if( outOfContext ) { - preds = predsEmpty; - } else { - ExistPred pred; - if( hrnID != null ) { - assert tdSrc == null; - assert hrnSrcID == null; - assert hrnDstID == null; - pred = ExistPred.factory( hrnID, - stateCaller ); - } else { - assert tdSrc != null || hrnSrcID != null; - assert hrnDstID != null; - pred = ExistPred.factory( tdSrc, - hrnSrcID, - hrnDstID, - type, - field, - stateCaller, - false ); - } - preds = ExistPredSet.factory( pred ); - } + // attach the passed in preds stateCallee = Canonical.attach( stateCallee, preds ); @@ -1619,16 +1588,14 @@ public class ReachGraph { false, // out-of-context? hrnCaller.getType(), hrnCaller.getAllocSite(), - toCalleeContext( oocTuples, - hrnCaller.getInherent(), // in state - hrnCaller.getID(), // node pred - null, null, null, null, null, // edge pred - false ), // ooc pred - toCalleeContext( oocTuples, - hrnCaller.getAlpha(), // in state - hrnCaller.getID(), // node pred - null, null, null, null, null, // edge pred - false ), // ooc pred + toCalleeContext( hrnCaller.getInherent(), + preds, + oocTuples + ), + toCalleeContext( hrnCaller.getAlpha(), + preds, + oocTuples + ), preds, hrnCaller.getDescription() ); @@ -1658,7 +1625,9 @@ public class ReachGraph { reArg.getType(), reArg.getField(), null, - false ); // out-of-context + true, // out-of-callee-context + false // out-of-caller-context + ); ExistPredSet preds = ExistPredSet.factory( pred ); @@ -1668,15 +1637,10 @@ public class ReachGraph { hrnDstCallee, reArg.getType(), reArg.getField(), - toCalleeContext( oocTuples, - reArg.getBeta(), // in state - null, // node pred - arg, // edge pred - null, // edge pred - hrnDstCallee.getID(), // edge pred - reArg.getType(), // edge pred - reArg.getField(), // edge pred - false ), // ooc pred + toCalleeContext( reArg.getBeta(), + preds, + oocTuples + ), preds ); @@ -1707,7 +1671,9 @@ public class ReachGraph { reCaller.getType(), reCaller.getField(), null, - false ); // out-of-context + false, // out-of-callee-context + false // out-of-caller-context + ); ExistPredSet preds = ExistPredSet.factory( pred ); @@ -1717,15 +1683,10 @@ public class ReachGraph { hrnDstCallee, reCaller.getType(), reCaller.getField(), - toCalleeContext( oocTuples, - reCaller.getBeta(), // in state - null, // node pred - null, // edge pred - hrnSrcCallee.getID(), // edge pred - hrnDstCallee.getID(), // edge pred - reCaller.getType(), // edge pred - reCaller.getField(), // edge pred - false ), // ooc pred + toCalleeContext( reCaller.getBeta(), + preds, + oocTuples + ), preds ); @@ -1748,14 +1709,16 @@ public class ReachGraph { ReachSet oocReach; TempDescriptor oocPredSrcTemp = null; Integer oocPredSrcID = null; - boolean oocooc; + boolean outOfCalleeContext; + boolean outOfCallerContext; if( rsnCaller instanceof VariableNode ) { VariableNode vnCaller = (VariableNode) rsnCaller; oocNodeType = null; oocReach = rsetEmpty; oocPredSrcTemp = vnCaller.getTempDescriptor(); - oocooc = false; + outOfCalleeContext = true; + outOfCallerContext = false; } else { HeapRegionNode hrnSrcCaller = (HeapRegionNode) rsnCaller; @@ -1763,7 +1726,13 @@ public class ReachGraph { oocNodeType = hrnSrcCaller.getType(); oocReach = hrnSrcCaller.getAlpha(); oocPredSrcID = hrnSrcCaller.getID(); - oocooc = hrnSrcCaller.isOutOfContext(); + if( hrnSrcCaller.isOutOfContext() ) { + outOfCalleeContext = false; + outOfCallerContext = true; + } else { + outOfCalleeContext = true; + outOfCallerContext = false; + } } ExistPred pred = @@ -1773,7 +1742,9 @@ public class ReachGraph { reCaller.getType(), reCaller.getField(), null, - oocooc ); // out-of-context + outOfCalleeContext, + outOfCallerContext + ); ExistPredSet preds = ExistPredSet.factory( pred ); @@ -1809,18 +1780,14 @@ public class ReachGraph { true, // out-of-context? oocNodeType, null, // alloc site, shouldn't be used - toCalleeContext( oocTuples, - oocReach, // in state - null, // node pred - null, null, null, null, null, // edge pred - true // ooc pred - ), // inherent - toCalleeContext( oocTuples, - oocReach, // in state - null, // node pred - null, null, null, null, null, // edge pred - true // ooc pred - ), // alpha + toCalleeContext( oocReach, + preds, + oocTuples + ), + toCalleeContext( oocReach, + preds, + oocTuples + ), preds, "out-of-context" ); @@ -1842,18 +1809,14 @@ public class ReachGraph { true, // out-of-context? oocNodeType, null, // alloc site, shouldn't be used - toCalleeContext( oocTuples, - oocReach, // in state - null, // node pred - null, null, null, null, null, // edge pred - true // ooc pred - ), // inherent - toCalleeContext( oocTuples, - oocReach, // in state - null, // node pred - null, null, null, null, null, // edge pred - true // ooc pred - ), // alpha + toCalleeContext( oocReach, + preds, + oocTuples + ), + toCalleeContext( oocReach, + preds, + oocTuples + ), preds, "out-of-context" ); @@ -1866,15 +1829,9 @@ public class ReachGraph { hrnDstCallee, reCaller.getType(), reCaller.getField(), - toCalleeContext( oocTuples, - reCaller.getBeta(), // in state - null, // node pred - oocPredSrcTemp, // edge pred - oocPredSrcID, // edge pred - hrnDstCaller.getID(), // edge pred - reCaller.getType(), // edge pred - reCaller.getField(), // edge pred - false // ooc pred + toCalleeContext( reCaller.getBeta(), + preds, + oocTuples ), preds ) @@ -1883,16 +1840,10 @@ public class ReachGraph { } else { // the out-of-context edge already exists oocEdgeExisting.setBeta( Canonical.unionORpreds( oocEdgeExisting.getBeta(), - toCalleeContext( oocTuples, - reCaller.getBeta(), // in state - null, // node pred - oocPredSrcTemp, // edge pred - oocPredSrcID, // edge pred - hrnDstCaller.getID(), // edge pred - reCaller.getType(), // edge pred - reCaller.getField(), // edge pred - false // ooc pred - ) + toCalleeContext( reCaller.getBeta(), + preds, + oocTuples + ) ) ); @@ -2041,12 +1992,6 @@ public class ReachGraph { continue; } - - - System.out.println( " preds satisfied? for "+reCallee+" "+reCallee.getPreds() ); - - - // first see if the source is out-of-context, and only // proceed with this edge if we find some caller-context // matches @@ -2126,15 +2071,7 @@ public class ReachGraph { calleeStatesSatisfied.put( stateCallee, predsIfSatis ); } } - - System.out.println( " YES" ); } - - - else { - System.out.println( " NO" ); - } - } } diff --git a/Robust/src/Tests/disjoint/predicateTest3/test.java b/Robust/src/Tests/disjoint/predicateTest3/test.java index ba689695..7bbce921 100644 --- a/Robust/src/Tests/disjoint/predicateTest3/test.java +++ b/Robust/src/Tests/disjoint/predicateTest3/test.java @@ -16,7 +16,7 @@ public class Test { } public static void addSomething( Foo x ) { - //x.f = disjoint added new Foo(); + x.f = disjoint added new Foo(); } public static Foo getAFoo() { -- 2.34.1