Merge "build(tools/cbmc): integrate cbmc-viewer" into integration

TF-RMM · Dec 18, 2023 · 236188a · 236188a
2 parents 5e5a39d + 0361dcb
commit 236188a
Show file tree

Hide file tree

Showing 5 changed files with 200 additions and 53 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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")