adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

riscv aspec: sync with C fix for SELFOUR-1955 

aspec now in sync with seL4 master@a39c9b6a76d279364e28d3415d750d7287fefd67
This commit is contained in:
Gerwin Klein 2019-03-15 09:48:34 +11:00 committed by Rafal Kolanski
parent decbdd9c17
commit bda33be6b9
1 changed files with 7 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
spec/abstract/RISCV64/ArchVSpace_A.thy
View File

@ -71,26 +71,15 @@ fun handle_vm_fault :: "obj_ref \<Rightarrow> vmfault_type \<Rightarrow> (unit,'
let
loadf = (\<lambda>a. throwError $ ArchFault $ VMFault a [0, vmFaultTypeFSR RISCVLoadAccessFault]);
storef = (\<lambda>a. throwError $ ArchFault $ VMFault a [0, vmFaultTypeFSR RISCVStoreAccessFault]);
instrf = (\<lambda>a. throwError $ ArchFault $ VMFault a [1, vmFaultTypeFSR RISCVInstructionAccessFault]);
set_pc = do
faultip \<leftarrow> as_user thread $ getRegister FaultIP;
as_user thread $ setRegister NextIP faultip
od
instrf = (\<lambda>a. throwError $ ArchFault $ VMFault a [1, vmFaultTypeFSR RISCVInstructionAccessFault])
in
case fault_type of
RISCVLoadPageFault \<Rightarrow> loadf addr
| RISCVLoadAccessFault \<Rightarrow> loadf addr
| RISCVStorePageFault \<Rightarrow> storef addr
| RISCVStoreAccessFault \<Rightarrow> storef addr
| RISCVInstructionPageFault \<Rightarrow> doE
liftE set_pc;
instrf addr
odE
| RISCVInstructionAccessFault \<Rightarrow> doE
liftE set_pc;
instrf addr
odE
| _ \<Rightarrow> fail (* FIXME RISCV: SELFOUR-1955 *)
RISCVLoadPageFault \<Rightarrow> loadf addr
| RISCVLoadAccessFault \<Rightarrow> loadf addr
| RISCVStorePageFault \<Rightarrow> storef addr
| RISCVStoreAccessFault \<Rightarrow> storef addr
| RISCVInstructionPageFault \<Rightarrow> instrf addr
| RISCVInstructionAccessFault \<Rightarrow> instrf addr
odE"
text \<open>