1717
1818import cpp
1919import experimental.semmle.code.cpp.dataflow.ProductFlow
20- import semmle.code.cpp.ir.dataflow.DataFlow3
2120import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
2221import experimental.semmle.code.cpp.semantic.SemanticBound
2322import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
@@ -204,14 +203,14 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
204203 * A configuration to track flow from a pointer-arithmetic operation found
205204 * by `AllocToInvalidPointerConf` to a dereference of the pointer.
206205 */
207- class InvalidPointerToDerefConf extends DataFlow3 :: Configuration {
208- InvalidPointerToDerefConf ( ) { this = "InvalidPointerToDerefConf" }
206+ module InvalidPointerToDerefConfig implements DataFlow :: ConfigSig {
207+ predicate isSource ( DataFlow :: Node source ) { invalidPointerToDerefSource ( _ , source , _ ) }
209208
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 , _, _) }
213210}
214211
212+ module InvalidPointerToDerefFlow = DataFlow:: Make< InvalidPointerToDerefConfig > ;
213+
215214/**
216215 * Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
217216 * pointer-value that is non-strictly upper bounded by `pai + delta`.
@@ -236,13 +235,13 @@ newtype TMergedPathNode =
236235 // The path nodes computed by the first projection of `AllocToInvalidPointerConf`
237236 TPathNode1 ( DataFlow:: PathNode p ) or
238237 // The path nodes computed by `InvalidPointerToDerefConf`
239- TPathNode3 ( DataFlow3 :: PathNode p ) or
238+ TPathNode3 ( InvalidPointerToDerefFlow :: PathNode p ) or
240239 // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConf`.
241240 // This one is needed because the sink identified by `InvalidPointerToDerefConf` is the
242241 // pointer, but we want to raise an alert at the dereference.
243242 TPathNodeSink ( Instruction i ) {
244243 exists ( DataFlow:: Node n |
245- any ( InvalidPointerToDerefConf conf ) . hasFlow ( _, n ) and
244+ InvalidPointerToDerefFlow :: hasFlow ( _, n ) and
246245 isInvalidPointerDerefSink ( n , i , _)
247246 )
248247 }
@@ -252,7 +251,7 @@ class MergedPathNode extends TMergedPathNode {
252251
253252 final DataFlow:: PathNode asPathNode1 ( ) { this = TPathNode1 ( result ) }
254253
255- final DataFlow3 :: PathNode asPathNode3 ( ) { this = TPathNode3 ( result ) }
254+ final InvalidPointerToDerefFlow :: PathNode asPathNode3 ( ) { this = TPathNode3 ( result ) }
256255
257256 final Instruction asSinkNode ( ) { this = TPathNodeSink ( result ) }
258257
@@ -280,7 +279,7 @@ class PathNode1 extends MergedPathNode, TPathNode1 {
280279
281280class PathNode3 extends MergedPathNode , TPathNode3 {
282281 override string toString ( ) {
283- exists ( DataFlow3 :: PathNode p |
282+ exists ( InvalidPointerToDerefFlow :: PathNode p |
284283 this = TPathNode3 ( p ) and
285284 result = p .toString ( )
286285 )
@@ -324,7 +323,9 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
324323 * Holds if `p1` is a sink of `AllocToInvalidPointerConf` and `p2` is a source
325324 * of `InvalidPointerToDerefConf`, and they are connected through `pai`.
326325 */
327- predicate joinOn1 ( PointerArithmeticInstruction pai , DataFlow:: PathNode p1 , DataFlow3:: PathNode p2 ) {
326+ predicate joinOn1 (
327+ PointerArithmeticInstruction pai , DataFlow:: PathNode p1 , InvalidPointerToDerefFlow:: PathNode p2
328+ ) {
328329 isSinkImpl ( pai , p1 .getNode ( ) , _, _) and
329330 invalidPointerToDerefSource ( pai , p2 .getNode ( ) , _)
330331}
@@ -334,28 +335,29 @@ predicate joinOn1(PointerArithmeticInstruction pai, DataFlow::PathNode p1, DataF
334335 * that dereferences `p1`. The string `operation` describes whether the `i` is
335336 * a `StoreInstruction` or `LoadInstruction`.
336337 */
337- predicate joinOn2 ( DataFlow3 :: PathNode p1 , Instruction i , string operation ) {
338+ predicate joinOn2 ( InvalidPointerToDerefFlow :: PathNode p1 , Instruction i , string operation ) {
338339 isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation )
339340}
340341
341342predicate hasFlowPath (
342- MergedPathNode source1 , MergedPathNode sink , DataFlow3 :: PathNode source3 ,
343+ MergedPathNode source1 , MergedPathNode sink , InvalidPointerToDerefFlow :: PathNode source3 ,
343344 PointerArithmeticInstruction pai , string operation
344345) {
345346 exists (
346- AllocToInvalidPointerConf conf1 , InvalidPointerToDerefConf conf2 , DataFlow3 :: PathNode sink3 ,
347+ AllocToInvalidPointerConf conf1 , InvalidPointerToDerefFlow :: PathNode sink3 ,
347348 DataFlow:: PathNode sink1
348349 |
349350 conf1 .hasFlowPath ( source1 .asPathNode1 ( ) , _, sink1 , _) and
350351 joinOn1 ( pai , sink1 , source3 ) and
351- conf2 . hasFlowPath ( source3 , sink3 ) and
352+ InvalidPointerToDerefFlow :: hasFlowPath ( source3 , sink3 ) and
352353 joinOn2 ( sink3 , sink .asSinkNode ( ) , operation )
353354 )
354355}
355356
356357from
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
359361where
360362 hasFlowPath ( source , sink , source3 , pai , operation ) and
361363 invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k ) and
0 commit comments