49 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
49 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
50 is_tcp_sock_simps is_udp_sock_simps |
50 is_tcp_sock_simps is_udp_sock_simps |
51 dest:is_dir_in_current split:if_splits option.splits) |
51 dest:is_dir_in_current split:if_splits option.splits) |
52 done |
52 done |
53 |
53 |
|
54 (* sock is not inherited on Execve, Clone cases, cause I simplified it with os_grant. |
|
55 * chunhan, 2013-11-20 |
54 lemma alive_execve: |
56 lemma alive_execve: |
55 "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = ( |
57 "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = ( |
56 \<lambda> obj. case obj of |
58 \<lambda> obj. case obj of |
57 O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd) |
59 O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd) |
58 else if (p = p') then False |
60 else if (p = p') then False |
66 | _ \<Rightarrow> alive s obj )" |
68 | _ \<Rightarrow> alive s obj )" |
67 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
69 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
68 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
70 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
69 is_tcp_sock_simps is_udp_sock_simps |
71 is_tcp_sock_simps is_udp_sock_simps |
70 dest:is_dir_in_current split:if_splits option.splits) |
72 dest:is_dir_in_current split:if_splits option.splits) |
|
73 |
71 done |
74 done |
72 |
75 |
73 lemma alive_clone: |
76 lemma alive_clone: |
74 "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = ( |
77 "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = ( |
75 \<lambda> obj. case obj of |
78 \<lambda> obj. case obj of |
88 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
91 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
89 is_tcp_sock_simps is_udp_sock_simps |
92 is_tcp_sock_simps is_udp_sock_simps |
90 intro:is_tcp_in_current is_udp_in_current |
93 intro:is_tcp_in_current is_udp_in_current |
91 dest:is_dir_in_current split:if_splits option.splits) |
94 dest:is_dir_in_current split:if_splits option.splits) |
92 done |
95 done |
|
96 *) |
|
97 |
|
98 lemma alive_execve: |
|
99 "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = ( |
|
100 \<lambda> obj. case obj of |
|
101 O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd) |
|
102 else if (p = p') then False |
|
103 else alive s (O_fd p' fd)) |
|
104 | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p') then False |
|
105 else alive s (O_tcp_sock (p', fd))) |
|
106 | O_udp_sock (p', fd) \<Rightarrow> (if (p = p') then False |
|
107 else alive s (O_udp_sock (p', fd))) |
|
108 | _ \<Rightarrow> alive s obj )" |
|
109 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
|
110 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
|
111 is_tcp_sock_simps is_udp_sock_simps |
|
112 dest:is_dir_in_current split:if_splits option.splits) |
|
113 apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto) |
|
114 |
|
115 done |
|
116 |
|
117 lemma alive_clone: |
|
118 "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = ( |
|
119 \<lambda> obj. case obj of |
|
120 O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj |
|
121 | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True |
|
122 else if (p'' = p') then False |
|
123 else alive s obj |
|
124 | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd)) |
|
125 else if (p'' = p') then False |
|
126 else alive s (O_tcp_sock (p'', fd))) |
|
127 | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd)) |
|
128 else if (p'' = p') then False |
|
129 else alive s (O_udp_sock (p'', fd))) |
|
130 | _ \<Rightarrow> alive s obj )" |
|
131 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
|
132 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
|
133 is_tcp_sock_simps is_udp_sock_simps |
|
134 intro:is_tcp_in_current is_udp_in_current |
|
135 dest:is_dir_in_current split:if_splits option.splits) |
|
136 done |
|
137 |
93 |
138 |
94 lemma alive_kill: |
139 lemma alive_kill: |
95 "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = ( |
140 "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = ( |
96 \<lambda> obj. case obj of |
141 \<lambda> obj. case obj of |
97 O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj |
142 O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj |