C++: Improved query precision using SimpleRangeAnalysis

cpp/ql/src/Likely Bugs/Arithmetic/IntMultToLong.ql

@@ -18,6 +18,8 @@
 
 import cpp
 import semmle.code.cpp.controlflow.SSA
+import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
 /**
  * Holds if `e` is either:
@@ -64,29 +66,105 @@ int getEffectiveMulOperands(MulExpr me) {
     )
 }
 
-class LeafExpr extends Expr {
-  LeafExpr() { not this instanceof BinaryOperation }
+/**
+ * As SimpleRangeAnalysis does not support reasoning about multiplication
+ * we create a tiny abstract interpreter for handling multiplication, which
+ * we invoke only after weeding out of all of trivial cases that we do
+ * not care about. By default, the maximum and minimum values are computed
+ * using SimpleRangeAnalysis.
+ */
+class AnalyzableExpr extends Expr {
+  float maxValue() { result = upperBound(this.getFullyConverted()) }
+
+  float minValue() { result = lowerBound(this.getFullyConverted()) }
+}
+
+class ParenAnalyzableExpr extends AnalyzableExpr, ParenthesisExpr {
+  override float maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }
+
+  override float minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
+}
+
+class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
+  override float maxValue() {
+    exists(float x1, float y1, float x2, float y2 |
+      x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+      x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+      y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+      y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+      result = (x1 * y1).maximum(x1 * y2).maximum(x2 * y1).maximum(x2 * y2)
+    )
+  }
+
+  override float minValue() {
+    exists(float x1, float x2, float y1, float y2 |
+      x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+      x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+      y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+      y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+      result = (x1 * y1).minimum(x1 * y2).minimum(x2 * y1).minimum(x2 * y2)
+    )
+  }
+}
+
+class AddAnalyzableExpr extends AnalyzableExpr, AddExpr {
+  override float maxValue() {
+    result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() +
+        this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
+  }
+
+  override float minValue() {
+    result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() +
+        this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
+  }
+}
+
+class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
+  override float maxValue() {
+    result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() -
+        this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
+  }
+
+  override float minValue() {
+    result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() -
+        this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
+  }
+}
+
+class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
+  override float maxValue() {
+    exists(SsaDefinition def, Variable v |
+      def.getAUse(v) = this and
+      // if there is a defining expression, use that for
+      // computing the maximum value. Otherwise, assign the
+      // variable the largest possible value it can hold
+      if exists(def.getDefiningValue(v))
+      then result = def.getDefiningValue(v).(AnalyzableExpr).maxValue()
+      else result = exprMaxVal(this)
+    )
+  }
+
+  override float minValue() {
+    exists(SsaDefinition def, Variable v |
+      def.getAUse(v) = this and
+      if exists(def.getDefiningValue(v))
+      then result = def.getDefiningValue(v).(AnalyzableExpr).minValue()
+      else result = exprMinVal(this)
+    )
+  }
 }
 
 /**
- * Gets the size of the largest type (in bytes) of an non-literal
- * operand to a binary operation. For example, for
- * ```
- * unsigned char a; short b;
- * (a + 1) * b;
- * ```
- * the result is 2 (i.e., the size of a `short`)
+ * Holds if `t` is not an instance of `IntegralType`,
+ * or if `me` cannot be proven to not overflow
  */
-int widenedFromLiteralFromSize(Expr e) {
-  exists(Literal lit |
-    lit = e.(BinaryOperation).getAnOperand+() and
-    result = max(LeafExpr other |
-        other = e.(BinaryOperation).getAnOperand+() and
-        not other instanceof Literal
-      |
-        other.getType().getSize()
-      ) and
-    result < lit.getType().getSize()
+predicate overflows(MulExpr me, Type t) {
+  t instanceof IntegralType
+  implies
+  (
+    me.(MulAnalyzableExpr).maxValue() > exprMaxVal(me)
+    or
+    me.(MulAnalyzableExpr).minValue() < exprMinVal(me)
   )
 }
 
@@ -128,20 +206,10 @@ where
     ) and
     e.(Literal).getType().getSize() = t2.getSize()
   ) and
-  // exclude cases where the operands to the multiplication were
-  // small, but widened due to a literal in a subexpression.
-  // For instance, if the multiplication is
-  // ```
-  // int c = (a + 1) * (b + 1)
-  // ```
-  // where a and b are both unsigned chars. In this case the maximum
-  // value of c will be 256 * 256, even though the arguments to the
-  // multiplication are both typed as int.
-  not exists(Expr e1, Expr e2 |
-    e1 = me.getLeftOperand() and
-    e2 = me.getRightOperand() and
-    widenedFromLiteralFromSize(e1) + widenedFromLiteralFromSize(e2) < t1.getSize()
-  )
+  // only report if cannot prove that the result of the
+  // multiplication will be less (resp. greater) than the
+  // maximum (resp. minimum) number we can store.
+  overflows(me, t1)
 select me,
   "Multiplication result may overflow '" + me.getType().toString() + "' before it is converted to '"
     + me.getFullyConverted().getType().toString() + "'."

cpp/ql/test/query-tests/Likely Bugs/Arithmetic/IntMultToLong/IntMultToLong.expected

@@ -7,5 +7,6 @@
 | IntMultToLong.c:61:23:61:33 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'long long'. |
 | IntMultToLong.c:63:23:63:40 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'long long'. |
 | IntMultToLong.c:75:9:75:13 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'size_t'. |
-| IntMultToLong.c:99:9:99:25 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
-| IntMultToLong.c:103:9:103:31 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
+| IntMultToLong.c:99:14:99:35 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
+| IntMultToLong.c:103:14:103:46 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
+| IntMultToLong.c:108:14:108:78 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |