added support for SCA with Polyspace

cmake/sca/polyspace/README.md

@@ -0,0 +1,27 @@
+# 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,78 @@
+#!/usr/bin/python3
+"""
+Example script to illustrate the usage of the Polyspace Python tools
+Copyright (C) 2020-2024 The MathWorks, Inc.
+"""
+
+import os
+import sys
+import argparse
+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))
+
+    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("   {} issues in {}".format(cnt_and_fil[0], 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 Polyspace results to console')
+    parser.add_argument('file', type=str, help='output file from polyspace-results-export')
+    parser.add_argument('-d', '--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("SCA found {} issues in total".format(len(findings)))
+    return 0
+
+
+if __name__ == "__main__":
+    main(sys.argv[1:])

cmake/sca/polyspace/sca.cmake

@@ -0,0 +1,146 @@
+# 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