RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

arm hyp: gic_vcpu_num_list_regs should be word_t

Browse Source 
On AArch64, if this is int, we encounter a situation where we can't
prove equivalence with the abstract spec without an extra invariant that
the number of these registers isn't zero (to satisfy 32<->64 bit casts).
Sticking with word size will make sense on both 32 and 64 bit.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski
2023-12-05 14:17:34 +11:00
committed by Rafal Kolanski
parent 66e5c79d06
commit 55aee64707
4 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
include/arch/arm/arch/machine/gic_v2.h
View File

@@ -216,7 +216,7 @@ struct gich_vcpu_ctrl_map {
};
extern volatile struct gich_vcpu_ctrl_map *gic_vcpu_ctrl;
extern unsigned int gic_vcpu_num_list_regs;
extern word_t gic_vcpu_num_list_regs;
static inline uint32_t get_gic_vcpu_ctrl_hcr(void)
{

2
include/arch/arm/arch/machine/gic_v3.h
View File

@@ -320,7 +320,7 @@ static inline void ackInterrupt(irq_t irq)
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
extern unsigned int gic_vcpu_num_list_regs;
extern word_t gic_vcpu_num_list_regs;
static inline uint32_t get_gic_vcpu_ctrl_hcr(void)
{

2
src/arch/arm/machine/gic_v2.c
View File

@@ -228,6 +228,6 @@ volatile struct gich_vcpu_ctrl_map *gic_vcpu_ctrl =
(volatile struct gich_vcpu_ctrl_map *)(GIC_V2_VCPUCTRL_PPTR);
#endif /* GIC_PL400_GICVCPUCTRL_PPTR */
unsigned int gic_vcpu_num_list_regs;
word_t gic_vcpu_num_list_regs;
#endif /* End of CONFIG_ARM_HYPERVISOR_SUPPORT */

2
src/arch/arm/machine/gic_v3.c
View File

@@ -389,6 +389,6 @@ void setIRQTarget(irq_t irq, seL4_Word target)
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
unsigned int gic_vcpu_num_list_regs;
word_t gic_vcpu_num_list_regs;
#endif /* End of CONFIG_ARM_HYPERVISOR_SUPPORT */