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

riscv aspec: constrain asid type to asid_len 

We previously had asids at machine word representation, but it turns out that
constraining them to actual asid_len is almost no overhead and saves us proving
invariants about asid sizes.
This commit is contained in:
Gerwin Klein 2019-04-23 09:16:00 +10:00 committed by Rafal Kolanski
parent bb7062c263
commit 116009c1d7
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/abstract/RISCV64/ArchVSpace_A.thy
View File

@ -95,7 +95,7 @@ definition set_vm_root :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
ArchObjectCap (PageTableCap pt (Some (asid, _))) \<Rightarrow> doE
pt' \<leftarrow> find_vspace_for_asid asid;
whenE (pt \<noteq> pt') $ throwError InvalidRoot;
liftE $ do_machine_op $ setVSpaceRoot pt asid
liftE $ do_machine_op $ setVSpaceRoot pt (ucast asid)
odE
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
@ -129,7 +129,7 @@ definition delete_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::st
| Some pool_ptr \<Rightarrow> do
pool \<leftarrow> get_asid_pool pool_ptr;
when (pool (asid_low_bits_of asid) = Some pt) $ do
do_machine_op $ hwASIDFlush asid;
do_machine_op $ hwASIDFlush (ucast asid);
pool' \<leftarrow> return $ pool (asid_low_bits_of asid := None);
set_asid_pool pool_ptr pool';
tcb \<leftarrow> gets cur_thread;

2
spec/abstract/RISCV64/Machine_A.thy
View File

@ -38,7 +38,7 @@ type_synonym asid_high_len = 7
type_synonym asid_high_index = "asid_high_len word"
type_synonym asid_len = 16
type_synonym asid_rep_len = machine_word_len
type_synonym asid_rep_len = asid_len
type_synonym asid = "asid_rep_len word"
text \<open>