@@ -2170,9 +2170,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2170
2170
returnAp = apNone ( )
2171
2171
or
2172
2172
// store
2173
- exists ( Ap ap0 , Content c |
2173
+ exists ( NodeEx readTarget , Ap ap0 , Content c |
2174
2174
revFlowStore ( ap0 , c , ap , _, node , state , _, returnCtx , returnAp ) and
2175
- revFlowConsCand ( ap0 , c , ap )
2175
+ revFlowConsCand ( readTarget , ap0 , c , ap ) and
2176
+ PrevStage:: storeReachesRead ( node , readTarget )
2176
2177
)
2177
2178
or
2178
2179
// read
@@ -2238,11 +2239,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2238
2239
* resulting in access path `cons`.
2239
2240
*/
2240
2241
pragma [ nomagic]
2241
- private predicate revFlowConsCand ( Ap cons , Content c , Ap tail ) {
2242
- exists ( NodeEx mid , Ap tail0 |
2243
- revFlow ( mid , _, _, _, tail ) and
2242
+ private predicate revFlowConsCand ( NodeEx readTarget , Ap cons , Content c , Ap tail ) {
2243
+ exists ( Ap tail0 |
2244
+ revFlow ( readTarget , _, _, _, tail ) and
2244
2245
tail = pragma [ only_bind_into ] ( tail0 ) and
2245
- readStepFwd ( _, cons , c , mid , tail0 )
2246
+ readStepFwd ( _, cons , c , readTarget , tail0 )
2246
2247
)
2247
2248
}
2248
2249
@@ -2370,7 +2371,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2370
2371
exists ( Ap ap2 |
2371
2372
PrevStage:: storeStepCand ( node1 , _, c , node2 , contentType , containerType ) and
2372
2373
revFlowStore ( ap2 , c , ap1 , _, node1 , _, node2 , _, _) and
2373
- revFlowConsCand ( ap2 , c , ap1 )
2374
+ revFlowConsCand ( _ , ap2 , c , ap1 )
2374
2375
)
2375
2376
}
2376
2377
@@ -2397,7 +2398,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2397
2398
private predicate revConsCand ( Content c , Typ t , Ap ap ) {
2398
2399
exists ( Ap ap2 |
2399
2400
revFlowStore ( ap2 , c , ap , t , _, _, _, _, _) and
2400
- revFlowConsCand ( ap2 , c , ap )
2401
+ revFlowConsCand ( _ , ap2 , c , ap )
2401
2402
)
2402
2403
}
2403
2404
@@ -2502,18 +2503,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2502
2503
2503
2504
private signature predicate storeReachesReadSig ( NodeEx node1 , NodeEx node2 ) ;
2504
2505
2505
- private newtype TNodeAndAp = MkNodeAndAp ( TNodeEx node , Ap ap ) { revFlow ( node , _, _, _, ap ) }
2506
-
2507
2506
private module StoreReachesRead< storeReachesReadSig / 2 storeReachesReadIn> {
2508
2507
pragma [ nomagic]
2509
- private predicate step ( TNodeAndAp n1 , TNodeAndAp n2 ) {
2510
- exists ( NodeEx node1 , NodeEx node2 , Ap ap , FlowState state1 , FlowState state2 |
2511
- revFlow ( node1 , state1 ) and
2512
- revFlow ( node2 , state2 ) and
2513
- n1 = MkNodeAndAp ( node1 , pragma [ only_bind_into ] ( ap ) ) and
2514
- n2 = MkNodeAndAp ( node2 , pragma [ only_bind_into ] ( ap ) )
2508
+ private predicate step ( NodeEx node1 , NodeEx node2 ) {
2509
+ exists ( FlowState state , Ap ap , ApOption returnAp1 , ApOption returnAp2 |
2510
+ revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _, returnAp1 , pragma [ only_bind_into ] ( ap ) ) and
2511
+ revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _, returnAp2 , pragma [ only_bind_into ] ( ap ) )
2515
2512
|
2516
- localStep ( node1 , state1 , node2 , state2 , true , _, _)
2513
+ localStep ( node1 , state , node2 , state , true , _, _) and
2514
+ returnAp1 = returnAp2
2517
2515
or
2518
2516
jumpStepEx ( node1 , node2 )
2519
2517
or
@@ -2525,30 +2523,31 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2525
2523
)
2526
2524
}
2527
2525
2528
- private predicate isStoreTarget ( TNodeAndAp n ) {
2529
- exists ( NodeEx node , Ap ap |
2530
- n = MkNodeAndAp ( node , ap ) and
2531
- storeStepCand ( _, _, _, node , _, _)
2532
- )
2533
- }
2526
+ private predicate isStoreTarget ( NodeEx node ) { storeStepCand ( _, _, _, node , _, _) }
2534
2527
2535
- private predicate isReadSource ( TNodeAndAp n ) {
2536
- exists ( NodeEx node , Ap ap |
2537
- n = MkNodeAndAp ( node , ap ) and
2538
- readStepCand ( node , _, _)
2539
- )
2540
- }
2528
+ private predicate isReadSource ( NodeEx node ) { readStepCand ( node , _, _) }
2541
2529
2542
- private predicate storeReachesReadTc ( TNodeAndAp node1 , TNodeAndAp node2 ) =
2530
+ private predicate storeReachesReadTc ( NodeEx node1 , NodeEx node2 ) =
2543
2531
doublyBoundedFastTC( step / 2 , isStoreTarget / 1 , isReadSource / 1 ) ( node1 , node2 )
2544
2532
2533
+ bindingset [ node2, c]
2534
+ pragma [ inline_late]
2535
+ private predicate storeStepCand ( NodeEx node1 , Content c , NodeEx node2 ) {
2536
+ storeStepCand ( node1 , _, c , node2 , _, _)
2537
+ }
2538
+
2545
2539
pragma [ nomagic]
2546
2540
predicate storeReachesReadOut ( NodeEx node1 , NodeEx node2 ) {
2547
2541
exists ( Content c , NodeEx storeTarget , NodeEx readSource |
2548
- storeReachesReadTc ( MkNodeAndAp ( storeTarget , _ ) , MkNodeAndAp ( readSource , _ ) ) and
2549
- storeStepCand ( node1 , _ , c , storeTarget , _ , _ ) and
2542
+ storeReachesReadTc ( storeTarget , readSource ) and
2543
+ storeStepCand ( node1 , c , storeTarget ) and
2550
2544
readStepCand ( readSource , c , node2 )
2551
2545
)
2546
+ or
2547
+ exists ( Content c , NodeEx storeTargetReadSource |
2548
+ storeStepCand ( node1 , c , storeTargetReadSource ) and
2549
+ readStepCand ( storeTargetReadSource , c , node2 )
2550
+ )
2552
2551
}
2553
2552
}
2554
2553
0 commit comments