sca: added support for Polyspace tool

Add the cmake files for running static code analysis with the Polyspace
tools in the west build. The analysis leverages the compilation database.
Options for the analysis are documented in doc/develop/sca/polyspace.rst.

Analysis results are printed as command line output and provided as CSV.

Manually tested on v4.0.0 with various sample applications.

Signed-off-by: Martin Becker <mbecker@mathworks.com>

cmake/sca/polyspace/polyspace-print-console.py

@@ -0,0 +1,85 @@
+#!/usr/bin/python3
+"""
+Print Polyspace results on terminal, for easy review.
+Copyright (C) 2020-2024 The MathWorks, Inc.
+"""
+
+# SPDX-License-Identifier: Apache-2.0
+
+import argparse
+import os
+import sys
+from collections import Counter
+
+
+def _parse_findings(filename: str, ignore_metrics=True):
+    """Parse CSV file"""
+    csv_sep = '\t'  # Polyspace default separator
+
+    def consume_header(oneline):
+        parts = oneline.split(csv_sep)
+        header.extend([p.strip() for p in parts])
+
+    def consume_data(oneline):
+        columns = oneline.split(csv_sep)
+        return dict(zip(header, columns, strict=True))
+
+    findings = []
+    header = []
+    with open(filename, encoding="latin-1") as fp:
+        for lno, line in enumerate(fp):
+            if lno == 0:
+                consume_header(line.rstrip())
+            else:
+                onefind = consume_data(line.rstrip())
+                if onefind and (not ignore_metrics or onefind.get('Family', '') != 'Code Metric'):
+                    findings.append(onefind)
+    # --
+    return findings
+
+
+def print_sorted(mydict, maxlines=0):
+    """Print a dict sorted by value, largest first"""
+
+    for lno, cnt_and_fil in enumerate(
+        sorted(((cnt, fil) for fil, cnt in mydict.items()), reverse=True), start=1
+    ):
+        print(f"   {cnt_and_fil[0]} issues in {cnt_and_fil[1]}")
+        if lno >= maxlines and maxlines != 0:
+            break
+
+
+def main(argv):
+    # 1. command line arguments as required by your script
+    parser = argparse.ArgumentParser(description='Print results to console', allow_abbrev=False)
+    parser.add_argument('file', type=str, help='output file from polyspace-results-export')
+    parser.add_argument('--details', action='store_true', help='print details')
+    args = parser.parse_args()
+
+    # 2. parsing the Polyspace files -> report
+    findings = _parse_findings(args.file)
+    print("-= Polyspace Static Code Analysis results =-")
+
+    # 3. print details
+    if args.details:
+        for f in findings:
+            print(
+                f"{f.get('File', 'unknown file')}:"
+                + f"{f.get('Line', '?')}:"
+                + f"{f.get('Col', '?')}: "
+                + f"{f.get('Family', '')} {f.get('Check', 'Defect')}"
+            )
+
+    # 3. summary by category and file
+    print("By type:")
+    family = Counter([f.get('Family', 'Defect') for f in findings])
+    print_sorted(family)
+    print("Top 10 files:")
+    files = Counter([os.path.basename(f.get('File', 'Unknown')) for f in findings])
+    print_sorted(files, 10)
+    print(f"SCA found {len(findings)} issues in total")
+    return 0
+
+
+if __name__ == "__main__":
+    main(sys.argv[1:])

cmake/sca/polyspace/sca.cmake

