diff --git a/cmake/sca/polyspace/README.md b/cmake/sca/polyspace/README.md new file mode 100644 index 000000000000000..f08921f3f0196a8 --- /dev/null +++ b/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/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` | diff --git a/cmake/sca/polyspace/polyspace-print-console.py b/cmake/sca/polyspace/polyspace-print-console.py new file mode 100755 index 000000000000000..05781a384e3588e --- /dev/null +++ b/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:]) diff --git a/cmake/sca/polyspace/sca.cmake b/cmake/sca/polyspace/sca.cmake new file mode 100644 index 000000000000000..8d7ddae255a79ba --- /dev/null +++ b/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 diff --git a/cmake/sca/polyspace/zephyr.psopts b/cmake/sca/polyspace/zephyr.psopts new file mode 100644 index 000000000000000..5888849b58cc5c6 --- /dev/null +++ b/cmake/sca/polyspace/zephyr.psopts @@ -0,0 +1,3 @@ +# tweaks specifically for Zephyr +-D__thread= +-enable-concurrency-detection