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