SSA: Reduce caching in data-flow integration layer

Author: hvitved

shared/ssa/codeql/ssa/Ssa.qll

@@ -1307,11 +1307,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     /** An SSA definition into which another SSA definition may flow. */
     private class SsaInputDefinitionExt extends DefinitionExtFinal {
       SsaInputDefinitionExt() {
-        this instanceof PhiNode
-        or
-        this instanceof PhiReadNode
-        or
-        DfInput::allowFlowIntoUncertainDef(this)
+        hasCertainRead(this) and
+        (
+          this instanceof PhiNode
+          or
+          this instanceof PhiReadNode
+          or
+          DfInput::allowFlowIntoUncertainDef(this)
+        )
       }
 
       /** Holds if `def` may flow into this definition via basic block `input`. */
@@ -1324,30 +1327,45 @@ module Make<LocationSig Location, InputSig<Location> Input> {
 
     private module Cached {
       cached
-      newtype TNode =
-        TParamNode(DfInput::Parameter p) { DfInput::ssaDefInitializesParam(_, p) } or
-        TExprNode(DfInput::Expr e, Boolean isPost) {
-          e = DfInput::getARead(_)
-          or
-          DfInput::ssaDefAssigns(_, e) and
-          isPost = false
-        } or
-        TSsaDefinitionNode(DefinitionExt def) or
-        TSsaInputNode(SsaInputDefinitionExt def, BasicBlock input) {
-          def.hasInputFromBlock(_, _, _, _, input)
-        }
+      predicate hasCertainRead(DefinitionExt def) {
+        exists(SourceVariable v, BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+          def.definesAt(v, bb1, i1, _) and
+          adjacentDefSkipUncertainReadsExt(def, v, bb1, i1, bb2, i2) and
+          variableRead(bb2, i2, v, true)
+        )
+        or
+        def = getAPhiInputDef(_, _)
+      }
 
       cached
-      Definition getAPhiInputDef(SsaInputNode n) {
-        exists(SsaInputDefinitionExt phi, BasicBlock bb |
-          phi.hasInputFromBlock(result, _, _, _, bb) and
-          n.isInputInto(phi, bb)
-        )
+      DefinitionExt getAPhiInputDef(SsaInputDefinitionExt phi, BasicBlock bb) {
+        phi.hasInputFromBlock(result, _, _, _, bb)
       }
     }
 
     private import Cached
 
+    private newtype TNode =
+      TParamNode(DfInput::Parameter p) {
+        exists(WriteDefinition def |
+          DfInput::ssaDefInitializesParam(def, p) and
+          hasCertainRead(def)
+        )
+      } or
+      TExprNode(DfInput::Expr e, Boolean isPost) {
+        e = DfInput::getARead(_)
+        or
+        exists(DefinitionExt def |
+          DfInput::ssaDefAssigns(def, e) and
+          hasCertainRead(def) and
+          isPost = false
+        )
+      } or
+      TSsaDefinitionNode(DefinitionExt def) { hasCertainRead(def) } or
+      TSsaInputNode(SsaInputDefinitionExt phi, BasicBlock input) {
+        exists(getAPhiInputDef(phi, input))
+      }
+
     /**
      * A data flow node that we need to reference in the value step relation.
      *
@@ -1627,6 +1645,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      */
     signature predicate guardChecksSig(DfInput::Guard g, DfInput::Expr e, boolean branch);
 
+    pragma[nomagic]
+    private Definition getAPhiInputDef(SsaInputNode n) {
+      exists(SsaInputDefinitionExt phi, BasicBlock bb |
+        result = getAPhiInputDef(phi, bb) and
+        n.isInputInto(phi, bb)
+      )
+    }
+
     /**
      * Provides a set of barrier nodes for a guard that validates an expression.
      *