1(*  Title:      HOL/MicroJava/BV/JVM.thy
2    Author:     Tobias Nipkow, Gerwin Klein
3    Copyright   2000 TUM
4*)
5
6section \<open>Kildall for the JVM \label{sec:JVM}\<close>
7
8theory JVM
9imports Typing_Framework_JVM
10begin
11
12definition kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
13             instr list \<Rightarrow> JVMType.state list \<Rightarrow> JVMType.state list" where
14  "kiljvm G maxs maxr rT et bs ==
15  kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
16
17definition wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
18             exception_table \<Rightarrow> instr list \<Rightarrow> bool" where
19  "wt_kil G C pTs rT mxs mxl et ins ==
20   check_bounded ins et \<and> 0 < size ins \<and> 
21   (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
22        start  = OK first#(replicate (size ins - 1) (OK None));
23        result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
24    in \<forall>n < size ins. result!n \<noteq> Err)"
25
26definition wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool" where
27  "wt_jvm_prog_kildall G ==
28  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
29
30theorem is_bcv_kiljvm:
31  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
32      is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
33             (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
34  apply (unfold kiljvm_def sl_triple_conv)
35  apply (rule is_bcv_kildall)
36       apply (simp (no_asm) add: sl_triple_conv [symmetric]) 
37       apply (force intro!: semilat_JVM_slI dest: wf_acyclic 
38         simp add: symmetric sl_triple_conv)
39      apply (simp (no_asm) add: JVM_le_unfold)
40      apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
41                   dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
42     apply (simp add: JVM_le_unfold)
43    apply (erule exec_pres_type)
44   apply assumption
45  apply (drule wf_prog_ws_prog, erule exec_mono, assumption)  
46  done
47
48lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
49  by (induct n) auto
50
51lemma in_set_replicate:
52  "x \<in> set (replicate n y) \<Longrightarrow> x = y"
53proof -
54  assume "x \<in> set (replicate n y)"
55  also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate)
56  finally have "x \<in> {y}" .
57  thus ?thesis by simp
58qed
59
60theorem wt_kil_correct:
61  assumes wf:  "wf_prog wf_mb G"
62  assumes C:   "is_class G C"
63  assumes pTs: "set pTs \<subseteq> types G"
64  
65  assumes wtk: "wt_kil G C pTs rT maxs mxl et bs"
66  
67  shows "\<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
68proof -
69  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
70                #(replicate (size bs - 1) (OK None))"
71
72  from wtk obtain maxr r where    
73    bounded: "check_bounded bs et" and
74    result:  "r = kiljvm G maxs maxr rT et bs ?start" and
75    success: "\<forall>n < size bs. r!n \<noteq> Err" and
76    instrs:  "0 < size bs" and
77    maxr:    "maxr = Suc (length pTs + mxl)" 
78    by (unfold wt_kil_def) simp
79
80  from bounded have "bounded (exec G maxs rT et bs) (size bs)"
81    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
82  with wf have bcv:
83    "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 
84    (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
85    by (rule is_bcv_kiljvm)
86    
87  from C pTs instrs maxr
88  have "?start \<in> list (length bs) (states G maxs maxr)"
89    apply (unfold JVM_states_unfold)
90    apply (rule listI)
91    apply (auto intro: list_appendI dest!: in_set_replicate)
92    apply force
93    done    
94
95  with bcv success result have 
96    "\<exists>ts\<in>list (length bs) (states G maxs maxr).
97         ?start <=[JVMType.le G maxs maxr] ts \<and>
98         wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"
99    by (unfold is_bcv_def) auto
100  then obtain phi' where
101    phi': "phi' \<in> list (length bs) (states G maxs maxr)" and
102    s: "?start <=[JVMType.le G maxs maxr] phi'" and
103    w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
104    by blast
105  hence wt_err_step:
106    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
107    by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)
108
109  from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
110    by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
111
112  from phi' have l: "size phi' = size bs" by simp  
113  with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
114  with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
115    by auto
116
117  from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
118  also from w have "phi' = map OK (map ok_val phi')" 
119    by (auto simp add: wt_step_def intro!: nth_equalityI)
120  finally 
121  have check_types:
122    "check_types G maxs maxr (map OK (map ok_val phi'))" .
123
124  from l bounded 
125  have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
126    by (simp add: exec_def check_bounded_is_bounded)  
127  hence bounded': "bounded (exec G maxs rT et bs) (length bs)"
128    by (auto intro: bounded_lift simp add: exec_def l)
129  with wt_err_step
130  have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
131                   (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
132    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
133  with instrs l le bounded bounded' check_types maxr
134  have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
135    apply (unfold wt_method_def wt_app_eff_def)
136    apply simp
137    apply (rule conjI)
138     apply (unfold wt_start_def)
139     apply (rule JVM_le_convert [THEN iffD1])
140     apply (simp (no_asm) add: phi0)
141    apply clarify
142    apply (erule allE, erule impE, assumption)
143    apply (elim conjE)
144    apply (clarsimp simp add: lesub_def wt_instr_def)
145    apply (simp add: exec_def)
146    apply (drule bounded_err_stepD, assumption+)
147    apply blast
148    done
149
150  thus ?thesis by blast
151qed
152
153
154theorem wt_kil_complete:
155  assumes wf:  "wf_prog wf_mb G"  
156  assumes C:   "is_class G C"
157  assumes pTs: "set pTs \<subseteq> types G"
158
159  assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi"
160
161  shows "wt_kil G C pTs rT maxs mxl et bs"
162proof -
163  let ?mxr = "1+size pTs+mxl"
164  
165  from wtm obtain
166    instrs:   "0 < length bs" and
167    len:      "length phi = length bs" and
168    bounded:  "check_bounded bs et" and
169    ck_types: "check_types G maxs ?mxr (map OK phi)" and
170    wt_start: "wt_start G C pTs mxl phi" and
171    wt_ins:   "\<forall>pc. pc < length bs \<longrightarrow> 
172                    wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"
173    by (unfold wt_method_def) simp
174
175  from ck_types len
176  have istype_phi: 
177    "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
178    by (auto simp add: check_types_def intro!: listI)
179
180  let ?eff  = "\<lambda>pc. eff (bs!pc) G pc et"
181  let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
182
183  from bounded
184  have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
185    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
186 
187  from wt_ins
188  have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
189    apply (unfold wt_app_eff_def wt_instr_def lesub_def)
190    apply (simp (no_asm) only: len)
191    apply blast
192    done
193  with bounded_exec
194  have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
195    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len)
196  hence wt_err:
197    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
198    by (unfold exec_def) (simp add: len)
199 
200  from wf bounded_exec
201  have is_bcv: 
202    "is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) 
203            (size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)"
204    by (rule is_bcv_kiljvm)
205
206  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
207                #(replicate (size bs - 1) (OK None))"
208
209  from C pTs instrs
210  have start: "?start \<in> list (length bs) (states G maxs ?mxr)"
211    apply (unfold JVM_states_unfold)
212    apply (rule listI)
213    apply (auto intro!: list_appendI dest!: in_set_replicate)
214    apply force
215    done    
216
217  let ?phi = "map OK phi"  
218  have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi"
219  proof -
220    from len instrs
221    have "length ?start = length (map OK phi)" by simp
222    moreover
223    { fix n
224      from wt_start
225      have "G \<turnstile> ok_val (?start!0) <=' phi!0"
226        by (simp add: wt_start_def)
227      moreover
228      from instrs len
229      have "0 < length phi" by simp
230      ultimately
231      have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)"
232        by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
233      moreover
234      { fix n'
235        have "JVMType.le G maxs ?mxr (OK None) (?phi!n)"
236          by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
237            split: err.splits)        
238        hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> 
239          \<Longrightarrow> JVMType.le G maxs ?mxr (?start!n) (?phi!n)"
240          by simp
241      }
242      ultimately
243      have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)"
244        by (unfold lesub_def) (cases n, blast+)
245    } 
246    ultimately show ?thesis by (rule le_listI)
247  qed         
248
249  from wt_err
250  have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi"
251    by (simp add: wt_err_step_def JVM_le_Err_conv)  
252  with start istype_phi less_phi is_bcv
253  have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?mxr rT et bs ?start ! p \<noteq> Err"
254    by (unfold is_bcv_def) auto
255  with bounded instrs
256  show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
257qed
258
259
260theorem jvm_kildall_sound_complete:
261  "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
262proof 
263  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
264              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
265  
266  assume "wt_jvm_prog_kildall G"
267  hence "wt_jvm_prog G ?Phi"
268    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
269    apply (erule jvm_prog_lift)
270    apply (auto dest!: wt_kil_correct intro: someI)
271    done
272  thus "\<exists>Phi. wt_jvm_prog G Phi" by fast
273next
274  assume "\<exists>Phi. wt_jvm_prog G Phi"
275  thus "wt_jvm_prog_kildall G"
276    apply (clarify)
277    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
278    apply (erule jvm_prog_lift)
279    apply (auto intro: wt_kil_complete)
280    done
281qed
282
283end
284