Michaelrfairhurst/address rule amendments from amd3

amendments.csv

@@ -1,14 +1,14 @@
 language,standard,amendment,rule_id,supportable,implementation_category,implemented,difficulty
-c,MISRA-C-2012,Amendment3,DIR-4-6,Yes,Expand,No,Easy
+c,MISRA-C-2012,Amendment3,DIR-4-6,Yes,Expand,Yes,Easy
 c,MISRA-C-2012,Amendment3,DIR-4-9,Yes,Refine,No,Easy
 c,MISRA-C-2012,Amendment3,DIR-4-11,Yes,Refine,No,Import
-c,MISRA-C-2012,Amendment3,RULE-1-4,Yes,Replace,No,Easy
-c,MISRA-C-2012,Amendment3,RULE-10-1,Yes,Replace,No,Easy
-c,MISRA-C-2012,Amendment3,RULE-10-3,Yes,Refine,No,Easy
-c,MISRA-C-2012,Amendment3,RULE-10-4,Yes,Refine,No,Import
-c,MISRA-C-2012,Amendment3,RULE-10-5,Yes,Expand,No,Easy
-c,MISRA-C-2012,Amendment3,RULE-10-7,Yes,Refine,No,Import
-c,MISRA-C-2012,Amendment3,RULE-10-8,Yes,Refine,No,Import
+c,MISRA-C-2012,Amendment3,RULE-1-4,Yes,Replace,Yes,Easy
+c,MISRA-C-2012,Amendment3,RULE-10-1,Yes,Replace,Yes,Easy
+c,MISRA-C-2012,Amendment3,RULE-10-3,Yes,Refine,Yes,Easy
+c,MISRA-C-2012,Amendment3,RULE-10-4,Yes,Refine,Yes,Import
+c,MISRA-C-2012,Amendment3,RULE-10-5,Yes,Expand,Yes,Easy
+c,MISRA-C-2012,Amendment3,RULE-10-7,Yes,Refine,Yes,Import
+c,MISRA-C-2012,Amendment3,RULE-10-8,Yes,Refine,Yes,Import
 c,MISRA-C-2012,Amendment3,RULE-21-11,Yes,Clarification,No,Import
 c,MISRA-C-2012,Amendment3,RULE-21-12,Yes,Replace,No,Easy
 c,MISRA-C-2012,Amendment4,RULE-11-3,Yes,Expand,No,Easy
@@ -24,7 +24,7 @@ c,MISRA-C-2012,Corrigendum2,RULE-8-9,Yes,Clarification,No,Import
 c,MISRA-C-2012,Corrigendum2,RULE-9-4,Yes,Clarification,No,Import
 c,MISRA-C-2012,Corrigendum2,RULE-10-1,Yes,Clarification,No,Import
 c,MISRA-C-2012,Corrigendum2,RULE-18-3,Yes,Clarification,No,Import
-c,MISRA-C-2012,Corrigendum2,RULE-1-4,Yes,Replace,No,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-1-4,Yes,Replace,Yes,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-9-1,Yes,Refine,No,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-9-2,Yes,Refine,No,Import
 c,MISRA-C-2012,Corrigendum2,DIR-4-10,Yes,Clarification,No,Import

c/misra/src/codingstandards/c/misra/EssentialTypes.qll

@@ -6,13 +6,17 @@ import codingstandards.c.misra
 import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 import MisraExpressions
 
+newtype TEssentialFloatCategory =
+  Real() or
+  Complex()
+
 newtype TEssentialTypeCategory =
   EssentiallyBooleanType() or
   EssentiallyCharacterType() or
   EssentiallyEnumType() or
   EssentiallySignedType() or
   EssentiallyUnsignedType() or
-  EssentiallyFloatingType()
+  EssentiallyFloatingType(TEssentialFloatCategory c)
 
 /** An essential type category, as specified by Appendix D.1. */
 class EssentialTypeCategory extends TEssentialTypeCategory {
@@ -27,7 +31,9 @@ class EssentialTypeCategory extends TEssentialTypeCategory {
     or
     this = EssentiallyUnsignedType() and result = "essentially Unsigned type"
     or
-    this = EssentiallyFloatingType() and result = "essentially Floating type"
+    this = EssentiallyFloatingType(Real()) and result = "essentially Floating type"
+    or
+    this = EssentiallyFloatingType(Complex()) and result = "essentially Complex Floating type"
   }
 }
 
