C++: SimpleRangeAnalysis: unsigned multiplication

Author: jbj

cpp/ql/src/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

@@ -156,6 +156,10 @@ float safeFloor(float v) {
   result = v
 }
 
+private class UnsignedMulExpr extends MulExpr {
+  UnsignedMulExpr() { this.getType().(IntegralType).isUnsigned() }
+}
+
 /** Set of expressions which we know how to analyze. */
 private predicate analyzableExpr(Expr e) {
   // The type of the expression must be arithmetic. We reuse the logic in
@@ -178,6 +182,8 @@ private predicate analyzableExpr(Expr e) {
     or
     e instanceof SubExpr
     or
+    e instanceof UnsignedMulExpr
+    or
     e instanceof AssignExpr
     or
     e instanceof AssignAddExpr
@@ -278,6 +284,8 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
   or
   exists(SubExpr subExpr | e = subExpr | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar))
   or
+  exists(UnsignedMulExpr mulExpr | e = mulExpr | exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar))
+  or
   exists(AssignExpr addExpr | e = addExpr | exprDependsOnDef(addExpr.getRValue(), srcDef, srcVar))
   or
   exists(AssignAddExpr addExpr | e = addExpr |
@@ -625,6 +633,13 @@ private float getLowerBoundsImpl(Expr expr) {
     result = addRoundingDown(xLow, -yHigh)
   )
   or
+  exists(UnsignedMulExpr mulExpr, float xLow, float yLow |
+    expr = mulExpr and
+    xLow = getFullyConvertedLowerBounds(mulExpr.getLeftOperand()) and
+    yLow = getFullyConvertedLowerBounds(mulExpr.getRightOperand()) and
+    result = xLow * yLow
+  )
+  or
   exists(AssignExpr assign |
     expr = assign and
     result = getFullyConvertedLowerBounds(assign.getRValue())
@@ -794,6 +809,13 @@ private float getUpperBoundsImpl(Expr expr) {
     result = addRoundingUp(xHigh, -yLow)
   )
   or
+  exists(UnsignedMulExpr mulExpr, float xHigh, float yHigh |
+    expr = mulExpr and
+    xHigh = getFullyConvertedUpperBounds(mulExpr.getLeftOperand()) and
+    yHigh = getFullyConvertedUpperBounds(mulExpr.getRightOperand()) and
+    result = xHigh * yHigh
+  )
+  or
   exists(AssignExpr assign |
     expr = assign and
     result = getFullyConvertedUpperBounds(assign.getRValue())

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

@@ -447,40 +447,40 @@
 | test.c:433:13:433:13 | a | 3 |
 | test.c:433:15:433:15 | b | 5 |
 | test.c:434:5:434:9 | total | 0 |
-| test.c:434:14:434:14 | r | -2147483648 |
+| test.c:434:14:434:14 | r | 15 |
 | test.c:436:12:436:12 | a | 0 |
 | test.c:436:17:436:17 | a | 3 |
 | test.c:436:33:436:33 | b | 0 |
 | test.c:436:38:436:38 | b | 0 |
 | test.c:437:13:437:13 | a | 3 |
 | test.c:437:15:437:15 | b | 0 |
-| test.c:438:5:438:9 | total | -2147483648 |
-| test.c:438:14:438:14 | r | -2147483648 |
+| test.c:438:5:438:9 | total | 0 |
+| test.c:438:14:438:14 | r | 0 |
 | test.c:440:12:440:12 | a | 0 |
 | test.c:440:17:440:17 | a | 3 |
 | test.c:440:34:440:34 | b | 0 |
 | test.c:440:39:440:39 | b | 13 |
 | test.c:441:13:441:13 | a | 3 |
 | test.c:441:15:441:15 | b | 13 |
-| test.c:442:5:442:9 | total | -2147483648 |
-| test.c:442:14:442:14 | r | -2147483648 |
-| test.c:445:10:445:14 | total | -2147483648 |
+| test.c:442:5:442:9 | total | 0 |
+| test.c:442:14:442:14 | r | 39 |
+| test.c:445:10:445:14 | total | 0 |
 | test.c:451:12:451:12 | b | 0 |
 | test.c:451:17:451:17 | b | 5 |
 | test.c:452:16:452:16 | b | 5 |
 | test.c:453:5:453:9 | total | 0 |
-| test.c:453:14:453:14 | r | -2147483648 |
+| test.c:453:14:453:14 | r | 55 |
 | test.c:455:12:455:12 | b | 0 |
 | test.c:455:17:455:17 | b | 0 |
 | test.c:456:16:456:16 | b | 0 |
-| test.c:457:5:457:9 | total | -2147483648 |
-| test.c:457:14:457:14 | r | -2147483648 |
+| test.c:457:5:457:9 | total | 0 |
+| test.c:457:14:457:14 | r | 0 |
 | test.c:459:13:459:13 | b | 0 |
 | test.c:459:18:459:18 | b | 13 |
 | test.c:460:16:460:16 | b | 13 |
-| test.c:461:5:461:9 | total | -2147483648 |
-| test.c:461:14:461:14 | r | -2147483648 |
-| test.c:464:10:464:14 | total | -2147483648 |
+| test.c:461:5:461:9 | total | 0 |
+| test.c:461:14:461:14 | r | 143 |
+| test.c:464:10:464:14 | total | 0 |
 | test.cpp:10:7:10:7 | b | -2147483648 |
 | test.cpp:11:5:11:5 | x | -2147483648 |
 | test.cpp:13:10:13:10 | x | -2147483648 |

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

@@ -447,40 +447,40 @@
 | test.c:433:13:433:13 | a | 11 |
 | test.c:433:15:433:15 | b | 23 |
 | test.c:434:5:434:9 | total | 0 |
-| test.c:434:14:434:14 | r | 2147483647 |
+| test.c:434:14:434:14 | r | 253 |
 | test.c:436:12:436:12 | a | 4294967295 |
 | test.c:436:17:436:17 | a | 4294967295 |
 | test.c:436:33:436:33 | b | 4294967295 |
 | test.c:436:38:436:38 | b | 4294967295 |
 | test.c:437:13:437:13 | a | 11 |
 | test.c:437:15:437:15 | b | 23 |
-| test.c:438:5:438:9 | total | 2147483647 |
-| test.c:438:14:438:14 | r | 2147483647 |
+| test.c:438:5:438:9 | total | 253 |
+| test.c:438:14:438:14 | r | 253 |
 | test.c:440:12:440:12 | a | 4294967295 |
 | test.c:440:17:440:17 | a | 4294967295 |
 | test.c:440:34:440:34 | b | 4294967295 |
 | test.c:440:39:440:39 | b | 4294967295 |
 | test.c:441:13:441:13 | a | 11 |
 | test.c:441:15:441:15 | b | 23 |
-| test.c:442:5:442:9 | total | 2147483647 |
-| test.c:442:14:442:14 | r | 2147483647 |
-| test.c:445:10:445:14 | total | 2147483647 |
+| test.c:442:5:442:9 | total | 506 |
+| test.c:442:14:442:14 | r | 253 |
+| test.c:445:10:445:14 | total | 759 |
 | test.c:451:12:451:12 | b | 4294967295 |
 | test.c:451:17:451:17 | b | 4294967295 |
 | test.c:452:16:452:16 | b | 23 |
 | test.c:453:5:453:9 | total | 0 |
-| test.c:453:14:453:14 | r | 2147483647 |
+| test.c:453:14:453:14 | r | 253 |
 | test.c:455:12:455:12 | b | 4294967295 |
 | test.c:455:17:455:17 | b | 4294967295 |
 | test.c:456:16:456:16 | b | 23 |
-| test.c:457:5:457:9 | total | 2147483647 |
-| test.c:457:14:457:14 | r | 2147483647 |
+| test.c:457:5:457:9 | total | 253 |
+| test.c:457:14:457:14 | r | 253 |
 | test.c:459:13:459:13 | b | 4294967295 |
 | test.c:459:18:459:18 | b | 4294967295 |
 | test.c:460:16:460:16 | b | 23 |
-| test.c:461:5:461:9 | total | 2147483647 |
-| test.c:461:14:461:14 | r | 2147483647 |
-| test.c:464:10:464:14 | total | 2147483647 |
+| test.c:461:5:461:9 | total | 506 |
+| test.c:461:14:461:14 | r | 253 |
+| test.c:464:10:464:14 | total | 759 |
 | test.cpp:10:7:10:7 | b | 2147483647 |
 | test.cpp:11:5:11:5 | x | 2147483647 |
 | test.cpp:13:10:13:10 | x | 2147483647 |

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

@@ -385,10 +385,10 @@ void bitwise_ands()
 
 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 > 1024) {} // always false
       if(x * y < 204) {}
       if(x >= 3 && y >= 2) {
-        if(x * y < 5) {} // always false [NOT DETECTED]
+        if(x * y < 5) {} // always false
       }
   }
 }