diff --git a/cmake/sca/polyspace/polyspace-print-console.py b/cmake/sca/polyspace/polyspace-print-console.py new file mode 100755 index 00000000000..352fed1bdb3 --- /dev/null +++ b/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:]) diff --git a/cmake/sca/polyspace/sca.cmake b/cmake/sca/polyspace/sca.cmake new file mode 100644 index 00000000000..e9a73d71fda --- /dev/null +++ b/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 +) diff --git a/cmake/sca/polyspace/zephyr.psopts b/cmake/sca/polyspace/zephyr.psopts new file mode 100644 index 00000000000..5888849b58c --- /dev/null +++ b/cmake/sca/polyspace/zephyr.psopts @@ -0,0 +1,3 @@ +# tweaks specifically for Zephyr +-D__thread= +-enable-concurrency-detection diff --git a/doc/develop/sca/index.rst b/doc/develop/sca/index.rst index 37c30827d27..8269b0be483 100644 --- a/doc/develop/sca/index.rst +++ b/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 diff --git a/doc/develop/sca/polyspace.rst b/doc/develop/sca/polyspace.rst new file mode 100644 index 00000000000..438472027fc --- /dev/null +++ b/doc/develop/sca/polyspace.rst @@ -0,0 +1,93 @@ +.. _polyspace: + +Polyspace support +################# + +`Polyspace® `__ 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/bin`` must be on the list. + +For installation instructions, see +`here `__. +To use formal verification (proving the *absence* of defects), you +additionally need to install +`this `__. + +A license file must be available +in the installation folder. To request a trial license, visit `this +page `__. + +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 `__ +or `uploaded to the web interface `__ +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 `__. + - ``-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 `__ 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``