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