feat(tools/cbmc): add option to test a single testbench
This feature becomes useful when working on a single testbench. There is
no need to wait for the other testbenches to finish analysis.
Change-Id: I277b37ef796c66c26c03c4b3ca2cd29c705cfc88
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst
index de0e8cc..805482b 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -282,6 +282,7 @@
RMM_COVERAGE ,ON | OFF ,OFF ,"Enable coverage analysis"
RMM_HTML_COV_REPORT ,ON | OFF ,ON ,"Enable HTML output report for coverage analysis"
RMM_CBMC_VIEWER_OUTPUT ,ON | OFF ,OFF ,"Generate report of CBMC results using the tool cbmc-viewer"
+ RMM_CBMC_SINGLE_TESTBENCH , ,OFF ,"Run CBMC on a single testbench instead on all of them"
.. _llvm_build:
diff --git a/docs/resources/application-notes/cbmc.rst b/docs/resources/application-notes/cbmc.rst
index 0564ef3..60569be 100644
--- a/docs/resources/application-notes/cbmc.rst
+++ b/docs/resources/application-notes/cbmc.rst
@@ -53,6 +53,12 @@
For an example build command please refer to :ref:`RMM Build Examples`
+The CMake system by default runs CBMC on all the testbenches. This can take a
+long time, and it can be convenient to run a single testcase at once. This can
+be achieved using the option ``-DRMM_CBMC_SINGLE_TESTBENCH="testbench_name"``.
+The list of possible ``testbench_name``s can be listed by using the option
+``-DRMM_CBMC_SINGLE_TESTBENCH="help"``.
+
The CMake system provides different modes in which CBMC can be called, along
with their respective build targets.
diff --git a/tools/cbmc/CMakeLists.txt b/tools/cbmc/CMakeLists.txt
index d6218db..7d11b72 100644
--- a/tools/cbmc/CMakeLists.txt
+++ b/tools/cbmc/CMakeLists.txt
@@ -9,12 +9,36 @@
HELP "Use XML format for CBMC output and generate cbmc-viewer report."
DEFAULT OFF)
+arm_config_option(
+ NAME RMM_CBMC_SINGLE_TESTBENCH
+ HELP "Run CBMC on a single testbench instead on all of them."
+ DEFAULT OFF)
+
if("${RMM_CBMC_STATIC_ANALYSIS}")
+ set (TESTBENCH_DIR "${CMAKE_CURRENT_SOURCE_DIR}/testbenches")
+
if (NOT (${HOST_VARIANT} STREQUAL "host_cbmc"))
message(FATAL_ERROR "cbmc analysis requires host variant `host_cbmc`. (Add `-DHOST_VARIANT=host_cbmc`)")
endif()
+ file(GLOB_RECURSE TESTBENCH_FILES "${TESTBENCH_DIR}/*.c")
+ if(RMM_CBMC_SINGLE_TESTBENCH)
+ set(TESTBENCH_NAMES ${TESTBENCH_FILES})
+ list(TRANSFORM TESTBENCH_NAMES REPLACE "\\.c" "")
+ list(TRANSFORM TESTBENCH_NAMES REPLACE "${TESTBENCH_DIR}/" "")
+ if (NOT "${RMM_CBMC_SINGLE_TESTBENCH}" IN_LIST TESTBENCH_NAMES)
+ message(STATUS "Invalid testbench name '${RMM_CBMC_SINGLE_TESTBENCH}'")
+ message(STATUS "The valid options are: ")
+ foreach(tb ${TESTBENCH_NAMES})
+ message(STATUS " ${tb}")
+ endforeach()
+ message(FATAL_ERROR "Invalid testbench name '${RMM_CBMC_SINGLE_TESTBENCH}'")
+ else()
+ set(TESTBENCH_FILES "${TESTBENCH_DIR}/${RMM_CBMC_SINGLE_TESTBENCH}.c")
+ endif()
+ endif()
+
#
# Create the list of source files and include directories that are to be
# included in the analysis.
@@ -59,7 +83,8 @@
-DRMM_CBMC_CONFIGURATION=COVERAGE
-DSOURCE_DIR=${CMAKE_SOURCE_DIR}
-DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
- -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+ -DTESTBENCH_DIR="${TESTBENCH_DIR}"
+ -DTESTBENCH_FILES="${TESTBENCH_FILES}"
-DRMM_IMP_SRCS="${rmm_implementation_srcs}"
-DRMM_IMP_INCS="${rmm_implementation_includes}"
-P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
@@ -72,7 +97,8 @@
-DRMM_CBMC_VIEWER_OUTPUT=${RMM_CBMC_VIEWER_OUTPUT}
-DSOURCE_DIR=${CMAKE_SOURCE_DIR}
-DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
- -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+ -DTESTBENCH_DIR="${TESTBENCH_DIR}"
+ -DTESTBENCH_FILES="${TESTBENCH_FILES}"
-DRMM_IMP_SRCS="${rmm_implementation_srcs}"
-DRMM_IMP_INCS="${rmm_implementation_includes}"
-P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
@@ -85,7 +111,8 @@
-DRMM_CBMC_VIEWER_OUTPUT=${RMM_CBMC_VIEWER_OUTPUT}
-DSOURCE_DIR=${CMAKE_SOURCE_DIR}
-DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
- -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+ -DTESTBENCH_DIR="${TESTBENCH_DIR}"
+ -DTESTBENCH_FILES="${TESTBENCH_FILES}"
-DRMM_IMP_SRCS="${rmm_implementation_srcs}"
-DRMM_IMP_INCS="${rmm_implementation_includes}"
-P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake
index 1f9d030..e31e82f 100644
--- a/tools/cbmc/CheckCBMC.cmake
+++ b/tools/cbmc/CheckCBMC.cmake
@@ -132,7 +132,8 @@
message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'")
endif()
-file(GLOB_RECURSE TESTBENCH_FILES "${TESTBENCH_DIR}/*.c")
+# Convert the space separated strings to a CMake list
+string(REPLACE " " ";" TESTBENCH_FILES "${TESTBENCH_FILES}")
#
# Create semi-colon separated list from white-space seperated ones.
@@ -273,10 +274,12 @@
endforeach()
message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}")
+list(TRANSFORM TESTBENCH_FILES REPLACE "${TESTBENCH_DIR}/" "" OUTPUT_VARIABLE TESTBENCH_FILENAMES)
execute_process(
WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
COMMAND ${CHECK_CBMC_SUMMARY_EXECUTABLE}
${CMAKE_SOURCE_DIR}/tools/cbmc/testbenches_results/BASELINE.${CBMC_RESULT_FILE_SUFFIX}
+ --testbench-files "${TESTBENCH_FILENAMES}"
${RMM_TESTBENCH_RESULT_DIR}/${SUMMARY_FILE}
OUTPUT_VARIABLE CHECK_SUMMARY_OUTPUT
ERROR_VARIABLE CHECK_SUMMARY_ERROR
diff --git a/tools/cbmc/compare_summary.py b/tools/cbmc/compare_summary.py
index ca4e4df..5cec772 100755
--- a/tools/cbmc/compare_summary.py
+++ b/tools/cbmc/compare_summary.py
@@ -16,6 +16,7 @@
import argparse
import logging
+import ntpath
import re
import sys
@@ -158,12 +159,20 @@
# The number of asserts in the code can change frequently, so don't do a check on it.
-def compare_summary_lists(baseline_list, actual_list, comparator):
+def compare_summary_lists(baseline_list, actual_list, comparator, testbench_list):
"""
Compare two summary lists.
- List items are expected to be in the format of a tuple:
- (testbench name, first integer value, second integer value)
+ Arguments:
+ baseline_list -- List of testbench baseline results
+ actual_list -- List of testbench actual results
+ comparator -- A function that can compare 2 testbench result items
+ testbench_list -- A list of testbenches to be considered. If None, all
+ testbenches are considered
+
+ baseline_list and actual_list items are expected to be in the format of a
+ tuple: (testbench name, first integer value, second integer value)
+
"""
# TODO: check for duplicated lines
baseline = {summary[0]: summary[1:] for summary in baseline_list}
@@ -174,6 +183,10 @@
# that was triggered by a tetsbench addition/deletion.
actual_extra = {}
+ if testbench_list is not None:
+ baseline = {k: v for k, v in baseline.items() if k in testbench_list}
+ actual_list = [e for e in actual_list if e[0] in testbench_list]
+
for summary in actual_list:
testbench_name = summary[0]
if testbench_name not in baseline.keys():
@@ -191,7 +204,7 @@
)
-def compare_summary_files(baseline_filename, actual_filename):
+def compare_summary_files(baseline_filename, actual_filename, testbench_list):
"""
Compare two summary files.
"""
@@ -213,7 +226,7 @@
raise ParseException(f"Unknown summary type {base_type}")
compare_summary_lists(
- base_summary_list, actual_summary_list, comparators[base_type]
+ base_summary_list, actual_summary_list, comparators[base_type], testbench_list
)
@@ -223,10 +236,9 @@
"""
parser = argparse.ArgumentParser(description="compare CBMC summary siles")
parser.add_argument(
- "-v", "--verbosity",
+ "--testbench-files",
type=str,
- choices='',
- help="The path of the baseline summary file.",
+ help="A semicolon (;) separated list of files to check in the summaries.",
)
parser.add_argument(
"baseline",
@@ -238,8 +250,13 @@
)
args = parser.parse_args()
+ if args.testbench_files:
+ testbench_list = [ntpath.basename(p) for p in args.testbench_files.split(";")]
+ else:
+ testbench_list = None
+
try:
- compare_summary_files(args.baseline, args.actual)
+ compare_summary_files(args.baseline, args.actual, testbench_list)
except ParseException as exc:
logging.error("Failed to compare summaries:")
logging.error(f"{str(exc)}")