# HG changeset patch
# User chunhan
# Date 1384931998 -28800
# Node ID 002c34a6ff4fed12c2228b5aea37cc4029ea13ec
# Parent  fc7151df7f8e7c52f7702cc0180117fb402d4632
add conflict of p fd as file_fd & socket

diff -r fc7151df7f8e -r 002c34a6ff4f Alive_prop.thy
--- a/Alive_prop.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Alive_prop.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -1,5 +1,5 @@
 theory Alive_prop
-imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop
+imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop Proc_fd_of_file_prop
 begin
 
 context flask begin
@@ -51,6 +51,8 @@
             dest:is_dir_in_current split:if_splits option.splits)
 done
 
+(* sock is not inherited on Execve, Clone cases, cause I simplified it with os_grant. 
+ * chunhan, 2013-11-20
 lemma alive_execve:
   "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
      \<lambda> obj. case obj of
@@ -68,6 +70,7 @@
 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
                  is_tcp_sock_simps is_udp_sock_simps
             dest:is_dir_in_current split:if_splits option.splits)
+
 done
 
 lemma alive_clone:
@@ -90,6 +93,48 @@
            intro:is_tcp_in_current is_udp_in_current
             dest:is_dir_in_current split:if_splits option.splits)
 done
+*)
+
+lemma alive_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
+     \<lambda> obj. case obj of
+              O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd)
+                             else if (p = p') then False
+                                  else alive s (O_fd p' fd))
+            | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+                                      else alive s (O_tcp_sock (p', fd)))
+            | O_udp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+                                      else alive s (O_udp_sock (p', fd)))
+            | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
+                 is_tcp_sock_simps is_udp_sock_simps
+            dest:is_dir_in_current split:if_splits option.splits)
+apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto)
+
+done
+
+lemma alive_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = (
+     \<lambda> obj. case obj of
+              O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj
+            | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
+                             else if (p'' = p') then False
+                                  else alive s obj
+            | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
+                                      else if (p'' = p') then False
+                                           else alive s (O_tcp_sock (p'', fd)))
+            | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
+                                      else if (p'' = p') then False
+                                           else alive s (O_udp_sock (p'', fd)))
+            | _ \<Rightarrow> alive s obj )"  
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
+                 is_tcp_sock_simps is_udp_sock_simps
+           intro:is_tcp_in_current is_udp_in_current
+            dest:is_dir_in_current split:if_splits option.splits)
+done
+
 
 lemma alive_kill:
   "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (
diff -r fc7151df7f8e -r 002c34a6ff4f Dynamic_static.thy
--- a/Dynamic_static.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Dynamic_static.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -119,7 +119,7 @@
 
 lemma enrich_inherit_fds_check:
   assumes grant: "inherit_fds_check s (up, nr, nt) p fds"  and vd: "valid s"
-  and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
+  and cp2sp: "\<forall> p. p  \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
   and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'"
   and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p"
   shows "inherit_fds_check s' (up, nr, nt) p fds"
diff -r fc7151df7f8e -r 002c34a6ff4f Flask.thy
--- a/Flask.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Flask.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -154,7 +154,7 @@
                                          init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))"
 
   and init_procfds_valid:      "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)"
-  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_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> (p, fd) \<notin> init_sockets"
   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_flag_of_proc_shm p h = Some flag"
@@ -162,7 +162,7 @@
   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"
 
-  and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p"
+  and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p \<and> init_file_of_proc_fd p fd = None"
   and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
 (*
   and init_netobj_has_state:   "bidirect_in_init init_netobjs init_netobj_state"
@@ -260,6 +260,13 @@
 where
   "proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}"
 
+definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
+where
+  "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"
+
+definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
+where
+  "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
 
 (****** files and directories ******)
 
@@ -802,16 +809,6 @@
 | "deleted obj (RecvMsg p q m # s)  = (obj = O_msg q m \<or> deleted obj s)"
 | "deleted obj (_ # s) = deleted obj s"
 
-
-definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
-where
-  "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"
-
-
-definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
-where
-  "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
-
 end
 
 
diff -r fc7151df7f8e -r 002c34a6ff4f Proc_fd_of_file_prop.thy
--- a/Proc_fd_of_file_prop.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Proc_fd_of_file_prop.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -1,5 +1,5 @@
 theory Proc_fd_of_file_prop
-imports Main Flask Flask_type Valid_prop Current_files_prop
+imports Main Flask Flask_type Valid_prop Current_files_prop Current_sockets_prop
 begin
 
 context flask begin
@@ -45,6 +45,24 @@
 lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
 by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')
 
+lemma file_fds_subset_pfds:
+  "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p"
+by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)
+
+lemma tcp_filefd_conflict:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s, simp)
+apply (auto simp:is_tcp_sock_simps)
+
+
+lemma tcp_not_file_fd:
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+apply (auto simp:proc_file_fds_def)
+
+lemma udp_not_file_fd:
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+
+lemma
 
 (******************* rebuild proc_fd_of_file simpset ***********************)
 (*