C++: add reason to buffer write estimations

Author: redsun82

cpp/ql/lib/semmle/code/cpp/commons/Printf.qll

@@ -9,6 +9,30 @@ import semmle.code.cpp.models.interfaces.FormattingFunction
 private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
+private newtype TBufferWriteEstimationReason =
+  TTypeBoundsAnalysis() or
+  TValueFlowAnalysis()
+
+class BufferWriteEstimationReason extends TBufferWriteEstimationReason {
+  BufferWriteEstimationReason() {
+    this = TTypeBoundsAnalysis() or
+    this = TValueFlowAnalysis()
+  }
+
+  string toString() {
+    this = TTypeBoundsAnalysis() and result = "based on type bounds" or
+    this = TValueFlowAnalysis() and result = "based on flow analysis of value bounds"
+  }
+
+  BufferWriteEstimationReason combineWith(BufferWriteEstimationReason other) {
+    (this = TTypeBoundsAnalysis() or other = TTypeBoundsAnalysis()) and result = TTypeBoundsAnalysis() or
+    (this = TValueFlowAnalysis() and other = TValueFlowAnalysis()) and result = TValueFlowAnalysis()
+  }
+}
+
+BufferWriteEstimationReason typeBoundsAnalysis() { result = TTypeBoundsAnalysis() }
+BufferWriteEstimationReason valueFlowAnalysis() { result = TValueFlowAnalysis() }
+
 class PrintfFormatAttribute extends FormatAttribute {
   PrintfFormatAttribute() { this.getArchetype() = ["printf", "__printf__"] }
 }
@@ -990,7 +1014,7 @@ class FormatLiteral extends Literal {
    * conversion specifier of this format string; has no result if this cannot
    * be determined.
    */
-  int getMaxConvertedLength(int n) {
+  int getMaxConvertedLength(int n, BufferWriteEstimationReason reason) {
     exists(int len |
       (
         (
@@ -1002,10 +1026,10 @@ class FormatLiteral extends Literal {
       ) and
       (
         this.getConversionChar(n) = "%" and
-        len = 1
+        len = 1 and reason = TValueFlowAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "c" and
-        len = 1 // e.g. 'a'
+        len = 1 and reason = TValueFlowAnalysis() // e.g. 'a'
         or
         this.getConversionChar(n).toLowerCase() = "f" and
         exists(int dot, int afterdot |
@@ -1019,7 +1043,7 @@ class FormatLiteral extends Literal {
             afterdot = 6
           ) and
           len = 1 + 309 + dot + afterdot
-        ) // e.g. -1e308="-100000"...
+        ) and reason = TTypeBoundsAnalysis() // e.g. -1e308="-100000"...
         or
         this.getConversionChar(n).toLowerCase() = "e" and
         exists(int dot, int afterdot |
@@ -1033,7 +1057,7 @@ class FormatLiteral extends Literal {
             afterdot = 6
           ) and
           len = 1 + 1 + dot + afterdot + 1 + 1 + 3
-        ) // -1e308="-1.000000e+308"
+        ) and reason = TTypeBoundsAnalysis() // -1e308="-1.000000e+308"
         or
         this.getConversionChar(n).toLowerCase() = "g" and
         exists(int dot, int afterdot |
@@ -1056,67 +1080,78 @@ class FormatLiteral extends Literal {
           //       (e.g. 123456, 0.000123456 are just OK)
           //       so case %f can be at most P characters + 4 zeroes, sign, dot = P + 6
           len = (afterdot.maximum(1) + 6).maximum(1 + 1 + dot + afterdot + 1 + 1 + 3)
-        ) // (e.g. "-1.59203e-319")
+        ) and reason = TTypeBoundsAnalysis() // (e.g. "-1.59203e-319")
         or
         this.getConversionChar(n).toLowerCase() = ["d", "i"] and
         // e.g. -2^31 = "-2147483648"
-        len =
-          min(float cand |
+        exists(float typeBasedBound, float valueBasedBound |
             // The first case handles length sub-specifiers
             // Subtract one in the exponent because one bit is for the sign.
             // Add 1 to account for the possible sign in the output.
-            cand = 1 + lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8 - 1))
-            or
+            typeBasedBound = 1 + lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8 - 1)) and
             // The second case uses range analysis to deduce a length that's shorter than the length
             // of the number -2^31.
-            exists(Expr arg, float lower, float upper |
+            exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
               arg = this.getUse().getConversionArgument(n) and
               lower = lowerBound(arg.getFullyConverted()) and
-              upper = upperBound(arg.getFullyConverted())
+              upper = upperBound(arg.getFullyConverted()) and
+              typeLower = exprMinVal(arg.getFullyConverted()) and
+              typeUpper = exprMaxVal(arg.getFullyConverted()) 
             |
-              cand =
-                max(int cand0 |
+              valueBasedBound =
+                max(int cand |
                   // Include the sign bit in the length if it can be negative
                   (
                     if lower < 0
-                    then cand0 = 1 + lengthInBase10(lower.abs())
-                    else cand0 = lengthInBase10(lower)
+                    then cand = 1 + lengthInBase10(lower.abs())
+                    else cand = lengthInBase10(lower)
                   )
                   or
                   (
                     if upper < 0
-                    then cand0 = 1 + lengthInBase10(upper.abs())
-                    else cand0 = lengthInBase10(upper)
+                    then cand = 1 + lengthInBase10(upper.abs())
+                    else cand = lengthInBase10(upper)
                   )
-                )
-            )
-          )
+                ) and
+              (
+                if lower > typeLower or upper < typeUpper
+                then reason = TValueFlowAnalysis()
+                else reason = TTypeBoundsAnalysis()
+              )
+            ) and
+            len = valueBasedBound.minimum(typeBasedBound)
+        )
         or
         this.getConversionChar(n).toLowerCase() = "u" and
         // e.g. 2^32 - 1 = "4294967295"
