Python: Add some CFG-validation queries

These use the annotated, self-verifying test files to check various
consistency requirements.

Some of these may be expressing the same thing in different ways, but
it's fairly cheap to keep them around, so I have not attempted to
produce a minimal set of queries for this.

python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql

@@ -5,13 +5,13 @@
  * have separate CFGs and are excluded from this check.
  */
 
-import OldCfgImpl
-
-private module Utils = EvalOrderCfgUtils<OldCfg>;
-
-private import Utils
-private import Utils::CfgTests
+import python
+import TimerUtils
 
 from TimerCfgNode a, TestFunction f
-where allLiveReachable(a, f)
+where
+  not a.isDead() and
+  f = a.getTestFunction() and
+  a.getScope() = f and
+  not f.getEntryNode().getBasicBlock().reaches(a.getBasicBlock())
 select a, "Unreachable live annotation; entry of $@ does not reach this node", f, f.getName()

python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql

@@ -8,14 +8,19 @@
  * edge leaves the basic block and the normal successor may be dead.
  */
 
-import OldCfgImpl
+import python
+import TimerUtils
 
-private module Utils = EvalOrderCfgUtils<OldCfg>;
-
-private import Utils
-private import Utils::CfgTests
-
-from TimerCfgNode a, CfgNode succ
-where basicBlockAnnotationGap(a, succ)
+from TimerCfgNode a, ControlFlowNode succ
+where
+  exists(BasicBlock bb, int i |
+    a = bb.getNode(i) and
+    succ = bb.getNode(i + 1)
+  ) and
+  not succ instanceof TimerCfgNode and
+  not isUnannotatable(succ.getNode()) and
+  not isTimerMechanism(succ.getNode(), a.getTestFunction()) and
+  not exists(a.getAnExceptionalSuccessor()) and
+  succ.getNode() instanceof Expr
 select a, "Annotated node followed by unannotated $@ in the same basic block", succ,
   succ.getNode().toString()

python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql

@@ -4,6 +4,7 @@
  * in at least one annotation (live or dead).
  */
 
+import python
 import TimerUtils
 
 from TestFunction f, int missing, int maxTs, TimerAnnotation maxAnn

python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql

@@ -4,14 +4,16 @@
  * exist timestamps a in A and b in B with a < b.
  */
 
-import OldCfgImpl
-
-private module Utils = EvalOrderCfgUtils<OldCfg>;
-
-private import Utils
-private import Utils::CfgTests
+import python
+import TimerUtils
 
 from TimerCfgNode a, TimerCfgNode b, int minA, int maxB
-where noBackwardFlow(a, b, minA, maxB)
+where
+  nextTimerAnnotation(a, b) and
+  not a.isDead() and
+  not b.isDead() and
+  minA = min(a.getATimestamp()) and
+  maxB = max(b.getATimestamp()) and
+  minA >= maxB
 select a, "Backward flow: $@ flows to $@ (max timestamp $@)", a.getTimestampExpr(minA),
   minA.toString(), b, b.getNode().toString(), b.getTimestampExpr(maxB), maxB.toString()

python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql

@@ -3,14 +3,21 @@
  * mutually exclusive CFG paths (neither can reach the other).
  */
 
-import OldCfgImpl
-
-private module Utils = EvalOrderCfgUtils<OldCfg>;
-
-private import Utils
-private import Utils::CfgTests
+import python
+import TimerUtils
 
 from TimerCfgNode a, TimerCfgNode b, int ts
-where noSharedReachable(a, b, ts)
+where
+  a != b and
+  not a.isDead() and
+  not b.isDead() and
+  a.getTestFunction() = b.getTestFunction() and
+  ts = a.getATimestamp() and
+  ts = b.getATimestamp() and
+  (
+    a.getBasicBlock().strictlyReaches(b.getBasicBlock())
+    or
+    exists(BasicBlock bb, int i, int j | a = bb.getNode(i) and b = bb.getNode(j) and i < j)
+  )
 select a, "Shared timestamp $@ but this node reaches $@", a.getTimestampExpr(ts), ts.toString(), b,
   b.getNode().toString()

python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql

@@ -4,14 +4,22 @@
  * NOT dominate A (forward edge), requires max(A) < min(B).
  */
 
-import OldCfgImpl
-
-private module Utils = EvalOrderCfgUtils<OldCfg>;
-
-private import Utils
-private import Utils::CfgTests
+import python
+import TimerUtils
 
 from TimerCfgNode a, TimerCfgNode b, int maxA, int minB
-where strictForward(a, b, maxA, minB)
+where
+  nextTimerAnnotation(a, b) and
+  not a.isDead() and
+  not b.isDead() and
+  // Only apply to non-loop code (single timestamps on both sides)
+  strictcount(a.getATimestamp()) = 1 and
+  strictcount(b.getATimestamp()) = 1 and
+  // Forward edge: B does not strictly dominate A (excludes loop back-edges
+  // but still checks same-basic-block pairs)
+  not b.getBasicBlock().strictlyDominates(a.getBasicBlock()) and
+  maxA = max(a.getATimestamp()) and
+  minB = min(b.getATimestamp()) and
+  maxA >= minB
 select a, "Strict forward violation: $@ flows to $@", a.getTimestampExpr(maxA), "timestamp " + maxA,
   b.getTimestampExpr(minB), "timestamp " + minB