@@ -228,6 +228,83 @@ abstract class BarrierFlowStateTransformer extends DataFlow::Node {
228
228
abstract MaxValueState transform ( MaxValueState flowstate ) ;
229
229
}
230
230
231
+ private predicate upperBoundCheckGuard ( DataFlow:: Node g , Expr e , boolean branch ) {
232
+ g .( UpperBoundCheckGuard ) .checks ( e , branch )
233
+ }
234
+
235
+ /** An upper bound check that compares a variable to a constant value. */
236
+ class UpperBoundCheckGuard extends DataFlow:: RelationalComparisonNode {
237
+ UpperBoundCheckGuard ( ) {
238
+ count ( expr .getAnOperand ( ) .getExactValue ( ) ) = 1 and
239
+ expr .getAnOperand ( ) .getType ( ) .getUnderlyingType ( ) instanceof IntegerType
240
+ }
241
+
242
+ /**
243
+ * Holds if the upper bound check ensures the non-constant operand is less
244
+ * than or equal to the maximum value for `bitSize` and `isSigned`. In this
245
+ * case, the upper bound check is a barrier guard.
246
+ */
247
+ deprecated predicate isBoundFor ( int bitSize , boolean isSigned ) {
248
+ bitSize = [ 8 , 16 , 32 ] and
249
+ exists ( float bound , float strictnessOffset |
250
+ // For `x < c` the bound is `c-1`. For `x >= c` we will be an upper bound
251
+ // on the `branch` argument of `checks` is false, which is equivalent to
252
+ // `x < c`.
253
+ if expr instanceof LssExpr or expr instanceof GeqExpr
254
+ then strictnessOffset = 1
255
+ else strictnessOffset = 0
256
+ |
257
+ exists ( DeclaredConstant maxint , DeclaredConstant maxuint |
258
+ maxint .hasQualifiedName ( "math" , "MaxInt" ) and maxuint .hasQualifiedName ( "math" , "MaxUint" )
259
+ |
260
+ if expr .getAnOperand ( ) = maxint .getAReference ( )
261
+ then bound = getMaxIntValue ( 32 , true )
262
+ else
263
+ if expr .getAnOperand ( ) = maxuint .getAReference ( )
264
+ then bound = getMaxIntValue ( 32 , false )
265
+ else bound = expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( )
266
+ ) and
267
+ bound - strictnessOffset <= getMaxIntValue ( bitSize , isSigned )
268
+ )
269
+ }
270
+
271
+ /**
272
+ * Holds if this upper bound check ensures the non-constant operand is less
273
+ * than or equal to `2^(bitsize) - 1`. In this case, the upper bound check
274
+ * is a barrier guard.
275
+ */
276
+ predicate isBoundFor2 ( int bitSize , int architectureBitSize ) {
277
+ bitSize = validBitSize ( ) and
278
+ architectureBitSize = [ 32 , 64 ] and
279
+ exists ( float bound , float strictnessOffset |
280
+ // For `x < c` the bound is `c-1`. For `x >= c` we will be an upper bound
281
+ // on the `branch` argument of `checks` is false, which is equivalent to
282
+ // `x < c`.
283
+ if expr instanceof LssExpr or expr instanceof GeqExpr
284
+ then strictnessOffset = 1
285
+ else strictnessOffset = 0
286
+ |
287
+ exists ( DeclaredConstant maxint , DeclaredConstant maxuint |
288
+ maxint .hasQualifiedName ( "math" , "MaxInt" ) and maxuint .hasQualifiedName ( "math" , "MaxUint" )
289
+ |
290
+ if expr .getAnOperand ( ) = maxint .getAReference ( )
291
+ then bound = getMaxIntValue ( architectureBitSize , true )
292
+ else
293
+ if expr .getAnOperand ( ) = maxuint .getAReference ( )
294
+ then bound = getMaxIntValue ( architectureBitSize , false )
295
+ else bound = expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( )
296
+ ) and
297
+ bound - strictnessOffset < 2 .pow ( bitSize ) - 1
298
+ )
299
+ }
300
+
301
+ /** Holds if this guard validates `e` upon evaluating to `branch`. */
302
+ predicate checks ( Expr e , boolean branch ) {
303
+ this .leq ( branch , DataFlow:: exprNode ( e ) , _, _) and
304
+ not e .isConst ( )
305
+ }
306
+ }
307
+
231
308
/**
232
309
* A node that is safely guarded by an `UpperBoundCheckGuard`.
233
310
*
@@ -385,83 +462,6 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
385
462
*/
386
463
module Flow = TaintTracking:: GlobalWithState< ConversionWithoutBoundsCheckConfig > ;
387
464
388
- private predicate upperBoundCheckGuard ( DataFlow:: Node g , Expr e , boolean branch ) {
389
- g .( UpperBoundCheckGuard ) .checks ( e , branch )
390
- }
391
-
392
- /** An upper bound check that compares a variable to a constant value. */
393
- class UpperBoundCheckGuard extends DataFlow:: RelationalComparisonNode {
394
- UpperBoundCheckGuard ( ) {
395
- count ( expr .getAnOperand ( ) .getExactValue ( ) ) = 1 and
396
- expr .getAnOperand ( ) .getType ( ) .getUnderlyingType ( ) instanceof IntegerType
397
- }
398
-
399
- /**
400
- * Holds if the upper bound check ensures the non-constant operand is less
401
- * than or equal to the maximum value for `bitSize` and `isSigned`. In this
402
- * case, the upper bound check is a barrier guard.
403
- */
404
- deprecated predicate isBoundFor ( int bitSize , boolean isSigned ) {
405
- bitSize = [ 8 , 16 , 32 ] and
406
- exists ( float bound , float strictnessOffset |
407
- // For `x < c` the bound is `c-1`. For `x >= c` we will be an upper bound
408
- // on the `branch` argument of `checks` is false, which is equivalent to
409
- // `x < c`.
410
- if expr instanceof LssExpr or expr instanceof GeqExpr
411
- then strictnessOffset = 1
412
- else strictnessOffset = 0
413
- |
414
- exists ( DeclaredConstant maxint , DeclaredConstant maxuint |
415
- maxint .hasQualifiedName ( "math" , "MaxInt" ) and maxuint .hasQualifiedName ( "math" , "MaxUint" )
416
- |
417
- if expr .getAnOperand ( ) = maxint .getAReference ( )
418
- then bound = getMaxIntValue ( 32 , true )
419
- else
420
- if expr .getAnOperand ( ) = maxuint .getAReference ( )
421
- then bound = getMaxIntValue ( 32 , false )
422
- else bound = expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( )
423
- ) and
424
- bound - strictnessOffset <= getMaxIntValue ( bitSize , isSigned )
425
- )
426
- }
427
-
428
- /**
429
- * Holds if this upper bound check ensures the non-constant operand is less
430
- * than or equal to `2^(bitsize) - 1`. In this case, the upper bound check
431
- * is a barrier guard.
432
- */
433
- predicate isBoundFor2 ( int bitSize , int architectureBitSize ) {
434
- bitSize = validBitSize ( ) and
435
- architectureBitSize = [ 32 , 64 ] and
436
- exists ( float bound , float strictnessOffset |
437
- // For `x < c` the bound is `c-1`. For `x >= c` we will be an upper bound
438
- // on the `branch` argument of `checks` is false, which is equivalent to
439
- // `x < c`.
440
- if expr instanceof LssExpr or expr instanceof GeqExpr
441
- then strictnessOffset = 1
442
- else strictnessOffset = 0
443
- |
444
- exists ( DeclaredConstant maxint , DeclaredConstant maxuint |
445
- maxint .hasQualifiedName ( "math" , "MaxInt" ) and maxuint .hasQualifiedName ( "math" , "MaxUint" )
446
- |
447
- if expr .getAnOperand ( ) = maxint .getAReference ( )
448
- then bound = getMaxIntValue ( architectureBitSize , true )
449
- else
450
- if expr .getAnOperand ( ) = maxuint .getAReference ( )
451
- then bound = getMaxIntValue ( architectureBitSize , false )
452
- else bound = expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( )
453
- ) and
454
- bound - strictnessOffset < 2 .pow ( bitSize ) - 1
455
- )
456
- }
457
-
458
- /** Holds if this guard validates `e` upon evaluating to `branch`. */
459
- predicate checks ( Expr e , boolean branch ) {
460
- this .leq ( branch , DataFlow:: exprNode ( e ) , _, _) and
461
- not e .isConst ( )
462
- }
463
- }
464
-
465
465
/** Gets a string describing the size of the integer parsed. */
466
466
deprecated string describeBitSize ( int bitSize , int intTypeBitSize ) {
467
467
intTypeBitSize in [ 0 , 32 , 64 ] and
0 commit comments