# HG changeset patch # User chunhan # Date 1368069584 -28800 # Node ID e9c5594d59639aa5d30dcc4a9b3010034397d759 # Parent b6ee5f35c41f2da94550de529b72fc08dbb2b5ae fixed bugs in deleted definition diff -r b6ee5f35c41f -r e9c5594d5963 Co2sobj_prop.thy --- a/Co2sobj_prop.thy Wed May 08 10:00:38 2013 +0800 +++ b/Co2sobj_prop.thy Thu May 09 11:19:44 2013 +0800 @@ -10,13 +10,28 @@ declare get_parentfs_ctxts.simps [simp del] -lemma cf2sfile_open_none: +lemma cf2sfile_open_none1: "valid (Open p f flag fd None # s) \ cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b" apply (frule vd_cons, frule vt_grant_os) -apply (frule noroot_events) -by (auto split:if_splits option.splits dest!:current_has_sec' +apply (frule noroot_events, case_tac f, simp) +apply (auto split:if_splits option.splits dest!:current_has_sec' dest:parentf_in_current' simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps get_parentfs_ctxts_simps) +done + +lemma cf2sfile_open_none2: + "valid (Open p f flag fd None # s) \ cf2sfile (Open p f flag fd None # s) f' b = cf2sfile s f' b" +apply (frule vd_cons, frule vt_grant_os) +apply (induct f', simp add:cf2sfile_def) +apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps + get_parentfs_ctxts_simps) +done + +lemma cf2sfile_open_none: + "valid (Open p f flag fd None # s) \ cf2sfile (Open p f flag fd None # s) = cf2sfile s" +apply (rule ext, rule ext) +apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2) +done lemma sroot_only: "cf2sfile s [] = (\ b. if b then None else Some sroot)" @@ -26,12 +41,10 @@ "\valid (Open p f flag fd (Some inum) # s); f' \ current_files s\ \ cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) -apply (induct f', simp add:sroot_only) -apply simp +apply (case_tac "f = f'", simp) +apply (induct f', simp add:sroot_only, simp) apply (frule parentf_in_current', simp+) -apply (auto simp:cf2sfile_def split:if_splits option.splits) -apply (auto split:if_splits option.splits dest!:current_has_sec' - simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps get_parentfs_ctxts_simps) done @@ -56,6 +69,11 @@ | _ \ None) | None \ None)" apply (frule vd_cons, frule vt_grant_os, frule noroot_events) +apply (case_tac f, simp) +apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps + get_parentfs_ctxts_simps) +apply (rule impI) +thm not_deleted_imp_exists apply (auto split:if_splits option.splits dest!:current_has_sec' simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps get_parentfs_ctxts_simps) diff -r b6ee5f35c41f -r e9c5594d5963 Current_sockets_prop.thy --- a/Current_sockets_prop.thy Wed May 08 10:00:38 2013 +0800 +++ b/Current_sockets_prop.thy Thu May 09 11:19:44 2013 +0800 @@ -242,6 +242,21 @@ apply (case_tac t_sock_trans_state, case_tac [!] how) by auto +lemma is_tcp_sock_imp_curernt_proc: + "\is_tcp_sock s (p,fd); valid s\ \ p \ current_procs s" +apply (induct s) +apply (simp add:is_tcp_sock_nil is_init_tcp_sock_prop3) +apply (frule vd_cons, frule vt_grant_os, case_tac a) +by (auto simp:is_tcp_sock_simps split:if_splits option.splits t_socket_type.splits) + +lemma is_udp_sock_imp_curernt_proc: + "\is_udp_sock s (p,fd); valid s\ \ p \ current_procs s" +apply (induct s) +apply (simp add:is_udp_sock_nil is_init_udp_sock_prop3) +apply (frule vd_cons, frule vt_grant_os, case_tac a) +by (auto simp:is_udp_sock_simps split:if_splits option.splits t_socket_type.splits) + + (***** below should be adjusted after starting static analysis of sockets ! ??? ****) (* diff -r b6ee5f35c41f -r e9c5594d5963 Delete_prop.thy --- a/Delete_prop.thy Wed May 08 10:00:38 2013 +0800 +++ b/Delete_prop.thy Thu May 09 11:19:44 2013 +0800 @@ -1,5 +1,5 @@ theory Deleted_prop -imports Main Flask Flask_type Init_prop Alive_prop +imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop begin context flask begin @@ -10,21 +10,132 @@ lemma not_deleted_cons_D: "\ deleted obj (e # s) \ \ deleted obj s" by (auto dest:deleted_cons_I) -lemma not_deleted_imp_exists: +lemma not_deleted_init_file: + "\\ deleted (O_file f) s; valid s; is_init_file f\ \ is_file s f" +apply (induct s, simp add:is_init_file_prop1) +apply (frule vd_cons, frule vt_grant_os) +apply (case_tac a) prefer 6 apply (case_tac option) +apply (auto simp:is_file_simps split:option.splits) +done + +lemma not_deleted_init_dir: + "\\ deleted (O_dir f) s; valid s; is_init_dir f\ \ is_dir s f" +apply (induct s, simp add:is_init_dir_prop1) +apply (frule vd_cons, frule vt_grant_os) +apply (case_tac a) prefer 6 apply (case_tac option) +apply (auto simp:is_dir_simps split:option.splits) +done + +lemma not_deleted_init_proc: + "\\ deleted (O_proc p) s; p \ init_procs\ \ p \ current_procs s" +apply (induct s, simp) +by (case_tac a, auto) + +(**** ???*) +lemma current_fd_imp_current_proc: + "\fd \ current_proc_fds s p; valid s\ \ p \ current_procs s" +apply (induct s) +apply (simp add:init_fds_of_proc_prop1) +apply (frule vd_cons, drule vt_grant_os, case_tac a) +by (auto split:if_splits option.splits) + +lemma not_deleted_init_fd_aux: + "\\ deleted (O_fd p fd) s; valid s; fd \ init_fds_of_proc p\ + \ fd \ current_proc_fds s p \ \ deleted (O_proc p) s" +apply (induct s arbitrary: p, simp) +apply (frule vd_cons, drule vt_grant_os) +apply (case_tac a, auto dest:current_fd_imp_current_proc) +done + +lemma not_deleted_init_fd2: + "\\ deleted (O_fd p fd) s; fd \ init_fds_of_proc p; valid s\ \ \ deleted (O_proc p) s" +by (auto dest:not_deleted_init_fd_aux) + +lemma not_deleted_init_fd1: + "\\ deleted (O_fd p fd) s; valid s; fd \ init_fds_of_proc p\ \ fd \ current_proc_fds s p" +by (auto dest:not_deleted_init_fd_aux) + +lemma not_deleted_init_tcp_aux: + "\\ deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\ + \ is_tcp_sock s (p,fd) \ \ deleted (O_proc p) s" +apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1) +apply (frule vd_cons, frule vt_grant_os) +apply (case_tac a) prefer 6 apply (case_tac option) +by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits + dest:is_tcp_sock_imp_curernt_proc) + +lemma not_deleted_init_tcp1: + "\\ deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\ + \ is_tcp_sock s (p,fd)" +by (auto dest:not_deleted_init_tcp_aux) + +lemma not_deleted_init_tcp2: + "\\ deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\ + \ \ deleted (O_proc p) s" +by (auto dest:not_deleted_init_tcp_aux) + +lemma not_deleted_init_udp_aux: + "\\ deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\ + \ is_udp_sock s (p,fd) \ \ deleted (O_proc p) s" +apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1) +apply (frule vd_cons, frule vt_grant_os) +apply (case_tac a) prefer 6 apply (case_tac option) +by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits + dest:is_udp_sock_imp_curernt_proc) + +lemma not_deleted_init_udp1: + "\\ deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\ + \ is_udp_sock s (p,fd)" +by (auto dest:not_deleted_init_udp_aux) + +lemma not_deleted_init_udp2: + "\\ deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\ + \ \ deleted (O_proc p) s" +by (auto dest:not_deleted_init_udp_aux) + +lemma not_deleted_init_shm: + "\\ deleted (O_shm h) s; h \ init_shms\ \ h \ current_shms s" +apply (induct s, simp) +by (case_tac a, auto) + +lemma not_deleted_init_msgq: + "\\ deleted (O_msgq q) s; q \ init_msgqs\ \ q \ current_msgqs s" +apply (induct s, simp) +by (case_tac a, auto) + +lemma current_msg_imp_current_msgq: + "\m \ set (msgs_of_queue s q); valid s\ \ q \ current_msgqs s" +apply (induct s) +apply (simp add:init_msgs_valid) +apply (frule vd_cons, drule vt_grant_os) +apply (case_tac a, auto split:if_splits) +done + +lemma not_deleted_init_msg: + "\\ deleted (O_msg q m) s; valid s; m \ set (init_msgs_of_queue q)\ \ m \ set (msgs_of_queue s q)" +apply (induct s, simp) +apply (frule vd_cons, frule vt_grant_os) +apply (case_tac a, auto dest:current_msg_imp_current_msgq) +apply (case_tac "msgs_of_queue s q", simp+) +done + +lemma not_deleted_imp_alive: "\\ deleted obj s; valid s; init_alive obj\ \ alive s obj" -apply (induct s, simp add:init_alive_prop) -apply (frule vd_cons) -apply (case_tac a, auto simp:alive_simps split:t_object.splits) -pr 19 +apply (case_tac obj) +apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc + not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm + not_deleted_init_msgq + intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current + current_msg_imp_current_msgq) done lemma cons_app_simp_aux: "(a # b) @ c = a # (b @ c)" by auto -lemma not_deleted_imp_exists': - "\\ deleted obj (s'@s); exists s obj\ \ exists (s'@s) obj" +lemma not_deleted_imp_alive_app: + "\\ deleted obj (s'@s); alive s obj\ \ alive (s'@s) obj" apply (induct s', simp, simp only:cons_app_simp_aux) -apply (frule not_deleted_cons_D) +apply (frule not_deleted_cons_D, simp) apply (case_tac a, case_tac [!] obj, auto) done diff -r b6ee5f35c41f -r e9c5594d5963 Flask.thy --- a/Flask.thy Wed May 08 10:00:38 2013 +0800 +++ b/Flask.thy Thu May 09 11:19:44 2013 +0800 @@ -158,6 +158,7 @@ and init_procs_has_shm: "\ p h flag. (p,flag) \ init_procs_of_shm h \ p \ init_procs \ h \ init_shms" and init_msgs_distinct: "\ q. distinct (init_msgs_of_queue q)" + and init_msgs_valid: "\ m q. m \ set (init_msgs_of_queue q) \ q \ init_msgqs" and init_socket_has_inode: "\ p fd. (p, fd) \ init_sockets \ \ im. init_inum_of_socket (p, fd) = Some im \ p \ init_procs \ fd \ init_fds_of_proc p" and inos_has_sock_tag: "\ s im. init_inum_of_socket s = Some im \ s \ init_sockets \ (\ tag. init_itag_of_inum im = Some tag \ is_sock_itag tag)" @@ -735,11 +736,15 @@ (\ fd. obj = O_udp_sock (p', fd) \ is_udp_sock s (p',fd)) \ deleted obj s)" | "deleted obj (CloseFd p fd # s) = ((obj = O_fd p fd) \ (obj = O_tcp_sock (p,fd) \ is_tcp_sock s (p,fd)) \ - (obj = O_udp_sock (p,fd) \ is_udp_sock s (p, fd)) \ deleted obj s)" + (obj = O_udp_sock (p,fd) \ is_udp_sock s (p, fd)) \ + (\ f. obj = O_file f \ proc_fd_of_file s f = {(p, fd)} \ + f \ files_hung_by_del s) \ deleted obj s)" | "deleted obj (Execve p f fds # s) = ((\ fd \ current_proc_fds s p. obj = O_fd p fd \ fd \ fds) \ (\ fd. obj = O_tcp_sock (p, fd) \ is_tcp_sock s (p,fd) \ fd \ fds) \ (\ fd. obj = O_udp_sock (p, fd) \ is_udp_sock s (p,fd) \ fd \ fds) \ deleted obj s)" +| "deleted obj (Clone p p' fds shms # s) = ((\ fd \ current_proc_fds s p. obj = O_fd p' fd \ fd \ fds) \ + deleted obj s)" | "deleted obj (UnLink p f # s) = ((obj = O_file f) \ deleted obj s)" | "deleted obj (Rmdir p f # s) = ((obj = O_dir f) \ deleted obj s)" | "deleted obj (Exit p # s) = ((obj = O_proc p) \ (\ fd \ current_proc_fds s p. obj = O_fd p fd) \ diff -r b6ee5f35c41f -r e9c5594d5963 Init_prop.thy --- a/Init_prop.thy Wed May 08 10:00:38 2013 +0800 +++ b/Init_prop.thy Thu May 09 11:19:44 2013 +0800 @@ -90,6 +90,10 @@ lemma is_dir_nil: "is_dir [] = is_init_dir" by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits) +lemma is_udp_sock_nil: + "is_udp_sock [] k = is_init_udp_sock k" +by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits) + lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \ init_sockets \ is_udp_sock [] s)" apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props dest:init_socket_has_inode split:option.splits) @@ -100,7 +104,22 @@ dest:init_socket_has_inode split:option.splits) done -lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 +lemma is_init_udp_sock_prop3: + "is_init_udp_sock (p, fd) \ p \ init_procs" +by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits + dest:init_socket_has_inode inos_has_sock_tag) + +lemma is_init_udp_sock_prop4: + "is_init_udp_sock (p, fd) \ fd \ init_fds_of_proc p" +by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits + dest:init_socket_has_inode inos_has_sock_tag) + +lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3 + is_init_udp_sock_prop4 + +lemma is_tcp_sock_nil: + "is_tcp_sock [] k = is_init_tcp_sock k" +by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits) lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \ init_sockets \ is_tcp_sock [] s)" apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props @@ -112,8 +131,18 @@ dest:init_socket_has_inode split:option.splits) done -lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 +lemma is_init_tcp_sock_prop3: + "is_init_tcp_sock (p, fd) \ p \ init_procs" +by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits + dest:init_socket_has_inode inos_has_sock_tag) +lemma is_init_tcp_sock_prop4: + "is_init_tcp_sock (p, fd) \ fd \ init_fds_of_proc p" +by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits + dest:init_socket_has_inode inos_has_sock_tag) + +lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3 + is_init_tcp_sock_prop4 lemma init_parent_file_prop1: "\parent f = Some pf; f \ init_files\ \ is_init_dir pf"