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(* 12Arch-specific functions for the abstract model of CSpace. 13*) 14 15chapter "Architecture-specific TCB functions" 16 17theory ArchTcb_A 18imports "../KHeap_A" 19begin 20 21context Arch begin global_naming X64_A 22 23definition 24 arch_tcb_set_ipc_buffer :: "machine_word \<Rightarrow> vspace_ref \<Rightarrow> (unit, 'a::state_ext) s_monad" 25where 26 "arch_tcb_set_ipc_buffer target ptr \<equiv> return ()" 27 28(* Allow most pre-existing proofs to continue to work. *) 29declare arch_tcb_set_ipc_buffer_def [simp] 30 31definition 32 sanitise_or_flags :: machine_word 33where 34 "sanitise_or_flags \<equiv> bit 1 || bit 9" 35 36definition 37 sanitise_and_flags :: machine_word 38where 39 "sanitise_and_flags \<equiv> mask 12 && ~~ bit 8 && ~~ bit 3 && ~~ bit 5" 40 41definition 42 sanitise_register :: "bool \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word" 43where 44 "sanitise_register t r v \<equiv> 45 let val = (if r = FaultIP \<or> r = NextIP 46 then if v > 0x00007fffffffffff \<and> v < 0xffff800000000000 then 0 else v 47 else v) 48 in 49 if r = FLAGS then (val || sanitise_or_flags) && sanitise_and_flags else val" 50 51definition 52 arch_get_sanitise_register_info :: "obj_ref \<Rightarrow> (bool, 'a::state_ext) s_monad" 53where 54 "arch_get_sanitise_register_info t \<equiv> return False" 55 56definition 57 arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit, 'a::state_ext) s_monad" 58where 59 "arch_post_modify_registers cur t \<equiv> when (t \<noteq> cur) $ as_user t $ setRegister ErrorRegister 0" 60 61end 62end 63