diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst index 6dab78d5..de0e8cc9 100644 --- a/docs/getting_started/build-options.rst +++ b/docs/getting_started/build-options.rst @@ -281,6 +281,7 @@ The |RMM| build system supports the following CMake build options. HOST_MEM_SIZE , ,0x40000000 ,"Host memory size that will be used as physical granules" 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" .. _llvm_build: diff --git a/docs/resources/application-notes/cbmc.rst b/docs/resources/application-notes/cbmc.rst index 01378f69..0564ef35 100644 --- a/docs/resources/application-notes/cbmc.rst +++ b/docs/resources/application-notes/cbmc.rst @@ -57,7 +57,7 @@ The CMake system provides different modes in which CBMC can be called, along with their respective build targets. CBMC Assert -=========== +----------- In this mode CBMC is configured, so that it tries to find inputs that makes an assertion in the code to fail. If there is such an input, then CBMC provides a @@ -66,7 +66,7 @@ trace that leads to that assertion failure. To use this mode the target ``cbmc-assert`` must be passed to the build command. CBMC Analysis -============= +------------- In this mode CBMC is configured to generate assertions for certain properties in the code. The properties are selected so that for example no buffer overflows, @@ -79,7 +79,7 @@ To use this mode the target ``cbmc-analysis`` must be passed to the build command. CBMC Coverage -============= +------------- This mode checks whether all the conditions for an ABI function are covered. The pre and post conditions for the command are expressed as boolean values in @@ -96,10 +96,48 @@ command. For all the modes the summary files are committed in the source tree as baseline in ``tools/cbmc/testbenches_results/BASELINE.${MODE}``. +cbmc-viewer +=========== + +cbmc-viewer is a python package that can parse the XML output of CBMC. It +generates a html report that can be opened in a browser. The report contains a +collapsible representation of assert traces, and clickable links to the source +code locations associated with a specific trace item. + +The RMM cmake build system is capable of generating the cbmc-viewer report. If +the option ``-DRMM_CBMC_VIEWER_OUTPUT=ON`` is passed to the RMM Cmake +configuration command then the Cmake system calls cbmc-viewer and generates the +report under ``${RMM_BUILD_DIR}/tools/cbmc/cbmc_${MODE}_results/report`` + +Please note that the CMake build system currently only generates report for the +``cbmc-assert`` target. The ``cbmc-coverage`` and ``cbmc-analysis`` targets +doesn't generate trace, so generating a report wouldn't be useful. + +``cbmc-viewer`` can be installed using the following command: + +.. code-block:: bash + + python3 -m pip install cbmc-viewer + +For further details and installation guide on cbmc-viewer please see the +`cbmc-viewer github page`_. + +CBMC proof debugger +=================== + +CBMC proof debugger is an extension to a popular code editor that can be used to +load the json summaries of a CBMC analysis that is generated by cbmc-viewer. +The trace then can be explored in the built in debugger of the editor as if +stepping through an actual code execution. + +For further details on installing and using the extension please see +`CBMC proof debugger in the editor's extensions page`_. + ----- .. _CBMC Home: https://www.cprover.org/cbmc/ .. _Writing a good proof: https://model-checking.github.io/cbmc-training/management/Write-a-good-proof.html .. _github release page: https://github.com/diffblue/cbmc/releases .. _Automatically Generating Properties: https://www.cprover.org/cprover-manual/properties/ - +.. _cbmc-viewer github page: https://github.com/model-checking/cbmc-viewer +.. _CBMC proof debugger in the editor's extensions page: https://marketplace.visualstudio.com/items?itemName=model-checking.cbmc-proof-debugger diff --git a/tools/cbmc/CMakeLists.txt b/tools/cbmc/CMakeLists.txt index 7cf9c578..d6218dbf 100644 --- a/tools/cbmc/CMakeLists.txt +++ b/tools/cbmc/CMakeLists.txt @@ -4,6 +4,11 @@ # include("SourceCollectHelpers.cmake") +arm_config_option( + NAME RMM_CBMC_VIEWER_OUTPUT + HELP "Use XML format for CBMC output and generate cbmc-viewer report." + DEFAULT OFF) + if("${RMM_CBMC_STATIC_ANALYSIS}") if (NOT (${HOST_VARIANT} STREQUAL "host_cbmc")) @@ -64,6 +69,7 @@ if("${RMM_CBMC_STATIC_ANALYSIS}") WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}" COMMAND ${CMAKE_COMMAND} -DRMM_CBMC_CONFIGURATION=ANALYSIS + -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" @@ -76,6 +82,7 @@ if("${RMM_CBMC_STATIC_ANALYSIS}") WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}" COMMAND ${CMAKE_COMMAND} -DRMM_CBMC_CONFIGURATION=ASSERT + -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" diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake index 4eecfdb9..0ce1a180 100644 --- a/tools/cbmc/CheckCBMC.cmake +++ b/tools/cbmc/CheckCBMC.cmake @@ -7,6 +7,10 @@ include(FetchContent) include("${SOURCE_DIR}/tools/cbmc/SummaryHelpers.cmake") find_program(RMM_CBMC_PATH "cbmc" DOC "Path to cbmc.") +find_program(RMM_GOTO_CC_PATH "goto-cc" + DOC "Path to goto-cc.") +find_program(RMM_CBMC_VIEWER_PATH "cbmc-viewer" + DOC "Path to cbmc-viewer.") find_package(Python3 REQUIRED) find_program(CHECK_CBMC_SUMMARY_EXECUTABLE "compare_summary.py" @@ -22,23 +26,16 @@ if(NOT (EXISTS "${RMM_CBMC_PATH}")) message(FATAL_ERROR "cbmc executable not found. (${RMM_CBMC_PATH})") endif() -if("${RMM_CBMC_CONFIGURATION}" STREQUAL "COVERAGE") - set(CBMC_RESULT_FILE_SUFFIX "coverage") - set(CBMC_SUMMARY_HEADER "COVERAGE") - set(CBMC_SUMMARY_PATTERN "covered") -elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "ASSERT") - set(CBMC_RESULT_FILE_SUFFIX "assert") - set(CBMC_SUMMARY_HEADER "ASSERT") - set(CBMC_SUMMARY_PATTERN "failed") -elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "ANALYSIS") - set(CBMC_RESULT_FILE_SUFFIX "analysis") - set(CBMC_SUMMARY_HEADER "ANALYSIS") - set(CBMC_SUMMARY_PATTERN "failed") +string(TOLOWER "${RMM_CBMC_CONFIGURATION}" CBMC_RESULT_FILE_SUFFIX) + +if(RMM_CBMC_VIEWER_OUTPUT) + set(CBMC_OUT_FILE_ENDING "xml") + set(CBMC_UI_OPTION "--xml-ui") else() - message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'") + set(CBMC_OUT_FILE_ENDING "output") + set(CBMC_UI_OPTION "") endif() - set(RMM_TESTBENCH_RESULT_DIR "${BINARY_DIR}/cbmc_${CBMC_RESULT_FILE_SUFFIX}_results") set(SUMMARY_FILE "SUMMARY.${CBMC_RESULT_FILE_SUFFIX}") set(RMM_CBMC_SUMMARY_FIELD_WIDTH 38) @@ -111,7 +108,6 @@ set(cbmc_analysis_flags_list "--memory-leak-check") set(cbmc_flags_list - "--c11" "--timestamp;wall" "--verbosity;9" # Optimisation flags: @@ -148,55 +144,131 @@ separate_arguments(RMM_IMP_INCS) # Execute CBMC on the testbench files # rmm_cbmc_write_summary_header(${RMM_CBMC_SUMMARY_FIELD_WIDTH} - ${RMM_TESTBENCH_RESULT_DIR} ${SUMMARY_FILE} ${CBMC_SUMMARY_HEADER}) + ${RMM_TESTBENCH_RESULT_DIR} ${SUMMARY_FILE} ${RMM_CBMC_CONFIGURATION}) + +function(rmm_cbmc_gen_file_names + testbench_file_path + filename_prefix + out_file_ending + cmd_file_var_name + out_file_var_name + err_file_var_name) + get_filename_component(testbench_file_name "${testbench_file_path}" NAME) + get_filename_component(parent "${testbench_file_path}" DIRECTORY) + set("${cmd_file_var_name}" "${parent}/${filename_prefix}_${testbench_file_name}.cmd" PARENT_SCOPE) + set("${out_file_var_name}" "${parent}/${filename_prefix}_${testbench_file_name}.${out_file_ending}" PARENT_SCOPE) + set("${err_file_var_name}" "${parent}/${filename_prefix}_${testbench_file_name}.error" PARENT_SCOPE) +endfunction() + +function(normalise_cmd cmd_str out_var_name) + # replace the ; with space + string (REPLACE ";" " " cmd_str "${cmd_str}") + set("${out_var_name}" "${cmd_str}" PARENT_SCOPE) +endfunction() foreach(testbench_file ${TESTBENCH_FILES}) string(REPLACE ${TESTBENCH_DIR}/ "" testbench_filename ${testbench_file}) string(REGEX REPLACE "\\.[^\\.]*$" "" entry_point "${testbench_filename}") - set(cmd - ${RMM_CBMC_PATH} - ${cbmc_flags_list} + set(RMM_GOTO_PROG_NAME "${RMM_TESTBENCH_RESULT_DIR}/rmm_${entry_point}.goto") + + # Set the names of output files + string(REPLACE ${TESTBENCH_DIR} ${RMM_TESTBENCH_RESULT_DIR} OUT_FILE_NAME_PREFIX "${testbench_file}") + rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "cbmc" "${CBMC_OUT_FILE_ENDING}" + cbmc_cmd_file cbmc_output_file cbmc_error_file) + rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "cbmc_prop" "xml" + cbmc_prop_cmd_file cbmc_prop_output_file cbmc_prop_error_file) + rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "goto_cc" "output" + goto_cc_cmd_file goto_cc_output_file goto_cc_error_file) + rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "cbmc_viewer" "output" + cbmc_viewer_cmd_file cbmc_viewer_output_file cbmc_viewer_error_file) + set(CBMC_VIEWER_REPORT_DIR "${RMM_TESTBENCH_RESULT_DIR}/report_${entry_point}") + + set(goto_cc_cmd + ${RMM_GOTO_CC_PATH} + ${cbmc_compiler_options} + ${cbmc_defines_list} "--function;${entry_point}" + "-o;${RMM_GOTO_PROG_NAME}" ${RMM_IMP_INCS} - ${cbmc_unwinds_list} - ${cbmc_defines_list} ${RMM_IMP_SRCS} - ${testbench_file}) + ${testbench_file} + ) - # Set the names of output files - string(REPLACE ${TESTBENCH_DIR} ${RMM_TESTBENCH_RESULT_DIR} output_file ${testbench_file}) - set(error_file ${output_file}) - set(cmd_file ${output_file}) - string(APPEND output_file ".${CBMC_RESULT_FILE_SUFFIX}" ".output") - string(APPEND error_file ".${CBMC_RESULT_FILE_SUFFIX}" ".error") - string(APPEND cmd_file ".${CBMC_RESULT_FILE_SUFFIX}" ".cmd") - - # remove the absolute path making it relative - string (REPLACE "${SOURCE_DIR}/" "" cmd "${cmd}") - # replace the ; with space - string (REPLACE ";" " " CMD_STR "${cmd}") - # add double quotes - string (REPLACE "\"" "\\\"" CMD_STR "${CMD_STR}") - # escape parentheses - string (REPLACE "(" "\"(" CMD_STR "${CMD_STR}") - string (REPLACE ")" ")\"" CMD_STR "${CMD_STR}") - file(WRITE ${cmd_file} "${CMD_STR}") + set(cbmc_cmd + ${RMM_CBMC_PATH} + ${CBMC_UI_OPTION} + ${cbmc_flags_list} + ${cbmc_unwinds_list} + ${RMM_GOTO_PROG_NAME}) + + set(cbmc_prop_cmd + ${RMM_CBMC_PATH} + ${cbmc_flags_list} + "--xml-ui" + "--show-properties" + ${RMM_GOTO_PROG_NAME}) + + set(cbmc_viewer_cmd + "${RMM_CBMC_VIEWER_PATH}" + "--goto;${RMM_GOTO_PROG_NAME}" + "--result;${cbmc_output_file}" + "--property;${cbmc_prop_output_file}" + "--srcdir;${CMAKE_SOURCE_DIR}" + "--reportdir;${CBMC_VIEWER_REPORT_DIR}") + + # remove the absolute path making it relative (shorten the command line) + string (REPLACE "${SOURCE_DIR}/" "" goto_cc_cmd "${goto_cc_cmd}") + + normalise_cmd("${goto_cc_cmd}" GOTO_CC_CMD_STR) + normalise_cmd("${cbmc_cmd}" CBMC_CMD_STR) + + file(WRITE ${goto_cc_cmd_file} "${GOTO_CC_CMD_STR}") + file(WRITE ${cbmc_cmd_file} "${CBMC_CMD_STR}") execute_process(COMMAND ${CMAKE_COMMAND} -E echo_append "CBMC: ${testbench_file}... ") execute_process( - COMMAND ${cmd} + COMMAND ${goto_cc_cmd} + RESULT_VARIABLE res_var + OUTPUT_FILE ${goto_cc_output_file} + ERROR_FILE ${goto_cc_error_file}) + if (NOT ${res_var} EQUAL "0") + message(FATAL_ERROR "Compiling testbench with goto-cc failed. For details see: ${goto_cc_error_file}") + endif() + + execute_process( + COMMAND ${cbmc_cmd} + RESULT_VARIABLE res_var + OUTPUT_FILE ${cbmc_output_file} + ERROR_FILE ${cbmc_error_file}) + + if(RMM_CBMC_VIEWER_OUTPUT) + normalise_cmd("${cbmc_prop_cmd}" CBMC_PROP_CMD_STR) + file(WRITE ${cbmc_prop_cmd_file} "${CBMC_PROP_CMD_STR}") + execute_process( + COMMAND ${cbmc_prop_cmd} + RESULT_VARIABLE res_var + OUTPUT_FILE ${cbmc_prop_output_file} + ERROR_FILE ${cbmc_prop_error_file}) + + normalise_cmd("${cbmc_viewer_cmd}" CBMC_VIEWER_CMD_STR) + file(WRITE ${cbmc_viewer_cmd_file} "${CBMC_VIEWER_CMD_STR}") + execute_process( + COMMAND ${cbmc_viewer_cmd} RESULT_VARIABLE res_var - OUTPUT_FILE ${output_file} - ERROR_FILE ${error_file} - ) + OUTPUT_FILE ${cbmc_viewer_output_file} + ERROR_FILE ${cbmc_viewer_error_file}) + if (NOT ${res_var} EQUAL "0") + message(FATAL_ERROR "Failed to run cbmc-viewer. For details see: ${goto_cc_error_file}") + endif() + endif() execute_process(COMMAND ${CMAKE_COMMAND} -E echo "DONE") - rmm_cbmc_append_summary("${testbench_filename}" "${output_file}" - ${RMM_CBMC_SUMMARY_FIELD_WIDTH} ${RMM_TESTBENCH_RESULT_DIR} ${SUMMARY_FILE} - ${CBMC_SUMMARY_PATTERN}) + rmm_cbmc_append_summary("${testbench_filename}" "${cbmc_output_file}" + "${CBMC_RESULT_FILE_SUFFIX}-${CBMC_OUT_FILE_ENDING}" + ${RMM_CBMC_SUMMARY_FIELD_WIDTH} ${RMM_TESTBENCH_RESULT_DIR} ${SUMMARY_FILE}) endforeach() message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}") diff --git a/tools/cbmc/SummaryHelpers.cmake b/tools/cbmc/SummaryHelpers.cmake index ca53361e..0e920f07 100644 --- a/tools/cbmc/SummaryHelpers.cmake +++ b/tools/cbmc/SummaryHelpers.cmake @@ -44,11 +44,40 @@ function(rmm_cbmc_write_summary_header summary_width result_dir file summary_hea rmm_cbmc_append_separator(${summary_width} ${result_dir} ${file}) endfunction() -function(rmm_cbmc_append_summary testbench_filename output_file summary_width result_dir file summary_pattern) +function (rmm_cbmc_generate_summary file mode summary_var_name) + execute_process(COMMAND grep -cE "Solving with" ${output_file} OUTPUT_VARIABLE iteration_counts) + if(${iteration_counts} EQUAL "0") + set("${summary_var_name}" "" PARENT_SCOPE) + return() + endif() + if(("${mode}" STREQUAL "assert-output") OR ("${mode}" STREQUAL "analysis-output")) + execute_process(COMMAND grep -cE "\\[.*\\] .*: SUCCESS" ${output_file} OUTPUT_VARIABLE passed_asserts) + execute_process(COMMAND grep -cE "\\[.*\\] .*: FAILURE" ${output_file} OUTPUT_VARIABLE failed_asserts) + math(EXPR all_asserts "${passed_asserts} + ${failed_asserts}") + set("${summary_var_name}" "** ${failed_asserts} of ${all_asserts} failed (${iteration_counts} iterations)" PARENT_SCOPE) + elseif(("${mode}" STREQUAL "assert-xml") OR ("${mode}" STREQUAL "analysis-xml")) + execute_process(COMMAND grep -cE "property=.*status=.SUCCESS" ${output_file} OUTPUT_VARIABLE passed_asserts) + execute_process(COMMAND grep -cE "property=.*status=.FAILURE" ${output_file} OUTPUT_VARIABLE failed_asserts) + math(EXPR all_asserts "${passed_asserts} + ${failed_asserts}") + set("${summary_var_name}" "** ${failed_asserts} of ${all_asserts} failed (${iteration_counts} iterations)" PARENT_SCOPE) + elseif(("${mode}" STREQUAL "coverage-xml") OR ("${mode}" STREQUAL "coverage-output")) + execute_process(COMMAND grep -cE "\\[.*\\] file .* line .* function .*: SATISFIED" ${output_file} OUTPUT_VARIABLE passed_coverages) + execute_process(COMMAND grep -cE "\\[.*\\] file .* line .* function .*: FAILED" ${output_file} OUTPUT_VARIABLE failed_coverages) + math(EXPR all_coverages "${passed_coverages} + ${failed_coverages}") + math(EXPR cover_percent_int_part "${passed_coverages} * 100 / ${all_coverages}") + math(EXPR cover_percent_dec_part "(${passed_coverages} * 1000 / ${all_coverages}) % 10") + set("${summary_var_name}" "** ${passed_coverages} of ${all_coverages} covered (${cover_percent_int_part}.${cover_percent_dec_part}%)" PARENT_SCOPE) + else() + message(FATAL_ERROR "Unknown mode ${mode}") + endif() + +endfunction() + +function(rmm_cbmc_append_summary testbench_filename output_file mode summary_width result_dir file) rmm_cbmc_align_to_middle(${summary_width} " " ${testbench_filename}) set(testbench_filename "${aligned_text}") - execute_process(COMMAND grep -E "${summary_pattern}" ${output_file} OUTPUT_VARIABLE testbench_result) + rmm_cbmc_generate_summary("${output_file}" "${mode}" testbench_result) if("${testbench_result}" STREQUAL "") rmm_cbmc_align_to_middle(${summary_width} " " "N/A")