Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
/**
* Checks that every live (non-dead) annotation in the test function's
* own scope is reachable from the function entry in the CFG.
* Annotations in nested scopes (generators, async, lambdas, comprehensions)
* have separate CFGs and are excluded from this check.
*/

import python
import TimerUtils

from TimerCfgNode a, TestFunction 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()
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
/**
* Checks that within a basic block, if a node is annotated then its
* successor is also annotated (or excluded). A gap in annotations
* within a basic block indicates a missing annotation, since there
* are no branches to justify the gap.
*
* Nodes with exceptional successors are excluded, as the exception
* edge leaves the basic block and the normal successor may be dead.
*/

import python
import TimerUtils

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()
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
| test_comprehensions.py:21:29:21:40 | ControlFlowNode for BinaryExpr | Basic block ordering: $@ appears before $@ | test_comprehensions.py:21:35:21:35 | IntegerLiteral | timestamp 9 | test_comprehensions.py:21:21:21:21 | IntegerLiteral | timestamp 8 |
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
/**
* Checks that within a single basic block, annotations appear in
* increasing minimum-timestamp order.
*/

import python
import TimerUtils

from TimerCfgNode a, TimerCfgNode b, int minA, int minB
where
exists(BasicBlock 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
select a, "Basic block ordering: $@ appears before $@", a.getTimestampExpr(minA),
"timestamp " + minA, b.getTimestampExpr(minB), "timestamp " + minB
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
| test_if.py:51:9:51:16 | BinaryExpr | $@ in $@ has no consecutive successor (expected 6) | test_if.py:51:15:51:15 | IntegerLiteral | Timestamp 5 | test_if.py:43:1:43:31 | Function test_if_elif_else_first | test_if_elif_else_first |
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
/**
* Checks that consecutive annotated nodes have consecutive timestamps:
* for each annotation with timestamp `a`, some CFG node for that annotation
* must have a next annotation containing `a + 1`.
*
* Handles CFG splitting (e.g., finally blocks duplicated for normal/exceptional
* flow) by checking that at least one split has the required successor.
*
* Only applies to functions where all annotations are in the function's
* own scope (excludes tests with generators, async, comprehensions, or
* lambdas that have annotations in nested scopes).
*/

import python
import TimerUtils

/**
* 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.getExpr().getScope() != f
)
}

from TimerAnnotation ann, int a
where
not hasNestedScopeAnnotation(ann.getTestFunction()) and
not ann.isDead() and
a = ann.getATimestamp() and
not exists(TimerCfgNode x, TimerCfgNode y |
ann.getExpr() = 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()
)
select ann, "$@ in $@ has no consecutive successor (expected " + (a + 1) + ")",
ann.getTimestampExpr(a), "Timestamp " + a, ann.getTestFunction(), ann.getTestFunction().getName()
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
/**
* Checks that timestamps form a contiguous sequence {0, 1, ..., max}
* within each test function. Every integer in the range must appear
* in at least one annotation (live or dead).
*/

import python
import TimerUtils

from TestFunction f, int missing, int maxTs, TimerAnnotation maxAnn
where
maxTs = max(TimerAnnotation a | a.getTestFunction() = f | a.getATimestamp()) and
maxAnn.getTestFunction() = f and
maxAnn.getATimestamp() = maxTs and
missing = [0 .. maxTs] and
not exists(TimerAnnotation a | a.getTestFunction() = f and a.getATimestamp() = missing)
select f, "Missing timestamp " + missing + " (max is $@)", maxAnn.getTimestampExpr(maxTs),
maxTs.toString()
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
/**
* Finds expressions in test functions that lack a timer annotation
* and are not part of the timer mechanism or otherwise excluded.
* An empty result means every annotatable expression is covered.
*/

import python
import TimerUtils

from TestFunction f, Expr e
where
e.getScope().getEnclosingScope*() = f and
not isTimerMechanism(e, f) and
not isUnannotatable(e)
select e, "Missing annotation in $@", f, f.getName()
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
| test_match.py:159:13:159:23 | BinaryExpr | Node annotated with t.never is reachable in $@ | test_match.py:151:1:151:42 | Function test_match_exhaustive_return_first | test_match_exhaustive_return_first |
| test_match.py:172:13:172:23 | BinaryExpr | Node annotated with t.never is reachable in $@ | test_match.py:164:1:164:45 | Function test_match_exhaustive_return_wildcard | test_match_exhaustive_return_wildcard |
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
/**
* Checks that expressions annotated with `t.never` either have no CFG
* node, or if they do, that the node is not reachable from its scope's
* entry (including within the same basic block).
*/

import python
import TimerUtils

from NeverTimerAnnotation ann
where
exists(ControlFlowNode n, Scope s |
n.getNode() = ann.getExpr() and
s = n.getScope() and
(
// Reachable via inter-block path (includes same block)
s.getEntryNode().getBasicBlock().reaches(n.getBasicBlock())
or
// In same block as entry but at a later index
exists(BasicBlock bb, int i, int j |
bb.getNode(i) = s.getEntryNode() and bb.getNode(j) = n and i < j
)
)
)
select ann, "Node annotated with t.never is reachable in $@", ann.getTestFunction(),
ann.getTestFunction().getName()
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
/**
* Checks that time never flows backward between consecutive timer annotations
* in the CFG. For each pair of consecutive annotated nodes (A -> B), there must
* exist timestamps a in A and b in B with a < b.
*/

import python
import TimerUtils

from TimerCfgNode a, TimerCfgNode b, int minA, int 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()
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
/**
* Checks that two annotations sharing a timestamp value are on
* mutually exclusive CFG paths (neither can reach the other).
*/

import python
import TimerUtils

from TimerCfgNode a, TimerCfgNode b, int 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()
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
/**
* Stronger version of NoBackwardFlow: for consecutive annotated nodes
* A -> B that both have a single timestamp (non-loop code) and B does
* NOT dominate A (forward edge), requires max(A) < min(B).
*/

import python
import TimerUtils

from TimerCfgNode a, TimerCfgNode b, int maxA, int 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
Loading
Loading