1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11(* 12Types and operations to access the underlying machine, instantiated 13for x64. 14*) 15 16chapter "x64 Machine Instantiation" 17 18theory Machine_A 19imports 20 "Word_Lib.WordSetup" 21 "Lib.NonDetMonad" 22 "ExecSpec.MachineTypes" 23 "ExecSpec.MachineOps" 24begin 25 26context Arch begin global_naming X64_A 27 28text {* 29 The specification is written with abstract type names for object 30 references, user pointers, word-based data, cap references, and so 31 on. This theory provides an instantiation of these names to concrete 32 types for the x64 architecture. Other architectures may have slightly 33 different instantiations. 34*} 35type_synonym obj_ref = machine_word 36type_synonym vspace_ref = machine_word 37 38type_synonym data = machine_word 39type_synonym cap_ref = "bool list" 40type_synonym length_type = machine_word 41 42type_synonym asid_low_len = 9 43type_synonym asid_low_index = "asid_low_len word" 44 45type_synonym asid_high_len = 3 46type_synonym asid_high_index = "asid_high_len word" 47 48(* It might be nice if asid was "12 word", but Refine is easier if it is a machine_word. *) 49(* Making asid a machine_word means that we need invariants that the extra bits are zero. *) 50type_synonym asid_len = 12 51type_synonym asid_rep_len = machine_word_len 52type_synonym asid = "asid_rep_len word" 53 54text {* With the definitions above, most conversions between abstract 55type names boil down to just the identity function, some convert from 56@{text word} to @{typ nat} and others between different word sizes 57using @{const ucast}. *} 58definition 59 oref_to_data :: "obj_ref \<Rightarrow> data" where 60 "oref_to_data \<equiv> id" 61 62definition 63 data_to_oref :: "data \<Rightarrow> obj_ref" where 64 "data_to_oref \<equiv> id" 65 66definition 67 vref_to_data :: "vspace_ref \<Rightarrow> data" where 68 "vref_to_data \<equiv> id" 69 70definition 71 data_to_vref :: "data \<Rightarrow> vspace_ref" where 72 "data_to_vref \<equiv> id" 73 74definition 75 nat_to_len :: "nat \<Rightarrow> length_type" where 76 "nat_to_len \<equiv> of_nat" 77 78definition 79 data_to_nat :: "data \<Rightarrow> nat" where 80 "data_to_nat \<equiv> unat" 81 82definition 83 data_to_16 :: "data \<Rightarrow> 16 word" where 84 "data_to_16 \<equiv> ucast" 85 86definition 87 data_to_cptr :: "data \<Rightarrow> cap_ref" where 88 "data_to_cptr \<equiv> to_bl" 89 90definition 91 combine_ntfn_badges :: "data \<Rightarrow> data \<Rightarrow> data" where 92 "combine_ntfn_badges \<equiv> bitOR" 93 94definition 95 combine_ntfn_msgs :: "data \<Rightarrow> data \<Rightarrow> data" where 96 "combine_ntfn_msgs \<equiv> bitOR" 97 98 99text {* These definitions will be unfolded automatically in proofs. *} 100lemmas data_convs [simp] = 101 oref_to_data_def data_to_oref_def vref_to_data_def data_to_vref_def 102 nat_to_len_def data_to_nat_def data_to_16_def data_to_cptr_def 103 104 105text {* The following definitions provide architecture-dependent sizes 106 such as the standard page size and capability size of the underlying 107 machine. 108*} 109definition 110 slot_bits :: nat where 111 "slot_bits \<equiv> 5" 112 113definition 114 msg_label_bits :: nat where 115 [simp]: "msg_label_bits \<equiv> 52" 116 117definition 118 new_context :: "user_context" where 119 "new_context \<equiv> UserContext FPUNullState ((\<lambda>r. 0)(CS := selCS3, SS := selDS3, FLAGS := 0x202))" 120 121definition 122 pptr_base :: "machine_word" where 123 "pptr_base = Platform.X64.pptrBase" 124 125(* Virtual address space available to users. *) 126definition 127 user_vtop :: "machine_word" where 128 "user_vtop = Platform.X64.pptrUserTop" 129 130text {* The lowest virtual address in the kernel window. The kernel reserves the 131virtual addresses from here up in every virtual address space. *} 132definition 133 kernel_base :: "vspace_ref" where 134 "kernel_base \<equiv> 0xffffffff80000000" 135 136definition 137 idle_thread_ptr :: vspace_ref where 138 "idle_thread_ptr = kernel_base + 0x1000" 139 140end 141 142context begin interpretation Arch . 143 requalify_consts idle_thread_ptr 144end 145 146context Arch begin global_naming X64_A 147 148(* is nat_to_cref arch specific ? *) 149definition 150 nat_to_cref :: "nat \<Rightarrow> nat \<Rightarrow> cap_ref" where 151 "nat_to_cref len n \<equiv> drop (word_bits - len) 152 (to_bl (of_nat n :: machine_word))" 153definition 154 "msg_info_register \<equiv> msgInfoRegister" 155definition 156 "msg_registers \<equiv> msgRegisters" 157definition 158 "cap_register \<equiv> capRegister" 159definition 160 "badge_register \<equiv> badgeRegister" 161definition 162 "frame_registers \<equiv> frameRegisters" 163definition 164 "gp_registers \<equiv> gpRegisters" 165definition 166 "exception_message \<equiv> exceptionMessage" 167definition 168 "syscall_message \<equiv> syscallMessage" 169 170datatype arch_fault 171 = VMFault vspace_ref "machine_word list" 172 173end 174end 175 176