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

riscv aspec: make decode case distinctions complete

This commit is contained in:
Gerwin Klein 2019-03-07 10:24:42 +11:00 committed by Rafal Kolanski
parent a37d867e66
commit c0b7d2fc83
1 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
spec/abstract/RISCV64/ArchDecode_A.thy
View File

@ -94,7 +94,8 @@ definition decode_fr_inv_map :: "'z::state_ext arch_decoder"
pte \<leftarrow> returnOk $ make_user_pte (addrFromPPtr p) attribs vm_rights;
returnOk $ InvokePage $ PageMap (FrameCap p R pgsz dev (Some (asid,vaddr))) cte (pte,slot)
odE
else throwError TruncatedMessage"
else throwError TruncatedMessage
| _ \<Rightarrow> fail"
definition decode_fr_inv_remap :: "'z::state_ext arch_decoder"
where
@ -123,7 +124,8 @@ definition decode_fr_inv_remap :: "'z::state_ext arch_decoder"
pte \<leftarrow> returnOk $ make_user_pte (addrFromPPtr p) (attribs_from_word attr) vm_rights;
returnOk $ InvokePage $ PageRemap (pte, slot)
odE
else throwError TruncatedMessage"
else throwError TruncatedMessage
| _ \<Rightarrow> fail"
definition decode_frame_invocation :: "'z::state_ext arch_decoder"
where
@ -162,7 +164,8 @@ definition decode_pt_inv_map :: "'z::state_ext arch_decoder"
cap' <- returnOk $ PageTableCap p $ Some (asid, vaddr);
returnOk $ InvokePageTable $ PageTableMap cap' cte pte slot
odE
else throwError TruncatedMessage"
else throwError TruncatedMessage
| _ \<Rightarrow> fail"
definition decode_page_table_invocation :: "'z::state_ext arch_decoder"
where