build(tools/cbmc): integrate cbmc-viewer
Add option to the build system to call cbmc-viewer. The following
changes were necessary:
- Add option to make call of cbmc-viewer optional
- Update CBMC Application note with cbmc-viewer
- Separate CBMC run to 2 steps: compiling to GOTO program, and call
CBMC on the resulting goto program. This is necessary becasue
cbmc-viewer operates on the GOTO program.
- Rewrite extraction of summary, as XML output (required by CBMC) files
doesn't contain summary
Change-Id: Ieb2623d3b03845dcb4ab74baead81d3c0fc6dee8
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/tools/cbmc/SummaryHelpers.cmake b/tools/cbmc/SummaryHelpers.cmake
index ca53361..0e920f0 100644
--- a/tools/cbmc/SummaryHelpers.cmake
+++ b/tools/cbmc/SummaryHelpers.cmake
@@ -44,11 +44,40 @@
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")