Skip to content

Commit 9fa9c10

Browse files
hvitvedhvitved
authored
Merge pull request github#2921 from aschackmull/dataflow/consistency-checks
Java: Add data-flow consistency checks.
2 parents caf0d15 + 85d6b7c commit 9fa9c10

22 files changed

+3232
-1
lines changed

‎config/identical-files.json

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,12 @@
3939
"java/ql/src/semmle/code/java/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
4040
"java/ql/src/semmle/code/java/dataflow/internal/tainttracking2/TaintTrackingImpl.qll"
4141
],
42+
"DataFlow Java/C++/C# Consistency checks": [
43+
"java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll",
44+
"cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll",
45+
"cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll",
46+
"csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll"
47+
],
4248
"C++ SubBasicBlocks": [
4349
"cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
4450
"cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll"

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll

Lines changed: 175 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
1+
/**
2+
* Provides consistency queries for checking invariants in the language-specific
3+
* data-flow classes and predicates.
4+
*/
5+
6+
private import DataFlowImplSpecific::Private
7+
private import DataFlowImplSpecific::Public
8+
private import tainttracking1.TaintTrackingParameter::Private
9+
private import tainttracking1.TaintTrackingParameter::Public
10+
11+
module Consistency {
12+
private class RelevantNode extends Node {
13+
RelevantNode() {
14+
this instanceof ArgumentNode or
15+
this instanceof ParameterNode or
16+
this instanceof ReturnNode or
17+
this = getAnOutNode(_, _) or
18+
simpleLocalFlowStep(this, _) or
19+
simpleLocalFlowStep(_, this) or
20+
jumpStep(this, _) or
21+
jumpStep(_, this) or
22+
storeStep(this, _, _) or
23+
storeStep(_, _, this) or
24+
readStep(this, _, _) or
25+
readStep(_, _, this) or
26+
defaultAdditionalTaintStep(this, _) or
27+
defaultAdditionalTaintStep(_, this)
28+
}
29+
}
30+
31+
query predicate uniqueEnclosingCallable(Node n, string msg) {
32+
exists(int c |
33+
n instanceof RelevantNode and
34+
c = count(n.getEnclosingCallable()) and
35+
c != 1 and
36+
msg = "Node should have one enclosing callable but has " + c + "."
37+
)
38+
}
39+
40+
query predicate uniqueTypeBound(Node n, string msg) {
41+
exists(int c |
42+
n instanceof RelevantNode and
43+
c = count(n.getTypeBound()) and
44+
c != 1 and
45+
msg = "Node should have one type bound but has " + c + "."
46+
)
47+
}
48+
49+
query predicate uniqueTypeRepr(Node n, string msg) {
50+
exists(int c |
51+
n instanceof RelevantNode and
52+
c = count(getErasedRepr(n.getTypeBound())) and
53+
c != 1 and
54+
msg = "Node should have one type representation but has " + c + "."
55+
)
56+
}
57+
58+
query predicate uniqueNodeLocation(Node n, string msg) {
59+
exists(int c |
60+
c =
61+
count(string filepath, int startline, int startcolumn, int endline, int endcolumn |
62+
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
63+
) and
64+
c != 1 and
65+
msg = "Node should have one ___location but has " + c + "."
66+
)
67+
}
68+
69+
query predicate missingLocation(string msg) {
70+
exists(int c |
71+
c =
72+
strictcount(Node n |
73+
not exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
74+
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
75+
)
76+
) and
77+
msg = "Nodes without ___location: " + c
78+
)
79+
}
80+
81+
query predicate uniqueNodeToString(Node n, string msg) {
82+
exists(int c |
83+
c = count(n.toString()) and
84+
c != 1 and
85+
msg = "Node should have one toString but has " + c + "."
86+
)
87+
}
88+
89+
query predicate missingToString(string msg) {
90+
exists(int c |
91+
c = strictcount(Node n | not exists(n.toString())) and
92+
msg = "Nodes without toString: " + c
93+
)
94+
}
95+
96+
query predicate parameterCallable(ParameterNode p, string msg) {
97+
exists(DataFlowCallable c | p.isParameterOf(c, _) and c != p.getEnclosingCallable()) and
98+
msg = "Callable mismatch for parameter."
99+
}
100+
101+
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
102+
simpleLocalFlowStep(n1, n2) and
103+
n1.getEnclosingCallable() != n2.getEnclosingCallable() and
104+
msg = "Local flow step does not preserve enclosing callable."
105+
}
106+
107+
private DataFlowType typeRepr() { result = getErasedRepr(any(Node n).getTypeBound()) }
108+
109+
query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
110+
t = typeRepr() and
111+
not compatibleTypes(t, t) and
112+
msg = "Type compatibility predicate is not reflexive."
113+
}
114+
115+
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
116+
isUnreachableInCall(n, call) and
117+
exists(DataFlowCallable c |
118+
c = n.getEnclosingCallable() and
119+
not viableCallable(call) = c
120+
) and
121+
msg = "Call context for isUnreachableInCall is inconsistent with call graph."
122+
}
123+
124+
query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
125+
(
126+
n = getAnOutNode(call, _) and
127+
msg = "OutNode and call does not share enclosing callable."
128+
or
129+
n.(ArgumentNode).argumentOf(call, _) and
130+
msg = "ArgumentNode and call does not share enclosing callable."
131+
) and
132+
n.getEnclosingCallable() != call.getEnclosingCallable()
133+
}
134+
135+
query predicate postIsNotPre(PostUpdateNode n, string msg) {
136+
n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
137+
}
138+
139+
query predicate postHasUniquePre(PostUpdateNode n, string msg) {
140+
exists(int c |
141+
c = count(n.getPreUpdateNode()) and
142+
c != 1 and
143+
msg = "PostUpdateNode should have one pre-update node but has " + c + "."
144+
)
145+
}
146+
147+
query predicate uniquePostUpdate(Node n, string msg) {
148+
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
149+
msg = "Node has multiple PostUpdateNodes."
150+
}
151+
152+
query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
153+
n.getEnclosingCallable() != n.getPreUpdateNode().getEnclosingCallable() and
154+
msg = "PostUpdateNode does not share callable with its pre-update node."
155+
}
156+
157+
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
158+
159+
query predicate reverseRead(Node n, string msg) {
160+
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
161+
msg = "Origin of readStep is missing a PostUpdateNode."
162+
}
163+
164+
query predicate storeIsPostUpdate(Node n, string msg) {
165+
storeStep(_, _, n) and
166+
not n instanceof PostUpdateNode and
167+
msg = "Store targets should be PostUpdateNodes."
168+
}
169+
170+
query predicate argHasPostUpdate(ArgumentNode n, string msg) {
171+
not hasPost(n) and
172+
not isImmutableOrUnobservable(n) and
173+
msg = "ArgumentNode is missing PostUpdateNode."
174+
}
175+
}

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowPrivate.qll

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -293,3 +293,12 @@ class DataFlowCall extends Expr {
293293
predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub implementation
294294

295295
int accessPathLimit() { result = 5 }
296+
297+
/**
298+
* Holds if `n` does not require a `PostUpdateNode` as it either cannot be
299+
* modified or its modification cannot be observed, for example if it is a
300+
* freshly created object that is not saved in a variable.
301+
*
302+
* This predicate is only used for consistency checks.
303+
*/
304+
predicate isImmutableOrUnobservable(Node n) { none() }

‎cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll

Lines changed: 175 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
1+
/**
2+
* Provides consistency queries for checking invariants in the language-specific
3+
* data-flow classes and predicates.
4+
*/
5+
6+
private import DataFlowImplSpecific::Private
7+
private import DataFlowImplSpecific::Public
8+
private import tainttracking1.TaintTrackingParameter::Private
9+
private import tainttracking1.TaintTrackingParameter::Public
10+
11+
module Consistency {
12+
private class RelevantNode extends Node {
13+
RelevantNode() {
14+
this instanceof ArgumentNode or
15+
this instanceof ParameterNode or
16+
this instanceof ReturnNode or
17+
this = getAnOutNode(_, _) or
18+
simpleLocalFlowStep(this, _) or
19+
simpleLocalFlowStep(_, this) or
20+
jumpStep(this, _) or
21+
jumpStep(_, this) or
22+
storeStep(this, _, _) or
23+
storeStep(_, _, this) or
24+
readStep(this, _, _) or
25+
readStep(_, _, this) or
26+
defaultAdditionalTaintStep(this, _) or
27+
defaultAdditionalTaintStep(_, this)
28+
}
29+
}
30+
31+
query predicate uniqueEnclosingCallable(Node n, string msg) {
32+
exists(int c |
33+
n instanceof RelevantNode and
34+
c = count(n.getEnclosingCallable()) and
35+
c != 1 and
36+
msg = "Node should have one enclosing callable but has " + c + "."
37+
)
38+
}
39+
40+
query predicate uniqueTypeBound(Node n, string msg) {
41+
exists(int c |
42+
n instanceof RelevantNode and
43+
c = count(n.getTypeBound()) and
44+
c != 1 and
45+
msg = "Node should have one type bound but has " + c + "."
46+
)
47+
}
48+
49+
query predicate uniqueTypeRepr(Node n, string msg) {
50+
exists(int c |
51+
n instanceof RelevantNode and
52+
c = count(getErasedRepr(n.getTypeBound())) and
53+
c != 1 and
54+
msg = "Node should have one type representation but has " + c + "."
55+
)
56+
}
57+
58+
query predicate uniqueNodeLocation(Node n, string msg) {
59+
exists(int c |
60+
c =
61+
count(string filepath, int startline, int startcolumn, int endline, int endcolumn |
62+
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
63+
) and
64+
c != 1 and
65+
msg = "Node should have one ___location but has " + c + "."
66+
)
67+
}
68+
69+
query predicate missingLocation(string msg) {
70+
exists(int c |
71+
c =
72+
strictcount(Node n |
73+
not exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
74+
n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
75+
)
76+
) and
77+
msg = "Nodes without ___location: " + c
78+
)
79+
}
80+
81+
query predicate uniqueNodeToString(Node n, string msg) {
82+
exists(int c |
83+
c = count(n.toString()) and
84+
c != 1 and
85+
msg = "Node should have one toString but has " + c + "."
86+
)
87+
}
88+
89+
query predicate missingToString(string msg) {
90+
exists(int c |
91+
c = strictcount(Node n | not exists(n.toString())) and
92+
msg = "Nodes without toString: " + c
93+
)
94+
}
95+
96+
query predicate parameterCallable(ParameterNode p, string msg) {
97+
exists(DataFlowCallable c | p.isParameterOf(c, _) and c != p.getEnclosingCallable()) and
98+
msg = "Callable mismatch for parameter."
99+
}
100+
101+
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
102+
simpleLocalFlowStep(n1, n2) and
103+
n1.getEnclosingCallable() != n2.getEnclosingCallable() and
104+
msg = "Local flow step does not preserve enclosing callable."
105+
}
106+
107+
private DataFlowType typeRepr() { result = getErasedRepr(any(Node n).getTypeBound()) }
108+
109+
query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
110+
t = typeRepr() and
111+
not compatibleTypes(t, t) and
112+
msg = "Type compatibility predicate is not reflexive."
113+
}
114+
115+
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
116+
isUnreachableInCall(n, call) and
117+
exists(DataFlowCallable c |
118+
c = n.getEnclosingCallable() and
119+
not viableCallable(call) = c
120+
) and
121+
msg = "Call context for isUnreachableInCall is inconsistent with call graph."
122+
}
123+
124+
query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
125+
(
126+
n = getAnOutNode(call, _) and
127+
msg = "OutNode and call does not share enclosing callable."
128+
or
129+
n.(ArgumentNode).argumentOf(call, _) and
130+
msg = "ArgumentNode and call does not share enclosing callable."
131+
) and
132+
n.getEnclosingCallable() != call.getEnclosingCallable()
133+
}
134+
135+
query predicate postIsNotPre(PostUpdateNode n, string msg) {
136+
n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
137+
}
138+
139+
query predicate postHasUniquePre(PostUpdateNode n, string msg) {
140+
exists(int c |
141+
c = count(n.getPreUpdateNode()) and
142+
c != 1 and
143+
msg = "PostUpdateNode should have one pre-update node but has " + c + "."
144+
)
145+
}
146+
147+
query predicate uniquePostUpdate(Node n, string msg) {
148+
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
149+
msg = "Node has multiple PostUpdateNodes."
150+
}
151+
152+
query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
153+
n.getEnclosingCallable() != n.getPreUpdateNode().getEnclosingCallable() and
154+
msg = "PostUpdateNode does not share callable with its pre-update node."
155+
}
156+
157+
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
158+
159+
query predicate reverseRead(Node n, string msg) {
160+
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
161+
msg = "Origin of readStep is missing a PostUpdateNode."
162+
}
163+
164+
query predicate storeIsPostUpdate(Node n, string msg) {
165+
storeStep(_, _, n) and
166+
not n instanceof PostUpdateNode and
167+
msg = "Store targets should be PostUpdateNodes."
168+
}
169+
170+
query predicate argHasPostUpdate(ArgumentNode n, string msg) {
171+
not hasPost(n) and
172+
not isImmutableOrUnobservable(n) and
173+
msg = "ArgumentNode is missing PostUpdateNode."
174+
}
175+
}

‎cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,3 +202,12 @@ class DataFlowCall extends CallInstruction {
202202
predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub implementation
203203

204204
int accessPathLimit() { result = 5 }
205+
206+
/**
207+
* Holds if `n` does not require a `PostUpdateNode` as it either cannot be
208+
* modified or its modification cannot be observed, for example if it is a
209+
* freshly created object that is not saved in a variable.
210+
*
211+
* This predicate is only used for consistency checks.
212+
*/
213+
predicate isImmutableOrUnobservable(Node n) { none() }

0 commit comments

Comments
 (0)