Merge pull request #1037 from kevinbackhouse/RangeAnalysisAssignAddOverflow

Better overflow detection for AssignAdd/AssignSub

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

@@ -106,6 +106,9 @@ predicate analyzableExpr(Expr e) {
    (e instanceof ConditionalExpr) or
    (e instanceof AddExpr) or
    (e instanceof SubExpr) or
+   (e instanceof AssignExpr) or
+   (e instanceof AssignAddExpr) or
+   (e instanceof AssignSubExpr) or
    (e instanceof CrementOperation) or
    (e instanceof RemExpr) or
    (e instanceof CommaExpr) or
@@ -203,6 +206,18 @@ predicate exprDependsOnDef(
   | e = subExpr
   | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar))
   or
+  exists (AssignExpr addExpr
+  | e = addExpr
+  | exprDependsOnDef(addExpr.getRValue(), srcDef, srcVar))
+  or
+  exists (AssignAddExpr addExpr
+  | e = addExpr
+  | exprDependsOnDef(addExpr.getAnOperand(), srcDef, srcVar))
+  or
+  exists (AssignSubExpr subExpr
+  | e = subExpr
+  | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar))
+  or
   exists (CrementOperation crementExpr
   | e = crementExpr
   | exprDependsOnDef(crementExpr.getOperand(), srcDef, srcVar))
@@ -534,6 +549,22 @@ float getLowerBoundsImpl(Expr expr) {
     yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and
     result = addRoundingDown(xLow, -yHigh))
   or
