@@ -1322,31 +1322,27 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1322
1322
}
1323
1323
}
1324
1324
1325
- private module Cached {
1326
- cached
1327
- newtype TNode =
1328
- TParamNode ( DfInput:: Parameter p ) { DfInput:: ssaDefInitializesParam ( _, p ) } or
1329
- TExprNode ( DfInput:: Expr e , Boolean isPost ) {
1330
- e = DfInput:: getARead ( _)
1331
- or
1332
- DfInput:: ssaDefAssigns ( _, e ) and
1325
+ cached
1326
+ private DefinitionExt getAPhiInputDef ( SsaInputDefinitionExt phi , BasicBlock bb ) {
1327
+ phi .hasInputFromBlock ( result , _, _, _, bb )
1328
+ }
1329
+
1330
+ private newtype TNode =
1331
+ TParamNode ( DfInput:: Parameter p ) {
1332
+ exists ( WriteDefinition def | DfInput:: ssaDefInitializesParam ( def , p ) )
1333
+ } or
1334
+ TExprNode ( DfInput:: Expr e , Boolean isPost ) {
1335
+ e = DfInput:: getARead ( _)
1336
+ or
1337
+ exists ( DefinitionExt def |
1338
+ DfInput:: ssaDefAssigns ( def , e ) and
1333
1339
isPost = false
1334
- } or
1335
- TSsaDefinitionNode ( DefinitionExt def ) or
1336
- TSsaInputNode ( SsaInputDefinitionExt def , BasicBlock input ) {
1337
- def .hasInputFromBlock ( _, _, _, _, input )
1338
- }
1339
-
1340
- cached
1341
- Definition getAPhiInputDef ( SsaInputNode n ) {
1342
- exists ( SsaInputDefinitionExt phi , BasicBlock bb |
1343
- phi .hasInputFromBlock ( result , _, _, _, bb ) and
1344
- n .isInputInto ( phi , bb )
1345
1340
)
1341
+ } or
1342
+ TSsaDefinitionNode ( DefinitionExt def ) or
1343
+ TSsaInputNode ( SsaInputDefinitionExt phi , BasicBlock input ) {
1344
+ exists ( getAPhiInputDef ( phi , input ) )
1346
1345
}
1347
- }
1348
-
1349
- private import Cached
1350
1346
1351
1347
/**
1352
1348
* A data flow node that we need to reference in the value step relation.
@@ -1627,6 +1623,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1627
1623
*/
1628
1624
signature predicate guardChecksSig ( DfInput:: Guard g , DfInput:: Expr e , boolean branch ) ;
1629
1625
1626
+ pragma [ nomagic]
1627
+ private Definition getAPhiInputDef ( SsaInputNode n ) {
1628
+ exists ( SsaInputDefinitionExt phi , BasicBlock bb |
1629
+ result = getAPhiInputDef ( phi , bb ) and
1630
+ n .isInputInto ( phi , bb )
1631
+ )
1632
+ }
1633
+
1630
1634
/**
1631
1635
* Provides a set of barrier nodes for a guard that validates an expression.
1632
1636
*
0 commit comments