Skip to content

Commit ee9c0dc

Browse files
committed
C++: Add library for must-flow.
1 parent eece222 commit ee9c0dc

File tree

1 file changed

+265
-0
lines changed

1 file changed

+265
-0
lines changed
Lines changed: 265 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,265 @@
1+
/**
2+
* This file provides a library for inter-procedural must-flow data flow analysis.
3+
* Unlike `DataFlow.qll`, the analysis provided by this file checks whether data _must_ flow
4+
* from a source to a _sink_.
5+
*/
6+
7+
private import cpp
8+
import semmle.code.cpp.ir.dataflow.DataFlow
9+
private import semmle.code.cpp.ir.IR
10+
11+
/**
12+
* A configuration of a data flow analysis that performs must-flow analysis. This is different
13+
* from `DataFlow.qll` which performs may-flow analysis (i.e., it finds paths where the source _may_
14+
* flow to the sink).
15+
*
16+
* Like in `DataFlow.qll`, each use of the `MustFlow.qll` library must define its own unique extension
17+
* of this abstract class. To create a configuration, extend this class with a subclass whose
18+
* characteristic predicate is a unique singleton string and override `isSource`, `isSink` (and
19+
* `isAdditionalFlowStep` if additional steps are required).
20+
*/
21+
abstract class MustFlowConfiguration extends string {
22+
bindingset[this]
23+
MustFlowConfiguration() { any() }
24+
25+
/**
26+
* Holds if `source` is a relevant data flow source.
27+
*/
28+
abstract predicate isSource(DataFlow::Node source);
29+
30+
/**
31+
* Holds if `sink` is a relevant data flow sink.
32+
*/
33+
abstract predicate isSink(DataFlow::Node sink);
34+
35+
/**
36+
* Holds if the additional flow step from `node1` to `node2` must be taken
37+
* into account in the analysis.
38+
*/
39+
predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
40+
41+
/**
42+
* Holds if data must flow from `source` to `sink` for this configuration.
43+
*
44+
* The corresponding paths are generated from the end-points and the graph
45+
* included in the module `PathGraph`.
46+
*/
47+
final predicate hasFlowPath(MustFlowPathNode source, MustFlowPathSink sink) {
48+
this.isSource(source.getNode()) and
49+
source.getASuccessor+() = sink
50+
}
51+
}
52+
53+
/** Holds if `node` flows from a source. */
54+
pragma[nomagic]
55+
private predicate flowsFromSource(DataFlow::Node node, MustFlowConfiguration config) {
56+
config.isSource(node)
57+
or
58+
exists(DataFlow::Node mid |
59+
step(mid, node, config) and
60+
flowsFromSource(mid, pragma[only_bind_into](config))
61+
)
62+
}
63+
64+
/** Holds if `instr` flows to a sink. */
65+
pragma[nomagic]
66+
private predicate flowsToSink(DataFlow::Node node, MustFlowConfiguration config) {
67+
flowsFromSource(node, pragma[only_bind_into](config)) and
68+
(
69+
config.isSink(node)
70+
or
71+
exists(DataFlow::Node mid |
72+
step(node, mid, config) and
73+
flowsToSink(mid, pragma[only_bind_into](config))
74+
)
75+
)
76+
}
77+
78+
cached
79+
private module Cached {
80+
/** Holds if `p` is the `n`'th parameter of the non-virtual function `f`. */
81+
private predicate parameterOf(Parameter p, Function f, int n) {
82+
not f.isVirtual() and f.getParameter(n) = p
83+
}
84+
85+
/**
86+
* Holds if `instr` is the `n`'th argument to a call to the non-virtual function `f`, and
87+
* `init` is the corresponding initiazation instruction that receives the value of `instr` in `f`.
88+
*/
89+
private predicate flowIntoParameter(
90+
Function f, int n, CallInstruction call, Instruction instr, InitializeParameterInstruction init
91+
) {
92+
not f.isVirtual() and
93+
call.getPositionalArgument(n) = instr and
94+
f = call.getStaticCallTarget() and
95+
getEnclosingNonVirtualFunctionInitializeParameter(init, f) and
96+
init.getParameter().getIndex() = pragma[only_bind_into](pragma[only_bind_out](n))
97+
}
98+
99+
/**
100+
* Holds if `instr` is an argument to a call to the function `f`, and `init` is the
101+
* corresponding initialization instruction that receives the value of `instr` in `f`.
102+
*/
103+
pragma[noinline]
104+
private predicate getPositionalArgumentInitParam(
105+
CallInstruction call, Instruction instr, InitializeParameterInstruction init, Function f
106+
) {
107+
exists(int n |
108+
parameterOf(_, f, n) and
109+
flowIntoParameter(f, pragma[only_bind_into](pragma[only_bind_out](n)), call, instr, init)
110+
)
111+
}
112+
113+
/**
114+
* Holds if `instr` is the qualifier to a call to the non-virtual function `f`, and
115+
* `init` is the corresponding initiazation instruction that receives the value of
116+
* `instr` in `f`.
117+
*/
118+
pragma[noinline]
119+
private predicate getThisArgumentInitParam(
120+
CallInstruction call, Instruction instr, InitializeParameterInstruction init, Function f
121+
) {
122+
not f.isVirtual() and
123+
call.getStaticCallTarget() = f and
124+
getEnclosingNonVirtualFunctionInitializeParameter(init, f) and
125+
call.getThisArgument() = instr and
126+
init.getIRVariable() instanceof IRThisVariable
127+
}
128+
129+
/** Holds if `f` is the enclosing non-virtual function of `init`. */
130+
private predicate getEnclosingNonVirtualFunctionInitializeParameter(
131+
InitializeParameterInstruction init, Function f
132+
) {
133+
not f.isVirtual() and
134+
init.getEnclosingFunction() = f
135+
}
136+
137+
/** Holds if `f` is the enclosing non-virtual function of `init`. */
138+
private predicate getEnclosingNonVirtualFunctionInitializeIndirection(
139+
InitializeIndirectionInstruction init, Function f
140+
) {
141+
not f.isVirtual() and
142+
init.getEnclosingFunction() = f
143+
}
144+
145+
/**
146+
* Holds if `instr` is an argument (or argument indirection) to a call, and
147+
* `succ` is the corresponding initialization instruction in the call target.
148+
*/
149+
private predicate flowThroughCallable(Instruction argument, Instruction parameter) {
150+
// Flow from an argument to a parameter
151+
exists(CallInstruction call, InitializeParameterInstruction init | init = parameter |
152+
getPositionalArgumentInitParam(call, argument, init, call.getStaticCallTarget())
153+
or
154+
getThisArgumentInitParam(call, argument, init, call.getStaticCallTarget())
155+
)
156+
or
157+
// Flow from argument indirection to parameter indirection
158+
exists(
159+
CallInstruction call, ReadSideEffectInstruction read, InitializeIndirectionInstruction init
160+
|
161+
init = parameter and
162+
read.getPrimaryInstruction() = call and
163+
getEnclosingNonVirtualFunctionInitializeIndirection(init, call.getStaticCallTarget())
164+
|
165+
exists(int n |
166+
read.getSideEffectOperand().getAnyDef() = argument and
167+
read.getIndex() = pragma[only_bind_into](n) and
168+
init.getParameter().getIndex() = pragma[only_bind_into](n)
169+
)
170+
or
171+
call.getThisArgument() = argument and
172+
init.getIRVariable() instanceof IRThisVariable
173+
)
174+
}
175+
176+
private predicate instructionToOperandStep(Instruction instr, Operand operand) {
177+
operand.getDef() = instr
178+
}
179+
180+
private predicate operandToInstructionStep(Operand operand, Instruction instr) {
181+
instr.(CopyInstruction).getSourceValueOperand() = operand
182+
or
183+
instr.(ConvertInstruction).getUnaryOperand() = operand
184+
or
185+
instr.(CheckedConvertOrNullInstruction).getUnaryOperand() = operand
186+
or
187+
instr.(InheritanceConversionInstruction).getUnaryOperand() = operand
188+
or
189+
instr.(ChiInstruction).getTotalOperand() = operand
190+
}
191+
192+
cached
193+
predicate step(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
194+
instructionToOperandStep(nodeFrom.asInstruction(), nodeTo.asOperand())
195+
or
196+
flowThroughCallable(nodeFrom.asInstruction(), nodeTo.asInstruction())
197+
or
198+
operandToInstructionStep(nodeFrom.asOperand(), nodeTo.asInstruction())
199+
}
200+
}
201+
202+
/** Holds if `nodeFrom` flows to `nodeTo`. */
203+
private predicate step(DataFlow::Node nodeFrom, DataFlow::Node nodeTo, MustFlowConfiguration config) {
204+
exists(config) and
205+
Cached::step(nodeFrom, nodeTo)
206+
or
207+
config.isAdditionalFlowStep(nodeFrom, nodeTo)
208+
}
209+
210+
private newtype TLocalPathNode =
211+
MkLocalPathNode(DataFlow::Node n, MustFlowConfiguration config) {
212+
flowsToSink(n, config) and
213+
(
214+
config.isSource(n)
215+
or
216+
exists(MustFlowPathNode mid | step(mid.getNode(), n, config))
217+
)
218+
}
219+
220+
/** A `Node` that is in a path from a source to a sink. */
221+
class MustFlowPathNode extends TLocalPathNode {
222+
DataFlow::Node n;
223+
224+
MustFlowPathNode() { this = MkLocalPathNode(n, _) }
225+
226+
/** Gets the underlying node. */
227+
DataFlow::Node getNode() { result = n }
228+
229+
/** Gets a textual representation of this node. */
230+
string toString() { result = n.toString() }
231+
232+
/** Gets the location of this element. */
233+
Location getLocation() { result = n.getLocation() }
234+
235+
/** Gets a successor node, if any. */
236+
MustFlowPathNode getASuccessor() {
237+
step(this.getNode(), result.getNode(), this.getConfiguration())
238+
}
239+
240+
/** Gets the associated configuration. */
241+
MustFlowConfiguration getConfiguration() { this = MkLocalPathNode(_, result) }
242+
}
243+
244+
private class MustFlowPathSink extends MustFlowPathNode {
245+
MustFlowPathSink() { this.getConfiguration().isSink(this.getNode()) }
246+
}
247+
248+
/**
249+
* Provides the query predicates needed to include a graph in a path-problem query.
250+
*/
251+
module PathGraph {
252+
private predicate reach(MustFlowPathNode n) {
253+
n instanceof MustFlowPathSink or reach(n.getASuccessor())
254+
}
255+
256+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
257+
query predicate edges(MustFlowPathNode a, MustFlowPathNode b) {
258+
a.getASuccessor() = b and reach(b)
259+
}
260+
261+
/** Holds if `n` is a node in the graph of data flow path explanations. */
262+
query predicate nodes(MustFlowPathNode n, string key, string val) {
263+
reach(n) and key = "semmle.label" and val = n.toString()
264+
}
265+
}

0 commit comments

Comments
 (0)