feat(cbmc): add initial support for CBMC
This commit adds initial, partial support for analysing RMM source code
with CBMC (https://www.cprover.org/cbmc/)
Signed-off-by: Shale Xiong <shale.xiong@arm.com>
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
Change-Id: I1c66838328782cb2db630769830809c5b0847a81
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9e6e7ee..0ba8879 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -216,3 +216,4 @@
-DBUILD_DIR=${CMAKE_BINARY_DIR}
-P ${CMAKE_SOURCE_DIR}/tools/clang-tidy/clang-tidy.cmake
)
+
diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst
index 985fc6b..58edeb7 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -234,6 +234,16 @@
`build/Debug/coverage` within the build directory. The HTML generation can be
disabled by setting `RMM_HTML_COV_REPORT=OFF`.
+17. Run CBMC analysis:
+
+Run ``COVERAGE``, ``ANALYSIS`` and ``ASSERT`` targets for CBMC. The results
+are generated in ``${RMM_BUILD_DIR}/tools/cbmc/cbmc_coverage_results``.
+
+.. code-block:: bash
+
+ cmake -DRMM_CONFIG=host_defcfg -DHOST_VARIANT=host_cbmc -S ${RMM_SOURCE_DIR} -B ${RMM_BUILD_DIR}
+ cmake --build ${RMM_BUILD_DIR} -- cbmc-coverage cbmc-analysis cbmc-assert
+
.. _build_options_table:
###################
diff --git a/docs/getting_started/getting-started.rst b/docs/getting_started/getting-started.rst
index 88747c9..bbf744e 100644
--- a/docs/getting_started/getting-started.rst
+++ b/docs/getting_started/getting-started.rst
@@ -50,6 +50,7 @@
"Graphviz dot",">v2.38.0","Documentation"
"docutils",">v2.38.0","Documentation"
"gcovr",">=v4.2","Tools(Coverage analysis)"
+ "CBMC",">=5.84.0","Tools(CBMC analysis)"
.. _getting_started_toolchain:
@@ -225,6 +226,19 @@
sudo mkdir /usr/local/share/Cppcheck/misra
sudo cp -a <path to the misra rules file>/<file name> /usr/local/share/Cppcheck/misra/misra.rules
+############
+Install CBMC
+############
+
+.. note::
+
+ The installation of CBMC is an optional step. This is required only
+ if running source code analysis with CBMC.
+
+Follow the public documentation to install CBMC either from the official
+website https://www.cprover.org/cbmc/ or from the official github
+https://github.com/diffblue/cbmc
+
###########################
Performing an Initial Build
###########################
diff --git a/lib/mbedtls/CMakeLists.txt b/lib/mbedtls/CMakeLists.txt
index 7baf798..8c94c4a 100644
--- a/lib/mbedtls/CMakeLists.txt
+++ b/lib/mbedtls/CMakeLists.txt
@@ -6,6 +6,12 @@
find_package(Python3 COMPONENTS Interpreter REQUIRED)
find_package(Git)
+# The Mbed TLS library is not included in the CBMC analysis
+if(RMM_CBMC_STATIC_ANALYSIS)
+ add_library(rmm-mbedtls INTERFACE)
+ return()
+endif()
+
add_library(rmm-mbedtls INTERFACE)
set(MBEDTLS_SRC_DIR "${RMM_SOURCE_DIR}/ext/mbedtls")
diff --git a/lib/qcbor/CMakeLists.txt b/lib/qcbor/CMakeLists.txt
index dca9b3f..b0a4b6e 100644
--- a/lib/qcbor/CMakeLists.txt
+++ b/lib/qcbor/CMakeLists.txt
@@ -3,6 +3,12 @@
# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
#
+# The QCBOR library is not included in the CBMC analysis
+if(RMM_CBMC_STATIC_ANALYSIS)
+ add_library(qcbor INTERFACE)
+ return()
+endif()
+
#
# Set qcbor options to not use FPU.
#
diff --git a/lib/realm/include/granule_types.h b/lib/realm/include/granule_types.h
index bc15a7f..6aaac4b 100644
--- a/lib/realm/include/granule_types.h
+++ b/lib/realm/include/granule_types.h
@@ -74,11 +74,6 @@
*/
GRANULE_STATE_NS,
/*
- * TODO: remove the next line when spec aligment is done
- * currently this has been renamed in alp03 and is needed for CBMC testbench
- */
- GRANULE_STATE_UNDELEGATED = GRANULE_STATE_NS,
- /*
* Delegated Granule (external)
*
* Granule content is protected by granule::lock.
diff --git a/lib/t_cose/CMakeLists.txt b/lib/t_cose/CMakeLists.txt
index 88aa267..ce8d9c7 100644
--- a/lib/t_cose/CMakeLists.txt
+++ b/lib/t_cose/CMakeLists.txt
@@ -3,6 +3,12 @@
# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
#
+# The t_cose library is not included in the CBMC analysis
+if(RMM_CBMC_STATIC_ANALYSIS)
+ add_library(t_cose INTERFACE)
+ return()
+endif()
+
add_library(t_cose)
set(T_COSE_SOURCE_DIR "${RMM_SOURCE_DIR}/ext/t_cose")
diff --git a/plat/host/host_cbmc/CMakeLists.txt b/plat/host/host_cbmc/CMakeLists.txt
index 7562bb0..5f45c17 100644
--- a/plat/host/host_cbmc/CMakeLists.txt
+++ b/plat/host/host_cbmc/CMakeLists.txt
@@ -5,6 +5,11 @@
add_library(rmm-plat-host_cbmc)
+arm_config_option(
+ NAME RMM_CBMC_STATIC_ANALYSIS
+ HELP "Enable CBMC static analysis."
+ DEFAULT TRUE FORCE)
+
target_link_libraries(rmm-plat-host_cbmc
PRIVATE rmm-lib
PUBLIC rmm-host-common)
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
index 8021dbb..9811bf3 100644
--- a/tools/CMakeLists.txt
+++ b/tools/CMakeLists.txt
@@ -8,3 +8,4 @@
HELP "Enable static analysis checkers.")
add_subdirectory("cppcheck")
+add_subdirectory("cbmc")
diff --git a/tools/cbmc/CMakeLists.txt b/tools/cbmc/CMakeLists.txt
new file mode 100644
index 0000000..69e6a8f
--- /dev/null
+++ b/tools/cbmc/CMakeLists.txt
@@ -0,0 +1,92 @@
+#
+# SPDX-License-Identifier: BSD-3-Clause
+# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+#
+include("SourceCollectHelpers.cmake")
+
+if("${RMM_CBMC_STATIC_ANALYSIS}")
+
+ if (NOT (${HOST_VARIANT} STREQUAL "host_cbmc"))
+ message(FATAL_ERROR "cbmc analysis requires host variant `host_cbmc`. (Add `-DHOST_VARIANT=host_cbmc`)")
+ endif()
+
+ #
+ # Create the list of source files and include directories that are to be
+ # included in the analysis.
+ #
+
+ set(rmm_implementation_srcs)
+ set(rmm_implementation_includes)
+
+ add_source_and_include_recursively(rmm-runtime)
+
+ list(APPEND rmm_implementation_srcs
+ "${CMAKE_CURRENT_SOURCE_DIR}/src/tb.c"
+ "${CMAKE_CURRENT_SOURCE_DIR}/src/tb_common.c"
+ "${CMAKE_CURRENT_SOURCE_DIR}/src/tb_granules.c")
+
+ list(APPEND rmm_implementation_includes
+ "-I${CMAKE_CURRENT_SOURCE_DIR}/include"
+ "-I${CMAKE_CURRENT_SOURCE_DIR}/testbenches")
+
+ list(REMOVE_DUPLICATES rmm_implementation_includes)
+ list(REMOVE_DUPLICATES rmm_implementation_srcs)
+
+ # Filter source files that are not analysed by CBMC
+ set(src_filters
+ "lib/allocator/src"
+ "lib/arch/src"
+ "lib/attestation/src"
+ "lib/measurement/src"
+ "lib/rmm_el3_ifc/src"
+ "lib/timers/src"
+ "lib/xlat/src"
+ "plat/common/src"
+ "runtime/rsi"
+ "runtime/core/run.c"
+ )
+
+ foreach(filter ${src_filters})
+ list(FILTER rmm_implementation_srcs EXCLUDE REGEX "${filter}")
+ endforeach()
+
+ #
+ # Rules for running cbmc analysis
+ #
+ add_custom_target(cbmc-coverage
+ WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}"
+ COMMAND ${CMAKE_COMMAND}
+ -DRMM_CBMC_CONFIGURATION=COVERAGE
+ -DSOURCE_DIR=${CMAKE_SOURCE_DIR}
+ -DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
+ -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+ -DRMM_IMP_SRCS="${rmm_implementation_srcs}"
+ -DRMM_IMP_INCS="${rmm_implementation_includes}"
+ -P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
+ )
+
+ add_custom_target(cbmc-analysis
+ WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}"
+ COMMAND ${CMAKE_COMMAND}
+ -DRMM_CBMC_CONFIGURATION=ANALYSIS
+ -DSOURCE_DIR=${CMAKE_SOURCE_DIR}
+ -DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
+ -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+ -DRMM_IMP_SRCS="${rmm_implementation_srcs}"
+ -DRMM_IMP_INCS="${rmm_implementation_includes}"
+ -P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
+ )
+
+ add_custom_target(cbmc-assert
+ WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}"
+ COMMAND ${CMAKE_COMMAND}
+ -DRMM_CBMC_CONFIGURATION=ASSERT
+ -DSOURCE_DIR=${CMAKE_SOURCE_DIR}
+ -DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
+ -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+ -DRMM_IMP_SRCS="${rmm_implementation_srcs}"
+ -DRMM_IMP_INCS="${rmm_implementation_includes}"
+ -P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
+ )
+
+endif() # RMM_CBMC_STATIC_ANALYSIS
\ No newline at end of file
diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake
new file mode 100644
index 0000000..251f541
--- /dev/null
+++ b/tools/cbmc/CheckCBMC.cmake
@@ -0,0 +1,195 @@
+#
+# SPDX-License-Identifier: BSD-3-Clause
+# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+#
+
+include(FetchContent)
+include("${SOURCE_DIR}/tools/cbmc/SummaryHelpers.cmake")
+find_program(RMM_CBMC_PATH "cbmc"
+ DOC "Path to cbmc.")
+
+#
+# Configure and execute CBMC
+#
+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")
+else()
+ message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'")
+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)
+
+# Configurations for the initial state.
+set(GRANULE_SHIFT "7")
+set(MAX_NUM_OF_GRANULE "8")
+set(HOST_MEM_SIZE "1024UL")
+
+set(MAX_RTT_UNWIND "6")
+set(MAX_AUX_REC "2")
+set(MAX_ROOT_RTT "3")
+set(MAX_UNWIND_FLAGS "")
+
+#
+# Set up cbmc command line
+#
+set(cbmc_unwinds_list
+ "--unwindset;find_lock_rd_granules.0:${MAX_RTT_UNWIND}"
+ "--unwindset;find_lock_rd_granules.1:${MAX_RTT_UNWIND}"
+ "--unwindset;smc_realm_create.0:${MAX_RTT_UNWIND}"
+ "--unwindset;total_root_rtt_refcount.0:${MAX_RTT_UNWIND}"
+ "--unwindset;free_sl_rtts.0:${MAX_RTT_UNWIND}"
+ "--unwindset;rtt_walk_lock_unlock.0:${MAX_RTT_UNWIND}"
+ "--unwindset;RttWalk.0:${MAX_RTT_UNWIND}"
+ "--unwindset;init_walk_path.0:${MAX_RTT_UNWIND}"
+ "--unwindset;smc_rec_create.0:${MAX_AUX_REC}"
+ "--unwindset;free_rec_aux_granules.0:${MAX_AUX_REC}"
+ "--unwindset;find_lock_granules.3:${MAX_ROOT_RTT}"
+ "--unwindset;RealmIsLive.0:${MAX_ROOT_RTT}"
+ "--unwindset;init_rtt_root_page.0:${MAX_ROOT_RTT}"
+ "--unwindset;init_rec.0:${MAX_AUX_REC}"
+ "--unwindset;RealmIsLive.2:${MAX_ROOT_RTT}"
+ "--unwindset;init_realm_descriptor_page.0:${MAX_ROOT_RTT}"
+ "--unwindset;init_rec.0:${MAX_AUX_REC}"
+ "--unwindset;lock_order_invariable.0:21"
+ "--unwindset;lock_order_invariable.1:11"
+ "--unwindset;lock_order_invariable.2:"
+)
+
+set(cbmc_defines_list
+ "-DCBMC"
+ "-DDISABLE_COMPILER_ASSERT"
+ "-DDISABLE_SET_MEMBER"
+ "-DGRANULE_SHIFT=${GRANULE_SHIFT}"
+ "-DXLAT_GRANULARITY_SIZE_SHIFT=${GRANULE_SHIFT}"
+ "-DRMM_MAX_GRANULES=${MAX_NUM_OF_GRANULE}"
+ "-DMAX_CPUS=1"
+ "-DMAX_RTT_LEVEL=${MAX_RTT_UNWIND}"
+ "-DHOST_MEM_SIZE=${HOST_MEM_SIZE}"
+ "-DNAME=\"RMM\""
+ "-DVERSION=\"CBMC\""
+ "-DCOMMIT_INFO=\"CBMC\""
+)
+
+# CBMC flags for memory safety analysis and undefined behaviour analysis.
+set(cbmc_analysis_flags_list
+ "--bounds-check"
+ "--pointer-check"
+ "--div-by-zero-check"
+ "--signed-overflow-check"
+ "--unsigned-overflow-check"
+ "--pointer-overflow-check"
+ "--conversion-check"
+ "--undefined-shift-check"
+ "--float-overflow-check"
+ "--nan-check"
+ "--enum-range-check"
+ "--pointer-primitive-check"
+ "--memory-leak-check")
+
+set(cbmc_flags_list
+ "--c11"
+ "--timestamp;wall"
+ "--verbosity;9"
+ # Optimisation flags:
+ "--drop-unused-functions"
+ "--reachability-slice"
+ )
+
+if("${RMM_CBMC_CONFIGURATION}" STREQUAL "COVERAGE")
+ list(APPEND cbmc_flags_list
+ "--cover;cover"
+ "--no-assertions")
+elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "ASSERT")
+ list(APPEND cbmc_flags_list
+ "--unwinding-assertions"
+ "--trace"
+ "--trace-show-function-calls")
+elseif("${RMM_CBMC_CONFIGURATION}" STREQUAL "ANALYSIS")
+ list(APPEND cbmc_flags_list
+ "--unwinding-assertions"
+ "${cbmc_analysis_flags_list}")
+else()
+ message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'")
+endif()
+
+file(GLOB_RECURSE TESTBENCH_FILES "${TESTBENCH_DIR}/*.c")
+
+#
+# Create semi-colon separated list from white-space seperated ones.
+#
+separate_arguments(RMM_IMP_SRCS)
+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})
+
+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}
+ "--function;${entry_point}"
+ ${RMM_IMP_INCS}
+ ${cbmc_unwinds_list}
+ ${cbmc_defines_list}
+ ${RMM_IMP_SRCS}
+ ${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}")
+
+ execute_process(COMMAND ${CMAKE_COMMAND} -E echo_append "CBMC: ${testbench_file}... ")
+ execute_process(
+ COMMAND ${cmd}
+ RESULT_VARIABLE res_var
+ OUTPUT_FILE ${output_file}
+ ERROR_FILE ${error_file}
+ )
+
+ 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})
+
+endforeach()
+message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}")
diff --git a/tools/cbmc/SourceCollectHelpers.cmake b/tools/cbmc/SourceCollectHelpers.cmake
new file mode 100644
index 0000000..3f89746
--- /dev/null
+++ b/tools/cbmc/SourceCollectHelpers.cmake
@@ -0,0 +1,124 @@
+#
+# SPDX-License-Identifier: BSD-3-Clause
+# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+#
+
+#
+# Helper functions for collecting all the source files and include paths that
+# are used in the RMM build
+#
+
+function(is_valid_target_name target_name output_variable)
+ string(FIND ${target_name} "NOTFOUND" notfound_pos)
+ string(FIND ${target_name} "::@" link_addr_pos)
+ string(FIND ${target_name} "$<$<" gen_expr_pos)
+ if((NOT ${notfound_pos} EQUAL "-1") OR
+ (NOT ${link_addr_pos} EQUAL "-1") OR
+ (NOT ${gen_expr_pos} EQUAL "-1"))
+ set(${output_variable} FALSE PARENT_SCOPE)
+ else()
+ set(${output_variable} TRUE PARENT_SCOPE)
+ endif()
+endfunction()
+
+function(normalise_property_value target_name output_variable)
+ foreach(value_prefix "INSTALL_INTERFACE" "BUILD_INTERFACE" "LINK_ONLY")
+ string(REGEX REPLACE "^.*${value_prefix}:([^>]+)>$" "\\1" target_name ${target_name})
+ endforeach()
+ set(${output_variable} ${target_name} PARENT_SCOPE)
+endfunction()
+
+function(collect_targets_recursively collected_targets new_target output_variable)
+ normalise_property_value("${new_target}" new_target)
+
+ if ("${new_target}" IN_LIST collected_targets)
+ set("${output_variable}" "${collected_targets}" PARENT_SCOPE)
+ return()
+ endif()
+
+ set(extended_target_list "${collected_targets}")
+ list(APPEND extended_target_list "${new_target}")
+
+ foreach(link_property "INTERFACE_LINK_LIBRARIES" "LINK_LIBRARIES")
+ # workaround for cmake older than 3.19:
+ # INTERFACE_LIBRARY targets may only have whitelisted properties. This is typically
+ # property names starting with 'INTERFACE_'
+ get_target_property(target_type ${new_target} TYPE)
+ if(${target_type} STREQUAL "INTERFACE_LIBRARY")
+ string(FIND "${link_property}" "INTERFACE_" interface_pos)
+ if (NOT interface_pos EQUAL 0)
+ continue()
+ endif()
+ endif()
+
+ get_target_property(target_interface "${new_target}" "${link_property}")
+ if(NOT "${target_interface}" STREQUAL "target_interface-NOTFOUND")
+ foreach(target_lib ${target_interface})
+ is_valid_target_name(${target_lib} valid_target_name)
+ if (valid_target_name)
+ collect_targets_recursively("${extended_target_list}" "${target_lib}" extended_target_list)
+ endif()
+ endforeach()
+ endif()
+ endforeach()
+
+ set("${output_variable}" "${extended_target_list}" PARENT_SCOPE)
+endfunction()
+
+function(add_include_from_target target_name)
+ foreach(include_property "INTERFACE_INCLUDE_DIRECTORIES" "INCLUDE_DIRECTORIES")
+ # workaround for cmake older than 3.19:
+ # INTERFACE_LIBRARY targets may only have whitelisted properties. This is typically
+ # property names starting with 'INTERFACE_'
+ get_target_property(target_type ${target_name} TYPE)
+ if(${target_type} STREQUAL "INTERFACE_LIBRARY")
+ string(FIND "${include_property}" "INTERFACE_" interface_pos)
+ if (NOT interface_pos EQUAL 0)
+ continue()
+ endif()
+ endif()
+
+ get_target_property(target_includes_dir ${target_name} ${include_property})
+ if(NOT "${target_includes_dir}" STREQUAL "target_includes_dir-NOTFOUND")
+ foreach(target_includes_dir ${target_includes_dir})
+ normalise_property_value(${target_includes_dir} target_includes_dir)
+ list(APPEND rmm_implementation_includes "-I${target_includes_dir}")
+ endforeach()
+ set (rmm_implementation_includes ${rmm_implementation_includes} PARENT_SCOPE)
+ endif()
+ endforeach()
+endfunction()
+
+function(add_source_and_include_from_target target_name)
+ add_include_from_target(${target_name} ${level})
+ set (rmm_implementation_includes ${rmm_implementation_includes} PARENT_SCOPE)
+
+ # workaround for cmake older than 3.19:
+ # INTERFACE_LIBRARY targets may only have whitelisted properties. This is typically
+ # property names starting with 'INTERFACE_'. So SOURCES.* is not allowed.
+ get_target_property(target_type ${target_name} TYPE)
+ if(${target_type} STREQUAL "INTERFACE_LIBRARY")
+ return()
+ endif()
+
+ get_target_property(target_srcs ${target_name} SOURCES)
+ get_target_property(target_srcs_dir ${target_name} SOURCE_DIR)
+ if((NOT "${target_srcs}" STREQUAL "target_srcs-NOTFOUND") AND
+ (NOT "${target_srcs_dir}" STREQUAL "target_srcs_dir-NOTFOUND"))
+ foreach(target_src ${target_srcs})
+ list(APPEND rmm_implementation_srcs "${target_srcs_dir}/${target_src}")
+ endforeach()
+ set (rmm_implementation_srcs ${rmm_implementation_srcs} PARENT_SCOPE)
+ endif()
+endfunction()
+
+function(add_source_and_include_recursively target_name)
+ collect_targets_recursively("" "${target_name}" rmm_target_list)
+
+ foreach(target_lib ${rmm_target_list})
+ add_source_and_include_from_target("${target_lib}")
+ endforeach()
+
+ set (rmm_implementation_srcs ${rmm_implementation_srcs} PARENT_SCOPE)
+ set (rmm_implementation_includes ${rmm_implementation_includes} PARENT_SCOPE)
+endfunction()
diff --git a/tools/cbmc/SummaryHelpers.cmake b/tools/cbmc/SummaryHelpers.cmake
new file mode 100644
index 0000000..ca53361
--- /dev/null
+++ b/tools/cbmc/SummaryHelpers.cmake
@@ -0,0 +1,67 @@
+#
+# SPDX-License-Identifier: BSD-3-Clause
+# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+#
+
+#
+# Helper functions for formatting the summary file
+#
+
+function(rmm_cbmc_align_to_middle field_width padding_character text)
+ set (pad_pool "")
+ foreach(i RANGE ${field_width})
+ string(APPEND pad_pool ${padding_character})
+ endforeach()
+ string(LENGTH ${text} text_len)
+ math(EXPR leading_space "(${field_width} - ${text_len}) / 2")
+ math(EXPR trailing_space "${field_width} - ${text_len} - ${leading_space}")
+ string (SUBSTRING ${pad_pool} 0 ${leading_space} leading_spaces)
+ string (SUBSTRING ${pad_pool} 0 ${trailing_space} trailing_spaces)
+
+ set(aligned_text "")
+ string (APPEND aligned_text "${leading_spaces}" "${text}" "${trailing_spaces}")
+ set(aligned_text "${aligned_text}" PARENT_SCOPE)
+endfunction()
+
+function(rmm_cbmc_append_separator summary_width result_dir file)
+ rmm_cbmc_align_to_middle(${summary_width} "-" "-")
+ set(separator_line "")
+ string(APPEND separator_line "+" "${aligned_text}" "+" "${aligned_text}" "+\n")
+ file(APPEND ${result_dir}/${file} ${separator_line})
+endfunction()
+
+function(rmm_cbmc_write_summary_header summary_width result_dir file summary_header)
+ file(MAKE_DIRECTORY ${result_dir})
+ file(WRITE ${result_dir}/${file} "")
+ rmm_cbmc_append_separator(${summary_width} ${result_dir} ${file})
+ rmm_cbmc_align_to_middle(${summary_width} " " "FILENAME")
+ set(field1 "${aligned_text}")
+ rmm_cbmc_align_to_middle(${summary_width} " " "${summary_header}")
+ set(field2 "${aligned_text}")
+ set(header "")
+ string(APPEND header "|" "${field1}" "|" "${field2}" "|\n")
+ file(APPEND ${result_dir}/${file} ${header})
+ 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)
+ 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)
+
+ if("${testbench_result}" STREQUAL "")
+ rmm_cbmc_align_to_middle(${summary_width} " " "N/A")
+ set(testbench_result "${aligned_text}")
+ endif()
+
+ string(REPLACE "\n" "" testbench_result "${testbench_result}")
+ string(REGEX REPLACE "[^\\*]*\\*\\*[\\s]*" "" testbench_result "${testbench_result}")
+
+ rmm_cbmc_align_to_middle(${summary_width} " " ${testbench_result})
+ set(testbench_result "${aligned_text}")
+
+ string(APPEND summary_data "|${testbench_filename}|${testbench_result}|\n")
+ file(APPEND ${result_dir}/${file} ${summary_data})
+ rmm_cbmc_append_separator(${summary_width} ${result_dir} ${file})
+endfunction()
diff --git a/tools/cbmc/include/tb.h b/tools/cbmc/include/tb.h
new file mode 100644
index 0000000..0c491f2
--- /dev/null
+++ b/tools/cbmc/include/tb.h
@@ -0,0 +1,25 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_H__
+#define TB_H__
+
+#include "smc-rmi.h"
+#include "tb_common.h"
+#include "tb_granules.h"
+
+/* Initialize the global state based on the commands */
+void __init_global_state(unsigned long cmd);
+
+/* Sanity check on the implementation of CBMC */
+void global_sanity_check(void);
+
+/* Call the function based on the X0 value in `config` */
+void tb_handle_smc(struct tb_regs *config);
+
+/* Assertion used to check consistency of the testbench */
+void __tb_expect_fail(void);
+
+#endif /* !TB_H */
diff --git a/tools/cbmc/include/tb_common.h b/tools/cbmc/include/tb_common.h
new file mode 100644
index 0000000..bc79922
--- /dev/null
+++ b/tools/cbmc/include/tb_common.h
@@ -0,0 +1,134 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_COMMON_H
+#define TB_COMMON_H
+
+#include "host_defs.h"
+#include "stdbool.h"
+#include "stdint.h"
+#include "string.h"
+
+/* Forces the model-checker to only consider executions where `p` holds. */
+#define __ASSUME(p) \
+ do { \
+ __CPROVER_assume((p)); \
+ } while (false)
+
+#define ASSUME(p) __ASSUME(p)
+
+/*
+ * Challenges the model checker to show that `p` holds in the current execution
+ * (in which case this behaves like a no-op), or otherwise come up with a
+ * counterexample trace of states and assignments to variables which refutes
+ * `p`, associating the name `name` to this trace.
+ */
+#define __ASSERT(p, name) \
+ do { \
+ __CPROVER_assert((p), (name)); \
+ } while (false)
+
+#define ASSERT(p, name) __ASSERT((p), (name))
+
+/*
+ * A marker for reachability: running CBMC with `--cover cover` will check that
+ * all instances of `COVER` are reachable from the program entry point.
+ */
+#define __COVER(p) \
+ do { \
+ __CPROVER_cover(p); \
+ } while (false)
+
+#define COVER(p) __COVER(p)
+
+#define REACHABLE COVER(true)
+
+/*
+ * An assertion that always fails, useful for checking code-paths are never
+ * reachable.
+ */
+#define UNREACHABLE ASSERT(false, "UNREACHABLE")
+
+/*
+ * Declare nondet_* functions for primitive types.
+ * Ref: CBMC automatically returns nondet values, or symbolic values, matching
+ * the return types. However, enum is treated as integer hence the value might
+ * be out of range.
+ */
+bool nondet_bool(void);
+unsigned char nondet_unsigned_char(void);
+unsigned short nondet_unsigned_short(void);
+unsigned int nondet_unsigned_int(void);
+unsigned long nondet_unsigned_long(void);
+char nondet_char(void);
+short nondet_short(void);
+int nondet_int(void);
+long nondet_long(void);
+uint32_t nondet_uint32_t(void);
+uint64_t nondet_uint64_t(void);
+int32_t nondet_int32_t(void);
+int64_t nondet_int64_t(void);
+size_t nondet_size_t(void);
+
+struct tb_regs {
+ uint64_t X0;
+ uint64_t X1;
+ uint64_t X2;
+ uint64_t X3;
+ uint64_t X4;
+ uint64_t X5;
+ uint64_t X6;
+};
+
+struct tb_regs __tb_arb_regs(void);
+
+bool ResultEqual_2(unsigned int code, unsigned int expected);
+bool ResultEqual_3(unsigned int code, unsigned int expected, unsigned int walk_level);
+uint64_t Zeros(void);
+
+/* Some autogen contains this function. */
+bool __tb_arb_bool(void);
+
+struct tb_lock_status {
+ uint64_t something;
+};
+void __tb_lock_invariant(struct tb_lock_status *lock_status);
+
+struct tb_lock_status __tb_lock_status(void);
+
+/*
+ * Functions that manipulates internal states,
+ * including PA, granule metadata and granule buffer, or content.
+ */
+bool valid_pa(uint64_t addr);
+bool valid_granule_metadata_ptr(struct granule *p);
+struct granule *pa_to_granule_metadata_ptr(uint64_t addr);
+uint64_t granule_metadata_ptr_to_pa(struct granule *g_ptr);
+void *granule_metadata_ptr_to_buffer_ptr(struct granule *g_ptr);
+size_t granule_metadata_ptr_to_index(struct granule *g_ptr);
+void *pa_to_granule_buffer_ptr(uint64_t addr);
+/* TODO change the function name */
+void init_pa_page(const void *content, size_t size);
+
+
+/*
+ * Return an unused continuous index to both `granules` and `granules_buffer`
+ * arrays.
+ */
+size_t next_index(void);
+bool unused_index(size_t index);
+/*
+ * Initialise granule at an non-deterministic granule. It updates both granule
+ * metadata array and physical page array.
+ */
+struct granule *inject_granule_at(const struct granule *granule_metadata,
+ const void *src_page,
+ size_t src_size,
+ size_t idx);
+struct granule *inject_granule(const struct granule *granule_metadata,
+ const void *src_page,
+ size_t src_size);
+
+#endif /* !TB_COMMON_H */
diff --git a/tools/cbmc/include/tb_granules.h b/tools/cbmc/include/tb_granules.h
new file mode 100644
index 0000000..64ce47f
--- /dev/null
+++ b/tools/cbmc/include/tb_granules.h
@@ -0,0 +1,63 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_GRANULES_H
+#define TB_GRANULES_H
+
+#include "buffer.h"
+#include "granule.h"
+#include "granule_types.h"
+#include "sizes.h"
+#include "host_defs.h"
+#include "host_utils.h"
+#include "platform_api.h"
+
+/*
+ * The granule states and gpt state
+ */
+#define UNDELEGATED GRANULE_STATE_NS
+#define DELEGATED GRANULE_STATE_DELEGATED
+#define RD GRANULE_STATE_RD
+#define DATA GRANULE_STATE_DATA
+#define REC GRANULE_STATE_REC
+#define RTT GRANULE_STATE_RTT
+
+#define RMM_GRANULE_SIZE GRANULE_SIZE
+
+enum granule_gpt {
+ GPT_AAP,
+ GPT_NS,
+ GPT_REALM,
+ GPT_ROOT,
+ GPT_SECURE
+};
+
+struct SPEC_granule {
+ enum granule_gpt gpt;
+ enum granule_state state;
+};
+
+extern unsigned char granules_buffer[HOST_MEM_SIZE];
+
+/*
+ * Declare nondet_* functions.
+ * CBMC automatically returns nondet values based on the return types.
+ * However, enum is treated as integer hence the value might out of range.
+ */
+struct granule nondet_struct_granule(void);
+struct SPEC_granule nondet_struct_SPEC_granule(void);
+
+bool valid_granule_ptr(struct granule *p);
+struct granule init_granule(void);
+void init_granule_and_page(void);
+
+/*
+ * Pedicates
+ */
+bool AddrIsGranuleAligned(uint64_t addr);
+bool PaIsDelegable(uint64_t addr);
+struct SPEC_granule Granule(uint64_t addr);
+
+#endif /* !TB_GRANULES_H */
diff --git a/tools/cbmc/src/tb.c b/tools/cbmc/src/tb.c
new file mode 100644
index 0000000..441193e
--- /dev/null
+++ b/tools/cbmc/src/tb.c
@@ -0,0 +1,63 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include "tb.h"
+#include "tb_common.h"
+#include "tb_granules.h"
+
+#include "rsi-handler.h"
+#include "smc-handler.h"
+#include "smc-rsi.h"
+#include "smc.h"
+
+void __init_global_state(unsigned long cmd)
+{
+ REACHABLE;
+ global_sanity_check();
+ /* Set up all the system register */
+ host_util_setup_sysreg_and_boot_manifest();
+ switch (cmd) {
+ case SMC_RMM_FEATURES: {
+ return;
+ }
+ case SMC_RMM_GRANULE_DELEGATE:
+ case SMC_RMM_GRANULE_UNDELEGATE: {
+ init_granule_and_page();
+ return;
+ }
+ default:
+ ASSERT(false, "tb_handle_smc fail");
+ }
+}
+
+/* Sanity check on the implementation of CBMC */
+void global_sanity_check(void)
+{
+ __CPROVER_cover(valid_pa(nondet_unsigned_long()));
+}
+
+void tb_handle_smc(struct tb_regs *config)
+{
+ unsigned long result = 0;
+
+ switch (config->X0) {
+ case SMC_RMM_GRANULE_DELEGATE:
+ result = smc_granule_delegate(config->X1);
+ break;
+ case SMC_RMM_GRANULE_UNDELEGATE:
+ result = smc_granule_undelegate(config->X1);
+ break;
+ default:
+ ASSERT(false, "_tb_handle_smc fail");
+ }
+
+ /* Update the return value. */
+ config->X0 = result;
+}
+
+void __tb_expect_fail(void)
+{
+ /* Assertion used to check consistency of the testbench */
+}
diff --git a/tools/cbmc/src/tb_common.c b/tools/cbmc/src/tb_common.c
new file mode 100644
index 0000000..4aa5f1d
--- /dev/null
+++ b/tools/cbmc/src/tb_common.c
@@ -0,0 +1,185 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include "status.h"
+#include "table.h"
+#include "utils_def.h"
+#include "tb_common.h"
+#include "host_defs.h"
+#include "host_utils.h"
+#include "string.h"
+#include "granule.h"
+#include "tb_granules.h"
+#include "measurement.h"
+
+/* Declare a nondet function for registers information. */
+struct tb_regs nondet_tb_regs(void);
+
+struct tb_regs __tb_arb_regs(void)
+{
+ return nondet_tb_regs();
+}
+
+bool ResultEqual_2(unsigned int code, unsigned int expected)
+{
+ return code == expected;
+}
+
+/* TODO */
+bool ResultEqual_3(unsigned int code, unsigned int expected, unsigned int level)
+{
+ return true;
+}
+
+uint64_t Zeros(void)
+{
+ return UINT64_C(0);
+}
+
+bool __tb_arb_bool(void)
+{
+ return nondet_bool();
+}
+
+void __tb_lock_invariant(struct tb_lock_status *lock_status)
+{
+ /* TODO */
+}
+
+struct tb_lock_status __tb_lock_status(void)
+{
+ struct tb_lock_status r = {NULL};
+ return r;
+}
+
+extern struct granule granules[RMM_MAX_GRANULES];
+bool used_granules_buffer[HOST_NR_GRANULES] = { 0 };
+
+bool valid_pa(uint64_t addr)
+{
+ /*
+ * NOTE: the explicit pointer to integer type cast is necessary, as CBMC
+ * check fails without it.
+ */
+ if (GRANULE_ALIGNED(addr) && (uint64_t)granules_buffer <= addr &&
+ addr < (uint64_t)granules_buffer + sizeof(granules_buffer)) {
+ /*
+ * Keep these assserts for sanitary check, there was situation
+ * these asserts fail possibly due to CBMC dislike type
+ * conversion between number and pointer
+ */
+ ASSERT(GRANULE_ALIGNED(addr), "internal: `_valid_pa`, addr in alignment");
+ ASSERT(addr >= (uint64_t)granules_buffer,
+ "internal: `_valid_pa`, addr in lower range");
+ ASSERT(addr < (uint64_t)granules_buffer + sizeof(granules_buffer),
+ "internal: `_valid_pa`, addr in upper range");
+ return true;
+ }
+ return false;
+}
+
+struct granule *pa_to_granule_metadata_ptr(uint64_t addr)
+{
+ uint64_t idx = (addr - (uint64_t)granules_buffer)/GRANULE_SIZE;
+
+ __ASSERT(idx >= 0, "internal: `_pa_to_granule_metadata_ptr`, addr is in lower range");
+ __ASSERT(idx < RMM_MAX_GRANULES,
+ "internal: `_pa_to_granule_metadata_ptr`, addr is in upper range");
+
+ return &granules[idx];
+}
+
+uint64_t granule_metadata_ptr_to_pa(struct granule *g_ptr)
+{
+ return (uint64_t)granules_buffer + (g_ptr - granules) * GRANULE_SIZE;
+}
+
+void *pa_to_granule_buffer_ptr(uint64_t addr)
+{
+ __ASSERT((unsigned char *)addr - granules_buffer >= 0,
+ "internal: `_pa_to_granule_buffer_ptr`, addr is in lower range");
+ /*
+ * NOTE: Has to do this strange computation and type cast so CBMC can
+ * handle.
+ */
+ return (void *)granules_buffer + ((unsigned char *)addr - granules_buffer);
+}
+
+void *granule_metadata_ptr_to_buffer_ptr(struct granule *g_ptr)
+{
+ if (!valid_granule_metadata_ptr(g_ptr)) {
+ return NULL;
+ }
+ return granules_buffer + (g_ptr - granules) * GRANULE_SIZE;
+}
+
+size_t granule_metadata_ptr_to_index(struct granule *g_ptr)
+{
+ return g_ptr - granules;
+}
+
+bool valid_granule_metadata_ptr(struct granule *p)
+{
+ return p >= granules
+ && p < granules + RMM_MAX_GRANULES;
+}
+
+/*
+ * Return the first index of `number` of unused continuous indice to both
+ * `granules` and `granules_buffer` arrays.
+ */
+size_t next_index(void)
+{
+ size_t index = nondet_size_t();
+
+ __ASSUME(unused_index(index));
+ if (!unused_index(index)) {
+ return -1;
+ }
+
+ REACHABLE;
+
+ return index;
+}
+
+bool unused_index(size_t index)
+{
+ if (index < HOST_NR_GRANULES && !used_granules_buffer[index]) {
+ return true;
+ }
+ return false;
+}
+
+void init_pa_page(const void *content, size_t size)
+{
+ unsigned long index = next_index();
+ unsigned long offset = index * GRANULE_SIZE;
+
+ (void)memcpy(granules_buffer + offset, content, size);
+ used_granules_buffer[index] = true;
+}
+
+struct granule *inject_granule_at(const struct granule *granule_metadata,
+ const void *src_page,
+ size_t src_size,
+ size_t index)
+{
+ size_t offset = index * GRANULE_SIZE;
+
+ granules[index] = *granule_metadata;
+ (void)memcpy(granules_buffer + offset, src_page, src_size);
+ used_granules_buffer[index] = true;
+ return &granules[index];
+}
+
+struct granule *inject_granule(const struct granule *granule_metadata,
+ const void *src_page,
+ size_t src_size)
+{
+ size_t index = next_index();
+
+ return inject_granule_at(granule_metadata, src_page, src_size, index);
+}
+
diff --git a/tools/cbmc/src/tb_granules.c b/tools/cbmc/src/tb_granules.c
new file mode 100644
index 0000000..5668c5a
--- /dev/null
+++ b/tools/cbmc/src/tb_granules.c
@@ -0,0 +1,115 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include "tb_granules.h"
+#include "tb_common.h"
+#include "buffer.h"
+#include "granule.h"
+#include "granule_types.h"
+#include "sizes.h"
+#include "host_defs.h"
+#include "host_utils.h"
+#include "platform_api.h"
+#include "string.h"
+
+extern struct granule granules[RMM_MAX_GRANULES];
+
+/* Chooses an arbitrary granule state. */
+bool valid_granule_state(enum granule_state value)
+{
+ return value == GRANULE_STATE_NS
+ || value == GRANULE_STATE_DELEGATED
+ || value == GRANULE_STATE_RD
+ || value == GRANULE_STATE_REC
+ || value == GRANULE_STATE_REC_AUX
+ || value == GRANULE_STATE_DATA
+ || value == GRANULE_STATE_RTT;
+}
+
+/* Ref to `__granule_assert_unlocked_invariants` function in `granule.h`. */
+bool valid_granule(struct granule value)
+{
+ if (value.lock.val != 0) {
+ return false;
+ }
+
+ switch (value.state) {
+ case GRANULE_STATE_NS:
+ case GRANULE_STATE_DELEGATED:
+ case GRANULE_STATE_DATA:
+ case GRANULE_STATE_REC_AUX: return value.refcount == 0;
+ /*
+ * refcount is used to check if RD and associated granules can
+ * be freed because they're no longer referenced by any other
+ * object. Can be any non-negative number.
+ */
+ case GRANULE_STATE_REC: return value.refcount <= 1;
+ case GRANULE_STATE_RTT: return value.refcount >= 0 &&
+ value.refcount <= GRANULE_SIZE / sizeof(uint64_t);
+ case GRANULE_STATE_RD: return true;
+ default: return false;
+ }
+ return false;
+}
+
+struct granule init_granule(void)
+{
+ struct granule rst = nondet_struct_granule();
+
+ __CPROVER_assume(valid_granule(rst));
+ return rst;
+}
+
+void init_granule_and_page(void)
+{
+ struct granule g = init_granule();
+ /* just write one byte when call the `inject_granule` functions */
+ char ns_granule[1] = { 0 };
+
+ inject_granule(&g, ns_granule, sizeof(ns_granule));
+}
+
+/*
+ * Implementation of pedicates
+ */
+bool AddrIsGranuleAligned(uint64_t addr)
+{
+ return GRANULE_ALIGNED(addr);
+}
+
+bool PaIsDelegable(uint64_t addr)
+{
+ return valid_pa(addr);
+}
+
+struct SPEC_granule Granule(uint64_t addr)
+{
+ if (!valid_pa(addr)) {
+ return nondet_struct_SPEC_granule();
+ }
+
+ struct granule *result = pa_to_granule_metadata_ptr(addr);
+
+ struct SPEC_granule spec_granule;
+
+ spec_granule.state = result->state;
+
+ switch (result->state) {
+ case GRANULE_STATE_NS:
+ case GRANULE_STATE_RTT:
+ spec_granule.gpt = GPT_NS;
+ break;
+ case GRANULE_STATE_RD:
+ case GRANULE_STATE_DATA:
+ case GRANULE_STATE_REC:
+ case GRANULE_STATE_DELEGATED:
+ spec_granule.gpt = GPT_REALM;
+ break;
+ default:
+ spec_granule.gpt = GPT_AAP;
+ }
+
+ return spec_granule;
+}
diff --git a/tools/cbmc/testbenches/tb_rmi_granule_delegate.c b/tools/cbmc/testbenches/tb_rmi_granule_delegate.c
new file mode 100644
index 0000000..83cadcc
--- /dev/null
+++ b/tools/cbmc/testbenches/tb_rmi_granule_delegate.c
@@ -0,0 +1,157 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ *
+ * This file was AUTOGENERATED from the RMM specification.
+ * RMM specification source version: 790fd539
+ */
+
+#include "tb.h"
+#include "tb_rmi_granule_delegate.h"
+
+bool tb_rmi_granule_delegate(
+ uint64_t addr)
+{
+ /*
+ * Initialize registers
+ */
+
+ struct tb_regs __tb_regs = __tb_arb_regs();
+
+ __tb_regs.X0 = SMC_RMM_GRANULE_DELEGATE;
+ __tb_regs.X1 = (uint64_t)addr;
+
+ /*
+ * Initialize global state
+ */
+
+ __init_global_state(__tb_regs.X0);
+
+ /*
+ * Pre-conditions
+ */
+
+ bool failure_gran_align_pre = !AddrIsGranuleAligned(addr);
+ bool failure_gran_bound_pre = !PaIsDelegable(addr);
+ bool failure_gran_state_pre = Granule(addr).state != UNDELEGATED;
+ bool failure_gran_gpt_pre = Granule(addr).gpt != GPT_NS;
+ bool no_failures_pre = !failure_gran_align_pre
+ && !failure_gran_bound_pre
+ && !failure_gran_state_pre
+ && !failure_gran_gpt_pre;
+
+ /*
+ * Execute command and read the result.
+ */
+
+ tb_handle_smc(&__tb_regs);
+ uint64_t result = __tb_regs.X0;
+
+ /*
+ * Post-conditions
+ */
+
+ bool failure_gran_align_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool failure_gran_bound_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool failure_gran_state_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool failure_gran_gpt_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool success_gran_state_post = Granule(addr).state == DELEGATED;
+ bool success_gran_gpt_post = Granule(addr).gpt == GPT_REALM;
+
+ /*
+ * Failure condition assertions
+ */
+
+ bool prop_failure_gran_align_ante = failure_gran_align_pre;
+
+ __COVER(prop_failure_gran_align_ante);
+ if (prop_failure_gran_align_ante) {
+ bool prop_failure_gran_align_cons = failure_gran_align_post;
+
+ __COVER(prop_failure_gran_align_cons);
+ __ASSERT(prop_failure_gran_align_cons, "prop_failure_gran_align_cons");
+ }
+
+ bool prop_failure_gran_bound_ante = !failure_gran_align_pre
+ && failure_gran_bound_pre;
+
+ __COVER(prop_failure_gran_bound_ante);
+ if (prop_failure_gran_bound_ante) {
+ bool prop_failure_gran_bound_cons = failure_gran_bound_post;
+
+ __COVER(prop_failure_gran_bound_cons);
+ __ASSERT(prop_failure_gran_bound_cons, "prop_failure_gran_bound_cons");
+ }
+
+ bool prop_failure_gran_state_ante = !failure_gran_align_pre
+ && !failure_gran_bound_pre
+ && failure_gran_state_pre;
+
+ __COVER(prop_failure_gran_state_ante);
+ if (prop_failure_gran_state_ante) {
+ bool prop_failure_gran_state_cons = failure_gran_state_post;
+
+ __COVER(prop_failure_gran_state_cons);
+ __ASSERT(prop_failure_gran_state_cons, "prop_failure_gran_state_cons");
+ }
+
+ bool prop_failure_gran_gpt_ante = !failure_gran_align_pre
+ && !failure_gran_bound_pre
+ && !failure_gran_state_pre
+ && failure_gran_gpt_pre;
+
+ __COVER(prop_failure_gran_gpt_ante);
+ if (prop_failure_gran_gpt_ante) {
+ bool prop_failure_gran_gpt_cons = failure_gran_gpt_post;
+
+ __COVER(prop_failure_gran_gpt_cons);
+ __ASSERT(prop_failure_gran_gpt_cons, "prop_failure_gran_gpt_cons");
+ }
+
+ /*
+ * Result assertion
+ */
+
+ bool prop_result_ante = no_failures_pre;
+
+ __COVER(prop_result_ante);
+ if (prop_result_ante) {
+ bool prop_result_cons = result == RMI_SUCCESS;
+
+ __COVER(prop_result_cons);
+ __ASSERT(prop_result_cons, "prop_result_cons");
+ }
+
+ /*
+ * Success condition assertions
+ */
+
+ bool prop_success_gran_state_ante = no_failures_pre;
+
+ __COVER(prop_success_gran_state_ante);
+ if (prop_success_gran_state_ante) {
+ bool prop_success_gran_state_cons = success_gran_state_post
+ && (result == RMI_SUCCESS);
+
+ __COVER(prop_success_gran_state_cons);
+ __ASSERT(prop_success_gran_state_cons, "prop_success_gran_state_cons");
+ }
+
+ bool prop_success_gran_gpt_ante = no_failures_pre;
+
+ __COVER(prop_success_gran_gpt_ante);
+ if (prop_success_gran_gpt_ante) {
+ bool prop_success_gran_gpt_cons = success_gran_gpt_post
+ && (result == RMI_SUCCESS);
+
+ __COVER(prop_success_gran_gpt_cons);
+ __ASSERT(prop_success_gran_gpt_cons, "prop_success_gran_gpt_cons");
+ }
+
+ /*
+ * Assertion used to check consistency of the testbench
+ */
+ __tb_expect_fail();
+
+ return no_failures_pre;
+}
diff --git a/tools/cbmc/testbenches/tb_rmi_granule_delegate.h b/tools/cbmc/testbenches/tb_rmi_granule_delegate.h
new file mode 100644
index 0000000..d60b5c5
--- /dev/null
+++ b/tools/cbmc/testbenches/tb_rmi_granule_delegate.h
@@ -0,0 +1,28 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ *
+ * This file was AUTOGENERATED from the RMM specification.
+ * RMM specification source version: 790fd539
+ */
+
+#ifndef __TB_RMI_GRANULE_DELEGATE_H
+#define __TB_RMI_GRANULE_DELEGATE_H
+
+#include "stdbool.h"
+#include "stdint.h"
+
+/*
+ * Testbench for RMI_GRANULE_DELEGATE command. Check via CBMC with flag
+ * `--entry-point tb_rmi_granule_delegate`.
+ *
+ * Arguments:
+ * addr: PA of the target Granule.
+ *
+ * Returns:
+ * bool: Output value.
+ */
+bool tb_rmi_granule_delegate(
+ uint64_t addr);
+
+#endif /* __TB_RMI_GRANULE_DELEGATE_H */
diff --git a/tools/cbmc/testbenches/tb_rmi_granule_undelegate.c b/tools/cbmc/testbenches/tb_rmi_granule_undelegate.c
new file mode 100644
index 0000000..d5ee71c
--- /dev/null
+++ b/tools/cbmc/testbenches/tb_rmi_granule_undelegate.c
@@ -0,0 +1,153 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ *
+ * This file was AUTOGENERATED from the RMM specification.
+ * RMM specification source version: 790fd539
+ */
+
+#include "tb.h"
+#include "tb_rmi_granule_undelegate.h"
+
+bool tb_rmi_granule_undelegate(
+ uint64_t addr)
+{
+ /*
+ * Initialize registers
+ */
+
+ struct tb_regs __tb_regs = __tb_arb_regs();
+
+ __tb_regs.X0 = SMC_RMM_GRANULE_UNDELEGATE;
+ __tb_regs.X1 = (uint64_t)addr;
+
+ /*
+ * Initialize global state
+ */
+
+ __init_global_state(__tb_regs.X0);
+
+ /*
+ * Pre-conditions
+ */
+
+ bool failure_gran_align_pre = !AddrIsGranuleAligned(addr);
+ bool failure_gran_bound_pre = !PaIsDelegable(addr);
+ bool failure_gran_state_pre = Granule(addr).state != DELEGATED;
+ bool no_failures_pre = !failure_gran_align_pre
+ && !failure_gran_bound_pre
+ && !failure_gran_state_pre;
+
+ /*
+ * Execute command and read the result.
+ */
+
+ tb_handle_smc(&__tb_regs);
+ uint64_t result = __tb_regs.X0;
+
+ /*
+ * Post-conditions
+ */
+
+ bool failure_gran_align_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool failure_gran_bound_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool failure_gran_state_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+ bool success_gran_gpt_post = Granule(addr).gpt == GPT_NS;
+ bool success_gran_state_post = Granule(addr).state == UNDELEGATED;
+ bool success_gran_content_post = true;
+
+ /*
+ * Failure condition assertions
+ */
+
+ bool prop_failure_gran_align_ante = failure_gran_align_pre;
+
+ __COVER(prop_failure_gran_align_ante);
+ if (prop_failure_gran_align_ante) {
+ bool prop_failure_gran_align_cons = failure_gran_align_post;
+
+ __COVER(prop_failure_gran_align_cons);
+ __ASSERT(prop_failure_gran_align_cons, "prop_failure_gran_align_cons");
+ }
+
+ bool prop_failure_gran_bound_ante = !failure_gran_align_pre
+ && failure_gran_bound_pre;
+
+ __COVER(prop_failure_gran_bound_ante);
+ if (prop_failure_gran_bound_ante) {
+ bool prop_failure_gran_bound_cons = failure_gran_bound_post;
+
+ __COVER(prop_failure_gran_bound_cons);
+ __ASSERT(prop_failure_gran_bound_cons, "prop_failure_gran_bound_cons");
+ }
+
+ bool prop_failure_gran_state_ante = !failure_gran_align_pre
+ && !failure_gran_bound_pre
+ && failure_gran_state_pre;
+
+ __COVER(prop_failure_gran_state_ante);
+ if (prop_failure_gran_state_ante) {
+ bool prop_failure_gran_state_cons = failure_gran_state_post;
+
+ __COVER(prop_failure_gran_state_cons);
+ __ASSERT(prop_failure_gran_state_cons, "prop_failure_gran_state_cons");
+ }
+
+ /*
+ * Result assertion
+ */
+
+ bool prop_result_ante = no_failures_pre;
+
+ __COVER(prop_result_ante);
+ if (prop_result_ante) {
+ bool prop_result_cons = result == RMI_SUCCESS;
+
+ __COVER(prop_result_cons);
+ __ASSERT(prop_result_cons, "prop_result_cons");
+ }
+
+ /*
+ * Success condition assertions
+ */
+
+ bool prop_success_gran_gpt_ante = no_failures_pre;
+
+ __COVER(prop_success_gran_gpt_ante);
+ if (prop_success_gran_gpt_ante) {
+ bool prop_success_gran_gpt_cons = success_gran_gpt_post
+ && (result == RMI_SUCCESS);
+
+ __COVER(prop_success_gran_gpt_cons);
+ __ASSERT(prop_success_gran_gpt_cons, "prop_success_gran_gpt_cons");
+ }
+
+ bool prop_success_gran_state_ante = no_failures_pre;
+
+ __COVER(prop_success_gran_state_ante);
+ if (prop_success_gran_state_ante) {
+ bool prop_success_gran_state_cons = success_gran_state_post
+ && (result == RMI_SUCCESS);
+
+ __COVER(prop_success_gran_state_cons);
+ __ASSERT(prop_success_gran_state_cons, "prop_success_gran_state_cons");
+ }
+
+ bool prop_success_gran_content_ante = no_failures_pre;
+
+ __COVER(prop_success_gran_content_ante);
+ if (prop_success_gran_content_ante) {
+ bool prop_success_gran_content_cons = success_gran_content_post
+ && (result == RMI_SUCCESS);
+
+ __COVER(prop_success_gran_content_cons);
+ __ASSERT(prop_success_gran_content_cons, "prop_success_gran_content_cons");
+ }
+
+ /*
+ * Assertion used to check consistency of the testbench
+ */
+ __tb_expect_fail();
+
+ return no_failures_pre;
+}
diff --git a/tools/cbmc/testbenches/tb_rmi_granule_undelegate.h b/tools/cbmc/testbenches/tb_rmi_granule_undelegate.h
new file mode 100644
index 0000000..13649d5
--- /dev/null
+++ b/tools/cbmc/testbenches/tb_rmi_granule_undelegate.h
@@ -0,0 +1,28 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ *
+ * This file was AUTOGENERATED from the RMM specification.
+ * RMM specification source version: 790fd539
+ */
+
+#ifndef __TB_RMI_GRANULE_UNDELEGATE_H
+#define __TB_RMI_GRANULE_UNDELEGATE_H
+
+#include "stdbool.h"
+#include "stdint.h"
+
+/*
+ * Testbench for RMI_GRANULE_UNDELEGATE command. Check via CBMC with flag
+ * `--entry-point tb_rmi_granule_undelegate`.
+ *
+ * Arguments:
+ * addr: PA of the target Granule.
+ *
+ * Returns:
+ * bool: Output value.
+ */
+bool tb_rmi_granule_undelegate(
+ uint64_t addr);
+
+#endif /* __TB_RMI_GRANULE_UNDELEGATE_H */
diff --git a/tools/cbmc/testbenches_results/BASELINE.analysis b/tools/cbmc/testbenches_results/BASELINE.analysis
new file mode 100644
index 0000000..5e9e8b0
--- /dev/null
+++ b/tools/cbmc/testbenches_results/BASELINE.analysis
@@ -0,0 +1,7 @@
++--------------------------------------+--------------------------------------+
+| FILENAME | ANALYSIS |
++--------------------------------------+--------------------------------------+
+| tb_rmi_granule_delegate.c | 9 of 363 failed (6 iterations) |
++--------------------------------------+--------------------------------------+
+| tb_rmi_granule_undelegate.c | 8 of 361 failed (5 iterations) |
++--------------------------------------+--------------------------------------+
diff --git a/tools/cbmc/testbenches_results/BASELINE.assert b/tools/cbmc/testbenches_results/BASELINE.assert
new file mode 100644
index 0000000..7ebd935
--- /dev/null
+++ b/tools/cbmc/testbenches_results/BASELINE.assert
@@ -0,0 +1,7 @@
++--------------------------------------+--------------------------------------+
+| FILENAME | ASSERT |
++--------------------------------------+--------------------------------------+
+| tb_rmi_granule_delegate.c | 0 of 40 failed (1 iterations) |
++--------------------------------------+--------------------------------------+
+| tb_rmi_granule_undelegate.c | 0 of 40 failed (1 iterations) |
++--------------------------------------+--------------------------------------+
diff --git a/tools/cbmc/testbenches_results/BASELINE.coverage b/tools/cbmc/testbenches_results/BASELINE.coverage
new file mode 100644
index 0000000..5670a12
--- /dev/null
+++ b/tools/cbmc/testbenches_results/BASELINE.coverage
@@ -0,0 +1,7 @@
++--------------------------------------+--------------------------------------+
+| FILENAME | COVERAGE |
++--------------------------------------+--------------------------------------+
+| tb_rmi_granule_delegate.c | 15 of 17 covered (88.2%) |
++--------------------------------------+--------------------------------------+
+| tb_rmi_granule_undelegate.c | 17 of 17 covered (100.0%) |
++--------------------------------------+--------------------------------------+