refactor(tools/cbmc): rework cbmc delegate and undelegate
The cbmc analysis now has 0 failures for RMI_DELEGATE and
RMI_UNDELEGATE after this patch.
Change-Id: Ib7434e31870ee860d6eafb86af5b8c7aa742f777
Signed-off-by: Soby Mathew <soby.mathew@arm.com>
diff --git a/plat/host/host_cbmc/include/tb_common.h b/plat/host/host_cbmc/include/tb_common.h
index 36d989c..c77462f 100644
--- a/plat/host/host_cbmc/include/tb_common.h
+++ b/plat/host/host_cbmc/include/tb_common.h
@@ -128,9 +128,9 @@
const void *src_page,
size_t src_size);
-/* Returns whether the granule with address is set to NS in the GPT, or not */
-bool is_granule_gpt_ns(uint64_t addr);
-/* Set for a granule whether it is set to NS in GPT, or not. */
-void set_granule_gpt_ns(uint64_t addr, bool gpt_ns);
+/* Returns the status of the granule in the GPT. */
+enum granule_gpt get_granule_gpt(uint64_t addr);
+/* Set the status of the granule in GPT. */
+void set_granule_gpt(uint64_t addr, enum granule_gpt granule_gpt);
#endif /* !TB_COMMON_H */
diff --git a/plat/host/host_cbmc/include/tb_granules.h b/plat/host/host_cbmc/include/tb_granules.h
index 75f8817..b5fc79f 100644
--- a/plat/host/host_cbmc/include/tb_granules.h
+++ b/plat/host/host_cbmc/include/tb_granules.h
@@ -27,11 +27,11 @@
#define RMM_GRANULE_SIZE GRANULE_SIZE
enum granule_gpt {
- GPT_AAP,
+ GPT_SECURE,
GPT_NS,
GPT_REALM,
GPT_ROOT,
- GPT_SECURE
+ GPT_AAP
};
struct SPEC_granule {
diff --git a/plat/host/host_cbmc/src/host_harness.c b/plat/host/host_cbmc/src/host_harness.c
index d2e1ca8..3742cac 100644
--- a/plat/host/host_cbmc/src/host_harness.c
+++ b/plat/host/host_cbmc/src/host_harness.c
@@ -6,6 +6,7 @@
#include <buffer.h>
#include <host_harness.h>
#include <tb_common.h>
+#include <tb_granules.h>
void *host_buffer_arch_map(unsigned int slot, unsigned long addr)
{
@@ -21,8 +22,8 @@
unsigned long host_gtsi_delegate(unsigned long addr)
{
- if (is_granule_gpt_ns(addr)) {
- set_granule_gpt_ns(addr, false);
+ if (get_granule_gpt(addr) == GPT_NS) {
+ set_granule_gpt(addr, GPT_REALM);
return 0UL;
} else {
return 1UL;
@@ -31,7 +32,8 @@
unsigned long host_gtsi_undelegate(unsigned long addr)
{
- assert(!is_granule_gpt_ns(addr));
- set_granule_gpt_ns(addr, true);
+ assert(get_granule_gpt(addr) == GPT_REALM);
+
+ set_granule_gpt(addr, GPT_NS);
return 0UL;
}
diff --git a/plat/host/host_cbmc/src/tb_common.c b/plat/host/host_cbmc/src/tb_common.c
index 20158ef..4f94174 100644
--- a/plat/host/host_cbmc/src/tb_common.c
+++ b/plat/host/host_cbmc/src/tb_common.c
@@ -14,11 +14,8 @@
#include "tb_granules.h"
#include "utils_def.h"
-/*
- * This array holds information on whether the granule that is injected in
- * RMM's granule array is set to NS in the GPT, or not.
- */
-static bool granule_gpt_ns_array[RMM_MAX_GRANULES];
+/* This array holds information on the injected granule's status in the GPT. */
+static enum granule_gpt granule_gpt_array[RMM_MAX_GRANULES];
/* Declare a nondet function for registers information. */
struct tb_regs nondet_tb_regs(void);
@@ -156,23 +153,25 @@
size_t index = next_index();
if (granule_metadata->state == GRANULE_STATE_NS) {
- granule_gpt_ns_array[index] = nondet_bool();
- } else{
- granule_gpt_ns_array[index] = false;
+ /* 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);
}
-bool is_granule_gpt_ns(uint64_t addr)
+enum granule_gpt get_granule_gpt(uint64_t addr)
{
uint64_t idx = (addr - (uint64_t)granules_buffer)/GRANULE_SIZE;
- return granule_gpt_ns_array[idx];
+ return granule_gpt_array[idx];
}
-void set_granule_gpt_ns(uint64_t addr, bool gpt_ns)
+void set_granule_gpt(uint64_t addr, enum granule_gpt granule_gpt)
{
uint64_t idx = (addr - (uint64_t)granules_buffer)/GRANULE_SIZE;
- granule_gpt_ns_array[idx] = gpt_ns;
+ granule_gpt_array[idx] = granule_gpt;
}
diff --git a/plat/host/host_cbmc/src/tb_granules.c b/plat/host/host_cbmc/src/tb_granules.c
index a69e0bb..d66e2ad 100644
--- a/plat/host/host_cbmc/src/tb_granules.c
+++ b/plat/host/host_cbmc/src/tb_granules.c
@@ -58,6 +58,7 @@
{
struct granule rst = nondet_struct_granule();
+ __CPROVER_assume(__CPROVER_enum_is_in_range(rst.state));
__CPROVER_assume(valid_granule(rst));
return rst;
}
@@ -87,7 +88,10 @@
struct SPEC_granule Granule(uint64_t addr)
{
if (!valid_pa(addr)) {
- return nondet_struct_SPEC_granule();
+ struct SPEC_granule nd_granule = nondet_struct_SPEC_granule();
+ __CPROVER_assume(__CPROVER_enum_is_in_range(nd_granule.state));
+ __CPROVER_assume(__CPROVER_enum_is_in_range(nd_granule.gpt));
+ return nd_granule;
}
struct granule *result = pa_to_granule_metadata_ptr(addr);
@@ -98,11 +102,7 @@
switch (result->state) {
case GRANULE_STATE_NS:
- if (is_granule_gpt_ns(addr)) {
- spec_granule.gpt = GPT_NS;
- } else {
- spec_granule.gpt = GPT_SECURE;
- }
+ spec_granule.gpt = get_granule_gpt(addr);
break;
case GRANULE_STATE_RTT:
spec_granule.gpt = GPT_NS;