-
Notifications
You must be signed in to change notification settings - Fork 105
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.
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
Proofs for SGI API #733
base: master
Are you sure you want to change the base?
Proofs for SGI API #733
Commits on Mar 26, 2024
-
cspec: explain why config keys are renamed
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for c5d88c7 - Browse repository at this point
Copy the full SHA c5d88c7View commit details -
cspec: make config_ARM_GIC_V3 config visible to proofs
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]>
Configuration menu - View commit details
-
Copy full SHA for 32a8990 - Browse repository at this point
Copy the full SHA 32a8990View commit details -
aarch64 machine: add ipiSendTarget machine op
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for b6943d5 - Browse repository at this point
Copy the full SHA b6943d5View commit details -
This affects all architectures, because generic interfaces are changing, but the SGISignalCap API is only added to ARM, ARM_HYP, and AARCH64. For X64 and RISCV64, we trivially implement the new interfaces, and in generic code we call those interfaces. These new interfaces are isArchMDBParentOf and isIRQControlCapDescendant, for checking in generic code if there are architecture specific cases in isMDBParentOf and isCapRevocable respectively. Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 5e0b269 - Browse repository at this point
Copy the full SHA 5e0b269View commit details -
arm+arm-hyp+aarch64 machine: IPI + SGI machine interface
Define the new constants numSGIs and gicSGITargetMaskBits, plus a new machine operation ipiSendTarget. Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for f54f8aa - Browse repository at this point
Copy the full SHA f54f8aaView commit details -
design+haskell-translator: add new arch interfaces and caseconvs
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for c75b9f8 - Browse repository at this point
Copy the full SHA c75b9f8View commit details -
aspec: add SGISignalCap API + cdt interfaces
- add SGISignalCap API for ARM, ARM_HYP, AARCH64 - add generic interface for should_be_arch_parent_of and is_irq_control_descendant in the cdt implementation - add default interface implementations new interfaces for RISCV64, X64 Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 5d1ef38 - Browse repository at this point
Copy the full SHA 5d1ef38View commit details -
x64+riscv ainvs: adjust for new CDT interface
This contains a slight tweak to generic CSpace_AI and proof adjustments for the architectures that do not implement the SGISignalCap API. Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 7a1a026 - Browse repository at this point
Copy the full SHA 7a1a026View commit details -
arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for b4bd110 - Browse repository at this point
Copy the full SHA b4bd110View commit details -
x64+riscv refine: CDT interface update
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for bd4e95b - Browse repository at this point
Copy the full SHA bd4e95bView commit details -
arm+arm-hyp+aarch64: SGISignalCap proofs
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 1670481 - Browse repository at this point
Copy the full SHA 1670481View commit details -
x64+riscv crefine: CTD interface updates
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 6b9a2ab - Browse repository at this point
Copy the full SHA 6b9a2abView commit details -
arm+arm-hyp+aarch64: SGISignalCap proofs
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 05d4e36 - Browse repository at this point
Copy the full SHA 05d4e36View commit details -
arm access+infoflow: SGISignalCap security thms
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 961e607 - Browse repository at this point
Copy the full SHA 961e607View commit details -
capDL: add SGISignalCap API to capDL
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for bb2d6e6 - Browse repository at this point
Copy the full SHA bb2d6e6View commit details -
drefine+dpolicy: SGISignalCap proofs
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 0144f61 - Browse repository at this point
Copy the full SHA 0144f61View commit details -
capDL: SGISignalCap API for SepDSpec and DSpecProofs
Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 9116b66 - Browse repository at this point
Copy the full SHA 9116b66View commit details -
sys-init: exclude SGISignalCap
For now exclude SGISignalCap from wellformed specs. To be relaxed later. Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 3f971a8 - Browse repository at this point
Copy the full SHA 3f971a8View commit details -
Fix + modernise style and proofs. Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 6d1df8d - Browse repository at this point
Copy the full SHA 6d1df8dView commit details -
capDL-api: seplogic lemmas for ARMIssueSGISignal
Add separation logic specification lemmas for the new SGISignalCap API for later use in sys-init. Signed-off-by: Gerwin Klein <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for dc2fd26 - Browse repository at this point
Copy the full SHA dc2fd26View commit details