Merge changes I277b37ef,I41c330c1,I22e730b3 into integration

* changes:
  feat(tools/cbmc): add option to test a single testbench
  feat(tools/cbmc): add testbench for RMI_REALM_ACTIVATE
  refactor(lib/realm): rename realm states according to spec

docs/getting_started/build-options.rst

@@ -282,6 +282,7 @@ The |RMM| build system supports the following CMake build options.
    RMM_COVERAGE 		,ON | OFF		,OFF			,"Enable coverage analysis"
    RMM_HTML_COV_REPORT		,ON | OFF		,ON			,"Enable HTML output report for coverage analysis"
    RMM_CBMC_VIEWER_OUTPUT	,ON | OFF		,OFF			,"Generate report of CBMC results using the tool cbmc-viewer"
+   RMM_CBMC_SINGLE_TESTBENCH	,			,OFF			,"Run CBMC on a single testbench instead on all of them"
 
 .. _llvm_build:
 

docs/resources/application-notes/cbmc.rst

@@ -53,6 +53,12 @@ each build.
 
 For an example build command please refer to :ref:`RMM Build Examples`
 
+The CMake system by default runs CBMC on all the testbenches. This can take a
+long time, and it can be convenient to run a single testcase at once. This can
+be achieved using the option ``-DRMM_CBMC_SINGLE_TESTBENCH="testbench_name"``.
+The list of possible ``testbench_name``s can be listed by using the option
+``-DRMM_CBMC_SINGLE_TESTBENCH="help"``.
+
 The CMake system provides different modes in which CBMC can be called, along
 with their respective build targets.
 

lib/arch/include/arch_features.h

@@ -111,6 +111,13 @@ static inline bool is_feat_hpmn0_present(void)
 		read_id_aa64dfr0_el1()) == 1UL);
 }
 
+#ifndef CBMC
 unsigned int arch_feat_get_pa_width(void);
+#else /* CBMC */
+static inline unsigned int arch_feat_get_pa_width(void)
+{
+	return 32U;
+}
+#endif /* CBMC */
 
 #endif /* ARCH_FEATURES_H */

lib/arch/include/simd.h

@@ -187,7 +187,15 @@ COMPILER_ASSERT((U(offsetof(struct sve_regs, ffr))) == SVE_REGS_OFFSET_FFR);
 void simd_init(void);
 
 /* Returns the CPU SIMD config discovered during the init time */
+#ifndef CBMC
 int simd_get_cpu_config(struct simd_config *simd_cfg);
