(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: BVExec.html 1910 2004-05-19 04:46:04Z kleing $
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
theory BVExec = Abstract_BV + TF_JVM:
constdefs
kiljvm :: "jvm_prog => nat => nat => ty =>
instr list => ex_table => tyi' err list => tyi' err list"
"kiljvm P mxs mxl Tr is xt ≡
kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl)
(exec P mxs Tr xt is)"
wt_kildall :: "jvm_prog => cname => ty list => ty => nat => nat =>
instr list => ex_table => bool"
"wt_kildall P C' Ts Tr mxs mxl0 is xt ≡
0 < size is ∧
(let first = Some ([],[OK (Class C')]@(map OK Ts)@(replicate mxl0 Err));
start = OK first#(replicate (size is - 1) (OK None));
result = kiljvm P mxs (1+size Ts+mxl0) Tr is xt start
in ∀n < size is. result!n ≠ Err)"
wf_jvm_progk :: "jvm_prog => bool"
"wf_jvm_progk P ≡
wf_prog (λP C' (M,Ts,Tr,(mxs,mxl0,is,xt)). wt_kildall P C' Ts Tr mxs mxl0 is xt) P"
theorem (in start_context) is_bcv_kiljvm:
"is_bcv r Err step (size is) A (kiljvm P mxs mxl Tr is xt)"
(*<*)
apply (insert wf)
apply (unfold kiljvm_def)
apply (fold r_def f_def step_def_exec)
apply (rule is_bcv_kildall)
apply simp
apply (fold sl_def2, erule semilat_JVM)
apply simp
apply blast
apply (simp add: JVM_le_unfold)
apply (rule exec_pres_type)
apply (rule bounded_step)
apply (erule step_mono)
done
(*>*)
(* FIXME: move? *)
lemma subset_replicate [intro?]: "set (replicate n x) ⊆ {x}"
by (induct n) auto
lemma in_set_replicate:
assumes "x ∈ set (replicate n y)"
shows "x = y"
(*<*)
proof -
note prems
also have "set (replicate n y) ⊆ {y}" ..
finally show ?thesis by simp
qed
(*>*)
lemma (in start_context) start_in_A [intro?]:
"0 < size is ==> start ∈ list (size is) A"
using Ts C
(*<*)
apply (simp add: JVM_states_unfold)
apply (force intro!: listI list_appendI dest!: in_set_replicate)
done
(*>*)
theorem (in start_context) wt_kil_correct:
assumes wtk: "wt_kildall P C Ts Tr mxs mxl0 is xt"
shows "∃τs. wt_method P C Ts Tr mxs mxl0 is xt τs"
(*<*)
proof -
from wtk obtain res where
result: "res = kiljvm P mxs mxl Tr is xt start" and
success: "∀n < size is. res!n ≠ Err" and
instrs: "0 < size is"
by (unfold wt_kildall_def) simp
have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl Tr is xt)"
by (rule is_bcv_kiljvm)
from instrs have "start ∈ list (size is) A" ..
with bcv success result have
"∃ts∈list (size is) A. start [\<sqsubseteq>r] ts ∧ wt_step r Err step ts"
by (unfold is_bcv_def) blast
then obtain τs' where
in_A: "τs' ∈ list (size is) A" and
s: "start [\<sqsubseteq>r] τs'" and
w: "wt_step r Err step τs'"
by blast
hence wt_err_step: "wt_err_step (sup_state_opt P) step τs'"
by (simp add: wt_err_step_def JVM_le_Err_conv)
from in_A have l: "size τs' = size is" by simp
moreover {
from in_A have "check_types P mxs mxl τs'" by (simp add: check_types_def)
also from w have "∀x ∈ set τs'. x ≠ Err"
by (auto simp add: wt_step_def all_set_conv_all_nth)
hence [symmetric]: "map OK (map ok_val τs') = τs'"
by (auto intro!: map_idI simp add: wt_step_def map_compose [symmetric])
finally have "check_types P mxs mxl (map OK (map ok_val τs'))" .
}
moreover {
from s have "start!0 \<sqsubseteq>r τs'!0" by (rule le_listD) simp
moreover
from instrs w l
have "τs'!0 ≠ Err" by (unfold wt_step_def) simp
then obtain τs0 where "τs'!0 = OK τs0" by auto
ultimately
have "wt_start P C Ts mxl0 (map ok_val τs')" using l instrs
by (unfold wt_start_def)
(simp add: lesub_def JVM_le_Err_conv Err.le_def)
}
moreover
from in_A have "set τs' ⊆ A" by simp
with wt_err_step bounded_step
have "wt_app_eff (sup_state_opt P) app eff (map ok_val τs')"
by (auto intro: wt_err_imp_wt_app_eff simp add: l)
ultimately
have "wt_method P C Ts Tr mxs mxl0 is xt (map ok_val τs')"
using instrs by (simp add: wt_method_def2 check_types_def)
thus ?thesis by blast
qed
(*>*)
theorem (in start_context) wt_kil_complete:
assumes wtm: "wt_method P C Ts Tr mxs mxl0 is xt τs"
shows "wt_kildall P C Ts Tr mxs mxl0 is xt"
(*<*)
proof -
from wtm obtain
instrs: "0 < size is" and
length: "length τs = length is" and
ck_type: "check_types P mxs mxl (map OK τs)" and
wt_start: "wt_start P C Ts mxl0 τs" and
app_eff: "wt_app_eff (sup_state_opt P) app eff τs"
by (simp add: wt_method_def2 check_types_def)
from ck_type
have in_A: "set (map OK τs) ⊆ A"
by (simp add: check_types_def)
with app_eff in_A bounded_step
have "wt_err_step (sup_state_opt P) (err_step (size τs) app eff) (map OK τs)"
by - (erule wt_app_eff_imp_wt_err,
auto simp add: exec_def length states_def)
hence wt_err: "wt_err_step (sup_state_opt P) step (map OK τs)"
by (simp add: length)
have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl Tr is xt)"
by (rule is_bcv_kiljvm)
moreover from instrs have "start ∈ list (size is) A" ..
moreover
let ?τs = "map OK τs"
have less_τs: "start [\<sqsubseteq>r] ?τs"
proof (rule le_listI)
from length instrs
show "length start = length (map OK τs)" by simp
next
fix n
from wt_start have "P \<turnstile> ok_val (start!0) ≤' τs!0"
by (simp add: wt_start_def)
moreover from instrs length have "0 < length τs" by simp
ultimately have "start!0 \<sqsubseteq>r ?τs!0"
by (simp add: JVM_le_Err_conv lesub_def)
moreover {
fix n'
have "OK None \<sqsubseteq>r ?τs!n"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
hence "[|n = Suc n'; n < size start|] ==> start!n \<sqsubseteq>r ?τs!n" by simp
}
ultimately
show "n < size start ==> start!n \<sqsubseteq>r ?τs!n" by (cases n, blast+)
qed
moreover
from ck_type length
have "?τs ∈ list (size is) A"
by (auto intro!: listI simp add: check_types_def)
moreover
from wt_err have "wt_step r Err step ?τs"
by (simp add: wt_err_step_def JVM_le_Err_conv)
ultimately
have "∀p. p < size is --> kiljvm P mxs mxl Tr is xt start ! p ≠ Err"
by (unfold is_bcv_def) blast
with instrs
show "wt_kildall P C Ts Tr mxs mxl0 is xt" by (unfold wt_kildall_def) simp
qed
(*>*)
theorem jvm_kildall_correct:
"wf_jvm_progk P = wf_jvm_prog P"
(*<*)
proof
let ?Φ = "λC M. let (C,Ts,Tr,(mxs,mxl0,is,xt)) = method P C M in
SOME τs. wt_method P C Ts Tr mxs mxl0 is xt τs"
-- "soundness"
assume wt: "wf_jvm_progk P"
hence "wf_jvm_prog?Φ P"
apply (unfold wf_jvm_prog_phi_def wf_jvm_progk_def)
apply (erule wf_prog_lift)
apply (auto dest!: start_context.wt_kil_correct [OF start_context.intro]
intro: someI)
apply (erule sees_method_is_class)
done
thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
next
-- "completeness"
assume wt: "wf_jvm_prog P"
thus "wf_jvm_progk P"
apply (unfold wf_jvm_prog_def wf_jvm_prog_phi_def wf_jvm_progk_def)
apply (clarify)
apply (erule wf_prog_lift)
apply (auto intro!: start_context.wt_kil_complete start_context.intro)
apply (erule sees_method_is_class)
done
qed
(*>*)
end
theorem is_bcv_kiljvm:
start_context P Ts p C ==> is_bcv (JVM_SemiType.le P mxs (1 + length Ts + mxl0)) Err (err_step (length is) (%pc. app (is ! pc) P mxs Tr pc (length is) xt) (%pc. eff (is ! pc) P pc xt)) (length is) (states P mxs (1 + length Ts + mxl0)) (kiljvm P mxs (1 + length Ts + mxl0) Tr is xt)
lemma subset_replicate:
set (replicate n x) <= {x}
lemma
x : set (replicate n y) ==> x = y
lemma start_in_A:
[| start_context P Ts p C; 0 < length is |] ==> OK ⌊([], OK (Class C) # map OK Ts @ replicate mxl0 Err)⌋ # replicate (length is - 1) (OK None) : list (length is) (states P mxs (1 + length Ts + mxl0))
theorem
[| start_context P Ts p C; wt_kildall P C Ts Tr mxs mxl0 is xt |] ==> EX τs. wt_method P C Ts Tr mxs mxl0 is xt τs
theorem
[| start_context P Ts p C; wt_method P C Ts Tr mxs mxl0 is xt τs |] ==> wt_kildall P C Ts Tr mxs mxl0 is xt
theorem jvm_kildall_correct:
wf_jvm_progk P = wf_jvm_prog P