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