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

riscv: rename sbadaddr -> stval 

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2020-08-26 15:19:05 +10:00 committed by Matthew Brecknell
parent 6f23d50ea9
commit b77f83c57b
13 changed files with 28 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proof/crefine/RISCV64/Machine_C.thy
View File

@ -27,10 +27,10 @@ assumes hwASIDFlush_ccorres:
(doMachineOp (RISCV64.hwASIDFlush asid))
(Call hwASIDFlush_'proc)"
assumes read_sbadaddr_ccorres:
assumes read_stval_ccorres:
"ccorres (=) ret__unsigned_long_' \<top> UNIV []
(doMachineOp RISCV64.read_sbadaddr)
(Call read_sbadaddr_'proc)"
(doMachineOp RISCV64.read_stval)
(Call read_stval_'proc)"
assumes sfence_ccorres:
"ccorres dc xfdc \<top> UNIV []

2
proof/crefine/RISCV64/VSpace_C.thy
View File

@ -251,7 +251,7 @@ lemma handleVMFault_ccorres:
prefer 3 apply simp
apply (simp add: handleVMFault_def handleVMFault'_def liftE_bindE condition_const
ucast_ucast_mask bind_assoc)
apply (rule corres_split[OF _ read_sbadaddr_ccorres[ac]], drule sym, clarsimp)
apply (rule corres_split[OF _ read_stval_ccorres[ac]], drule sym, clarsimp)
apply (wpc; simp add: vm_fault_type_from_H_def vm_fault_defs_C
true_def false_def bind_assoc)
apply (rule returnVMFault_corres;

6
proof/invariant-abstract/RISCV64/ArchAcc_AI.thy
View File

@ -2918,9 +2918,9 @@ lemma user_getreg_inv[wp]:
apply (simp add: getRegister_def)
done
lemma dmo_read_sbadaddr_inv[wp]:
"do_machine_op read_sbadaddr \<lbrace>P\<rbrace>"
by (rule dmo_inv) (simp add: read_sbadaddr_def)
lemma dmo_read_stval_inv[wp]:
"do_machine_op read_stval \<lbrace>P\<rbrace>"
by (rule dmo_inv) (simp add: read_stval_def)
end

6
proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy
View File

@ -13,7 +13,7 @@ context Arch begin global_naming RISCV64
named_theorems EmptyFail_AI_assms
crunch_ignore (empty_fail)
(add: setVSpaceRoot_impl sfence_impl hwASIDFlush_impl read_sbadaddr resetTimer_impl sbadaddr_val
(add: setVSpaceRoot_impl sfence_impl hwASIDFlush_impl read_stval resetTimer_impl stval_val
pt_lookup_from_level setIRQTrigger_impl plic_complete_claim_impl)
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
@ -166,8 +166,8 @@ global_interpretation EmptyFail_AI_schedule?: EmptyFail_AI_schedule
context Arch begin global_naming RISCV64
crunch (empty_fail) empty_fail[wp]: read_sbadaddr
(ignore_del: read_sbadaddr)
crunch (empty_fail) empty_fail[wp]: read_stval
(ignore_del: read_stval)
lemma plic_complete_claim_empty_fail[wp, EmptyFail_AI_assms]:
"empty_fail (plic_complete_claim irq)"

2
proof/invariant-abstract/RISCV64/ArchSyscall_AI.thy
View File

@ -52,7 +52,7 @@ lemma eq_no_cap_to_obj_with_diff_ref [Syscall_AI_assms]:
lemma hv_invs[wp, Syscall_AI_assms]: "\<lbrace>invs\<rbrace> handle_vm_fault t' flt \<lbrace>\<lambda>r. invs\<rbrace>"
unfolding handle_vm_fault_def by (cases flt; wpsimp)
crunch inv[wp]: getRegister, read_sbadaddr "P"
crunch inv[wp]: getRegister, read_stval "P"
(ignore_del: getRegister)
lemma hv_inv_ex [Syscall_AI_assms]:

4
proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy
View File

@ -933,11 +933,11 @@ lemma is_final_cap_caps_of_state_2D:
prod_eqI)
done
crunch underlying_memory[wp]: ackInterrupt, hwASIDFlush, read_sbadaddr, setVSpaceRoot, sfence
crunch underlying_memory[wp]: ackInterrupt, hwASIDFlush, read_stval, setVSpaceRoot, sfence
"\<lambda>m'. underlying_memory m' p = um"
(simp: cache_machine_op_defs machine_op_lift_def machine_rest_lift_def split_def)
crunches storeWord, ackInterrupt, hwASIDFlush, read_sbadaddr, setVSpaceRoot, sfence
crunches storeWord, ackInterrupt, hwASIDFlush, read_stval, setVSpaceRoot, sfence
for device_state_inv[wp]: "\<lambda>ms. P (device_state ms)"
(simp: crunch_simps)

6
proof/refine/RISCV64/Syscall_R.thy
View File

@ -1637,10 +1637,10 @@ lemma hy_invs':
apply (simp add:ct_active_runnable'[unfolded ct_in_state'_def])
done
lemma dmo_read_sbadaddr[wp]:
"doMachineOp read_sbadaddr \<lbrace>invs'\<rbrace>"
lemma dmo_read_stval[wp]:
"doMachineOp read_stval \<lbrace>invs'\<rbrace>"
apply (wp dmo_invs')
apply (clarsimp simp: in_monad read_sbadaddr_def)
apply (clarsimp simp: in_monad read_stval_def)
done
lemma hv_invs'[wp]: "\<lbrace>invs' and tcb_at' t'\<rbrace> handleVMFault t' vptr \<lbrace>\<lambda>r. invs'\<rbrace>"

8
proof/refine/RISCV64/VSpace_R.thy
View File

@ -52,9 +52,9 @@ lemma asidBits_asid_bits[simp]:
"asidBits = asid_bits"
by (simp add: bit_simps' asid_bits_def asidBits_def)
lemma no_fail_read_sbadaddr[intro!,simp]:
"no_fail \<top> read_sbadaddr"
by (simp add: read_sbadaddr_def)
lemma no_fail_read_stval[intro!,simp]:
"no_fail \<top> read_stval"
by (simp add: read_stval_def)
lemma hv_corres:
"corres (fr \<oplus> dc) (tcb_at thread) (tcb_at' thread)
@ -66,7 +66,7 @@ lemma hv_corres:
apply simp
apply (rule corres_machine_op[where r="(=)"])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_read_sbadaddr)
apply (rule no_fail_read_stval)
apply wpsimp+
done

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

@ -63,7 +63,7 @@ text \<open>
definition handle_vm_fault :: "obj_ref \<Rightarrow> vmfault_type \<Rightarrow> (unit,'z::state_ext) f_monad"
where
"handle_vm_fault thread fault_type = doE
addr \<leftarrow> liftE $ do_machine_op read_sbadaddr;
addr \<leftarrow> liftE $ do_machine_op read_stval;
let
loadf = (\<lambda>a. throwError $ ArchFault $ VMFault a [0, vmFaultTypeFSR RISCVLoadAccessFault]);
storef = (\<lambda>a. throwError $ ArchFault $ VMFault a [0, vmFaultTypeFSR RISCVStoreAccessFault]);

2
spec/design/skel/RISCV64/Hardware_H.thy
View File

@ -12,7 +12,7 @@ begin
context Arch begin global_naming RISCV64_H
#INCLUDE_HASKELL SEL4/Machine/Hardware/RISCV64.hs Platform=Platform.RISCV64 CONTEXT RISCV64_H NOT plic_complete_claim getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory setHardwareASID wordFromPDE wordFromPTE VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize toPAddr addrFromPPtr ptrFromPAddr sfence physBase ptTranslationBits vmFaultTypeFSR read_sbadaddr setVSpaceRoot hwASIDFlush setIRQTrigger
#INCLUDE_HASKELL SEL4/Machine/Hardware/RISCV64.hs Platform=Platform.RISCV64 CONTEXT RISCV64_H NOT plic_complete_claim getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory setHardwareASID wordFromPDE wordFromPTE VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize toPAddr addrFromPPtr ptrFromPAddr sfence physBase ptTranslationBits vmFaultTypeFSR read_stval setVSpaceRoot hwASIDFlush setIRQTrigger
end

2
spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs
View File

@ -165,7 +165,7 @@ lookupPTSlot = lookupPTSlotFromLevel maxPTLevel
handleVMFault :: PPtr TCB -> VMFaultType -> KernelF Fault ()
handleVMFault thread f = do
w <- withoutFailure $ doMachineOp read_sbadaddr
w <- withoutFailure $ doMachineOp read_stval
let addr = VPtr w
case f of
RISCVLoadPageFault -> throw $ loadf addr

4
spec/haskell/src/SEL4/Machine/Hardware/RISCV64.hs
View File

@ -306,8 +306,8 @@ maskInterrupt maskI irq = do
debugPrint :: String -> MachineMonad ()
debugPrint str = liftIO $ putStrLn str
read_sbadaddr :: MachineMonad Word
read_sbadaddr = error "Unimplemented - machine op"
read_stval :: MachineMonad Word
read_stval = error "Unimplemented - machine op"
plic_complete_claim :: IRQ -> MachineMonad ()
plic_complete_claim = error "Unimplemented - machine op"

6
spec/machine/RISCV64/MachineOps.thy
View File

@ -237,10 +237,10 @@ lemmas cache_machine_op_defs = sfence_def hwASIDFlush_def
subsection "Faults"
consts' sbadaddr_val :: "machine_state \<Rightarrow> machine_word"
definition read_sbadaddr :: "machine_word machine_monad"
consts' stval_val :: "machine_state \<Rightarrow> machine_word"
definition read_stval :: "machine_word machine_monad"
where
"read_sbadaddr = gets sbadaddr_val"
"read_stval = gets stval_val"
subsection "Virtual Memory"