Skip to content

Commit

Permalink
aarch64 machine+aspec+cspec: pt_type ghost+table array sizes
Browse files Browse the repository at this point in the history 
- add ghost state corresponding to gsPTTypes in Haskell and ASpec
- add ghost type comments
- style update for old definitions since we need to touch most of these
- define vs/pt_array_len for use in C annotations
- make NormalPT_T/VSRootPT_T names available for use in C annotations

Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
@lsf37
lsf37 committed Jan 15, 2024
1 parent afcbba9 commit 52b4ba5
Show file tree
Hide file tree
Showing 3 changed files with 110 additions and 71 deletions.
43 changes: 1 addition & 42 deletions spec/abstract/AARCH64/Arch_Structs_A.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,48 +113,7 @@ definition pte_base_addr :: "pte \<Rightarrow> paddr" where
definition ppn_from_pptr :: "obj_ref \<Rightarrow> ppn" where
"ppn_from_pptr p = ucast (addrFromPPtr p >> pageBits)"

definition vs_index_bits :: nat where
"vs_index_bits \<equiv> if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)"

lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits"
by (simp add: vs_index_bits_def)

(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can
retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain
number such as 9 or 10. *)
typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto

end

instantiation AARCH64_A.vs_index_len :: len0
begin
interpretation Arch .
definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \<equiv> CARD(vs_index_len)"
instance ..
end

instantiation AARCH64_A.vs_index_len :: len
begin
interpretation Arch .
instance
proof
show "0 < LENGTH(vs_index_len)"
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
qed
end

context Arch begin global_naming AARCH64_A

type_synonym vs_index = "vs_index_len word"

type_synonym pt_index_len = 9
type_synonym pt_index = "pt_index_len word"

text \<open>Sanity check:\<close>
lemma length_vs_index_len[simp]:
"LENGTH(vs_index_len) = vs_index_bits"
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])

(* Sanity check for page table type sizes -- ptTranslationBits not yet available at definition site *)
lemma vs_index_ptTranslationBits:
"ptTranslationBits VSRootPT_T = LENGTH(vs_index_len)"
by (simp add: ptTranslationBits_def vs_index_bits_def)
Expand Down
79 changes: 50 additions & 29 deletions spec/cspec/AARCH64/Kernel_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,61 +18,82 @@ context begin interpretation Arch .

requalify_types
machine_state
pt_array_len
vs_array_len

end

declare [[populate_globals=true]]

context begin interpretation Arch . (*FIXME: arch_split*)

type_synonym cghost_state = "(machine_word \<rightharpoonup> vmpage_size) * (machine_word \<rightharpoonup> nat)
* ghost_assertions"
(* Sanity checks for array sizes. ptTranslationBits not yet available at definition site. *)
lemma ptTranslationBits_vs_index_bits:
"ptTranslationBits VSRootPT_T = vs_index_bits"
by (simp add: ptTranslationBits_def vs_index_bits_def)

definition
gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
(* FIXME AARCH64: this is guaranteed to always succeed even though config_ARM_PA_SIZE_BITS_40
is unfolded. It'd be nicer if we could also get something symbolic out of value_type, though *)
lemma ptTranslationBits_vs_array_len':
"2 ^ ptTranslationBits VSRootPT_T = vs_array_len"
by (simp add: vs_array_len_def ptTranslationBits_vs_index_bits vs_index_bits_def
Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)

lemmas ptTranslationBits_vs_array_len = ptTranslationBits_vs_array_len'[unfolded vs_array_len_def]

type_synonym cghost_state =
"(machine_word \<rightharpoonup> vmpage_size) \<times> \<comment> \<open>Frame sizes\<close>
(machine_word \<rightharpoonup> nat) \<times> \<comment> \<open>CNode sizes\<close>
(machine_word \<rightharpoonup> pt_type) \<times> \<comment> \<open>PT types\<close>
ghost_assertions" \<comment> \<open>ASMRefine assertions\<close>

definition gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
"gs_clear_region ptr bits gs \<equiv>
(%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
%x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))"
(\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x,
\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd (snd gs)) x,
snd (snd (snd gs)))"

