@@ -8,83 +8,145 @@ private import cpp
88private import semmle.code.cpp.ir.IR
99
1010/**
11- * A configuration of a data flow analysis that performs must-flow analysis. This is different
12- * from `DataFlow.qll` which performs may-flow analysis (i.e., it finds paths where the source _may_
13- * flow to the sink).
14- *
15- * Like in `DataFlow.qll`, each use of the `MustFlow.qll` library must define its own unique extension
16- * of this abstract class. To create a configuration, extend this class with a subclass whose
17- * characteristic predicate is a unique singleton string and override `isSource`, `isSink` (and
18- * `isAdditionalFlowStep` if additional steps are required).
11+ * Provides an inter-procedural must-flow data flow analysis.
1912 */
20- abstract class MustFlowConfiguration extends string {
21- bindingset [ this ]
22- MustFlowConfiguration ( ) { any ( ) }
23-
24- /**
25- * Holds if `source` is a relevant data flow source.
26- */
27- abstract predicate isSource ( Instruction source ) ;
28-
13+ module MustFlow {
2914 /**
30- * Holds if `sink` is a relevant data flow sink.
15+ * An input configuration of a data flow analysis that performs must-flow analysis. This is different
16+ * from `DataFlow.qll` which performs may-flow analysis (i.e., it finds paths where the source _may_
17+ * flow to the sink).
3118 */
32- abstract predicate isSink ( Operand sink ) ;
33-
34- /**
35- * Holds if data flow through `instr` is prohibited.
36- */
37- predicate isBarrier ( Instruction instr ) { none ( ) }
19+ signature module ConfigSig {
20+ /**
21+ * Holds if `source` is a relevant data flow source.
22+ */
23+ predicate isSource ( Instruction source ) ;
24+
25+ /**
26+ * Holds if `sink` is a relevant data flow sink.
27+ */
28+ predicate isSink ( Operand sink ) ;
29+
30+ /**
31+ * Holds if data flow through `instr` is prohibited.
32+ */
33+ default predicate isBarrier ( Instruction instr ) { none ( ) }
34+
35+ /**
36+ * Holds if the additional flow step from `node1` to `node2` must be taken
37+ * into account in the analysis.
38+ */
39+ default predicate isAdditionalFlowStep ( Operand node1 , Instruction node2 ) { none ( ) }
40+
41+ /** Holds if this configuration allows flow from arguments to parameters. */
42+ default predicate allowInterproceduralFlow ( ) { any ( ) }
43+ }
3844
3945 /**
40- * Holds if the additional flow step from `node1` to `node2` must be taken
41- * into account in the analysis.
46+ * Constructs a global must-flow computation.
4247 */
43- predicate isAdditionalFlowStep ( Operand node1 , Instruction node2 ) { none ( ) }
44-
45- /** Holds if this configuration allows flow from arguments to parameters. */
46- predicate allowInterproceduralFlow ( ) { any ( ) }
48+ module Global< ConfigSig Config> {
49+ import Config
50+
51+ /**
52+ * Holds if data must flow from `source` to `sink`.
53+ *
54+ * The corresponding paths are generated from the end-points and the graph
55+ * included in the module `PathGraph`.
56+ */
57+ predicate flowPath ( PathNode source , PathSink sink ) {
58+ isSource ( source .getInstruction ( ) ) and
59+ source .getASuccessor * ( ) = sink
60+ }
61+
62+ /** Holds if `node` flows from a source. */
63+ pragma [ nomagic]
64+ private predicate flowsFromSource ( Instruction node ) {
65+ not isBarrier ( node ) and
66+ (
67+ isSource ( node )
68+ or
69+ exists ( Instruction mid |
70+ step ( mid , node ) and
71+ flowsFromSource ( mid )
72+ )
73+ )
74+ }
75+
76+ /** Holds if `node` flows to a sink. */
77+ pragma [ nomagic]
78+ private predicate flowsToSink ( Instruction node ) {
79+ flowsFromSource ( node ) and
80+ (
81+ isSink ( node .getAUse ( ) )
82+ or
83+ exists ( Instruction mid |
84+ step ( node , mid ) and
85+ flowsToSink ( mid )
86+ )
87+ )
88+ }
4789
48- /**
49- * Holds if data must flow from `source` to `sink` for this configuration.
50- *
51- * The corresponding paths are generated from the end-points and the graph
52- * included in the module `PathGraph`.
53- */
54- final predicate hasFlowPath ( MustFlowPathNode source , MustFlowPathSink sink ) {
55- this .isSource ( source .getInstruction ( ) ) and
56- source .getASuccessor * ( ) = sink
90+ /** Holds if `nodeFrom` flows to `nodeTo`. */
91+ private predicate step ( Instruction nodeFrom , Instruction nodeTo ) {
92+ Cached:: localStep ( nodeFrom , nodeTo )
93+ or
94+ allowInterproceduralFlow ( ) and
95+ Cached:: flowThroughCallable ( nodeFrom , nodeTo )
96+ or
97+ isAdditionalFlowStep ( nodeFrom .getAUse ( ) , nodeTo )
98+ }
99+
100+ private newtype TLocalPathNode =
101+ MkLocalPathNode ( Instruction n ) {
102+ flowsToSink ( n ) and
103+ (
104+ isSource ( n )
105+ or
106+ exists ( PathNode mid | step ( mid .getInstruction ( ) , n ) )
107+ )
108+ }
109+
110+ /** A `Node` that is in a path from a source to a sink. */
111+ class PathNode extends TLocalPathNode {
112+ Instruction n ;
113+
114+ PathNode ( ) { this = MkLocalPathNode ( n ) }
115+
116+ /** Gets the underlying node. */
117+ Instruction getInstruction ( ) { result = n }
118+
119+ /** Gets a textual representation of this node. */
120+ string toString ( ) { result = n .getAst ( ) .toString ( ) }
121+
122+ /** Gets the location of this element. */
123+ Location getLocation ( ) { result = n .getLocation ( ) }
124+
125+ /** Gets a successor node, if any. */
126+ PathNode getASuccessor ( ) { step ( this .getInstruction ( ) , result .getInstruction ( ) ) }
127+ }
128+
129+ private class PathSink extends PathNode {
130+ PathSink ( ) { isSink ( this .getInstruction ( ) .getAUse ( ) ) }
131+ }
132+
133+ /**
134+ * Provides the query predicates needed to include a graph in a path-problem query.
135+ */
136+ module PathGraph {
137+ private predicate reach ( PathNode n ) { n instanceof PathSink or reach ( n .getASuccessor ( ) ) }
138+
139+ /** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
140+ query predicate edges ( PathNode a , PathNode b ) { a .getASuccessor ( ) = b and reach ( b ) }
141+
142+ /** Holds if `n` is a node in the graph of data flow path explanations. */
143+ query predicate nodes ( PathNode n , string key , string val ) {
144+ reach ( n ) and key = "semmle.label" and val = n .toString ( )
145+ }
146+ }
57147 }
58148}
59149
60- /** Holds if `node` flows from a source. */
61- pragma [ nomagic]
62- private predicate flowsFromSource ( Instruction node , MustFlowConfiguration config ) {
63- not config .isBarrier ( node ) and
64- (
65- config .isSource ( node )
66- or
67- exists ( Instruction mid |
68- step ( mid , node , config ) and
69- flowsFromSource ( mid , pragma [ only_bind_into ] ( config ) )
70- )
71- )
72- }
73-
74- /** Holds if `node` flows to a sink. */
75- pragma [ nomagic]
76- private predicate flowsToSink ( Instruction node , MustFlowConfiguration config ) {
77- flowsFromSource ( node , pragma [ only_bind_into ] ( config ) ) and
78- (
79- config .isSink ( node .getAUse ( ) )
80- or
81- exists ( Instruction mid |
82- step ( node , mid , config ) and
83- flowsToSink ( mid , pragma [ only_bind_into ] ( config ) )
84- )
85- )
86- }
87-
88150cached
89151private module Cached {
90152 /** Holds if `p` is the `n`'th parameter of the non-virtual function `f`. */
@@ -102,7 +164,7 @@ private module Cached {
102164 not f .isVirtual ( ) and
103165 call .getPositionalArgument ( n ) = instr and
104166 f = call .getStaticCallTarget ( ) and
105- getEnclosingNonVirtualFunctionInitializeParameter ( init , f ) and
167+ isEnclosingNonVirtualFunctionInitializeParameter ( init , f ) and
106168 init .getParameter ( ) .getIndex ( ) = pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( n ) )
107169 }
108170
@@ -111,7 +173,7 @@ private module Cached {
111173 * corresponding initialization instruction that receives the value of `instr` in `f`.
112174 */
113175 pragma [ noinline]
114- private predicate getPositionalArgumentInitParam (
176+ private predicate isPositionalArgumentInitParam (
115177 CallInstruction call , Instruction instr , InitializeParameterInstruction init , Function f
116178 ) {
117179 exists ( int n |
@@ -126,42 +188,43 @@ private module Cached {
126188 * `instr` in `f`.
127189 */
128190 pragma [ noinline]
129- private predicate getThisArgumentInitParam (
191+ private predicate isThisArgumentInitParam (
130192 CallInstruction call , Instruction instr , InitializeParameterInstruction init , Function f
131193 ) {
132194 not f .isVirtual ( ) and
133195 call .getStaticCallTarget ( ) = f and
134- getEnclosingNonVirtualFunctionInitializeParameter ( init , f ) and
196+ isEnclosingNonVirtualFunctionInitializeParameter ( init , f ) and
135197 call .getThisArgument ( ) = instr and
136198 init .getIRVariable ( ) instanceof IRThisVariable
137199 }
138200
139201 /** Holds if `f` is the enclosing non-virtual function of `init`. */
140- private predicate getEnclosingNonVirtualFunctionInitializeParameter (
202+ private predicate isEnclosingNonVirtualFunctionInitializeParameter (
141203 InitializeParameterInstruction init , Function f
142204 ) {
143205 not f .isVirtual ( ) and
144206 init .getEnclosingFunction ( ) = f
145207 }
146208
147209 /** Holds if `f` is the enclosing non-virtual function of `init`. */
148- private predicate getEnclosingNonVirtualFunctionInitializeIndirection (
210+ private predicate isEnclosingNonVirtualFunctionInitializeIndirection (
149211 InitializeIndirectionInstruction init , Function f
150212 ) {
151213 not f .isVirtual ( ) and
152214 init .getEnclosingFunction ( ) = f
153215 }
154216
155217 /**
156- * Holds if `instr ` is an argument (or argument indirection) to a call, and
157- * `succ ` is the corresponding initialization instruction in the call target.
218+ * Holds if `argument ` is an argument (or argument indirection) to a call, and
219+ * `parameter ` is the corresponding initialization instruction in the call target.
158220 */
159- private predicate flowThroughCallable ( Instruction argument , Instruction parameter ) {
221+ cached
222+ predicate flowThroughCallable ( Instruction argument , Instruction parameter ) {
160223 // Flow from an argument to a parameter
161224 exists ( CallInstruction call , InitializeParameterInstruction init | init = parameter |
162- getPositionalArgumentInitParam ( call , argument , init , call .getStaticCallTarget ( ) )
225+ isPositionalArgumentInitParam ( call , argument , init , call .getStaticCallTarget ( ) )
163226 or
164- getThisArgumentInitParam ( call , argument , init , call .getStaticCallTarget ( ) )
227+ isThisArgumentInitParam ( call , argument , init , call .getStaticCallTarget ( ) )
165228 )
166229 or
167230 // Flow from argument indirection to parameter indirection
@@ -170,7 +233,7 @@ private module Cached {
170233 |
171234 init = parameter and
172235 read .getPrimaryInstruction ( ) = call and
173- getEnclosingNonVirtualFunctionInitializeIndirection ( init , call .getStaticCallTarget ( ) )
236+ isEnclosingNonVirtualFunctionInitializeIndirection ( init , call .getStaticCallTarget ( ) )
174237 |
175238 exists ( int n |
176239 read .getSideEffectOperand ( ) .getAnyDef ( ) = argument and
@@ -205,92 +268,10 @@ private module Cached {
205268 }
206269
207270 cached
208- predicate step ( Instruction nodeFrom , Instruction nodeTo ) {
271+ predicate localStep ( Instruction nodeFrom , Instruction nodeTo ) {
209272 exists ( Operand mid |
210273 instructionToOperandStep ( nodeFrom , mid ) and
211274 operandToInstructionStep ( mid , nodeTo )
212275 )
213- or
214- flowThroughCallable ( nodeFrom , nodeTo )
215- }
216- }
217-
218- /**
219- * Gets the enclosing callable of `n`. Unlike `n.getEnclosingCallable()`, this
220- * predicate ensures that joins go from `n` to the result instead of the other
221- * way around.
222- */
223- pragma [ inline]
224- private IRFunction getEnclosingCallable ( Instruction n ) {
225- pragma [ only_bind_into ] ( result ) = pragma [ only_bind_out ] ( n ) .getEnclosingIRFunction ( )
226- }
227-
228- /** Holds if `nodeFrom` flows to `nodeTo`. */
229- private predicate step ( Instruction nodeFrom , Instruction nodeTo , MustFlowConfiguration config ) {
230- exists ( config ) and
231- Cached:: step ( pragma [ only_bind_into ] ( nodeFrom ) , pragma [ only_bind_into ] ( nodeTo ) ) and
232- (
233- config .allowInterproceduralFlow ( )
234- or
235- getEnclosingCallable ( nodeFrom ) = getEnclosingCallable ( nodeTo )
236- )
237- or
238- config .isAdditionalFlowStep ( nodeFrom .getAUse ( ) , nodeTo )
239- }
240-
241- private newtype TLocalPathNode =
242- MkLocalPathNode ( Instruction n , MustFlowConfiguration config ) {
243- flowsToSink ( n , config ) and
244- (
245- config .isSource ( n )
246- or
247- exists ( MustFlowPathNode mid | step ( mid .getInstruction ( ) , n , config ) )
248- )
249- }
250-
251- /** A `Node` that is in a path from a source to a sink. */
252- class MustFlowPathNode extends TLocalPathNode {
253- Instruction n ;
254-
255- MustFlowPathNode ( ) { this = MkLocalPathNode ( n , _) }
256-
257- /** Gets the underlying node. */
258- Instruction getInstruction ( ) { result = n }
259-
260- /** Gets a textual representation of this node. */
261- string toString ( ) { result = n .getAst ( ) .toString ( ) }
262-
263- /** Gets the location of this element. */
264- Location getLocation ( ) { result = n .getLocation ( ) }
265-
266- /** Gets a successor node, if any. */
267- MustFlowPathNode getASuccessor ( ) {
268- step ( this .getInstruction ( ) , result .getInstruction ( ) , this .getConfiguration ( ) )
269- }
270-
271- /** Gets the associated configuration. */
272- MustFlowConfiguration getConfiguration ( ) { this = MkLocalPathNode ( _, result ) }
273- }
274-
275- private class MustFlowPathSink extends MustFlowPathNode {
276- MustFlowPathSink ( ) { this .getConfiguration ( ) .isSink ( this .getInstruction ( ) .getAUse ( ) ) }
277- }
278-
279- /**
280- * Provides the query predicates needed to include a graph in a path-problem query.
281- */
282- module PathGraph {
283- private predicate reach ( MustFlowPathNode n ) {
284- n instanceof MustFlowPathSink or reach ( n .getASuccessor ( ) )
285- }
286-
287- /** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
288- query predicate edges ( MustFlowPathNode a , MustFlowPathNode b ) {
289- a .getASuccessor ( ) = b and reach ( b )
290- }
291-
292- /** Holds if `n` is a node in the graph of data flow path explanations. */
293- query predicate nodes ( MustFlowPathNode n , string key , string val ) {
294- reach ( n ) and key = "semmle.label" and val = n .toString ( )
295276 }
296277}
0 commit comments