Skip to content

Commit de7c9bd

Browse files
hvitvedhvitved
committed
Data flow: Add consistency checks to shared ql pack
1 parent 62c2316 commit de7c9bd

File tree

1 file changed

+290
-0
lines changed

1 file changed

+290
-0
lines changed

‎shared/dataflow/codeql/dataflow/internal/DataFlowImplConsistency.qll

Lines changed: 290 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,290 @@
1+
/**
2+
* Provides consistency queries for checking invariants in the language-specific
3+
* data-flow classes and predicates.
4+
*/
5+
6+
private import codeql.dataflow.DataFlow as DF
7+
private import codeql.dataflow.TaintTracking as TT
8+
9+
signature module InputSig<DF::InputSig DataFlowLang> {
10+
/** Holds if `n` should be excluded from the consistency test `uniqueEnclosingCallable`. */
11+
default predicate uniqueEnclosingCallableExclude(DataFlowLang::Node n) { none() }
12+
13+
/** Holds if `call` should be excluded from the consistency test `uniqueCallEnclosingCallable`. */
14+
default predicate uniqueCallEnclosingCallableExclude(DataFlowLang::DataFlowCall call) { none() }
15+
16+
/** Holds if `n` should be excluded from the consistency test `uniqueNodeLocation`. */
17+
default predicate uniqueNodeLocationExclude(DataFlowLang::Node n) { none() }
18+
19+
/** Holds if `n` should be excluded from the consistency test `missingLocation`. */
20+
default predicate missingLocationExclude(DataFlowLang::Node n) { none() }
21+
22+
/** Holds if `n` should be excluded from the consistency test `postWithInFlow`. */
23+
default predicate postWithInFlowExclude(DataFlowLang::Node n) { none() }
24+
25+
/** Holds if `n` should be excluded from the consistency test `argHasPostUpdate`. */
26+
default predicate argHasPostUpdateExclude(DataFlowLang::ArgumentNode n) { none() }
27+
28+
/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
29+
default predicate reverseReadExclude(DataFlowLang::Node n) { none() }
30+
31+
/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
32+
default predicate postHasUniquePreExclude(DataFlowLang::PostUpdateNode n) { none() }
33+
34+
/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
35+
default predicate uniquePostUpdateExclude(DataFlowLang::Node n) { none() }
36+
37+
/** Holds if `(call, ctx)` should be excluded from the consistency test `viableImplInCallContextTooLargeExclude`. */
38+
default predicate viableImplInCallContextTooLargeExclude(
39+
DataFlowLang::DataFlowCall call, DataFlowLang::DataFlowCall ctx,
40+
DataFlowLang::DataFlowCallable callable
41+
) {
42+
none()
43+
}
44+
45+
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodeAtPosition`. */
46+
default predicate uniqueParameterNodeAtPositionExclude(
47+
DataFlowLang::DataFlowCallable c, DataFlowLang::ParameterPosition pos, DataFlowLang::Node p
48+
) {
49+
none()
50+
}
51+
52+
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodePosition`. */
53+
default predicate uniqueParameterNodePositionExclude(
54+
DataFlowLang::DataFlowCallable c, DataFlowLang::ParameterPosition pos, DataFlowLang::Node p
55+
) {
56+
none()
57+
}
58+
59+
/** Holds if `n` should be excluded from the consistency test `identityLocalStep`. */
60+
default predicate identityLocalStepExclude(DataFlowLang::Node n) { none() }
61+
}
62+
63+
module MakeConsistency<
64+
DF::InputSig DataFlowLang, TT::InputSig<DataFlowLang> TaintTrackingLang,
65+
InputSig<DataFlowLang> Input>
66+
{
67+
private import DataFlowLang
68+
private import TaintTrackingLang
69+
70+
final private class NodeFinal = Node;
71+
72+
private class RelevantNode extends NodeFinal {
73+
RelevantNode() {
74+
this instanceof ArgumentNode or
75+
this instanceof ParameterNode or
76+
this instanceof ReturnNode or
77+
this = getAnOutNode(_, _) or
78+
simpleLocalFlowStep(this, _) or
79+
simpleLocalFlowStep(_, this) or
80+
jumpStep(this, _) or
81+
jumpStep(_, this) or
82+
storeStep(this, _, _) or
83+
storeStep(_, _, this) or
84+
readStep(this, _, _) or
85+
readStep(_, _, this) or
86+
defaultAdditionalTaintStep(this, _) or
87+
defaultAdditionalTaintStep(_, this)
88+
}
89+
}
90+
91+
query predicate uniqueEnclosingCallable(Node n, string msg) {
92+
exists(int c |
93+
n instanceof RelevantNode and
94+
c = count(nodeGetEnclosingCallable(n)) and
95+
c != 1 and
96+
not Input::uniqueEnclosingCallableExclude(n) and
97+
msg = "Node should have one enclosing callable but has " + c + "."
98+
)
99+
}
100+
101+
query predicate uniqueCallEnclosingCallable(DataFlowCall call, string msg) {
102+
exists(int c |
103+
c = count(call.getEnclosingCallable()) and
104+
c != 1 and
105+
not Input::uniqueCallEnclosingCallableExclude(call) and
106+
msg = "Call should have one enclosing callable but has " + c + "."
107+
)
108+
}
109+
110+
query predicate uniqueType(Node n, string msg) {
111+
exists(int c |
112+
n instanceof RelevantNode and
113+
c = count(getNodeType(n)) and
114+
c != 1 and
115+
msg = "Node should have one type but has " + c + "."
116+
)
117+
}
118+
119+
query predicate uniqueNodeLocation(Node n, string msg) {
120+
exists(int c |
121+
c =
122+
count(string filepath, int startline, int startcolumn, int endline, int endcolumn |
123+
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
124+
) and
125+
c != 1 and
126+
not Input::uniqueNodeLocationExclude(n) and
127+
msg = "Node should have one location but has " + c + "."
128+
)
129+
}
130+
131+
query predicate missingLocation(string msg) {
132+
exists(int c |
133+
c =
134+
strictcount(Node n |
135+
not n.hasLocationInfo(_, _, _, _, _) and
136+
not Input::missingLocationExclude(n)
137+
) and
138+
msg = "Nodes without location: " + c
139+
)
140+
}
141+
142+
query predicate uniqueNodeToString(Node n, string msg) {
143+
exists(int c |
144+
c = count(n.toString()) and
145+
c != 1 and
146+
msg = "Node should have one toString but has " + c + "."
147+
)
148+
}
149+
150+
query predicate missingToString(string msg) {
151+
exists(int c |
152+
c = strictcount(Node n | not exists(n.toString())) and
153+
msg = "Nodes without toString: " + c
154+
)
155+
}
156+
157+
query predicate parameterCallable(ParameterNode p, string msg) {
158+
exists(DataFlowCallable c | isParameterNode(p, c, _) and c != nodeGetEnclosingCallable(p)) and
159+
msg = "Callable mismatch for parameter."
160+
}
161+
162+
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
163+
simpleLocalFlowStep(n1, n2) and
164+
nodeGetEnclosingCallable(n1) != nodeGetEnclosingCallable(n2) and
165+
msg = "Local flow step does not preserve enclosing callable."
166+
}
167+
168+
query predicate readStepIsLocal(Node n1, Node n2, string msg) {
169+
readStep(n1, _, n2) and
170+
nodeGetEnclosingCallable(n1) != nodeGetEnclosingCallable(n2) and
171+
msg = "Read step does not preserve enclosing callable."
172+
}
173+
174+
query predicate storeStepIsLocal(Node n1, Node n2, string msg) {
175+
storeStep(n1, _, n2) and
176+
nodeGetEnclosingCallable(n1) != nodeGetEnclosingCallable(n2) and
177+
msg = "Store step does not preserve enclosing callable."
178+
}
179+
180+
private DataFlowType typeRepr() { result = getNodeType(_) }
181+
182+
query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
183+
t = typeRepr() and
184+
not compatibleTypes(t, t) and
185+
msg = "Type compatibility predicate is not reflexive."
186+
}
187+
188+
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
189+
isUnreachableInCall(n, call) and
190+
exists(DataFlowCallable c |
191+
c = nodeGetEnclosingCallable(n) and
192+
not viableCallable(call) = c
193+
) and
194+
msg = "Call context for isUnreachableInCall is inconsistent with call graph."
195+
}
196+
197+
query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
198+
(
199+
n = getAnOutNode(call, _) and
200+
msg = "OutNode and call does not share enclosing callable."
201+
or
202+
isArgumentNode(n, call, _) and
203+
msg = "ArgumentNode and call does not share enclosing callable."
204+
) and
205+
nodeGetEnclosingCallable(n) != call.getEnclosingCallable()
206+
}
207+
208+
query predicate postIsNotPre(PostUpdateNode n, string msg) {
209+
n = n.getPreUpdateNode() and
210+
msg = "PostUpdateNode should not equal its pre-update node."
211+
}
212+
213+
query predicate postHasUniquePre(PostUpdateNode n, string msg) {
214+
not Input::postHasUniquePreExclude(n) and
215+
exists(int c |
216+
c = count(n.getPreUpdateNode()) and
217+
c != 1 and
218+
msg = "PostUpdateNode should have one pre-update node but has " + c + "."
219+
)
220+
}
221+
222+
query predicate uniquePostUpdate(Node n, string msg) {
223+
not Input::uniquePostUpdateExclude(n) and
224+
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
225+
msg = "Node has multiple PostUpdateNodes."
226+
}
227+
228+
query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
229+
nodeGetEnclosingCallable(n) != nodeGetEnclosingCallable(n.getPreUpdateNode()) and
230+
msg = "PostUpdateNode does not share callable with its pre-update node."
231+
}
232+
233+
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
234+
235+
query predicate reverseRead(Node n, string msg) {
236+
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
237+
not Input::reverseReadExclude(n) and
238+
msg = "Origin of readStep is missing a PostUpdateNode."
239+
}
240+
241+
query predicate argHasPostUpdate(ArgumentNode n, string msg) {
242+
not hasPost(n) and
243+
not Input::argHasPostUpdateExclude(n) and
244+
msg = "ArgumentNode is missing PostUpdateNode."
245+
}
246+
247+
query predicate postWithInFlow(PostUpdateNode n, string msg) {
248+
not clearsContent(n, _) and
249+
simpleLocalFlowStep(_, n) and
250+
not Input::postWithInFlowExclude(n) and
251+
msg = "PostUpdateNode should not be the target of local flow."
252+
}
253+
254+
query predicate viableImplInCallContextTooLarge(
255+
DataFlowCall call, DataFlowCall ctx, DataFlowCallable callable
256+
) {
257+
callable = viableImplInCallContext(call, ctx) and
258+
not callable = viableCallable(call) and
259+
not Input::viableImplInCallContextTooLargeExclude(call, ctx, callable)
260+
}
261+
262+
query predicate uniqueParameterNodeAtPosition(
263+
DataFlowCallable c, ParameterPosition pos, Node p, string msg
264+
) {
265+
not Input::uniqueParameterNodeAtPositionExclude(c, pos, p) and
266+
isParameterNode(p, c, pos) and
267+
not exists(unique(Node p0 | isParameterNode(p0, c, pos))) and
268+
msg = "Parameters with overlapping positions."
269+
}
270+
271+
query predicate uniqueParameterNodePosition(
272+
DataFlowCallable c, ParameterPosition pos, Node p, string msg
273+
) {
274+
not Input::uniqueParameterNodePositionExclude(c, pos, p) and
275+
isParameterNode(p, c, pos) and
276+
not exists(unique(ParameterPosition pos0 | isParameterNode(p, c, pos0))) and
277+
msg = "Parameter node with multiple positions."
278+
}
279+
280+
query predicate uniqueContentApprox(Content c, string msg) {
281+
not exists(unique(ContentApprox approx | approx = getContentApprox(c))) and
282+
msg = "Non-unique content approximation."
283+
}
284+
285+
query predicate identityLocalStep(Node n, string msg) {
286+
simpleLocalFlowStep(n, n) and
287+
not Input::identityLocalStepExclude(n) and
288+
msg = "Node steps to itself"
289+
}
290+
}

0 commit comments

Comments
 (0)