@@ -1223,7 +1223,16 @@ private module MkStage<StageSig PrevStage> {
12231223 bindingset [ tc, tail]
12241224 Ap apCons ( TypedContent tc , Ap tail ) ;
12251225
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 ) ;
12271236
12281237 class ApOption ;
12291238
@@ -1471,34 +1480,32 @@ private module MkStage<StageSig PrevStage> {
14711480 )
14721481 }
14731482
1474- private class ApNonNil instanceof Ap {
1475- pragma [ nomagic]
1476- ApNonNil ( ) { not this instanceof ApNil }
1477-
1478- string toString ( ) { result = "" }
1479- }
1480-
14811483 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
14851486 ) {
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 )
14881489 }
14891490
1490- bindingset [ ap , c ]
1491+ bindingset [ node1 , apc ]
14911492 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+ }
14931498
14941499 pragma [ nomagic]
14951500 private predicate fwdFlowRead (
14961501 Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
14971502 ParamNodeOption summaryCtx , ApOption argAp , Configuration config
14981503 ) {
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+ )
15021509 }
15031510
15041511 pragma [ nomagic]
@@ -2072,8 +2079,12 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
20722079 bindingset [ tc, tail]
20732080 Ap apCons ( TypedContent tc , Ap tail ) { result = true and exists ( tc ) and exists ( tail ) }
20742081
2082+ class ApHeadContent = Unit ;
2083+
20752084 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 ( ) }
20772088
20782089 class ApOption = BooleanOption ;
20792090
@@ -2337,8 +2348,12 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
23372348 bindingset [ tc, tail]
23382349 Ap apCons ( TypedContent tc , Ap tail ) { result .getAHead ( ) = tc and exists ( tail ) }
23392350
2351+ class ApHeadContent = ContentApprox ;
2352+
23402353 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 ;
23422357
23432358 class ApOption = ApproxAccessPathFrontOption ;
23442359
@@ -2413,8 +2428,12 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
24132428 bindingset [ tc, tail]
24142429 Ap apCons ( TypedContent tc , Ap tail ) { result .getHead ( ) = tc and exists ( tail ) }
24152430
2431+ class ApHeadContent = Content ;
2432+
24162433 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 }
24182437
24192438 class ApOption = AccessPathFrontOption ;
24202439
@@ -2743,8 +2762,12 @@ private module Stage5Param implements MkStage<Stage4>::StageParam {
27432762 bindingset [ tc, tail]
27442763 Ap apCons ( TypedContent tc , Ap tail ) { result = push ( tc , tail ) }
27452764
2765+ class ApHeadContent = Content ;
2766+
27462767 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 }
27482771
27492772 class ApOption = AccessPathApproxOption ;
27502773
0 commit comments