1# 2# SPDX-License-Identifier: BSD-3-Clause 3# SPDX-FileCopyrightText: Copyright TF-RMM Contributors. 4# 5 6include(FetchContent) 7include("${SOURCE_DIR}/tools/cbmc/SummaryHelpers.cmake") 8find_program(RMM_CBMC_PATH "cbmc" 9 DOC "Path to cbmc.") 10find_program(RMM_GOTO_CC_PATH "goto-cc" 11 DOC "Path to goto-cc.") 12find_program(RMM_CBMC_VIEWER_PATH "cbmc-viewer" 13 DOC "Path to cbmc-viewer.") 14find_program(RMM_GCC_PATH "gcc" 15 DOC "Path to gcc.") 16 17find_package(Python3 REQUIRED) 18find_program(CHECK_CBMC_SUMMARY_EXECUTABLE "compare_summary.py" 19 PATHS ${CMAKE_SOURCE_DIR} 20 PATH_SUFFIXES tools/cbmc 21 DOC "Path to compare_summary.py" 22 ) 23 24# 25# Configure and execute CBMC 26# 27if(NOT (EXISTS "${RMM_CBMC_PATH}")) 28 message(FATAL_ERROR "cbmc executable not found. (${RMM_CBMC_PATH})") 29endif() 30 31string(TOLOWER "${RMM_CBMC_CONFIGURATION}" CBMC_RESULT_FILE_SUFFIX) 32 33if(RMM_CBMC_VIEWER_OUTPUT) 34 set(CBMC_OUT_FILE_ENDING "xml") 35 set(CBMC_UI_OPTION "--xml-ui") 36else() 37 set(CBMC_OUT_FILE_ENDING "output") 38 set(CBMC_UI_OPTION "") 39endif() 40 41if(${RMM_CBMC_CONFIGURATION} STREQUAL "GCC") 42 set(COMPILED_FILE_PREFIX "gcc") 43 set(RMM_CBMC_COMPILER_PATH "${RMM_GCC_PATH}") 44 list(APPEND RMM_IMP_SRCS "${TESTBENCH_DIR}/../gcc/gcc_defs.c") 45else() 46 set(COMPILED_FILE_PREFIX "goto_cc") 47 set(RMM_CBMC_COMPILER_PATH "${RMM_GOTO_CC_PATH}") 48endif() 49 50set(RMM_TESTBENCH_RESULT_DIR "${BINARY_DIR}/cbmc_${CBMC_RESULT_FILE_SUFFIX}_results") 51set(SUMMARY_FILE "SUMMARY.${CBMC_RESULT_FILE_SUFFIX}") 52set(RMM_CBMC_SUMMARY_FIELD_WIDTH 38) 53 54# Configurations for the initial state. 55set(GRANULE_SHIFT "9") 56set(MAX_NUM_OF_GRANULE "4") 57set(MAX_NUM_OF_COH_GRANULE "1") 58set(MAX_NUM_OF_NCOH_GRANULE "4") 59math(EXPR HOST_DRAM_SIZE "(1 << ${GRANULE_SHIFT}) * ${MAX_NUM_OF_GRANULE}") 60set(HOST_DRAM_SIZE "${HOST_DRAM_SIZE}UL") 61math(EXPR HOST_NCOH_DEV_SIZE "(1 << ${GRANULE_SHIFT}) * ${MAX_NUM_OF_NCOH_GRANULE}") 62set(HOST_NCOH_DEV_SIZE "${HOST_NCOH_DEV_SIZE}UL") 63 64set(MAX_RTT_UNWIND "6") 65set(MAX_AUX_REC "2") 66set(MAX_ROOT_RTT "3") 67set(MAX_UNWIND_FLAGS "") 68 69# 70# Set up cbmc command line 71# 72set(cbmc_unwinds_list 73 "--unwindset;find_lock_granules.3:${MAX_ROOT_RTT}" 74 "--unwindset;find_lock_rd_granules.0:${MAX_RTT_UNWIND}" 75 "--unwindset;find_lock_rd_granules.1:${MAX_RTT_UNWIND}" 76 "--unwindset;free_rec_aux_granules.0:${MAX_AUX_REC}" 77 "--unwindset;free_sl_rtts.0:${MAX_RTT_UNWIND}" 78 "--unwindset;init_realm_descriptor_page.0:${MAX_ROOT_RTT}" 79 "--unwindset;init_realm_descriptor_page.1:${MAX_ROOT_RTT}" 80 "--unwindset;init_rec.0:${MAX_AUX_REC}" 81 "--unwindset;init_rtt_root_page.0:${MAX_ROOT_RTT}" 82 "--unwindset;init_walk_path.0:${MAX_RTT_UNWIND}" 83 "--unwindset;lock_order_invariable.0:21" 84 "--unwindset;lock_order_invariable.1:11" 85 "--unwindset;lock_order_invariable.2:" 86 "--unwindset;RealmIsLive.0:${MAX_ROOT_RTT}" 87 "--unwindset;RealmIsLive.2:${MAX_ROOT_RTT}" 88 "--unwindset;rtt_walk_lock_unlock.0:${MAX_RTT_UNWIND}" 89 "--unwindset;RttWalk.0:${MAX_RTT_UNWIND}" 90 "--unwindset;smc_realm_create.0:${MAX_RTT_UNWIND}" 91 "--unwindset;smc_rec_create.0:${MAX_AUX_REC}" 92 "--unwindset;total_root_rtt_refcount.0:${MAX_RTT_UNWIND}" 93) 94 95set(cbmc_defines_list 96 "-DCBMC" 97 "-DGRANULE_SHIFT=${GRANULE_SHIFT}" 98 "-DXLAT_GRANULARITY_SIZE_SHIFT=${GRANULE_SHIFT}" 99 "-DRMM_MAX_GRANULES=${MAX_NUM_OF_GRANULE}" 100 "-DRMM_MAX_COH_GRANULES=${MAX_NUM_OF_COH_GRANULE}" 101 "-DRMM_MAX_NCOH_GRANULES=${MAX_NUM_OF_NCOH_GRANULE}" 102 "-DMAX_CPUS=1" 103 "-DMAX_RTT_LEVEL=${MAX_RTT_UNWIND}" 104 "-DHOST_DRAM_SIZE=${HOST_DRAM_SIZE}" 105 "-DHOST_NCOH_DEV_SIZE=${HOST_NCOH_DEV_SIZE}" 106 "-DNAME=\"RMM\"" 107 "-DVERSION=\"CBMC\"" 108 "-DCOMMIT_INFO=\"CBMC\"" 109 "-DRMM_NUM_PAGES_PER_STACK=1" 110) 111 112# CBMC flags for memory safety analysis and undefined behaviour analysis. 113set(cbmc_analysis_flags_list 114 "--bounds-check" 115 "--pointer-check" 116 "--div-by-zero-check" 117 "--signed-overflow-check" 118 "--unsigned-overflow-check" 119 "--pointer-overflow-check" 120 "--conversion-check" 121 "--undefined-shift-check" 122 "--float-overflow-check" 123 "--nan-check" 124 "--enum-range-check" 125 "--pointer-primitive-check" 126 "--memory-leak-check") 127 128set(cbmc_flags_list 129 "--timestamp;wall" 130 "--verbosity;9" 131 # Optimisation flags: 132 "--drop-unused-functions" 133 "--reachability-slice" 134 ) 135 136if("${RMM_CBMC_CONFIGURATION}" STREQUAL "COVERAGE") 137 list(APPEND cbmc_flags_list 138 "--cover;cover" 139 "--no-assertions") 140elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "ASSERT") 141 list(APPEND cbmc_flags_list 142 "--unwinding-assertions" 143 "--trace" 144 "--trace-show-function-calls") 145elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "ANALYSIS") 146 list(APPEND cbmc_flags_list 147 "--unwinding-assertions" 148 "${cbmc_analysis_flags_list}") 149elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "GCC") 150 list(APPEND cbmc_compiler_options 151 "-Wall" 152 "-Werror" 153 "-Wno-unused-function" 154 "-Wno-main" # Do not warning on the non-standard signature of main 155 "-Wno-error=unused-variable" # Some of the testbenches contain unused variables 156 "-include;${TESTBENCH_DIR}/../gcc/gcc_defs.h") 157else() 158 message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'") 159endif() 160 161# Convert the space separated strings to a CMake list 162string(REPLACE " " ";" TESTBENCH_FILES "${TESTBENCH_FILES}") 163 164# 165# Create semi-colon separated list from white-space seperated ones. 166# 167separate_arguments(RMM_IMP_SRCS) 168separate_arguments(RMM_IMP_INCS) 169 170# 171# Execute CBMC on the testbench files 172# 173rmm_cbmc_write_summary_header(${RMM_CBMC_SUMMARY_FIELD_WIDTH} 174 ${RMM_TESTBENCH_RESULT_DIR} ${SUMMARY_FILE} ${RMM_CBMC_CONFIGURATION}) 175 176function(rmm_cbmc_gen_file_names 177 testbench_file_path 178 filename_prefix 179 out_file_ending 180 cmd_file_var_name 181 out_file_var_name 182 err_file_var_name) 183 get_filename_component(testbench_file_name "${testbench_file_path}" NAME) 184 get_filename_component(parent "${testbench_file_path}" DIRECTORY) 185 set("${cmd_file_var_name}" "${parent}/${filename_prefix}_${testbench_file_name}.cmd" PARENT_SCOPE) 186 set("${out_file_var_name}" "${parent}/${filename_prefix}_${testbench_file_name}.${out_file_ending}" PARENT_SCOPE) 187 set("${err_file_var_name}" "${parent}/${filename_prefix}_${testbench_file_name}.error" PARENT_SCOPE) 188endfunction() 189 190function(normalise_cmd cmd_str out_var_name) 191 # replace the ; with space 192 string (REPLACE ";" " " cmd_str "${cmd_str}") 193 set("${out_var_name}" "${cmd_str}" PARENT_SCOPE) 194endfunction() 195 196foreach(testbench_file ${TESTBENCH_FILES}) 197 198 string(REPLACE ${TESTBENCH_DIR}/ "" testbench_filename ${testbench_file}) 199 string(REGEX REPLACE "\\.[^\\.]*$" "" entry_point "${testbench_filename}") 200 201 set(RMM_GOTO_PROG_NAME "${RMM_TESTBENCH_RESULT_DIR}/rmm_${entry_point}.goto") 202 203 # Set the names of output files 204 string(REPLACE ${TESTBENCH_DIR} ${RMM_TESTBENCH_RESULT_DIR} OUT_FILE_NAME_PREFIX "${testbench_file}") 205 rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "cbmc" "${CBMC_OUT_FILE_ENDING}" 206 cbmc_cmd_file cbmc_output_file cbmc_error_file) 207 rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "cbmc_prop" "xml" 208 cbmc_prop_cmd_file cbmc_prop_output_file cbmc_prop_error_file) 209 rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "${COMPILED_FILE_PREFIX}" "output" 210 compile_cmd_file compile_output_file compile_error_file) 211 rmm_cbmc_gen_file_names(${OUT_FILE_NAME_PREFIX} "cbmc_viewer" "output" 212 cbmc_viewer_cmd_file cbmc_viewer_output_file cbmc_viewer_error_file) 213 set(CBMC_VIEWER_REPORT_DIR "${RMM_TESTBENCH_RESULT_DIR}/report_${entry_point}") 214 215 if(${RMM_CBMC_CONFIGURATION} STREQUAL "GCC") 216 set(CBMC_ENTRY_POINT "-D${entry_point}=main") 217 else() 218 set(CBMC_ENTRY_POINT "--function;${entry_point}") 219 endif() 220 221 set(compile_cmd 222 ${RMM_CBMC_COMPILER_PATH} 223 ${cbmc_compiler_options} 224 ${cbmc_defines_list} 225 ${CBMC_ENTRY_POINT} 226 "-o;${RMM_GOTO_PROG_NAME}" 227 ${RMM_IMP_INCS} 228 ${RMM_IMP_SRCS} 229 ${testbench_file} 230 ) 231 232 set(cbmc_cmd 233 ${RMM_CBMC_PATH} 234 ${CBMC_UI_OPTION} 235 ${cbmc_flags_list} 236 ${cbmc_unwinds_list} 237 ${RMM_GOTO_PROG_NAME}) 238 239 set(cbmc_prop_cmd 240 ${RMM_CBMC_PATH} 241 ${cbmc_flags_list} 242 "--xml-ui" 243 "--show-properties" 244 ${RMM_GOTO_PROG_NAME}) 245 246 set(cbmc_viewer_cmd 247 "${RMM_CBMC_VIEWER_PATH}" 248 "--goto;${RMM_GOTO_PROG_NAME}" 249 "--result;${cbmc_output_file}" 250 "--property;${cbmc_prop_output_file}" 251 "--srcdir;${CMAKE_SOURCE_DIR}" 252 "--reportdir;${CBMC_VIEWER_REPORT_DIR}") 253 254 # remove the absolute path making it relative (shorten the command line) 255 string (REPLACE "${SOURCE_DIR}/" "" compile_cmd "${compile_cmd}") 256 257 normalise_cmd("${compile_cmd}" COMPILE_CMD_STR) 258 normalise_cmd("${cbmc_cmd}" CBMC_CMD_STR) 259 260 file(WRITE ${compile_cmd_file} "${COMPILE_CMD_STR}") 261 file(WRITE ${cbmc_cmd_file} "${CBMC_CMD_STR}") 262 263 execute_process(COMMAND ${CMAKE_COMMAND} -E echo_append "CBMC: ${testbench_file}... ") 264 execute_process( 265 COMMAND ${compile_cmd} 266 RESULT_VARIABLE res_var 267 OUTPUT_FILE ${compile_output_file} 268 ERROR_FILE ${compile_error_file}) 269 if (NOT ${res_var} EQUAL "0") 270 message(FATAL_ERROR "Compiling testbench with ${RMM_CBMC_COMPILER_PATH} failed. For details see: ${compile_error_file}") 271 endif() 272 273 # Only run CBMC if not using compiler-only mode: 274 if(NOT ${RMM_CBMC_CONFIGURATION} STREQUAL "GCC") 275 execute_process( 276 COMMAND ${cbmc_cmd} 277 RESULT_VARIABLE res_var 278 OUTPUT_FILE ${cbmc_output_file} 279 ERROR_FILE ${cbmc_error_file}) 280 281 if(RMM_CBMC_VIEWER_OUTPUT) 282 normalise_cmd("${cbmc_prop_cmd}" CBMC_PROP_CMD_STR) 283 file(WRITE ${cbmc_prop_cmd_file} "${CBMC_PROP_CMD_STR}") 284 execute_process( 285 COMMAND ${cbmc_prop_cmd} 286 RESULT_VARIABLE res_var 287 OUTPUT_FILE ${cbmc_prop_output_file} 288 ERROR_FILE ${cbmc_prop_error_file}) 289 290 normalise_cmd("${cbmc_viewer_cmd}" CBMC_VIEWER_CMD_STR) 291 file(WRITE ${cbmc_viewer_cmd_file} "${CBMC_VIEWER_CMD_STR}") 292 execute_process( 293 COMMAND ${cbmc_viewer_cmd} 294 RESULT_VARIABLE res_var 295 OUTPUT_FILE ${cbmc_viewer_output_file} 296 ERROR_FILE ${cbmc_viewer_error_file}) 297 if (NOT ${res_var} EQUAL "0") 298 message(FATAL_ERROR "Failed to run cbmc-viewer. For details see: ${cbmc_viewer_error_file}") 299 endif() 300 endif() 301 302 rmm_cbmc_append_summary("${testbench_filename}" "${cbmc_output_file}" 303 "${CBMC_RESULT_FILE_SUFFIX}-${CBMC_OUT_FILE_ENDING}" 304 ${RMM_CBMC_SUMMARY_FIELD_WIDTH} ${RMM_TESTBENCH_RESULT_DIR} ${SUMMARY_FILE}) 305 306 endif() 307 308 execute_process(COMMAND ${CMAKE_COMMAND} -E echo "DONE") 309 310endforeach() 311message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}") 312 313# Only run CBMC if not using compiler-only mode: 314if(NOT ${RMM_CBMC_CONFIGURATION} STREQUAL "GCC") 315 list(TRANSFORM TESTBENCH_FILES REPLACE "${TESTBENCH_DIR}/" "" OUTPUT_VARIABLE TESTBENCH_FILENAMES) 316 execute_process( 317 WORKING_DIRECTORY ${CMAKE_SOURCE_DIR} 318 COMMAND ${CHECK_CBMC_SUMMARY_EXECUTABLE} 319 ${CMAKE_SOURCE_DIR}/tools/cbmc/testbenches_results/BASELINE.${CBMC_RESULT_FILE_SUFFIX} 320 --testbench-files "${TESTBENCH_FILENAMES}" 321 ${RMM_TESTBENCH_RESULT_DIR}/${SUMMARY_FILE} 322 OUTPUT_VARIABLE CHECK_SUMMARY_OUTPUT 323 ERROR_VARIABLE CHECK_SUMMARY_ERROR 324 RESULT_VARIABLE CHECK_SUMMARY_RC 325 OUTPUT_STRIP_TRAILING_WHITESPACE 326 ) 327 328 if (NOT ${CHECK_SUMMARY_RC} EQUAL "0") 329 message(WARNING 330 "cbmc-${CBMC_RESULT_FILE_SUFFIX}: FAILED\n${CHECK_SUMMARY_ERROR}") 331 else() 332 message(STATUS "cbmc-${CBMC_RESULT_FILE_SUFFIX}: PASSED") 333 endif() 334endif() 335