+#else /* CBMC */
+static inline int simd_get_cpu_config(struct simd_config *simd_cfg)
+{
+	memset(simd_cfg, 0, sizeof(*simd_cfg));
+	return 0;
+}
+#endif /* CBMC */
 
 /* Initialize the SIMD context in RMM corresponding to NS world or Realm */
 int simd_context_init(simd_owner_t owner, struct simd_context *simd_ctx,

lib/measurement/include/measurement.h

@@ -41,11 +41,15 @@ enum hash_algo {
 #define MEASURE_DESC_TYPE_REC		0x1
 #define MEASURE_DESC_TYPE_RIPAS		0x2
 
+#ifndef CBMC
 /*
  * Size in bytes of the largest measurement type that can be supported.
  * This macro needs to be updated accordingly if new algorithms are supported.
  */
 #define MAX_MEASUREMENT_SIZE		SHA512_SIZE
+#else
+#define MAX_MEASUREMENT_SIZE		sizeof(uint64_t)
+#endif
 
 /* RmmMeasurementDescriptorData type as per RMM spec */
 struct measurement_desc_data {

lib/realm/include/realm.h

@@ -12,9 +12,9 @@
 #include <rec.h>
 #include <table.h>
 
-#define REALM_STATE_NEW		0U
-#define REALM_STATE_ACTIVE	1U
-#define REALM_STATE_SYSTEM_OFF	2U
+#define REALM_NEW		0U
+#define REALM_ACTIVE		1U
+#define REALM_SYSTEM_OFF	2U
 
 /*
  * Stage 2 configuration of the Realm

lib/smc/include/smc-rmi.h

@@ -366,7 +366,15 @@
 #define SMC_RMM_RTT_SET_RIPAS			SMC64_RMI_FID(U(0x19))
 
 /* Size of Realm Personalization Value */
+#ifndef CBMC
 #define RPV_SIZE		64
+#else
+/*
+ * Small RPV size so that `struct rd` fits in the reduced sized granule defined
+ * for CBMC
+ */
+#define RPV_SIZE		1
+#endif
 
 /* RmiRealmFlags format */
 #define RMI_REALM_FLAGS_LPA2_SHIFT	UL(0)

plat/host/host_cbmc/CMakeLists.txt

@@ -19,6 +19,9 @@ target_sources(rmm-plat-host_cbmc
         "src/host_harness.c"
         "src/tb_common.c"
         "src/tb_granules.c"
+        "src/tb_measurement.c"
+        "src/tb_realm.c"
+        "src/tb_rtt.c"
         "src/tb.c"
         )
 

plat/host/host_cbmc/include/tb.h

@@ -9,6 +9,7 @@
 #include "smc-rmi.h"
 #include "tb_common.h"
 #include "tb_granules.h"
+#include "tb_realm.h"
 
 typedef uint64_t rmi_interface_version_t;
 

plat/host/host_cbmc/include/tb_common.h

@@ -106,6 +106,8 @@ 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 *pa_to_granule_buffer_ptr(uint64_t addr);
+
 /* TODO change the function name */
 void init_pa_page(const void *content, size_t size);
 

plat/host/host_cbmc/include/tb_granules.h

@@ -39,7 +39,12 @@ struct SPEC_granule {
 	enum granule_state state;
 };
 
+/*
+ * CBMC needs access to the below data structures which are not otherwise
+ * visible outside their respective files.
+ */
 extern unsigned char granules_buffer[HOST_MEM_SIZE];
+extern struct granule granules[RMM_MAX_GRANULES];
 
 /*
  * Declare nondet_* functions.

plat/host/host_cbmc/include/tb_measurement.h

@@ -0,0 +1,13 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_MEASUREMENT_H
+#define TB_MEASUREMENT_H
+
+#include "measurement.h"
+
+bool valid_hash_algo(enum hash_algo value);
+
+#endif /* !TB_MEASUREMENT_H */

plat/host/host_cbmc/include/tb_realm.h

@@ -0,0 +1,65 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_REALM_H
+#define TB_REALM_H
+
+#include <measurement.h>
+#include <realm.h>
+#include <smc-rmi.h>
+#include <tb_granules.h>
+
+#define DESTROYED RIPAS_DESTROYED
+#define EMPTY RIPAS_EMPTY
+#define RAM RIPAS_RAM
+
+extern unsigned long vmids[];
+
+enum rmm_rtt_entry_state {
+	ASSIGNED,
+	ASSIGNED_NS,
+	TABLE,
+	UNASSIGNED,
+	UNASSIGNED_NS,
+};
+
+struct rmm_realm {
+	uint64_t ipa_width;
+	uint64_t measurements[MEASUREMENT_SLOT_NR];
+	uint64_t hash_algo;
+	uint64_t rec_index;
+	uint64_t rtt_base;
+	uint64_t rtt_level_start;
+	uint64_t rtt_num_start;
+	uint64_t state;
+	uint64_t vmid;
+	uint8_t rpv[RPV_SIZE];
+};
+
+struct rmi_realm_params_buffer {
+	uint8_t flags;
+	uint8_t s2sz;
+	uint8_t sve_vl;
+	uint8_t num_bps;
+	uint8_t num_wps;
+	uint8_t pmu_num_ctrs;
+	uint8_t hash_algo;
+	uint8_t rpv[RPV_SIZE];
+	uint16_t vmid;
+	uint64_t rtt_base;
+	int64_t rtt_level_start;
+	uint32_t rtt_num_start;
+};
+
+bool VmidIsFree(uint16_t vmid);
+struct rmm_realm Realm(uint64_t rd);
+
+struct rd nondet_struct_rd(void);
+struct rmm_realm nondet_struct_rmm_realm(void);
+
+struct granule *init_realm_descriptor_page(void);
+
+#endif /* TB_REALM_H */
+

plat/host/host_cbmc/include/tb_rtt.h

@@ -0,0 +1,12 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_RTT_H
+#define TB_RTT_H
+
+bool valid_num_root_rtts(unsigned int num_root_rtts);
+struct granule *init_rtt_root_page(unsigned int num_root_rtts);
+
+#endif

plat/host/host_cbmc/src/tb.c

@@ -11,6 +11,7 @@
 #include "tb.h"
 #include "tb_common.h"
 #include "tb_granules.h"
+#include "tb_realm.h"
 
 void __init_global_state(unsigned long cmd)
 {
@@ -24,6 +25,10 @@ void __init_global_state(unsigned long cmd)
 			init_granule_and_page();
 			return;
 		}
+	case SMC_RMM_REALM_ACTIVATE:{
+			init_realm_descriptor_page();
+			return;
+	}
 	case SMC_RMM_FEATURES:
 	case SMC_RMM_VERSION: {
 			/* No state to initialize */
@@ -52,6 +57,9 @@ void tb_handle_smc(struct tb_regs *config)
 	case SMC_RMM_GRANULE_UNDELEGATE:
 		result = smc_granule_undelegate(config->X1);
 		break;
+	case SMC_RMM_REALM_ACTIVATE:
+		result = smc_realm_activate(config->X1);
+		break;
 	case SMC_RMM_VERSION:
 		smc_version(config->X1, &res);
 		result = res.x[0];

plat/host/host_cbmc/src/tb_common.c

@@ -94,6 +94,28 @@ struct granule *pa_to_granule_metadata_ptr(uint64_t addr)
 	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");
+	/*
+	 * CBMC has difficulty doing an integer->object mapping, when the
+	 * integer is the address of the expected object, and the integer is not
+	 * derived from a pointer.
+	 * So instead of simply returning addr we need to tell CBMC that the
+	 * object we are looking for is in the `granules_buffer` array, at an
+	 * offset. To calculate the offset we can use `addr`, and the address of
+	 * `granules_buffer`.
+	 * For details see https://github.com/diffblue/cbmc/issues/8103
+	 */
+	return (void *)granules_buffer + ((unsigned char *)addr - granules_buffer);
+}
+
 bool valid_granule_metadata_ptr(struct granule *p)
 {
 	return p >= granules
@@ -140,6 +162,13 @@ struct granule *inject_granule_at(const struct granule *granule_metadata,
 {
 	size_t offset = index * GRANULE_SIZE;
 
+	if (granule_metadata->state == GRANULE_STATE_NS) {
+		/* initialise the granules as either secure or non-secure */
+		granule_gpt_array[index] = nondet_bool() ? GPT_SECURE : GPT_NS;
+	} else {
+		granule_gpt_array[index] = GPT_REALM;
+	}
+
 	granules[index] = *granule_metadata;
 	(void)memcpy(granules_buffer + offset, src_page, src_size);
 	used_granules_buffer[index] = true;
@@ -152,13 +181,6 @@ struct granule *inject_granule(const struct granule *granule_metadata,
 {
 	size_t index = next_index();
 
-	if (granule_metadata->state == GRANULE_STATE_NS) {
-		/* initialise the granules as either secure or non-secure */
-		granule_gpt_array[index] = nondet_bool() ? GPT_SECURE : GPT_NS;
-	} else {
-		granule_gpt_array[index] = GPT_REALM;
-	}
-
 	return inject_granule_at(granule_metadata, src_page, src_size, index);
 }
 

plat/host/host_cbmc/src/tb_granules.c

@@ -14,8 +14,6 @@
 #include "tb_common.h"
 #include "tb_granules.h"
 
-extern struct granule granules[RMM_MAX_GRANULES];
-
 /* Chooses an arbitrary granule state. */
 bool valid_granule_state(enum granule_state value)
 {

plat/host/host_cbmc/src/tb_measurement.c

@@ -0,0 +1,13 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include "measurement.h"
+#include "tb_measurement.h"
+
+bool valid_hash_algo(enum hash_algo value)
+{
+	return value == RMI_HASH_SHA_256 ||
+	       value == RMI_HASH_SHA_512;
+}