Skip to content

Commit

Permalink
SimpleRangeAnalysis src/: float -> BigInt
Browse files Browse the repository at this point in the history
  • Loading branch information
d10c committed Jul 1, 2024
1 parent 13a3d9a commit 5c8a160
Show file tree
Hide file tree
Showing 9 changed files with 94 additions and 75 deletions.
11 changes: 6 additions & 5 deletions cpp/ql/src/Critical/OverflowStatic.ql
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,8 @@ predicate overflowOffsetInLoop(BufferAccess bufaccess, string msg) {
loop.limit() >= bufaccess.bufferSize() and
loop.counter().getAnAccess() = bufaccess.getArrayOffset() and
// Ensure that we don't have an upper bound on the array index that's less than the buffer size.
not upperBound(bufaccess.getArrayOffset().getFullyConverted()) < bufaccess.bufferSize() and
not upperBound(bufaccess.getArrayOffset().getFullyConverted()) <
bufaccess.bufferSize().toBigInt() and
// The upper bounds analysis must not have been widended
not upperBoundMayBeWidened(bufaccess.getArrayOffset().getFullyConverted()) and
msg =
Expand Down Expand Up @@ -101,24 +102,24 @@ class CallWithBufferSize extends FunctionCall {
)
}

int statedSizeValue() {
QlBuiltins::BigInt statedSizeValue() {
// `upperBound(e)` defaults to `exprMaxVal(e)` when `e` isn't analyzable. So to get a meaningful
// result in this case we pick the minimum value obtainable from dataflow and range analysis.
result =
upperBound(this.statedSizeExpr())
.minimum(min(Expr statedSizeSrc |
DataFlow::localExprFlow(statedSizeSrc, this.statedSizeExpr())
|
statedSizeSrc.getValue().toInt()
statedSizeSrc.getValue().toBigInt()
))
}
}