+  exists (AssignExpr assign
+  | expr = assign and
+    result = getFullyConvertedLowerBounds(assign.getRValue()))
+  or
+  exists (AssignAddExpr addExpr, float xLow, float yLow
+  | expr = addExpr and
+    xLow = getFullyConvertedLowerBounds(addExpr.getLValue()) and
+    yLow = getFullyConvertedLowerBounds(addExpr.getRValue()) and
+    result = addRoundingDown(xLow, yLow))
+  or
+  exists (AssignSubExpr subExpr, float xLow, float yHigh
+  | expr = subExpr and
+    xLow = getFullyConvertedLowerBounds(subExpr.getLValue()) and
+    yHigh = getFullyConvertedUpperBounds(subExpr.getRValue()) and
+    result = addRoundingDown(xLow, -yHigh))
+  or
   exists (PrefixIncrExpr incrExpr, float xLow
   | expr = incrExpr and
     xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and
@@ -656,6 +687,22 @@ float getUpperBoundsImpl(Expr expr) {
     yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and
     result = addRoundingUp(xHigh, -yLow))
   or
+  exists (AssignExpr assign
+  | expr = assign and
+    result = getFullyConvertedUpperBounds(assign.getRValue()))
+  or
+  exists (AssignAddExpr addExpr, float xHigh, float yHigh
+  | expr = addExpr and
+    xHigh = getFullyConvertedUpperBounds(addExpr.getLValue()) and
+    yHigh = getFullyConvertedUpperBounds(addExpr.getRValue()) and
+    result = addRoundingUp(xHigh, yHigh))
+  or
+  exists (AssignSubExpr subExpr, float xHigh, float yLow
+  | expr = subExpr and
+    xHigh = getFullyConvertedUpperBounds(subExpr.getLValue()) and
+    yLow = getFullyConvertedLowerBounds(subExpr.getRValue()) and
+    result = addRoundingUp(xHigh, -yLow))
+  or
   exists (PrefixIncrExpr incrExpr, float xHigh
   | expr = incrExpr and
     xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
@@ -1156,7 +1203,7 @@ private cached module SimpleRangeAnalysisCached {
     // single minimum value.
     result = min(float lb | lb = getTruncatedLowerBounds(expr) | lb)
   }
-  
+
   /**
    * Gets the upper bound of the expression.
    *
@@ -1175,7 +1222,7 @@ private cached module SimpleRangeAnalysisCached {
     // single maximum value.
     result = max(float ub | ub = getTruncatedUpperBounds(expr) | ub)
   }
-  
+
   /**
    * Holds if `expr` has a provably empty range. For example:
    *
@@ -1204,13 +1251,13 @@ private cached module SimpleRangeAnalysisCached {
   predicate defMightOverflowNegatively(RangeSsaDefinition def, LocalScopeVariable v) {
     getDefLowerBoundsImpl(def, v) < varMinVal(v)
   }
-  
+
   /** Holds if the definition might overflow positively. */
   cached
   predicate defMightOverflowPositively(RangeSsaDefinition def, LocalScopeVariable v) {
     getDefUpperBoundsImpl(def, v) > varMaxVal(v)
   }
-  
+
   /**
    * Holds if the definition might overflow (either positively or
    * negatively).
@@ -1220,7 +1267,7 @@ private cached module SimpleRangeAnalysisCached {
     defMightOverflowNegatively(def, v) or
     defMightOverflowPositively(def, v)
   }
-  
+
   /**
    * Holds if the expression might overflow negatively. This predicate
    * does not consider the possibility that the expression might overflow
@@ -1228,9 +1275,14 @@ private cached module SimpleRangeAnalysisCached {
    */
   cached
   predicate exprMightOverflowNegatively(Expr expr) {
-    getLowerBoundsImpl(expr) < exprMinVal(expr)
+    getLowerBoundsImpl(expr) < exprMinVal(expr) or
+
+    // The lower bound of the expression `x--` is the same as the lower
+    // bound of `x`, so the standard logic (above) does not work for
+    // detecting whether it might overflow.
+    getLowerBoundsImpl(expr.(PostfixDecrExpr)) = exprMinVal(expr)
   }
-  
+
   /**
    * Holds if the expression might overflow negatively. Conversions
    * are also taken into account. For example the expression
@@ -1242,7 +1294,7 @@ private cached module SimpleRangeAnalysisCached {
     exprMightOverflowNegatively(expr) or
     convertedExprMightOverflowNegatively(expr.getConversion())
   }
-  
+
     /**
    * Holds if the expression might overflow positively. This predicate
    * does not consider the possibility that the expression might overflow
@@ -1250,9 +1302,14 @@ private cached module SimpleRangeAnalysisCached {
    */
   cached
   predicate exprMightOverflowPositively(Expr expr) {
-    getUpperBoundsImpl(expr) > exprMaxVal(expr)
+    getUpperBoundsImpl(expr) > exprMaxVal(expr) or
+
+    // The upper bound of the expression `x++` is the same as the upper
+    // bound of `x`, so the standard logic (above) does not work for
+    // detecting whether it might overflow.
+    getUpperBoundsImpl(expr.(PostfixIncrExpr)) = exprMaxVal(expr)
   }
-  
+
   /**
    * Holds if the expression might overflow positively. Conversions
    * are also taken into account. For example the expression
@@ -1264,7 +1321,7 @@ private cached module SimpleRangeAnalysisCached {
     exprMightOverflowPositively(expr) or
     convertedExprMightOverflowPositively(expr.getConversion())
   }
-  
+
   /**
    * Holds if the expression might overflow (either positively or
    * negatively). The possibility that the expression might overflow

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

@@ -423,6 +423,23 @@
 | test.c:398:22:398:22 | y | 5.0 |
 | test.c:399:10:399:11 | y1 | 1.0 |
 | test.c:399:15:399:16 | y2 | 5.0 |
+| test.c:407:3:407:3 | i | -2.147483648E9 |
+| test.c:408:7:408:7 | i | 10.0 |
+| test.c:410:3:410:3 | i | -2.147483648E9 |
+| test.c:411:3:411:3 | i | 10.0 |
+| test.c:412:7:412:7 | i | -2.147483648E9 |
+| test.c:414:3:414:3 | i | -2.147483648E9 |
+| test.c:415:3:415:3 | i | 40.0 |
+| test.c:416:7:416:7 | i | -2.147483648E9 |
+| test.c:418:3:418:3 | i | -2.147483648E9 |
+| test.c:418:7:418:7 | j | -2.147483648E9 |
+| test.c:419:7:419:7 | i | 40.0 |
+| test.c:421:3:421:3 | i | -2.147483648E9 |
+| test.c:421:8:421:8 | j | 40.0 |
+| test.c:422:7:422:7 | i | 50.0 |
+| 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.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

@@ -398,3 +398,29 @@ unsigned int test_comma01(unsigned int x) {
   y2 = (y++, y += 3, y);
   return y1 + y2;
 }
+
+void out(int i);
+
+void test17() {
+  int i, j;
+
+  i = 10;
+  out(i); // 10
+
+  i = 10;
+  i += 10;
+  out(i); // 20
+
+  i = 40;
+  i -= 10;
+  out(i); // 30
+
+  i = j = 40;
+  out(i); // 40
+
+  i = (j += 10);
+  out(i); // 50
+
+  i = 20 + (j -= 10);
+  out(i); // 60 [BUG: the analysis thinks it's 2^-31 .. 2^31-1]
+}

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

@@ -423,6 +423,23 @@
 | test.c:398:22:398:22 | y | 105.0 |
 | test.c:399:10:399:11 | y1 | 101.0 |
 | test.c:399:15:399:16 | y2 | 105.0 |
+| test.c:407:3:407:3 | i | 2.147483647E9 |
+| test.c:408:7:408:7 | i | 10.0 |
+| test.c:410:3:410:3 | i | 2.147483647E9 |
+| test.c:411:3:411:3 | i | 10.0 |
+| test.c:412:7:412:7 | i | 2.147483647E9 |
+| test.c:414:3:414:3 | i | 2.147483647E9 |
+| test.c:415:3:415:3 | i | 40.0 |
+| test.c:416:7:416:7 | i | 2.147483647E9 |
+| test.c:418:3:418:3 | i | 2.147483647E9 |
+| test.c:418:7:418:7 | j | 2.147483647E9 |
+| test.c:419:7:419:7 | i | 40.0 |
+| test.c:421:3:421:3 | i | 2.147483647E9 |
+| test.c:421:8:421:8 | j | 40.0 |
+| test.c:422:7:422:7 | i | 50.0 |
+| 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.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/Security/CWE/CWE-190/semmle/tainted/IntegerOverflowTainted.expected

@@ -2,3 +2,5 @@
 | test3.c:13:16:13:19 | * ... | $@ flows to here and is used in an expression which might overflow negatively. | test3.c:11:15:11:18 | argv | User-provided value |
 | test4.cpp:13:17:13:20 | access to array | $@ flows to here and is used in an expression which might overflow negatively. | test4.cpp:9:13:9:16 | argv | User-provided value |
 | test5.cpp:10:9:10:15 | call to strtoul | $@ flows to here and is used in an expression which might overflow. | test5.cpp:9:7:9:9 | buf | User-provided value |
+| test.c:44:7:44:12 | ... -- | $@ flows to here and is used in an expression which might overflow negatively. | test.c:41:17:41:20 | argv | User-provided value |
+| test.c:54:7:54:12 | ... -- | $@ flows to here and is used in an expression which might overflow negatively. | test.c:51:17:51:20 | argv | User-provided value |