IntegerOverflow: recognise safe crements

Due to widening in loops, SimpleRangeAnalysis is overly cautious about
crement operations in loop updates. This commit makes some small
adjustments to identify "safe" crement operations that cannot overflow
due to the bounding by the loop counters.

Author: lcartey

cpp/autosar/test/rules/A4-7-1/IntegerExpressionLeadToDataLoss.expected

@@ -8,4 +8,5 @@
 | IntMultToLongc.cpp:109:13:109:28 | ... + ... | Binary expression ...+... may overflow. |
 | test.cpp:2:10:2:14 | ... + ... | Binary expression ...+... may overflow. |
 | test.cpp:22:12:22:16 | ... + ... | Binary expression ...+... may overflow. |
-| test.cpp:52:7:52:14 | ... + ... | Binary expression ...+... may overflow. |
+| test.cpp:50:7:50:14 | ... + ... | Binary expression ...+... may overflow. |
+| test.cpp:62:8:62:10 | ... ++ | Binary expression ...++... may overflow. |

cpp/autosar/test/rules/A4-7-1/test.cpp

@@ -35,21 +35,31 @@ short test_addition_invalid_overflow_check(short x, short y) {
   return 0;
 }
 
-void test_addition_loop_bound(unsigned int base, unsigned int size) {
-  if (size > 0) {
-    int n = size - 1;
-    for (int i = 0; i < n; i++) {
-      base + i; // COMPLIANT - `i` is bounded
+void test_addition_loop_bound(unsigned short base, unsigned int n) {
+  if (n < 1000) {
+    for (unsigned int i = 0; i < n; i++) { // COMPLIANT
+      base + i;                            // COMPLIANT - `i` is bounded
     }
   }
 }
 
-void test_addition_invalid_loop_bound(unsigned int base, unsigned int j,
-                                      unsigned int size) {
-  if (size > 0) {
-    int n = size - 1;
-    for (int i = 0; i < n; i++) {
+void test_addition_invalid_loop_bound(unsigned short base, unsigned int j,
+                                      unsigned int n) {
+  if (n < 1000) {
+    for (unsigned int i = 0; i < n; i++) { // COMPLIANT
       base + j; // NON_COMPLIANT - guards are not related
     }
   }
+}
+
+void test_loop_bound(unsigned int n) {
+  for (unsigned int i = 0; i < n; i++) { // COMPLIANT
+  }
+}
+
+void test_loop_bound_bad(unsigned int n) {
+  for (unsigned short i = 0; i < n;
+       i++) { // NON_COMPLIANT - crement will overflow before loop bound is
+              // reached
+  }
 }

cpp/common/src/codingstandards/cpp/Overflow.qll

@@ -33,6 +33,8 @@ class InterestingOverflowingOperation extends Operation {
     // Multiplication is not covered by the standard range analysis library, so implement our own
     // mini analysis.
     (this instanceof MulExpr implies MulExprAnalysis::overflows(this)) and
+    // This shouldn't be a "safe" crement operation
+    not LoopCounterAnalysis::isCrementSafeFromOverflow(this) and
     // Not within a macro
     not this.isAffectedByMacro() and
     // Ignore pointer arithmetic
@@ -328,3 +330,68 @@ private module MulExprAnalysis {
     me.(MulAnalyzableExpr).minValue() < exprMinVal(me)
   }
 }
+
+/**
+ * An analysis on safe loop counters.
+ */
+module LoopCounterAnalysis {
+  newtype LoopBound =
+    LoopUpperBound() or
+    LoopLowerBound()
+
+  predicate isLoopBounded(
+    CrementOperation cop, ForStmt fs, Variable loopCounter, Expr initializer, Expr counterBound,
+    LoopBound boundKind, boolean equals
+  ) {
+    // Initialization sets the loop counter
+    (
+      loopCounter = fs.getInitialization().(DeclStmt).getADeclaration() and
+      initializer = loopCounter.getInitializer().getExpr()
+      or
+      loopCounter.getAnAssignment() = initializer and
+      initializer = fs.getInitialization().(ExprStmt).getExpr()
+    ) and
+    // Condition is a relation operation on the loop counter
+    exists(RelationalOperation relOp |
+      fs.getCondition() = relOp and
+      (if relOp.getOperator().charAt(1) = "=" then equals = true else equals = false)
+    |
+      relOp.getGreaterOperand() = loopCounter.getAnAccess() and
+      relOp.getLesserOperand() = counterBound and
+      cop instanceof DecrementOperation and
+      boundKind = LoopLowerBound()
+      or
+      relOp.getLesserOperand() = loopCounter.getAnAccess() and
+      relOp.getGreaterOperand() = counterBound and
+      cop instanceof IncrementOperation and
+      boundKind = LoopUpperBound()
+    ) and
+    // Update is a crement operation with the loop counter
+    fs.getUpdate() = cop and
+    cop.getOperand() = loopCounter.getAnAccess()
+  }
+
+  /**
+   * Holds if the crement operation is safe from under/overflow.
+   */
+  predicate isCrementSafeFromOverflow(CrementOperation op) {
+    exists(
+      Expr initializer, Expr counterBound, LoopBound boundKind, boolean equals, int equalsOffset
+    |
+      isLoopBounded(op, _, _, initializer, counterBound, boundKind, equals) and
+      (
+        equals = true and equalsOffset = 1
+        or
+        equals = false and equalsOffset = 0
+      )
+    |
+      boundKind = LoopUpperBound() and
+      // upper bound of the inccrement is smaller than the maximum value representable in the type
+      upperBound(counterBound) + equalsOffset <= typeUpperBound(op.getType().getUnspecifiedType())
+      or
+      // the lower bound of the decrement is larger than the smal
+      boundKind = LoopLowerBound() and
+      lowerBound(counterBound) - equalsOffset >= typeLowerBound(op.getType().getUnspecifiedType())
+    )
+  }
+}