@@ -143,8 +149,11 @@ EssentialTypeCategory getEssentialTypeCategory(Type type) {
     essentialType instanceof NamedEnumType and
     not essentialType instanceof MisraBoolType
     or
-    result = EssentiallyFloatingType() and
-    essentialType instanceof FloatingPointType
+    result = EssentiallyFloatingType(Real()) and
+    essentialType instanceof RealNumberType
+    or
+    result = EssentiallyFloatingType(Complex()) and
+    essentialType instanceof ComplexNumberType
   )
 }
 
@@ -166,6 +175,17 @@ Type getEssentialType(Expr e) {
 
 Type getEssentialTypeBeforeConversions(Expr e) { result = e.(EssentialExpr).getEssentialType() }
 
+/**
+ * For most essential types, `Type.getSize()` is correct, except for complex floating types.
+ *
+ * For complex floating types, the size is the size of the real part, so we divide by 2.
+ */
+int getEssentialSize(Type essentialType) {
+  if getEssentialTypeCategory(essentialType) = EssentiallyFloatingType(Complex())
+  then result = essentialType.getSize() / 2
+  else result = essentialType.getSize()
+}
+
 class EssentialExpr extends Expr {
   Type getEssentialType() { result = this.getType() }
 

c/misra/src/rules/DIR-4-6/PlainNumericalTypeUsedOverExplicitTypedef.ql

@@ -29,6 +29,8 @@ class BuiltInNumericType extends BuiltInType {
     this instanceof DoubleType
     or
     this instanceof LongDoubleType
+    or
+    this instanceof ComplexNumberType
   }
 }
 
@@ -38,22 +40,64 @@ predicate forbiddenBuiltinNumericUsedInDecl(Variable var, string message) {
   message = "The type " + var.getType() + " is not a fixed-width numeric type."
 }
 
+class SizedTypeString extends string {
+  string pattern;
+  int size;
+
+  bindingset[this]
+  pragma[inline]
+  SizedTypeString() {
+    pattern = "(u?int|c?float)(4|8|16|32|64|128)_t" and
+    this.regexpMatch(pattern) and
+    size = this.regexpCapture(pattern, 2).toInt()
+  }
+
+  bindingset[this]
+  pragma[inline]
+  int getSize() { result = size }
+
+  bindingset[this]
+  pragma[inline]
+  predicate isComplex() { this.charAt(0) = "c" }
+}
+
+predicate forbiddenComplexType(CTypedefType typedef, string message) {
+  typedef.getName().(SizedTypeString).isComplex() and
+  (
+    if typedef.getBaseType().stripTopLevelSpecifiers() instanceof ComplexNumberType
+    then
+      typedef.getSize() * 8 != typedef.getName().(SizedTypeString).getSize() * 2 and
+      message = "The typedef type " + typedef.getName() + " does not have its indicated real size."
+    else message = "The typedef type " + typedef.getName() + " is not a complex type."
+  )
+}
+
+predicate forbiddenRealType(CTypedefType typedef, string message) {
+  not typedef.getName().(SizedTypeString).isComplex() and
+  (
+    if typedef.getBaseType().stripTopLevelSpecifiers() instanceof ComplexNumberType
+    then message = "The typedef name " + typedef.getName() + " does not indicate a complex type."
+    else (
+      typedef.getSize() * 8 != typedef.getName().(SizedTypeString).getSize() and
+      message = "The typedef type " + typedef.getName() + " does not have its indicated size."
+    )
+  )
+}
+
 predicate forbiddenTypedef(CTypedefType typedef, string message) {
   /* If the typedef's name contains an explicit size */
   (
-    if typedef.getName().regexpMatch("u?(int|float)(4|8|16|32|64|128)_t")
+    if typedef.getName() instanceof SizedTypeString
     then (
-      /* Then the actual type size should match. */
-      not typedef.getSize() * 8 =
-        // times 8 because getSize() gets the size in bytes
-        typedef.getName().regexpCapture("u?(int|float)(4|8|16|32|64|128)_t", 2).toInt() and
-      message = "The typedef type " + typedef.getName() + " does not have its indicated size."
+      forbiddenRealType(typedef, message)
+      or
+      forbiddenComplexType(typedef, message)
     ) else (
       (
         // type def is to a built in numeric type
         typedef.getBaseType() instanceof BuiltInNumericType and
         // but does not include the size in the name
-        not typedef.getName().regexpMatch("u?(int|float)(4|8|16|32|64|128)_t")
+        not typedef.getName() instanceof SizedTypeString
         or
         // this is a typedef to a forbidden type def
         forbiddenTypedef(typedef.getBaseType(), _)

c/misra/src/rules/RULE-10-1/OperandsOfAnInappropriateEssentialType.ql

@@ -16,6 +16,15 @@ import cpp
 import codingstandards.c.misra
 import codingstandards.c.misra.EssentialTypes
 
+predicate hasComparableFloatValue(Expr e) {
+  exists(float value |
+    value = e.getValue().toFloat() or
+    value = -e.(UnaryMinusExpr).getOperand().getValue().toFloat()
+  |
+    value in [0.0, "Infinity".toFloat(), -"Infinity".toFloat()]
+  )
+}
+
 /**
  * Holds if the operator `operator` has an operand `child` that is of an inappropriate essential type
  * according to MISRA C 2012 Rule 10.1.
@@ -33,8 +42,11 @@ predicate isInappropriateEssentialType(
       etc = EssentiallyCharacterType() and
       rationaleId = 4
       or
-      etc = EssentiallyFloatingType() and
+      etc = EssentiallyFloatingType(Real()) and
       rationaleId = 1
+      or
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
     )
     or
     child = operator.(UnaryPlusExpr).getOperand() and
@@ -64,8 +76,6 @@ predicate isInappropriateEssentialType(
       rationaleId = 8
     )
     or
-    // The table only talks about + and -, but below it clarifies ++ and -- are also considered to
-    // be equivalent.
     child =
       [
         operator.(AddExpr).getAnOperand(), operator.(SubExpr).getAnOperand(),
@@ -80,6 +90,13 @@ predicate isInappropriateEssentialType(
       rationaleId = 5
     )
     or
+    child =
+      [operator.(IncrementOperation).getAnOperand(), operator.(DecrementOperation).getAnOperand()] and
+    (
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
+    )
+    or
     child =
       [
         operator.(DivExpr).getAnOperand(), operator.(MulExpr).getAnOperand(),
@@ -107,13 +124,26 @@ predicate isInappropriateEssentialType(
       etc = EssentiallyEnumType() and
       rationaleId = 5
       or
-      etc = EssentiallyFloatingType() and
+      etc = EssentiallyFloatingType(Real()) and
       rationaleId = 1
+      or
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
     )
     or
     child = operator.(RelationalOperation).getAnOperand() and
-    etc = EssentiallyBooleanType() and
-    rationaleId = 3
+    (
+      etc = EssentiallyBooleanType() and
+      rationaleId = 3
+      or
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
+    )
+    or
+    child = operator.(EqualityOperation).getAnOperand() and
+    rationaleId = 10 and
+    not hasComparableFloatValue(operator.(EqualityOperation).getAnOperand()) and
+    etc = EssentiallyFloatingType(_)
     or
     child = [operator.(NotExpr).getAnOperand(), operator.(BinaryLogicalOperation).getAnOperand()] and
     rationaleId = 2 and
@@ -126,7 +156,7 @@ predicate isInappropriateEssentialType(
       or
       etc = EssentiallyUnsignedType()
       or
-      etc = EssentiallyFloatingType()
+      etc = EssentiallyFloatingType(_)
     )
     or
     child =
@@ -147,8 +177,11 @@ predicate isInappropriateEssentialType(
       etc = EssentiallySignedType() and
       rationaleId = 6
       or
-      etc = EssentiallyFloatingType() and
+      etc = EssentiallyFloatingType(Real()) and
       rationaleId = 1
+      or
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
     )
     or
     child =
@@ -171,8 +204,11 @@ predicate isInappropriateEssentialType(
       etc = EssentiallySignedType() and
       rationaleId = 7
       or
-      etc = EssentiallyFloatingType() and
+      etc = EssentiallyFloatingType(Real()) and
       rationaleId = 1
+      or
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
     )
     or
     child =
@@ -197,8 +233,11 @@ predicate isInappropriateEssentialType(
       etc = EssentiallySignedType() and
       rationaleId = 6
       or
-      etc = EssentiallyFloatingType() and
+      etc = EssentiallyFloatingType(Real()) and
       rationaleId = 1
+      or
+      etc = EssentiallyFloatingType(Complex()) and
+      rationaleId = 9
     )
     or
     child = operator.(ConditionalExpr).getCondition() and
@@ -215,7 +254,7 @@ predicate isInappropriateEssentialType(
       etc = EssentiallyUnsignedType() and
       rationaleId = 2
       or
-      etc = EssentiallyFloatingType() and
+      etc = EssentiallyFloatingType(_) and
       rationaleId = 2
     )
   )
@@ -245,6 +284,13 @@ string getRationaleMessage(int rationaleId, EssentialTypeCategory etc) {
   rationaleId = 8 and
   result =
     "Operand of essentially Unsigned type will be converted to a signed type with the signedness dependent on the implemented size of int."
+  or
+  rationaleId = 9 and
+  result = "Use of essentially Complex type in this way is a constraint violation."
+  or
+  rationaleId = 10 and
+  result =
+    "Floating point numbers have inherent error such that comparisons should consider precision and not exact equality."
 }
 
 from Expr operator, Expr child, int rationaleId, EssentialTypeCategory etc

c/misra/src/rules/RULE-10-3/AssignmentOfIncompatibleEssentialType.ql

@@ -48,5 +48,11 @@ where
     lValueTypeCategory = EssentiallyUnsignedType() and
     const >= 0 and
     const <= 2.pow(lValueEssentialType.getSize() * 8)
+  ) and
+  // Exception 4: Real floating point values may be assignable to complex floating point values
+  not (
+    lValueTypeCategory = EssentiallyFloatingType(Complex()) and
+    rValueTypeCategory = EssentiallyFloatingType(Real()) and
+    lValueEssentialType.getSize() >= rValueEssentialType.getSize() * 2
   )
 select rValue, message

c/misra/src/rules/RULE-10-4/OperandsWithMismatchedEssentialTypeCategory.ql

@@ -30,6 +30,11 @@ where
   rightOpTypeCategory = getEssentialTypeCategory(rightOpEssentialType) and
   (
     not leftOpTypeCategory = rightOpTypeCategory and
+    not (
+      // Exception 3: Operands where both are real or complex floating types are allowed.
+      leftOpTypeCategory = EssentiallyFloatingType(_) and
+      rightOpTypeCategory = EssentiallyFloatingType(_)
+    ) and
     message =
       "The operands of this operator with usual arithmetic conversions have mismatched essential types (left operand: "
         + leftOpTypeCategory + ", right operand: " + rightOpTypeCategory + ")."

c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql

@@ -23,14 +23,14 @@ predicate isIncompatibleEssentialTypeCast(EssentialTypeCategory fromCat, Essenti
   toCat =
     [
       EssentiallyCharacterType(), EssentiallyEnumType(), EssentiallySignedType(),
-      EssentiallyUnsignedType(), EssentiallyFloatingType().(TEssentialTypeCategory)
+      EssentiallyUnsignedType(), EssentiallyFloatingType(_).(TEssentialTypeCategory)
     ]
   or
   fromCat = EssentiallyCharacterType() and
   toCat =
     [
       EssentiallyBooleanType(), EssentiallyEnumType(),
-      EssentiallyFloatingType().(TEssentialTypeCategory)
+      EssentiallyFloatingType(_).(TEssentialTypeCategory)
     ]
   or
   fromCat = EssentiallyEnumType() and
@@ -42,7 +42,7 @@ predicate isIncompatibleEssentialTypeCast(EssentialTypeCategory fromCat, Essenti
   fromCat = EssentiallyUnsignedType() and
   toCat = [EssentiallyBooleanType(), EssentiallyEnumType().(TEssentialTypeCategory)]
   or
-  fromCat = EssentiallyFloatingType() and
+  fromCat = EssentiallyFloatingType(_) and
   toCat =
     [
       EssentiallyBooleanType(), EssentiallyCharacterType(),

c/misra/src/rules/RULE-10-7/ImplicitConversionOfCompositeExpression.ql

@@ -23,6 +23,10 @@ bindingset[essentialTypeLeft, essentialTypeRight]
 pragma[inline_late]
 predicate isSameEssentialTypeCategory(Type essentialTypeLeft, Type essentialTypeRight) {
   getEssentialTypeCategory(essentialTypeLeft) = getEssentialTypeCategory(essentialTypeRight)
+  or
+  // Complex and real floating types are considered interchangeable
+  getEssentialTypeCategory(essentialTypeLeft) = EssentiallyFloatingType(_) and
+  getEssentialTypeCategory(essentialTypeRight) = EssentiallyFloatingType(_)
 }
 
 from
@@ -35,7 +39,7 @@ where
   not otherOp = compositeOp and
   compositeEssentialType = getEssentialType(compositeOp) and
   otherOpEssentialType = getEssentialType(otherOp) and
-  compositeEssentialType.getSize() < otherOpEssentialType.getSize() and
+  getEssentialSize(compositeEssentialType) < getEssentialSize(otherOpEssentialType) and
   // Operands of a different type category in an operation with the usual arithmetic conversions is
   // prohibited by Rule 10.4, so we only report cases here where the essential type categories are
   // the same