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

riscv aspec: fail not too early in lookup_pt_slot_from_level

This commit is contained in:
Gerwin Klein 2018-11-09 19:37:55 +11:00 committed by Rafal Kolanski
parent e2e68953ae
commit 0b8af8800c
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
spec/abstract/RISCV64/ArchVSpaceAcc_A.thy
View File

@ -156,10 +156,14 @@ fun lookup_pt_slot_from_level ::
where
"lookup_pt_slot_from_level level bot_level pt_ptr vptr = do {
let slot = pt_slot_index level pt_ptr vptr;
pte \<leftarrow> oapply slot;
if is_PageTablePTE pte \<and> level > bot_level
then lookup_pt_slot_from_level (level - 1) bot_level (pptr_from_pte pte) vptr
else oreturn (level, slot)
if \<not>(bot_level < level)
then oreturn (level, slot)
else do {
pte \<leftarrow> oapply slot;
if is_PageTablePTE pte
then lookup_pt_slot_from_level (level - 1) bot_level (pptr_from_pte pte) vptr
else oreturn (level, slot)
}
}"
declare lookup_pt_slot_from_level.simps[simp del]