97 "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of |
97 "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of |
98 (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms) |
98 (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms) |
99 | _ \<Rightarrow> None)" |
99 | _ \<Rightarrow> None)" |
100 *) |
100 *) |
101 |
101 |
102 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option" |
102 fun init_obj2sobj :: "t_dobject \<Rightarrow> t_sobject option" |
103 where |
103 where |
104 "init_obj2sobj (O_proc p) = |
104 "init_obj2sobj (D_proc p) = |
105 (case (init_cp2sproc p) of |
105 (case (init_cp2sproc p) of |
106 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
106 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
107 | _ \<Rightarrow> None)" |
107 | _ \<Rightarrow> None)" |
108 | "init_obj2sobj (O_file f) = |
108 | "init_obj2sobj (D_file f) = |
109 Some (S_file (init_cf2sfiles f) |
109 Some (S_file (init_cf2sfiles f) |
110 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))" |
110 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))" |
111 | "init_obj2sobj (O_dir f) = |
111 | "init_obj2sobj (D_dir f) = |
112 (case (init_cf2sfile f) of |
112 (case (init_cf2sfile f) of |
113 Some sf \<Rightarrow> Some (S_dir sf) |
113 Some sf \<Rightarrow> Some (S_dir sf) |
114 | _ \<Rightarrow> None)" |
114 | _ \<Rightarrow> None)" |
115 | "init_obj2sobj (O_msgq q) = None" |
115 | "init_obj2sobj (D_msgq q) = None" |
116 |
116 |
117 (* |
117 fun init_dalive :: "t_dobject \<Rightarrow> bool" |
118 (case (init_cq2smsgq q) of |
118 where |
119 Some sq \<Rightarrow> Some (S_msgq sq) |
119 "init_dalive (D_proc p) = (p \<in> init_procs)" |
120 | _ \<Rightarrow> None)" |
120 | "init_dalive (D_file f) = (is_init_file f)" |
121 |
121 | "init_dalive (D_dir f) = (is_init_dir f)" |
122 | "init_obj2sobj (O_shm h) = |
122 | "init_dalive (D_msgq q) = False" |
123 (case (init_ch2sshm h) of |
|
124 Some sh \<Rightarrow> Some (S_shm sh) |
|
125 | _ \<Rightarrow> None)" |
|
126 | "init_obj2sobj (O_msg q m) = |
|
127 (case (init_cq2smsgq q, init_cm2smsg q m) of |
|
128 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
|
129 | _ \<Rightarrow> None)" *) |
|
130 | "init_obj2sobj _ = None" |
|
131 |
123 |
132 definition |
124 definition |
133 "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}" |
125 "init_static_state \<equiv> {sobj. \<exists> obj. init_dalive obj \<and> init_obj2sobj obj = Some sobj}" |
134 |
126 |
135 (**************** translation from dynamic to static *******************) |
127 (**************** translation from dynamic to static *******************) |
136 |
128 |
137 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
129 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
138 where |
130 where |
225 where |
217 where |
226 "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of |
218 "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of |
227 (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms) |
219 (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms) |
228 | _ \<Rightarrow> None)" |
220 | _ \<Rightarrow> None)" |
229 |
221 |
230 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option" |
222 fun co2sobj :: "t_state \<Rightarrow> t_dobject \<Rightarrow> t_sobject option" |
231 where |
223 where |
232 "co2sobj s (O_proc p) = |
224 "co2sobj s (D_proc p) = |
233 (case (cp2sproc s p) of |
225 (case (cp2sproc s p) of |
234 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
226 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
235 | _ \<Rightarrow> None)" |
227 | _ \<Rightarrow> None)" |
236 | "co2sobj s (O_file f) = |
228 | "co2sobj s (D_file f) = |
237 Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))" |
229 Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))" |
238 | "co2sobj s (O_dir f) = |
230 | "co2sobj s (D_dir f) = |
239 (case (cf2sfile s f) of |
231 (case (cf2sfile s f) of |
240 Some sf \<Rightarrow> Some (S_dir sf) |
232 Some sf \<Rightarrow> Some (S_dir sf) |
241 | _ \<Rightarrow> None)" |
233 | _ \<Rightarrow> None)" |
242 | "co2sobj s (O_msgq q) = |
234 | "co2sobj s (D_msgq q) = |
243 (case (cq2smsgq s q) of |
235 (case (cq2smsgq s q) of |
244 Some sq \<Rightarrow> Some (S_msgq sq) |
236 Some sq \<Rightarrow> Some (S_msgq sq) |
245 | _ \<Rightarrow> None)" |
237 | _ \<Rightarrow> None)" |
246 (* |
238 |
247 | "co2sobj s (O_shm h) = |
239 fun dalive :: "t_state \<Rightarrow> t_dobject \<Rightarrow> bool" |
248 (case (ch2sshm s h) of |
240 where |
249 Some sh \<Rightarrow> Some (S_shm sh) |
241 "dalive s (D_proc p) = (p \<in> current_procs s)" |
250 | _ \<Rightarrow> None)" |
242 | "dalive s (D_file f) = (is_file s f)" |
251 |
243 | "dalive s (D_dir f) = (is_dir s f)" |
252 | "co2sobj s (O_msg q m) = |
244 | "dalive s (D_msgq q) = (q \<in> current_msgqs s)" |
253 (case (cq2smsgq s q, cm2smsg s q m) of |
|
254 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
|
255 | _ \<Rightarrow> None)" |
|
256 *) |
|
257 | "co2sobj s _ = None" |
|
258 |
|
259 |
245 |
260 definition s2ss :: "t_state \<Rightarrow> t_static_state" |
246 definition s2ss :: "t_state \<Rightarrow> t_static_state" |
261 where |
247 where |
262 "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}" |
248 "s2ss s \<equiv> {sobj. \<exists> obj. dalive s obj \<and> co2sobj s obj = Some sobj}" |
263 |
249 |
264 |
250 |
265 (* ******************************************************** *) |
251 (* ******************************************************** *) |
266 |
252 |
267 |
253 |