# HG changeset patch # User chunhan # Date 1380079753 -28800 # Node ID 68649272054c52f0a2afd217a44ba56f0c0d5472 # Parent bf8c09ec11867af44d11886e96148f49e963fcad 600 loc to finish s2ss_closefd diff -r bf8c09ec1186 -r 68649272054c S2ss_prop.thy --- a/S2ss_prop.thy Tue Sep 24 23:39:03 2013 +0800 +++ b/S2ss_prop.thy Wed Sep 25 11:29:13 2013 +0800 @@ -1258,72 +1258,161 @@ apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (case_tac "f = a", simp add:alive_simps) -apply (case_tac "f \ same_inode_files s a", rule disjI2) +apply (case_tac "f \ 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 (rule conjI, rule_tac x = "O_file f''" in exI) -apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted) -apply (rule notI, simp) -apply (rule disjI2, rule conjI, rule_tac x = obj in exI) +apply (erule_tac x = f'' in ballE, simp, simp) +apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) +apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) +apply (rule notI, simp add:co2sobj_closefd) +apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) +apply (rule disjI2, rule conjI, rule disjI2, 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.simps) -apply (rule disjI2, rule conjI, rule_tac x = obj in exI) +apply (rule notI, simp add:co2sobj.simps split:option.splits) +apply (rule disjI2, rule conjI, rule disjI2, 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.simps split:option.splits) +apply (rule disjI2, rule conjI, rule disjI2, 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.simps split:option.splits) -apply (rule disjI2, rule conjI, rule_tac x = obj in exI) +apply (rule impI, rule conjI, 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 notI, simp) +apply (rule conjI, 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 (erule_tac x = obj in allE, simp add:co2sobj_closefd) +apply (rule notI, simp add:co2sobj.simps split:option.splits) +apply (case_tac "f = a", simp add:alive_simps) +apply (case_tac "f \ same_inode_files s a", rule conjI, rule disjI2, rule conjI) +apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) +apply (simp add:co2sobj.simps) +apply (rule notI, simp add:co2sobj.simps) +apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) +apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) +apply (rule notI, simp add:co2sobj.simps) +apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted) +apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) +apply (rule conjI, 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.simps split:option.splits) -apply (rule disjI2, rule conjI, rule_tac x = obj in exI) +apply (rule notI, simp add:co2sobj.simps split:option.splits)+ +apply (rule conjI, 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.simps split:option.splits)+ +apply (rule conjI, 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.simps split:option.splits)+ +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 notI, simp) +apply (rule disjI2, rule conjI, 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 (erule_tac x = obj in allE, simp add:co2sobj_closefd) apply (rule notI, simp add:co2sobj.simps split:option.splits) +apply (case_tac "f = a", simp add:alive_simps) +apply (case_tac "f \ same_inode_files s a", rule disjI1) +apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted) +apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp) +apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) +apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) +apply (rule notI, simp add:co2sobj.simps) +apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted) +apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) +apply (rule disjI2, rule conjI, 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.simps split:option.splits)+ +apply (rule disjI2, rule conjI, 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.simps split:option.splits)+ +apply (rule disjI2, rule conjI, 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.simps split:option.splits)+ -apply (erule bexE, erule conjE) -apply (simp add:update_s2ss_obj_def split:if_splits) -apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits) +apply (erule conjE, 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_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_proc p") +apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE) +apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+) +apply (simp add:co2sobj_closefd) +apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (erule conjE|erule exE|erule disjE)+ +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (erule conjE, erule exE, erule conjE) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_proc p") +apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (erule conjE|erule exE|erule disjE)+ +apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE) +apply (rule_tac x = "O_file f'" in exI) +apply (frule same_inode_files_prop11) +apply (frule_tac obj = "O_file f'" in co2sobj_closefd) +apply (simp add:alive_simps)+ +apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE) +apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) +apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) +apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) +apply (erule conjE, erule disjE) +apply (rule_tac x = "O_proc p" in exI) +apply (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) -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 (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) -apply (rule conjI) -apply (rule impI) -apply (rule_tac x = f' in ballE, simp, simp, simp) -apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted) -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 (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) -apply (erule conjE, erule exE, erule conjE) -apply (case_tac "obj = O_proc p") +apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE) +apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+) +apply (simp add:co2sobj_closefd tainted_eq_Tainted) 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 (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) -apply (rule conjI) -apply (rule impI) -apply (rule_tac x = f' in ballE, simp, simp, simp) -apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted) -apply (rule_tac x = obj in exI) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) 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 (erule_tac obj = obj in co2sobj_some_caseD) +apply (rule_tac x = obj in exI) +apply (simp add:co2sobj_closefd) +apply (case_tac "f = a", simp add:alive_simps) +apply (case_tac "f \ same_inode_files s a") +apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (erule disjE) +apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE) +apply (rule_tac x = "O_file f'" in exI) +apply (frule same_inode_files_prop11) +apply (frule_tac obj = "O_file f'" in co2sobj_closefd) +apply (simp add:alive_simps)+ +apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE) +apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) +apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) +apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) +apply (erule conjE, erule disjE) +apply (rule_tac x = "O_proc p" in exI) +apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (erule conjE, erule exE, erule conjE) +apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (erule_tac obj = obj in co2sobj_some_caseD) +apply (rule_tac x = obj in exI) +apply (simp add:co2sobj_closefd) +apply (case_tac "f \ same_inode_files s a") +apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps) +apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) - - -apply - -defer apply (rule impI) apply (simp add:update_s2ss_obj_def) apply (rule conjI, rule impI, erule exE, erule conjE)