--- 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) = (