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

Commits on Jul 5, 2024

  1. aarch64 machine+crefine: clear up irqInvalid confusion 

    - 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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    bed780f View commit details
    Browse the repository at this point in the history

  2. arm machine+proof: treat irqInvalid abstractly 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    3795ee5 View commit details
    Browse the repository at this point in the history

  3. arm-hyp machine+proof: treat irqInvalid abstractly 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    9a568b5 View commit details
    Browse the repository at this point in the history

  4. word_lib: lemma on toEnum (ucast _) 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    46170b5 View commit details
    Browse the repository at this point in the history

  5. word_lib: more lemmas about mask 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    7daf753 View commit details
    Browse the repository at this point in the history

  6. lib: add variation on mod_less_eq_dividend 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    973bc91 View commit details
    Browse the repository at this point in the history

  7. cspec: remove duplicate keys in gen-config-thy.py 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    a7001e5 View commit details
    Browse the repository at this point in the history

  8. cspec: extract maxIRQ definition from platform_gen.h 

    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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    380f108 View commit details
    Browse the repository at this point in the history

  9. arm+arm-hyp+aarch64 spec: use maxIRQ from Kernel_Config 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    b3f1326 View commit details
    Browse the repository at this point in the history

  10. cspec: extract irqBits from platform_gen.h 

    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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    cfa2c2c View commit details
    Browse the repository at this point in the history

  11. machine+design: use irqBits for ASpec irq type 

    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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    4840ea4 View commit details
    Browse the repository at this point in the history

  12. machine: make int_word available on all arches 

    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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    5f3ddd5 View commit details
    Browse the repository at this point in the history

  13. aarch64 machine+ainvs+refine+crefine: make proofs generic in maxIRQ 

    - 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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    2b6b02f View commit details
    Browse the repository at this point in the history

  14. arm+arm-hyp machine+proof: make proofs generic in maxIRQ 

    - 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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    65c25df View commit details
    Browse the repository at this point in the history

  15. x64 machine+crefine: reduce magic numbers 

    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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    1a44075 View commit details
    Browse the repository at this point in the history

  16. riscv crefine: reduce magic numbers 

    Define size of IRQ array and interrupt state array symbolically.

Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    37e0bdd View commit details
    Browse the repository at this point in the history

  17. aarch64 crefine: make proof generic in irq type size 

    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
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    13e6d82 View commit details
    Browse the repository at this point in the history

  18. proof/Makefile: declare InfoFlowCBase dependencies 

    Signed-off-by: Gerwin Klein <[email protected]>
    @lsf37
    lsf37 committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    4a9a6c6 View commit details
    Browse the repository at this point in the history