riscv machine: style
This commit is contained in:
parent
aa510dbb93
commit
a84b7c624e
|
@ -63,16 +63,22 @@ lemma loadWord_storeWord_is_return:
|
||||||
modify_def gets_def get_def eval_nat_numeral put_def upto0_7_def
|
modify_def gets_def get_def eval_nat_numeral put_def upto0_7_def
|
||||||
word_rsplit_rcat_size word_size)
|
word_rsplit_rcat_size word_size)
|
||||||
|
|
||||||
|
consts'
|
||||||
|
memory_regions :: "(paddr \<times> paddr) list"
|
||||||
|
definition
|
||||||
|
getMemoryRegions :: "(paddr * paddr) list machine_monad"
|
||||||
|
where
|
||||||
|
"getMemoryRegions \<equiv> return memory_regions"
|
||||||
|
|
||||||
text {* This instruction is required in the simulator, only. *}
|
text {* This instruction is required in the simulator, only. *}
|
||||||
definition
|
definition
|
||||||
storeWordVM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
storeWordVM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||||
where "storeWordVM w p \<equiv> return ()"
|
where
|
||||||
|
"storeWordVM w p \<equiv> return ()"
|
||||||
|
|
||||||
consts'
|
consts'
|
||||||
configureTimer_impl :: "unit machine_rest_monad"
|
configureTimer_impl :: "unit machine_rest_monad"
|
||||||
configureTimer_val :: "machine_state \<Rightarrow> irq"
|
configureTimer_val :: "machine_state \<Rightarrow> irq"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
configureTimer :: "irq machine_monad"
|
configureTimer :: "irq machine_monad"
|
||||||
where
|
where
|
||||||
|
@ -150,12 +156,13 @@ section "Memory Clearance"
|
||||||
text {* Clear memory contents to recycle it as user memory *}
|
text {* Clear memory contents to recycle it as user memory *}
|
||||||
definition
|
definition
|
||||||
clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||||
where
|
where
|
||||||
"clearMemory ptr bytelength \<equiv> mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1]"
|
"clearMemory ptr bytelength \<equiv>
|
||||||
|
mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1]"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||||
where
|
where
|
||||||
"clearMemoryVM ptr bits \<equiv> return ()"
|
"clearMemoryVM ptr bits \<equiv> return ()"
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
@ -176,9 +183,9 @@ text {*
|
||||||
*}
|
*}
|
||||||
definition
|
definition
|
||||||
freeMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
freeMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||||
where
|
where
|
||||||
"freeMemory ptr bits \<equiv>
|
"freeMemory ptr bits \<equiv>
|
||||||
mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + 2 ^ bits - 1]"
|
mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + 2 ^ bits - 1]"
|
||||||
|
|
||||||
|
|
||||||
section "User Monad"
|
section "User Monad"
|
||||||
|
@ -195,6 +202,8 @@ where
|
||||||
"getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
|
"getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
modify_registers :: "(user_regs \<Rightarrow> user_regs) \<Rightarrow> user_context \<Rightarrow> user_context"
|
||||||
|
where
|
||||||
"modify_registers f uc \<equiv> UserContext (f (user_regs uc))"
|
"modify_registers f uc \<equiv> UserContext (f (user_regs uc))"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
|
Loading…
Reference in New Issue