mirror of
https://github.com/github/codeql.git
synced 2025-12-21 19:26:31 +01:00
112 lines
2.5 KiB
Plaintext
112 lines
2.5 KiB
Plaintext
/**
|
|
* Provides basic arithmetic operations that have no result if their result
|
|
* would overflow a 32-bit two's complement integer.
|
|
*/
|
|
|
|
/**
|
|
* Gets the value of the maximum representable integer.
|
|
*/
|
|
int maxValue() { result = 2147483647 }
|
|
|
|
/**
|
|
* Gets the value of the minimum representable integer.
|
|
*/
|
|
int minValue() { result = -2147483648 }
|
|
|
|
/**
|
|
* Holds if the value `f` is within the range of representable integers.
|
|
*/
|
|
bindingset[f]
|
|
pragma[inline]
|
|
private predicate isRepresentable(float f) { f >= minValue() and f <= maxValue() }
|
|
|
|
/**
|
|
* Returns `a + b`. If the addition overflows, there is no result.
|
|
*/
|
|
bindingset[a, b]
|
|
int add(int a, int b) {
|
|
isRepresentable(a.(float) + b.(float)) and
|
|
result = a + b
|
|
}
|
|
|
|
/**
|
|
* Returns `a - b`. If the subtraction overflows, there is no result.
|
|
*/
|
|
bindingset[a, b]
|
|
int sub(int a, int b) {
|
|
isRepresentable(a.(float) - b.(float)) and
|
|
result = a - b
|
|
}
|
|
|
|
/**
|
|
* Returns `a * b`. If the multiplication overflows, there is no result. If
|
|
* either input is not given, and the other input is non-zero, there is no
|
|
* result.
|
|
*/
|
|
bindingset[a, b]
|
|
int mul(int a, int b) {
|
|
a = 0 and
|
|
result = 0
|
|
or
|
|
b = 0 and
|
|
result = 0
|
|
or
|
|
isRepresentable(a.(float) * b.(float)) and
|
|
result = a * b
|
|
}
|
|
|
|
/**
|
|
* Returns `a / b`. If the division overflows, there is no result.
|
|
*/
|
|
bindingset[a, b]
|
|
int div(int a, int b) {
|
|
b != 0 and
|
|
(a != minValue() or b != -1) and
|
|
result = a / b
|
|
}
|
|
|
|
/** Returns `a == b`. */
|
|
bindingset[a, b]
|
|
int compareEQ(int a, int b) { if a = b then result = 1 else result = 0 }
|
|
|
|
/** Returns `a != b`. */
|
|
bindingset[a, b]
|
|
int compareNE(int a, int b) { if a != b then result = 1 else result = 0 }
|
|
|
|
/** Returns `a < b`. */
|
|
bindingset[a, b]
|
|
int compareLT(int a, int b) { if a < b then result = 1 else result = 0 }
|
|
|
|
/** Returns `a > b`. */
|
|
bindingset[a, b]
|
|
int compareGT(int a, int b) { if a > b then result = 1 else result = 0 }
|
|
|
|
/** Returns `a <= b`. */
|
|
bindingset[a, b]
|
|
int compareLE(int a, int b) { if a <= b then result = 1 else result = 0 }
|
|
|
|
/** Returns `a >= b`. */
|
|
bindingset[a, b]
|
|
int compareGE(int a, int b) { if a >= b then result = 1 else result = 0 }
|
|
|
|
/** Returns `a | b`. */
|
|
bindingset[a, b]
|
|
int bitOr(int a, int b) { result = a.bitOr(b) }
|
|
|
|
/** Returns `a & b`. */
|
|
bindingset[a, b]
|
|
int bitAnd(int a, int b) { result = a.bitAnd(b) }
|
|
|
|
/** Returns `a ^ b`. */
|
|
bindingset[a, b]
|
|
int bitXor(int a, int b) { result = a.bitXor(b) }
|
|
|
|
/**
|
|
* Returns `-a`. If the negation would overflow, there is no result.
|
|
*/
|
|
bindingset[a]
|
|
int neg(int a) {
|
|
a != minValue() and
|
|
result = -a
|
|
}
|