forked from Imagelibrary/seL4
arm,gic_v3: consolidate types for verification
Verification requires inline assembly blocks to have consistent types. In gic_v3 files, the `msr` and `mrs` instructions are used both with uint32_t and uint64_t types, which causes the Isabelle C parser to fail. According to the Arm GICv3 specification, the registers we are accessing are all 64 bit registers. Some of them have the top 32 bits reserved as res0. These are the ones that currently are used with uint32_t, presumably for consistency with the corresponding gic_v2 functions. To make the C parser succeed: - for the SYSTEM_READ_WORD and SYSTEM_WRITE_WORD macros, use word_t or uint64_t - for functions that are declared with uint32_t, leave the declaration intact, but use uint64_t internally for MSR with an explicit cast to/from uint32_t. This is the behaviour we are assuming the C compiler to have added implicitly before. This commit does not change the fact that the gic_v3 virtualisation functions assume a 64-bit architecture. For AArch32, word_t and uint64_t may be incorrect. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
@@ -265,7 +265,7 @@ static inline irq_t getActiveIRQ(void)
|
||||
irq_t irq;
|
||||
|
||||
if (!IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) {
|
||||
uint32_t val = 0;
|
||||
word_t val = 0;
|
||||
SYSTEM_READ_WORD(ICC_IAR1_EL1, val);
|
||||
active_irq[CURRENT_CPU_INDEX()] = val;
|
||||
}
|
||||
@@ -288,7 +288,7 @@ static inline irq_t getActiveIRQ(void)
|
||||
/** DONT_TRANSLATE */
|
||||
static inline bool_t isIRQPending(void)
|
||||
{
|
||||
uint32_t val = 0;
|
||||
word_t val = 0;
|
||||
/* Check for pending IRQs in group 1: ICC_HPPIR1_EL1 */
|
||||
SYSTEM_READ_WORD(ICC_HPPIR1_EL1, val);
|
||||
return IS_IRQ_VALID(val);
|
||||
@@ -324,9 +324,10 @@ extern word_t gic_vcpu_num_list_regs;
|
||||
|
||||
static inline uint32_t get_gic_vcpu_ctrl_hcr(void)
|
||||
{
|
||||
uint32_t reg;
|
||||
uint64_t reg;
|
||||
MRS(ICH_HCR_EL2, reg);
|
||||
return reg;
|
||||
/* 64 bit register read, top 32 bits reserved */
|
||||
return (uint32_t) reg;
|
||||
}
|
||||
|
||||
static inline void set_gic_vcpu_ctrl_hcr(uint32_t hcr)
|
||||
@@ -336,9 +337,10 @@ static inline void set_gic_vcpu_ctrl_hcr(uint32_t hcr)
|
||||
|
||||
static inline uint32_t get_gic_vcpu_ctrl_vmcr(void)
|
||||
{
|
||||
uint32_t reg;
|
||||
uint64_t reg;
|
||||
MRS(ICH_VMCR_EL2, reg);
|
||||
return reg;
|
||||
/* 64 bit register read, top 32 bits reserved */
|
||||
return (uint32_t) reg;
|
||||
}
|
||||
|
||||
static inline void set_gic_vcpu_ctrl_vmcr(uint32_t vmcr)
|
||||
@@ -353,9 +355,10 @@ static inline void set_gic_vcpu_ctrl_vmcr(uint32_t vmcr)
|
||||
*/
|
||||
static inline uint32_t get_gic_vcpu_ctrl_apr(void)
|
||||
{
|
||||
uint32_t reg;
|
||||
uint64_t reg;
|
||||
MRS(ICH_AP1R0_EL2, reg);
|
||||
return reg;
|
||||
/* 64 bit register read, top 32 bits reserved */
|
||||
return (uint32_t) reg;
|
||||
}
|
||||
|
||||
static inline void set_gic_vcpu_ctrl_apr(uint32_t apr)
|
||||
@@ -365,15 +368,17 @@ static inline void set_gic_vcpu_ctrl_apr(uint32_t apr)
|
||||
|
||||
static inline uint32_t get_gic_vcpu_ctrl_vtr(void)
|
||||
{
|
||||
uint32_t reg;
|
||||
uint64_t reg;
|
||||
MRS(ICH_VTR_EL2, reg);
|
||||
return reg;
|
||||
/* 64 bit register read, top 32 bits reserved */
|
||||
return (uint32_t) reg;
|
||||
}
|
||||
|
||||
static inline uint32_t get_gic_vcpu_ctrl_eisr0(void)
|
||||
{
|
||||
uint32_t reg;
|
||||
uint64_t reg;
|
||||
MRS(ICH_EISR_EL2, reg);
|
||||
/* 64 bit register read, top 32 bits reserved */
|
||||
return reg;
|
||||
}
|
||||
|
||||
@@ -387,9 +392,10 @@ static inline uint32_t get_gic_vcpu_ctrl_eisr1(void)
|
||||
|
||||
static inline uint32_t get_gic_vcpu_ctrl_misr(void)
|
||||
{
|
||||
uint32_t reg;
|
||||
uint64_t reg;
|
||||
MRS(ICH_MISR_EL2, reg);
|
||||
return reg;
|
||||
/* 64 bit register read, top 32 bits reserved */
|
||||
return (uint32_t) reg;
|
||||
}
|
||||
|
||||
static inline virq_t get_gic_vcpu_ctrl_lr(int num)
|
||||
|
||||
@@ -123,7 +123,7 @@ static void gicv3_redist_wait_for_rwp(void)
|
||||
|
||||
static void gicv3_enable_sre(void)
|
||||
{
|
||||
uint32_t val = 0;
|
||||
word_t val = 0;
|
||||
|
||||
/* ICC_SRE_EL1 */
|
||||
SYSTEM_READ_WORD(ICC_SRE_EL1, val);
|
||||
@@ -265,7 +265,7 @@ BOOT_CODE static void gicr_init(void)
|
||||
|
||||
BOOT_CODE static void cpu_iface_init(void)
|
||||
{
|
||||
uint32_t icc_ctlr = 0;
|
||||
word_t icc_ctlr = 0;
|
||||
|
||||
/* Enable system registers */
|
||||
gicv3_enable_sre();
|
||||
|
||||
Reference in New Issue
Block a user