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
11theory ArchTcbAcc_AI
12imports "../TcbAcc_AI"
13begin
14
15context Arch begin global_naming ARM
16
17named_theorems TcbAcc_AI_assms
18
19lemmas cap_master_cap_simps =
20  cap_master_cap_def[simplified cap_master_arch_cap_def, split_simps cap.split arch_cap.split]
21
22lemma cap_master_cap_arch_eqDs:
23  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageCap dev ref rghts sz mapdata)
24     \<Longrightarrow> rghts = UNIV \<and> mapdata = None
25          \<and> (\<exists>rghts mapdata. cap = cap.ArchObjectCap (arch_cap.PageCap dev ref rghts sz mapdata))"
26  "cap_master_cap cap = cap.ArchObjectCap arch_cap.ASIDControlCap
27     \<Longrightarrow> cap = cap.ArchObjectCap arch_cap.ASIDControlCap"
28  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid)
29     \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid))"
30  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data)
31     \<Longrightarrow> data = None \<and> (\<exists>data. cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data))"
32  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2)
33     \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2))"
34  by (clarsimp simp: cap_master_cap_def
35              split: cap.split_asm arch_cap.split_asm)+
36
37lemmas cap_master_cap_eqDs =
38  cap_master_cap_eqDs1 cap_master_cap_arch_eqDs
39  cap_master_cap_eqDs1 [OF sym] cap_master_cap_arch_eqDs[OF sym]
40
41
42lemma vm_sets_diff[simp]:
43  "vm_read_only \<noteq> vm_read_write"
44  by (simp add: vm_read_write_def vm_read_only_def)
45
46
47lemmas vm_sets_diff2[simp] = not_sym[OF vm_sets_diff]
48
49lemma cap_master_cap_tcb_cap_valid_arch:
50  "\<lbrakk> cap_master_cap c = cap_master_cap c'; is_arch_cap c \<rbrakk> \<Longrightarrow>
51  tcb_cap_valid c p s = tcb_cap_valid c' p s"
52  by (auto simp add: cap_master_cap_def tcb_cap_valid_def tcb_cap_cases_def
53                   valid_ipc_buffer_cap_def  is_cap_simps
54                   is_nondevice_page_cap_simps is_nondevice_page_cap_arch_def
55            split: option.splits cap.splits arch_cap.splits
56                   Structures_A.thread_state.splits)
57
58crunch device_state_inv[wp]: invalidateLocalTLB_ASID "\<lambda>ms. P (device_state ms)"
59  (ignore: ignore_failure)
60
61crunch device_state_inv[wp]: invalidateLocalTLB_VAASID "\<lambda>ms. P (device_state ms)"
62crunch device_state_inv[wp]: setHardwareASID "\<lambda>ms. P (device_state ms)"
63crunch device_state_inv[wp]: isb "\<lambda>ms. P (device_state ms)"
64crunch device_state_inv[wp]: dsb "\<lambda>ms. P (device_state ms)"
65crunch device_state_inv[wp]: storeWord "\<lambda>ms. P (device_state ms)"
66crunch device_state_inv[wp]: cleanByVA_PoU "\<lambda>ms. P (device_state ms)"
67crunch device_state_inv[wp]: cleanL2Range "\<lambda>ms. P (device_state ms)"
68
69lemma storeWord_invs[wp, TcbAcc_AI_assms]:
70  "\<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace>"
71proof -
72  have aligned_offset_ignore:
73    "\<And>l sz. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow>
74       p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)"
75  proof -
76    fix l sz
77    assume al: "p && mask 2 = 0"
78    assume "(l::word32) < 4" hence less: "l<2^2" by simp
79    have le: "2 \<le> pageBitsForSize sz" by (case_tac sz, simp_all)
80    show "?thesis l sz"
81      by (rule is_aligned_add_helper[simplified is_aligned_mask,
82          THEN conjunct2, THEN mask_out_first_mask_some,
83          where n=2, OF al less le])
84  qed
85
86  show ?thesis
87    apply (wp dmo_invs)
88    apply (clarsimp simp: storeWord_def invs_def valid_state_def)
89    apply (fastforce simp: valid_machine_state_def in_user_frame_def
90               assert_def simpler_modify_def fail_def bind_def return_def
91               pageBits_def aligned_offset_ignore
92             split: if_split_asm)
93    done
94qed
95
96lemma valid_ipc_buffer_cap_0[simp, TcbAcc_AI_assms]:
97  "valid_ipc_buffer_cap cap a \<Longrightarrow> valid_ipc_buffer_cap cap 0"
98  by (auto simp add: valid_ipc_buffer_cap_def case_bool_If
99    split: cap.split arch_cap.split)
100
101lemma thread_set_hyp_refs_trivial [TcbAcc_AI_assms]:
102  assumes x: "\<And>tcb. tcb_state  (f tcb) = tcb_state  tcb"
103  assumes y: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb"
104  shows      "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
105  apply (simp add: thread_set_def set_object_def)
106  apply wp
107  apply (clarsimp dest!: get_tcb_SomeD)
108  apply (clarsimp elim!: rsubst[where P=P])
109  apply (rule all_ext;
110         clarsimp simp: state_hyp_refs_of_def hyp_refs_of_def tcb_hyp_refs_def get_tcb_def x y[simplified tcb_arch_ref_def])
111  done
112
113lemma mab_pb [simp]:
114  "msg_align_bits \<le> pageBits"
115  unfolding msg_align_bits pageBits_def by simp
116
117lemma mab_wb [simp]:
118  "msg_align_bits < word_bits"
119  unfolding msg_align_bits word_bits_conv by simp
120
121
122lemma get_cap_valid_ipc [TcbAcc_AI_assms]:
123  "\<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t\<rbrace>
124     get_cap (t, tcb_cnode_index 4)
125   \<lbrace>\<lambda>rv s. valid_ipc_buffer_cap rv v\<rbrace>"
126  apply (wp get_cap_wp)
127  apply clarsimp
128  apply (drule(1) cte_wp_tcb_cap_valid)
129  apply (clarsimp simp add: tcb_cap_valid_def obj_at_def)
130  apply (simp add: valid_ipc_buffer_cap_def mask_cap_def cap_rights_update_def
131                   acap_rights_update_def is_tcb
132            split: cap.split_asm arch_cap.split_asm)
133  done
134
135
136
137lemma pred_tcb_cap_wp_at [TcbAcc_AI_assms]:
138  "\<lbrakk>pred_tcb_at proj P t s; valid_objs s;
139    ref \<in> dom tcb_cap_cases;
140    \<forall>cap. (pred_tcb_at proj P t s \<and> tcb_cap_valid cap (t, ref) s) \<longrightarrow> Q cap\<rbrakk> \<Longrightarrow>
141   cte_wp_at Q (t, ref) s"
142  apply (clarsimp simp: cte_wp_at_cases tcb_at_def dest!: get_tcb_SomeD)
143  apply (rename_tac getF setF restr)
144  apply (clarsimp simp: tcb_cap_valid_def pred_tcb_at_def obj_at_def)
145  apply (erule(1) valid_objsE)
146  apply (clarsimp simp add: valid_obj_def valid_tcb_def)
147  apply (erule_tac x="(getF, setF, restr)" in ballE)
148   apply fastforce+
149  done
150
151lemma as_user_hyp_refs_of[wp, TcbAcc_AI_assms]:
152  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
153     as_user t m
154   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
155  apply (wp as_user_wp_thread_set_helper
156            thread_set_hyp_refs_trivial | simp)+
157  done
158
159lemmas sts_typ_ats = sts_typ_ats abs_atyp_at_lifts [OF set_thread_state_typ_at]
160
161lemma arch_tcb_context_set_eq_ARM[TcbAcc_AI_assms]: "arch_tcb_context_set (arch_tcb_context_get t) t = t"
162  unfolding arch_tcb_context_get_def arch_tcb_context_set_def
163  by simp
164
165lemma arch_tcb_context_get_eq_ARM[TcbAcc_AI_assms]: "arch_tcb_context_get (arch_tcb_context_set uc t) = uc"
166  unfolding arch_tcb_context_get_def arch_tcb_context_set_def
167  by simp
168
169lemma arch_tcb_update_aux2: "(\<lambda>tcb. tcb\<lparr> tcb_arch := f (tcb_arch tcb) \<rparr>)  = tcb_arch_update f"
170  by (rule ext, simp)
171
172lemma arch_tcb_update_aux3: "tcb\<lparr>tcb_arch := f (tcb_arch tcb)\<rparr>  = tcb_arch_update f tcb"
173  by(simp)
174
175lemma tcb_context_update_aux: "arch_tcb_context_set (P (arch_tcb_context_get atcb)) atcb
176                               = tcb_context_update (\<lambda>ctx. P ctx) atcb"
177  by (simp add: arch_tcb_context_set_def arch_tcb_context_get_def)
178
179end
180
181global_interpretation TcbAcc_AI?: TcbAcc_AI
182  proof goal_cases
183  interpret Arch .
184  case 1 show ?case by (unfold_locales; (fact TcbAcc_AI_assms)?)
185  qed
186
187end
188