Merge pull request github#3950 from MathiasVP/simple-range-analysis-unsigned-multiplication-tests

C++: Add test cases for range analysis for unsigned multiplication

Author: Robert Marsh

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected

@@ -440,6 +440,47 @@
 | test.c:424:3:424:3 | i | -2.147483648E9 |
 | test.c:424:13:424:13 | j | -2.147483648E9 |
 | test.c:425:7:425:7 | i | -2.147483648E9 |
+| test.c:432:12:432:12 | a | 0.0 |
+| test.c:432:17:432:17 | a | 3.0 |
+| test.c:432:33:432:33 | b | 0.0 |
+| test.c:432:38:432:38 | b | 5.0 |
+| test.c:433:13:433:13 | a | 3.0 |
+| test.c:433:15:433:15 | b | 5.0 |
+| test.c:434:5:434:9 | total | 0.0 |
+| test.c:434:14:434:14 | r | -2.147483648E9 |
+| test.c:436:12:436:12 | a | 0.0 |
+| test.c:436:17:436:17 | a | 3.0 |
+| test.c:436:33:436:33 | b | 0.0 |
+| test.c:436:38:436:38 | b | 0.0 |
+| test.c:437:13:437:13 | a | 3.0 |
+| test.c:437:15:437:15 | b | 0.0 |
+| test.c:438:5:438:9 | total | -2.147483648E9 |
+| test.c:438:14:438:14 | r | -2.147483648E9 |
+| test.c:440:12:440:12 | a | 0.0 |
+| test.c:440:17:440:17 | a | 3.0 |
+| test.c:440:34:440:34 | b | 0.0 |
+| test.c:440:39:440:39 | b | 13.0 |
+| test.c:441:13:441:13 | a | 3.0 |
+| test.c:441:15:441:15 | b | 13.0 |
+| test.c:442:5:442:9 | total | -2.147483648E9 |
+| test.c:442:14:442:14 | r | -2.147483648E9 |
+| test.c:445:10:445:14 | total | -2.147483648E9 |
+| test.c:451:12:451:12 | b | 0.0 |
+| test.c:451:17:451:17 | b | 5.0 |
+| test.c:452:16:452:16 | b | 5.0 |
+| test.c:453:5:453:9 | total | 0.0 |
+| test.c:453:14:453:14 | r | -2.147483648E9 |
+| test.c:455:12:455:12 | b | 0.0 |
+| test.c:455:17:455:17 | b | 0.0 |
+| test.c:456:16:456:16 | b | 0.0 |
+| test.c:457:5:457:9 | total | -2.147483648E9 |
+| test.c:457:14:457:14 | r | -2.147483648E9 |
+| test.c:459:13:459:13 | b | 0.0 |
+| test.c:459:18:459:18 | b | 13.0 |
+| test.c:460:16:460:16 | b | 13.0 |
+| test.c:461:5:461:9 | total | -2.147483648E9 |
+| test.c:461:14:461:14 | r | -2.147483648E9 |
+| test.c:464:10:464:14 | total | -2.147483648E9 |
 | test.cpp:10:7:10:7 | b | -2.147483648E9 |
 | test.cpp:11:5:11:5 | x | -2.147483648E9 |
 | test.cpp:13:10:13:10 | x | -2.147483648E9 |

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c

@@ -424,3 +424,42 @@ void test17() {
   i = 20 + (j -= 10);
   out(i); // 60 [BUG: the analysis thinks it's 2^-31 .. 2^31-1]
 }
+
+// Tests for unsigned multiplication.
+int test_unsigned_mult01(unsigned int a, unsigned b) {
+  int total = 0;
+
+  if (3 <= a && a <= 11 && 5 <= b && b <= 23) {
+    int r = a*b;  // 15 .. 253
+    total += r;
+  }
+  if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
+    int r = a*b;  // 0 .. 253
+    total += r;
+  }
+  if (3 <= a && a <= 11 && 13 <= b && b <= 23) {
+    int r = a*b;  // 39 .. 253
+    total += r;
+  }
+
+  return total;
+}
+
+int test_unsigned_mult02(unsigned b) {
+  int total = 0;
+
+  if (5 <= b && b <= 23) {
+    int r = 11*b;  // 55 .. 253
+    total += r;
+  }
+  if (0 <= b && b <= 23) {
+    int r = 11*b;  // 0 .. 253
+    total += r;
+  }
+  if (13 <= b && b <= 23) {
+    int r = 11*b;  // 143 .. 253
+    total += r;
+  }
+
+  return total;
+}

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected

