@@ -233,7 +233,7 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
233
233
state .getConcreteBitsize ( ) =
234
234
min ( int bitsize |
235
235
bitsize = validBitsize ( ) and
236
- f ( effectiveBitSize , ip .isSigned ( ) , 64 ) <= state . getConcreteBitsize ( )
236
+ f ( effectiveBitSize , ip .isSigned ( ) , 64 ) <= bitsize
237
237
|
238
238
bitsize
239
239
)
@@ -248,16 +248,25 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
248
248
*/
249
249
additional predicate isSink2 ( DataFlow:: TypeCastNode sink , FlowState state ) {
250
250
sink .asExpr ( ) instanceof ConversionExpr and
251
- exists ( IntegerType integerType | sink .getResultType ( ) .getUnderlyingType ( ) = integerType |
251
+ exists ( IntegerType integerType , int sinkBitsize , boolean sinkIsSigned |
252
+ sink .getResultType ( ) .getUnderlyingType ( ) = integerType and
252
253
(
253
- state . getBitSize ( ) = integerType .getSize ( )
254
+ sinkBitsize = integerType .getSize ( )
254
255
or
255
256
not exists ( integerType .getSize ( ) ) and
256
- state . getBitSize ( ) = getIntTypeBitSize ( sink .getFile ( ) , 0 )
257
+ sinkBitsize = getIntTypeBitSize ( sink .getFile ( ) , 0 )
257
258
) and
258
- if integerType instanceof SignedIntegerType
259
- then state .getIsSigned ( ) = true
260
- else state .getIsSigned ( ) = false
259
+ if integerType instanceof SignedIntegerType then sinkIsSigned = true else sinkIsSigned = false
260
+ |
261
+ // Flow state has a concrete value
262
+ f ( sinkBitsize , sinkIsSigned , 32 ) < state .getConcreteBitsize ( )
263
+ or
264
+ // Flow state has an architecture-independent value
265
+ exists ( boolean signed | signed = state .getArchictureDependentSignedness ( ) |
266
+ if sinkBitsize = 0
267
+ then sinkIsSigned = true and signed = false
268
+ else f ( sinkBitsize , sinkIsSigned , 32 ) < f ( 0 , signed , 64 )
269
+ )
261
270
) and
262
271
not exists ( ShrExpr shrExpr |
263
272
shrExpr .getLeftOperand ( ) .getGlobalValueNumber ( ) =
@@ -276,16 +285,42 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
276
285
}
277
286
278
287
predicate isBarrier ( DataFlow:: Node node , FlowState state ) {
288
+ isUpperBoundCheckBarrier ( node , state , _)
289
+ or
290
+ isSink2 ( node , state )
291
+ }
292
+
293
+ additional predicate isUpperBoundCheckBarrier (
294
+ DataFlow:: Node node , FlowState state , UpperBoundCheckGuard g
295
+ ) {
279
296
// To catch flows that only happen on 32-bit architectures we consider an
280
297
// architecture-dependent sink bit size to be 32.
281
- exists ( UpperBoundCheckGuard g , int effectiveSinkBitSize |
282
- effectiveSinkBitSize = replaceZeroWith ( state .getBitSize ( ) , 32 )
298
+ exists ( int effectiveSinkBitSize |
299
+ effectiveSinkBitSize = state .getConcreteBitsize ( ) or
300
+ effectiveSinkBitSize = f ( 0 , state .getArchictureDependentSignedness ( ) , 32 )
283
301
|
284
302
node = DataFlow:: BarrierGuard< upperBoundCheckGuard / 3 > :: getABarrierNodeForGuard ( g ) and
285
- g .isBoundFor ( effectiveSinkBitSize , state .getIsSigned ( ) )
303
+ // use `false` for `isSigned` as we have already subtracted 1 from
304
+ // `effectiveSinkBitSize` if necessary
305
+ g .isBoundFor2 ( effectiveSinkBitSize )
306
+ )
307
+ }
308
+
309
+ predicate isAdditionalFlowStep (
310
+ DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
311
+ ) {
312
+ exists ( UpperBoundCheckGuard g |
313
+ isUpperBoundCheckBarrier ( node1 , state1 , g ) and
314
+ node2 = node1 .getASuccessor ( ) and
315
+ state2 .getConcreteBitsize ( ) =
316
+ max ( int bitsize |
317
+ bitsize = validBitsize ( ) and
318
+ bitsize < state1 .getConcreteBitsize ( ) and
319
+ not g .isBoundFor2 ( bitsize )
320
+ |
321
+ bitsize
322
+ )
286
323
)
287
- or
288
- isSink2 ( node , state )
289
324
}
290
325
}
291
326
@@ -337,6 +372,33 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
337
372
)
338
373
}
339
374
375
+ predicate isBoundFor2 ( int bitSize ) {
376
+ bitSize = [ 7 , 8 , 15 , 16 , 31 , 32 , 63 , 64 ] and
377
+ exists ( float bound , float strictnessOffset |
378
+ // For `x < c` the bound is `c-1`. For `x >= c` we will be an upper bound
379
+ // on the `branch` argument of `checks` is false, which is equivalent to
380
+ // `x < c`.
381
+ if expr instanceof LssExpr or expr instanceof GeqExpr
382
+ then strictnessOffset = 1
383
+ else strictnessOffset = 0
384
+ |
385
+ (
386
+ bound = expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( )
387
+ or
388
+ exists ( DeclaredConstant maxint | maxint .hasQualifiedName ( "math" , "MaxInt" ) |
389
+ expr .getAnOperand ( ) = maxint .getAReference ( ) and
390
+ bound = getMaxIntValue ( 32 , true )
391
+ )
392
+ or
393
+ exists ( DeclaredConstant maxuint | maxuint .hasQualifiedName ( "math" , "MaxUint" ) |
394
+ expr .getAnOperand ( ) = maxuint .getAReference ( ) and
395
+ bound = getMaxIntValue ( 32 , false )
396
+ )
397
+ ) and
398
+ bound - strictnessOffset <= 2 .pow ( bitSize ) - 1
399
+ )
400
+ }
401
+
340
402
/** Holds if this guard validates `e` upon evaluating to `branch`. */
341
403
predicate checks ( Expr e , boolean branch ) {
342
404
this .leq ( branch , DataFlow:: exprNode ( e ) , _, _) and
0 commit comments