feat(tools/cbmc): add testbench for RMI_REC_DESTROY
- Add testbench code for RMI_REALM_DESTROY
- Remove fields from struct rec so that the structure fits in the
reduced granule size for CBMC.
- Also remove code that uses the removed fields.
- Add CBMC glue layer code for REC handling.
- Increase CBMC GRANULE_SHIFT from 7 to 9 because 128 bytes is too
small 'struct rec'
- Update CBMC run baseline with tb_rmi_rec_destroy.c results
- Decrease MAX_NUM_OF_GRANULE to prevent CBMC run out of memory, and
add further changes to `struct rec` to increase its size
Change-Id: Ib2a646ecc2ed74d055364256bcad9976421d0ed9
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/plat/host/host_cbmc/CMakeLists.txt b/plat/host/host_cbmc/CMakeLists.txt
index 43e9027..bb380be 100644
--- a/plat/host/host_cbmc/CMakeLists.txt
+++ b/plat/host/host_cbmc/CMakeLists.txt
@@ -23,6 +23,7 @@
"src/tb_measurement.c"
"src/tb_ns_access.c"
"src/tb_realm.c"
+ "src/tb_rec.c"
"src/tb_rtt.c"
"src/tb.c"
)
diff --git a/plat/host/host_cbmc/include/tb.h b/plat/host/host_cbmc/include/tb.h
index 6bddf41..3c8c97d 100644
--- a/plat/host/host_cbmc/include/tb.h
+++ b/plat/host/host_cbmc/include/tb.h
@@ -10,6 +10,7 @@
#include "tb_common.h"
#include "tb_granules.h"
#include "tb_realm.h"
+#include "tb_rec.h"
typedef uint64_t rmi_interface_version_t;
diff --git a/plat/host/host_cbmc/include/tb_common.h b/plat/host/host_cbmc/include/tb_common.h
index 9e972a6..9a29474 100644
--- a/plat/host/host_cbmc/include/tb_common.h
+++ b/plat/host/host_cbmc/include/tb_common.h
@@ -106,6 +106,7 @@
bool valid_pa(uint64_t addr);
bool valid_granule_metadata_ptr(struct granule *p);
struct granule *pa_to_granule_metadata_ptr(uint64_t addr);
+void *granule_metadata_ptr_to_buffer_ptr(struct granule *g_ptr);
uint64_t granule_metadata_ptr_to_pa(struct granule *g_ptr);
void *pa_to_granule_buffer_ptr(uint64_t addr);
diff --git a/plat/host/host_cbmc/include/tb_rec.h b/plat/host/host_cbmc/include/tb_rec.h
new file mode 100644
index 0000000..1916780
--- /dev/null
+++ b/plat/host/host_cbmc/include/tb_rec.h
@@ -0,0 +1,42 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include <granule_types.h>
+
+#define REC_READY false
+#define REC_RUNNING true
+
+struct Rec_Runnable {
+ bool runnable;
+};
+
+/*
+ * In the spec, Rec predicate must return a concrete rec.
+ * We use a global fallback rec to by-pass this constraint.
+ * There is a mismatch in the type of `struct rec` against spec.
+ */
+struct rmm_rec {
+ enum attest_token_gen_state_t attest_state;
+ struct granule *aux[MAX_REC_AUX_GRANULES];
+ struct Rec_Runnable flags;
+ uint64_t gprs[RPV_SIZE];
+ uint64_t mpidr;
+ uint64_t owner;
+ uint64_t pc;
+ bool state; /* Either `REC_READY` or `REC_RUNNING` */
+ uint64_t ripas_addr;
+ uint64_t ripas_top;
+ enum ripas ripas_value;
+ enum ripas_change_destroyed ripas_destroyed;
+ bool host_call_pending;
+};
+
+struct granule *init_rec_page(struct granule *g_rd);
+struct rmm_rec Rec(uint64_t addr);
+
+bool AuxStateEqual(struct granule **aux, uint64_t num_aux, unsigned char state);
+
+struct rmm_rec nondet_struct_rmm_rec(void);
+struct rec nondet_rec(void);
diff --git a/plat/host/host_cbmc/src/tb.c b/plat/host/host_cbmc/src/tb.c
index c31d730..0566075 100644
--- a/plat/host/host_cbmc/src/tb.c
+++ b/plat/host/host_cbmc/src/tb.c
@@ -30,7 +30,13 @@
case SMC_RMM_REC_AUX_COUNT: {
init_realm_descriptor_page();
return;
- }
+ }
+ case SMC_RMM_REC_DESTROY: {
+ struct granule *g_rd = init_realm_descriptor_page();
+
+ init_rec_page(g_rd);
+ return;
+ }
case SMC_RMM_FEATURES:
case SMC_RMM_VERSION: {
/* No state to initialize */
@@ -70,6 +76,9 @@
result = res.x[0];
config->X1 = res.x[1];
break;
+ case SMC_RMM_REC_DESTROY:
+ result = smc_rec_destroy(config->X1);
+ break;
case SMC_RMM_VERSION:
smc_version(config->X1, &res);
result = res.x[0];
diff --git a/plat/host/host_cbmc/src/tb_common.c b/plat/host/host_cbmc/src/tb_common.c
index 5fcb3f4..2929ec5 100644
--- a/plat/host/host_cbmc/src/tb_common.c
+++ b/plat/host/host_cbmc/src/tb_common.c
@@ -94,6 +94,14 @@
return &granules[idx];
}
+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;
+}
+
uint64_t granule_metadata_ptr_to_pa(struct granule *g_ptr)
{
return (uint64_t)granules_buffer + (g_ptr - granules) * GRANULE_SIZE;
diff --git a/plat/host/host_cbmc/src/tb_realm.c b/plat/host/host_cbmc/src/tb_realm.c
index 91253c1..a4c7228 100644
--- a/plat/host/host_cbmc/src/tb_realm.c
+++ b/plat/host/host_cbmc/src/tb_realm.c
@@ -144,7 +144,7 @@
* This assert is necessary because the COMPILER_ASSERT in realm.h is
* disabled for CBMC.
*/
- __CPROVER_assert(sizeof(struct rd) <= GRANULE_SIZE, "check size");
+ __CPROVER_assert(sizeof(struct rd) <= GRANULE_SIZE, "check rd size");
struct granule *rd_granule = inject_granule(&g, &rd, sizeof(rd));
diff --git a/plat/host/host_cbmc/src/tb_rec.c b/plat/host/host_cbmc/src/tb_rec.c
new file mode 100644
index 0000000..723245e
--- /dev/null
+++ b/plat/host/host_cbmc/src/tb_rec.c
@@ -0,0 +1,102 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include <realm.h>
+#include <rec.h>
+#include <tb_common.h>
+#include <tb_granules.h>
+#include <tb_rec.h>
+
+static struct granule *init_aux_page(void)
+{
+ /* Add a rec_aux page */
+ unsigned long aux_content = 0;
+ struct granule g = init_granule();
+
+ __CPROVER_assume(g.state == GRANULE_STATE_REC_AUX);
+ struct granule *g_aux = inject_granule(&g, &aux_content, sizeof(aux_content));
+
+ return g_aux;
+}
+
+struct granule *init_rec_page(struct granule *g_rd)
+{
+ struct granule g = init_granule();
+
+ __CPROVER_assume(g.state == GRANULE_STATE_REC);
+ struct rec rec = nondet_rec();
+
+ /*
+ * This assert is necessary because the COMPILER_ASSERT in realm.h is
+ * disabled for CBMC.
+ */
+ __CPROVER_assert(sizeof(struct rec) <= GRANULE_SIZE, "check rec size");
+
+ rec.realm_info.g_rd = g_rd;
+
+ /* It must be a valid g_rd */
+ __CPROVER_assert(g_rd->state == GRANULE_STATE_RD,
+ "internal, `_init_rec_page` valid `g_rd`.");
+ struct rd *realm = granule_metadata_ptr_to_buffer_ptr(g_rd);
+
+ rec.realm_info.s2_ctx.g_rtt = realm->s2_ctx.g_rtt;
+ rec.realm_info.s2_ctx.s2_starting_level = realm->s2_ctx.s2_starting_level;
+
+ rec.num_rec_aux = 1;
+ rec.g_aux[0] = init_aux_page();
+
+ struct granule *g_rec = inject_granule(&g, &rec, sizeof(rec));
+
+ /*
+ * Look up the newly created 'struct rec' in the grenule buffer, and set
+ * the g_rec field
+ */
+ struct rec *rec_buf = (struct rec *)granule_metadata_ptr_to_buffer_ptr(g_rec);
+
+ rec_buf->g_rec = g_rec;
+
+ return g_rec;
+}
+
+struct rmm_rec Rec(uint64_t addr)
+{
+ if (!valid_pa(addr)) {
+ return nondet_struct_rmm_rec();
+ }
+
+ struct rec *rec_ptr = pa_to_granule_buffer_ptr(addr);
+
+ struct rmm_rec spec_rec = {
+ /* TODO .attest_state = */
+ .owner = granule_metadata_ptr_to_pa(rec_ptr->realm_info.g_rd),
+ .flags.runnable = rec_ptr->runnable,
+ .state = rec_ptr->g_rec->refcount == 0 ? REC_READY:REC_RUNNING,
+ .ripas_addr = rec_ptr->set_ripas.addr,
+ .ripas_top = rec_ptr->set_ripas.top,
+ .ripas_value = rec_ptr->set_ripas.ripas_val,
+ .ripas_destroyed = rec_ptr->set_ripas.change_destroyed,
+ .host_call_pending = rec_ptr->host_call
+ };
+
+ for (int i = 0; i < rec_ptr->num_rec_aux && i < MAX_REC_AUX_GRANULES; ++i) {
+ spec_rec.aux[i] = rec_ptr->g_aux[i];
+ }
+ return spec_rec;
+}
+
+bool AuxStateEqual(struct granule **aux, uint64_t num_aux, unsigned char state)
+{
+ struct granule *g_rec_aux = aux[0];
+ unsigned char aux_state = g_rec_aux->state;
+
+ __CPROVER_assert(num_aux >= 0 && num_aux <= MAX_REC_AUX_GRANULES,
+ "internal: _AuxStateEqual range check.");
+ for (int i = 0; i < num_aux && i < MAX_REC_AUX_GRANULES; ++i) {
+ if (!PaIsDelegable(granule_metadata_ptr_to_pa(aux[i])) || aux[i]->state != state) {
+ return false;
+ }
+ }
+ return true;
+}