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

arm-hyp abstract: set asid_high_bits for non-SMMU platform 

Should be 7, had 6.
This commit is contained in:
Rafal Kolanski 2017-04-06 02:10:39 +10:00 committed by Alejandro Gomez-Londono
parent 8aacdd5d56
commit 6f2b32dba2
3 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy
View File

@ -31,7 +31,7 @@ section "Encodings"
text {* The high bits of a virtual ASID. *}
definition
asid_high_bits_of :: "asid \<Rightarrow> 6 word" where
asid_high_bits_of :: "asid \<Rightarrow> 7 word" where
"asid_high_bits_of asid \<equiv> ucast (asid >> asid_low_bits)"

8
spec/abstract/ARM_HYP/Arch_Structs_A.thy
View File

@ -62,13 +62,13 @@ definition
definition
asid_high_bits :: nat where
"asid_high_bits \<equiv> 6"
"asid_high_bits \<equiv> 7"
definition
asid_low_bits :: nat where
"asid_low_bits \<equiv> 10 :: nat"
definition
asid_bits :: nat where
"asid_bits \<equiv> 16 :: nat"
"asid_bits \<equiv> 17 :: nat"
section {* Architecture-specific objects *}
@ -320,7 +320,7 @@ qualify ARM_A (in Arch)
text {* arch\_state *}
record arch_state =
arm_asid_table :: "6 word \<rightharpoonup> obj_ref"
arm_asid_table :: "7 word \<rightharpoonup> obj_ref"
arm_hwasid_table :: "ARM_A.hw_asid \<rightharpoonup> ARM_A.asid"
arm_next_asid :: ARM_A.hw_asid
arm_asid_map :: "ARM_A.asid \<rightharpoonup> (ARM_A.hw_asid \<times> obj_ref)"
@ -394,4 +394,4 @@ definition
end
end
end

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

@ -37,7 +37,7 @@ type_synonym data = machine_word
type_synonym cap_ref = "bool list"
type_synonym length_type = machine_word
type_synonym asid_pool_index = "10 word"
type_synonym asid_index = "6 word" (* FIXME: better name? *)
type_synonym asid_index = "7 word" (* FIXME: better name? *)
text {* With the definitions above, most conversions between abstract
type names boil down to just the identity function, some convert from