11import go
22
3- /**
4- * Gets the maximum value of an integer (signed if `isSigned`
5- * is true, unsigned otherwise) with `bitSize` bits.
6- */
7- float getMaxIntValue ( int bitSize , boolean isSigned ) {
8- bitSize in [ 8 , 16 , 32 ] and
9- (
10- isSigned = true and result = 2 .pow ( bitSize - 1 ) - 1
11- or
12- isSigned = false and result = 2 .pow ( bitSize ) - 1
13- )
3+ /** The constant `math.MaxInt` or the constant `math.MaxUint`. */
4+ abstract private class MaxIntOrMaxUint extends DeclaredConstant {
5+ /**
6+ * Gets the (binary) order of magnitude when the architecture has bit size
7+ * `architectureBitSize`, which is defined to be the integer `x` such that
8+ * `2.pow(x) - 1` is the value of this constant.
9+ */
10+ abstract int getOrder ( int architectureBitSize ) ;
11+
12+ /**
13+ * Holds if the value of this constant given `architectureBitSize` minus
14+ * `strictnessOffset` is less than or equal to `2.pow(b) - 1`.
15+ */
16+ predicate isBoundFor ( int b , int architectureBitSize , float strictnessOffset ) {
17+ // 2.pow(x) - 1 - strictnessOffset <= 2.pow(b) - 1
18+ exists ( int x |
19+ x = this .getOrder ( architectureBitSize ) and
20+ b = validBitSize ( ) and
21+ (
22+ strictnessOffset = 0 and x <= b
23+ or
24+ strictnessOffset = 1 and x <= b - 1
25+ )
26+ )
27+ }
28+ }
29+
30+ /** The constant `math.MaxInt`. */
31+ private class MaxInt extends MaxIntOrMaxUint {
32+ MaxInt ( ) { this .hasQualifiedName ( "math" , "MaxInt" ) }
33+
34+ override int getOrder ( int architectureBitSize ) {
35+ architectureBitSize = [ 32 , 64 ] and result = architectureBitSize - 1
36+ }
37+ }
38+
39+ /** The constant `math.MaxUint`. */
40+ private class MaxUint extends MaxIntOrMaxUint {
41+ MaxUint ( ) { this .hasQualifiedName ( "math" , "MaxUint" ) }
42+
43+ override int getOrder ( int architectureBitSize ) {
44+ architectureBitSize = [ 32 , 64 ] and result = architectureBitSize
45+ }
1446}
1547
1648/**
@@ -204,7 +236,7 @@ private class MaxValueState extends TMaxValueState {
204236 predicate architectureBitSizeUnknown ( ) { this .architectureBitSize ( ) .isUnknown ( ) }
205237
206238 /**
207- * Gets the bitsize we should use for a sink.
239+ * Gets the bitsize we should use for a sink of type `uint` .
208240 *
209241 * If the architecture bit size is known, then we should use that. Otherwise,
210242 * we should use 32 bits, because that will find results that only exist on
@@ -257,15 +289,27 @@ private predicate upperBoundCheckGuard(DataFlow::Node g, Expr e, boolean branch)
257289/** An upper bound check that compares a variable to a constant value. */
258290class UpperBoundCheckGuard extends DataFlow:: RelationalComparisonNode {
259291 UpperBoundCheckGuard ( ) {
292+ // Note that even though `x > c` and `x >= c` do not look like upper bound
293+ // checks, on the branches where they are false the conditions are `x <= c`
294+ // and `x < c` respectively, which are upper bound checks.
260295 count ( expr .getAnOperand ( ) .getExactValue ( ) ) = 1 and
261296 expr .getAnOperand ( ) .getType ( ) .getUnderlyingType ( ) instanceof IntegerType
262297 }
263298
264299 /**
265- * Holds if this upper bound check ensures the non-constant operand is less
266- * than or equal to `2^(bitsize) - 1`. In this case, the upper bound check
267- * is a barrier guard. `architectureBitSize` is used if the constant operand
268- * is `math.MaxInt` or `math.MaxUint`.
300+ * Holds if this upper bound check should stop flow for a flow state with bit
301+ * size `bitSize` and architecture bit size `architectureBitSize`.
302+ *
303+ * A flow state has bit size `bitSize` if that is the smallest valid bit size
304+ * `b` such that the maximum value that could get to that point is less than
305+ * or equal to `2^(b) - 1`. So the flow should be stopped if there is a valid
306+ * bit size `b` which is less than `bitSize` such that the maximum value that
307+ * could get to that point is than or equal to `2^(b) - 1`. In this case,
308+ * the upper bound check is a barrier guard, because the flow should have bit
309+ * size equal to the smallest such `b` instead of `bitSize`.
310+ *
311+ * The argument `architectureBitSize` is only used if the constant operand is
312+ * `math.MaxInt` or `math.MaxUint`.
269313 *
270314 * Note that we have to use floats here because integers in CodeQL are
271315 * represented by 32-bit signed integers, which cannot represent some of the
@@ -274,25 +318,25 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
274318 predicate isBoundFor ( int bitSize , int architectureBitSize ) {
275319 bitSize = validBitSize ( ) and
276320 architectureBitSize = [ 32 , 64 ] and
277- exists ( float bound , float strictnessOffset |
278- // For `x < c` the bound is `c-1`. For `x >= c` we will be an upper bound
279- // on the `branch` argument of `checks` is false, which is equivalent to
280- // `x < c`.
321+ exists ( int b , float strictnessOffset |
322+ // It is sufficient to check for the next valid bit size below `bitSize`.
323+ b = max ( int a | a = validBitSize ( ) and a < bitSize ) and
324+ // We will use the format `x <= c - strictnessOffset`. Since `x < c` is
325+ // the same as `x <= c-1`, we set `strictnessOffset` to 1 in this case.
326+ // For `x >= c` we will be dealing with the case where the `branch`
327+ // argument of `checks` is false, which is equivalent to `x < c`.
281328 if expr instanceof LssExpr or expr instanceof GeqExpr
282329 then strictnessOffset = 1
283330 else strictnessOffset = 0
284331 |
285- exists ( DeclaredConstant maxint , DeclaredConstant maxuint |
286- maxint .hasQualifiedName ( "math" , "MaxInt" ) and maxuint .hasQualifiedName ( "math" , "MaxUint" )
287- |
288- if expr .getAnOperand ( ) = maxint .getAReference ( )
289- then bound = getMaxIntValue ( architectureBitSize , true )
290- else
291- if expr .getAnOperand ( ) = maxuint .getAReference ( )
292- then bound = getMaxIntValue ( architectureBitSize , false )
293- else bound = expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( )
294- ) and
295- bound - strictnessOffset < 2 .pow ( bitSize ) - 1
332+ if expr .getAnOperand ( ) = any ( MaxIntOrMaxUint m ) .getAReference ( )
333+ then
334+ any ( MaxIntOrMaxUint m | expr .getAnOperand ( ) = m .getAReference ( ) )
335+ .isBoundFor ( b , architectureBitSize , strictnessOffset )
336+ else
337+ // We want `x <= c - strictnessOffset` to guarantee that `x <= 2^b - 1`,
338+ // which is equivalent to saying `c - strictnessOffset <= 2^b - 1`.
339+ expr .getAnOperand ( ) .getExactValue ( ) .toFloat ( ) - strictnessOffset <= 2 .pow ( b ) - 1
296340 )
297341 }
298342
@@ -316,7 +360,7 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
316360 * _ = uint16(parsed)
317361 * }
318362 * ```
319- * `parsed < math.MaxInt16` is an `UpperBoundCheckGuard` and `uint16(parsed)`
363+ * `parsed <= math.MaxInt16` is an `UpperBoundCheckGuard` and `uint16(parsed)`
320364 * is an `UpperBoundCheck` that would be a barrier for flow states with bit
321365 * size greater than 15 and would transform them to a flow state with bit size
322366 * 15 and the same architecture bit size.
0 commit comments