1#
2# SPDX-License-Identifier: BSD-3-Clause
3# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
4#
5
6#
7# Helper functions for formatting the summary file
8#
9
10function(rmm_cbmc_align_to_middle field_width padding_character text)
11  set (pad_pool "")
12  foreach(i RANGE ${field_width})
13    string(APPEND pad_pool ${padding_character})
14  endforeach()
15  string(LENGTH ${text} text_len)
16  math(EXPR leading_space "(${field_width} - ${text_len}) / 2")
17  math(EXPR trailing_space "${field_width} - ${text_len} - ${leading_space}")
18  string (SUBSTRING ${pad_pool} 0 ${leading_space} leading_spaces)
19  string (SUBSTRING ${pad_pool} 0 ${trailing_space} trailing_spaces)
20
21  set(aligned_text "")
22  string (APPEND aligned_text "${leading_spaces}" "${text}" "${trailing_spaces}")
23  set(aligned_text "${aligned_text}" PARENT_SCOPE)
24endfunction()
25
26function(rmm_cbmc_append_separator summary_width result_dir file)
27  rmm_cbmc_align_to_middle(${summary_width} "-" "-")
28  set(separator_line "")
29  string(APPEND separator_line "+" "${aligned_text}" "+" "${aligned_text}" "+\n")
30  file(APPEND ${result_dir}/${file} ${separator_line})
31endfunction()
32
33function(rmm_cbmc_write_summary_header summary_width result_dir file summary_header)
34  file(MAKE_DIRECTORY ${result_dir})
35  file(WRITE ${result_dir}/${file} "")
36  rmm_cbmc_append_separator(${summary_width} ${result_dir} ${file})
37  rmm_cbmc_align_to_middle(${summary_width} " " "FILENAME")
38  set(field1 "${aligned_text}")
39  rmm_cbmc_align_to_middle(${summary_width} " " "${summary_header}")
40  set(field2 "${aligned_text}")
41  set(header "")
42  string(APPEND header "|" "${field1}" "|" "${field2}" "|\n")
43  file(APPEND ${result_dir}/${file} ${header})
44  rmm_cbmc_append_separator(${summary_width} ${result_dir} ${file})
45endfunction()
46
47function (rmm_cbmc_generate_summary file mode summary_var_name)
48  execute_process(COMMAND grep -cE "Solving with" ${output_file} OUTPUT_VARIABLE iteration_counts)
49  if(${iteration_counts} EQUAL "0")
50    set("${summary_var_name}" "" PARENT_SCOPE)
51    return()
52  endif()
53  if(("${mode}" STREQUAL "assert-output") OR ("${mode}" STREQUAL "analysis-output"))
54    execute_process(COMMAND grep -cE "\\[.*\\] .*: SUCCESS" ${output_file} OUTPUT_VARIABLE passed_asserts)
55    execute_process(COMMAND grep -cE "\\[.*\\] .*: FAILURE" ${output_file} OUTPUT_VARIABLE failed_asserts)
56    math(EXPR all_asserts "${passed_asserts} + ${failed_asserts}")
57    set("${summary_var_name}" "** ${failed_asserts} of ${all_asserts} failed (${iteration_counts} iterations)" PARENT_SCOPE)
58  elseif(("${mode}" STREQUAL "assert-xml") OR ("${mode}" STREQUAL "analysis-xml"))
59    execute_process(COMMAND grep -cE "property=.*status=.SUCCESS" ${output_file} OUTPUT_VARIABLE passed_asserts)
60    execute_process(COMMAND grep -cE "property=.*status=.FAILURE" ${output_file} OUTPUT_VARIABLE failed_asserts)
61    math(EXPR all_asserts "${passed_asserts} + ${failed_asserts}")
62    set("${summary_var_name}" "** ${failed_asserts} of ${all_asserts} failed (${iteration_counts} iterations)" PARENT_SCOPE)
63  elseif(("${mode}" STREQUAL "coverage-xml") OR ("${mode}" STREQUAL "coverage-output"))
64    execute_process(COMMAND grep -cE "\\[.*\\] file .* line .* function .*: SATISFIED" ${output_file} OUTPUT_VARIABLE passed_coverages)
65    execute_process(COMMAND grep -cE "\\[.*\\] file .* line .* function .*: FAILED" ${output_file} OUTPUT_VARIABLE failed_coverages)
66    math(EXPR all_coverages "${passed_coverages} + ${failed_coverages}")
67    math(EXPR cover_percent_int_part "${passed_coverages} * 100 / ${all_coverages}")
68    math(EXPR cover_percent_dec_part "(${passed_coverages} * 1000 / ${all_coverages}) % 10")
69    set("${summary_var_name}" "** ${passed_coverages} of ${all_coverages} covered (${cover_percent_int_part}.${cover_percent_dec_part}%)" PARENT_SCOPE)
70  else()
71    message(FATAL_ERROR "Unknown mode ${mode}")
72  endif()
73
74endfunction()
75
76function(rmm_cbmc_append_summary testbench_filename output_file mode summary_width result_dir file)
77  rmm_cbmc_align_to_middle(${summary_width} " " ${testbench_filename})
78  set(testbench_filename "${aligned_text}")
79
80  rmm_cbmc_generate_summary("${output_file}" "${mode}" testbench_result)
81
82  if("${testbench_result}" STREQUAL "")
83    rmm_cbmc_align_to_middle(${summary_width} " " "N/A")
84    set(testbench_result "${aligned_text}")
85  endif()
86
87  string(REPLACE "\n" "" testbench_result "${testbench_result}")
88  string(REGEX REPLACE "[^\\*]*\\*\\*[\\s]*" "" testbench_result "${testbench_result}")
89
90  rmm_cbmc_align_to_middle(${summary_width} " " ${testbench_result})
91  set(testbench_result "${aligned_text}")
92
93  string(APPEND summary_data "|${testbench_filename}|${testbench_result}|\n")
94  file(APPEND ${result_dir}/${file} ${summary_data})
95  rmm_cbmc_append_separator(${summary_width} ${result_dir} ${file})
96endfunction()
97