Skip to content

Commit 8a0af35

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 06eacc8 commit 8a0af35

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
@@ -107,6 +107,24 @@ class ControlFlowNodeWithPointsTo extends ControlFlowNode {
107107
// for that variable.
108108
exists(SsaVariable v | v.getAUse() = this | varHasCompletePointsToSet(v))
109109
}
110+
111+
/** Whether it is unlikely that this ControlFlowNode can be reached */
112+
predicate unlikelyReachable() {
113+
not start_bb_likely_reachable(this.getBasicBlock())
114+
or
115+
exists(BasicBlock b |
116+
start_bb_likely_reachable(b) and
117+
not end_bb_likely_reachable(b) and
118+
// If there is an unlikely successor edge earlier in the BB
119+
// than this node, then this node must be unreachable.
120+
exists(ControlFlowNode p, int i, int j |
121+
p.(RaisingNode).unlikelySuccessor(_) and
122+
p = b.getNode(i) and
123+
this = b.getNode(j) and
124+
i < j
125+
)
126+
)
127+
}
110128
}
111129

112130
/**
@@ -135,6 +153,45 @@ private predicate varHasCompletePointsToSet(SsaVariable var) {
135153
)
136154
}
137155

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

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
@@ -32,9 +32,9 @@ class FunctionMetrics extends Function {
3232
*/
3333
int getCyclomaticComplexity() {
3434
exists(int e, int n |
35-
n = count(BasicBlock b | b = this.getABasicBlock() and b.likelyReachable()) and
35+
n = count(BasicBlockWithPointsTo b | b = this.getABasicBlock() and b.likelyReachable()) and
3636
e =
37-
count(BasicBlock b1, BasicBlock b2 |
37+
count(BasicBlockWithPointsTo b1, BasicBlockWithPointsTo b2 |
3838
b1 = this.getABasicBlock() and
3939
b1.likelyReachable() and
4040
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)