From 9a4fb5c97177a20fcc329da825d42d9f4a9118fb Mon Sep 17 00:00:00 2001
From: Taus <tausbn@github.com>
Date: Thu, 16 Apr 2026 14:38:34 +0000
Subject: [PATCH] Python: Add self-validating CFG tests

These tests consist of various Python constructions (hopefully a
somewhat comprehensive set) with specific timestamp annotations
scattered throughout. When the tests are run using the Python 3
interpreter, these annotations are checked and compared to the "current
timestamp" to see that they are in agreement. This is what makes the
tests "self-validating".

There are a few different kinds of annotations: the basic `t[4]` style
(meaning this is executed at timestamp 4), the `t.dead[4]` variant
(meaning this _would_ happen at timestamp 4, but it is in a dead
branch), and `t.never` (meaning this is never executed at all).

In addition to this, there is a query, MissingAnnotations, which checks
whether we have applied these annotations maximally. Many expression
nodes are not actually annotatable, so there is a sizeable list of
excluded nodes for that query.
---
 .../evaluation-order/TimerUtils.qll           | 521 ++++--------------
 .../evaluation-order/test_assert_raise.py     |   4 +-
 .../evaluation-order/test_basic.py            |  14 +-
 .../evaluation-order/test_boolean.py          |  16 +-
 .../evaluation-order/test_conditional.py      |  14 +-
 .../ControlFlow/evaluation-order/test_if.py   |  28 +-
 .../evaluation-order/test_loops.py            |  10 +-
 .../evaluation-order/test_match.py            |  34 +-
 .../ControlFlow/evaluation-order/test_try.py  |  18 +-
 .../ControlFlow/evaluation-order/timer.py     | 101 ++--
 10 files changed, 217 insertions(+), 543 deletions(-)

diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll b/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
index 23f8f3a50a0..6ad4ef1ef19 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
@@ -1,10 +1,9 @@
 /**
  * Utility library for identifying timer annotations in evaluation-order tests.
  *
- * Identifies `expr @ t[n]` (matmul) and `t(expr, n)` (call) patterns,
- * including `dead(n)` and `never` markers within subscripts, extracts
- * timestamp values, and provides predicates for traversing consecutive
- * annotated CFG nodes.
+ * Identifies `expr @ t[n]` (matmul), `t(expr, n)` (call), and
+ * `expr @ t.dead[n]` (dead-code) patterns, extracts timestamp values,
+ * and provides predicates for traversing consecutive annotated CFG nodes.
  */
 
 import python
@@ -23,40 +22,16 @@ class TestFunction extends Function {
   string getTimerParamName() { result = this.getArgName(0) }
 }
 
