Implement DIR-4-15, detection of NaNs and Infinities

c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql

@@ -0,0 +1,142 @@
+/**
+ * @id c/misra/possible-misuse-of-undetected-infinity
+ * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of infinities
+ * @description Evaluation of floating-point expressions shall not lead to the undetected generation
+ *              of infinities.
+ * @kind path-problem
+ * @precision medium
+ * @problem.severity warning
+ * @tags external/misra/id/dir-4-15
+ *       correctness
+ *       external/misra/c/2012/amendment3
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codeql.util.Boolean
+import codingstandards.c.misra
+import codingstandards.cpp.RestrictedRangeAnalysis
+import codingstandards.cpp.FloatingPoint
+import codingstandards.cpp.AlertReporting
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.dataflow.new.DataFlow
+import semmle.code.cpp.dataflow.new.TaintTracking
+import semmle.code.cpp.controlflow.Dominance
+
+module InvalidInfinityUsage implements DataFlow::ConfigSig {
+  /**
+   * An operation which does not have Infinity as an input, but may produce Infinity, according
+   * to the `RestrictedRangeAnalysis` module.
+   */
+  predicate isSource(DataFlow::Node node) {
+    potentialSource(node) and
+    not exists(DataFlow::Node prior |
+      isAdditionalFlowStep(prior, node) and
+      potentialSource(prior)
+    )
+  }
+
+  /**
+   * An operation which may produce Infinity acconding to the `RestrictedRangeAnalysis` module.
+   */
+  additional predicate potentialSource(DataFlow::Node node) {
+    node.asExpr() instanceof Operation and
+    exprMayEqualInfinity(node.asExpr(), _)
+  }
+
+  predicate isBarrierOut(DataFlow::Node node) {
+    guardedNotFPClass(node.asExpr(), TInfinite())
+    or
+    exists(Expr e |
+      e.getType() instanceof IntegralType and
+      e = node.asConvertedExpr()
+    )
+  }
+
+  /**
+   * An additional flow step to handle operations which propagate Infinity.
+   *
+   * This double checks that an Infinity may propagate by checking the `RestrictedRangeAnalysis`
+   * value estimate. This is conservative, since `RestrictedRangeAnalysis` is performed locally
+   * in scope with unanalyzable values in a finite range. However, this conservative approach
+   * leverages analysis of guards and other local conditions to avoid false positives.
+   */
+  predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
+    exists(Operation o |
+      o.getAnOperand() = source.asExpr() and
+      o = sink.asExpr() and
+      potentialSource(sink)
+    )
+  }
+
+  predicate isSink(DataFlow::Node node) {
+    node instanceof InvalidInfinityUsage and
+    (
+      // Require that range analysis finds this value potentially infinite, to avoid false positives
+      // in the presence of guards. This may induce false negatives.
+      exprMayEqualInfinity(node.asExpr(), _)
+      or
+      // Unanalyzable expressions are not checked against range analysis, which assumes a finite
+      // range.
+      not RestrictedRangeAnalysis::canBoundExpr(node.asExpr())
+      or
+      node.asExpr().(VariableAccess).getTarget() instanceof Parameter
+    )
+  }
+}
+
+class InvalidInfinityUsage extends DataFlow::Node {
+  string description;
+
+  InvalidInfinityUsage() {
+    // Case 2: NaNs and infinities shall not be cast to integers
+    exists(Conversion c |
+      asExpr() = c.getUnconverted() and
+      c.getExpr().getType() instanceof FloatingPointType and
+      c.getType() instanceof IntegralType and
+      description = "cast to integer."
+    )
+    or
+    // Case 3: Infinities shall not underflow or otherwise produce finite values
+    exists(BinaryOperation op |
+      asExpr() = op.getRightOperand() and
+      op.getOperator() = "/" and
+      description = "divisor, which would silently underflow and produce zero."
+    )
+  }
+
+  string getDescription() { result = description }
+}
+
+module InvalidInfinityFlow = DataFlow::Global<InvalidInfinityUsage>;
+
+import InvalidInfinityFlow::PathGraph
+
+from
+  Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink,
+  InvalidInfinityUsage usage, Expr sourceExpr, string sourceString, Function function,
+  string computedInFunction
+where
+  elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
+  not InvalidInfinityFlow::PathGraph::edges(_, source, _, _) and
+  not InvalidInfinityFlow::PathGraph::edges(sink, _, _, _) and
+  not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and
+  not sourceExpr.isFromTemplateInstantiation(_) and
+  not usage.asExpr().isFromTemplateInstantiation(_) and
+  usage = sink.getNode() and
+  sourceExpr = source.getNode().asExpr() and
+  function = sourceExpr.getEnclosingFunction() and
+  InvalidInfinityFlow::flow(source.getNode(), usage) and
+  (
+    if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
+    then computedInFunction = "computed in function $@ "
+    else computedInFunction = ""
+  ) and
+  (
+    if sourceExpr instanceof DivExpr
+    then sourceString = "from division by zero"
+    else sourceString = sourceExpr.toString()
+  )
+select elem, source, sink,
+  "Possibly infinite float value $@ " + computedInFunction + "flows to " + usage.getDescription(),
+  sourceExpr, sourceString, function, function.getName()

