Resolve FP reported in 396

c/cert/src/rules/INT34-C/ExprShiftedbyNegativeOrGreaterPrecisionOperand.ql

@@ -15,91 +15,8 @@ import codingstandards.c.cert
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 import semmle.code.cpp.valuenumbering.GlobalValueNumbering
 import semmle.code.cpp.controlflow.Guards
+import codingstandards.cpp.UndefinedBehavior
 
-/*
- * Precision predicate based on a sample implementation from
- * https://wiki.sei.cmu.edu/confluence/display/c/INT35-C.+Use+correct+integer+precisions
- */
-
-/**
- * A function whose name is suggestive that it counts the number of bits set.
- */
-class PopCount extends Function {
-  PopCount() { this.getName().toLowerCase().matches("%popc%nt%") }
-}
-
-/**
- * A macro which is suggestive that it is used to determine the precision of an integer.
- */
-class PrecisionMacro extends Macro {
-  PrecisionMacro() { this.getName().toLowerCase().matches("precision") }
-}
-
-class LiteralZero extends Literal {
-  LiteralZero() { this.getValue() = "0" }
-}
-
-class BitShiftExpr extends BinaryBitwiseOperation {
-  BitShiftExpr() {
-    this instanceof LShiftExpr or
-    this instanceof RShiftExpr
-  }
-}
-
-int getPrecision(IntegralType type) {
-  type.isExplicitlyUnsigned() and result = type.getSize() * 8
-  or
-  type.isExplicitlySigned() and result = type.getSize() * 8 - 1
-}
-
-predicate isForbiddenShiftExpr(BitShiftExpr shift, string message) {
-  (
-    (
-      getPrecision(shift.getLeftOperand().getExplicitlyConverted().getUnderlyingType()) <=
-        upperBound(shift.getRightOperand()) and
-      message =
-        "The operand " + shift.getLeftOperand() + " is shifted by an expression " +
-          shift.getRightOperand() + " whose upper bound (" + upperBound(shift.getRightOperand()) +
-          ") is greater than or equal to the precision."
-      or
-      lowerBound(shift.getRightOperand()) < 0 and
-      message =
-        "The operand " + shift.getLeftOperand() + " is shifted by an expression " +
-          shift.getRightOperand() + " which may be negative."
-    ) and
-    /*
-     * Shift statement is not at a basic block where
-     * `shift_rhs < PRECISION(...)` is ensured
-     */
-
-    not exists(GuardCondition gc, BasicBlock block, Expr precisionCall, Expr lTLhs |
-      block = shift.getBasicBlock() and
-      (
-        precisionCall.(FunctionCall).getTarget() instanceof PopCount
-        or
-        precisionCall = any(PrecisionMacro pm).getAnInvocation().getExpr()
-      )
-    |
-      globalValueNumber(lTLhs) = globalValueNumber(shift.getRightOperand()) and
-      gc.ensuresLt(lTLhs, precisionCall, 0, block, true)
-    ) and
-    /*
-     * Shift statement is not at a basic block where
-     * `shift_rhs < 0` is ensured
-     */
-
-    not exists(GuardCondition gc, BasicBlock block, Expr literalZero, Expr lTLhs |
-      block = shift.getBasicBlock() and
-      literalZero instanceof LiteralZero
-    |
-      globalValueNumber(lTLhs) = globalValueNumber(shift.getRightOperand()) and
-      gc.ensuresLt(lTLhs, literalZero, 0, block, true)
-    )
-  )
-}
-
-from BinaryBitwiseOperation badShift, string message
-where
-  not isExcluded(badShift, Types1Package::exprShiftedbyNegativeOrGreaterPrecisionOperandQuery()) and
-  isForbiddenShiftExpr(badShift, message)
-select badShift, message
+from ShiftByNegativeOrGreaterPrecisionOperand badShift
+where not isExcluded(badShift, Types1Package::exprShiftedbyNegativeOrGreaterPrecisionOperandQuery())
+select badShift, badShift.getReason()

c/common/src/codingstandards/c/UndefinedBehavior.qll

@@ -25,4 +25,9 @@ class CUndefinedMainDefinition extends CUndefinedBehavior, Function {
     (this.getName() = "main" or this.getName().indexOf("____codeql_coding_standards") = 0) and
     not this instanceof C99MainFunction
   }
+
+  override string getReason() {
+    result =
+      "The behavior of the program is undefined because the main function is not defined according to the C standard."
+  }
 }

change_notes/2024-02-21-fix-reported-fp-a4-7-1.md

