diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll index 0576f5ff373..ee87eab1f1c 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll @@ -574,16 +574,6 @@ module RangeStage< ) } - /** Holds if `e >= 1` as determined by sign analysis. */ - private predicate strictlyPositiveIntegralExpr(SemExpr e) { - semStrictlyPositive(e) and getTrackedType(e) instanceof SemIntegerType - } - - /** Holds if `e <= -1` as determined by sign analysis. */ - private predicate strictlyNegativeIntegralExpr(SemExpr e) { - semStrictlyNegative(e) and getTrackedType(e) instanceof SemIntegerType - } - /** * Holds if `e1 + delta` is a valid bound for `e2`. * - `upper = true` : `e2 <= e1 + delta` @@ -597,27 +587,6 @@ module RangeStage< delta = D::fromInt(0) and (upper = true or upper = false) or - exists(SemExpr x, SemSubExpr sub | - e2 = sub and - sub.getLeftOperand() = e1 and - sub.getRightOperand() = x - | - // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep - not x instanceof SemConstantIntegerExpr and - if strictlyPositiveIntegralExpr(x) - then upper = true and delta = D::fromInt(-1) - else - if semPositive(x) - then upper = true and delta = D::fromInt(0) - else - if strictlyNegativeIntegralExpr(x) - then upper = false and delta = D::fromInt(1) - else - if semNegative(x) - then upper = false and delta = D::fromInt(0) - else none() - ) - or e2.(SemRemExpr).getRightOperand() = e1 and semPositive(e1) and delta = D::fromInt(-1) and @@ -1137,6 +1106,30 @@ module RangeStage< b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound ) or + exists( + D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft, + D::Delta odRight, SemReason rLeft, SemReason rRight + | + boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, odLeft, rLeft) and + boundedSubOperandRight(e, upper, dRight, fbeRight, odRight, rRight) and + // when `upper` is `true` we have: + // left <= b + dLeft + // right >= 0 + dRight + // left - right <= b + dLeft - (0 + dRight) + // = b + (dLeft - dRight) + // and when `upper` is `false` we have: + // left >= b + dLeft + // right <= 0 + dRight + // left - right >= b + dLeft - (0 + dRight) + // = b + (dLeft - dRight) + delta = D::fromFloat(D::toFloat(dLeft) - D::toFloat(dRight)) and + fromBackEdge = fbeLeft.booleanOr(fbeRight) + | + origdelta = odLeft and reason = rLeft + or + origdelta = odRight and reason = rRight + ) + or exists( SemRemExpr rem, D::Delta d_max, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2, D::Delta od1, D::Delta od2, SemReason r1, SemReason r2 @@ -1201,6 +1194,38 @@ module RangeStage< ) } + /** + * Holds if `sub = left - right` and `left <= b + delta` if `upper` is `true` + * and `left >= b + delta` is `upper` is `false`. + */ + pragma[nomagic] + private predicate boundedSubOperandLeft( + SemSubExpr sub, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge, + D::Delta origdelta, SemReason reason + ) { + // `semValueFlowStep` already handles the case where one of the operands is a constant. + not semValueFlowStep(sub, _, _) and + bounded(sub.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason) + } + + /** + * Holds if `sub = left - right` and `right <= 0 + delta` if `upper` is `false` + * and `right >= 0 + delta` is `upper` is `true`. + * + * Note that the boolean value of `upper` is flipped compared to many other predicates in + * this file. This ensures a clean join at the call-site. + */ + pragma[nomagic] + private predicate boundedSubOperandRight( + SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, + SemReason reason + ) { + // `semValueFlowStep` already handles the case where one of the operands is a constant. + not semValueFlowStep(sub, _, _) and + bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge, + origdelta, reason) + } + pragma[nomagic] private predicate boundedRemExpr( SemRemExpr rem, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected index f8b8bab0e4f..b5bbc68dbd4 100644 --- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected +++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected @@ -69,12 +69,6 @@ edges | test.cpp:322:19:322:27 | ... + ... | test.cpp:325:24:325:26 | end | | test.cpp:324:23:324:26 | temp | test.cpp:324:23:324:32 | ... + ... | | test.cpp:324:23:324:32 | ... + ... | test.cpp:325:15:325:19 | temp2 | -| test.cpp:351:9:351:11 | arr | test.cpp:351:9:351:14 | access to array | -| test.cpp:351:9:351:11 | arr | test.cpp:351:18:351:25 | access to array | -| test.cpp:351:18:351:20 | arr | test.cpp:351:9:351:14 | access to array | -| test.cpp:351:18:351:20 | arr | test.cpp:351:18:351:25 | access to array | -| test.cpp:351:29:351:31 | arr | test.cpp:351:9:351:14 | access to array | -| test.cpp:351:29:351:31 | arr | test.cpp:351:18:351:25 | access to array | nodes | test.cpp:34:5:34:24 | access to array | semmle.label | access to array | | test.cpp:34:10:34:12 | buf | semmle.label | buf | @@ -167,11 +161,6 @@ nodes | test.cpp:325:15:325:19 | temp2 | semmle.label | temp2 | | test.cpp:325:24:325:26 | end | semmle.label | end | | test.cpp:325:24:325:26 | end | semmle.label | end | -| test.cpp:351:9:351:11 | arr | semmle.label | arr | -| test.cpp:351:9:351:14 | access to array | semmle.label | access to array | -| test.cpp:351:18:351:20 | arr | semmle.label | arr | -| test.cpp:351:18:351:25 | access to array | semmle.label | access to array | -| test.cpp:351:29:351:31 | arr | semmle.label | arr | subpaths #select | test.cpp:35:5:35:22 | PointerAdd: access to array | test.cpp:35:10:35:12 | buf | test.cpp:35:5:35:22 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:35:5:35:26 | Store: ... = ... | write | @@ -194,6 +183,3 @@ subpaths | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:330:13:330:24 | Store: ... = ... | write | | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:331:13:331:24 | Store: ... = ... | write | | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:333:13:333:24 | Store: ... = ... | write | -| test.cpp:351:18:351:25 | PointerAdd: access to array | test.cpp:351:9:351:11 | arr | test.cpp:351:18:351:25 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:348:9:348:11 | arr | arr | test.cpp:351:18:351:25 | Load: access to array | read | -| test.cpp:351:18:351:25 | PointerAdd: access to array | test.cpp:351:18:351:20 | arr | test.cpp:351:18:351:25 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:348:9:348:11 | arr | arr | test.cpp:351:18:351:25 | Load: access to array | read | -| test.cpp:351:18:351:25 | PointerAdd: access to array | test.cpp:351:29:351:31 | arr | test.cpp:351:18:351:25 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:348:9:348:11 | arr | arr | test.cpp:351:18:351:25 | Load: access to array | read | diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp index 2d3945e48db..03de927073a 100644 --- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp +++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp @@ -348,7 +348,7 @@ int positiveRange(int x) { int arr[128]; for(int i=127-offset; i>= 0; i--) { - arr[i] = arr[i+1] + arr[i+offset]; // GOOD [FALSE POSITIVE] + arr[i] = arr[i+1] + arr[i+offset]; // GOOD } return arr[0]; } diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp index b7a0386cd6b..a11e6abc879 100644 --- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp +++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp @@ -733,3 +733,12 @@ void test36(unsigned size, unsigned n) { *end = 0; // $ deref=L733 // BAD } } + +void test37(unsigned long n) +{ + int *p = new int[n]; + for (unsigned long i = n; i != 0u; i--) + { + p[n - i] = 0; // GOOD + } +} \ No newline at end of file diff --git a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp index 2271953b7ab..ff9acbfae1a 100644 --- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp +++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp @@ -95,3 +95,25 @@ void gotoLoop(bool b1, bool b2) } } } + +void test_sub(int x, int y, int n) { + if(x > 0 && x < 500) { + if(y > 0 && y < 10) { + range(x - y); // $ range=<=498 range=>=-8 + } + + if(n > 0 && n < 100) { + for (int i = 0; i < n; i++) + { + range(n - i); // $ range=">=Phi: i-97" range=<=99 range=>=-97 + range(i - n); // $ range="<=Phi: i-1" range=">=Phi: i-99" range=<=97 range=>=-99 + } + + for (int i = n; i != 0; i--) + { + range(n - i); // $ SPURIOUS: overflow=+ + range(i - n); // $ range=">=Phi: i-99" + } + } + } +}