hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-05-14 19:29:28 +02:00
Code Issues Packages Projects Releases Wiki Activity

Python: Add some CFG-validation queries

Browse Source 
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.
This commit is contained in:
Taus
2026-04-28 15:06:50 +00:00
parent 795b138584
commit edfbaa5ceb
16 changed files with 162 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

0
python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.expected Normal file
View File

18
python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql Normal file
View File

@@ -0,0 +1,18 @@
/**
* 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 TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils
private import Utils::CfgTests
from TimerCfgNode a, TestFunction f
where allLiveReachable(a, f)
select a, "Unreachable live annotation; entry of $@ does not reach this node", f, f.getName()

1
python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.expected Normal file
View File

@@ -0,0 +1 @@

15
python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.ql Normal file
View File

@@ -0,0 +1,15 @@
/**
* Checks that every timer annotation has a corresponding CFG node.
*/
import TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils::CfgTests
from TimerAnnotation ann
where annotationWithoutCfgNode(ann)
select ann, "Annotation in $@ has no CFG node", ann.getTestFunction(),
ann.getTestFunction().getName()

0
python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.expected Normal file
View File

22
python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql Normal file
View File

@@ -0,0 +1,22 @@
/**
* 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 TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils
private import Utils::CfgTests
from TimerCfgNode a, CfgNode succ
where basicBlockAnnotationGap(a, succ)
select a, "Annotated node followed by unannotated $@ in the same basic block", succ,
succ.getNode().toString()

0
python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.expected Normal file
View File

17
python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql Normal file
View File

@@ -0,0 +1,17 @@
/**
* 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 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()

10
python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected Normal file
View File

@@ -0,0 +1,10 @@
| test_boolean.py:9:10:9:43 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:9:59:9:59 | IntegerLiteral | 2 | test_boolean.py:9:10:9:13 | ControlFlowNode for True | True | test_boolean.py:9:19:9:19 | IntegerLiteral | 0 |
| test_boolean.py:15:10:15:43 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:15:50:15:50 | IntegerLiteral | 1 | test_boolean.py:15:10:15:14 | ControlFlowNode for False | False | test_boolean.py:15:20:15:20 | IntegerLiteral | 0 |
| test_boolean.py:21:10:21:42 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:21:49:21:49 | IntegerLiteral | 1 | test_boolean.py:21:10:21:13 | ControlFlowNode for True | True | test_boolean.py:21:19:21:19 | IntegerLiteral | 0 |
| test_boolean.py:27:10:27:43 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:27:59:27:59 | IntegerLiteral | 2 | test_boolean.py:27:10:27:14 | ControlFlowNode for False | False | test_boolean.py:27:20:27:20 | IntegerLiteral | 0 |
| test_boolean.py:40:10:40:61 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:40:86:40:86 | IntegerLiteral | 3 | test_boolean.py:40:10:40:10 | ControlFlowNode for IntegerLiteral | IntegerLiteral | test_boolean.py:40:16:40:16 | IntegerLiteral | 0 |
| test_boolean.py:46:10:46:61 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:46:86:46:86 | IntegerLiteral | 3 | test_boolean.py:46:10:46:10 | ControlFlowNode for IntegerLiteral | IntegerLiteral | test_boolean.py:46:16:46:16 | IntegerLiteral | 0 |
| test_boolean.py:52:10:52:95 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:52:120:52:120 | IntegerLiteral | 4 | test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | BoolExpr | test_boolean.py:52:63:52:63 | IntegerLiteral | 2 |
| test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:52:63:52:63 | IntegerLiteral | 2 | test_boolean.py:52:11:52:14 | ControlFlowNode for True | True | test_boolean.py:52:20:52:20 | IntegerLiteral | 0 |
| test_boolean.py:64:10:64:52 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:64:59:64:59 | IntegerLiteral | 6 | test_boolean.py:64:11:64:11 | ControlFlowNode for f | f | test_boolean.py:64:17:64:17 | IntegerLiteral | 0 |
| test_boolean.py:76:10:76:51 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:76:58:76:58 | IntegerLiteral | 6 | test_boolean.py:76:11:76:11 | ControlFlowNode for f | f | test_boolean.py:76:17:76:17 | IntegerLiteral | 0 |

18
python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql Normal file
View File

@@ -0,0 +1,18 @@
/**
* 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 TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils
private import Utils::CfgTests
from TimerCfgNode a, TimerCfgNode b, int minA, int maxB
where noBackwardFlow(a, b, minA, maxB)
select a, "Backward flow: $@ flows to $@ (max timestamp $@)", a.getTimestampExpr(minA),
minA.toString(), b, b.getNode().toString(), b.getTimestampExpr(maxB), maxB.toString()

1
python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.expected Normal file
View File

@@ -0,0 +1 @@

15
python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.ql Normal file
View File

@@ -0,0 +1,15 @@
/**
* Checks that every annotated CFG node belongs to a basic block.
*/
import TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils
private import Utils::CfgTests
from CfgNode n, TestFunction f
where noBasicBlock(n, f)
select n, "CFG node in $@ does not belong to any basic block", f, f.getName()

