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 ArchAInvsPre
12imports "../AInvsPre"
13begin
14
15context Arch begin
16
17global_naming ARM
18
19lemma get_pd_of_thread_reachable:
20  "get_pd_of_thread (kheap s) (arch_state s) t \<noteq> 0
21   \<Longrightarrow> (\<exists>\<rhd> get_pd_of_thread (kheap s) (arch_state s) t) s"
22  by (auto simp: get_pd_of_thread_vs_lookup
23          split: Structures_A.kernel_object.splits if_split_asm option.splits
24                 cap.splits arch_cap.splits)
25
26lemma is_aligned_ptrFromPAddrD:
27"\<lbrakk>is_aligned (ptrFromPAddr b) a; a \<le> 25\<rbrakk> \<Longrightarrow> is_aligned b a"
28  apply (clarsimp simp: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
29  apply (erule is_aligned_addD2)
30  apply (rule is_aligned_weaken[where x = 25])
31   apply (simp add: is_aligned_def)
32  apply simp
33  done
34
35lemma obj_bits_data_at:
36  "data_at sz (ptrFromPAddr b) s
37  \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz"
38  apply (clarsimp simp add: obj_at_def a_type_def data_at_def
39                     split: kernel_object.splits arch_kernel_obj.split_asm if_splits)
40  apply (case_tac ko,simp_all)
41   apply fastforce
42  subgoal for ko archko
43   by (case_tac archko,fastforce+)
44  done
45
46lemma some_get_page_info_umapsD:
47  "\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
48    (\<exists>\<rhd> pd_ref) s; valid_vspace_objs s; pspace_aligned s;
49    valid_asid_table (arm_asid_table (arch_state s)) s; valid_objs s\<rbrakk>
50   \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and>
51             data_at sz (ptrFromPAddr b) s)"
52  apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
53                 split: option.splits Structures_A.kernel_object.splits
54                        arch_kernel_obj.splits if_splits)
55  apply (frule (1) valid_vspace_objsD[rotated 2])
56   apply (simp add: obj_at_def)
57  apply (simp add: valid_vspace_obj_def vspace_bits_defs)
58  apply (drule_tac x="ucast (p >> 21)" in spec)
59  apply (simp split: pde.splits)
60    apply (rename_tac rs pd pt_ref)
61    apply (subgoal_tac
62        "((rs, pd_ref) \<rhd>1
63          (VSRef (ucast (ucast (p >> 21))) (Some APageDirectory) # rs,
64           ptrFromPAddr pt_ref)) s")
65     prefer 2
66     apply (rule vs_lookup1I[rotated 2], simp)
67      apply (simp add: obj_at_def)
68     apply (simp add: vs_refs_def pde_ref_def image_def graph_of_def)
69     apply (rule_tac x="ucast (p >> 21)" in exI, rule conjI, simp+)
70    apply (frule (1) vs_lookup_step)
71    apply (drule (2) stronger_vspace_objsD[where ref="x # xs" for x xs])
72    apply clarsimp
73    apply (case_tac ao, simp_all add: a_type_simps obj_at_def)[1]
74     apply (simp add: get_pt_info_def get_pt_entry_def)
75     apply (drule_tac x="(ucast ((p >> 12) && mask 9))" in spec)
76     apply (clarsimp simp: obj_at_def
77      split: pte.splits,intro exI conjI,simp_all)[1]
78      apply (frule obj_bits_data_at)
79      apply (clarsimp simp: pspace_aligned_def data_at_def)
80      apply (drule_tac x = "(ptrFromPAddr b)" in  bspec )
81       apply (fastforce simp: obj_at_def)
82      apply (clarsimp dest!: is_aligned_ptrFromPAddrD)
83     apply (intro exI conjI, simp_all add: pageBits_def)[1]
84    apply (simp add: get_pt_info_def get_pt_entry_def)
85   apply clarsimp
86   apply (frule obj_bits_data_at)
87   apply (intro exI conjI, simp_all add: pageBits_def)[1]
88   apply (clarsimp simp: pspace_aligned_def data_at_def)
89    apply (drule_tac x = "(ptrFromPAddr b)" in  bspec)
90    apply (fastforce simp: obj_at_def)
91   apply (clarsimp dest!: is_aligned_ptrFromPAddrD)
92  apply clarsimp
93  apply (frule obj_bits_data_at)
94  apply (intro exI conjI, simp_all add: pageBits_def)[1]
95  apply (clarsimp simp: pspace_aligned_def data_at_def)
96   apply (drule_tac x = "(ptrFromPAddr b)" in  bspec)
97   apply (fastforce simp: obj_at_def)
98  apply (clarsimp dest!: is_aligned_ptrFromPAddrD)
99  done
100
101lemma user_mem_dom_cong:
102  "kheap s = kheap s' \<Longrightarrow> dom (user_mem s) = dom (user_mem s')"
103  by (simp add: user_mem_def in_user_frame_def dom_def obj_at_def)
104
105lemma device_mem_dom_cong:
106  "kheap s = kheap s' \<Longrightarrow> dom (device_mem s) = dom (device_mem s')"
107  by (simp add: device_mem_def in_device_frame_def dom_def obj_at_def)
108
109lemma device_frame_in_device_region:
110  "\<lbrakk>in_device_frame p s; pspace_respects_device_region s\<rbrakk>
111  \<Longrightarrow> device_state (machine_state s) p \<noteq> None"
112  by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
113
114lemma is_aligned_physMappingOffset:
115"is_aligned physMappingOffset (pageBitsForSize sz)"
116  by (case_tac sz, simp_all add: physMappingOffset_def
117                   kernelBase_addr_def physBase_def is_aligned_def)[1]
118
119global_naming Arch
120named_theorems AInvsPre_asms
121
122lemma get_page_info_0[simp]:
123  "get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) 0 x = None"
124  by (simp add: get_page_info_def)
125
126lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]:
127  assumes "valid_state s"
128  shows "ptable_rights t s x \<noteq> {} \<Longrightarrow>
129         ptable_lift t s x = Some (addrFromPPtr y) \<Longrightarrow>
130         in_user_frame y s \<or> in_device_frame y s"
131  apply (clarsimp simp: ptable_rights_def ptable_lift_def in_user_frame_def
132                        in_device_frame_def data_at_def
133                 split: option.splits)
134  apply (rename_tac b a r)
135  apply (frule some_get_page_info_umapsD)
136       apply (rule get_pd_of_thread_reachable, clarsimp)
137      using assms
138      apply (simp_all add: valid_state_def valid_pspace_def
139                           valid_arch_state_def)
140  apply clarsimp
141  apply (frule is_aligned_add_helper[OF _ and_mask_less',
142                                     THEN conjunct2, of _ _ x])
143   apply (simp only: pbfs_less_wb'[simplified word_bits_def])
144  apply (clarsimp simp: ptrFromPAddr_def addrFromPPtr_def
145                        field_simps)
146  apply (rule_tac x=sz in exI)
147  apply (drule_tac x = sz in spec)
148  apply (subst add.assoc[symmetric])
149  apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_physMappingOffset]])
150    apply (rule le_refl)
151   apply (rule_tac w = x in and_mask_less')
152    apply (case_tac sz, simp_all add: word_bits_conv)[1]
153  apply (clarsimp simp: field_simps simp: data_at_def)
154  done
155end
156
157global_interpretation AInvsPre?: AInvsPre
158  proof goal_cases
159  interpret Arch .
160  case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_asms)?)
161  qed
162
163requalify_facts
164  ARM.user_mem_dom_cong
165  ARM.device_mem_dom_cong
166  ARM.device_frame_in_device_region
167  ARM.is_aligned_physMappingOffset
168end
169