@@ -440,6 +440,47 @@
 | test.c:424:3:424:3 | i | 2.147483647E9 |
 | test.c:424:13:424:13 | j | 2.147483647E9 |
 | test.c:425:7:425:7 | i | 2.147483647E9 |
+| test.c:432:12:432:12 | a | 4.294967295E9 |
+| test.c:432:17:432:17 | a | 4.294967295E9 |
+| test.c:432:33:432:33 | b | 4.294967295E9 |
+| test.c:432:38:432:38 | b | 4.294967295E9 |
+| test.c:433:13:433:13 | a | 11.0 |
+| test.c:433:15:433:15 | b | 23.0 |
+| test.c:434:5:434:9 | total | 0.0 |
+| test.c:434:14:434:14 | r | 2.147483647E9 |
+| test.c:436:12:436:12 | a | 4.294967295E9 |
+| test.c:436:17:436:17 | a | 4.294967295E9 |
+| test.c:436:33:436:33 | b | 4.294967295E9 |
+| test.c:436:38:436:38 | b | 4.294967295E9 |
+| test.c:437:13:437:13 | a | 11.0 |
+| test.c:437:15:437:15 | b | 23.0 |
+| test.c:438:5:438:9 | total | 2.147483647E9 |
+| test.c:438:14:438:14 | r | 2.147483647E9 |
+| test.c:440:12:440:12 | a | 4.294967295E9 |
+| test.c:440:17:440:17 | a | 4.294967295E9 |
+| test.c:440:34:440:34 | b | 4.294967295E9 |
+| test.c:440:39:440:39 | b | 4.294967295E9 |
+| test.c:441:13:441:13 | a | 11.0 |
+| test.c:441:15:441:15 | b | 23.0 |
+| test.c:442:5:442:9 | total | 2.147483647E9 |
+| test.c:442:14:442:14 | r | 2.147483647E9 |
+| test.c:445:10:445:14 | total | 2.147483647E9 |
+| test.c:451:12:451:12 | b | 4.294967295E9 |
+| test.c:451:17:451:17 | b | 4.294967295E9 |
+| test.c:452:16:452:16 | b | 23.0 |
+| test.c:453:5:453:9 | total | 0.0 |
+| test.c:453:14:453:14 | r | 2.147483647E9 |
+| test.c:455:12:455:12 | b | 4.294967295E9 |
+| test.c:455:17:455:17 | b | 4.294967295E9 |
+| test.c:456:16:456:16 | b | 23.0 |
+| test.c:457:5:457:9 | total | 2.147483647E9 |
+| test.c:457:14:457:14 | r | 2.147483647E9 |
+| test.c:459:13:459:13 | b | 4.294967295E9 |
+| test.c:459:18:459:18 | b | 4.294967295E9 |
+| test.c:460:16:460:16 | b | 23.0 |
+| test.c:461:5:461:9 | total | 2.147483647E9 |
+| test.c:461:14:461:14 | r | 2.147483647E9 |
+| test.c:464:10:464:14 | total | 2.147483647E9 |
 | test.cpp:10:7:10:7 | b | 2.147483647E9 |
 | test.cpp:11:5:11:5 | x | 2.147483647E9 |
 | test.cpp:13:10:13:10 | x | 2.147483647E9 |

cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.c

@@ -365,7 +365,7 @@ int callCommand(void)
   return 0;
 }
 
-int shifts(void)
+void shifts(void)
 {
 	unsigned int x = 3;
 
@@ -374,11 +374,21 @@ int shifts(void)
 	if (x >> 1 == 1) {} // always true [NOT DETECTED]
 }
 
-int bitwise_ands()
+void bitwise_ands()
 {
 	unsigned int x = 0xFF;
 
 	if ((x & 2) >= 1) {}
 	if ((x & 2) >= 2) {}
 	if ((x & 2) >= 3) {} // always false
 }
+
+void unsigned_mult(unsigned int x, unsigned int y) {
+  if(x < 13 && y < 35) {
+      if(x * y > 1024) {} // always false [NOT DETECTED]
+      if(x * y < 204) {}
+      if(x >= 3 && y >= 2) {
+        if(x * y < 5) {} // always false [NOT DETECTED]
+      }
+  }
+}