@@ -214,24 +214,35 @@ private predicate relevantNode(ObjNode n) {
214
214
exists ( ObjNode mid | relevantNode ( mid ) and objStep ( mid , n ) and relevantNodeBack ( n ) )
215
215
}
216
216
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
+ )
220
233
}
221
234
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 )
223
241
224
242
/**
225
243
* Holds if the qualifier `n` of an `Object.toString()` call might have type `t`.
226
244
*/
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 ) ) }
235
246
236
247
private VirtualMethodCall objectToString ( ObjNode n ) {
237
248
result .getQualifier ( ) = n .asExpr ( ) and sink ( n )
0 commit comments