definition
gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
where
definition gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
"gs_new_frames sz ptr bits \<equiv> \<lambda>gs.
if bits < pageBitsForSize sz then gs
else (\<lambda>x. if \<exists>n\<le>mask (bits - pageBitsForSize sz).
x = ptr + n * 2 ^ pageBitsForSize sz then Some sz
else fst gs x, snd gs)"
if bits < pageBitsForSize sz then gs
else (\<lambda>x. if \<exists>n\<le>mask (bits - pageBitsForSize sz).
x = ptr + n * 2 ^ pageBitsForSize sz then Some sz
else fst gs x, snd gs)"

definition
gs_new_cnodes:: "nat \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
where
definition gs_new_cnodes:: "nat \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
"gs_new_cnodes sz ptr bits \<equiv> \<lambda>gs.
if bits < sz + 4 then gs
else (fst gs, \<lambda>x. if \<exists>n\<le>mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4)
then Some sz
else fst (snd gs) x, snd (snd gs))"
if bits < sz + 4 then gs
else (fst gs, \<lambda>x. if \<exists>n\<le>mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4)
then Some sz
else fst (snd gs) x, snd (snd gs))"

definition gs_new_pt_t:: "pt_type \<Rightarrow> addr \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
"gs_new_pt_t pt_t ptr \<equiv>
\<lambda>gs. (fst gs, fst (snd gs), (fst (snd (snd gs))) (ptr \<mapsto> pt_t), snd (snd (snd gs)))"

abbreviation
gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> machine_word"
where
"gs_get_assn k \<equiv> ghost_assertion_data_get k (snd o snd)"
abbreviation gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> machine_word" where
"gs_get_assn k \<equiv> ghost_assertion_data_get k (snd \<circ> snd \<circ> snd)"

abbreviation
gs_set_assn :: "int \<Rightarrow> machine_word \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
where
"gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd o apsnd)"
abbreviation gs_set_assn :: "int \<Rightarrow> machine_word \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
"gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd \<circ> apsnd \<circ> apsnd)"

declare [[record_codegen = false]]
declare [[allow_underscore_idents = true]]

end

(* workaround for the fact that the C parser wants to know the vmpage sizes*)
(* Workaround for the fact that the retype annotations need the vmpage sizes*)
(* create appropriately qualified aliases *)
context begin interpretation Arch . global_naming vmpage_size
requalify_consts ARMSmallPage ARMLargePage ARMHugePage
end

(* Also need pt_type constructors for retype annotations. We leave them available globally for C. *)
context begin interpretation Arch .
requalify_consts NormalPT_T VSRootPT_T
end

definition
ctcb_size_bits :: nat
where
Expand Down
59 changes: 59 additions & 0 deletions spec/machine/AARCH64/Platform.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,5 +101,64 @@ definition irqVTimerEvent :: irq where
definition pageColourBits :: nat where
"pageColourBits \<equiv> undefined" \<comment> \<open>not implemented on this platform\<close>


section \<open>Page table sizes\<close>

definition vs_index_bits :: nat where
"vs_index_bits \<equiv> if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)"

end

(* Need to declare code equation outside Arch locale *)
declare AARCH64.vs_index_bits_def[code]

context Arch begin global_naming AARCH64

lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits"
by (simp add: vs_index_bits_def)

(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can
retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain
number such as 9 or 10. *)
typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto

end

instantiation AARCH64.vs_index_len :: len0
begin
interpretation Arch .
definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \<equiv> CARD(vs_index_len)"
instance ..
end

instantiation AARCH64.vs_index_len :: len
begin
interpretation Arch .
instance
proof
show "0 < LENGTH(vs_index_len)"
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
qed
end

context Arch begin global_naming AARCH64

type_synonym vs_index = "vs_index_len word"

type_synonym pt_index_len = 9
type_synonym pt_index = "pt_index_len word"

text \<open>Sanity check:\<close>
lemma length_vs_index_len[simp]:
"LENGTH(vs_index_len) = vs_index_bits"
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])


section \<open>C array sizes corresponding to page table sizes\<close>

value_type pt_array_len = "(2::nat) ^ LENGTH(pt_index_len)"
value_type vs_array_len = "(2::nat) ^ vs_index_bits"

end

end

0 comments on commit 52b4ba5

Please sign in to comment.