@@ -2358,13 +2358,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2358
2358
string toString ( ) ;
2359
2359
}
2360
2360
2361
+ predicate nodeRange ( NodeEx node , boolean fromArg ) ;
2362
+
2361
2363
predicate localValueStep ( NodeEx node1 , NodeEx node2 ) ;
2362
2364
2363
2365
predicate jumpValueStep ( NodeEx node1 , NodeEx node2 ) ;
2364
2366
2365
2367
predicate callEdgeArgParam ( NodeEx arg , NodeEx param ) ;
2366
2368
2367
- predicate callEdgeReturn ( NodeEx ret , NodeEx out ) ;
2369
+ predicate callEdgeReturn ( NodeEx ret , NodeEx out , boolean mayFlowThrough ) ;
2368
2370
2369
2371
predicate readContentStep ( NodeEx node1 , Content c , NodeEx node2 ) ;
2370
2372
@@ -2394,23 +2396,16 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2394
2396
module StoreReadMatching< StoreReadMatchingInputSig Input> {
2395
2397
private import Input
2396
2398
2397
- pragma [ nomagic]
2398
- private predicate valueStep ( NodeEx node1 , NodeEx node2 ) {
2399
- localValueStep ( node1 , node2 )
2400
- or
2401
- jumpValueStep ( node1 , node2 )
2402
- or
2403
- callEdgeArgParam ( node1 , node2 )
2404
- or
2405
- callEdgeReturn ( node1 , node2 )
2406
- }
2407
-
2408
2399
private signature module StoreReachesReadInputSig {
2409
2400
int iteration ( ) ;
2410
2401
2411
- predicate storeMayReachReadDelta ( NodeEx storeSource , Content c , NodeEx readTarget ) ;
2402
+ predicate storeMayReachReadDelta (
2403
+ NodeEx storeSource , Content c , NodeEx readTarget , boolean fromArg1 , boolean fromArg2
2404
+ ) ;
2412
2405
2413
- predicate storeMayReachReadPrev ( NodeEx storeSource , Content c , NodeEx readTarget ) ;
2406
+ predicate storeMayReachReadPrev (
2407
+ NodeEx storeSource , Content c , NodeEx readTarget , boolean fromArg1 , boolean fromArg2
2408
+ ) ;
2414
2409
}
2415
2410
2416
2411
private signature class UsesPrevDeltaInfoSig {
@@ -2428,13 +2423,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2428
2423
private predicate enabled ( ) { accessPathConfigLimit ( ) > Prev:: iteration ( ) }
2429
2424
2430
2425
private newtype TNodeOrContent =
2431
- TNodeOrContentNode ( NodeEx n , UsesPrevDeltaInfo usesPrevDelta ) { enabled ( ) } or
2426
+ TNodeOrContentNode ( NodeEx n , UsesPrevDeltaInfo usesPrevDelta , boolean fromArg ) {
2427
+ enabled ( ) and nodeRange ( n , fromArg )
2428
+ } or
2432
2429
TNodeOrContentStoreContent ( Content c ) { enabled ( ) and storeContentStep ( _, c , _) } or
2433
2430
TNodeOrContentReadContent ( Content c ) { enabled ( ) and readContentStep ( _, c , _) }
2434
2431
2435
2432
private class NodeOrContent extends TNodeOrContent {
2436
- NodeEx asNodeEx ( UsesPrevDeltaInfo usesPrevDelta ) {
2437
- this = TNodeOrContentNode ( result , usesPrevDelta )
2433
+ NodeEx asNodeEx ( UsesPrevDeltaInfo usesPrevDelta , boolean fromArg ) {
2434
+ this = TNodeOrContentNode ( result , usesPrevDelta , fromArg )
2438
2435
}
2439
2436
2440
2437
Content asStoreContent ( ) { this = TNodeOrContentStoreContent ( result ) }
@@ -2446,41 +2443,68 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2446
2443
or
2447
2444
result = this .asReadContent ( ) .toString ( )
2448
2445
or
2449
- result = this .asNodeEx ( _) .toString ( )
2446
+ result = this .asNodeEx ( _, _ ) .toString ( )
2450
2447
}
2451
2448
}
2452
2449
2450
+ bindingset [ usesPrevDelta]
2451
+ pragma [ inline_late]
2452
+ private predicate usesPrevDelta ( UsesPrevDeltaInfo usesPrevDelta , boolean b ) {
2453
+ usesPrevDelta .toBoolean ( ) = b
2454
+ }
2455
+
2456
+ pragma [ nomagic]
2457
+ private predicate stepNode (
2458
+ NodeOrContent node1 , NodeEx n2 , UsesPrevDeltaInfo usesPrevDelta1 ,
2459
+ UsesPrevDeltaInfo usesPrevDelta2 , Boolean fromArg1 , Boolean fromArg2
2460
+ ) {
2461
+ exists ( NodeEx n1 | n1 = node1 .asNodeEx ( usesPrevDelta1 , fromArg1 ) |
2462
+ usesPrevDelta1 = usesPrevDelta2 and
2463
+ (
2464
+ localValueStep ( n1 , n2 ) and
2465
+ fromArg1 = fromArg2
2466
+ or
2467
+ jumpValueStep ( n1 , n2 ) and
2468
+ fromArg2 = false
2469
+ or
2470
+ callEdgeArgParam ( n1 , n2 ) and
2471
+ fromArg2 = true
2472
+ or
2473
+ exists ( boolean mayFlowThrough | callEdgeReturn ( n1 , n2 , mayFlowThrough ) |
2474
+ fromArg1 = false or mayFlowThrough = true
2475
+ )
2476
+ )
2477
+ or
2478
+ Prev:: storeMayReachReadDelta ( n1 , _, n2 , fromArg1 , fromArg2 ) and
2479
+ usesPrevDelta ( usesPrevDelta2 , true )
2480
+ or
2481
+ Prev:: storeMayReachReadPrev ( n1 , _, n2 , fromArg1 , fromArg2 ) and
2482
+ usesPrevDelta1 = usesPrevDelta2
2483
+ )
2484
+ }
2485
+
2453
2486
pragma [ nomagic]
2454
2487
private predicate step ( NodeOrContent node1 , NodeOrContent node2 ) {
2455
2488
exists (
2456
- NodeEx n1 , NodeEx n2 , UsesPrevDeltaInfo usesPrevDelta1 , UsesPrevDeltaInfo usesPrevDelta2
2489
+ NodeEx n2 , UsesPrevDeltaInfo usesPrevDelta1 , UsesPrevDeltaInfo usesPrevDelta2 ,
2490
+ boolean fromArg1 , boolean fromArg2
2457
2491
|
2458
- n1 = node1 .asNodeEx ( usesPrevDelta1 ) and
2459
- n2 = node2 .asNodeEx ( usesPrevDelta2 )
2460
- |
2461
- valueStep ( n1 , n2 ) and
2462
- pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( usesPrevDelta2 ) ) =
2463
- pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( usesPrevDelta1 ) )
2464
- or
2465
- Prev:: storeMayReachReadDelta ( n1 , _, n2 ) and usesPrevDelta2 .toBoolean ( ) = true
2466
- or
2467
- Prev:: storeMayReachReadPrev ( n1 , _, n2 ) and
2468
- pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( usesPrevDelta2 ) ) =
2469
- pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( usesPrevDelta1 ) )
2492
+ n2 = node2 .asNodeEx ( usesPrevDelta2 , fromArg2 ) and
2493
+ stepNode ( node1 , n2 , usesPrevDelta1 , usesPrevDelta2 , fromArg1 , fromArg2 )
2470
2494
)
2471
2495
or
2472
2496
exists ( NodeEx n2 , Content c , UsesPrevDeltaInfo usesPrevDelta2 |
2473
- n2 = node2 .asNodeEx ( usesPrevDelta2 ) and
2497
+ n2 = node2 .asNodeEx ( usesPrevDelta2 , _ ) and
2474
2498
c = node1 .asStoreContent ( ) and
2475
2499
storeContentStep ( _, c , n2 ) and
2476
- usesPrevDelta2 . toBoolean ( ) = false
2500
+ usesPrevDelta ( usesPrevDelta2 , false )
2477
2501
)
2478
2502
or
2479
2503
exists ( NodeEx n1 , Content c , UsesPrevDeltaInfo usesPrevDelta1 |
2480
- n1 = node1 .asNodeEx ( usesPrevDelta1 ) and
2504
+ n1 = node1 .asNodeEx ( usesPrevDelta1 , _ ) and
2481
2505
c = node2 .asReadContent ( ) and
2482
2506
readContentStep ( n1 , c , _) and
2483
- usesPrevDelta1 . toBoolean ( ) = true
2507
+ usesPrevDelta ( usesPrevDelta1 , true )
2484
2508
)
2485
2509
}
2486
2510
@@ -2508,8 +2532,8 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2508
2532
private predicate isStoreTarget0 ( NodeOrContent node , Content c ) {
2509
2533
exists ( UsesPrevDeltaInfo usesPrevDelta |
2510
2534
contentIsReadAndStored ( c ) and
2511
- storeContentStep ( _, c , node .asNodeEx ( usesPrevDelta ) ) and
2512
- usesPrevDelta . toBoolean ( ) = false
2535
+ storeContentStep ( _, c , node .asNodeEx ( usesPrevDelta , _ ) ) and
2536
+ usesPrevDelta ( usesPrevDelta , false )
2513
2537
)
2514
2538
}
2515
2539
@@ -2519,8 +2543,8 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2519
2543
private predicate isReadSource0 ( NodeOrContent node , Content c ) {
2520
2544
exists ( UsesPrevDeltaInfo usesPrevDelta |
2521
2545
contentIsReadAndStored ( c ) and
2522
- readContentStep ( node .asNodeEx ( usesPrevDelta ) , c , _) and
2523
- usesPrevDelta . toBoolean ( ) = true
2546
+ readContentStep ( node .asNodeEx ( usesPrevDelta , _ ) , c , _) and
2547
+ usesPrevDelta ( usesPrevDelta , true )
2524
2548
)
2525
2549
}
2526
2550
@@ -2566,47 +2590,63 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2566
2590
doublyBoundedFastTC( step / 2 , isStoreTargetPruned / 1 , isReadSourcePruned / 1 ) ( node1 , node2 )
2567
2591
2568
2592
pragma [ nomagic]
2569
- private predicate storeMayReachReadDeltaJoinLeft ( NodeEx node1 , Content c , NodeOrContent node2 ) {
2593
+ private predicate storeMayReachReadDeltaJoinLeft (
2594
+ NodeEx node1 , Content c , NodeOrContent node2 , boolean fromArg
2595
+ ) {
2570
2596
exists ( UsesPrevDeltaInfo usesPrevDelta |
2571
- storeMayReachARead ( node2 , c ) and
2572
- storeContentStep ( node1 , c , node2 .asNodeEx ( usesPrevDelta ) ) and
2573
- usesPrevDelta . toBoolean ( ) = false
2597
+ storeMayReachARead ( pragma [ only_bind_into ] ( node2 ) , pragma [ only_bind_into ] ( c ) ) and
2598
+ storeContentStep ( node1 , c , node2 .asNodeEx ( usesPrevDelta , fromArg ) ) and
2599
+ usesPrevDelta ( usesPrevDelta , false )
2574
2600
)
2575
2601
}
2576
2602
2577
2603
pragma [ nomagic]
2578
- private predicate storeMayReachReadDeltaJoinRight ( NodeOrContent node1 , Content c , NodeEx node2 ) {
2604
+ private predicate storeMayReachReadDeltaJoinRight (
2605
+ NodeOrContent node1 , Content c , NodeEx node2 , boolean fromArg
2606
+ ) {
2579
2607
exists ( UsesPrevDeltaInfo usesPrevDelta |
2580
- aStoreMayReachRead ( node1 , c ) and
2581
- readContentStep ( node1 .asNodeEx ( usesPrevDelta ) , c , node2 ) and
2582
- usesPrevDelta . toBoolean ( ) = true
2608
+ aStoreMayReachRead ( pragma [ only_bind_into ] ( node1 ) , pragma [ only_bind_into ] ( c ) ) and
2609
+ readContentStep ( node1 .asNodeEx ( usesPrevDelta , fromArg ) , c , node2 ) and
2610
+ usesPrevDelta ( usesPrevDelta , true )
2583
2611
)
2584
2612
}
2585
2613
2586
2614
pragma [ nomagic]
2587
- predicate storeMayReachReadDelta ( NodeEx storeSource , Content c , NodeEx readTarget ) {
2615
+ predicate storeMayReachReadDelta (
2616
+ NodeEx storeSource , Content c , NodeEx readTarget , boolean fromArg1 , boolean fromArg2
2617
+ ) {
2588
2618
exists ( NodeOrContent storeTarget , NodeOrContent readSource |
2589
2619
storeMayReachReadTc ( storeTarget , readSource ) and
2590
- storeMayReachReadDeltaJoinLeft ( storeSource , c , storeTarget ) and
2591
- storeMayReachReadDeltaJoinRight ( readSource , c , readTarget )
2620
+ storeMayReachReadDeltaJoinLeft ( storeSource , c , storeTarget , fromArg1 ) and
2621
+ storeMayReachReadDeltaJoinRight ( readSource , c , readTarget , fromArg2 )
2592
2622
) and
2593
- not Prev:: storeMayReachReadPrev ( storeSource , c , readTarget )
2623
+ not Prev:: storeMayReachReadPrev ( storeSource , c , readTarget , fromArg1 , fromArg2 )
2594
2624
}
2595
2625
2596
2626
pragma [ nomagic]
2597
- predicate storeMayReachReadPrev ( NodeEx storeSource , Content c , NodeEx readTarget ) {
2598
- Prev:: storeMayReachReadPrev ( storeSource , c , readTarget )
2627
+ predicate storeMayReachReadPrev (
2628
+ NodeEx storeSource , Content c , NodeEx readTarget , boolean fromArg1 , boolean fromArg2
2629
+ ) {
2630
+ Prev:: storeMayReachReadPrev ( storeSource , c , readTarget , fromArg1 , fromArg2 )
2599
2631
or
2600
- Prev:: storeMayReachReadDelta ( storeSource , c , readTarget )
2632
+ Prev:: storeMayReachReadDelta ( storeSource , c , readTarget , fromArg1 , fromArg2 )
2601
2633
}
2602
2634
}
2603
2635
2604
2636
module Iteration0 implements StoreReachesReadInputSig {
2605
2637
int iteration ( ) { result = 0 }
2606
2638
2607
- predicate storeMayReachReadDelta ( NodeEx node1 , Content c , NodeEx node2 ) { none ( ) }
2639
+ predicate storeMayReachReadDelta (
2640
+ NodeEx node1 , Content c , NodeEx node2 , boolean fromArg1 , boolean fromArg2
2641
+ ) {
2642
+ none ( )
2643
+ }
2608
2644
2609
- predicate storeMayReachReadPrev ( NodeEx node1 , Content c , NodeEx node2 ) { none ( ) }
2645
+ predicate storeMayReachReadPrev (
2646
+ NodeEx node1 , Content c , NodeEx node2 , boolean fromArg1 , boolean fromArg2
2647
+ ) {
2648
+ none ( )
2649
+ }
2610
2650
}
2611
2651
2612
2652
// in the first iteration there is no previous delta to use
@@ -2619,15 +2659,20 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2619
2659
2620
2660
import M
2621
2661
2622
- predicate storeMayReachReadDelta ( NodeEx storeSource , Content c , NodeEx readTarget ) {
2623
- M:: storeMayReachReadDelta ( storeSource , c , readTarget )
2662
+ predicate storeMayReachReadDelta (
2663
+ NodeEx storeSource , Content c , NodeEx readTarget , boolean fromArg1 , boolean fromArg2
2664
+ ) {
2665
+ M:: storeMayReachReadDelta ( storeSource , c , readTarget , fromArg1 , fromArg2 )
2624
2666
or
2625
2667
// special case only needed for the first iteration: a store immediately followed by a read
2626
2668
exists ( NodeEx storeTargetReadSource |
2627
2669
StoreReachesRead1:: contentIsReadAndStored ( c ) and
2628
2670
storeContentStep ( storeSource , c , storeTargetReadSource ) and
2629
2671
readContentStep ( storeTargetReadSource , c , readTarget )
2630
- )
2672
+ ) and
2673
+ nodeRange ( storeSource , fromArg1 ) and
2674
+ nodeRange ( readTarget , fromArg2 ) and
2675
+ fromArg1 = fromArg2
2631
2676
}
2632
2677
}
2633
2678
@@ -2650,9 +2695,9 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
2650
2695
StoreReachesRead< StoreReachesRead4 , UsesPrevDeltaInfoBoolean > ;
2651
2696
2652
2697
predicate storeMayReachRead ( NodeEx storeSource , Content c , NodeEx readTarget ) {
2653
- StoreReachesRead5:: storeMayReachReadDelta ( storeSource , c , readTarget )
2698
+ StoreReachesRead5:: storeMayReachReadDelta ( storeSource , c , readTarget , _ , _ )
2654
2699
or
2655
- StoreReachesRead5:: storeMayReachReadPrev ( storeSource , c , readTarget )
2700
+ StoreReachesRead5:: storeMayReachReadPrev ( storeSource , c , readTarget , _ , _ )
2656
2701
}
2657
2702
}
2658
2703
}
0 commit comments