@@ -0,0 +1,4 @@
+- `A4-7-1` -  `IntegerExpressionLeadToDataLoss.ql`:
+    - Address reported FP in #396. Exclude shift operations guarded to prevent undefined behavior that could lead to dataloss. 
+- `INT34-C` - `ExprShiftedbyNegativeOrGreaterPrecisionOperand.ql`:
+  - Format the alert message according to the style-guide.

cpp/autosar/src/rules/M0-1-4/SingleUsePODVariable.qll

@@ -11,7 +11,7 @@ private string getConstExprValue(Variable v) {
 }
 
 /**
- * Gets the number of uses of variable `v` in an opaque assignment, where an opaqua assignment for example a cast from one type to the other and `v` is assumed to be a member of the resulting type.
+ * Gets the number of uses of variable `v` in an opaque assignment, where an opaque assignment is a cast from one type to the other, and `v` is assumed to be a member of the resulting type.
  * e.g.,
  * struct foo {
  *  int bar;
@@ -42,7 +42,7 @@ Expr getIndirectSubObjectAssignedValue(MemberVariable subobject) {
       result = externalInitializerCall
     )
     or
-    // the object this subject is part of is initialized and we assumes this initializes the subobject.
+    // the object this subject is part of is initialized and we assume this initializes the subobject.
     instanceOfSomeStruct.getType() = someStruct and
     result = instanceOfSomeStruct.getInitializer().getExpr()
   )

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

@@ -10,3 +10,6 @@
 | test.cpp:22:12:22:16 | ... + ... | Binary expression ...+... may overflow. |
 | test.cpp:50:7:50:14 | ... + ... | Binary expression ...+... may overflow. |
 | test.cpp:62:8:62:10 | ... ++ | Binary expression ...++... may overflow. |
+| test.cpp:91:10:91:17 | ... << ... | Binary expression ...<<... may overflow. |
+| test.cpp:95:10:95:17 | ... << ... | Binary expression ...<<... may overflow. |
+| test.cpp:98:8:98:15 | ... << ... | Binary expression ...<<... may overflow. |

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

@@ -72,4 +72,29 @@ void test_pointer() {
   int *p = nullptr;
   p++; // COMPLIANT - not covered by this rule
   p--; // COMPLIANT - not covered by this rule
+}
+
+extern unsigned int popcount(unsigned int);
+#define PRECISION(x) popcount(x)
+void test_guarded_shifts(unsigned int p1, int p2) {
+  unsigned int l1;
+
+  if (p2 < popcount(p1) && p2 > 0) {
+    l1 = p1 << p2; // COMPLIANT
+  }
+
+  if (p2 < PRECISION(p1) && p2 > 0) {
+    l1 = p1 << p2; // COMPLIANT
+  }
+
+  if (p2 < popcount(p1)) {
+    l1 = p1 << p2; // NON_COMPLIANT - p2 could be negative
+  }
+
+  if (p2 > 0) {
+    l1 = p1 << p2; // NON_COMPLIANT - p2 could have a higher precision
+  }
+
+  l1 = p1 << p2; // NON_COMPLIANT - p2 may have a higher precision or could be
+                 // negative
 }

cpp/common/src/codingstandards/cpp/Expr.qll

@@ -203,3 +203,11 @@ class UnevaluatedExprExtension extends Expr {
     )
   }
 }
+
+/** A class representing left and right bitwise shift operations. */
+class BitShiftExpr extends BinaryBitwiseOperation {
+  BitShiftExpr() {
+    this instanceof LShiftExpr or
+    this instanceof RShiftExpr
+  }
+}

cpp/common/src/codingstandards/cpp/Function.qll

@@ -0,0 +1,10 @@
+/** A module to reason about functions, such as well-known functions. */
+
+import cpp
+
+/**
+ * A function whose name is suggestive that it counts the number of bits set.
+ */
+class PopCount extends Function {
+  PopCount() { this.getName().toLowerCase().matches("%popc%nt%") }
+}

cpp/common/src/codingstandards/cpp/Literals.qll

@@ -30,6 +30,10 @@ class Utf32StringLiteral extends StringLiteral {
   Utf32StringLiteral() { this.getValueText().regexpMatch("(?s)\\s*U\".*") }
 }
 
+class LiteralZero extends Literal {
+  LiteralZero() { this.getValue() = "0" }
+}
+
 /**
  * A literal resulting from the use of a constexpr
  * variable, or macro expansion.

cpp/common/src/codingstandards/cpp/Macro.qll

@@ -88,3 +88,10 @@ class UserProvidedMacro extends Macro {
 class LibraryMacro extends Macro {
   LibraryMacro() { not this instanceof UserProvidedMacro }
 }
+
+/**
+ * A macro which is suggestive that it is used to determine the precision of an integer.
+ */
+class PrecisionMacro extends Macro {
+  PrecisionMacro() { this.getName().toLowerCase().matches("precision") }
+}

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