@@ -0,0 +1,142 @@
+# SPDX-License-Identifier: Apache-2.0
+#
+# Copyright (c) 2024, The MathWorks, Inc.
+
+include(boards)
+include(git)
+include(extensions)
+include(west)
+
+# find Polyspace, stop if missing
+find_program(POLYSPACE_CONFIGURE_EXE NAMES polyspace-configure)
+if(NOT POLYSPACE_CONFIGURE_EXE)
+  message(FATAL_ERROR "Polyspace not found. For install instructions, see https://mathworks.com/help/bugfinder/install")
+else()
+  cmake_path(GET POLYSPACE_CONFIGURE_EXE PARENT_PATH POLYSPACE_BIN)
+  message(STATUS "Found SCA: Polyspace (${POLYSPACE_BIN})")
+endif()
+find_program(POLYSPACE_RESULTS_EXE NAMES polyspace-results-export REQUIRED)
+
+
+# Get Polyspace specific variables
+zephyr_get(POLYSPACE_ONLY_APP)
+zephyr_get(POLYSPACE_CONFIGURE_OPTIONS)
+zephyr_get(POLYSPACE_MODE)
+zephyr_get(POLYSPACE_OPTIONS)
+zephyr_get(POLYSPACE_OPTIONS_FILE)
+zephyr_get(POLYSPACE_PROG_NAME)
+zephyr_get(POLYSPACE_PROG_VERSION)
+message(TRACE "POLYSPACE_OPTIONS is ${POLYSPACE_OPTIONS}")
+
+
+# Get path and name of user application
+zephyr_get(APPLICATION_SOURCE_DIR)
+cmake_path(GET APPLICATION_SOURCE_DIR FILENAME APPLICATION_NAME)
+message(TRACE "APPLICATION_SOURCE_DIR is ${APPLICATION_SOURCE_DIR}")
+message(TRACE "APPLICATION_NAME is ${APPLICATION_NAME}")
+
+
+# process options
+if(POLYSPACE_ONLY_APP)
+  set(POLYSPACE_CONFIGURE_OPTIONS ${POLYSPACE_CONFIGURE_OPTIONS} -include-sources ${APPLICATION_SOURCE_DIR}/**)
+  message(WARNING "SCA only analyzes application code")
+endif()
+if(POLYSPACE_MODE STREQUAL "prove")
+  message(NOTICE "POLYSPACE in proof mode")
+  find_program(POLYSPACE_EXE NAMES polyspace-code-prover-server polyspace-code-prover)
+else()
+  message(NOTICE "POLYSPACE in bugfinding mode")
+  find_program(POLYSPACE_EXE NAMES polyspace-bug-finder-server polyspace-bug-finder)
+endif()
+if(NOT POLYSPACE_PROG_NAME)
+  set(POLYSPACE_PROG_NAME "zephyr-${BOARD}-${APPLICATION_NAME}")
+endif()
+message(TRACE "POLYSPACE_PROG_NAME is ${POLYSPACE_PROG_NAME}")
+if(POLYSPACE_OPTIONS_FILE)
+  message(TRACE "POLYSPACE_OPTIONS_FILE is ${POLYSPACE_OPTIONS_FILE}")
+  set(POLYSPACE_OPTIONS_FILE -options-file ${POLYSPACE_OPTIONS_FILE})
+endif()
+if(POLYSPACE_PROG_VERSION)
+  set(POLYSPACE_PROG_VERSION -verif-version '${POLYSPACE_PROG_VERSION}')
+else()
+  git_describe(${APPLICATION_SOURCE_DIR} app_version)
+  if(app_version)
+    set(POLYSPACE_PROG_VERSION -verif-version '${app_version}')
+  endif()
+endif()
+message(TRACE "POLYSPACE_PROG_VERSION is ${POLYSPACE_PROG_VERSION}")
+
+# tell Polyspace about Zephyr specials
+set(POLYSPACE_OPTIONS_ZEPHYR -options-file ${CMAKE_CURRENT_LIST_DIR}/zephyr.psopts)
+
+# Polyspace requires the compile_commands.json as input
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
+# Create results directory
+set(POLYSPACE_RESULTS_DIR ${CMAKE_BINARY_DIR}/sca/polyspace)
+set(POLYSPACE_RESULTS_FILE ${POLYSPACE_RESULTS_DIR}/results.csv)
+file(MAKE_DIRECTORY ${POLYSPACE_RESULTS_DIR})
+message(TRACE "POLYSPACE_RESULTS_DIR is ${POLYSPACE_RESULTS_DIR}")
+set(POLYSPACE_OPTIONS_FILE_BASE ${POLYSPACE_RESULTS_DIR}/polyspace.psopts)
+
+
+#####################
+# mandatory targets #
+#####################
+
+add_custom_target(polyspace_configure ALL
+  COMMAND ${POLYSPACE_CONFIGURE_EXE}
+    -allow-overwrite
+    -silent
+    -prog ${POLYSPACE_PROG_NAME}
+    -compilation-database ${CMAKE_BINARY_DIR}/compile_commands.json
+    -output-options-file ${POLYSPACE_OPTIONS_FILE_BASE}
+    ${POLYSPACE_CONFIGURE_OPTIONS}
+  VERBATIM
+  DEPENDS ${CMAKE_BINARY_DIR}/compile_commands.json
+  BYPRODUCTS ${POLYSPACE_OPTIONS_FILE_BASE}
+  USES_TERMINAL
+  COMMAND_EXPAND_LISTS
+)
+
+add_custom_target(polyspace-analyze ALL
+  COMMAND ${POLYSPACE_EXE}
+    -results-dir ${POLYSPACE_RESULTS_DIR}
+    -options-file ${POLYSPACE_OPTIONS_FILE_BASE}
+    ${POLYSPACE_PROG_VERSION}
+    ${POLYSPACE_OPTIONS_ZEPHYR}
+    ${POLYSPACE_OPTIONS_FILE}
+    ${POLYSPACE_OPTIONS}
+      || ${CMAKE_COMMAND} -E true # allow to continue processing results
+  DEPENDS ${POLYSPACE_OPTIONS_FILE_BASE}
+  USES_TERMINAL
+  COMMAND_EXPAND_LISTS
+)
+
+add_custom_target(polyspace-results ALL
+  COMMAND ${POLYSPACE_RESULTS_EXE}
+    -results-dir ${POLYSPACE_RESULTS_DIR}
+    -output-name ${POLYSPACE_RESULTS_FILE}
+    -format csv
+      || ${CMAKE_COMMAND} -E true # allow to continue processing results
+  VERBATIM
+  USES_TERMINAL
+  COMMAND_EXPAND_LISTS
+)
+
+add_dependencies(polyspace-results polyspace-analyze)
+
+
+#####################
+# summarize results #
+#####################
+
+add_custom_command(TARGET polyspace-results POST_BUILD
+  COMMAND ${CMAKE_CURRENT_LIST_DIR}/polyspace-print-console.py
+  ${POLYSPACE_RESULTS_FILE}
+  COMMAND
+    ${CMAKE_COMMAND} -E cmake_echo_color --cyan --bold
+    "SCA results are here: ${POLYSPACE_RESULTS_DIR}"
+  VERBATIM
+  USES_TERMINAL
+)

cmake/sca/polyspace/zephyr.psopts

@@ -0,0 +1,3 @@
+# tweaks specifically for Zephyr
+-D__thread=
+-enable-concurrency-detection

doc/develop/sca/index.rst

@@ -66,3 +66,4 @@ The following is a list of SCA tools natively supported by Zephyr build system.
    gcc
    cpptest
    eclair
+   polyspace

doc/develop/sca/polyspace.rst

@@ -0,0 +1,93 @@
+.. _polyspace:
+
+Polyspace support
+#################
+
+`Polyspace® <https://mathworks.com/products/polyspace.html>`__ is
+a commercial static code analysis tool from MathWorks, which is certified
+for use in highest safety contexts. It can check compliance to coding
+guidelines like MISRA C and CERT C, find CWEs, detect bugs and calculate
+code complexity metrics. Optionally, it can run a formal proof to verify
+the absence of run-time errors like array out of bounds access, overflows,
+race conditions and more, and thus help achieving memory safety.
+
+Installing
+**********
+
+The Polyspace tools must be installed and made available in the
+operating system's or container's PATH variable. Specifically, the path
+``<polyspace_root>/polyspace/bin`` must be on the list.
+
+For installation instructions, see
+`here <https://mathworks.com/help/bugfinder/install-polyspace.html>`__.
+To use formal verification (proving the *absence* of defects), you
+additionally need to install
+`this <https://mathworks.com/help/codeprover/install-polyspace.html>`__.
+
+A license file must be available
+in the installation folder. To request a trial license, visit `this
+page <https://www.mathworks.com/campaigns/products/trials.html>`__.
+
+Running
+*******
+
+The code analysis can be triggered through the ``west`` command by
+appending the option ``-DZEPHYR_SCA_VARIANT=polyspace`` to the build,
+for example:
+
+.. code-block:: shell
+
+   west build -b qemu_x86 samples/hello_world -- -DZEPHYR_SCA_VARIANT=polyspace
+
+Reviewing results
+*****************
+
+The identified issues are summarized at the end of the build and printed
+in the console window, along with the path of the folder containing
+detailed results.
+
+For an efficient review, the folder should be opened in the
+`Polyspace user interface <https://mathworks.com/help/bugfinder/review-results-1.html>`__
+or `uploaded to the web interface <https://mathworks.com/help/bugfinder/gs/run-bug-finder-on-server.html>`__
+and reviewed there.
+
+For programmatic access of the results, e.g., in the CI pipeline, the
+individual issues are also described in a CSV file in the results folder.
+
+Configuration
+*************
+
+By default, Polyspace scans for typical programming defects on all C and C++ sources.
+The following options are available to customize the default behavior:
+
+.. list-table::
+   :widths: 20 40 30
+   :header-rows: 1
+
+   * - Option
+     - Effect
+     - Example
+   * - ``POLYSPACE_ONLY_APP``
+     - If set, only user code is analyzed and Zephyr sources are ignored.
+     - ``-DPOLYSPACE_ONLY_APP=1``
+   * - ``POLYSPACE_OPTIONS``
+     - Provide additional command line flags, e.g., for selection of coding
+       rules. Separate the options and their values by semicolon. For a list
+       of options, see `here <https://mathworks.com/help/bugfinder/referencelist.html?type=analysisopt&s_tid=CRUX_topnav>`__.
+     - ``-DPOLYSPACE_OPTIONS="-misra3;mandatory-required;-checkers;all"``
+   * - ``POLYSPACE_OPTIONS_FILE``
+     - Command line flags can also be provided in a text file, line by
+       line. Provide the absolute path to the file.
+     - ``-DPOLYSPACE_OPTIONS_FILE=/workdir/zephyr/myoptions.txt``
+   * - ``POLYSPACE_MODE``
+     - Switch between bugfinding and proving mode. Default is bugfinding.
+       See `here <https://mathworks.com/help/bugfinder/gs/use-bug-finder-and-code-prover.html>`__ for more details.
+     - ``-DPOLYSPACE_MODE=prove``
+   * - ``POLYSPACE_PROG_NAME``
+     - Override the name of the analyzed application. Default is board
+       and application name.
+     - ``-DPOLYSPACE_PROG_NAME=myapp``
+   * - ``POLYSPACE_PROG_VERSION``
+     - Override the version of the analyzed application. Default is taken
+       from git-describe.
+     - ``-DPOLYSPACE_PROG_VERSION=v1.0b-28f023``