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

x64: set cteRightsBits to 0 (VER-930)

This commit is contained in:
Michael Sproul 2018-05-07 15:32:01 +10:00 committed by Joel Beeren
parent df9c791a3f
commit c481c7d2df
4 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/invariant-abstract/X64/ArchIpc_AI.thy
View File

@ -33,7 +33,7 @@ lemma update_cap_data_closedform:
then NullCap
else CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits))
(to_bl g''))
((w >> 8) && mask 58))
((w >> 6) && mask 58))
| ThreadCap r \<Rightarrow> ThreadCap r
| DomainCap \<Rightarrow> DomainCap
| UntypedCap d p n idx \<Rightarrow> UntypedCap d p n idx

6
proof/refine/X64/CSpace1_R.thy
View File

@ -423,8 +423,8 @@ proof -
isCap_defs is_cap_defs Let_def badge_bits_def
cap_rights_update_def badge_update_def
{ fix x :: machine_word
def y \<equiv> "(x >> 8) && mask 58" (* guard_bits *)
def z \<equiv> "unat ((x >> 2) && mask 6)" (* cnode_padding_bits, cnode_guard_size_bits *)
def y \<equiv> "(x >> 6) && mask 58" (* guard_bits *)
def z \<equiv> "unat (x && mask 6)" (* cnode_guard_size_bits *)
have "of_bl (to_bl (y && mask z)) = (of_bl (replicate (64-z) False @ drop (64-z) (to_bl y))::machine_word)"
by (simp add: bl_and_mask)
then
@ -449,7 +449,7 @@ proof -
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
rightsFromWord_def data_to_rights_def nth_ucast cteRightsBits_def cteGuardBits_def)
apply (insert x)
apply (subgoal_tac "unat ((x >> 2) && mask 6) < unat (2^6::machine_word)")
apply (subgoal_tac "unat (x && mask 6) < unat (2^6::machine_word)")
prefer 2
apply (fold word_less_nat_alt)[1]
apply (rule and_mask_less_size)

2
spec/abstract/X64/ArchCSpace_A.thy
View File

@ -27,7 +27,7 @@ where
definition cnode_padding_bits :: "nat"
where
"cnode_padding_bits \<equiv> 2"
"cnode_padding_bits \<equiv> 0"
text {* On a user request to modify a cnode capability, extract new guard bits and guard. *}
definition

2
spec/haskell/src/SEL4/Object/ObjectType/X64.lhs
View File

@ -124,7 +124,7 @@ ASID capabilities can be copied without modification, as can IOPort and IOSpace
CNodes have differing numbers of guard bits and rights bits
> cteRightsBits :: Int
> cteRightsBits = 2
> cteRightsBits = 0
> cteGuardBits :: Int
> cteGuardBits = 58