Skip to content

Commit 2871f1a

Browse files
Martin Beckerkartben
Martin Becker
authored and
kartben
committed
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 <[email protected]>
1 parent 4c5e74d commit 2871f1a

File tree

5 files changed

+324
-0
lines changed

5 files changed

+324
-0
lines changed

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

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
#!/usr/bin/python3
2+
"""
3+
Print Polyspace results on terminal, for easy review.
4+
Copyright (C) 2020-2024 The MathWorks, Inc.
5+
"""
6+
7+
# SPDX-License-Identifier: Apache-2.0
8+
9+
import argparse
10+
import os
11+
import sys
12+
from collections import Counter
13+
14+
15+
def _parse_findings(filename: str, ignore_metrics=True):
16+
"""Parse CSV file"""
17+
csv_sep = '\t' # Polyspace default separator
18+
19+
def consume_header(oneline):
20+
parts = oneline.split(csv_sep)
21+
header.extend([p.strip() for p in parts])
22+
23+
def consume_data(oneline):
24+
columns = oneline.split(csv_sep)
25+
return dict(zip(header, columns, strict=True))
26+
27+
findings = []
28+
header = []
29+
with open(filename, encoding="latin-1") as fp:
30+
for lno, line in enumerate(fp):
31+
if lno == 0:
32+
consume_header(line.rstrip())
33+
else:
34+
onefind = consume_data(line.rstrip())
35+
if onefind and (not ignore_metrics or onefind.get('Family', '') != 'Code Metric'):
36+
findings.append(onefind)
37+
# --
38+
return findings
39+
40+
41+
def print_sorted(mydict, maxlines=0):
42+
"""Print a dict sorted by value, largest first"""
43+
44+
for lno, cnt_and_fil in enumerate(
45+
sorted(((cnt, fil) for fil, cnt in mydict.items()), reverse=True), start=1
46+
):
47+
print(f" {cnt_and_fil[0]} issues in {cnt_and_fil[1]}")
48+
if lno >= maxlines and maxlines != 0:
49+
break
50+
51+
52+
def main(argv):
53+
# 1. command line arguments as required by your script
54+
parser = argparse.ArgumentParser(description='Print results to console', allow_abbrev=False)
55+
parser.add_argument('file', type=str, help='output file from polyspace-results-export')
56+
parser.add_argument('--details', action='store_true', help='print details')
57+
args = parser.parse_args()
58+
59+
# 2. parsing the Polyspace files -> report
60+
findings = _parse_findings(args.file)
61+
print("-= Polyspace Static Code Analysis results =-")
62+
63+
# 3. print details
64+
if args.details:
65+
for f in findings:
66+
print(
67+
f"{f.get('File', 'unknown file')}:"
68+
+ f"{f.get('Line', '?')}:"
69+
+ f"{f.get('Col', '?')}: "
70+
+ f"{f.get('Family', '')} {f.get('Check', 'Defect')}"
71+
)
72+
73+
# 3. summary by category and file
74+
print("By type:")
75+
family = Counter([f.get('Family', 'Defect') for f in findings])
76+
print_sorted(family)
77+
print("Top 10 files:")
78+
files = Counter([os.path.basename(f.get('File', 'Unknown')) for f in findings])
79+
print_sorted(files, 10)
80+
print(f"SCA found {len(findings)} issues in total")
81+
return 0
82+
83+
84+
if __name__ == "__main__":
85+
main(sys.argv[1:])

