C++: Add a back-edge safeguard

This prevents loops of non-back-edges on ChakraCore (see #811).

Author: jbj

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/IRBlock.qll

@@ -138,7 +138,7 @@ private predicate startsBasicBlock(Instruction instr) {
       not kind instanceof GotoEdge
     ) or  // Incoming edge is not a GotoEdge
     exists(Instruction predecessor |
-      instr = predecessor.getBackEdgeSuccessor(_)
+      instr = Construction::getInstructionBackEdgeSuccessor(predecessor, _)
     )  // A back edge enters this instruction
   )
 }
@@ -192,9 +192,36 @@ private cached module Cached {
   }
 
   cached predicate backEdgeSuccessor(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
+    backEdgeSuccessorRaw(pred, succ, kind)
+    or
+    forwardEdgeRaw+(pred, pred) and
+    blockSuccessor(pred, succ, kind)
+  }
+
+  /**
+   * Holds if there is an edge from `pred` to `succ` that is not a back edge.
+   */
+  private predicate forwardEdgeRaw(TIRBlock pred, TIRBlock succ) {
+    exists(EdgeKind kind |
+      blockSuccessor(pred, succ, kind) and
+      not backEdgeSuccessorRaw(pred, succ, kind)
+    )
+  }
+
+  /**
+   * Holds if the `kind`-edge from `pred` to `succ` is a back edge according to
+   * `Construction`.
+   *
+   * There could be loops of non-back-edges if there is a flaw in the IR
+   * construction or back-edge detection, and this could cause non-termination
+   * of subsequent analysis. To prevent that, a subsequent predicate further
+   * classifies all edges as back edges if they are involved in a loop of
+   * non-back-edges.
+   */
+  private predicate backEdgeSuccessorRaw(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
     exists(Instruction predLast, Instruction succFirst |
       predLast = getInstruction(pred, getInstructionCount(pred) - 1) and
-      succFirst = predLast.getBackEdgeSuccessor(kind) and
+      succFirst = Construction::getInstructionBackEdgeSuccessor(predLast, kind) and
       succ = MkIRBlock(succFirst)
     )
   }

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll

