Recognize FW_ASSERT in JPL CodeQL Rule 16 assertion queries

Co-Authored-By: michael.d.starch <michael.d.starch@jpl.nasa.gov>

Author: devin-ai-integration[bot]

.github/actions/codeql/jpl-standard-pack-1.yml

@@ -6,7 +6,18 @@ packs:
   # Source of the query pack is https://github.com/github/codeql/tree/main/cpp/ql/src/JPL_C
   - codeql/cpp-queries:JPL_C
 
+queries:
+  # FW_ASSERT-aware replacements for the Rule 16 assertion queries
+  - uses: ./.github/codeql/fprime-queries
+
 query-filters:
   - exclude:
       problem.severity:
         - recommendation
+  # Excluded in favor of the FW_ASSERT-aware replacements above, which
+  # recognize F Prime's FW_ASSERT macro as an assertion
+  - exclude:
+      id:
+        - cpp/jpl-c/use-of-assertions-constant
+        - cpp/jpl-c/use-of-assertions-non-boolean
+        - cpp/jpl-c/use-of-assertions-side-effect

.github/actions/codeql/jpl-standard-pack-2.yml

@@ -6,6 +6,10 @@ packs:
   # Source of the query pack is https://github.com/github/codeql/tree/main/cpp/ql/src/JPL_C
   - codeql/cpp-queries:JPL_C
 
+queries:
+  # FW_ASSERT-aware replacements for the Rule 16 assertion queries
+  - uses: ./.github/codeql/fprime-queries
+
 query-filters:
   - exclude:
       problem.severity:
@@ -18,3 +22,8 @@ query-filters:
   - exclude:
       id:
         - cpp/jpl-c/basic-int-types
+  # Excluded in favor of the FW_ASSERT-aware replacement above, which
+  # recognizes F Prime's FW_ASSERT macro as an assertion
+  - exclude:
+      id:
+        - cpp/jpl-c/use-of-assertions-density

.github/codeql/fprime-queries/FprimeAssertions.qll

@@ -0,0 +1,31 @@
+/**
+ * Extends the standard CodeQL assertion library with support for the F Prime
+ * `FW_ASSERT` macro family, so that the JPL Coding Standard Rule 16 queries
+ * recognize F Prime assertions.
+ */
+
+import cpp
+import semmle.code.cpp.commons.Assertions
+
+/**
+ * An F Prime assertion: an invocation of an `FW_ASSERT` macro, which expands
+ * to a conditional expression of the form
+ * `(condition ? (void)0 : Fw::SwAssert(...))`.
+ */
+class FwAssert extends MacroInvocation, Assertion {
+  FwAssert() { this.getMacro().getName() = "FW_ASSERT" }
+
+  override Expr getAsserted() {
+    exists(ConditionalExpr ce |
+      ce = this.getAGeneratedElement() and
+      // Restrict to the outermost conditional generated by this macro
+      // invocation (nested FW_ASSERTs are separate macro invocations).
+      not exists(ConditionalExpr outer |
+        outer = this.getAGeneratedElement() and
+        ce.getParent+() = outer
+      )
+    |
+      result = ce.getCondition()
+    )
+  }
+}

.github/codeql/fprime-queries/FprimeUseOfAssertionsConstant.ql

@@ -0,0 +1,20 @@
+/**
+ * @name Constant assertion
+ * @description Assertions should check dynamic properties of pre-/post-conditions and invariants. Assertions that either always succeed or always fail are an error.
+ * @kind problem
+ * @id cpp/fprime/jpl-c/use-of-assertions-constant
+ * @problem.severity warning
+ * @tags maintainability
+ *       reliability
+ *       external/jpl
+ */
+
+import FprimeAssertions
+
+from Assertion a, string value, string msg
+where
+  value = a.getAsserted().getValue() and
+  if value.toInt() = 0
+  then msg = "This assertion is always false."
+  else msg = "This assertion is always true."
+select a.getAsserted(), msg

.github/codeql/fprime-queries/FprimeUseOfAssertionsDensity.ql

@@ -0,0 +1,18 @@
+/**
+ * @name Long function without assertion
+ * @description All functions of more than 10 lines should have at least one assertion.
+ * @kind problem
+ * @id cpp/fprime/jpl-c/use-of-assertions-density
+ * @problem.severity recommendation
+ * @tags maintainability
+ *       reliability
+ *       external/jpl
+ */
+
+import FprimeAssertions
+
+from Function f
+where
+  f.getMetrics().getNumberOfLinesOfCode() > 10 and
+  not exists(Assertion a | a.getAsserted().getEnclosingFunction() = f)
+select f, "All functions of more than 10 lines should have at least one assertion."

.github/codeql/fprime-queries/FprimeUseOfAssertionsNonBoolean.ql

@@ -0,0 +1,15 @@
+/**
+ * @name Non-boolean assertion
+ * @description Assertions should be defined as Boolean tests, meaning "assert(p != NULL)" rather than "assert(p)".
+ * @kind problem
+ * @id cpp/fprime/jpl-c/use-of-assertions-non-boolean
+ * @problem.severity warning
+ * @tags correctness
+ *       external/jpl
+ */
+
+import FprimeAssertions
+
+from Assertion a
+where a.getAsserted().getType() instanceof PointerType
+select a.getAsserted(), "Assertions should be defined as Boolean tests."

.github/codeql/fprime-queries/FprimeUseOfAssertionsSideEffect.ql

@@ -0,0 +1,15 @@
+/**
+ * @name Assertion with side effects
+ * @description Assertions should not have side-effects -- they may be disabled completely, changing program behavior.
+ * @kind problem
+ * @id cpp/fprime/jpl-c/use-of-assertions-side-effect
+ * @problem.severity warning
+ * @tags correctness
+ *       external/jpl
+ */
+
+import FprimeAssertions
+
+from Assertion a
+where not a.getAsserted().isPure()
+select a.getAsserted(), "Assertions should not have side effects."

.github/codeql/fprime-queries/codeql-pack.lock.yml

@@ -0,0 +1,28 @@
+---
+lockVersion: 1.0.0
+dependencies:
+  codeql/controlflow:
+    version: 2.0.35
+  codeql/cpp-all:
+    version: 10.2.0
+  codeql/dataflow:
+    version: 2.1.7
+  codeql/mad:
+    version: 1.0.51
+  codeql/quantum:
+    version: 0.0.29
+  codeql/rangeanalysis:
+    version: 1.0.51
+  codeql/ssa:
+    version: 2.0.27
+  codeql/tutorial:
+    version: 1.0.51
+  codeql/typeflow:
+    version: 1.0.51
+  codeql/typetracking:
+    version: 2.0.35
+  codeql/util:
+    version: 2.0.38
+  codeql/xml:
+    version: 1.0.51
+compiled: false

.github/codeql/fprime-queries/qlpack.yml

@@ -0,0 +1,4 @@
+name: fprime/jpl-c-queries
+version: 1.0.0
+dependencies:
+  codeql/cpp-all: "*"