Add GIC v3 support for AArch64 platforms #846
Conversation
Signed-off-by: Gerwin Klein <[email protected]>
In preparation for adding an API for software-generated interrupts, make config_ARM_GIC_V3 visible to the proofs, so values of constants can be defined conditionally on GICv2/v3 use. Signed-off-by: Gerwin Klein <[email protected]>
Adjust accessor functions in ASpec and Haskell to be dependent on GIC version. For GIC_v3 the encoding of the virq type changes. Although all of the fields are still present, they are at different bit positions and the IRQ field is larger. Signed-off-by: Gerwin Klein <[email protected]>
lsf37
added
platforms
- abstract over the value of max_armKSGICVCPUNumListRegs - adjust virq access proofs - abstract over vcpu type size in C (changes with GIC version, because number of LR registers changes) Signed-off-by: Gerwin Klein <[email protected]>
| groupShift = if config_ARM_GIC_V3 then 60 else 30; | ||
| prioShift = if config_ARM_GIC_V3 then 48 else 23; | ||
| irqPending = 1 << virq_type_shift; | ||
| eoiirqen = 1 << eoiirqen_shift; |
There was a problem hiding this comment.
Maybe not worth it because it's only used a few times, but we could pull eoiirqen out into its own definition or abbreviation and reuse it in virqSetEOIIRQEN in ArchInterrupt_A.
| groupShift = if config_ARM_GIC_V3 then 60 else 30; | ||
| prioShift = if config_ARM_GIC_V3 then 48 else 23; | ||
| irqPending = 1 << virq_type_shift; | ||
| eoiirqen = 1 << eoiirqen_shift; | ||
| irqMask = mask (if config_ARM_GIC_V3 then 32 else 10); | ||
| prioMask = mask (if config_ARM_GIC_V3 then 8 else 5) |
There was a problem hiding this comment.
Just to confirm, I guess the other bit positions aren't made into separate definitions because they're not used anywhere else?
| lemma virqType_eq[simp]: | ||
| "virqType = virq_type" |
There was a problem hiding this comment.
Not needed as part of this PR, but maybe we want a separate file near the start of Refine to put these lemmas connecting terms from the abstract and design specs. That would both make sure that they're accessible throughout all of Refine and also keep them all together for us to find them if/when we have time to try and reuse more between the specs.
| (* config unfolding to match bitfield shift in virq_get_tag with virq_type_shift in virq_type *) | ||
| by (simp add: virq_to_H_def virq_type_def virq_get_tag_def virq_type_shift_def mask_def | ||
| Kernel_Config.config_ARM_GIC_V3_def) | ||
|
|
||
| lemma decodeVCPUInjectIRQ_ccorres: |
There was a problem hiding this comment.
Nice cleanup in this lemma, it looks a lot better!
| schematic_goal max_armKSGICVCPUNumListRegs_int_val: | ||
| "int max_armKSGICVCPUNumListRegs = numeral ?n" | ||
| by (simp add: max_armKSGICVCPUNumListRegs_val) |
There was a problem hiding this comment.
Should this be moved to Wellformed_C with the rest of the max_armKSGICVCPUNumListRegs interface?
There was a problem hiding this comment.
I was trying to make it this one not too available, because I want to discourage its use. I'd usually have made it a have or something like that, but that doesn't work with schematics in the goal.
There was a problem hiding this comment.
Ah, that makes sense. Probably worth a comment then otherwise we'll move it when someone stumbles across it in the future and we've forgotten your intent.
| sint (word_of_nat n :: int_word) < int max_armKSGICVCPUNumListRegs" | ||
| by (simp add: max_armKSGICVCPUNumListRegs_val int_eq_sint) | ||
|
|
||
| (* needs "simp del: of_nat_add", because of rhs *) |
There was a problem hiding this comment.
This should maybe say (* needs "simp del: of_nat_add" when used, because of rhs *). I was confused when I first read it and there wasn't a simp del immediately visible.
config_ARM_GIC_V3visible to the proofs (cherry-pick from SGI PR Proofs for SGI API #733)virqbit positions and widthsmax_armKSGICVCPUNumListRegs(changes with GIC version)virqaccess proofsvcpu_ttype size in C (changes with GIC version, because number of LR registers changes)This PR enables the functional correctness proof on all remaining AArch64 platforms.
Test with: seL4/seL4#1337