-        len =
-          min(float cand |
+        exists(float typeBasedBound, float valueBasedBound |
             // The first case handles length sub-specifiers
-            cand = 2.pow(this.getIntegralDisplayType(n).getSize() * 8)
-            or
+            typeBasedBound = lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8) - 1) and
             // The second case uses range analysis to deduce a length that's shorter than
             // the length of the number 2^31 - 1.
-            exists(Expr arg, float lower |
+            exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
               arg = this.getUse().getConversionArgument(n) and
-              lower = lowerBound(arg.getFullyConverted())
+              lower = lowerBound(arg.getFullyConverted()) and
+              upper = upperBound(arg.getFullyConverted()) and
+              typeLower = exprMinVal(arg.getFullyConverted()) and
+              typeUpper = exprMaxVal(arg.getFullyConverted()) 
             |
-              cand =
-                max(float cand0 |
+              valueBasedBound =
+                lengthInBase10(max(float cand |
                   // If lower can be negative we use `(unsigned)-1` as the candidate value.
                   lower < 0 and
-                  cand0 = 2.pow(any(IntType t | t.isUnsigned()).getSize() * 8)
+                  cand = 2.pow(any(IntType t | t.isUnsigned()).getSize() * 8)
                   or
-                  cand0 = upperBound(arg.getFullyConverted())
-                )
-            )
-          |
-            lengthInBase10(cand)
-          )
+                  cand = upper
+                )) and
+              (
+                if lower > typeLower or upper < typeUpper
+                then reason = TValueFlowAnalysis()
+                else reason = TTypeBoundsAnalysis()
+              )
+            ) and
+            len = valueBasedBound.minimum(typeBasedBound)
+        )
         or
         this.getConversionChar(n).toLowerCase() = "x" and
         // e.g. "12345678"
@@ -1135,7 +1170,7 @@ class FormatLiteral extends Literal {
           (
             if this.hasAlternateFlag(n) then len = 2 + baseLen else len = baseLen // "0x"
           )
-        )
+        ) and reason = TTypeBoundsAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "p" and
         exists(PointerType ptrType, int baseLen |
@@ -1144,7 +1179,7 @@ class FormatLiteral extends Literal {
           (
             if this.hasAlternateFlag(n) then len = 2 + baseLen else len = baseLen // "0x"
           )
-        )
+        ) and reason = TValueFlowAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "o" and
         // e.g. 2^32 - 1 = "37777777777"
