// 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;
e_hrnDstID = null;
e_type = null;
e_field = null;
- e_srcOutContext = false;
+ e_srcOutCalleeContext = false;
+ e_srcOutCallerContext = false;
}
// node predicates
e_hrnDstID = null;
e_type = null;
e_field = null;
- e_srcOutContext = false;
+ e_srcOutCalleeContext = false;
+ e_srcOutCallerContext = false;
}
// edge predicates
TypeDescriptor type,
String field,
ReachState state,
- boolean srcOutContext ) {
+ boolean srcOutCalleeContext,
+ boolean srcOutCallerContext ) {
ExistPred out = new ExistPred( tdSrc,
hrnSrcID,
type,
field,
state,
- srcOutContext );
+ srcOutCalleeContext,
+ srcOutCallerContext );
out = (ExistPred) Canonical.makeCanonical( out );
return out;
TypeDescriptor type,
String field,
ReachState state,
- boolean srcOutContext ) {
+ boolean srcOutCalleeContext,
+ boolean srcOutCallerContext ) {
assert (tdSrc == null) || (hrnSrcID == null);
assert hrnDstID != null;
// 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;
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 ) {
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;
}
rsn = hrnSrc;
}
-
-
- System.out.println( " checking if dst in graph" );
-
-
// is the destination present?
HeapRegionNode hrnDst = rg.id2hrn.get( e_hrnDstID );
if( hrnDst == null ) {
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?
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 )
// 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;
}
s += e_hrnSrcID.toString();
}
- if( e_srcOutContext ) {
- s += "(ooc)";
+ if( e_srcOutCalleeContext ) {
+ s += "(ooCLEEc)";
+ }
+
+ if( e_srcOutCallerContext ) {
+ s += "(ooCLERc)";
}
s += "-->"+e_hrnDstID+")";
// used below to convert a ReachSet to its callee-context
// equivalent with respect to allocation sites in this graph
- protected ReachSet toCalleeContext( Set<ReachTuple> 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<ReachTuple> oocTuples
) {
ReachSet out = ReachSet.factory();
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;
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 );
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()
);
reArg.getType(),
reArg.getField(),
null,
- false ); // out-of-context
+ true, // out-of-callee-context
+ false // out-of-caller-context
+ );
ExistPredSet preds =
ExistPredSet.factory( pred );
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
);
reCaller.getType(),
reCaller.getField(),
null,
- false ); // out-of-context
+ false, // out-of-callee-context
+ false // out-of-caller-context
+ );
ExistPredSet preds =
ExistPredSet.factory( pred );
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
);
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;
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 =
reCaller.getType(),
reCaller.getField(),
null,
- oocooc ); // out-of-context
+ outOfCalleeContext,
+ outOfCallerContext
+ );
ExistPredSet preds =
ExistPredSet.factory( pred );
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"
);
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"
);
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
)
} 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
+ )
)
);
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
calleeStatesSatisfied.put( stateCallee, predsIfSatis );
}
}
-
- System.out.println( " YES" );
}
-
-
- else {
- System.out.println( " NO" );
- }
-
}
}
projects / IRC.git / commitdiff