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 the README.md.

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 <[email protected]>

cmake/sca/polyspace/README.md

@@ -0,0 +1,26 @@
+# Static Code Analysis with Polyspace
+This folder contains the CMake files to run a Static Code Analysis with the tool [Polyspace](https://mathworks.com/products/polyspace.html)® from MathWorks. It can check compliance to coding guidelines like MISRA C and CERT C, find CWEs, detect bugs, calculate code complexity metrics, and optionally run a formal proof to verify the absence of run-time errors like array out of bounds access, overflows, race conditions and more.
+
+## Prerequisites
+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. To request a trial license, visit [this page](https://www.mathworks.com/campaigns/products/trials.html).
+
+## Usage
+The code analysis can be triggered through the `west` command, for example:
+
+    west build -b qemu_x86 samples/hello_world -- -DZEPHYR_SCA_VARIANT=polyspace
+
+The following options are supported, to tweak analysis behavior:
+
+| 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. Use 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` |

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

@@ -0,0 +1,86 @@
+#!/usr/bin/python3
+"""
+Example script to illustrate the usage of the Polyspace Python tools
+Copyright (C) 2020-2024 The MathWorks, Inc.
+"""
+
+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:
+            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(
+                "{}:{}:{}: {} {}".format(
+                    f.get('File', 'unknown file'),
+                    f.get('Line', '?'),
+                    f.get('Col', '?'),
+                    f.get('Family', ''),
+                    f.get('Check', 'Unknown'),
+                )
+            )
+
+    # 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,145 @@
+# 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 speciic 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
+    #VERBATIM
+  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
+)
+
+# EOF

cmake/sca/polyspace/zephyr.psopts

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