@@ -1326,40 +1326,81 @@ predicate localInstructionFlow(Instruction e1, Instruction e2) {
13261326 localFlow ( instructionNode ( e1 ) , instructionNode ( e2 ) )
13271327}
13281328
1329+ cached
1330+ private module ExprFlowCached {
1331+ /**
1332+ * Holds if `n1.asExpr()` doesn't have a result and `n1` flows to `n2` in a single
1333+ * dataflow step.
1334+ */
1335+ private predicate localStepFromNonExpr ( Node n1 , Node n2 ) {
1336+ not exists ( n1 .asExpr ( ) ) and
1337+ localFlowStep ( n1 , n2 )
1338+ }
1339+
1340+ /**
1341+ * Holds if `n1.asExpr()` doesn't have a result, `n2.asExpr() = e2` and
1342+ * `n2` is the first node reachable from `n1` such that `n2.asExpr()` exists.
1343+ */
1344+ pragma [ nomagic]
1345+ private predicate localStepsToExpr ( Node n1 , Node n2 , Expr e2 ) {
1346+ localStepFromNonExpr * ( n1 , n2 ) and
1347+ e2 = n2 .asExpr ( )
1348+ }
1349+
1350+ /**
1351+ * Holds if `n1.asExpr() = e1` and `n2.asExpr() = e2` and `n2` is the first node
1352+ * reacahble from `n1` such that `n2.asExpr()` exists.
1353+ */
1354+ private predicate localExprFlowSingleExprStep ( Node n1 , Expr e1 , Node n2 , Expr e2 ) {
1355+ exists ( Node mid |
1356+ localFlowStep ( n1 , mid ) and
1357+ localStepsToExpr ( mid , n2 , e2 ) and
1358+ e1 = n1 .asExpr ( )
1359+ )
1360+ }
1361+
1362+ /**
1363+ * Holds if `n1.asExpr() = e1` and `e1 != e2` and `n2` is the first reachable node from
1364+ * `n1` such that `n2.asExpr() = e2`.
1365+ */
1366+ private predicate localExprFlowStepImpl ( Node n1 , Expr e1 , Node n2 , Expr e2 ) {
1367+ exists ( Node n , Expr e | localExprFlowSingleExprStep ( n1 , e1 , n , e ) |
1368+ // If `n.asExpr()` and `n1.asExpr()` both resolve to the same node (which can
1369+ // happen if `n2` is the node attached to a conversion of `e1`), then we recursively
1370+ // perform another expression step.
1371+ if e1 = e
1372+ then localExprFlowStepImpl ( n , e , n2 , e2 )
1373+ else (
1374+ // If we manage to step to a different expression we're done.
1375+ e2 = e and
1376+ n2 = n
1377+ )
1378+ )
1379+ }
1380+
1381+ /** Holds if data can flow from `e1` to `e2` in one local (intra-procedural) step. */
1382+ cached
1383+ predicate localExprFlowStep ( Expr e1 , Expr e2 ) { localExprFlowStepImpl ( _, e1 , _, e2 ) }
1384+ }
1385+
1386+ import ExprFlowCached
1387+
13291388/**
1330- * Holds if data can flow from `e1` to `e2` in zero or more
1389+ * Holds if data can flow from `e1` to `e2` in one or more
13311390 * local (intra-procedural) steps.
13321391 */
13331392pragma [ inline]
1334- predicate localExprFlow ( Expr e1 , Expr e2 ) { localExprFlowStep * ( e1 , e2 ) }
1335-
1336- /**
1337- * Holds if `n1.asExpr()` doesn't have a result and `n1` flows to `n2` in a single
1338- * dataflow step.
1339- */
1340- private predicate localStepFromNonExpr ( Node n1 , Node n2 ) {
1341- not exists ( n1 .asExpr ( ) ) and
1342- localFlowStep ( n1 , n2 )
1343- }
1393+ private predicate localExprFlowPlus ( Expr e1 , Expr e2 ) = fastTC( localExprFlowStep / 2 ) ( e1 , e2 )
13441394
13451395/**
1346- * Holds if `n1.asExpr()` doesn't have a result, `n2.asExpr() = e2` and
1347- * `n2` is the first node reachable from `n1` such that `n2.asExpr()` exists .
1396+ * Holds if data can flow from `e1` to ` e2` in zero or more
1397+ * local (intra-procedural) steps .
13481398 */
1349- pragma [ nomagic]
1350- private predicate localStepsToExpr ( Node n1 , Node n2 , Expr e2 ) {
1351- localStepFromNonExpr * ( n1 , n2 ) and
1352- e2 = n2 .asExpr ( )
1353- }
1354-
1355- /** Holds if data can flow from `e1` to `e2` in one local (intra-procedural) step. */
1356- cached
1357- predicate localExprFlowStep ( Expr e1 , Expr e2 ) {
1358- exists ( Node mid , Node n1 , Node n2 |
1359- localFlowStep ( n1 , mid ) and
1360- localStepsToExpr ( mid , n2 , e2 ) and
1361- e1 = n1 .asExpr ( )
1362- )
1399+ pragma [ inline]
1400+ predicate localExprFlow ( Expr e1 , Expr e2 ) {
1401+ e1 = e2
1402+ or
1403+ localExprFlowPlus ( e1 , e2 )
13631404}
13641405
13651406cached
0 commit comments