17
17
18
18
import cpp
19
19
import experimental.semmle.code.cpp.dataflow.ProductFlow
20
- import semmle.code.cpp.ir.dataflow.DataFlow3
21
20
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
22
21
import experimental.semmle.code.cpp.semantic.SemanticBound
23
22
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
@@ -204,14 +203,14 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
204
203
* A configuration to track flow from a pointer-arithmetic operation found
205
204
* by `AllocToInvalidPointerConf` to a dereference of the pointer.
206
205
*/
207
- class InvalidPointerToDerefConf extends DataFlow3 :: Configuration {
208
- InvalidPointerToDerefConf ( ) { this = "InvalidPointerToDerefConf" }
206
+ module InvalidPointerToDerefConfig implements DataFlow :: ConfigSig {
207
+ predicate isSource ( DataFlow :: Node source ) { invalidPointerToDerefSource ( _ , source , _ ) }
209
208
210
- override predicate isSource ( DataFlow:: Node source ) { invalidPointerToDerefSource ( _, source , _) }
211
-
212
- override predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
209
+ predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
213
210
}
214
211
212
+ module InvalidPointerToDerefFlow = DataFlow:: Make< InvalidPointerToDerefConfig > ;
213
+
215
214
/**
216
215
* Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
217
216
* pointer-value that is non-strictly upper bounded by `pai + delta`.
@@ -236,13 +235,13 @@ newtype TMergedPathNode =
236
235
// The path nodes computed by the first projection of `AllocToInvalidPointerConf`
237
236
TPathNode1 ( DataFlow:: PathNode p ) or
238
237
// The path nodes computed by `InvalidPointerToDerefConf`
239
- TPathNode3 ( DataFlow3 :: PathNode p ) or
238
+ TPathNode3 ( InvalidPointerToDerefFlow :: PathNode p ) or
240
239
// The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConf`.
241
240
// This one is needed because the sink identified by `InvalidPointerToDerefConf` is the
242
241
// pointer, but we want to raise an alert at the dereference.
243
242
TPathNodeSink ( Instruction i ) {
244
243
exists ( DataFlow:: Node n |
245
- any ( InvalidPointerToDerefConf conf ) . hasFlow ( _, n ) and
244
+ InvalidPointerToDerefFlow :: hasFlow ( _, n ) and
246
245
isInvalidPointerDerefSink ( n , i , _)
247
246
)
248
247
}
@@ -252,7 +251,7 @@ class MergedPathNode extends TMergedPathNode {
252
251
253
252
final DataFlow:: PathNode asPathNode1 ( ) { this = TPathNode1 ( result ) }
254
253
255
- final DataFlow3 :: PathNode asPathNode3 ( ) { this = TPathNode3 ( result ) }
254
+ final InvalidPointerToDerefFlow :: PathNode asPathNode3 ( ) { this = TPathNode3 ( result ) }
256
255
257
256
final Instruction asSinkNode ( ) { this = TPathNodeSink ( result ) }
258
257
@@ -280,7 +279,7 @@ class PathNode1 extends MergedPathNode, TPathNode1 {
280
279
281
280
class PathNode3 extends MergedPathNode , TPathNode3 {
282
281
override string toString ( ) {
283
- exists ( DataFlow3 :: PathNode p |
282
+ exists ( InvalidPointerToDerefFlow :: PathNode p |
284
283
this = TPathNode3 ( p ) and
285
284
result = p .toString ( )
286
285
)
@@ -324,7 +323,9 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
324
323
* Holds if `p1` is a sink of `AllocToInvalidPointerConf` and `p2` is a source
325
324
* of `InvalidPointerToDerefConf`, and they are connected through `pai`.
326
325
*/
327
- predicate joinOn1 ( PointerArithmeticInstruction pai , DataFlow:: PathNode p1 , DataFlow3:: PathNode p2 ) {
326
+ predicate joinOn1 (
327
+ PointerArithmeticInstruction pai , DataFlow:: PathNode p1 , InvalidPointerToDerefFlow:: PathNode p2
328
+ ) {
328
329
isSinkImpl ( pai , p1 .getNode ( ) , _, _) and
329
330
invalidPointerToDerefSource ( pai , p2 .getNode ( ) , _)
330
331
}
@@ -334,28 +335,29 @@ predicate joinOn1(PointerArithmeticInstruction pai, DataFlow::PathNode p1, DataF
334
335
* that dereferences `p1`. The string `operation` describes whether the `i` is
335
336
* a `StoreInstruction` or `LoadInstruction`.
336
337
*/
337
- predicate joinOn2 ( DataFlow3 :: PathNode p1 , Instruction i , string operation ) {
338
+ predicate joinOn2 ( InvalidPointerToDerefFlow :: PathNode p1 , Instruction i , string operation ) {
338
339
isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation )
339
340
}
340
341
341
342
predicate hasFlowPath (
342
- MergedPathNode source1 , MergedPathNode sink , DataFlow3 :: PathNode source3 ,
343
+ MergedPathNode source1 , MergedPathNode sink , InvalidPointerToDerefFlow :: PathNode source3 ,
343
344
PointerArithmeticInstruction pai , string operation
344
345
) {
345
346
exists (
346
- AllocToInvalidPointerConf conf1 , InvalidPointerToDerefConf conf2 , DataFlow3 :: PathNode sink3 ,
347
+ AllocToInvalidPointerConf conf1 , InvalidPointerToDerefFlow :: PathNode sink3 ,
347
348
DataFlow:: PathNode sink1
348
349
|
349
350
conf1 .hasFlowPath ( source1 .asPathNode1 ( ) , _, sink1 , _) and
350
351
joinOn1 ( pai , sink1 , source3 ) and
351
- conf2 . hasFlowPath ( source3 , sink3 ) and
352
+ InvalidPointerToDerefFlow :: hasFlowPath ( source3 , sink3 ) and
352
353
joinOn2 ( sink3 , sink .asSinkNode ( ) , operation )
353
354
)
354
355
}
355
356
356
357
from
357
- MergedPathNode source , MergedPathNode sink , int k , string kstr , DataFlow3:: PathNode source3 ,
358
- PointerArithmeticInstruction pai , string operation , Expr offset , DataFlow:: Node n
358
+ MergedPathNode source , MergedPathNode sink , int k , string kstr ,
359
+ InvalidPointerToDerefFlow:: PathNode source3 , PointerArithmeticInstruction pai , string operation ,
360
+ Expr offset , DataFlow:: Node n
359
361
where
360
362
hasFlowPath ( source , sink , source3 , pai , operation ) and
361
363
invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k ) and
0 commit comments