Python: Add ConsecutiveTimestamps test

This one is potentially a bit iffy -- it checks for a very powerful
propetry (that implies many of the other queries), but as the test
results show, it can produce false positives when there is in fact no
problem. We may want to get rid of it entirely, if it becomes too noisy.
This commit is contained in:
Taus
2026-04-16 16:14:56 +00:00
committed by yoff
parent f97bf38f3b
commit ba29e7e34d
2 changed files with 47 additions and 0 deletions

View File

@@ -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 |

View File

@@ -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()