From 87c144d33bfe597f696db3e596e1eb1382d29528 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Mon, 27 Mar 2023 13:19:47 +0100 Subject: [PATCH 1/2] C++: Throw away the sign analysis when analyzing add expressions: instead, we now recursively analyze both operands. --- .../semantic/analysis/RangeAnalysisStage.qll | 49 ++++++++++++------- 1 file changed, 31 insertions(+), 18 deletions(-) diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll index cdf0943eb65..2fb13cc8414 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll @@ -591,24 +591,6 @@ module RangeStage Bounds, LangSig LangParam, UtilSig< delta = D::fromInt(0) and (upper = true or upper = false) or - exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) | - // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep - not x instanceof SemConstantIntegerExpr and - not e1 instanceof SemConstantIntegerExpr and - if strictlyPositiveIntegralExpr(x) - then upper = false and delta = D::fromInt(1) - else - if semPositive(x) - then upper = false and delta = D::fromInt(0) - else - if strictlyNegativeIntegralExpr(x) - then upper = true and delta = D::fromInt(-1) - else - if semNegative(x) - then upper = true and delta = D::fromInt(0) - else none() - ) - or exists(SemExpr x, SemSubExpr sub | e2 = sub and sub.getLeftOperand() = e1 and @@ -1043,13 +1025,44 @@ module RangeStage Bounds, LangSig LangParam, UtilSig< delta = D::fromFloat(f) and if semPositive(e) then f >= 0 else any() ) + or + exists( + SemBound bLeft, SemBound bRight, D::Delta dLeft, D::Delta dRight, boolean fbeLeft, + boolean fbeRight, D::Delta odLeft, D::Delta odRight, SemReason rLeft, SemReason rRight + | + boundedAddOperand(e, upper, bLeft, false, dLeft, fbeLeft, odLeft, rLeft) and + boundedAddOperand(e, upper, bRight, true, dRight, fbeRight, odRight, rRight) and + delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and + fromBackEdge = fbeLeft.booleanOr(fbeRight) + | + b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound + or + b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound + ) ) } + pragma[nomagic] private predicate boundedConditionalExpr( SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, SemReason reason ) { bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason) } + + pragma[nomagic] + private predicate boundedAddOperand( + SemAddExpr add, boolean upper, SemBound b, boolean isLeft, 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(add, _, _) and + ( + isLeft = true and + bounded(add.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason) + or + isLeft = false and + bounded(add.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason) + ) + } } From 1a6186496f82558b121e991c5ded1fdf10ce76f7 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Mon, 27 Mar 2023 13:20:17 +0100 Subject: [PATCH 2/2] C++: Accept test changes. --- .../SimpleRangeAnalysis_tests.cpp | 122 +++++++++--------- .../library-tests/ir/range-analysis/test.cpp | 2 +- 2 files changed, 62 insertions(+), 62 deletions(-) diff --git a/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp b/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp index 58ed4fdf396..89b81e2829b 100644 --- a/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp +++ b/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp @@ -40,13 +40,13 @@ int test4() { int total = 0; for (i = 0; i < 2; i = i+1) { range(i); // $ range=<=1 range=>=0 - range(total); + range(total); // $ range=>=0 total += i; - range(total); + range(total); // $ range=<=i+1 range=<=i+1 range=>=0 range=>=i+0 } - range(total); + range(total); // $ range=>=0 range(i); // $ range===2 - range(total + i); // $ range=>=i+1 + range(total + i); // $ range===i+2 range=>=2 range=>=i+0 return total + i; } @@ -55,13 +55,13 @@ int test5() { int total = 0; for (i = 0; i < 2; i++) { range(i); // $ range=<=1 range=>=0 - range(total); + range(total); // $ range=>=0 total += i; - range(total); + range(total); // $ range=<=i+1 range=>=0 range=>=i+0 } - range(total); + range(total); // $ range=>=0 range(i); // $ range===2 - range(total + i); // $ range=>=i+1 + range(total + i); // $ range===i+2 range=>=2 range=>=i+0 return total + i; } @@ -70,9 +70,9 @@ int test6() { int total = 0; for (i = 0; i+2 < 4; i = i+1) { range(i); // $ range=<=1 range=>=0 - range(total); + range(total); // $ range=>=0 total += i; - range(total); + range(total); // $ range=<=i+1 range=>=0 range=>=i+0 } return total + i; } @@ -175,12 +175,12 @@ int test12() { size_type Start = 0; while (Start <= test12_helper()-1) { - range(Start); // $ range=>=0 + range(Start); const size_type Length = test12_helper(); Start += Length + 1; - range(Start); // $ range=>=1 range=>=Start+1 range=">=call to test12_helper+1" + range(Start); } - range(Start); // $ range=>=0 + range(Start); return 1; } @@ -194,8 +194,8 @@ int test13(char c, int i) { range(y); // $ range===-1 int z = i+1; range(z); // $ range===i+1 - range(c + i + uc + x + y + z); // $ range=>=1 range=">=... - ...+0" - range((double)(c + i + uc + x + y + z)); // $ range=>=1 range=">=... - ...+0" + range(c + i + uc + x + y + z); + range((double)(c + i + uc + x + y + z)); return (double)(c + i + uc + x + y + z); } @@ -233,9 +233,9 @@ int test_unary(int a) { range(b); // $ range=<=11 range=>=3 int c = -a; range(c); // $ range=<=-3 range=>=-11 - range(b+c); // $ range=<=10 range="<=+ ...:a-1" range=">=- ...+1" range=>=-10 + range(b+c); // $ range=<=8 range=>=-8 total += b+c; - range(total); + range(total); // $ range=<=8 range=>=-8 } if (0 <= a && a <= 11) { range(a); // $ range=<=11 range=>=0 @@ -243,9 +243,9 @@ int test_unary(int a) { range(b); // $ range=<=11 range=>=0 int c = -a; range(c); // $ range=<=0 range=>=-11 - range(b+c); // $ range=<=11 range="<=+ ...:a+0" range=">=- ...+0" range=>=-11 + range(b+c); // $ range=<=11 range=>=-11 total += b+c; - range(total); + range(total); // $ range=<=0+11 range=<=19 range=>=0-11 range=>=-19 } if (-7 <= a && a <= 11) { range(a); // $ range=<=11 range=>=-7 @@ -253,9 +253,9 @@ int test_unary(int a) { range(b); // $ range=<=11 range=>=-7 int c = -a; range(c); // $ range=<=7 range=>=-11 - range(b+c); + range(b+c); // $ range=<=18 range=>=-18 total += b+c; - range(total); + range(total); // $ range="<=- ...+18" range=">=- ...-18" range=<=0+29 range=<=37 range=>=0-29 range=>=-37 } if (-7 <= a && a <= 1) { range(a); // $ range=<=1 range=>=-7 @@ -263,9 +263,9 @@ int test_unary(int a) { range(b); // $ range=<=1 range=>=-7 int c = -a; range(c); // $ range=<=7 range=>=-1 - range(b+c); + range(b+c); // $ range=<=8 range=>=-8 total += b+c; - range(total); + range(total); // $ range="<=- ...+8" range="<=- ...+26" range=">=- ...-8" range=">=- ...-26" range=<=0+37 range=<=45 range=>=0-37 range=>=-45 } if (-7 <= a && a <= 0) { range(a); // $ range=<=0 range=>=-7 @@ -273,9 +273,9 @@ int test_unary(int a) { range(b); // $ range=<=0 range=>=-7 int c = -a; range(c); // $ range=<=7 range=>=0 - range(b+c); // $ range="<=- ...+0" range=">=+ ...:a+0" range=>=-7 range=<=7 + range(b+c); // $ range=>=-7 range=<=7 total += b+c; - range(total); + range(total); // $ range="<=- ...+7" range="<=- ...+15" range="<=- ...+33" range=">=- ...-7" range=">=- ...-15" range=">=- ...-33" range=<=0+44 range=<=52 range=>=0-44 range=>=-52 } if (-7 <= a && a <= -2) { range(a); // $ range=<=-2 range=>=-7 @@ -283,11 +283,11 @@ int test_unary(int a) { range(b); // $ range=<=-2 range=>=-7 int c = -a; range(c); // $ range=<=7 range=>=2 - range(b+c); // $ range="<=- ...-1" range=">=+ ...:a+1" range=>=-6 range=<=6 + range(b+c); // $ range=<=5 range=>=-5 total += b+c; - range(total); + range(total); // $ range="<=- ...+5" range="<=- ...+12" range="<=- ...+20" range="<=- ...+38" range=">=- ...-5" range=">=- ...-12" range=">=- ...-20" range=">=- ...-38" range=<=0+49 range=<=57 range=>=0-49 range=>=-57 } - range(total); + range(total); // $ range="<=- ...+5" range="<=- ...+12" range="<=- ...+20" range="<=- ...+38" range=">=- ...-5" range=">=- ...-12" range=">=- ...-20" range=">=- ...-38" range=<=0+49 range=<=57 range=>=0-49 range=>=-57 return total; } @@ -302,7 +302,7 @@ int test_mult01(int a, int b) { int r = a*b; // 15 .. 253 range(r); total += r; - range(total); // $ range=>=1 + range(total); // $ MISSING: range=>=1 } if (3 <= a && a <= 11 && 0 <= b && b <= 23) { range(a); // $ range=<=11 range=>=3 @@ -310,7 +310,7 @@ int test_mult01(int a, int b) { int r = a*b; // 0 .. 253 range(r); total += r; - range(total); // $ range=>=0 range=>=3+0 + range(total); // $ MISSING: range=>=0 range=>=3+0 } if (3 <= a && a <= 11 && -13 <= b && b <= 23) { range(a); // $ range=<=11 range=>=3 @@ -326,7 +326,7 @@ int test_mult01(int a, int b) { int r = a*b; // -143 .. 0 range(r); total += r; - range(total); // $ range=<=3+0 + range(total); // $ MISSING: range=<=3+0 } if (3 <= a && a <= 11 && -13 <= b && b <= -7) { range(a); // $ range=<=11 range=>=3 @@ -334,9 +334,9 @@ int test_mult01(int a, int b) { int r = a*b; // -143 .. -21 range(r); total += r; - range(total); // $ range=<=3-1 + range(total); // $ MISSING: range=<=3-1 } - range(total); // $ range=<=3+0 + range(total); // $ MISSING: range=<=3+0 return total; } @@ -350,7 +350,7 @@ int test_mult02(int a, int b) { int r = a*b; // 0 .. 253 range(r); total += r; - range(total); // $ range=>=0 + range(total); // $ MISSING: range=>=0 } if (0 <= a && a <= 11 && 0 <= b && b <= 23) { range(a); // $ range=<=11 range=>=0 @@ -358,7 +358,7 @@ int test_mult02(int a, int b) { int r = a*b; // 0 .. 253 range(r); total += r; - range(total); // $ range=>=0 range=>=0+0 + range(total); // $ MISSING: range=>=0 range=>=0+0 } if (0 <= a && a <= 11 && -13 <= b && b <= 23) { range(a); // $ range=<=11 range=>=0 @@ -374,7 +374,7 @@ int test_mult02(int a, int b) { int r = a*b; // -143 .. 0 range(r); total += r; - range(total); // $ range=<=0+0 + range(total); // $ MISSING: range=<=0+0 } if (0 <= a && a <= 11 && -13 <= b && b <= -7) { range(a); // $ range=<=11 range=>=0 @@ -382,9 +382,9 @@ int test_mult02(int a, int b) { int r = a*b; // -143 .. 0 range(r); total += r; - range(total); // $ range=<=0+0 + range(total); // $ MISSING: range=<=0+0 } - range(total); // $ range=<=0+0 + range(total); // $ MISSING: range=<=0+0 return total; } @@ -445,7 +445,7 @@ int test_mult04(int a, int b) { range(b); // $ range=<=23 range=>=5 int r = a*b; // -391 .. 0 total += r; - range(total); // $ range=<=0 + range(total); // $ MISSING: range=<=0 } if (-17 <= a && a <= 0 && 0 <= b && b <= 23) { range(a); // $ range=<=0 range=>=-17 @@ -453,7 +453,7 @@ int test_mult04(int a, int b) { int r = a*b; // -391 .. 0 range(r); total += r; - range(total); // $ range="<=- ...+0" range=<=0 + range(total); // $ MISSING: range="<=- ...+0" range=<=0 } if (-17 <= a && a <= 0 && -13 <= b && b <= 23) { range(a); // $ range=<=0 range=>=-17 @@ -469,7 +469,7 @@ int test_mult04(int a, int b) { int r = a*b; // 0 .. 221 range(r); total += r; - range(total); // $ range=">=- ...+0" + range(total); // $ MISSING: range=">=- ...+0" } if (-17 <= a && a <= 0 && -13 <= b && b <= -7) { range(a); // $ range=<=0 range=>=-17 @@ -477,9 +477,9 @@ int test_mult04(int a, int b) { int r = a*b; // 0 .. 221 range(r); total += r; - range(total); // $ range=">=- ...+0" + range(total); // $ MISSING: range=">=- ...+0" } - range(total); // $ range=">=- ...+0" + range(total); // $ MISSING: range=">=- ...+0" return total; } @@ -493,7 +493,7 @@ int test_mult05(int a, int b) { int r = a*b; // -391 .. -10 range(r); total += r; - range(total); // $ range=<=-1 + range(total); // $ MISSING: range=<=-1 } if (-17 <= a && a <= -2 && 0 <= b && b <= 23) { range(a); // $ range=<=-2 range=>=-17 @@ -501,7 +501,7 @@ int test_mult05(int a, int b) { int r = a*b; // -391 .. 0 range(r); total += r; - range(total); // $ range="<=- ...+0" range=<=0 + range(total); // $ MISSING: range="<=- ...+0" range=<=0 } if (-17 <= a && a <= -2 && -13 <= b && b <= 23) { range(a); // $ range=<=-2 range=>=-17 @@ -517,7 +517,7 @@ int test_mult05(int a, int b) { int r = a*b; // 0 .. 221 range(r); total += r; - range(total); // $ range=">=- ...+0" + range(total); // $ MISSING: range=">=- ...+0" } if (-17 <= a && a <= -2 && -13 <= b && b <= -7) { range(a); // $ range=<=-2 range=>=-17 @@ -525,9 +525,9 @@ int test_mult05(int a, int b) { int r = a*b; // 14 .. 221 range(r); total += r; - range(total); // $ range=">=- ...+1" + range(total); // $ MISSING: range=">=- ...+1" } - range(total); // $ range=">=- ...+0" + range(total); // $ MISSING: range=">=- ...+0" return total; } @@ -598,7 +598,7 @@ unsigned int test_ternary01(unsigned int x) { (range(x), 500); // $ range=<=299 range(y8); // y8 <= 300 } - range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ range=">=... = ...:... ? ... : ...+0" range=">=call to range+0" + range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0" return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8; } @@ -628,7 +628,7 @@ unsigned int test_ternary02(unsigned int x) { (range(x), 5); // $ range=>=300 range(y5); // y6 >= 0 } - range(y1 + y2 + y3 + y4 + y5); // $ range=">=... = ...:... ? ... : ...+0" range=">=call to range+0" + range(y1 + y2 + y3 + y4 + y5); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0" return y1 + y2 + y3 + y4 + y5; } @@ -647,7 +647,7 @@ unsigned int test_comma01(unsigned int x) { range(y), // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5" y); range(y2); // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5" - range(y1 + y2); // $ range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6" + range(y1 + y2); // $ MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6" return y1 + y2; } @@ -685,7 +685,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) { int r = a*b; // 15 .. 253 range(r); total += r; - range(total); // $ range=>=1 + range(total); // $ MISSING: range=>=1 } if (3 <= a && a <= 11 && 0 <= b && b <= 23) { range(a); // $ range=<=11 range=>=3 @@ -693,7 +693,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) { int r = a*b; // 0 .. 253 range(r); total += r; - range(total); // $ range=">=(unsigned int)...+0" range=>=0 + range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0 } if (3 <= a && a <= 11 && 13 <= b && b <= 23) { range(a); // $ range=<=11 range=>=3 @@ -701,9 +701,9 @@ int test_unsigned_mult01(unsigned int a, unsigned b) { int r = a*b; // 39 .. 253 range(r); total += r; - range(total); // $ range=">=(unsigned int)...+1" range=>=1 + range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1 } - range(total); // $ range=">=(unsigned int)...+0" range=>=0 + range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0 return total; } @@ -715,23 +715,23 @@ int test_unsigned_mult02(unsigned b) { int r = 11*b; // 55 .. 253 range(r); total += r; - range(total); // $ range=>=1 + range(total); // $ MISSING: range=>=1 } if (0 <= b && b <= 23) { range(b); // $ range=<=23 range=>=0 int r = 11*b; // 0 .. 253 range(r); total += r; - range(total); // $ range=">=(unsigned int)...+0" range=>=0 + range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0 } if (13 <= b && b <= 23) { range(b); // $ range=<=23 range=>=13 int r = 11*b; // 143 .. 253 range(r); total += r; - range(total); // $ range=">=(unsigned int)...+1" range=>=1 + range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1 } - range(total); // $ range=">=(unsigned int)...+0" range=>=0 + range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0 return total; } @@ -790,7 +790,7 @@ unsigned long mul_assign(unsigned int ui) { range(ulconst); // $ range===10 ulconst *= 4; range(ulconst); // $ range===40 - range(uiconst + ulconst); // $ range=">=... *= ...+1" range=>=41 + range(uiconst + ulconst); // $ range===80 return uiconst + ulconst; // 40 .. 40 for both } @@ -942,7 +942,7 @@ void widen_recursive_expr() { for (s = 0; s < 10; s++) { range(s); // $ range=<=9 range=>=0 int result = s + s; - range(result); // 0 .. 18 + range(result); // $ range=<=18 range=<=s+9 range=>=0 range=>=s+0 } } 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 5290fffc8fd..f8587c42d67 100644 --- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp +++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp @@ -7,7 +7,7 @@ } if (y - 2 == x && y > 300) { - range(x + y); // $ range=>=300 range=>=x+1 range=>=y-1 + range(x + y); // $ range=<=802 range=>=600 return x + y; }