Temporary workaround to make CBMC run on handle___pkvm_init without crashing
diff --git a/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h b/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h
index 1e6d995..bd1cc9e 100644
--- a/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h
+++ b/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h
@@ -13,6 +13,6 @@
#define cpu_reg(ctxt, r) (ctxt)->regs.regs[r]
#define DECLARE_REG(type, name, ctxt, reg) \
- type name = (type)cpu_reg(ctxt, (reg))
+ type name; //= (type)cpu_reg(ctxt, (reg))
#endif /* __ARM64_KVM_NVHE_TRAP_HANDLER_H__ */
diff --git a/arch/arm64/kvm/hyp/nvhe/hyp-main.c b/arch/arm64/kvm/hyp/nvhe/hyp-main.c
index 1086ff2..504a857 100644
--- a/arch/arm64/kvm/hyp/nvhe/hyp-main.c
+++ b/arch/arm64/kvm/hyp/nvhe/hyp-main.c
@@ -896,7 +896,7 @@
__vgic_v3_restore_vmcr_aprs(shadow_cpu_if);
}
-static void handle___pkvm_init(struct kvm_cpu_context *host_ctxt)
+static void handle___pkvm_init(int host_ctxt)
{
DECLARE_REG(phys_addr_t, phys, host_ctxt, 1);
DECLARE_REG(unsigned long, size, host_ctxt, 2);
@@ -910,7 +910,7 @@
* will tail-call in __pkvm_init_finalise() which will have to deal
* with the host context directly.
*/
- cpu_reg(host_ctxt, 1) = __pkvm_init(phys, size, nr_cpus, per_cpu_base,
+ __pkvm_init(phys, size, nr_cpus, per_cpu_base,
hyp_va_bits, iommu_driver);
}
diff --git a/cbmc.sh b/cbmc.sh
new file mode 100755
index 0000000..be29f7a
--- /dev/null
+++ b/cbmc.sh
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+CBMC=cbmc
+TARGET_FILE=arch/arm64/kvm/hyp/nvhe/kvm_nvhe.gb
+
+CHECKS="--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"
+
+$CBMC \
+ $CHECKS \
+ --nondet-static \
+ --trace \
+ --trace-show-code \
+ --trace-show-function-calls \
+ $@ \
+ $TARGET_FILE
