@@ -214,24 +214,35 @@ private predicate relevantNode(ObjNode n) {
214214 exists ( ObjNode mid | relevantNode ( mid ) and objStep ( mid , n ) and relevantNodeBack ( n ) )
215215}
216216
217- pragma [ noinline]
218- private predicate objStepPruned ( ObjNode n1 , ObjNode n2 ) {
219- objStep ( n1 , n2 ) and relevantNode ( n1 ) and relevantNode ( n2 )
217+ private newtype TObjFlowNode =
218+ TObjNode ( ObjNode n ) { relevantNode ( n ) } or
219+ TObjType ( RefType t ) { source ( t , _) }
220+
221+ private predicate objStepPruned ( TObjFlowNode node1 , TObjFlowNode node2 ) {
222+ exists ( ObjNode n1 , ObjNode n2 |
223+ node1 = TObjNode ( n1 ) and
224+ node2 = TObjNode ( n2 ) and
225+ objStep ( n1 , n2 )
226+ )
227+ or
228+ exists ( RefType t , ObjNode n |
229+ node1 = TObjType ( t ) and
230+ node2 = TObjNode ( n ) and
231+ source ( t , n )
232+ )
220233}
221234
222- private predicate stepPlus ( Node n1 , Node n2 ) = fastTC( objStepPruned / 2 ) ( n1 , n2 )
235+ private predicate flowSrc ( TObjFlowNode src ) { src instanceof TObjType }
236+
237+ private predicate flowSink ( TObjFlowNode sink ) { exists ( ObjNode n | sink = TObjNode ( n ) and sink ( n ) ) }
238+
239+ private predicate stepPlus ( TObjFlowNode n1 , TObjFlowNode n2 ) =
240+ doublyBoundedFastTC( objStepPruned / 2 , flowSrc / 1 , flowSink / 1 ) ( n1 , n2 )
223241
224242/**
225243 * Holds if the qualifier `n` of an `Object.toString()` call might have type `t`.
226244 */
227- pragma [ noopt]
228- private predicate objType ( ObjNode n , RefType t ) {
229- exists ( ObjNode n2 |
230- sink ( n ) and
231- ( stepPlus ( n2 , n ) or n2 = n ) and
232- source ( t , n2 )
233- )
234- }
245+ private predicate objType ( ObjNode n , RefType t ) { stepPlus ( TObjType ( t ) , TObjNode ( n ) ) }
235246
236247private VirtualMethodCall objectToString ( ObjNode n ) {
237248 result .getQualifier ( ) = n .asExpr ( ) and sink ( n )
0 commit comments