Skip to content

Commit 21e74a3

Browse files
committed
Python: Fully remove points-to from Flow.qll
Gets rid of a bunch of predicates relating to reachability (which depended on the modelling of exceptions, which uses points-to), moving them to `LegacyPointsTo`. In the process, we gained a new class `BasicBlockWithPointsTo`.
1 parent 7176898 commit 21e74a3

File tree

4 files changed

+62
-57
lines changed

4 files changed

+62
-57
lines changed

python/ql/lib/LegacyPointsTo.qll

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,24 @@ class ControlFlowNodeWithPointsTo extends ControlFlowNode {
106106
// for that variable.
107107
exists(SsaVariable v | v.getAUse() = this | varHasCompletePointsToSet(v))
108108
}
109+
110+
/** Whether it is unlikely that this ControlFlowNode can be reached */
111+
predicate unlikelyReachable() {
112+
not start_bb_likely_reachable(this.getBasicBlock())
113+
or
114+
exists(BasicBlock b |
115+
start_bb_likely_reachable(b) and
116+
not end_bb_likely_reachable(b) and
117+
// If there is an unlikely successor edge earlier in the BB
118+
// than this node, then this node must be unreachable.
119+
exists(ControlFlowNode p, int i, int j |
120+
p.(RaisingNode).unlikelySuccessor(_) and
121+
p = b.getNode(i) and
122+
this = b.getNode(j) and
123+
i < j
124+
)
125+
)
126+
}
109127
}
110128

111129
/**
@@ -134,6 +152,45 @@ private predicate varHasCompletePointsToSet(SsaVariable var) {
134152
)
135153
}
136154

155+
private predicate start_bb_likely_reachable(BasicBlock b) {
156+
exists(Scope s | s.getEntryNode() = b.getNode(_))
157+
or
158+
exists(BasicBlock pred |
159+
pred = b.getAPredecessor() and
160+
end_bb_likely_reachable(pred) and
161+
not pred.getLastNode().(RaisingNode).unlikelySuccessor(b)
162+
)
163+
}
164+
165+
private predicate end_bb_likely_reachable(BasicBlock b) {
166+
start_bb_likely_reachable(b) and
167+
not exists(ControlFlowNode p, ControlFlowNode s |
168+
p.(RaisingNode).unlikelySuccessor(s) and
169+
p = b.getNode(_) and
170+
s = b.getNode(_) and
171+
not p = b.getLastNode()
172+
)
173+
}
174+
175+
/**
176+
* An extension of `BasicBlock` that provides points-to related methods.
177+
*/
178+
class BasicBlockWithPointsTo extends BasicBlock {
179+
/**
180+
* Whether (as inferred by type inference) it is highly unlikely (or impossible) for control to flow from this to succ.
181+
*/
182+
predicate unlikelySuccessor(BasicBlockWithPointsTo succ) {
183+
this.getLastNode().(RaisingNode).unlikelySuccessor(succ.firstNode())
184+
or
185+
not end_bb_likely_reachable(this) and succ = this.getASuccessor()
186+
}
187+
188+
/**
189+
* Whether (as inferred by type inference) this basic block is likely to be reachable.
190+
*/
191+
predicate likelyReachable() { start_bb_likely_reachable(this) }
192+
}
193+
137194
/**
138195
* An extension of `Expr` that provides points-to predicates.
139196
*/

python/ql/lib/semmle/python/Flow.qll

Lines changed: 2 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
import python
22
private import semmle.python.internal.CachedStages
33
private import codeql.controlflow.BasicBlock as BB
4-
private import LegacyPointsTo
54

65
/*
76
* Note about matching parent and child nodes and CFG splitting:
@@ -191,24 +190,6 @@ class ControlFlowNode extends @py_flow_node {
191190
/** Whether this node is a normal (non-exceptional) exit */
192191
predicate isNormalExit() { py_scope_flow(this, _, 0) or py_scope_flow(this, _, 2) }
193192

194-
/** Whether it is unlikely that this ControlFlowNode can be reached */
195-
predicate unlikelyReachable() {
196-
not start_bb_likely_reachable(this.getBasicBlock())
197-
or
198-
exists(BasicBlock b |
199-
start_bb_likely_reachable(b) and
200-
not end_bb_likely_reachable(b) and
201-
// If there is an unlikely successor edge earlier in the BB
202-
// than this node, then this node must be unreachable.
203-
exists(ControlFlowNode p, int i, int j |
204-
p.(RaisingNode).unlikelySuccessor(_) and
205-
p = b.getNode(i) and
206-
this = b.getNode(j) and
207-
i < j
208-
)
209-
)
210-
}
211-
212193
/** Whether this strictly dominates other. */
213194
pragma[inline]
214195
predicate strictlyDominates(ControlFlowNode other) {
@@ -1005,7 +986,8 @@ class BasicBlock extends @py_flow_node {
1005986
)
1006987
}
1007988