predicate wrongBufferSize(Expr error, string msg) {
exists(CallWithBufferSize call, int bufsize, Variable buf, int statedSize |
exists(CallWithBufferSize call, int bufsize, Variable buf, QlBuiltins::BigInt statedSize |
staticBuffer(call.buffer(), buf, bufsize) and
statedSize = call.statedSizeValue() and
statedSize > bufsize and
statedSize > bufsize.toBigInt() and
error = call.statedSizeExpr() and
msg =
"Potential buffer-overflow: '" + buf.getName() + "' has size " + bufsize.toString() + " not " +
Expand Down
32 changes: 18 additions & 14 deletions cpp/ql/src/Likely Bugs/Arithmetic/IntMultToLong.ql
Original file line number Diff line number Diff line change
Expand Up @@ -76,20 +76,22 @@ int getEffectiveMulOperands(MulExpr me) {
* using SimpleRangeAnalysis.
*/
class AnalyzableExpr extends Expr {
float maxValue() { result = upperBound(this.getFullyConverted()) }
QlBuiltins::BigInt maxValue() { result = upperBound(this.getFullyConverted()) }

float minValue() { result = lowerBound(this.getFullyConverted()) }
QlBuiltins::BigInt minValue() { result = lowerBound(this.getFullyConverted()) }
}

class ParenAnalyzableExpr extends AnalyzableExpr, ParenthesisExpr {
override float maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }
override QlBuiltins::BigInt maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }

override float minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
override QlBuiltins::BigInt minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
}

class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
override float maxValue() {
exists(float x1, float y1, float x2, float y2 |
override QlBuiltins::BigInt maxValue() {
exists(
QlBuiltins::BigInt x1, QlBuiltins::BigInt y1, QlBuiltins::BigInt x2, QlBuiltins::BigInt y2
|
x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
Expand All @@ -98,8 +100,10 @@ class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
)
}

override float minValue() {
exists(float x1, float x2, float y1, float y2 |
override QlBuiltins::BigInt minValue() {
exists(
QlBuiltins::BigInt x1, QlBuiltins::BigInt x2, QlBuiltins::BigInt y1, QlBuiltins::BigInt y2
|
x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
Expand All @@ -110,27 +114,27 @@ class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
}

class AddAnalyzableExpr extends AnalyzableExpr, AddExpr {
override float maxValue() {
override QlBuiltins::BigInt maxValue() {
result =
this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() +
this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
}

override float minValue() {
override QlBuiltins::BigInt minValue() {
result =
this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() +
this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
}
}

class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
override float maxValue() {
override QlBuiltins::BigInt maxValue() {
result =
this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() -
this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
}

override float minValue() {
override QlBuiltins::BigInt minValue() {
result =
this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() -
this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
Expand All @@ -140,7 +144,7 @@ class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
VarAnalyzableExpr() { this.getTarget() instanceof StackVariable }

override float maxValue() {
override QlBuiltins::BigInt maxValue() {
exists(SsaDefinition def, Variable v |
def.getAUse(v) = this and
// if there is a defining expression, use that for
Expand All @@ -152,7 +156,7 @@ class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
)
}

override float minValue() {
override QlBuiltins::BigInt minValue() {
exists(SsaDefinition def, Variable v |
def.getAUse(v) = this and
if exists(def.getDefiningValue(v))
Expand Down
4 changes: 3 additions & 1 deletion cpp/ql/src/Likely Bugs/Arithmetic/PointlessComparison.ql
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,9 @@ import UnsignedGEZero
// So to reduce the number of false positives, we do not report a result if
// the comparison is in a macro expansion. Similarly for template
// instantiations.
from ComparisonOperation cmp, SmallSide ss, float left, float right, boolean value, string reason
from
ComparisonOperation cmp, SmallSide ss, QlBuiltins::BigInt left, QlBuiltins::BigInt right,
boolean value, string reason
where
not cmp.isInMacroExpansion() and
not cmp.isFromTemplateInstantiation(_) and
Expand Down
3 changes: 2 additions & 1 deletion cpp/ql/src/Security/CWE/CWE-190/ComparisonWithWiderType.ql
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,8 @@ where
// We adjust the comparison size in the case of a signed integer type.
// This is to exclude the sign bit from the comparison that determines if the small type's size is sufficient to hold
// the value of the larger type determined with range analysis.
upperBound(conv).log2() > (getComparisonSize(small) * 8 - getComparisonSizeAdjustment(small))
upperBound(conv).toString().length() / 10.log() >
(getComparisonSize(small) * 8 - getComparisonSizeAdjustment(small))
) and
// Ignore cases where the smaller type is int or larger
// These are still bugs, but you should need a very large string or array to
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -57,20 +57,20 @@ predicate exprIsSubLeftOrLess(SubExpr sub, DataFlow::Node n) {
isGuarded(sub, other.asExpr(), n.asExpr()) // other >= n
)
or
exists(DataFlow::Node other, float p, float q |
exists(DataFlow::Node other, QlBuiltins::BigInt p, QlBuiltins::BigInt q |
// linear access of `other`
exprIsSubLeftOrLess(sub, other) and
linearAccess(n.asExpr(), other.asExpr(), p, q) and // n = p * other + q
p <= 1 and
q <= 0
p <= 1.toBigInt() and
q <= 0.toBigInt()
)
or
exists(DataFlow::Node other, float p, float q |
exists(DataFlow::Node other, QlBuiltins::BigInt p, QlBuiltins::BigInt q |
// linear access of `n`
exprIsSubLeftOrLess(sub, other) and
linearAccess(other.asExpr(), n.asExpr(), p, q) and // other = p * n + q
p >= 1 and
q >= 0
p >= 1.toBigInt() and
q >= 0.toBigInt()
)
)
}
Expand Down
5 changes: 5 additions & 0 deletions cpp/ql/src/experimental/Likely Bugs/DerefNullResult.cpp
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
#define NULL nullptr
char *malloc(int);
void printf(const char *, ...);
int snprintf(char *, int, const char *);

char * create (int arg) {
if (arg > 42) {
// this function may return NULL
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
#define NULL nullptr

void test(char *arg1, int *arg2) {
if (arg1[0] == 'A') {
if (arg2 != NULL) { //maybe redundant
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,32 +28,32 @@ predicate isRealRange(Expr exp) {
lowerBound(exp).toString() != "-4294967296" and
lowerBound(exp).toString() != "-Infinity" and
lowerBound(exp).toString() != "NaN" and
upperBound(exp) != 2147483647 and
upperBound(exp) != 268435455 and
upperBound(exp) != 33554431 and
upperBound(exp) != 8388607 and
upperBound(exp) != 65535 and
upperBound(exp) != 32767 and
upperBound(exp) != 255 and
upperBound(exp) != 127 and
upperBound(exp) != 63 and
upperBound(exp) != 31 and
upperBound(exp) != 15 and
upperBound(exp) != 7 and
lowerBound(exp) != -2147483648 and
lowerBound(exp) != -268435456 and
lowerBound(exp) != -33554432 and
lowerBound(exp) != -8388608 and
lowerBound(exp) != -65536 and
lowerBound(exp) != -32768 and
lowerBound(exp) != -128
upperBound(exp) != 2147483647.toBigInt() and
upperBound(exp) != 268435455.toBigInt() and
upperBound(exp) != 33554431.toBigInt() and
upperBound(exp) != 8388607.toBigInt() and
upperBound(exp) != 65535.toBigInt() and
upperBound(exp) != 32767.toBigInt() and
upperBound(exp) != 255.toBigInt() and
upperBound(exp) != 127.toBigInt() and
upperBound(exp) != 63.toBigInt() and
upperBound(exp) != 31.toBigInt() and
upperBound(exp) != 15.toBigInt() and
upperBound(exp) != 7.toBigInt() and
lowerBound(exp) != "-2147483648".toBigInt() and
lowerBound(exp) != -268435456.toBigInt() and
lowerBound(exp) != -33554432.toBigInt() and
lowerBound(exp) != -8388608.toBigInt() and
lowerBound(exp) != -65536.toBigInt() and
lowerBound(exp) != -32768.toBigInt() and
lowerBound(exp) != -128.toBigInt()
}

/** Holds if the range of values for the condition is less than the choices. */
predicate isNotAllSelected(SwitchStmt swtmp) {
not swtmp.getExpr().isConstant() and
exists(int i |
i != 0 and
exists(QlBuiltins::BigInt i |
i != 0.toBigInt() and
(
i = lowerBound(swtmp.getASwitchCase().getExpr()) and
upperBound(swtmp.getExpr()) < i
Expand All @@ -70,7 +70,7 @@ predicate isNotAllSelected(SwitchStmt swtmp) {
/** Holds if the range of values for the condition is greater than the selection. */
predicate isConditionBig(SwitchStmt swtmp) {
not swtmp.hasDefaultCase() and
not exists(int iu, int il |
not exists(QlBuiltins::BigInt iu, QlBuiltins::BigInt il |
(
iu = upperBound(swtmp.getASwitchCase().getExpr()) or
iu = upperBound(swtmp.getASwitchCase().getEndExpr())
Expand Down Expand Up @@ -130,7 +130,7 @@ from SwitchStmt sw, string msg
where
isRealRange(sw.getExpr()) and
lowerBound(sw.getExpr()) != upperBound(sw.getExpr()) and
lowerBound(sw.getExpr()) != 0 and
lowerBound(sw.getExpr()) != 0.toBigInt() and
not exists(Expr cexp |
cexp = sw.getASwitchCase().getExpr() and not isRealRange(cexp)
or
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -97,24 +97,24 @@ predicate isRealRange(Expr exp) {
lowerBound(exp).toString() != "-4294967296" and
lowerBound(exp).toString() != "-Infinity" and
lowerBound(exp).toString() != "NaN" and
upperBound(exp) != 2147483647 and
upperBound(exp) != 268435455 and
upperBound(exp) != 33554431 and
upperBound(exp) != 8388607 and
upperBound(exp) != 65535 and
upperBound(exp) != 32767 and
upperBound(exp) != 255 and
upperBound(exp) != 127 and
lowerBound(exp) != -2147483648 and
lowerBound(exp) != -268435456 and
lowerBound(exp) != -33554432 and
lowerBound(exp) != -8388608 and
lowerBound(exp) != -65536 and
lowerBound(exp) != -32768 and
lowerBound(exp) != -128
upperBound(exp) != 2147483647.toBigInt() and
upperBound(exp) != 268435455.toBigInt() and
upperBound(exp) != 33554431.toBigInt() and
upperBound(exp) != 8388607.toBigInt() and
upperBound(exp) != 65535.toBigInt() and
upperBound(exp) != 32767.toBigInt() and
upperBound(exp) != 255.toBigInt() and
upperBound(exp) != 127.toBigInt() and
lowerBound(exp) != "-2147483648".toBigInt() and
lowerBound(exp) != -268435456.toBigInt() and
lowerBound(exp) != -33554432.toBigInt() and
lowerBound(exp) != -8388608.toBigInt() and
lowerBound(exp) != -65536.toBigInt() and
lowerBound(exp) != -32768.toBigInt() and
lowerBound(exp) != -128.toBigInt()
or
lowerBound(exp) = 0 and
upperBound(exp) = 1
lowerBound(exp) = 0.toBigInt() and
upperBound(exp) = 1.toBigInt()
}

/** Holds if expressions are of different size or range */
Expand All @@ -128,11 +128,15 @@ predicate isDifferentSize(Expr exp1, Expr exp2, Expr exp3) {
isRealRange(exp2) and
isRealRange(exp3)
) and
upperBound(exp1).maximum(upperBound(exp2)) - upperBound(exp1).minimum(upperBound(exp2)) < 16 and
lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) < 16 and
upperBound(exp1).maximum(upperBound(exp2)) - upperBound(exp1).minimum(upperBound(exp2)) <
16.toBigInt() and
lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) <
16.toBigInt() and
(
upperBound(exp1).maximum(upperBound(exp3)) - upperBound(exp1).minimum(upperBound(exp3)) > 256 or
lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) > 256
upperBound(exp1).maximum(upperBound(exp3)) - upperBound(exp1).minimum(upperBound(exp3)) >
256.toBigInt() or
lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) >
256.toBigInt()
)
}

Expand All @@ -146,10 +150,10 @@ predicate isDifferentResults(
isRealRange(exp2) and
isRealRange(exp3)
) and
exists(int i1, int i2, int i3 |
i1 in [lowerBound(exp1).floor() .. upperBound(exp1).floor()] and
i2 in [lowerBound(exp2).floor() .. upperBound(exp2).floor()] and
i3 in [lowerBound(exp3).floor() .. upperBound(exp3).floor()] and
exists(QlBuiltins::BigInt i1, QlBuiltins::BigInt i2, QlBuiltins::BigInt i3 |
i1 = lowerBound(exp1) + [0 .. (upperBound(exp1) - lowerBound(exp1)).toInt()].toBigInt() and
i2 = lowerBound(exp2) + [0 .. (upperBound(exp2) - lowerBound(exp2)).toInt()].toBigInt() and
i3 = lowerBound(exp3) + [0 .. (upperBound(exp3) - lowerBound(exp3)).toInt()].toBigInt() and
(
op1 instanceof BitwiseOrExpr and
op2 instanceof BitwiseAndExpr and
Expand Down

0 comments on commit 5c8a160

Please sign in to comment.