‎cmake/sca/polyspace/sca.cmake‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
#
3+
# Copyright (c) 2024, The MathWorks, Inc.
4+
5+
include(boards)
6+
include(git)
7+
include(extensions)
8+
include(west)
9+
10+
# find Polyspace, stop if missing
11+
find_program(POLYSPACE_CONFIGURE_EXE NAMES polyspace-configure)
12+
if(NOT POLYSPACE_CONFIGURE_EXE)
13+
message(FATAL_ERROR "Polyspace not found. For install instructions, see https://mathworks.com/help/bugfinder/install")
14+
else()
15+
cmake_path(GET POLYSPACE_CONFIGURE_EXE PARENT_PATH POLYSPACE_BIN)
16+
message(STATUS "Found SCA: Polyspace (${POLYSPACE_BIN})")
17+
endif()
18+
find_program(POLYSPACE_RESULTS_EXE NAMES polyspace-results-export REQUIRED)
19+
20+
21+
# Get Polyspace specific variables
22+
zephyr_get(POLYSPACE_ONLY_APP)
23+
zephyr_get(POLYSPACE_CONFIGURE_OPTIONS)
24+
zephyr_get(POLYSPACE_MODE)
25+
zephyr_get(POLYSPACE_OPTIONS)
26+
zephyr_get(POLYSPACE_OPTIONS_FILE)
27+
zephyr_get(POLYSPACE_PROG_NAME)
28+
zephyr_get(POLYSPACE_PROG_VERSION)
29+
message(TRACE "POLYSPACE_OPTIONS is ${POLYSPACE_OPTIONS}")
30+
31+
32+
# Get path and name of user application
33+
zephyr_get(APPLICATION_SOURCE_DIR)
34+
cmake_path(GET APPLICATION_SOURCE_DIR FILENAME APPLICATION_NAME)
35+
message(TRACE "APPLICATION_SOURCE_DIR is ${APPLICATION_SOURCE_DIR}")
36+
message(TRACE "APPLICATION_NAME is ${APPLICATION_NAME}")
37+
38+
39+
# process options
40+
if(POLYSPACE_ONLY_APP)
41+
set(POLYSPACE_CONFIGURE_OPTIONS ${POLYSPACE_CONFIGURE_OPTIONS} -include-sources ${APPLICATION_SOURCE_DIR}/**)
42+
message(WARNING "SCA only analyzes application code")
43+
endif()
44+
if(POLYSPACE_MODE STREQUAL "prove")
45+
message(NOTICE "POLYSPACE in proof mode")
46+
find_program(POLYSPACE_EXE NAMES polyspace-code-prover-server polyspace-code-prover)
47+
else()
48+
message(NOTICE "POLYSPACE in bugfinding mode")
49+
find_program(POLYSPACE_EXE NAMES polyspace-bug-finder-server polyspace-bug-finder)
50+
endif()
51+
if(NOT POLYSPACE_PROG_NAME)
52+
set(POLYSPACE_PROG_NAME "zephyr-${BOARD}-${APPLICATION_NAME}")
53+
endif()
54+
message(TRACE "POLYSPACE_PROG_NAME is ${POLYSPACE_PROG_NAME}")
55+
if(POLYSPACE_OPTIONS_FILE)
56+
message(TRACE "POLYSPACE_OPTIONS_FILE is ${POLYSPACE_OPTIONS_FILE}")
57+
set(POLYSPACE_OPTIONS_FILE -options-file ${POLYSPACE_OPTIONS_FILE})
58+
endif()
59+
if(POLYSPACE_PROG_VERSION)
60+
set(POLYSPACE_PROG_VERSION -verif-version '${POLYSPACE_PROG_VERSION}')
61+
else()
62+
git_describe(${APPLICATION_SOURCE_DIR} app_version)
63+
if(app_version)
64+
set(POLYSPACE_PROG_VERSION -verif-version '${app_version}')
65+
endif()
66+
endif()
67+
message(TRACE "POLYSPACE_PROG_VERSION is ${POLYSPACE_PROG_VERSION}")
68+
69+
# tell Polyspace about Zephyr specials
70+
set(POLYSPACE_OPTIONS_ZEPHYR -options-file ${CMAKE_CURRENT_LIST_DIR}/zephyr.psopts)
71+
72+
# Polyspace requires the compile_commands.json as input
73+
set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
74+
75+
# Create results directory
76+
set(POLYSPACE_RESULTS_DIR ${CMAKE_BINARY_DIR}/sca/polyspace)
77+
set(POLYSPACE_RESULTS_FILE ${POLYSPACE_RESULTS_DIR}/results.csv)
78+
file(MAKE_DIRECTORY ${POLYSPACE_RESULTS_DIR})
79+
message(TRACE "POLYSPACE_RESULTS_DIR is ${POLYSPACE_RESULTS_DIR}")
80+
set(POLYSPACE_OPTIONS_FILE_BASE ${POLYSPACE_RESULTS_DIR}/polyspace.psopts)
81+
82+
83+
#####################
84+
# mandatory targets #
85+
#####################
86+
87+
add_custom_target(polyspace_configure ALL
88+
COMMAND ${POLYSPACE_CONFIGURE_EXE}
89+
-allow-overwrite
90+
-silent
91+
-prog ${POLYSPACE_PROG_NAME}
92+
-compilation-database ${CMAKE_BINARY_DIR}/compile_commands.json
93+
-output-options-file ${POLYSPACE_OPTIONS_FILE_BASE}
94+
${POLYSPACE_CONFIGURE_OPTIONS}
95+
VERBATIM
96+
DEPENDS ${CMAKE_BINARY_DIR}/compile_commands.json
97+
BYPRODUCTS ${POLYSPACE_OPTIONS_FILE_BASE}
98+
USES_TERMINAL
99+
COMMAND_EXPAND_LISTS
100+
)
101+
102+
add_custom_target(polyspace-analyze ALL
103+
COMMAND ${POLYSPACE_EXE}
104+
-results-dir ${POLYSPACE_RESULTS_DIR}
105+
-options-file ${POLYSPACE_OPTIONS_FILE_BASE}
106+
${POLYSPACE_PROG_VERSION}
107+
${POLYSPACE_OPTIONS_ZEPHYR}
108+
${POLYSPACE_OPTIONS_FILE}
109+
${POLYSPACE_OPTIONS}
110+
|| ${CMAKE_COMMAND} -E true # allow to continue processing results
111+
DEPENDS ${POLYSPACE_OPTIONS_FILE_BASE}
112+
USES_TERMINAL
113+
COMMAND_EXPAND_LISTS
114+
)
115+
116+
add_custom_target(polyspace-results ALL
117+
COMMAND ${POLYSPACE_RESULTS_EXE}
118+
-results-dir ${POLYSPACE_RESULTS_DIR}
119+
-output-name ${POLYSPACE_RESULTS_FILE}
120+
-format csv
121+
|| ${CMAKE_COMMAND} -E true # allow to continue processing results
122+
VERBATIM
123+
USES_TERMINAL
124+
COMMAND_EXPAND_LISTS
125+
)
126+
127+
add_dependencies(polyspace-results polyspace-analyze)
128+
129+
130+
#####################
131+
# summarize results #
132+
#####################
133+
134+
add_custom_command(TARGET polyspace-results POST_BUILD
135+
COMMAND ${CMAKE_CURRENT_LIST_DIR}/polyspace-print-console.py
136+
${POLYSPACE_RESULTS_FILE}
137+
COMMAND
138+
${CMAKE_COMMAND} -E cmake_echo_color --cyan --bold
139+
"SCA results are here: ${POLYSPACE_RESULTS_DIR}"
140+
VERBATIM
141+
USES_TERMINAL
142+
)

‎cmake/sca/polyspace/zephyr.psopts‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# tweaks specifically for Zephyr
2+
-D__thread=
3+
-enable-concurrency-detection

‎doc/develop/sca/index.rst‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,3 +66,4 @@ The following is a list of SCA tools natively supported by Zephyr build system.
6666
gcc
6767
cpptest
6868
eclair
69+
polyspace

‎doc/develop/sca/polyspace.rst‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
.. _polyspace:
2+
3+
Polyspace support
4+
#################
5+
6+
`Polyspace® <https://mathworks.com/products/polyspace.html>`__ is
7+
a commercial static code analysis tool from MathWorks, which is certified
8+
for use in highest safety contexts. It can check compliance to coding
9+
guidelines like MISRA C and CERT C, find CWEs, detect bugs and calculate
10+
code complexity metrics. Optionally, it can run a formal proof to verify
11+
the absence of run-time errors like array out of bounds access, overflows,
12+
race conditions and more, and thus help achieving memory safety.
13+
14+
Installing
15+
**********
16+
17+
The Polyspace tools must be installed and made available in the
18+
operating system's or container's PATH variable. Specifically, the path
19+
``<polyspace_root>/polyspace/bin`` must be on the list.
20+
21+
For installation instructions, see
22+
`here <https://mathworks.com/help/bugfinder/install-polyspace.html>`__.
23+
To use formal verification (proving the *absence* of defects), you
24+
additionally need to install
25+
`this <https://mathworks.com/help/codeprover/install-polyspace.html>`__.
26+
27+
A license file must be available
28+
in the installation folder. To request a trial license, visit `this
29+
page <https://www.mathworks.com/campaigns/products/trials.html>`__.
30+
31+
Running
32+
*******
33+
34+
The code analysis can be triggered through the ``west`` command by
35+
appending the option ``-DZEPHYR_SCA_VARIANT=polyspace`` to the build,
36+
for example:
37+
38+
.. code-block:: shell
39+
40+
west build -b qemu_x86 samples/hello_world -- -DZEPHYR_SCA_VARIANT=polyspace
41+
42+
Reviewing results
43+
*****************
44+
45+
The identified issues are summarized at the end of the build and printed
46+
in the console window, along with the path of the folder containing
47+
detailed results.
48+
49+
For an efficient review, the folder should be opened in the
50+
`Polyspace user interface <https://mathworks.com/help/bugfinder/review-results-1.html>`__
51+
or `uploaded to the web interface <https://mathworks.com/help/bugfinder/gs/run-bug-finder-on-server.html>`__
52+
and reviewed there.
53+
54+
For programmatic access of the results, e.g., in the CI pipeline, the
55+
individual issues are also described in a CSV file in the results folder.
56+
57+
Configuration
58+
*************
59+
60+
By default, Polyspace scans for typical programming defects on all C and C++ sources.
61+
The following options are available to customize the default behavior:
62+
63+
.. list-table::
64+
:widths: 20 40 30
65+
:header-rows: 1
66+
67+
* - Option
68+
- Effect
69+
- Example
70+
* - ``POLYSPACE_ONLY_APP``
71+
- If set, only user code is analyzed and Zephyr sources are ignored.
72+
- ``-DPOLYSPACE_ONLY_APP=1``
73+
* - ``POLYSPACE_OPTIONS``
74+
- Provide additional command line flags, e.g., for selection of coding
75+
rules. Separate the options and their values by semicolon. For a list
76+
of options, see `here <https://mathworks.com/help/bugfinder/referencelist.html?type=analysisopt&s_tid=CRUX_topnav>`__.
77+
- ``-DPOLYSPACE_OPTIONS="-misra3;mandatory-required;-checkers;all"``
78+
* - ``POLYSPACE_OPTIONS_FILE``
79+
- Command line flags can also be provided in a text file, line by
80+
line. Provide the absolute path to the file.
81+
- ``-DPOLYSPACE_OPTIONS_FILE=/workdir/zephyr/myoptions.txt``
82+
* - ``POLYSPACE_MODE``
83+
- Switch between bugfinding and proving mode. Default is bugfinding.
84+
See `here <https://mathworks.com/help/bugfinder/gs/use-bug-finder-and-code-prover.html>`__ for more details.
85+
- ``-DPOLYSPACE_MODE=prove``
86+
* - ``POLYSPACE_PROG_NAME``
87+
- Override the name of the analyzed application. Default is board
88+
and application name.
89+
- ``-DPOLYSPACE_PROG_NAME=myapp``
90+
* - ``POLYSPACE_PROG_VERSION``
91+
- Override the version of the analyzed application. Default is taken
92+
from git-describe.
93+
- ``-DPOLYSPACE_PROG_VERSION=v1.0b-28f023``

0 commit comments

Comments
 (0)