c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql

@@ -0,0 +1,202 @@
+/**
+ * @id c/misra/possible-misuse-of-undetected-nan
+ * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs
+ * @description Evaluation of floating-point expressions shall not lead to the undetected generation
+ *              of NaNs.
+ * @kind path-problem
+ * @precision low
+ * @problem.severity warning
+ * @tags external/misra/id/dir-4-15
+ *       correctness
+ *       external/misra/c/2012/amendment3
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codeql.util.Boolean
+import codingstandards.c.misra
+import codingstandards.cpp.RestrictedRangeAnalysis
+import codingstandards.cpp.FloatingPoint
+import codingstandards.cpp.AlertReporting
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.dataflow.new.DataFlow
+import semmle.code.cpp.dataflow.new.TaintTracking
+import semmle.code.cpp.controlflow.Dominance
+
+abstract class PotentiallyNaNExpr extends Expr {
+  abstract string getReason();
+}
+
+class DomainErrorFunctionCall extends FunctionCall, PotentiallyNaNExpr {
+  string reason;
+
+  DomainErrorFunctionCall() { RestrictedDomainError::hasDomainError(this, reason) }
+
+  override string getReason() { result = reason }
+}
+
+// IEEE 754-1985 Section 7.1 invalid operations
+class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr {
+  string reason;
+
+  InvalidOperationExpr() {
+    // Usual arithmetic conversions in both languages mean that if either operand is a floating
+    // type, the other one is converted to a floating type as well.
+    getAnOperand().getFullyConverted().getType() instanceof FloatingPointType and
+    (
+      // 7.1.1 propagates signaling NaNs, we rely on flow analysis and/or assume quiet NaNs, so we
+      // intentionally do not cover this case.
+      // 7.1.2: magnitude subtraction of infinities, such as +Inf + -Inf
+      getOperator() = "+" and
+      exists(Boolean sign |
+        exprMayEqualInfinity(getLeftOperand(), sign) and
+        exprMayEqualInfinity(getRightOperand(), sign.booleanNot())
+      ) and
+      reason = "from addition of infinity and negative infinity"
+      or
+      // 7.1.2 continued
+      getOperator() = "-" and
+      exists(Boolean sign |
+        exprMayEqualInfinity(getLeftOperand(), sign) and
+        exprMayEqualInfinity(getRightOperand(), sign)
+      ) and
+      reason = "from subtraction of an infinity from itself"
+      or
+      // 7.1.3: multiplication of zero by infinity
+      getOperator() = "*" and
+      exists(Expr zeroOp, Expr infinityOp |
+        zeroOp = getAnOperand() and
+        infinityOp = getAnOperand() and
+        not zeroOp = infinityOp and
+        exprMayEqualZero(zeroOp) and
+        exprMayEqualInfinity(infinityOp, _)
+      ) and
+      reason = "from multiplication of zero by infinity"
+      or
+      // 7.1.4: Division of zero by zero, or infinity by infinity
+      getOperator() = "/" and
+      exprMayEqualZero(getLeftOperand()) and
+      exprMayEqualZero(getRightOperand()) and
+      reason = "from division of zero by zero"
+      or
+      // 7.1.4 continued
+      getOperator() = "/" and
+      exprMayEqualInfinity(getLeftOperand(), _) and
+      exprMayEqualInfinity(getRightOperand(), _) and
+      reason = "from division of infinity by infinity"
+      or
+      // 7.1.5: x % y where y is zero or x is infinite
+      getOperator() = "%" and
+      exprMayEqualInfinity(getLeftOperand(), _) and
+      reason = "from modulus of infinity"
+      or
+      // 7.1.5 continued
+      getOperator() = "%" and
+      exprMayEqualZero(getRightOperand()) and
+      reason = "from modulus by zero"
+      // 7.1.6 handles the sqrt function, not covered here.
+      // 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow
+      // analysis.
+      // 7.1.8 declares exceptions for unordered comparisons, which we catch as sinks in our flow
+      // analysis.
+    )
+  }
+
+  override string getReason() { result = reason }
+}
+
+module InvalidNaNUsage implements DataFlow::ConfigSig {
+  /**
+   * An expression which has non-NaN inputs and may produce a NaN output.
+   */
+  predicate isSource(DataFlow::Node node) {
+    potentialSource(node) and
+    not exists(DataFlow::Node prior |
+      isAdditionalFlowStep(prior, node) and
+      potentialSource(prior)
+    )
+  }
+
+  /**
+   * An expression which may produce a NaN output.
+   */
+  additional predicate potentialSource(DataFlow::Node node) {
+    node.asExpr() instanceof PotentiallyNaNExpr
+  }
+
+  predicate isBarrierOut(DataFlow::Node node) {
+    guardedNotFPClass(node.asExpr(), TNaN())
+    or
+    exists(Expr e |
+      e.getType() instanceof IntegralType and
+      e = node.asConvertedExpr()
+    )
+  }
+
+  /**
+   * Add an additional flow step to handle NaN propagation through floating point operations.
+   */
+  predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
+    exists(Operation o |
+      o.getAnOperand() = source.asExpr() and
+      o = sink.asExpr() and
+      o.getType() instanceof FloatingPointType
+    )
+  }
+
+  predicate isSink(DataFlow::Node node) {
+    not guardedNotFPClass(node.asExpr(), TNaN()) and
+    node instanceof InvalidNaNUsage
+  }
+}
+
+class InvalidNaNUsage extends DataFlow::Node {
+  string description;
+
+  InvalidNaNUsage() {
+    // Case 1: NaNs shall not be compared, except to themselves
+    exists(ComparisonOperation cmp |
+      this.asExpr() = cmp.getAnOperand() and
+      not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) and
+      description = "comparison, which would always evaluate to false."
+    )
+    or
+    // Case 2: NaNs and infinities shall not be cast to integers
+    exists(Conversion c |
+      this.asExpr() = c.getUnconverted() and
+      c.getExpr().getType() instanceof FloatingPointType and
+      c.getType() instanceof IntegralType and
+      description = "a cast to integer."
+    )
+  }
+
+  string getDescription() { result = description }
+}
+
+module InvalidNaNFlow = DataFlow::Global<InvalidNaNUsage>;
+
+import InvalidNaNFlow::PathGraph
+
+from
+  Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink,
+  InvalidNaNUsage usage, Expr sourceExpr, string sourceString, Function function,
+  string computedInFunction
+where
+  not InvalidNaNFlow::PathGraph::edges(_, source, _, _) and
+  not InvalidNaNFlow::PathGraph::edges(sink, _, _, _) and
+  not sourceExpr.isFromTemplateInstantiation(_) and
+  not usage.asExpr().isFromTemplateInstantiation(_) and
+  elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
+  usage = sink.getNode() and
+  sourceExpr = source.getNode().asExpr() and
+  sourceString = source.getNode().asExpr().(PotentiallyNaNExpr).getReason() and
+  function = sourceExpr.getEnclosingFunction() and
+  InvalidNaNFlow::flow(source.getNode(), usage) and
+  (
+    if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
+    then computedInFunction = "computed in function $@ "
+    else computedInFunction = ""
+  )
+select elem, source, sink,
+  "Possible NaN value $@ " + computedInFunction + "flows to " + usage.getDescription(), sourceExpr,
+  sourceString, function, function.getName()