@@ -340,94 +340,13 @@ module ProductFlow {
340
340
fwdIsSuccessor ( _, _, node1 , node2 )
341
341
}
342
342
343
- pragma [ assume_small_delta]
344
- pragma [ nomagic]
345
- private predicate fwdLocalPathStep1 ( Flow1:: PathNode n ) {
346
- fwdReachableInterprocEntry ( n , _)
347
- or
348
- exists ( Flow1:: PathNode mid |
349
- fwdLocalPathStep1 ( mid ) and
350
- localPathStep1 ( mid , n )
351
- )
352
- }
353
-
354
- pragma [ assume_small_delta]
355
- pragma [ nomagic]
356
- private predicate revLocalPathStep1 ( Flow1:: PathNode n ) {
357
- fwdLocalPathStep1 ( n ) and
358
- (
359
- isSinkPair ( n , _)
360
- or
361
- interprocEdgePair ( n , _, _, _)
362
- or
363
- exists ( Flow1:: PathNode mid |
364
- revLocalPathStep1 ( mid ) and
365
- localPathStep1 ( n , mid )
366
- )
367
- )
368
- }
369
-
370
- pragma [ assume_small_delta]
371
- private predicate prunedLocalPathStep1 ( Flow1:: PathNode n1 , Flow1:: PathNode n2 ) {
372
- revLocalPathStep1 ( n1 ) and
373
- revLocalPathStep1 ( n2 ) and
374
- localPathStep1 ( n1 , n2 )
375
- }
376
-
377
- pragma [ nomagic]
378
- private predicate fwdLocalPathStep2 ( Flow2:: PathNode n ) {
379
- fwdReachableInterprocEntry ( _, n )
380
- or
381
- exists ( Flow2:: PathNode mid |
382
- fwdLocalPathStep2 ( mid ) and
383
- localPathStep2 ( mid , n )
384
- )
385
- }
386
-
387
- pragma [ assume_small_delta]
388
- pragma [ nomagic]
389
- private predicate revLocalPathStep2 ( Flow2:: PathNode n ) {
390
- fwdLocalPathStep2 ( n ) and
391
- (
392
- isSinkPair ( _, n )
393
- or
394
- interprocEdgePair ( _, n , _, _)
395
- or
396
- exists ( Flow2:: PathNode mid |
397
- revLocalPathStep2 ( mid ) and
398
- localPathStep2 ( n , mid )
399
- )
400
- )
401
- }
402
-
403
- pragma [ assume_small_delta]
404
- private predicate prunedLocalPathStep2 ( Flow2:: PathNode n1 , Flow2:: PathNode n2 ) {
405
- revLocalPathStep2 ( n1 ) and
406
- revLocalPathStep2 ( n2 ) and
407
- localPathStep2 ( n1 , n2 )
408
- }
409
-
410
- private predicate localPathStep1SuccPlus ( Flow1:: PathNode n1 , Flow1:: PathNode n2 ) =
411
- fastTC( prunedLocalPathStep1 / 2 ) ( n1 , n2 )
412
-
413
- private predicate localPathStep2SuccPlus ( Flow2:: PathNode n1 , Flow2:: PathNode n2 ) =
414
- fastTC( prunedLocalPathStep2 / 2 ) ( n1 , n2 )
415
-
416
- private predicate localPathStep1Tc ( Flow1:: PathNode n1 , Flow1:: PathNode n2 ) {
417
- localPathStep1SuccPlus ( n1 , n2 ) or n1 = n2
418
- }
419
-
420
- private predicate localPathStep2Tc ( Flow2:: PathNode n1 , Flow2:: PathNode n2 ) {
421
- localPathStep2SuccPlus ( n1 , n2 ) or n1 = n2
422
- }
423
-
424
343
private predicate fwdIsSuccessor (
425
344
Flow1:: PathNode pred1 , Flow2:: PathNode pred2 , Flow1:: PathNode succ1 , Flow2:: PathNode succ2
426
345
) {
427
346
fwdReachableInterprocEntry ( pred1 , pred2 ) and
428
347
exists ( Flow1:: PathNode mid1 , Flow2:: PathNode mid2 |
429
- localPathStep1Tc ( pred1 , mid1 ) and
430
- localPathStep2Tc ( pred2 , mid2 )
348
+ localPathStep1 * ( pred1 , mid1 ) and
349
+ localPathStep2 * ( pred2 , mid2 )
431
350
|
432
351
isSinkPair ( mid1 , mid2 ) and
433
352
succ1 = mid1 and
0 commit comments