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(*
12    Machine and kernel state.
13*)
14
15chapter "Machine State"
16
17theory State_H
18imports
19  "Lib.HaskellLib_H"
20  RegisterSet_H
21  "../../machine/ARM_HYP/MachineOps"
22begin
23context Arch begin global_naming ARM_HYP_H
24
25definition
26  Word :: "machine_word \<Rightarrow> machine_word"
27where
28  Word_def[simp]:
29 "Word \<equiv> id"
30
31#INCLUDE_HASKELL Data/WordLib.lhs all_bits ONLY wordBits
32
33end
34
35context begin interpretation Arch .
36
37requalify_consts
38  wordBits
39
40end
41
42#INCLUDE_HASKELL Data/WordLib.lhs all_bits NOT wordBits
43
44context Arch begin global_naming ARM_HYP_H
45
46
47#INCLUDE_HASKELL SEL4/Machine/RegisterSet.lhs Arch=ARM_HYP CONTEXT ARM_HYP_H all_bits NOT UserContext UserMonad getRegister setRegister newContext mask Word PPtr
48
49definition
50  PPtr :: "machine_word \<Rightarrow> machine_word"
51where
52  PPtr_def[simp]:
53 "PPtr \<equiv> id"
54
55definition
56  fromPPtr :: "machine_word \<Rightarrow> machine_word"
57where
58  fromPPtr_def[simp]:
59 "fromPPtr \<equiv> id"
60
61definition
62  nullPointer :: machine_word
63where
64 "nullPointer \<equiv> 0"
65
66end
67end
68