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

riscv crefine: introduce registers_count type abbrev 

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Rafal Kolanski 2020-04-17 03:01:31 +10:00 committed by Gerwin Klein
parent 70ee5750f6
commit e9e562c33d
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -233,7 +233,7 @@ fun
| "register_from_H RISCV64.NextIP = scast Kernel_C.NextIP" | "register_from_H RISCV64.NextIP = scast Kernel_C.NextIP"
definition definition
cregs_relation :: "(MachineTypes.register \<Rightarrow> machine_word) \<Rightarrow> machine_word[35] \<Rightarrow> bool" cregs_relation :: "(MachineTypes.register \<Rightarrow> machine_word) \<Rightarrow> machine_word[registers_count] \<Rightarrow> bool"
where where
"cregs_relation Hregs Cregs \<equiv> \<forall>r. Hregs r = Cregs.[unat (register_from_H r)]" "cregs_relation Hregs Cregs \<equiv> \<forall>r. Hregs r = Cregs.[unat (register_from_H r)]"

3
proof/crefine/RISCV64/Wellformed_C.thy
View File

@ -39,7 +39,8 @@ abbreviation
pt_Ptr :: "machine_word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr" pt_Ptr :: "machine_word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr"
type_synonym tcb_cnode_array = "cte_C[5]" type_synonym tcb_cnode_array = "cte_C[5]"
type_synonym registers_array = "machine_word[35]" type_synonym registers_count = 35
type_synonym registers_array = "machine_word[registers_count]"
abbreviation "user_context_Ptr \<equiv> Ptr :: addr \<Rightarrow> user_context_C ptr" abbreviation "user_context_Ptr \<equiv> Ptr :: addr \<Rightarrow> user_context_C ptr"
abbreviation "machine_word_Ptr \<equiv> Ptr :: addr \<Rightarrow> machine_word ptr" abbreviation "machine_word_Ptr \<equiv> Ptr :: addr \<Rightarrow> machine_word ptr"