@@ -228,6 +228,83 @@ abstract class BarrierFlowStateTransformer extends DataFlow::Node {
228228 abstract MaxValueState transform ( MaxValueState flowstate ) ;
229229}
230230
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+
231308/**
232309 * A node that is safely guarded by an `UpperBoundCheckGuard`.
233310 *
@@ -385,83 +462,6 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
385462 */
386463module Flow = TaintTracking:: GlobalWithState< ConversionWithoutBoundsCheckConfig > ;
387464
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-
465465/** Gets a string describing the size of the integer parsed. */
466466deprecated string describeBitSize ( int bitSize , int intTypeBitSize ) {
467467 intTypeBitSize in [ 0 , 32 , 64 ] and
0 commit comments