@@ -81,8 +81,8 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
8181 * ```
8282 *
8383 * We do this by splitting the task up into two configurations:
84- * 1. `AllocToInvalidPointerConf ` find flow from `malloc(size)` to `begin + size`, and
85- * 2. `InvalidPointerToDerefConf ` finds flow from `begin + size` to an `end` (on line 3).
84+ * 1. `AllocToInvalidPointerConfig ` find flow from `malloc(size)` to `begin + size`, and
85+ * 2. `InvalidPointerToDerefConfig ` finds flow from `begin + size` to an `end` (on line 3).
8686 *
8787 * Finally, the range-analysis library will find a load from (or store to) an address that
8888 * is non-strictly upper-bounded by `end` (which in this case is `*p`).
@@ -180,13 +180,13 @@ predicate isSinkImpl(
180180}
181181
182182/**
183- * Holds if `sink` is a sink for `InvalidPointerToDerefConf ` and `i` is a `StoreInstruction` that
183+ * Holds if `sink` is a sink for `InvalidPointerToDerefConfig ` and `i` is a `StoreInstruction` that
184184 * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
185185 * reads from an address that non-strictly upper-bounds `sink`.
186186 */
187187pragma [ inline]
188- predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation ) {
189- exists ( AddressOperand addr , int delta |
188+ predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation , int delta ) {
189+ exists ( AddressOperand addr |
190190 bounded1 ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
191191 delta >= 0 and
192192 i .getAnOperand ( ) = addr
@@ -201,13 +201,13 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
201201
202202/**
203203 * A configuration to track flow from a pointer-arithmetic operation found
204- * by `AllocToInvalidPointerConf ` to a dereference of the pointer.
204+ * by `AllocToInvalidPointerConfig ` to a dereference of the pointer.
205205 */
206206module InvalidPointerToDerefConfig implements DataFlow:: ConfigSig {
207207 predicate isSource ( DataFlow:: Node source ) { invalidPointerToDerefSource ( _, source , _) }
208208
209209 pragma [ inline]
210- predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
210+ predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _, _ ) }
211211
212212 predicate isBarrier ( DataFlow:: Node node ) {
213213 node = any ( DataFlow:: SsaPhiNode phi | not phi .isPhiRead ( ) ) .getAnInput ( true )
@@ -237,17 +237,17 @@ predicate invalidPointerToDerefSource(
237237}
238238
239239newtype TMergedPathNode =
240- // The path nodes computed by the first projection of `AllocToInvalidPointerConf `
240+ // The path nodes computed by the first projection of `AllocToInvalidPointerConfig `
241241 TPathNode1 ( AllocToInvalidPointerFlow:: PathNode1 p ) or
242- // The path nodes computed by `InvalidPointerToDerefConf `
242+ // The path nodes computed by `InvalidPointerToDerefConfig `
243243 TPathNode3 ( InvalidPointerToDerefFlow:: PathNode p ) or
244- // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConf `.
245- // This one is needed because the sink identified by `InvalidPointerToDerefConf ` is the
244+ // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConfig `.
245+ // This one is needed because the sink identified by `InvalidPointerToDerefConfig ` is the
246246 // pointer, but we want to raise an alert at the dereference.
247247 TPathNodeSink ( Instruction i ) {
248248 exists ( DataFlow:: Node n |
249249 InvalidPointerToDerefFlow:: flowTo ( n ) and
250- isInvalidPointerDerefSink ( n , i , _)
250+ isInvalidPointerDerefSink ( n , i , _, _ )
251251 )
252252 }
253253
@@ -321,7 +321,15 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
321321 or
322322 node1 .asPathNode3 ( ) .getASuccessor ( ) = node2 .asPathNode3 ( )
323323 or
324- joinOn2 ( node1 .asPathNode3 ( ) , node2 .asSinkNode ( ) , _)
324+ joinOn2 ( node1 .asPathNode3 ( ) , node2 .asSinkNode ( ) , _, _)
325+ }
326+
327+ query predicate nodes ( MergedPathNode n , string key , string val ) {
328+ AllocToInvalidPointerFlow:: PathGraph1:: nodes ( n .asPathNode1 ( ) , key , val )
329+ or
330+ InvalidPointerToDerefFlow:: PathGraph:: nodes ( n .asPathNode3 ( ) , key , val )
331+ or
332+ key = "semmle.label" and val = n .asSinkNode ( ) .toString ( )
325333}
326334
327335query predicate subpaths (
@@ -335,8 +343,8 @@ query predicate subpaths(
335343}
336344
337345/**
338- * Holds if `p1` is a sink of `AllocToInvalidPointerConf ` and `p2` is a source
339- * of `InvalidPointerToDerefConf `, and they are connected through `pai`.
346+ * Holds if `p1` is a sink of `AllocToInvalidPointerConfig ` and `p2` is a source
347+ * of `InvalidPointerToDerefConfig `, and they are connected through `pai`.
340348 */
341349predicate joinOn1 (
342350 PointerArithmeticInstruction pai , AllocToInvalidPointerFlow:: PathNode1 p1 ,
@@ -347,37 +355,37 @@ predicate joinOn1(
347355}
348356
349357/**
350- * Holds if `p1` is a sink of `InvalidPointerToDerefConf ` and `i` is the instruction
358+ * Holds if `p1` is a sink of `InvalidPointerToDerefConfig ` and `i` is the instruction
351359 * that dereferences `p1`. The string `operation` describes whether the `i` is
352360 * a `StoreInstruction` or `LoadInstruction`.
353361 */
354362pragma [ inline]
355- predicate joinOn2 ( InvalidPointerToDerefFlow:: PathNode p1 , Instruction i , string operation ) {
356- isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation )
363+ predicate joinOn2 ( InvalidPointerToDerefFlow:: PathNode p1 , Instruction i , string operation , int delta ) {
364+ isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation , delta )
357365}
358366
359367predicate hasFlowPath (
360368 MergedPathNode source1 , MergedPathNode sink , InvalidPointerToDerefFlow:: PathNode source3 ,
361- PointerArithmeticInstruction pai , string operation
369+ PointerArithmeticInstruction pai , string operation , int delta
362370) {
363371 exists ( InvalidPointerToDerefFlow:: PathNode sink3 , AllocToInvalidPointerFlow:: PathNode1 sink1 |
364372 AllocToInvalidPointerFlow:: flowPath ( source1 .asPathNode1 ( ) , _, sink1 , _) and
365373 joinOn1 ( pai , sink1 , source3 ) and
366374 InvalidPointerToDerefFlow:: flowPath ( source3 , sink3 ) and
367- joinOn2 ( sink3 , sink .asSinkNode ( ) , operation )
375+ joinOn2 ( sink3 , sink .asSinkNode ( ) , operation , delta )
368376 )
369377}
370378
371379from
372- MergedPathNode source , MergedPathNode sink , int k , string kstr ,
380+ MergedPathNode source , MergedPathNode sink , int k2 , int k3 , string kstr ,
373381 InvalidPointerToDerefFlow:: PathNode source3 , PointerArithmeticInstruction pai , string operation ,
374382 Expr offset , DataFlow:: Node n
375383where
376- hasFlowPath ( source , sink , source3 , pai , operation ) and
377- invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k ) and
384+ hasFlowPath ( source , sink , source3 , pai , operation , k3 ) and
385+ invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k2 ) and
378386 offset = pai .getRight ( ) .getUnconvertedResultExpression ( ) and
379387 n = source .asPathNode1 ( ) .getNode ( ) and
380- if k = 0 then kstr = "" else kstr = " + " + k
388+ if ( k2 + k3 ) = 0 then kstr = "" else kstr = " + " + ( k2 + k3 )
381389select sink , source , sink ,
382390 "This " + operation + " might be out of bounds, as the pointer might be equal to $@ + $@" + kstr +
383391 "." , n , n .toString ( ) , offset , offset .toString ( )
0 commit comments