refactor

Author: hvitved

shared/ssa/codeql/ssa/Ssa.qll

@@ -1198,6 +1198,21 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      * previous definitions or reads.
      */
     default predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) { none() }
+
+    /** A (potential) guard. */
+    class Guard {
+      /** Gets a textual representation of this guard. */
+      string toString();
+
+      /** Holds if the `i`th node of basic block `bb` evaluates this guard. */
+      predicate hasCfgNode(BasicBlock bb, int i);
+    }
+
+    /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
+    predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch);
+
+    /** Gets an immediate conditional successor of basic block `bb`, if any. */
+    BasicBlock getAConditionalBasicBlockSuccessor(BasicBlock bb, boolean branch);
   }
 
   /**
@@ -1294,6 +1309,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       }
     }
 
+    cached
+    private predicate ssaInputNode(SsaInputDefinitionExt def, BasicBlock input) {
+      def.hasInputFromBlock(_, _, _, _, input)
+    }
+
     private newtype TNode =
       TParamNode(DfInput::Parameter p) or
       TExprNode(DfInput::Expr e, Boolean isPost) {
@@ -1305,9 +1325,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
         isPost = false
       } or
       TSsaDefinitionNode(DefinitionExt def) or
-      TSsaInputNode(SsaInputDefinitionExt def, BasicBlock input) {
-        def.hasInputFromBlock(_, _, _, _, input)
-      }
+      TSsaInputNode(SsaInputDefinitionExt def, BasicBlock input) { ssaInputNode(def, input) }
 
     /**
      * A data flow node that we need to reference in the value step relation.
@@ -1577,94 +1595,46 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       nodeTo.(ExprNode).getExpr() = getARead(def)
     }
 
-    /** Provides the input to `BarrierGuards`. */
-    signature module BarrierGuardsInputSig {
-      /** A (potential) guard. */
-      class Guard {
-        /** Gets a textual representation of this guard. */
-        string toString();
+    pragma[nomagic]
+    private predicate guardControlsSsaRead(
+      DfInput::Guard g, boolean branch, Definition def, ExprNode n
+    ) {
+      exists(BasicBlock bb, DfInput::Expr e |
+        e = n.getExpr() and
+        getARead(def) = e and
+        DfInput::guardControlsBlock(g, bb, branch) and
+        e.hasCfgNode(bb, _)
+      )
+    }
 
-        /** Holds if the `i`th node of basic block `bb` evaluates this guard. */
-        predicate hasCfgNode(BasicBlock bb, int i);
-      }
+    pragma[nomagic]
+    private predicate guardControlsPhiInput(
+      DfInput::Guard g, boolean branch, Definition def, BasicBlock input, SsaInputDefinitionExt phi
+    ) {
+      phi.hasInputFromBlock(def, _, _, _, input) and
+      (
+        DfInput::guardControlsBlock(g, input, branch)
+        or
+        exists(int last |
+          last = input.length() - 1 and
+          g.hasCfgNode(input, last) and
+          DfInput::getAConditionalBasicBlockSuccessor(input, branch) = phi.getBasicBlock()
+        )
+      )
+    }
 
-      /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
-      predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch);
-
-      /** Gets an immediate conditional successor of basic block `bb`, if any. */
-      BasicBlock getAConditionalBasicBlockSuccessor(BasicBlock bb, boolean branch);
-    }
-
-    /** Provides an implementatino of the `BarrierGuard` module. */
-    module BarrierGuards<BarrierGuardsInputSig BgInput> {
-      /**
-       * Holds if the guard `g` validates the expression `e` upon evaluating to `branch`.
-       *
-       * The expression `e` is expected to be a syntactic part of the guard `g`.
-       * For example, the guard `g` might be a call `isSafe(x)` and the expression `e`
-       * the argument `x`.
-       */
-      signature predicate guardChecksSig(BgInput::Guard g, DfInput::Expr e, boolean branch);
-
-      /**
-       * Provides a set of barrier nodes for a guard that validates an expression.
-       *
-       * This is expected to be used in `isBarrier`/`isSanitizer` definitions
-       * in data flow and taint tracking.
-       */
-      module BarrierGuard<guardChecksSig/3 guardChecks> {
-        pragma[nomagic]
-        private predicate guardChecksSsaDef(BgInput::Guard g, boolean branch, Definition def) {
-          guardChecks(g, getARead(def), branch)
-        }
-
-        pragma[nomagic]
-        private predicate guardControlsSsaRead(
-          BgInput::Guard g, boolean branch, Definition def, ExprNode n
-        ) {
-          exists(BasicBlock bb, DfInput::Expr e |
-            e = n.getExpr() and
-            getARead(def) = e and
-            BgInput::guardControlsBlock(g, bb, branch) and
-            e.hasCfgNode(bb, _)
-          )
-        }
-
-        pragma[nomagic]
-        private predicate guardControlsPhiInput(
-          BgInput::Guard g, boolean branch, Definition def, BasicBlock input,
-          SsaInputDefinitionExt phi
-        ) {
-          phi.hasInputFromBlock(def, _, _, _, input) and
-          (
-            BgInput::guardControlsBlock(g, input, branch)
-            or
-            exists(int last |
-              last = input.length() - 1 and
-              g.hasCfgNode(input, last) and
-              BgInput::getAConditionalBasicBlockSuccessor(input, branch) = phi.getBasicBlock()
-            )
-          )
-        }
-
-        /** Gets a node that is safely guarded by the given guard check. */
-        pragma[nomagic]
-        Node getABarrierNode() {
-          exists(BgInput::Guard g, boolean branch, Definition def |
-            guardChecksSsaDef(g, branch, def) and
-            guardControlsSsaRead(g, branch, def, result)
-          )
-          or
-          exists(
-            BgInput::Guard g, boolean branch, Definition def, BasicBlock input,
-            SsaInputDefinitionExt phi
-          |
-            guardChecksSsaDef(g, branch, def) and
-            guardControlsPhiInput(g, branch, def, input, phi) and
-            result.(SsaInputNode).isInputInto(phi, input)
-          )
-        }
-      }
+    /**
+     * Gets a node that reads SSA defininition `def`, and which is guarded by
+     * `g` evaluating to `branch`.
+     */
+    pragma[nomagic]
+    Node getABarrierNode(DfInput::Guard g, Definition def, boolean branch) {
+      guardControlsSsaRead(g, branch, def, result)
+      or
+      exists(BasicBlock input, SsaInputDefinitionExt phi |
+        guardControlsPhiInput(g, branch, def, input, phi) and
+        result.(SsaInputNode).isInputInto(phi, input)
+      )
     }
   }
 }