From 4add4bdbf28b98e43bf7166f337a3e0c60d59f44 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 4 Jan 2024 11:15:22 +1100 Subject: [PATCH] aarch64 machine+aspec+cspec: pt_type ghost+table array sizes - 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 --- spec/abstract/AARCH64/Arch_Structs_A.thy | 43 +------------ spec/cspec/AARCH64/Kernel_C.thy | 79 +++++++++++++++--------- spec/machine/AARCH64/Platform.thy | 59 ++++++++++++++++++ 3 files changed, 110 insertions(+), 71 deletions(-) diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy index 075a7e3b2..fbc511338 100644 --- a/spec/abstract/AARCH64/Arch_Structs_A.thy +++ b/spec/abstract/AARCH64/Arch_Structs_A.thy @@ -113,48 +113,7 @@ definition pte_base_addr :: "pte \ paddr" where definition ppn_from_pptr :: "obj_ref \ ppn" where "ppn_from_pptr p = ucast (addrFromPPtr p >> pageBits)" -definition vs_index_bits :: nat where - "vs_index_bits \ 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) \ 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 \Sanity check:\ -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) diff --git a/spec/cspec/AARCH64/Kernel_C.thy b/spec/cspec/AARCH64/Kernel_C.thy index 60636c5c8..254e030c7 100644 --- a/spec/cspec/AARCH64/Kernel_C.thy +++ b/spec/cspec/AARCH64/Kernel_C.thy @@ -18,6 +18,8 @@ context begin interpretation Arch . requalify_types machine_state + pt_array_len + vs_array_len end @@ -25,54 +27,73 @@ declare [[populate_globals=true]] context begin interpretation Arch . (*FIXME: arch_split*) -type_synonym cghost_state = "(machine_word \ vmpage_size) * (machine_word \ 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 \ nat \ cghost_state \ 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 \ vmpage_size) \ \ \Frame sizes\ + (machine_word \ nat) \ \ \CNode sizes\ + (machine_word \ pt_type) \ \ \PT types\ + ghost_assertions" \ \ASMRefine assertions\ + +definition gs_clear_region :: "addr \ nat \ cghost_state \ cghost_state" where "gs_clear_region ptr bits gs \ - (%x. if x \ {ptr..+2 ^ bits} then None else fst gs x, - %x. if x \ {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))" + (\x. if x \ {ptr..+2 ^ bits} then None else fst gs x, + \x. if x \ {ptr..+2 ^ bits} then None else fst (snd gs) x, + \x. if x \ {ptr..+2 ^ bits} then None else fst (snd (snd gs)) x, + snd (snd (snd gs)))" -definition - gs_new_frames:: "vmpage_size \ addr \ nat \ cghost_state \ cghost_state" - where +definition gs_new_frames:: "vmpage_size \ addr \ nat \ cghost_state \ cghost_state" where "gs_new_frames sz ptr bits \ \gs. - if bits < pageBitsForSize sz then gs - else (\x. if \n\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 (\x. if \n\mask (bits - pageBitsForSize sz). + x = ptr + n * 2 ^ pageBitsForSize sz then Some sz + else fst gs x, snd gs)" -definition - gs_new_cnodes:: "nat \ addr \ nat \ cghost_state \ cghost_state" - where +definition gs_new_cnodes:: "nat \ addr \ nat \ cghost_state \ cghost_state" where "gs_new_cnodes sz ptr bits \ \gs. - if bits < sz + 4 then gs - else (fst gs, \x. if \n\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, \x. if \n\mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4) + then Some sz + else fst (snd gs) x, snd (snd gs))" -abbreviation - gs_get_assn :: "int \ cghost_state \ machine_word" - where - "gs_get_assn k \ ghost_assertion_data_get k (snd o snd)" +definition gs_new_pt_t:: "pt_type \ addr \ cghost_state \ cghost_state" where + "gs_new_pt_t pt_t ptr \ + \gs. (fst gs, fst (snd gs), (fst (snd (snd gs))) (ptr \ pt_t), snd (snd (snd gs)))" -abbreviation - gs_set_assn :: "int \ machine_word \ cghost_state \ cghost_state" - where - "gs_set_assn k v \ ghost_assertion_data_set k v (apsnd o apsnd)" +abbreviation gs_get_assn :: "int \ cghost_state \ machine_word" where + "gs_get_assn k \ ghost_assertion_data_get k (snd \ snd \ snd)" + +abbreviation gs_set_assn :: "int \ machine_word \ cghost_state \ cghost_state" where + "gs_set_assn k v \ ghost_assertion_data_set k v (apsnd \ apsnd \ 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 diff --git a/spec/machine/AARCH64/Platform.thy b/spec/machine/AARCH64/Platform.thy index 40f0b3e7e..6d6c5c712 100644 --- a/spec/machine/AARCH64/Platform.thy +++ b/spec/machine/AARCH64/Platform.thy @@ -101,5 +101,64 @@ definition irqVTimerEvent :: irq where definition pageColourBits :: nat where "pageColourBits \ undefined" \ \not implemented on this platform\ + +section \Page table sizes\ + +definition vs_index_bits :: nat where + "vs_index_bits \ 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) \ 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 \Sanity check:\ +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 \C array sizes corresponding to page table sizes\ + +value_type pt_array_len = "(2::nat) ^ LENGTH(pt_index_len)" +value_type vs_array_len = "(2::nat) ^ vs_index_bits" + +end + end