34 |
34 |
35 definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set" |
35 definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set" |
36 where |
36 where |
37 "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}" |
37 "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}" |
38 |
38 |
|
39 fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags" |
|
40 where |
|
41 "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})" |
|
42 |
39 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
43 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
40 where |
44 where |
41 "init_cfd2sfd p fd = |
45 "init_cfd2sfd p fd = |
42 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
46 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
43 (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of |
47 (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of |
44 Some sf \<Rightarrow> Some (sec, flags, sf) |
48 Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf) |
45 | _ \<Rightarrow> None) |
49 | _ \<Rightarrow> None) |
46 | _ \<Rightarrow> None)" |
50 | _ \<Rightarrow> None)" |
47 |
51 |
48 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set" |
52 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set" |
49 where |
53 where |
149 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
153 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
150 where |
154 where |
151 "cfd2sfd s p fd \<equiv> |
155 "cfd2sfd s p fd \<equiv> |
152 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |
156 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |
153 (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of |
157 (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of |
154 Some sf \<Rightarrow> Some (sec, flags, sf) |
158 Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf) |
155 | _ \<Rightarrow> None) |
159 | _ \<Rightarrow> None) |
156 | _ \<Rightarrow> None)" |
160 | _ \<Rightarrow> None)" |
157 |
161 |
158 |
162 |
159 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
163 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
662 |
666 |
663 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
667 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
664 where |
668 where |
665 "brandnew_proc s \<equiv> next_nat (all_procs s)" |
669 "brandnew_proc s \<equiv> next_nat (all_procs s)" |
666 |
670 |
667 fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags" |
|
668 where |
|
669 "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})" |
|
670 |
|
671 definition new_inode_num :: "t_state \<Rightarrow> nat" |
671 definition new_inode_num :: "t_state \<Rightarrow> nat" |
672 where |
672 where |
673 "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)" |
673 "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)" |
674 |
674 |
675 definition new_msgq :: "t_state \<Rightarrow> t_msgq" |
675 definition new_msgq :: "t_state \<Rightarrow> t_msgq" |