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

riscv aspec bugfix: need to check vaddr alignment for PT-map

This commit is contained in:
Gerwin Klein 2019-05-09 14:26:43 +10:00 committed by Rafal Kolanski
parent e77f11da9e
commit 519b672d08
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -160,6 +160,7 @@ definition decode_pt_inv_map :: "'z::state_ext arch_decoder"
(level, slot) \<leftarrow> liftE $ gets_the $ pt_lookup_slot pt vaddr \<circ> ptes_of;
old_pte \<leftarrow> liftE $ get_pte slot;
whenE (pt_bits_left level = pageBits \<or> old_pte \<noteq> InvalidPTE) $ throwError DeleteFirst;
unlessE (is_aligned vaddr (pt_bits_left level)) $ throwError AlignmentError;
pte \<leftarrow> returnOk $ PageTablePTE (ucast (addrFromPPtr p >> pageBits)) {};
cap' <- returnOk $ PageTableCap p $ Some (asid, vaddr);
returnOk $ InvokePageTable $ PageTableMap cap' cte pte slot