9de5bb27e4
aspec: factor out arch_mask_irq_signal
...
On RISC-V we do not call mask_irq.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
2e2d4c279d
riscv crefine: clear last sorry in Interrupt_C
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
0bdec8a194
riscv refine: adjust proofs to new invokeIRQHandler
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
fe566628da
haskell+design: factor out arch specific IRQ handling
...
RISC-V has a different machine op invocation for acknowledging IRQs.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
a33df75acb
riscv ainvs: update for invokeIRQHandler arch split spec change
...
Add appropriate lemmas for machine op plic_complete_claim.
Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>
2020-06-08 20:41:10 +08:00
461a798412
aspec: arch split on invokeIRQHandler
...
The RISCV implementation of invokeIRQHandler calls plic_complete_claim
instead of maskInterrupt. plicCompleteClaim is added as a machine op
and invokeIRQHandler has been arch split for the ACKIrq case.
Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>
2020-06-08 20:41:10 +08:00
877c667877
riscv crefine: Arch_C sorry-free
...
Completed decodeRISCVFrameInvocation_ccorres, synced with C changes and
cleaned up a little.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
06d6620340
riscv haskell: update vmRightsToBits
...
This was incorrect, but unused in the proofs. Once used, the numbers
turned out to be unrelated to the C.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
b7e9f610d9
riscv crefine: prove decodeRISCVMMUInvocation_ccorres
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
bf753fc564
riscv crefine: clear last sorry in Finalise_C
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
8e60a9af3e
riscv refine: prove new lookupPTFromLevel assertion
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
100f8ed949
riscv haskell+design: new assertion in lookupPTFromLevel
...
The corresponding C code (correctly) expects never to be called for a
top-level table.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
e8f9a341d8
riscv crefine: clear 3 sorries from Arch_C
...
Notably, decodeRISCVPageTableInvocation_ccorres is done.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
75e82bc006
riscv crefine: prove Arch_decodeIRQControlInvocation_ccorres
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
d8b64d4eb2
riscv crefine: prove decodeIRQControlInvocation_ccorres
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
d7fb06cac1
riscv crefine: prove Arch_finaliseCap_ccorres
...
Also modifies cap_to_H_PTCap to include capPTMappedAddress
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
aadf599ae5
riscv crefine: remove 1 sorry from Interrupt_C
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
b17b03befc
riscv crefine: clear remaining sorry in Ipc_C
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
e8ad7ddb72
riscv crefine: clear last sorry in Delete_C
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
4bc86adab1
riscv crefine: clear final sorry in Arch_C
...
This includes a slight tweak to the state relation for global PTs.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
fe21162804
riscv crefine: clear all sorries in VSpace_C
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
6eff34f312
riscv crefine: restrict abstract pools in casid_pool_relation
...
Since on RISCV64 we do not have restrictions on arch objects in
valid_obj', for the state relation to form a function from abstract to
concrete, we need to restrict the domains of the abstract asid pools.
Further we also need to ensure ASID 0 is not used in any of them, as
that is a sentinel value for "no ASID".
This is analogous to the restriction placed by valid_obj' on ASIDs on
X64, except occurring in the state relation rather than an invariant.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
0a397f626e
riscv crefine: reduce sorries in ADT_C
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
5f1fd9aa64
riscv crefine: clear sorries from Refine_C
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
2eeaae4017
riscv crefine: fix fault_to_H for VMFault
...
Arguments were backwards for some reason.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
39be004a1a
riscv crefine: sorry Refine_C
...
No examination of failing proofs this time. All CRefine files are now
present and accounted for.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
4bae495aa4
riscv crefine: sorried, very preliminary ADT_C
...
Broken bits blindly sorried or commented out with FIXME RISCV.
carch_state_to_H is currently wrong as valid_arch_state' is
insufficient to accurately describe global page tables.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
3775796809
riscv crefine: Init_C
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
1b92a83c01
riscv crefine: Syscall_C with a sorry needing spec update
...
On RISCV, we do not mask the interrupt on IRQSignal in handleInterrupt.
Spec currently masks this, so we provide the sorried intended spec
definition of handleInterrupt for the time being.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
6b3ae48b96
riscv crefine: Schedule_C
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
073db1c960
riscv crefine: Tcb_C
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
f9c1082a8b
riscv crefine: Arch_C: update for C changes
...
Make a bit more progress after merging fixes for decode/invoke model
violation, and missing page table cap type check.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
9b1291556e
riscv crefine: sorry Arch_C
...
There are sorries waiting on C updates, a few large sorries, and several
chunks of commented-out X64 proofs that may need to be adapted to
address the other sorries.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:10 +08:00
a29822c44e
riscv crefine: proof update for potential InvalidPTE mapping
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
ae3358cc2f
riscv crefine: prove lookupPTSlot_corres
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
9d00b566d7
riscv crefine: adjust cpte_relation for new pte invariant
...
cpte_relation now encodes that PagePTEs can't have 000 rwx rights.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:10 +08:00
4ecd369a2d
riscv refine: adjust proof for modified assertions
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
6b78e37cec
riscv design+haskell: move pt_at assertions to the recursive call
...
The proof needs to know that there is a page table at the entry
point in the induction for lookupPTSlot. Moving the assertion just
before the recursive call establishes this directly.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
8e4cc14c55
riscv refine: update proof for potential InvalidPTE mappings
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
1b4c6ba987
riscv ainvs: update AInvs for potential InvalidPTE mappings
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
9bd06da4d7
riscv aspec+haskell: make mapped PTE invalid for insufficient rights
...
The RISC-V ISA spec does not allow PagePTEs with 000 for rwx rights,
because 000 is used to identify PageTablePTEs. Instead we write
InvalidPTEs, which has the same effect for the user.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
1dccd9ceaf
riscv aspec: update arch API type decoding to new order
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
bdea44614d
riscv crefine: clear Invoke_C sorries
...
Use the previous Haskell changes and asserts to clear the remaining
sorries in Invoke_C.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
42c505c94a
riscv crefine: adjust proofs to new api-object order
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
14206e2536
riscv refine: prove new Haskell assertions
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
7b9249fe2a
riscv design: port new asserts into design spec
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
fca56f750b
riscv haskell: additional assertions for CRefine
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
6be8b794ec
riscv haskell: sync order with C enum
...
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
2020-06-08 20:41:09 +08:00
e650f39de3
riscv crefine: update for C setIRQTrigger changes
...
Update machine op assumption and remove Arch_invokeIRQControl_ccorres sorry.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:09 +08:00
0ee70f00a5
riscv crefine: clear 3 sorries in Invoke_C
...
Resolved via C changes.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
2020-06-08 20:41:09 +08:00
Gerwin Klein
Victor Phan
Rafal Kolanski