proofs: support code coverage using cbmc-viewer

A coverage report summarizing what lines of source code were
exercised by CBMC.

Tested with cbmc-viewer 3.11.1

Author: ligurio

proofs/cbmc/CMakeLists.txt

@@ -1,4 +1,5 @@
 find_program(CBMC_BIN cbmc)
+find_program(CBMC_VIEWER_BIN cbmc-viewer)
 
 list(APPEND GENERAL_CBMC_OPTS
   --bounds-check
@@ -28,6 +29,9 @@ list(APPEND GENERAL_CBMC_OPTS
 )
 
 set(DEFAULT_TIMEOUT 30)
+set(CBMC_REPORT_PATH ${CMAKE_CURRENT_BINARY_DIR}/report)
+
+file(MAKE_DIRECTORY ${CBMC_REPORT_PATH})
 
 list(APPEND DEFAULT_LUA_CBMC_OPTS
   ${GENERAL_CBMC_OPTS}
@@ -44,6 +48,7 @@ elseif (USE_LUAJIT)
 endif()
 
 set(PROOF_TARGETS "")
+set(PROOF_REPORTS "")
 
 function(create_proof)
   cmake_parse_arguments(
@@ -84,6 +89,56 @@ function(create_proof)
     TIMEOUT ${DEFAULT_TIMEOUT}
   )
   set(PROOF_TARGETS ${PROOF_TARGETS} ${test_name} PARENT_SCOPE)
+  set(PROOF_REPORTS ${PROOF_REPORTS} ${test_name}-report PARENT_SCOPE)
+
+  set(PROPERTY_REPORT ${test_name}_property.json)
+  set(COVERAGE_REPORT ${test_name}_coverage.json)
+  set(RESULT_REPORT ${test_name}_result.json)
+
+  add_custom_target(${RESULT_REPORT}
+    COMMAND ${CBMC_BIN} $<TARGET_FILE:${test_name}>
+      ${DEFAULT_CBMC_OPTS} --unwinding-assertions --trace --json-ui > ${RESULT_REPORT} || (exit 0)
+    DEPENDS ${test_name}
+    BYPRODUCTS ${RESULT_REPORT}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
+    COMMENT "Build ${RESULT_REPORT}"
+  )
+
+  add_custom_target(${PROPERTY_REPORT}
+    COMMAND ${CBMC_BIN} $<TARGET_FILE:${test_name}>
+      ${DEFAULT_CBMC_OPTS} --unwinding-assertions --show-properties --json-ui > ${PROPERTY_REPORT}
+    DEPENDS ${test_name}
+    BYPRODUCTS ${PROPERTY_REPORT}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
+    COMMENT "Build ${PROPERTY_REPORT}"
+  )
+
+  add_custom_target(${COVERAGE_REPORT}
+    COMMAND ${CBMC_BIN} $<TARGET_FILE:${test_name}>
+      ${DEFAULT_CBMC_OPTS} --cover location --json-ui > ${COVERAGE_REPORT}
+    DEPENDS ${test_name}
+    BYPRODUCTS ${COVERAGE_REPORT}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
+    COMMENT "Build ${COVERAGE_REPORT}"
+  )
+
+  list(APPEND CBMC_VIEWER_COMMAND
+    ${CBMC_VIEWER_BIN}
+    --goto $<TARGET_FILE:${test_name}>
+    --result ${RESULT_REPORT}
+    --coverage ${COVERAGE_REPORT}
+    --property ${PROPERTY_REPORT}
+    --reportdir ${CBMC_REPORT_PATH}/${test_name}
+    --srcdir ${LUA_INCLUDE_DIR}
+    --wkdir ${LUA_INCLUDE_DIR}
+  )
+
+  add_custom_target(${test_name}-report
+    COMMAND ${CBMC_VIEWER_COMMAND}
+    DEPENDS ${RESULT_REPORT} ${PROPERTY_REPORT} ${COVERAGE_REPORT}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
+    COMMENT "Build CBMC code coverage report for ${test_name}"
+  )
 endfunction()
 
 ##################################################################
@@ -96,3 +151,7 @@ add_custom_target(build_cbmc_proofs
   DEPENDS ${PROOF_TARGETS}
   COMMENT "Building CBMC proofs"
 )
+add_custom_target(build_cbmc_reports
+  DEPENDS ${PROOF_REPORTS}
+  COMMENT "Building CBMC reports"
+)

proofs/cbmc/README.md

@@ -3,8 +3,14 @@
 ### Usage
 
 ```
+python -m venv venv_cbmc_viewer
+source venv_cbmc_viewer/bin/activate
+python3 -m pip install cbmc-viewer 3.11.1
+sudo apt install universal-ctags
+
 nix-shell -p cbmc
 cmake -S . -B build -DUSE_LUA=ON -DCMAKE_BUILD_TYPE=Debug -DCMAKE_C_COMPILER=goto-cc -DENABLE_CBMC_PROOFS=ON -DENABLE_LUA_APICHECK=ON -DENABLE_LUA_ASSERT=ON
 cmake --build build --target build_cbmc_proofs --parallel
 ctest --test-dir build --output-on-failure --timeout 15 --tests-regex luaL_makeseed --verbose
+cmake --build build -t luaL_makeseed-report --parallel
 ```