@@ -1223,7 +1223,16 @@ private module MkStage<StageSig PrevStage> {
1223
1223
bindingset [ tc, tail]
1224
1224
Ap apCons ( TypedContent tc , Ap tail ) ;
1225
1225
1226
- Content getHeadContent ( Ap ap ) ;
1226
+ /**
1227
+ * An approximation of `Content` that corresponds to the precision level of
1228
+ * `Ap`, such that the mappings from both `Ap` and `Content` to this type
1229
+ * are functional.
1230
+ */
1231
+ class ApHeadContent ;
1232
+
1233
+ ApHeadContent getHeadContent ( Ap ap ) ;
1234
+
1235
+ ApHeadContent projectToHeadContent ( Content c ) ;
1227
1236
1228
1237
class ApOption ;
1229
1238
@@ -1471,34 +1480,32 @@ private module MkStage<StageSig PrevStage> {
1471
1480
)
1472
1481
}
1473
1482
1474
- private class ApNonNil instanceof Ap {
1475
- pragma [ nomagic]
1476
- ApNonNil ( ) { not this instanceof ApNil }
1477
-
1478
- string toString ( ) { result = "" }
1479
- }
1480
-
1481
1483
pragma [ nomagic]
1482
- private predicate fwdFlowRead0 (
1483
- NodeEx node1 , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , ApNonNil ap ,
1484
- Configuration config
1484
+ private predicate readStepCand (
1485
+ NodeEx node1 , ApHeadContent apc , Content c , NodeEx node2 , Configuration config
1485
1486
) {
1486
- fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1487
- PrevStage :: readStepCand ( node1 , _ , _ , config )
1487
+ PrevStage :: readStepCand ( node1 , c , node2 , config ) and
1488
+ apc = projectToHeadContent ( c )
1488
1489
}
1489
1490
1490
- bindingset [ ap , c ]
1491
+ bindingset [ node1 , apc ]
1491
1492
pragma [ inline_late]
1492
- private predicate hasHeadContent ( Ap ap , Content c ) { getHeadContent ( ap ) = c }
1493
+ private predicate readStepCand0 (
1494
+ NodeEx node1 , ApHeadContent apc , Content c , NodeEx node2 , Configuration config
1495
+ ) {
1496
+ readStepCand ( node1 , apc , c , node2 , config )
1497
+ }
1493
1498
1494
1499
pragma [ nomagic]
1495
1500
private predicate fwdFlowRead (
1496
1501
Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
1497
1502
ParamNodeOption summaryCtx , ApOption argAp , Configuration config
1498
1503
) {
1499
- fwdFlowRead0 ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1500
- PrevStage:: readStepCand ( node1 , c , node2 , config ) and
1501
- hasHeadContent ( ap , c )
1504
+ exists ( ApHeadContent apc |
1505
+ fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1506
+ apc = getHeadContent ( ap ) and
1507
+ readStepCand0 ( node1 , apc , c , node2 , config )
1508
+ )
1502
1509
}
1503
1510
1504
1511
pragma [ nomagic]
@@ -2072,8 +2079,12 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
2072
2079
bindingset [ tc, tail]
2073
2080
Ap apCons ( TypedContent tc , Ap tail ) { result = true and exists ( tc ) and exists ( tail ) }
2074
2081
2082
+ class ApHeadContent = Unit ;
2083
+
2075
2084
pragma [ inline]
2076
- Content getHeadContent ( Ap ap ) { exists ( result ) and ap = true }
2085
+ ApHeadContent getHeadContent ( Ap ap ) { exists ( result ) and ap = true }
2086
+
2087
+ ApHeadContent projectToHeadContent ( Content c ) { any ( ) }
2077
2088
2078
2089
class ApOption = BooleanOption ;
2079
2090
@@ -2337,8 +2348,12 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
2337
2348
bindingset [ tc, tail]
2338
2349
Ap apCons ( TypedContent tc , Ap tail ) { result .getAHead ( ) = tc and exists ( tail ) }
2339
2350
2351
+ class ApHeadContent = ContentApprox ;
2352
+
2340
2353
pragma [ noinline]
2341
- Content getHeadContent ( Ap ap ) { result = ap .getAHead ( ) .getContent ( ) }
2354
+ ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( ) .getContent ( ) }
2355
+
2356
+ predicate projectToHeadContent = getContentApprox / 1 ;
2342
2357
2343
2358
class ApOption = ApproxAccessPathFrontOption ;
2344
2359
@@ -2413,8 +2428,12 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
2413
2428
bindingset [ tc, tail]
2414
2429
Ap apCons ( TypedContent tc , Ap tail ) { result .getHead ( ) = tc and exists ( tail ) }
2415
2430
2431
+ class ApHeadContent = Content ;
2432
+
2416
2433
pragma [ noinline]
2417
- Content getHeadContent ( Ap ap ) { result = ap .getHead ( ) .getContent ( ) }
2434
+ ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( ) .getContent ( ) }
2435
+
2436
+ ApHeadContent projectToHeadContent ( Content c ) { result = c }
2418
2437
2419
2438
class ApOption = AccessPathFrontOption ;
2420
2439
@@ -2743,8 +2762,12 @@ private module Stage5Param implements MkStage<Stage4>::StageParam {
2743
2762
bindingset [ tc, tail]
2744
2763
Ap apCons ( TypedContent tc , Ap tail ) { result = push ( tc , tail ) }
2745
2764
2765
+ class ApHeadContent = Content ;
2766
+
2746
2767
pragma [ noinline]
2747
- Content getHeadContent ( Ap ap ) { result = ap .getHead ( ) .getContent ( ) }
2768
+ ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( ) .getContent ( ) }
2769
+
2770
+ ApHeadContent projectToHeadContent ( Content c ) { result = c }
2748
2771
2749
2772
class ApOption = AccessPathApproxOption ;
2750
2773
0 commit comments