Skip to content

Commit 67d386b

Browse files
aschackmullaschackmull
committed
C++/C#: Add synchronization.
1 parent 8e2b56c commit 67d386b

File tree

7 files changed

+441
-0
lines changed

7 files changed

+441
-0
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: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
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 TaintTrackingUtil
9+
10+
module Consistency {
11+
private class RelevantNode extends Node {
12+
RelevantNode() {
13+
this instanceof ArgumentNode or
14+
this instanceof ParameterNode or
15+
this instanceof ReturnNode or
16+
this = getAnOutNode(_, _) or
17+
simpleLocalFlowStep(this, _) or
18+
simpleLocalFlowStep(_, this) or
19+
jumpStep(this, _) or
20+
jumpStep(_, this) or
21+
storeStep(this, _, _) or
22+
storeStep(_, _, this) or
23+
readStep(this, _, _) or
24+
readStep(_, _, this) or
25+
defaultAdditionalTaintStep(this, _) or
26+
defaultAdditionalTaintStep(_, this)
27+
}
28+
}
29+
30+
query predicate uniqueEnclosingCallable(Node n, string msg) {
31+
exists(int c |
32+
n instanceof RelevantNode and
33+
c = count(n.getEnclosingCallable()) and
34+
c != 1 and
35+
msg = "Node should have one enclosing callable but has " + c + "."
36+
)
37+
}
38+
39+
query predicate uniqueTypeBound(Node n, string msg) {
40+
exists(int c |
41+
n instanceof RelevantNode and
42+
c = count(n.getTypeBound()) and
43+
c != 1 and
44+
msg = "Node should have one type bound but has " + c + "."
45+
)
46+
}
47+
48+
query predicate uniqueTypeRepr(Node n, string msg) {
49+
exists(int c |
50+
n instanceof RelevantNode and
51+
c = count(getErasedRepr(n.getTypeBound())) and
52+
c != 1 and
53+
msg = "Node should have one type representation but has " + c + "."
54+
)
55+
}
56+
57+
query predicate parameterCallable(ParameterNode p, string msg) {
58+
exists(DataFlowCallable c | p.isParameterOf(c, _) and c != p.getEnclosingCallable()) and
59+
msg = "Callable mismatch for parameter."
60+
}
61+
62+
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
63+
simpleLocalFlowStep(n1, n2) and
64+
n1.getEnclosingCallable() != n2.getEnclosingCallable() and
65+
msg = "Local flow step does not preserve enclosing callable."
66+
}
67+
68+
private DataFlowType typeRepr() { result = getErasedRepr(any(Node n).getTypeBound()) }
69+
70+
query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
71+
t = typeRepr() and
72+
not compatibleTypes(t, t) and
73+
msg = "Type compatibility predicate is not reflexive."
74+
}
75+
76+
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
77+
isUnreachableInCall(n, call) and
78+
exists(DataFlowCallable c |
79+
c = n.getEnclosingCallable() and
80+
not viableCallable(call) = c
81+
) and
82+
msg = "Call context for isUnreachableInCall is inconsistent with call graph."
83+
}
84+
85+
query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
86+
(
87+
n = getAnOutNode(call, _) and
88+
msg = "OutNode and call does not share enclosing callable."
89+
or
90+
n.(ArgumentNode).argumentOf(call, _) and
91+
msg = "ArgumentNode and call does not share enclosing callable."
92+
) and
93+
n.getEnclosingCallable() != call.getEnclosingCallable()
94+
}
95+
96+
query predicate postIsNotPre(PostUpdateNode n, string msg) {
97+
n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
98+
}
99+
100+
query predicate postHasUniquePre(PostUpdateNode n, string msg) {
101+
exists(int c |
102+
c = count(n.getPreUpdateNode()) and
103+
c != 1 and
104+
msg = "PostUpdateNode should have one pre-update node but has " + c + "."
105+
)
106+
}
107+
108+
query predicate uniquePostUpdate(Node n, string msg) {
109+
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
110+
msg = "Node has multiple PostUpdateNodes."
111+
}
112+
113+
query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
114+
n.getEnclosingCallable() != n.getPreUpdateNode().getEnclosingCallable() and
115+
msg = "PostUpdateNode does not share callable with its pre-update node."
116+
}
117+
118+
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
119+
120+
query predicate reverseRead(Node n, string msg) {
121+
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
122+
msg = "Origin of readStep is missing a PostUpdateNode."
123+
}
124+
125+
query predicate storeIsPostUpdate(Node n, string msg) {
126+
storeStep(_, _, n) and
127+
not n instanceof PostUpdateNode and
128+
msg = "Store targets should be PostUpdateNodes."
129+
}
130+
131+
query predicate argHasPostUpdate(ArgumentNode n, string msg) {
132+
not hasPost(n) and
133+
not isImmutableOrUnobservable(n) and
134+
msg = "ArgumentNode is missing PostUpdateNode."
135+
}
136+
}