1008-
private ControlFlowNode firstNode() { result = this }
989+
/** Gets the first node in this basic block */
990+
ControlFlowNode firstNode() { result = this }
1009991

1010992
/** Gets the last node in this basic block */
1011993
ControlFlowNode getLastNode() {
@@ -1094,15 +1076,6 @@ class BasicBlock extends @py_flow_node {
10941076
)
10951077
}
10961078

1097-
/**
1098-
* Whether (as inferred by type inference) it is highly unlikely (or impossible) for control to flow from this to succ.
1099-
*/
1100-
predicate unlikelySuccessor(BasicBlock succ) {
1101-
this.getLastNode().(RaisingNode).unlikelySuccessor(succ.firstNode())
1102-
or
1103-
not end_bb_likely_reachable(this) and succ = this.getASuccessor()
1104-
}
1105-
11061079
/** Holds if this basic block strictly reaches the other. Is the start of other reachable from the end of this. */
11071080
cached
11081081
predicate strictlyReaches(BasicBlock other) {
@@ -1113,11 +1086,6 @@ class BasicBlock extends @py_flow_node {
11131086
/** Holds if this basic block reaches the other. Is the start of other reachable from the end of this. */
11141087
predicate reaches(BasicBlock other) { this = other or this.strictlyReaches(other) }
11151088

1116-
/**
1117-
* Whether (as inferred by type inference) this basic block is likely to be reachable.
1118-
*/
1119-
predicate likelyReachable() { start_bb_likely_reachable(this) }
1120-
11211089
/**
11221090
* Gets the `ConditionBlock`, if any, that controls this block and
11231091
* does not control any other `ConditionBlock`s that control this block.
@@ -1145,26 +1113,6 @@ class BasicBlock extends @py_flow_node {
11451113
}
11461114
}
11471115

1148-
private predicate start_bb_likely_reachable(BasicBlock b) {
1149-
exists(Scope s | s.getEntryNode() = b.getNode(_))
1150-
or
1151-
exists(BasicBlock pred |
1152-
pred = b.getAPredecessor() and
1153-
end_bb_likely_reachable(pred) and
1154-
not pred.getLastNode().(RaisingNode).unlikelySuccessor(b)
1155-
)
1156-
}
1157-
1158-
private predicate end_bb_likely_reachable(BasicBlock b) {
1159-
start_bb_likely_reachable(b) and
1160-
not exists(ControlFlowNode p, ControlFlowNode s |
1161-
p.(RaisingNode).unlikelySuccessor(s) and
1162-
p = b.getNode(_) and
1163-
s = b.getNode(_) and
1164-
not p = b.getLastNode()
1165-
)
1166-
}
1167-
11681116
private class ControlFlowNodeAlias = ControlFlowNode;
11691117

11701118
final private class FinalBasicBlock = BasicBlock;

python/ql/lib/semmle/python/Metrics.qll

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,9 +29,9 @@ class FunctionMetrics extends Function {
2929
*/
3030
int getCyclomaticComplexity() {
3131
exists(int e, int n |
32-
n = count(BasicBlock b | b = this.getABasicBlock() and b.likelyReachable()) and
32+
n = count(BasicBlockWithPointsTo b | b = this.getABasicBlock() and b.likelyReachable()) and
3333
e =
34-
count(BasicBlock b1, BasicBlock b2 |
34+
count(BasicBlockWithPointsTo b1, BasicBlockWithPointsTo b2 |
3535
b1 = this.getABasicBlock() and
3636
b1.likelyReachable() and
3737
b2 = this.getABasicBlock() and

python/ql/lib/semmle/python/SSA.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ class SsaVariable extends @py_ssa_var {
9292
}
9393

9494
/** Gets the incoming edges for a Phi node, pruned of unlikely edges. */
95-
private BasicBlock getAPrunedPredecessorBlockForPhi() {
95+
private BasicBlockWithPointsTo getAPrunedPredecessorBlockForPhi() {
9696
result = this.getAPredecessorBlockForPhi() and
9797
not result.unlikelySuccessor(this.getDefinition().getBasicBlock())
9898
}

0 commit comments

Comments
 (0)