@@ -1163,14 +1198,15 @@ class FormatLiteral extends Literal {
           (
             if this.hasAlternateFlag(n) then len = 1 + baseLen else len = baseLen // "0"
           )
-        )
+        ) and reason = TTypeBoundsAnalysis()
         or
         this.getConversionChar(n).toLowerCase() = "s" and
         len =
           min(int v |
             v = this.getPrecision(n) or
             v = this.getUse().getFormatArgument(n).(AnalysedString).getMaxLength() - 1 // (don't count null terminator)
-          )
+          ) and
+        reason = TValueFlowAnalysis()
       )
     )
   }
@@ -1182,10 +1218,10 @@ class FormatLiteral extends Literal {
    * determining whether a buffer overflow is caused by long float to string
    * conversions.
    */
-  int getMaxConvertedLengthLimited(int n) {
+  int getMaxConvertedLengthLimited(int n, BufferWriteEstimationReason reason) {
     if this.getConversionChar(n).toLowerCase() = "f"
-    then result = this.getMaxConvertedLength(n).minimum(8)
-    else result = this.getMaxConvertedLength(n)
+    then result = this.getMaxConvertedLength(n, reason).minimum(8)
+    else result = this.getMaxConvertedLength(n, reason)
   }
 
   /**
@@ -1225,35 +1261,49 @@ class FormatLiteral extends Literal {
     )
   }
 
-  private int getMaxConvertedLengthAfter(int n) {
+  private int getMaxConvertedLengthAfter(int n, BufferWriteEstimationReason reason) {
     if n = this.getNumConvSpec()
-    then result = this.getConstantSuffix().length() + 1
+    then result = this.getConstantSuffix().length() + 1 and reason = TValueFlowAnalysis()
     else
-      result =
-        this.getConstantPart(n).length() + this.getMaxConvertedLength(n) +
-          this.getMaxConvertedLengthAfter(n + 1)
+      exists(BufferWriteEstimationReason headReason, BufferWriteEstimationReason tailReason |
+        result =
+          this.getConstantPart(n).length() + this.getMaxConvertedLength(n, headReason) +
+            this.getMaxConvertedLengthAfter(n + 1, tailReason) and
+            reason = headReason.combineWith(tailReason)
+      )
   }
 
-  private int getMaxConvertedLengthAfterLimited(int n) {
+  private int getMaxConvertedLengthAfterLimited(int n, BufferWriteEstimationReason reason) {
     if n = this.getNumConvSpec()
-    then result = this.getConstantSuffix().length() + 1
+    then result = this.getConstantSuffix().length() + 1 and reason = TValueFlowAnalysis()
     else
+    exists(BufferWriteEstimationReason headReason, BufferWriteEstimationReason tailReason |
       result =
-        this.getConstantPart(n).length() + this.getMaxConvertedLengthLimited(n) +
-          this.getMaxConvertedLengthAfterLimited(n + 1)
+        this.getConstantPart(n).length() + this.getMaxConvertedLengthLimited(n, headReason) +
+          this.getMaxConvertedLengthAfterLimited(n + 1, tailReason) and
+          reason = headReason.combineWith(tailReason)
+    )
   }
 
   /**
    * Gets the maximum length of the string that can be produced by this format
    * string.  Has no result if this cannot be determined.
    */
-  int getMaxConvertedLength() { result = this.getMaxConvertedLengthAfter(0) }
+  int getMaxConvertedLength() { result = this.getMaxConvertedLengthAfter(0, _) }
 
   /**
    * Gets the maximum length of the string that can be produced by this format
    * string, except that float to string conversions are assumed to be 8
    * characters.  This is helpful for determining whether a buffer overflow
    * is caused by long float to string conversions.
    */
-  int getMaxConvertedLengthLimited() { result = this.getMaxConvertedLengthAfterLimited(0) }
+  int getMaxConvertedLengthLimited() { result = this.getMaxConvertedLengthAfterLimited(0, _) }
+
+  int getMaxConvertedLengthWithReason(BufferWriteEstimationReason reason) {
+    result = this.getMaxConvertedLengthAfter(0, reason)
+  }
+
+  int getMaxConvertedLengthLimitedWithReason(BufferWriteEstimationReason reason) {
+    result = this.getMaxConvertedLengthAfterLimited(0, reason)
+  }
 }