0
python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.expected Normal file
View File

17
python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql Normal file
View File

@@ -0,0 +1,17 @@
/**
* Checks that two annotations sharing a timestamp value are on
* mutually exclusive CFG paths (neither can reach the other).
*/
import TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils
private import Utils::CfgTests
from TimerCfgNode a, TimerCfgNode b, int ts
where noSharedReachable(a, b, ts)
select a, "Shared timestamp $@ but this node reaches $@", a.getTimestampExpr(ts), ts.toString(), b,
b.getNode().toString()

10
python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected Normal file
View File

@@ -0,0 +1,10 @@
| test_boolean.py:9:10:9:43 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:9:59:9:59 | IntegerLiteral | timestamp 2 | test_boolean.py:9:19:9:19 | IntegerLiteral | timestamp 0 |
| test_boolean.py:15:10:15:43 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:15:50:15:50 | IntegerLiteral | timestamp 1 | test_boolean.py:15:20:15:20 | IntegerLiteral | timestamp 0 |
| test_boolean.py:21:10:21:42 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:21:49:21:49 | IntegerLiteral | timestamp 1 | test_boolean.py:21:19:21:19 | IntegerLiteral | timestamp 0 |
| test_boolean.py:27:10:27:43 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:27:59:27:59 | IntegerLiteral | timestamp 2 | test_boolean.py:27:20:27:20 | IntegerLiteral | timestamp 0 |
| test_boolean.py:40:10:40:61 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:40:86:40:86 | IntegerLiteral | timestamp 3 | test_boolean.py:40:16:40:16 | IntegerLiteral | timestamp 0 |
| test_boolean.py:46:10:46:61 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:46:86:46:86 | IntegerLiteral | timestamp 3 | test_boolean.py:46:16:46:16 | IntegerLiteral | timestamp 0 |
| test_boolean.py:52:10:52:95 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:52:120:52:120 | IntegerLiteral | timestamp 4 | test_boolean.py:52:63:52:63 | IntegerLiteral | timestamp 2 |
| test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:52:63:52:63 | IntegerLiteral | timestamp 2 | test_boolean.py:52:20:52:20 | IntegerLiteral | timestamp 0 |
| test_boolean.py:64:10:64:52 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:64:59:64:59 | IntegerLiteral | timestamp 6 | test_boolean.py:64:17:64:17 | IntegerLiteral | timestamp 0 |
| test_boolean.py:76:10:76:51 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:76:58:76:58 | IntegerLiteral | timestamp 6 | test_boolean.py:76:17:76:17 | IntegerLiteral | timestamp 0 |

18
python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql Normal file
View File

@@ -0,0 +1,18 @@
/**
* 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 TimerUtils
import OldCfgImpl
private module Utils = EvalOrderCfgUtils<OldCfg>;
private import Utils
private import Utils::CfgTests
from TimerCfgNode a, TimerCfgNode b, int maxA, int minB
where strictForward(a, b, maxA, minB)
select a, "Strict forward violation: $@ flows to $@", a.getTimestampExpr(maxA), "timestamp " + maxA,
b.getTimestampExpr(minB), "timestamp " + minB