@@ -8,6 +8,8 @@ import SimpleRangeAnalysisCustomizations
 import semmle.code.cpp.controlflow.Guards
 import codingstandards.cpp.dataflow.TaintTracking
 import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+import codingstandards.cpp.Expr
+import codingstandards.cpp.UndefinedBehavior
 
 /**
  * An integer operation that may overflow, underflow or wrap.
@@ -40,7 +42,9 @@ class InterestingOverflowingOperation extends Operation {
     // Not within a macro
     not this.isAffectedByMacro() and
     // Ignore pointer arithmetic
-    not this instanceof PointerArithmeticOperation
+    not this instanceof PointerArithmeticOperation and
+    // In case of the shift operation, it must cause undefined behavior
+    (this instanceof BitShiftExpr implies this instanceof ShiftByNegativeOrGreaterPrecisionOperand)
   }
 
   /**

cpp/common/src/codingstandards/cpp/Type.qll

@@ -59,3 +59,14 @@ Type stripSpecifiers(Type type) {
   then result = stripSpecifiers(type.(SpecifiedType).getBaseType())
   else result = type
 }
+
+/**
+ * Get the precision of an integral type, where precision is defined as the number of bits
+ * that can be used to represent the numeric value.
+ * https://wiki.sei.cmu.edu/confluence/display/c/INT35-C.+Use+correct+integer+precisions
+ */
+int getPrecision(IntegralType type) {
+  type.isExplicitlyUnsigned() and result = type.getSize() * 8
+  or
+  type.isExplicitlySigned() and result = type.getSize() * 8 - 1
+}

cpp/common/src/codingstandards/cpp/UndefinedBehavior.qll

@@ -1,8 +1,65 @@
 import cpp
+import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+import semmle.code.cpp.controlflow.Guards
+import codingstandards.cpp.Literals
+import codingstandards.cpp.Expr
+import codingstandards.cpp.Macro
+import codingstandards.cpp.Type
+import codingstandards.cpp.Function
 
 /**
  * Library for modeling undefined behavior.
  */
-abstract class UndefinedBehavior extends Locatable { }
+abstract class UndefinedBehavior extends Locatable {
+  abstract string getReason();
+}
 
 abstract class CPPUndefinedBehavior extends UndefinedBehavior { }
+
+class ShiftByNegativeOrGreaterPrecisionOperand extends UndefinedBehavior, BitShiftExpr {
+  string reason;
+
+  ShiftByNegativeOrGreaterPrecisionOperand() {
+    getPrecision(this.getLeftOperand().getExplicitlyConverted().getUnderlyingType()) <=
+      upperBound(this.getRightOperand()) and
+    reason =
+      "The operand  '" + this.getLeftOperand() + "' is shifted by an expression '" +
+        this.getRightOperand() + "' whose upper bound (" + upperBound(this.getRightOperand()) +
+        ") is greater than or equal to the precision." and
+    /*
+     * this statement is not at a basic block where
+     * `this_rhs < PRECISION(...)` is ensured
+     */
+
+    not exists(GuardCondition gc, BasicBlock block, Expr precisionCall, Expr lTLhs |
+      block = this.getBasicBlock() and
+      (
+        precisionCall.(FunctionCall).getTarget() instanceof PopCount
+        or
+        precisionCall = any(PrecisionMacro pm).getAnInvocation().getExpr()
+      )
+    |
+      globalValueNumber(lTLhs) = globalValueNumber(this.getRightOperand()) and
+      gc.ensuresLt(lTLhs, precisionCall, 0, block, true)
+    )
+    or
+    lowerBound(this.getRightOperand()) < 0 and
+    reason =
+      "The operand '" + this.getLeftOperand() + "' is shifted by an expression '" +
+        this.getRightOperand() + "' which may be negative." and
+    /*
+     * this statement is not at a basic block where
+     * `this_rhs > 0` is ensured
+     */
+
+    not exists(GuardCondition gc, BasicBlock block, Expr literalZero, Expr lTLhs |
+      block = this.getBasicBlock() and
+      literalZero instanceof LiteralZero and
+      globalValueNumber(lTLhs) = globalValueNumber(this.getRightOperand()) and
+      gc.ensuresLt(literalZero, lTLhs, 0, block, true)
+    )
+  }
+
+  override string getReason() { result = reason }
+}