‎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: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
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 TaintTrackingUtil
9+
10+
module Consistency {
11+
private class RelevantNode extends Node {
12+
RelevantNode() {
13+
this instanceof ArgumentNode or
14+
this instanceof ParameterNode or
15+
this instanceof ReturnNode or
16+
this = getAnOutNode(_, _) or
17+
simpleLocalFlowStep(this, _) or
18+
simpleLocalFlowStep(_, this) or
19+
jumpStep(this, _) or
20+
jumpStep(_, this) or
21+
storeStep(this, _, _) or
22+
storeStep(_, _, this) or
23+
readStep(this, _, _) or
24+
readStep(_, _, this) or
25+
defaultAdditionalTaintStep(this, _) or
26+
defaultAdditionalTaintStep(_, this)
27+
}
28+
}
29+
30+
query predicate uniqueEnclosingCallable(Node n, string msg) {
31+
exists(int c |
32+
n instanceof RelevantNode and
33+
c = count(n.getEnclosingCallable()) and
34+
c != 1 and
35+
msg = "Node should have one enclosing callable but has " + c + "."
36+
)
37+
}
38+
39+
query predicate uniqueTypeBound(Node n, string msg) {
40+
exists(int c |
41+
n instanceof RelevantNode and
42+
c = count(n.getTypeBound()) and
43+
c != 1 and
44+
msg = "Node should have one type bound but has " + c + "."
45+
)
46+
}
47+
48+
query predicate uniqueTypeRepr(Node n, string msg) {
49+
exists(int c |
50+
n instanceof RelevantNode and
51+
c = count(getErasedRepr(n.getTypeBound())) and
52+
c != 1 and
53+
msg = "Node should have one type representation but has " + c + "."
54+
)
55+
}
56+
57+
query predicate parameterCallable(ParameterNode p, string msg) {
58+
exists(DataFlowCallable c | p.isParameterOf(c, _) and c != p.getEnclosingCallable()) and
59+
msg = "Callable mismatch for parameter."
60+
}
61+
62+
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
63+
simpleLocalFlowStep(n1, n2) and
64+
n1.getEnclosingCallable() != n2.getEnclosingCallable() and
65+
msg = "Local flow step does not preserve enclosing callable."
66+
}
67+
68+
private DataFlowType typeRepr() { result = getErasedRepr(any(Node n).getTypeBound()) }
69+
70+
query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
71+
t = typeRepr() and
72+
not compatibleTypes(t, t) and
73+
msg = "Type compatibility predicate is not reflexive."
74+
}
75+
76+
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
77+
isUnreachableInCall(n, call) and
78+
exists(DataFlowCallable c |
79+
c = n.getEnclosingCallable() and
80+
not viableCallable(call) = c
81+
) and
82+
msg = "Call context for isUnreachableInCall is inconsistent with call graph."
83+
}
84+
85+
query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
86+
(
87+
n = getAnOutNode(call, _) and
88+
msg = "OutNode and call does not share enclosing callable."
89+
or
90+
n.(ArgumentNode).argumentOf(call, _) and
91+
msg = "ArgumentNode and call does not share enclosing callable."
92+
) and
93+
n.getEnclosingCallable() != call.getEnclosingCallable()
94+
}
95+
96+
query predicate postIsNotPre(PostUpdateNode n, string msg) {
97+
n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
98+
}
99+
100+
query predicate postHasUniquePre(PostUpdateNode n, string msg) {
101+
exists(int c |
102+
c = count(n.getPreUpdateNode()) and
103+
c != 1 and
104+
msg = "PostUpdateNode should have one pre-update node but has " + c + "."
105+
)
106+
}
107+
108+
query predicate uniquePostUpdate(Node n, string msg) {
109+
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
110+
msg = "Node has multiple PostUpdateNodes."
111+
}
112+
113+
query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
114+
n.getEnclosingCallable() != n.getPreUpdateNode().getEnclosingCallable() and
115+
msg = "PostUpdateNode does not share callable with its pre-update node."
116+
}
117+
118+
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
119+
120+
query predicate reverseRead(Node n, string msg) {
121+
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
122+
msg = "Origin of readStep is missing a PostUpdateNode."
123+
}
124+
125+
query predicate storeIsPostUpdate(Node n, string msg) {
126+
storeStep(_, _, n) and
127+
not n instanceof PostUpdateNode and
128+
msg = "Store targets should be PostUpdateNodes."
129+
}
130+
131+
query predicate argHasPostUpdate(ArgumentNode n, string msg) {
132+
not hasPost(n) and
133+
not isImmutableOrUnobservable(n) and
134+
msg = "ArgumentNode is missing PostUpdateNode."
135+
}
136+
}

‎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)