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

riscv crefine: sync frame PTE rights with C updates 

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Rafal Kolanski 2020-04-11 01:55:29 +10:00 committed by Gerwin Klein
parent 7bec00882e
commit 3a2bfe5a93
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -392,7 +392,13 @@ definition
definition
"writable_from_vm_rights R \<equiv> case R of
VMReadOnly \<Rightarrow> 0
VMReadWrite \<Rightarrow> 1
| _ \<Rightarrow> 0"
(* kernel-only conveys no *)
definition
"readable_from_vm_rights R \<equiv> case R of
VMKernelOnly \<Rightarrow> 0
| _ \<Rightarrow> 1"
(* if RWX are all 0, then the pte is a pointer to the next level page table *)
@ -421,10 +427,10 @@ where
pte_CL.dirty_CL = 1,
pte_CL.accessed_CL = 1,
pte_CL.global_CL = of_bool global,
pte_CL.user_CL = user_from_vm_rights rights, \<comment> \<open>FIXME RISCV user seems redundant for page ptes\<close>
pte_CL.user_CL = user_from_vm_rights rights,
pte_CL.execute_CL = of_bool execute,
pte_CL.write_CL = writable_from_vm_rights rights,
pte_CL.read_CL = undefined,
pte_CL.read_CL = readable_from_vm_rights rights,
pte_CL.valid_CL = 1 \<rparr>
| PageTablePTE ppn global user \<Rightarrow>
cpte' = \<lparr>