Mercurial Mercurial > hg > selinux / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Flask.thy
changeset 15 4ca824cd0c59
parent 14 cc1e46225a81
child 18 9b42765ce554 
--- a/Flask.thy	Thu May 30 15:28:57 2013 +0800
+++ b/Flask.thy	Mon Jun 03 10:34:58 2013 +0800
@@ -139,6 +139,7 @@
   and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
   and init_shms :: "t_shm set"
   and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" 
+  and init_flag_of_proc_shm :: "t_process \<Rightarrow> t_shm \<rightharpoonup> t_shm_attach_flag"
 
   assumes
       parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"
@@ -156,8 +157,8 @@
   and init_filefd_valid:       "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"
   and init_fileflag_valid:     "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"
 
-  and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"
-  and init_procshm_valid:      "\<And> p h flag flag'. \<lbrakk>(p,flag) \<in> init_procs_of_shm h; (p, flag') \<in> init_procs_of_shm h\<rbrakk> \<Longrightarrow> flag = flag'"
+  and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag"
+  and init_shmflag_has_proc:   "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"
   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
   and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
 
@@ -427,7 +428,30 @@
 | "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"
 | "current_shms (e # \<tau>) = current_shms \<tau> "
 
-fun procs_of_shm : "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
+fun flag_of_proc_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag option"
+where
+  "flag_of_proc_shm [] = init_flag_of_proc_shm"
+| "flag_of_proc_shm (Attach p h flag # s) = (\<lambda> p' h'. 
+     if (p' = p \<and> h' = h) then Some flag else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (Detach p h # s) = (\<lambda> p' h'. 
+     if (p' = p \<and> h' = h) then None else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (CreateShM p h # s) = (\<lambda> p' h'. 
+     if (h' = h) then None else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (DeleteShM p h # s) = (\<lambda> p' h'. 
+     if (h' = h) then None else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (Clone p p' fds shms # s) = (\<lambda> p'' h.
+     if (p'' = p' \<and> h \<in> shms) then flag_of_proc_shm s p h
+     else if (p'' = p') then None
+     else flag_of_proc_shm s p'' h)"
+| "flag_of_proc_shm (Execve p f fds # s) = (\<lambda> p' h. 
+     if (p' = p) then None else flag_of_proc_shm s p' h)"
+| "flag_of_proc_shm (Kill p p' # s) = (\<lambda> p'' h. 
+     if (p'' = p') then None else flag_of_proc_shm s p'' h)"
+| "flag_of_proc_shm (Exit p # s) = (\<lambda> p' h. 
+     if (p' = p) then None else flag_of_proc_shm s p' h)"
+| "flag_of_proc_shm (e # s) = flag_of_proc_shm s"
+
+fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
 where
   "procs_of_shm [] = init_procs_of_shm"
 | "procs_of_shm (CreateShM p h # \<tau>) =
selinux