diff -r f66d61f5439d -r 0960686df575 S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Sep 12 19:00:26 2013 +0800
+++ b/S2ss_prop.thy	Tue Sep 24 14:02:15 2013 +0800
@@ -766,11 +766,302 @@
 apply (simp add:co2sobj_writefile_unchange alive_simps)
 done
 
+
+definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "update_s2ss_obj s ss obj sobj sobj' = 
+     (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+      then ss \<union> {sobj'}
+      else ss - {sobj} \<union> {sobj'})"
+
+definition update_s2ss_sfile :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where 
+  "update_s2ss_sfile s ss f sf \<equiv> 
+     if (same_inode_files s f = {f})
+     then ss
+     else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"
+
+definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where
+  "del_s2ss_file s ss f sf = 
+     (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
+      then ss
+      else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
+           then update_s2ss_sfile s ss f sf
+           else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf"
+
+lemma alive_co2sobj_closefd1:
+  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
+    file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
+   \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd3:
+  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;
+    file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>
+   \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd2:
+  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>
+   \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd':
+  "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; 
+    valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)
+
+ML {*asm_full_simp_tac*}
+
+ML {*
+fun my_setiff_tac i = 
+     (etac @{thm CollectE} i 
+      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i
+              THEN etac @{thm disjE} i)
+      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i
+              THEN etac @{thm conjE} i 
+              THEN (REPEAT (etac @{thm CollectE} i))))
+THEN (REPEAT ((        etac @{thm exE} 
+               ORELSE' etac @{thm conjE}
+               ORELSE' etac @{thm bexE}) i))
+THEN (rtac @{thm CollectI} i
+      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i))
+
+*}
+
+ML {*
+fun my_seteq_tac i = 
+     (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1)
+THEN (rtac @{thm set_eqI} i)
+THEN (rtac @{thm iffI} i)
+THEN my_setiff_tac i
+*}
+
+lemma co2sobj_sproc_imp:
+  "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sfile_imp:
+  "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sdir_imp:
+  "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sshm_imp:
+  "co2sobj s obj = Some (S_shm sh) \<Longrightarrow> \<exists> h. obj = O_shm h"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_smsgq_imp:
+  "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
 lemma s2ss_closefd:
   "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
      case (file_of_proc_fd s p fd) of
-       Some f \<Rightarrow> if ("
+       Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})
+                 then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
+                         (Some sf, Some sp, Some sp') \<Rightarrow> 
+                            (del_s2ss_file s (
+                               update_s2ss_obj s (s2ss s) (O_proc p) 
+                                 (S_proc sp (O_proc p \<in> Tainted s))
+                                 (S_proc sp' (O_proc p \<in> Tainted s))) f sf)
+                      | _ \<Rightarrow> {})
+                 else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of 
+                         (Some sp, Some sp') \<Rightarrow> 
+                            (update_s2ss_obj s (s2ss s) (O_proc p)
+                               (S_proc sp (O_proc p \<in> Tainted s))
+                               (S_proc sp' (O_proc p \<in> Tainted s)))
+                      | _ \<Rightarrow> {})
+      | _     \<Rightarrow> s2ss s)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (frule current_proc_has_sp, simp, erule exE)
+apply (case_tac "file_of_proc_fd s p fd")
+
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (frule co2sobj_closefd, simp)
+apply (frule cp2sproc_closefd, simp)
+apply (simp add:proc_file_fds_def split:t_object.splits)
+apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)
+apply (frule cp2sproc_closefd, simp)
+apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted 
+            split:t_object.splits option.splits if_splits)[1]
+
+apply (case_tac "cp2sproc (CloseFd p fd # s) p")
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "cf2sfile s a")
+apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current)
+apply (simp)
+
+apply (rule conjI, rule impI, erule conjE)
+apply (simp add:del_s2ss_file_def)
+apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
+
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
+apply (tactic {*my_seteq_tac 1*})
+apply simp
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+
+apply (rule impI)+
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2)
+apply (case_tac "obj = O_file a", simp add:alive_simps)
+apply (rule DiffI, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (erule_tac x = "O_proc pa" in allE, simp)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)
+apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+
+apply (rule impI, tactic {*my_seteq_tac 1*})
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI, rule impI, (erule exE|erule conjE)+)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule impI)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = obj in allE, simp)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
+apply (tactic {*my_setiff_tac 1*})
+
+
+
+
+defer
+apply (rule impI)
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI, rule impI, erule exE, erule conjE)
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
+apply (rule disjI2, rule_tac x = obj in exI, erule conjE)
+apply (simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits)
+apply (simp, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1)
+apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits)
+apply (simp)
+apply (erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits 
+                simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1)
+done
+
+
+
+
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
-  s2ss_readfile s2ss_writefile
+  s2ss_readfile s2ss_writefile s2ss_closefd