Guards/Java: Use BasicBlock signature in Guards library.

Author: aschackmull

java/ql/lib/semmle/code/java/controlflow/Guards.qll

@@ -139,20 +139,17 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
   )
 }
 
-private module GuardsInput implements SharedGuards::InputSig<Location> {
+private module SuccessorTypes implements SharedGuards::SuccessorTypesSig<SuccessorType> {
+  import SuccessorType
+}
+
+private module GuardsInput implements SharedGuards::InputSig<Location, ControlFlowNode, BasicBlock> {
   private import java as J
   private import semmle.code.java.dataflow.internal.BaseSSA
   private import semmle.code.java.dataflow.NullGuards as NullGuards
-  import SuccessorType
-
-  class ControlFlowNode = J::ControlFlowNode;
 
   class NormalExitNode = ControlFlow::NormalExitNode;
 
-  class BasicBlock = J::BasicBlock;
-
-  predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }
-
   class AstNode = ExprParent;
 
   class Expr = J::Expr;
@@ -382,7 +379,7 @@ private module GuardsInput implements SharedGuards::InputSig<Location> {
   }
 }
 
-private module GuardsImpl = SharedGuards::Make<Location, GuardsInput>;
+private module GuardsImpl = SharedGuards::Make<Location, Cfg, SuccessorTypes, GuardsInput>;
 
 private module LogicInputCommon {
   private import semmle.code.java.dataflow.NullGuards as NullGuards

shared/controlflow/codeql/controlflow/Guards.qll

@@ -50,16 +50,14 @@
 overlay[local?]
 module;
 
+private import codeql.controlflow.BasicBlock as BB
 private import codeql.util.Boolean
 private import codeql.util.Location
 private import codeql.util.Unit
 
-signature module InputSig<LocationSig Location> {
-  class SuccessorType {
-    /** Gets a textual representation of this successor type. */
-    string toString();
-  }
+signature class TypSig;
 
+signature module SuccessorTypesSig<TypSig SuccessorType> {
   class ExceptionSuccessor extends SuccessorType;
 
   class ConditionalSuccessor extends SuccessorType {
@@ -70,61 +68,12 @@ signature module InputSig<LocationSig Location> {
   class BooleanSuccessor extends ConditionalSuccessor;
 
   class NullnessSuccessor extends ConditionalSuccessor;
+}
 
-  /** A control flow node. */
-  class ControlFlowNode {
-    /** Gets a textual representation of this control flow node. */
-    string toString();
-
-    /** Gets the location of this control flow node. */
-    Location getLocation();
-  }
-
+signature module InputSig<LocationSig Location, TypSig ControlFlowNode, TypSig BasicBlock> {
   /** A control flow node indicating normal termination of a callable. */
   class NormalExitNode extends ControlFlowNode;
 
-  /**
-   * A basic block, that is, a maximal straight-line sequence of control flow nodes
-   * without branches or joins.
-   */
-  class BasicBlock {
-    /** Gets a textual representation of this basic block. */
-    string toString();
-
-    /** Gets the `i`th node in this basic block. */
-    ControlFlowNode getNode(int i);
-
-    /** Gets the last control flow node in this basic block. */
-    ControlFlowNode getLastNode();
-
-    /** Gets the length of this basic block. */
-    int length();
-
-    /** Gets the location of this basic block. */
-    Location getLocation();
-
-    BasicBlock getASuccessor(SuccessorType t);
-
-    predicate dominates(BasicBlock bb);
-
-    predicate strictlyDominates(BasicBlock bb);
-  }
-
-  /**
-   * Holds if `bb1` has `bb2` as a direct successor and the edge between `bb1`
-   * and `bb2` is a dominating edge.
-   *
-   * An edge `(bb1, bb2)` is dominating if there exists a basic block that can
-   * only be reached from the entry block by going through `(bb1, bb2)`. This
-   * implies that `(bb1, bb2)` dominates its endpoint `bb2`. I.e., `bb2` can
-   * only be reached from the entry block by going via `(bb1, bb2)`.
-   *
-   * This is a necessary and sufficient condition for an edge to dominate some
-   * block, and therefore `dominatingEdge(bb1, bb2) and bb2.dominates(bb3)`
-   * means that the edge `(bb1, bb2)` dominates `bb3`.
-   */
-  predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2);
-
   class AstNode {
     /** Gets a textual representation of this AST node. */
     string toString();
@@ -254,7 +203,15 @@ signature module InputSig<LocationSig Location> {
 }
 
 /** Provides guards-related predicates and classes. */
-module Make<LocationSig Location, InputSig<Location> Input> {
+module Make<
+  LocationSig Location, BB::CfgSig<Location> Cfg,
+  SuccessorTypesSig<Cfg::SuccessorType> SuccessorTypes,
+  InputSig<Location, Cfg::ControlFlowNode, Cfg::BasicBlock> Input>
+{
+  private module Cfg_ = Cfg;
+
+  private import Cfg_
+  private import SuccessorTypes
   private import Input
 
   private newtype TAbstractSingleValue =