-/**
- * Gets an element from a timestamp subscript index. Each element is either
- * an `IntegerLiteral` (live), a `Call` to `dead` (dead), a `Name("never")`
- * (never), or a tuple containing any mix of these.
- */
-private Expr timestampElement(Expr timestamps) {
-  result = timestamps and not timestamps instanceof Tuple
+/** Gets an IntegerLiteral from a timestamp expression (single int or tuple of ints). */
+private IntegerLiteral timestampLiteral(Expr timestamps) {
+  result = timestamps
   or
   result = timestamps.(Tuple).getAnElt()
 }
 
-/** Gets a live timestamp value from a subscript index expression. */
-private IntegerLiteral liveTimestampLiteral(Expr timestamps) {
-  result = timestampElement(timestamps) and
-  not result = any(Call c).getAnArg()
-}
-
-/** Gets a dead timestamp value from a subscript index expression. */
-private IntegerLiteral deadTimestampLiteral(Expr timestamps) {
-  exists(Call c |
-    c = timestampElement(timestamps) and
-    c.getFunc().(Name).getId() = "dead" and
-    result = c.getArg(0)
-  )
-}
-
-/** Holds if the subscript index contains `never`. */
-private predicate hasNever(Expr timestamps) {
-  timestampElement(timestamps).(Name).getId() = "never"
-}
-
 /** A timer annotation in the AST. */
 private newtype TTimerAnnotation =
-  /** `expr @ t[n]` or `expr @ t[n, m, ...]` or `expr @ t[dead(n), m, never]` */
+  /** `expr @ t[n]` or `expr @ t[n, m, ...]` */
   TMatmulAnnotation(TestFunction func, Expr annotated, Expr timestamps) {
     exists(BinaryExpr be |
       be.getOp() instanceof MatMult and
@@ -74,29 +49,40 @@ private newtype TTimerAnnotation =
       annotated = call.getArg(0) and
       timestamps = call.getArg(1)
     )
+  } or
+  /** `expr @ t.dead[n]` — dead-code annotation */
+  TDeadAnnotation(TestFunction func, Expr annotated, Expr timestamps) {
+    exists(BinaryExpr be |
+      be.getOp() instanceof MatMult and
+      be.getRight().(Subscript).getObject().(Attribute).getObject("dead").(Name).getId() =
+        func.getTimerParamName() and
+      be.getScope().getEnclosingScope*() = func and
+      annotated = be.getLeft() and
+      timestamps = be.getRight().(Subscript).getIndex()
+    )
+  } or
+  /** `expr @ t.never` — annotation for code that should never be evaluated */
+  TNeverAnnotation(TestFunction func, Expr annotated) {
+    exists(BinaryExpr be |
+      be.getOp() instanceof MatMult and
+      be.getRight().(Attribute).getObject("never").(Name).getId() = func.getTimerParamName() and
+      be.getScope().getEnclosingScope*() = func and
+      annotated = be.getLeft()
+    )
   }
 
 /** A timer annotation (wrapping the newtype for a clean API). */
 class TimerAnnotation extends TTimerAnnotation {
-  /** Gets a live timestamp value from this annotation. */
+  /** Gets a timestamp value from this annotation. */
   int getATimestamp() { exists(this.getTimestampExpr(result)) }
 
-  /** Gets the source expression for live timestamp value `ts`. */
+  /** Gets the source expression for timestamp value `ts`. */
   IntegerLiteral getTimestampExpr(int ts) {
-    result = liveTimestampLiteral(this.getTimestampsExpr()) and
+    result = timestampLiteral(this.getTimestampsExpr()) and
     result.getValue() = ts
   }
 
-  /** Gets a dead timestamp value from this annotation. */
-  int getADeadTimestamp() { exists(this.getDeadTimestampExpr(result)) }
-
-  /** Gets the source expression for dead timestamp value `ts`. */
-  IntegerLiteral getDeadTimestampExpr(int ts) {
-    result = deadTimestampLiteral(this.getTimestampsExpr()) and
-    result.getValue() = ts
-  }
-
-  /** Gets the raw timestamp expression (single element or tuple). */
+  /** Gets the raw timestamp expression (single int or tuple). */
   abstract Expr getTimestampsExpr();
 
   /** Gets the test function this annotation belongs to. */
@@ -106,27 +92,20 @@ class TimerAnnotation extends TTimerAnnotation {
   abstract Expr getAnnotatedExpr();
 
   /** Gets the enclosing annotation expression (the `BinaryExpr` or `Call`). */
-  abstract Expr getTimerExpr();
+  abstract Expr getExpr();
 
-  /** Holds if timestamp `ts` is marked as dead in this annotation. */
-  predicate isDeadTimestamp(int ts) { ts = this.getADeadTimestamp() }
+  /** Holds if this is a dead-code annotation (`t.dead[n]`). */
+  predicate isDead() { this instanceof DeadTimerAnnotation }
 
-  /** Holds if all timestamps in this annotation are dead (no live timestamps). */
-  predicate isDead() {
-    not exists(this.getATimestamp()) and
-    not this.isNever() and
-    exists(this.getADeadTimestamp())
-  }
+  /** Holds if this is a never-evaluated annotation (`t.never`). */
+  predicate isNever() { this instanceof NeverTimerAnnotation }
 
-  /** Holds if this is a never-evaluated annotation (contains `never`). */
-  predicate isNever() { hasNever(this.getTimestampsExpr()) }
+  string toString() { result = this.getExpr().toString() }
 
-  string toString() { result = this.getAnnotatedExpr().toString() }
-
-  Location getLocation() { result = this.getAnnotatedExpr().getLocation() }
+  Location getLocation() { result = this.getExpr().getLocation() }
 }
 
-/** A matmul-based timer annotation: `expr @ t[...]`. */
+/** A matmul-based timer annotation: `expr @ t[n]`. */
 class MatmulTimerAnnotation extends TMatmulAnnotation, TimerAnnotation {
   TestFunction func;
   Expr annotated;
@@ -140,7 +119,7 @@ class MatmulTimerAnnotation extends TMatmulAnnotation, TimerAnnotation {
 
   override Expr getAnnotatedExpr() { result = annotated }
 
-  override BinaryExpr getTimerExpr() { result.getLeft() = annotated }
+  override BinaryExpr getExpr() { result.getLeft() = annotated }
 }
 
 /** A call-based timer annotation: `t(expr, n)`. */
@@ -157,377 +136,81 @@ class CallTimerAnnotation extends TCallAnnotation, TimerAnnotation {
 
   override Expr getAnnotatedExpr() { result = annotated }
 
-  override Call getTimerExpr() { result.getArg(0) = annotated }
+  override Call getExpr() { result.getArg(0) = annotated }
+}
+
+/** A dead-code timer annotation: `expr @ t.dead[n]`. */
+class DeadTimerAnnotation extends TDeadAnnotation, TimerAnnotation {
+  TestFunction func;
+  Expr annotated;
+  Expr timestamps;
+
+  DeadTimerAnnotation() { this = TDeadAnnotation(func, annotated, timestamps) }
+
+  override Expr getTimestampsExpr() { result = timestamps }
+
+  override TestFunction getTestFunction() { result = func }
+
+  override Expr getAnnotatedExpr() { result = annotated }
+
+  override BinaryExpr getExpr() { result.getLeft() = annotated }
+}
+
+/** A never-evaluated annotation: `expr @ t.never`. */
+class NeverTimerAnnotation extends TNeverAnnotation, TimerAnnotation {
+  TestFunction func;
+  Expr annotated;
+
+  NeverTimerAnnotation() { this = TNeverAnnotation(func, annotated) }
+
+  override Expr getTimestampsExpr() { none() }
+
+  override TestFunction getTestFunction() { result = func }
+
+  override Expr getAnnotatedExpr() { result = annotated }
+
+  override BinaryExpr getExpr() { result.getLeft() = annotated }
 }
 
 /**
- * Signature module defining the CFG interface needed by evaluation-order tests.
- * This allows the test utilities to be instantiated with different CFG implementations.
+ * A CFG node corresponding to a timer annotation.
  */
-signature module EvalOrderCfgSig {
-  /** A control flow node. */
-  class CfgNode {
-    /** Gets a textual representation of this node. */
-    string toString();
+class TimerCfgNode extends ControlFlowNode {
+  private TimerAnnotation annot;
 
-    /** Gets the location of this node. */
-    Location getLocation();
+  TimerCfgNode() { annot.getExpr() = this.getNode() }
 
-    /** Gets the AST node corresponding to this CFG node, if any. */
-    AstNode getNode();
+  /** Gets a timestamp value from this annotation. */
+  int getATimestamp() { result = annot.getATimestamp() }
 
-    /** Gets a successor of this CFG node (including exceptional). */
-    CfgNode getASuccessor();
+  /** Gets the source expression for timestamp value `ts`. */
+  IntegerLiteral getTimestampExpr(int ts) { result = annot.getTimestampExpr(ts) }
 
-    /** Gets a true-branch successor of this CFG node, if any. */
-    CfgNode getATrueSuccessor();
+  /** Gets the test function this annotation belongs to. */
+  TestFunction getTestFunction() { result = annot.getTestFunction() }
 
-    /** Gets a false-branch successor of this CFG node, if any. */
-    CfgNode getAFalseSuccessor();
+  /** Holds if this is a dead-code annotation. */
+  predicate isDead() { annot.isDead() }
 
-    /** Gets an exceptional successor of this CFG node. */
-    CfgNode getAnExceptionalSuccessor();
-
-    /** Gets the scope containing this CFG node. */
-    Scope getScope();
-
-    /** Gets the basic block containing this CFG node. */
-    BasicBlock getBasicBlock();
-  }
-
-  /** A basic block in the control flow graph. */
-  class BasicBlock {
-    /** Gets the CFG node at position `n` in this basic block. */
-    CfgNode getNode(int n);
-
-    /** Holds if this basic block reaches `bb` (reflexive). */
-    predicate reaches(BasicBlock bb);
-
-    /** Holds if this basic block strictly reaches `bb` (non-reflexive). */
-    predicate strictlyReaches(BasicBlock bb);
-
-    /** Holds if this basic block strictly dominates `bb`. */
-    predicate strictlyDominates(BasicBlock bb);
-  }
-
-  /** Gets the entry CFG node for scope `s`. */
-  CfgNode scopeGetEntryNode(Scope s);
+  /** Holds if this is a never-evaluated annotation. */
+  predicate isNever() { annot.isNever() }
 }
 
 /**
- * Parameterised module providing CFG-dependent utilities for evaluation-order tests.
- * Instantiate with a specific CFG implementation to get `TimerCfgNode` and related predicates.
+ * Holds if `next` is the next timer annotation reachable from `n` via
+ * CFG successors (both normal and exceptional), skipping non-annotated
+ * intermediaries within the same scope.
  */
-module EvalOrderCfgUtils<EvalOrderCfgSig Input> {
-  /** The CFG node type from the underlying implementation. */
-  final class CfgNode = Input::CfgNode;
-
-  /** The basic block type from the underlying implementation (named to avoid clash with `python::BasicBlock`). */
-  final class CfgBasicBlock = Input::BasicBlock;
-
-  /** Gets the entry CFG node for scope `s`. */
-  CfgNode scopeGetEntryNode(Scope s) { result = Input::scopeGetEntryNode(s) }
-
-  /**
-   * A CFG node corresponding to a timer annotation.
-   */
-  class TimerCfgNode extends CfgNode {
-    private TimerAnnotation annot;
-
-    TimerCfgNode() { annot.getAnnotatedExpr() = this.getNode() }
-
-    /** Gets a timestamp value from this annotation. */
-    int getATimestamp() { result = annot.getATimestamp() }
-
-    /** Gets the source expression for timestamp value `ts`. */
-    IntegerLiteral getTimestampExpr(int ts) { result = annot.getTimestampExpr(ts) }
-
-    /** Gets the test function this annotation belongs to. */
-    TestFunction getTestFunction() { result = annot.getTestFunction() }
-
-    /** Holds if timestamp `ts` is marked as dead. */
-    predicate isDeadTimestamp(int ts) { annot.isDeadTimestamp(ts) }
-
-    /** Holds if all timestamps in this annotation are dead. */
-    predicate isDead() { annot.isDead() }
-
-    /** Holds if this is a never-evaluated annotation. */
-    predicate isNever() { annot.isNever() }
-  }
-
-  /**
-   * Holds if `next` is the next timer annotation reachable from `n` via
-   * CFG successors (both normal and exceptional), skipping non-annotated
-   * intermediaries within the same scope.
-   */
-  predicate nextTimerAnnotation(CfgNode n, TimerCfgNode next) {
-    next = n.getASuccessor() and
-    next.getScope() = n.getScope()
-    or
-    exists(CfgNode mid |
-      mid = n.getASuccessor() and
-      not mid instanceof TimerCfgNode and
-      mid.getScope() = n.getScope() and
-      nextTimerAnnotation(mid, next)
-    )
-  }
-
-  /**
-   * Holds if `next` is the next timer annotation reachable from `n` via
-   * the true branch, skipping non-annotated intermediaries and after-value
-   * nodes for the same AST node.
-   */
-  predicate nextTimerAnnotationFromTrue(CfgNode n, TimerCfgNode next) {
-    exists(CfgNode trueSucc |
-      trueSucc = n.getATrueSuccessor() and
-      trueSucc.getScope() = n.getScope()
-    |
-      // If the true successor is a different annotated node, use it
-      next = trueSucc and next.getNode() != n.getNode()
-      or
-      // Otherwise skip through it (it's an after-value node for the same expr)
-      nextTimerAnnotation(trueSucc, next)
-    )
-  }
-
-  /**
-   * Holds if `next` is the next timer annotation reachable from `n` via
-   * the false branch, skipping non-annotated intermediaries and after-value
-   * nodes for the same AST node.
-   */
-  predicate nextTimerAnnotationFromFalse(CfgNode n, TimerCfgNode next) {
-    exists(CfgNode falseSucc |
-      falseSucc = n.getAFalseSuccessor() and
-      falseSucc.getScope() = n.getScope()
-    |
-      // If the false successor is a different annotated node, use it
-      next = falseSucc and next.getNode() != n.getNode()
-      or
-      // Otherwise skip through it (it's an after-value node for the same expr)
-      nextTimerAnnotation(falseSucc, next)
-    )
-  }
-
-  /** CFG-dependent test predicates, one per evaluation-order query. */
-  module CfgTests {
-    /**
-     * Holds if live annotation `a` in function `f` is unreachable from
-     * the function entry in the CFG.
-     */
-    predicate allLiveReachable(TimerCfgNode a, TestFunction f) {
-      not a.isDead() and
-      f = a.getTestFunction() and
-      a.getScope() = f and
-      not scopeGetEntryNode(f).getBasicBlock().reaches(a.getBasicBlock())
-    }
-
-    /**
-     * Holds if annotated node `a` is followed by unannotated `succ` in the
-     * same basic block.
-     */
-    predicate basicBlockAnnotationGap(TimerCfgNode a, CfgNode succ) {
-      exists(CfgBasicBlock 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
-    }
-
-    /**
-     * Holds if annotations `a` and `b` appear in the same basic block with
-     * `a` before `b`, but `a`'s minimum timestamp is not less than `b`'s.
-     */
-    predicate basicBlockOrdering(TimerCfgNode a, TimerCfgNode b, int minA, int minB) {
-      exists(CfgBasicBlock bb, int i, int j | a = bb.getNode(i) and b = bb.getNode(j) and i < j) and
-      minA = min(a.getATimestamp()) and
-      minB = min(b.getATimestamp()) and
-      minA >= minB
-    }
-
-    /**
-     * Holds if function `f` has an annotation in a nested scope
-     * (generator, async function, comprehension, lambda).
-     */
-    private predicate hasNestedScopeAnnotation(TestFunction f) {
-      exists(TimerAnnotation a |
-        a.getTestFunction() = f and
-        a.getAnnotatedExpr().getScope() != f
-      )
-    }
-
-    /**
-     * Holds if annotation `ann` with timestamp `a` has no consecutive
-     * successor (expected `a + 1`) in the CFG.
-     */
-    predicate consecutiveTimestamps(TimerAnnotation ann, int a) {
-      not hasNestedScopeAnnotation(ann.getTestFunction()) and
-      not ann.isDead() and
-      a = ann.getATimestamp() and
-      not exists(TimerCfgNode x, TimerCfgNode y |
-        ann.getAnnotatedExpr() = x.getNode() and
-        nextTimerAnnotation(x, y) and
-        (a + 1) = y.getATimestamp()
-      ) and
-      // Exclude the maximum timestamp in the function (it has no successor)
-      not a =
-        max(TimerAnnotation other |
-          other.getTestFunction() = ann.getTestFunction()
-        |
-          other.getATimestamp()
-        )
-    }
-
-    /**
-     * Holds if the expression annotated with `t.never` is reachable from
-     * its scope's entry.
-     */
-    predicate neverReachable(TimerAnnotation ann) {
-      ann.isNever() and
-      exists(CfgNode n, Scope s |
-        n.getNode() = ann.getAnnotatedExpr() and
-        s = n.getScope() and
-        (
-          // Reachable via inter-block path (includes same block)
-          scopeGetEntryNode(s).getBasicBlock().reaches(n.getBasicBlock())
-          or
-          // In same block as entry but at a later index
-          exists(CfgBasicBlock bb, int i, int j |
-            bb.getNode(i) = scopeGetEntryNode(s) and bb.getNode(j) = n and i < j
-          )
-        )
-      )
-    }
-
-    /**
-     * Holds if consecutive annotated nodes `a` -> `b` have backward time
-     * flow (`minA >= maxB`).
-     */
-    predicate noBackwardFlow(TimerCfgNode a, TimerCfgNode b, int minA, int maxB) {
-      nextTimerAnnotation(a, b) and
-      not a.isDead() and
-      not b.isDead() and
-      minA = min(a.getATimestamp()) and
-      maxB = max(b.getATimestamp()) and
-      minA >= maxB
-    }
-
-    /**
-     * Holds if annotations `a` and `b` share timestamp `ts` but `a`
-     * can reach `b` in the CFG.
-     */
-    predicate noSharedReachable(TimerCfgNode a, TimerCfgNode b, int ts) {
-      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(CfgBasicBlock bb, int i, int j | a = bb.getNode(i) and b = bb.getNode(j) and i < j)
-      )
-    }
-
-    /**
-     * Holds if consecutive single-timestamp annotations `a` -> `b` on a
-     * forward edge have `maxA >= minB`.
-     */
-    predicate strictForward(TimerCfgNode a, TimerCfgNode b, int maxA, int minB) {
-      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
-    }
-
-    /**
-     * Holds if CFG node `n` in test function `f` does not belong to any basic block.
-     */
-    predicate noBasicBlock(CfgNode n, TestFunction f) {
-      n.getScope() = f and
-      not exists(n.getBasicBlock())
-    }
-
-    /**
-     * Holds if non-dead annotation `ann` has no corresponding CFG node.
-     */
-    predicate annotationWithoutCfgNode(TimerAnnotation ann) {
-      not ann.isDead() and
-      not ann.isNever() and
-      not exists(CfgNode n | n.getNode() = ann.getAnnotatedExpr())
-    }
-
-    predicate annotationWithCfgNode(TimerAnnotation ann) {
-      exists(CfgNode n | n.getNode() = ann.getAnnotatedExpr())
-    }
-
-    /**
-     * Holds if annotation `ann` with timestamp `a` has no consecutive
-     * predecessor (expected `a - 1`) in the CFG.
-     */
-    predicate consecutivePredecessorTimestamps(TimerAnnotation ann, int a) {
-      not hasNestedScopeAnnotation(ann.getTestFunction()) and
-      not ann.isDead() and
-      a = ann.getATimestamp() and
-      not exists(TimerCfgNode x, TimerCfgNode y |
-        ann.getAnnotatedExpr() = y.getNode() and
-        nextTimerAnnotation(x, y) and
-        (a - 1) = x.getATimestamp()
-      ) and
-      // Exclude the minimum timestamp in the function (it has no predecessor)
-      not a =
-        min(TimerAnnotation other |
-          other.getTestFunction() = ann.getTestFunction() and
-          not other.isDead()
-        |
-          other.getATimestamp()
-        )
-    }
-
-    /**
-     * Holds if `node` has both a true and false successor, but the true
-     * successor's timestamp `ts` is not marked as dead on the false
-     * successor (or vice versa).
-     *
-     * This checks that boolean branches are properly annotated: when a
-     * condition splits into true/false paths, the next annotated node
-     * on each side should account for the other side's timestamps as dead.
-     */
-    predicate missingBranchTimestamp(TimerCfgNode node, int ts, string branch) {
-      not hasNestedScopeAnnotation(node.getTestFunction()) and
-      exists(TimerCfgNode trueNext, TimerCfgNode falseNext |
-        nextTimerAnnotationFromTrue(node, trueNext) and
-        nextTimerAnnotationFromFalse(node, falseNext) and
-        trueNext != falseNext
-      |
-        // True successor has live timestamp ts, but false successor
-        // doesn't have it as dead
-        ts = trueNext.getATimestamp() and
-        not falseNext.isDeadTimestamp(ts) and
-        not ts = falseNext.getATimestamp() and
-        branch = "false"
-        or
-        // False successor has live timestamp ts, but true successor
-        // doesn't have it as dead
-        ts = falseNext.getATimestamp() and
-        not trueNext.isDeadTimestamp(ts) and
-        not ts = trueNext.getATimestamp() and
-        branch = "true"
-      )
-    }
-  }
+predicate nextTimerAnnotation(ControlFlowNode n, TimerCfgNode next) {
+  next = n.getASuccessor() and
+  next.getScope() = n.getScope()
+  or
+  exists(ControlFlowNode mid |
+    mid = n.getASuccessor() and
+    not mid instanceof TimerCfgNode and
+    mid.getScope() = n.getScope() and
+    nextTimerAnnotation(mid, next)
+  )
 }
 
 /**
@@ -537,7 +220,7 @@ module EvalOrderCfgUtils<EvalOrderCfgSig Input> {
 predicate isTimerMechanism(Expr e, TestFunction f) {
   exists(TimerAnnotation a |
     a.getTestFunction() = f and
-    e = a.getTimerExpr().getASubExpression*()
+    e = a.getExpr().getASubExpression*()
   )
 }
 
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py
index 692a9c6e407..9958d922ec8 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py
@@ -1,6 +1,6 @@
 """Assert and raise statement evaluation order."""
 
-from timer import test, dead
+from timer import test
 
 
 @test
@@ -13,7 +13,7 @@ def test_assert_true(t):
 @test
 def test_assert_true_with_message(t):
     x = True @ t[0]
-    assert x @ t[1], "msg" @ t[dead(2)]
+    assert x @ t[1], "msg" @ t.dead[2]
     y = 1 @ t[2]
 
 
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py
index efea733b0d9..f2ece3a0820 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py
@@ -5,10 +5,10 @@ are evaluated in the expected order (typically left to right for
 operands of binary operators, elements of collection literals, etc.)
 
 Every evaluated expression has a timestamp annotation, except the
-timer mechanism itself (t[n], t[dead(n)], t[never]).
+timer mechanism itself (t[n], t.dead[n]).
 """
 
-from timer import test, never
+from timer import test
 
 
 @test
@@ -46,7 +46,7 @@ def test_nested_binary(t):
 @test
 def test_chained_add(t):
     """a + b + c is (a + b) + c: left to right."""
-    x = (1 @ t[0] + 2 @ t[1] + 3 @ t[2]) @ t[3]
+    x = ((1 @ t[0] + 2 @ t[1]) @ t[2] + 3 @ t[3]) @ t[4]
 
 
 @test
@@ -58,7 +58,7 @@ def test_mixed_precedence(t):
 @test
 def test_string_concat(t):
     """String concatenation operands: left to right."""
-    x = ("hello" @ t[0] + " " @ t[1] + "world" @ t[2]) @ t[3]
+    x = (("hello" @ t[0] + " " @ t[1]) @ t[2] + "world" @ t[3]) @ t[4]
 
 
 @test
@@ -142,8 +142,8 @@ def test_multiple_assignment(t):
 @test
 def test_callable_syntax(t):
     """t(value, n) is equivalent to value @ t[n]."""
-    x = t(t(1, 0) + t(2, 1), 2)
-    y = t(t(x, 3) * t(3, 4), 5)
+    x = (1 @ t[0] + 2 @ t[1]) @ t[2]
+    y = (x @ t[3] * 3 @ t[4]) @ t[5]
 
 
 @test
@@ -178,7 +178,7 @@ def test_unreachable_after_return(t):
     def f():
         x = 1 @ t[1]
         return x @ t[2]
-        y = 2 @ t[never]
+        y = 2 @ t.never
     result = (f @ t[0])() @ t[3]
 
 
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py
index a12975634f4..d8183cb6484 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py
@@ -1,30 +1,30 @@
 """Short-circuit boolean operators and evaluation order."""
 
-from timer import test, dead
+from timer import test
 
 
 @test
 def test_and_both_sides(t):
     # True and X — both operands evaluated, result is X
-    x = (True @ t[0] and 42 @ t[1, dead(2)]) @ t[dead(1), 2]
+    x = (True @ t[0] and 42 @ t[1]) @ t[2]
 
 
 @test
 def test_and_short_circuit(t):
     # False and ... — right side never evaluated
-    x = (False @ t[0] and True @ t[dead(1)]) @ t[1, dead(2)]
+    x = (False @ t[0] and True @ t.dead[1]) @ t[1]
 
 
 @test
 def test_or_short_circuit(t):
     # True or ... — right side never evaluated
-    x = (True @ t[0] or False @ t[dead(1)]) @ t[1, dead(2)]
+    x = (True @ t[0] or False @ t.dead[1]) @ t[1]
 
 
 @test
 def test_or_both_sides(t):
     # False or X — both operands evaluated, result is X
-    x = (False @ t[0] or 42 @ t[1]) @ t[dead(1), 2]
+    x = (False @ t[0] or 42 @ t[1]) @ t[2]
 
 
 @test
@@ -37,19 +37,19 @@ def test_not(t):
 @test
 def test_chained_and(t):
     # 1 and 2 and 3 — all truthy, all evaluated left-to-right
-    x = (1 @ t[0] and 2 @ t[1, dead(3)] and 3 @ t[2, dead(3)]) @ t[dead(1), dead(2), 3]
+    x = (1 @ t[0] and 2 @ t[1] and 3 @ t[2]) @ t[3]
 
 
 @test
 def test_chained_or(t):
     # 0 or "" or 42 — first two falsy, all evaluated until truthy found
-    x = (0 @ t[0] or "" @ t[1, dead(3)] or 42 @ t[2, dead(3)]) @ t[dead(1), dead(2), 3]
+    x = (0 @ t[0] or "" @ t[1] or 42 @ t[2]) @ t[3]
 
 
 @test
 def test_mixed_and_or(t):
     # True and False or 42 => (True and False) or 42 => False or 42 => 42
-    x = ((True @ t[0] and False @ t[1, dead(2)]) @ t[dead(1), 2, dead(4)] or 42 @ t[3, dead(4)]) @ t[dead(2), dead(3), 4]
+    x = ((True @ t[0] and False @ t[1]) @ t[2] or 42 @ t[3]) @ t[4]
 
 
 @test
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py
index 48d45a77958..2c543e913e4 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py
@@ -1,38 +1,38 @@
 """Ternary conditional expressions and evaluation order."""
 
-from timer import test, dead
+from timer import test
 
 
 @test
 def test_ternary_true(t):
     # Condition is True — consequent evaluated, alternative skipped
-    x = (1 @ t[1] if True @ t[0] else 2 @ t[dead(1)]) @ t[2]
+    x = (1 @ t[1] if True @ t[0] else 2 @ t.dead[1]) @ t[2]
 
 
 @test
 def test_ternary_false(t):
     # Condition is False — alternative evaluated, consequent skipped
-    x = (1 @ t[dead(1)] if False @ t[0] else 2 @ t[1]) @ t[2]
+    x = (1 @ t.dead[1] if False @ t[0] else 2 @ t[1]) @ t[2]
 
 
 @test
 def test_ternary_nested(t):
     # Nested: outer condition True, inner condition True
     # ((10 if C1 else 20) if C2 else 30) — C2 first, then C1, then 10
-    x = ((10 @ t[2] if True @ t[1] else 20 @ t[dead(2)]) @ t[3] if True @ t[0] else 30 @ t[dead(1)]) @ t[4]
+    x = ((10 @ t[2] if True @ t[1] else 20 @ t.dead[2]) @ t[3] if True @ t[0] else 30 @ t.dead[1]) @ t[4]
 
 
 @test
 def test_ternary_assignment(t):
     # Ternary result assigned, then used in later expression
-    value = (100 @ t[1] if True @ t[0] else 200 @ t[dead(1)]) @ t[2]
+    value = (100 @ t[1] if True @ t[0] else 200 @ t.dead[1]) @ t[2]
     result = (value @ t[3] + 1 @ t[4]) @ t[5]
 
 
 @test
 def test_ternary_complex_expressions(t):
     # Complex sub-expressions in condition and consequent
-    x = ((1 @ t[3] + 2 @ t[4]) @ t[5] if (3 @ t[0] > 2 @ t[1]) @ t[2] else (4 @ t[dead(3)] + 5 @ t[dead(4)]) @ t[dead(5)]) @ t[6]
+    x = ((1 @ t[3] + 2 @ t[4]) @ t[5] if (3 @ t[0] > 2 @ t[1]) @ t[2] else (4 @ t.dead[3] + 5 @ t.dead[4]) @ t.dead[5]) @ t[6]
 
 
 @test
@@ -41,4 +41,4 @@ def test_ternary_as_argument(t):
     def f(a):
         return a @ t[4]
 
-    result = (f @ t[0])((1 @ t[2] if True @ t[1] else 2 @ t[dead(2)]) @ t[3]) @ t[5]
+    result = (f @ t[0])((1 @ t[2] if True @ t[1] else 2 @ t.dead[2]) @ t[3]) @ t[5]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
index 8880aaaef34..3190e94c6eb 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
@@ -1,6 +1,6 @@
 """If/elif/else control flow evaluation order."""
 
-from timer import test, dead
+from timer import test
 
 
 @test
@@ -15,7 +15,7 @@ def test_if_true(t):
 def test_if_false(t):
     x = False @ t[0]
     if x @ t[1]:
-        y = 1 @ t[dead(2)]
+        y = 1 @ t.dead[2]
     z = 0 @ t[2]
 
 
@@ -25,7 +25,7 @@ def test_if_else_true(t):
     if x @ t[1]:
         y = 1 @ t[2]
     else:
-        y = 2 @ t[dead(2)]
+        y = 2 @ t.dead[2]
     z = 0 @ t[3]
 
 
@@ -33,7 +33,7 @@ def test_if_else_true(t):
 def test_if_else_false(t):
     x = False @ t[0]
     if x @ t[1]:
-        y = 1 @ t[dead(2)]
+        y = 1 @ t.dead[2]
     else:
         y = 2 @ t[2]
     z = 0 @ t[3]
@@ -44,10 +44,10 @@ def test_if_elif_else_first(t):
     x = 1 @ t[0]
     if (x @ t[1] == 1 @ t[2]) @ t[3]:
         y = "first" @ t[4]
-    elif (x @ t[dead(4)] == 2 @ t[dead(5)]) @ t[dead(6)]:
-        y = "second" @ t[dead(4)]
+    elif (x @ t.dead[4] == 2 @ t.dead[5]) @ t.dead[6]:
+        y = "second" @ t.dead[4]
     else:
-        y = "third" @ t[dead(4)]
+        y = "third" @ t.dead[4]
     z = 0 @ t[5]
 
 
@@ -55,11 +55,11 @@ def test_if_elif_else_first(t):
 def test_if_elif_else_second(t):
     x = 2 @ t[0]
     if (x @ t[1] == 1 @ t[2]) @ t[3]:
-        y = "first" @ t[dead(7)]
+        y = "first" @ t.dead[7]
     elif (x @ t[4] == 2 @ t[5]) @ t[6]:
         y = "second" @ t[7]
     else:
-        y = "third" @ t[dead(7)]
+        y = "third" @ t.dead[7]
     z = 0 @ t[8]
 
 
@@ -67,9 +67,9 @@ def test_if_elif_else_second(t):
 def test_if_elif_else_third(t):
     x = 3 @ t[0]
     if (x @ t[1] == 1 @ t[2]) @ t[3]:
-        y = "first" @ t[dead(7)]
+        y = "first" @ t.dead[7]
     elif (x @ t[4] == 2 @ t[5]) @ t[6]:
-        y = "second" @ t[dead(7)]
+        y = "second" @ t.dead[7]
     else:
         y = "third" @ t[7]
     z = 0 @ t[8]
@@ -83,9 +83,9 @@ def test_nested_if_else(t):
         if y @ t[3]:
             z = 1 @ t[4]
         else:
-            z = 2 @ t[dead(4)]
+            z = 2 @ t.dead[4]
     else:
-        z = 3 @ t[dead(4)]
+        z = 3 @ t.dead[4]
     w = 0 @ t[5]
 
 
@@ -94,7 +94,7 @@ def test_if_compound_condition(t):
     x = True @ t[0]
     y = False @ t[1]
     if (x @ t[2] and y @ t[3]) @ t[4]:
-        z = 1 @ t[dead(5)]
+        z = 1 @ t.dead[5]
     else:
         z = 2 @ t[5]
     w = 0 @ t[6]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py
index 17df7a4703a..e81c31acde5 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py
@@ -1,6 +1,6 @@
 """Loop control flow evaluation order tests."""
 
-from timer import test, dead
+from timer import test
 
 
 # 1. Simple while loop (fixed iterations)
@@ -55,7 +55,7 @@ def test_while_else_break(t):
             break
         i = (i @ t[7] + 1 @ t[8]) @ t[9]
     else:
-        never = True @ t[dead(16)]
+        never = True @ t.dead[16]
     after = True @ t[16]
 
 
@@ -113,7 +113,7 @@ def test_for_else_break(t):
             break
         x @ t[7]
     else:
-        never = True @ t[dead(11)]
+        never = True @ t.dead[11]
     after = True @ t[11]
 
 
@@ -122,8 +122,8 @@ def test_for_else_break(t):
 def test_nested_loops(t):
     for i in [1 @ t[0], 2 @ t[1]] @ t[2]:
         for j in [10 @ t[3, 12], 20 @ t[4, 13]] @ t[5, 14]:
-            (i @ t[6, 9, 15, 18, dead(21)] + j @ t[7, 10, 16, 19]) @ t[8, 11, 17, 20]
-    done = True @ t[dead(3), dead(6), dead(9), dead(12), dead(15), dead(18), 21]
+            (i @ t[6, 9, 15, 18] + j @ t[7, 10, 16, 19]) @ t[8, 11, 17, 20]
+    done = True @ t[21]
 
 
 # 13. While True with conditional break
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py
index ba15a2d7c85..1dac5b0985c 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py
@@ -7,7 +7,7 @@ if sys.version_info < (3, 10):
     print("0/0 tests passed")
     sys.exit(0)
 
-from timer import test, dead, never
+from timer import test
 
 
 @test
@@ -17,7 +17,7 @@ def test_match_literal(t):
         case 1:
             y = "one" @ t[2]
         case 2:
-            y = "two" @ t[dead(2)]
+            y = "two" @ t.dead[2]
     z = y @ t[3]
 
 
@@ -26,9 +26,9 @@ def test_match_literal_fallthrough(t):
     x = 3 @ t[0]
     match x @ t[1]:
         case 1:
-            y = "one" @ t[dead(2)]
+            y = "one" @ t.dead[2]
         case 2:
-            y = "two" @ t[dead(2)]
+            y = "two" @ t.dead[2]
         case 3:
             y = "three" @ t[2]
     z = y @ t[3]
@@ -39,7 +39,7 @@ def test_match_wildcard(t):
     x = 42 @ t[0]
     match x @ t[1]:
         case 1:
-            y = "one" @ t[dead(2)]
+            y = "one" @ t.dead[2]
         case _:
             y = "other" @ t[2]
     z = y @ t[3]
@@ -61,7 +61,7 @@ def test_match_or_pattern(t):
         case 1 | 2:
             y = "low" @ t[2]
         case _:
-            y = "other" @ t[dead(2)]
+            y = "other" @ t.dead[2]
     z = y @ t[3]
 
 
@@ -72,7 +72,7 @@ def test_match_guard(t):
         case n if (n @ t[2] > 3 @ t[3]) @ t[4]:
             y = n @ t[5]
         case _:
-            y = 0 @ t[dead(5)]
+            y = 0 @ t.dead[5]
     z = y @ t[6]
 
 
@@ -83,7 +83,7 @@ def test_match_class_pattern(t):
         case int():
             y = "integer" @ t[2]
         case str():
-            y = "string" @ t[dead(2)]
+            y = "string" @ t.dead[2]
     z = y @ t[3]
 
 
@@ -94,7 +94,7 @@ def test_match_sequence(t):
         case [a, b]:
             y = (a @ t[4] + b @ t[5]) @ t[6]
         case _:
-            y = 0 @ t[dead(6)]
+            y = 0 @ t.dead[6]
     z = y @ t[7]
 
 
@@ -105,7 +105,7 @@ def test_match_mapping(t):
         case {"key": value}:
             y = value @ t[4]
         case _:
-            y = 0 @ t[dead(4)]
+            y = 0 @ t.dead[4]
     z = y @ t[5]
 
 
@@ -116,7 +116,7 @@ def test_match_nested(t):
         case {"users": [{"name": name}]}:
             y = name @ t[7]
         case _:
-            y = "unknown" @ t[dead(7)]
+            y = "unknown" @ t.dead[7]
     z = y @ t[8]
 
 
@@ -129,7 +129,7 @@ def test_match_or_pattern_with_as(t):
             result = ((uses @ t[2]).partition @ t[3])("@" @ t[4]) @ t[5]
             x = (result @ t[6])[0 @ t[7]] @ t[8]
         case _:
-            raise ((ValueError @ t[dead(2)])(clause @ t[dead(3)]) @ t[dead(4)])
+            raise ((ValueError @ t.dead[2])(clause @ t.dead[3]) @ t.dead[4])
     y = x @ t[9]
 
 
@@ -140,7 +140,7 @@ def test_match_wildcard_raise(t):
     try:
         match clause @ t[1]:
             case (str() as uses) | {"uses": uses}:
-                result = uses @ t[dead(2)]
+                result = uses @ t.dead[2]
             case _:
                 raise ((ValueError @ t[2])(f"Invalid: {clause @ t[3]}" @ t[4]) @ t[5])
     except ValueError:
@@ -155,8 +155,8 @@ def test_match_exhaustive_return_first(t):
             case 1:
                 return "one" @ t[3]
             case _:
-                return "other" @ t[dead(3)]
-        y = 0 @ t[never]
+                return "other" @ t.dead[3]
+        y = 0 @ t.never
     result = (f @ t[0])(1 @ t[1]) @ t[4]
 
 
@@ -166,8 +166,8 @@ def test_match_exhaustive_return_wildcard(t):
     def f(x):
         match x @ t[2]:
             case 1:
-                return "one" @ t[dead(3)]
+                return "one" @ t.dead[3]
             case _:
                 return "other" @ t[3]
-        y = 0 @ t[never]
+        y = 0 @ t.never
     result = (f @ t[0])(99 @ t[1]) @ t[4]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py
index dd0b15457d6..d54730478b1 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py
@@ -1,6 +1,6 @@
 """Exception handling control flow: try/except/else/finally evaluation order."""
 
-from timer import test, dead, never
+from timer import test
 
 
 # 1. try/except — no exception raised (except block skipped)
@@ -10,7 +10,7 @@ def test_try_no_exception(t):
         x = 1 @ t[0]
         y = 2 @ t[1]
     except ValueError:
-        z = 3 @ t[dead(2)]
+        z = 3 @ t.dead[2]
     after = 0 @ t[2]
 
 
@@ -20,7 +20,7 @@ def test_try_with_exception(t):
     try:
         x = 1 @ t[0]
         raise ((ValueError @ t[1])() @ t[2])
-        y = 2 @ t[never]
+        y = 2 @ t.never
     except ValueError:
         z = 3 @ t[3]
     after = 0 @ t[4]
@@ -32,7 +32,7 @@ def test_try_except_else_no_exception(t):
     try:
         x = 1 @ t[0]
     except ValueError:
-        y = 2 @ t[dead(1)]
+        y = 2 @ t.dead[1]
     else:
         z = 3 @ t[1]
     after = 0 @ t[2]
@@ -47,7 +47,7 @@ def test_try_except_else_with_exception(t):
     except ValueError:
         y = 2 @ t[3]
     else:
-        z = 3 @ t[dead(3)]
+        z = 3 @ t.dead[3]
     after = 0 @ t[4]
 
 
@@ -81,7 +81,7 @@ def test_try_except_finally_no_exception(t):
     try:
         x = 1 @ t[0]
     except ValueError:
-        y = 2 @ t[dead(1)]
+        y = 2 @ t.dead[1]
     finally:
         z = 3 @ t[1]
     after = 0 @ t[2]
@@ -109,7 +109,7 @@ def test_multiple_except_first(t):
     except ValueError:
         y = 2 @ t[3]
     except TypeError:
-        z = 3 @ t[dead(3)]
+        z = 3 @ t.dead[3]
     after = 0 @ t[4]
 
 
@@ -120,7 +120,7 @@ def test_multiple_except_second(t):
         x = 1 @ t[0]
         raise ((TypeError @ t[1])() @ t[2])
     except ValueError:
-        y = 2 @ t[dead(3)]
+        y = 2 @ t.dead[3]
     except TypeError:
         z = 3 @ t[3]
     after = 0 @ t[4]
@@ -149,7 +149,7 @@ def test_nested_try_except(t):
             z = 3 @ t[4]
         w = 4 @ t[5]
     except TypeError:
-        v = 5 @ t[dead(6)]
+        v = 5 @ t.dead[6]
     after = 0 @ t[6]
 
 
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py
index ccec5d64f7c..6cec3fd50cb 100644
--- a/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py
@@ -5,7 +5,7 @@ that verify the order in which Python evaluates expressions.
 
 Usage with @test decorator (preferred):
 
-    from timer import test, dead, never
+    from timer import test
 
     @test
     def test_sequential(t):
@@ -13,65 +13,42 @@ Usage with @test decorator (preferred):
         y = 2 @ t[1]
         z = (x + y) @ t[2]
 
-Annotation forms:
-    t[n]              - assert current timestamp is n, return marker
-    t[n, m, ...]      - assert current timestamp is one of {n, m, ...}
-    t[dead(n)]        - mark timestamp n as dead (fails if evaluated)
-    t[dead(n), m]     - dead at n, live at m
-    t[never]          - mark as never evaluated (fails if evaluated)
-    t["label"]        - record current timestamp under label (development aid)
-    t(value, n)       - equivalent to: value @ t[n]
+Usage with context manager (manual):
+
+    from timer import Timer
+
+    with Timer("my_test") as t:
+        x = 1 @ t[0]
+
+Timer API:
+    t[n]          - assert current timestamp is n, return marker
+    t[n, m, ...]  - assert current timestamp is one of {n, m, ...}
+    t["label"]    - record current timestamp under label (development aid)
+    t(value, n)   - equivalent to: value @ t[n]
 
 Run a test file directly to self-validate: python test_file.py
 """
 
 import atexit
-import os
 import sys
 
 _results = []
 
 
 class _Check:
-    """Marker returned by t[n] — asserts the current timestamp.
+    """Marker returned by t[n] — asserts the current timestamp."""
 
-    Receives the raw subscript elements: plain ints are live timestamps,
-    dead(n) markers are dead timestamps, and `never` means any evaluation
-    is an error.
-    """
+    __slots__ = ("_timer", "_expected")
 
-    __slots__ = ("_timer", "_live", "_dead", "_never")
-
-    def __init__(self, timer, elements):
+    def __init__(self, timer, expected):
         self._timer = timer
-        self._live = set()
-        self._dead = set()
-        self._never = False
-        for e in elements:
-            if isinstance(e, int):
-                self._live.add(e)
-            elif isinstance(e, _DeadMarker):
-                self._dead.add(e.timestamp)
-            elif isinstance(e, _NeverSentinel):
-                self._never = True
-            else:
-                raise TypeError(
-                    f"Unknown element in timer subscript: {e!r} (type {type(e).__name__})"
-                )
+        self._expected = expected
 
     def __rmatmul__(self, value):
         ts = self._timer._tick()
-        if self._never:
+        if ts not in self._expected:
             self._timer._error(
-                f"expression annotated with t[never] was evaluated (timestamp {ts})"
-            )
-        elif ts in self._dead:
-            self._timer._error(
-                f"timestamp {ts} is marked dead but was evaluated"
-            )
-        elif ts not in self._live:
-            self._timer._error(
-                f"expected {sorted(self._live)}, got {ts}"
+                f"expected {sorted(self._expected)}, got {ts}"
             )
         return value
 
@@ -91,24 +68,36 @@ class _Label:
         return value
 
 
-class _DeadMarker:
-    """Marker returned by dead(n) — used inside t[...] to mark a timestamp as dead."""
+class _NeverCheck:
+    """Marker returned by t.never — fails if the expression is ever evaluated."""
 
-    def __init__(self, timestamp):
-        self.timestamp = timestamp
+    def __init__(self, timer):
+        self._timer = timer
+
+    def __rmatmul__(self, value):
+        self._timer._error("expression annotated with t.never was evaluated")
+        return value
 
 
-def dead(n):
-    """Mark timestamp `n` as dead code inside a timer subscript: t[dead(1), 2]."""
-    return _DeadMarker(n)
+class _DeadCheck:
+    """Marker returned by t.dead[n] — fails if the expression is ever evaluated."""
+
+    def __init__(self, timer):
+        self._timer = timer
+
+    def __rmatmul__(self, value):
+        self._timer._error("expression annotated with t.dead was evaluated")
+        return value
 
 
-class _NeverSentinel:
-    """Sentinel for never-evaluated annotations: t[never]."""
-    pass
+class _DeadSubscript:
+    """Subscriptable returned by t.dead — produces _DeadCheck markers."""
 
+    def __init__(self, timer):
+        self._timer = timer
 
-never = _NeverSentinel()
+    def __getitem__(self, key):
+        return _DeadCheck(self._timer)
 
 
 class Timer:
@@ -124,6 +113,8 @@ class Timer:
         self._counter = 0
         self._errors = []
         self._labels = {}
+        self.dead = _DeadSubscript(self)
+        self.never = _NeverCheck(self)
 
     def __enter__(self):
         return self
@@ -153,7 +144,7 @@ class Timer:
         if isinstance(key, str):
             return _Label(self, key)
         elif isinstance(key, tuple):
-            return _Check(self, key)
+            return _Check(self, list(key))
         else:
             return _Check(self, [key])
 
@@ -188,7 +179,7 @@ def _report():
     print("---")
     print(f"{passed}/{total} tests passed")
     if passed < total:
-        os._exit(1)
+        sys.exit(1)
 
 
 atexit.register(_report)