@@ -518,7 +518,15 @@ class Instruction extends Construction::TInstruction {
    * removed from the control-flow graph, it becomes acyclic.
    */
   final Instruction getBackEdgeSuccessor(EdgeKind kind) {
-    result = Construction::getInstructionBackEdgeSuccessor(this, kind)
+    // We don't take these edges from
+    // `Construction::getInstructionBackEdgeSuccessor` since that relation has
+    // not been treated to remove any loops that might be left over due to
+    // flaws in the IR construction or back-edge detection.
+    exists(IRBlock block |
+      block = this.getBlock() and
+      this = block.getLastInstruction() and
+      result = block.getBackEdgeSuccessor(kind).getFirstInstruction()
+    )
   }
 
   /**

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/IRBlock.qll

@@ -138,7 +138,7 @@ private predicate startsBasicBlock(Instruction instr) {
       not kind instanceof GotoEdge
     ) or  // Incoming edge is not a GotoEdge
     exists(Instruction predecessor |
-      instr = predecessor.getBackEdgeSuccessor(_)
+      instr = Construction::getInstructionBackEdgeSuccessor(predecessor, _)
     )  // A back edge enters this instruction
   )
 }
@@ -192,9 +192,36 @@ private cached module Cached {
   }
 
   cached predicate backEdgeSuccessor(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
+    backEdgeSuccessorRaw(pred, succ, kind)
+    or
+    forwardEdgeRaw+(pred, pred) and
+    blockSuccessor(pred, succ, kind)
+  }
+
+  /**
+   * Holds if there is an edge from `pred` to `succ` that is not a back edge.
+   */
+  private predicate forwardEdgeRaw(TIRBlock pred, TIRBlock succ) {
+    exists(EdgeKind kind |
+      blockSuccessor(pred, succ, kind) and
+      not backEdgeSuccessorRaw(pred, succ, kind)
+    )
+  }
+
+  /**
+   * Holds if the `kind`-edge from `pred` to `succ` is a back edge according to
+   * `Construction`.
+   *
+   * There could be loops of non-back-edges if there is a flaw in the IR
+   * construction or back-edge detection, and this could cause non-termination
+   * of subsequent analysis. To prevent that, a subsequent predicate further
+   * classifies all edges as back edges if they are involved in a loop of
+   * non-back-edges.
+   */
+  private predicate backEdgeSuccessorRaw(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
     exists(Instruction predLast, Instruction succFirst |
       predLast = getInstruction(pred, getInstructionCount(pred) - 1) and
-      succFirst = predLast.getBackEdgeSuccessor(kind) and
+      succFirst = Construction::getInstructionBackEdgeSuccessor(predLast, kind) and
       succ = MkIRBlock(succFirst)
     )
   }

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll

@@ -518,7 +518,15 @@ class Instruction extends Construction::TInstruction {
    * removed from the control-flow graph, it becomes acyclic.
    */
   final Instruction getBackEdgeSuccessor(EdgeKind kind) {
-    result = Construction::getInstructionBackEdgeSuccessor(this, kind)
+    // We don't take these edges from
+    // `Construction::getInstructionBackEdgeSuccessor` since that relation has
+    // not been treated to remove any loops that might be left over due to
+    // flaws in the IR construction or back-edge detection.
+    exists(IRBlock block |
+      block = this.getBlock() and
+      this = block.getLastInstruction() and
+      result = block.getBackEdgeSuccessor(kind).getFirstInstruction()
+    )
   }
 
   /**

cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/IRBlock.qll

@@ -138,7 +138,7 @@ private predicate startsBasicBlock(Instruction instr) {
       not kind instanceof GotoEdge
     ) or  // Incoming edge is not a GotoEdge
     exists(Instruction predecessor |
-      instr = predecessor.getBackEdgeSuccessor(_)
+      instr = Construction::getInstructionBackEdgeSuccessor(predecessor, _)
     )  // A back edge enters this instruction
   )
 }
@@ -192,9 +192,36 @@ private cached module Cached {
   }
 
   cached predicate backEdgeSuccessor(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
+    backEdgeSuccessorRaw(pred, succ, kind)
+    or
+    forwardEdgeRaw+(pred, pred) and
+    blockSuccessor(pred, succ, kind)
+  }
+
+  /**
+   * Holds if there is an edge from `pred` to `succ` that is not a back edge.
+   */
+  private predicate forwardEdgeRaw(TIRBlock pred, TIRBlock succ) {
+    exists(EdgeKind kind |
+      blockSuccessor(pred, succ, kind) and
+      not backEdgeSuccessorRaw(pred, succ, kind)
+    )
+  }
+
+  /**
+   * Holds if the `kind`-edge from `pred` to `succ` is a back edge according to
+   * `Construction`.
+   *
+   * There could be loops of non-back-edges if there is a flaw in the IR
+   * construction or back-edge detection, and this could cause non-termination
+   * of subsequent analysis. To prevent that, a subsequent predicate further
+   * classifies all edges as back edges if they are involved in a loop of
+   * non-back-edges.
+   */
+  private predicate backEdgeSuccessorRaw(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
     exists(Instruction predLast, Instruction succFirst |
       predLast = getInstruction(pred, getInstructionCount(pred) - 1) and
-      succFirst = predLast.getBackEdgeSuccessor(kind) and
+      succFirst = Construction::getInstructionBackEdgeSuccessor(predLast, kind) and
       succ = MkIRBlock(succFirst)
     )
   }

cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll

@@ -518,7 +518,15 @@ class Instruction extends Construction::TInstruction {
    * removed from the control-flow graph, it becomes acyclic.
    */
   final Instruction getBackEdgeSuccessor(EdgeKind kind) {
-    result = Construction::getInstructionBackEdgeSuccessor(this, kind)
+    // We don't take these edges from
+    // `Construction::getInstructionBackEdgeSuccessor` since that relation has
+    // not been treated to remove any loops that might be left over due to
+    // flaws in the IR construction or back-edge detection.
+    exists(IRBlock block |
+      block = this.getBlock() and
+      this = block.getLastInstruction() and
+      result = block.getBackEdgeSuccessor(kind).getFirstInstruction()
+    )
   }
 
   /**