1
1
import go
2
2
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
+ }
14
46
}
15
47
16
48
/**
@@ -204,7 +236,7 @@ private class MaxValueState extends TMaxValueState {
204
236
predicate architectureBitSizeUnknown ( ) { this .architectureBitSize ( ) .isUnknown ( ) }
205
237
206
238
/**
207
- * Gets the bitsize we should use for a sink.
239
+ * Gets the bitsize we should use for a sink of type `uint` .
208
240
*
209
241
* If the architecture bit size is known, then we should use that. Otherwise,
210
242
* 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)
257
289
/** An upper bound check that compares a variable to a constant value. */
258
290
class UpperBoundCheckGuard extends DataFlow:: RelationalComparisonNode {
259
291
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.
260
295
count ( expr .getAnOperand ( ) .getExactValue ( ) ) = 1 and
261
296
expr .getAnOperand ( ) .getType ( ) .getUnderlyingType ( ) instanceof IntegerType
262
297
}
263
298
264
299
/**
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`.
269
313
*
270
314
* Note that we have to use floats here because integers in CodeQL are
271
315
* represented by 32-bit signed integers, which cannot represent some of the
@@ -274,25 +318,25 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
274
318
predicate isBoundFor ( int bitSize , int architectureBitSize ) {
275
319
bitSize = validBitSize ( ) and
276
320
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`.
281
328
if expr instanceof LssExpr or expr instanceof GeqExpr
282
329
then strictnessOffset = 1
283
330
else strictnessOffset = 0
284
331
|
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
296
340
)
297
341
}
298
342
@@ -316,7 +360,7 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
316
360
* _ = uint16(parsed)
317
361
* }
318
362
* ```
319
- * `parsed < math.MaxInt16` is an `UpperBoundCheckGuard` and `uint16(parsed)`
363
+ * `parsed <= math.MaxInt16` is an `UpperBoundCheckGuard` and `uint16(parsed)`
320
364
* is an `UpperBoundCheck` that would be a barrier for flow states with bit
321
365
* size greater than 15 and would transform them to a flow state with bit size
322
366
* 15 and the same architecture bit size.
0 commit comments