Merge branch 'main' into mathiasvp/replace-ast-with-ir-use-usedataflow

cpp/ql/lib/change-notes/2022-10-22-format-literal.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* Fixed bugs in the `FormatLiteral` class that were causing `getMaxConvertedLength` and related predicates to return no results when the format literal was `%e`, `%f` or `%g` and an explicit precision was specified.

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/ModulusAnalysis.qll

@@ -4,6 +4,12 @@
  * variable), and `v` is an integer in the range `[0 .. m-1]`.
  */
 
+/*
+ * The main recursion has base cases in both `ssaModulus` (for guarded reads) and `semExprModulus`
+ * (for constant values). The most interesting recursive case is `phiModulusRankStep`, which
+ * handles phi inputs.
+ */
+
 private import ModulusAnalysisSpecific::Private
 private import experimental.semmle.code.cpp.semantic.Semantic
 private import ConstantAnalysis
@@ -162,6 +168,11 @@ private predicate phiModulusInit(SemSsaPhiNode phi, SemBound b, int val, int mod
  */
 pragma[nomagic]
 private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int mod, int rix) {
+  /*
+   * base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence
+   * class for the phi node.
+   */
+
   rix = 0 and
   phiModulusInit(phi, b, val, mod)
   or
@@ -169,6 +180,12 @@ private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int
     mod != 1 and
     val = remainder(v1, mod)
   |
+    /*
+     * Recursive case. If `inp` = `b + v2` mod `m2`, we combine that with the preceding potential
+     * congruence class `b + v1` mod `m1`. The result will be the congruence class of `v1` modulo
+     * the greatest common denominator of `m1`, `m2`, and `v1 - v2`.
+     */
+
     exists(int v2, int m2 |
       rankedPhiInput(pragma[only_bind_out](phi), inp, edge, rix) and
       phiModulusRankStep(phi, b, v1, m1, rix - 1) and
@@ -176,6 +193,12 @@ private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int
       mod = m1.gcd(m2).gcd(v1 - v2)
     )
     or
+    /*
+     * Recursive case. If `inp` = `phi` mod `m2`, we combine that with the preceding potential
+     * congruence class `b + v1` mod `m1`. The result will be a congruence class modulo the greatest
+     * common denominator of `m1` and `m2`.
+     */
+
     exists(int m2 |
       rankedPhiInput(phi, inp, edge, rix) and
       phiModulusRankStep(phi, b, v1, m1, rix - 1) and

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

@@ -1125,12 +1125,12 @@ class FormatLiteral extends Literal {
         exists(int dot, int afterdot |
           (if this.getPrecision(n) = 0 then dot = 0 else dot = 1) and
           (
-            (
-              if this.hasExplicitPrecision(n)
-              then afterdot = this.getPrecision(n)
-              else not this.hasImplicitPrecision(n)
-            ) and
-            afterdot = 6
+            if this.hasExplicitPrecision(n)
+            then afterdot = this.getPrecision(n)
+            else (
+              not this.hasImplicitPrecision(n) and
+              afterdot = 6
+            )
           ) and
           len = 1 + 309 + dot + afterdot
         ) and
@@ -1140,12 +1140,12 @@ class FormatLiteral extends Literal {
         exists(int dot, int afterdot |
           (if this.getPrecision(n) = 0 then dot = 0 else dot = 1) and
           (
-            (
-              if this.hasExplicitPrecision(n)
-              then afterdot = this.getPrecision(n)
-              else not this.hasImplicitPrecision(n)
-            ) and
-            afterdot = 6
+            if this.hasExplicitPrecision(n)
+            then afterdot = this.getPrecision(n)
+            else (
+              not this.hasImplicitPrecision(n) and
+              afterdot = 6
+            )
           ) and
           len = 1 + 1 + dot + afterdot + 1 + 1 + 3
         ) and
@@ -1155,12 +1155,12 @@ class FormatLiteral extends Literal {
         exists(int dot, int afterdot |
           (if this.getPrecision(n) = 0 then dot = 0 else dot = 1) and
           (
-            (
-              if this.hasExplicitPrecision(n)
-              then afterdot = this.getPrecision(n)
-              else not this.hasImplicitPrecision(n)
-            ) and
-            afterdot = 6
+            if this.hasExplicitPrecision(n)
+            then afterdot = this.getPrecision(n)
+            else (
+              not this.hasImplicitPrecision(n) and
+              afterdot = 6
+            )
           ) and
           // note: this could be displayed in the style %e or %f;
           //       however %f is only used when 'P > X >= -4'