Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

make proofs generic in maxIRQ and irq bit width #773

Merged
merged 18 commits into from
Jul 8, 2024
Merged

make proofs generic in maxIRQ and irq bit width #773

merged 18 commits into from
Jul 8, 2024

Conversation

lsf37
Copy link
Member

@lsf37 lsf37 commented Jul 5, 2024

  • clear up ancient irqInvalid encoding confusion
  • extract maxIRQ and irq_len from kernel config
  • use config maxIRQ and irq_len consistently in specs
  • adapt proofs to use the config value and not unfold it. This has different impact on different architectures:
    • on AARCH64, it was mostly avoiding unfoldings
    • on ARM and ARM_HYP, there is a lot of cleanup of magic numbers, using the right constants, adjusting types (the irq type had the wrong size, too big -- harmless but weaker), and avoiding unfolding. Correcting the type size required a new invariant on ARM_HYP in CRefine (but not on ARM). On AARCH64 that invariant was initially avoided, because we had changed the bitfield width of VPPIEvent IRQs in CRefine, but it turns out there are AARCH64 platforms with 8 bit IRQ width, so we have it there as well now.
    • no genericity on RISCV64 and X64, but at least reducing magic numbers a little bit
  • Word_Lib + Lib additions for the above

@lsf37 lsf37 added Aarch64 AArch64-specific proofs, specs, etc proof engineering nicer, shorter, more maintainable etc proofs labels Jul 5, 2024
@lsf37 lsf37 marked this pull request as ready for review July 5, 2024 00:50
@lsf37 lsf37 requested review from Xaphiosis and corlewis July 5, 2024 00:52
@lsf37 lsf37 self-assigned this Jul 5, 2024
@lsf37 lsf37 mentioned this pull request Jul 5, 2024
Merged
lsf37 added 18 commits July 5, 2024 18:02
@lsf37
aarch64 machine+crefine: clear up irqInvalid confusion
bed780f 
- getActiveIRQ in machine/ was trying to ensure that we're not returning
  "Some Kernel_C.irqInvalid", but it was using the wrong value (0xFF),
  and Kernel_C.irqInvalid is not representable in the type getActiveIRQ
  returns, so nothing needs to be done here.

  This is a remnant of old ARM 32 bit proofs were irqInvalid was 0xFF.
  Even in those times, it would not have been needed, because on
  platforms that use 0xFF, we already know maxIRQ < 0xFF.

- remove the lemmas in CRefine that were trying to make use of that
  obsolete check. It is obvious by type (and by simp) that
  Kernel_C.irqInvalid can't be returned, so none of them are needed
  on gic_v2/gic_v3 platforms.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
arm machine+proof: treat irqInvalid abstractly
3795ee5 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
arm-hyp machine+proof: treat irqInvalid abstractly
9a568b5 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
word_lib: lemma on toEnum (ucast _)
46170b5 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
word_lib: more lemmas about mask
7daf753 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
lib: add variation on mod_less_eq_dividend
973bc91 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
cspec: remove duplicate keys in gen-config-thy.py
a7001e5 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
cspec: extract maxIRQ definition from platform_gen.h
380f108 
For Arm platforms (32 and 64), maxIRQ is defined in platform_gen.h as
an explicit number. Parse this number and emit in Kernel_Config.thy.

For X64, the value is fixed and does not need to be generated.

For RISCV64, the value is computed (by virtue of being the last constant
in the enum) and extraction is more complex. Leaving it unimplemented
for now.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
arm+arm-hyp+aarch64 spec: use maxIRQ from Kernel_Config
b3f1326 
Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
cspec: extract irqBits from platform_gen.h
cfa2c2c 
Extract the value of IRQ_CNODE_SLOT_BITS into Kernel_Config.irqBits,
for later use in value_type to define irq_len and the irq type.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
machine+design: use irqBits for ASpec irq type
4840ea4 
Define irq_len and the irq type in terms of Kernel_Config.irqBits for
Arm and RISC-V platforms (fixed on X64). Use that type in ASpec via
machine/L4V_ARCH/Platform.thy.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
machine: make int_word available on all arches
5f3ddd5 
Consistently make `int_word` available on all architectures for the word
type that corresponds to a plain `int` in C for that architecture. All
unadorned C numerals are of this type.

This name can now be used generically in the rest of the proofs.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
aarch64 machine+ainvs+refine+crefine: make proofs generic in maxIRQ
2b6b02f 
- Kernel_Config lemmas for maxIRQ
- remove all unfoldings of maxIRQ_def
- use Arch_Kernel_Config lemmas for maxIRQ for array guards and other
  proof obligations.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
arm+arm-hyp machine+proof: make proofs generic in maxIRQ
65c25df 
- add Kernel_Config lemmas for maxIRQ
- use irq and irq_len types instead of magic type numbers
- use Kernel_Config.maxIRQ where possible instead of numbers
- avoid unfoldings of Kernel_Config.maxIRQ and Kernel_C.maxIRQ

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
x64 machine+crefine: reduce magic numbers
1a44075 
Give names to irq bith width, size of IRQ array, and size of interrupt
state array. Since there is no Kernel_Config.maxIRQ on X64, use
Kernel_C.maxIRQ where necessary.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
riscv crefine: reduce magic numbers
37e0bdd 
Define size of IRQ array and interrupt state array symbolically.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
aarch64 crefine: make proof generic in irq type size
13e6d82 
It turns out that there are platforms with 8-bit wide IRQ types on
AArch64. This means we need the same kind of invariant for VPPIEvent
fault here as we have in ARM_HYP, saying that VPPIEvent only stores IRQs
up to the IRQ bit width, even though the C declares a potentially wider
type.

Signed-off-by: Gerwin Klein <[email protected]>
@lsf37
proof/Makefile: declare InfoFlowCBase dependencies
4a9a6c6 
Signed-off-by: Gerwin Klein <[email protected]>
Xaphiosis
Xaphiosis approved these changes Jul 8, 2024
View reviewed changes
Copy link
Member

@Xaphiosis Xaphiosis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be fine now. Cheers

@lsf37 lsf37 merged commit 4a9a6c6 into master Jul 8, 2024
14 checks passed
@lsf37 lsf37 deleted the maxIRQ branch July 8, 2024 00:58
corlewis
corlewis reviewed Jul 8, 2024
View reviewed changes
Copy link
Member

@corlewis corlewis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the late comments, but here's a few very minor things that I had found.

There's also a typo in the first commit message, in the second paragraph were should be where.

proof/crefine/ARM/Finalise_C.thy Show resolved Hide resolved
proof/crefine/ARM_HYP/Finalise_C.thy Show resolved Hide resolved
proof/crefine/ARM/Refine_C.thy Show resolved Hide resolved
spec/abstract/X64/ArchInterrupt_A.thy Show resolved Hide resolved
spec/design/skel/AARCH64/ArchInterrupt_H.thy Show resolved Hide resolved
@lsf37 lsf37 mentioned this pull request Jul 11, 2024
Merged
@lsf37 lsf37 added the platforms making proofs generic in platform and config settings label Jul 12, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@corlewis corlewis corlewis left review comments

@Xaphiosis Xaphiosis Xaphiosis approved these changes

Assignees

@lsf37 lsf37

Labels
Aarch64 AArch64-specific proofs, specs, etc platforms making proofs generic in platform and config settings proof engineering nicer, shorter, more maintainable etc proofs
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@lsf37 @Xaphiosis @corlewis