(* Title: HOL/MicroJava/BV/JVM.thy

Author: Tobias Nipkow, Gerwin Klein

Copyright 2000 TUM

*)

header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}

theory JVM

imports Typing_Framework_JVM

begin

definition kiljvm :: "jvm_prog => nat => nat => ty => exception_table =>

instr list => JVMType.state list => JVMType.state list" where

"kiljvm G maxs maxr rT et bs ==

kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"

definition wt_kil :: "jvm_prog => cname => ty list => ty => nat => nat =>

exception_table => instr list => bool" where

"wt_kil G C pTs rT mxs mxl et ins ==

check_bounded ins et ∧ 0 < size ins ∧

(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));

start = OK first#(replicate (size ins - 1) (OK None));

result = kiljvm G mxs (1+size pTs+mxl) rT et ins start

in ∀n < size ins. result!n ≠ Err)"

definition wt_jvm_prog_kildall :: "jvm_prog => bool" where

"wt_jvm_prog_kildall G ==

wf_prog (λG C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"

theorem is_bcv_kiljvm:

"[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==>

is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)

(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"

apply (unfold kiljvm_def sl_triple_conv)

apply (rule is_bcv_kildall)

apply (simp (no_asm) add: sl_triple_conv [symmetric])

apply (force intro!: semilat_JVM_slI dest: wf_acyclic

simp add: symmetric sl_triple_conv)

apply (simp (no_asm) add: JVM_le_unfold)

apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype

dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)

apply (simp add: JVM_le_unfold)

apply (erule exec_pres_type)

apply assumption

apply (drule wf_prog_ws_prog, erule exec_mono, assumption)

done

lemma subset_replicate: "set (replicate n x) ⊆ {x}"

by (induct n) auto

lemma in_set_replicate:

"x ∈ set (replicate n y) ==> x = y"

proof -

assume "x ∈ set (replicate n y)"

also have "set (replicate n y) ⊆ {y}" by (rule subset_replicate)

finally have "x ∈ {y}" .

thus ?thesis by simp

qed

theorem wt_kil_correct:

assumes wf: "wf_prog wf_mb G"

assumes C: "is_class G C"

assumes pTs: "set pTs ⊆ types G"

assumes wtk: "wt_kil G C pTs rT maxs mxl et bs"

shows "∃phi. wt_method G C pTs rT maxs mxl bs et phi"

proof -

let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))

#(replicate (size bs - 1) (OK None))"

from wtk obtain maxr r where

bounded: "check_bounded bs et" and

result: "r = kiljvm G maxs maxr rT et bs ?start" and

success: "∀n < size bs. r!n ≠ Err" and

instrs: "0 < size bs" and

maxr: "maxr = Suc (length pTs + mxl)"

by (unfold wt_kil_def) simp

from bounded have "bounded (exec G maxs rT et bs) (size bs)"

by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)

with wf have bcv:

"is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)

(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"

by (rule is_bcv_kiljvm)

from C pTs instrs maxr

have "?start ∈ list (length bs) (states G maxs maxr)"

apply (unfold JVM_states_unfold)

apply (rule listI)

apply (auto intro: list_appendI dest!: in_set_replicate)

apply force

done

with bcv success result have

"∃ts∈list (length bs) (states G maxs maxr).

?start <=[JVMType.le G maxs maxr] ts ∧

wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"

by (unfold is_bcv_def) auto

then obtain phi' where

phi': "phi' ∈ list (length bs) (states G maxs maxr)" and

s: "?start <=[JVMType.le G maxs maxr] phi'" and

w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"

by blast

hence wt_err_step:

"wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"

by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)

from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"

by (drule_tac p=0 in le_listD) (simp add: lesub_def)+

from phi' have l: "size phi' = size bs" by simp

with instrs w have "phi' ! 0 ≠ Err" by (unfold wt_step_def) simp

with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"

by auto

from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)

also from w have "phi' = map OK (map ok_val phi')"

by (auto simp add: wt_step_def intro!: nth_equalityI)

finally

have check_types:

"check_types G maxs maxr (map OK (map ok_val phi'))" .

from l bounded

have "bounded (λpc. eff (bs!pc) G pc et) (length phi')"

by (simp add: exec_def check_bounded_is_bounded)

hence bounded': "bounded (exec G maxs rT et bs) (length bs)"

by (auto intro: bounded_lift simp add: exec_def l)

with wt_err_step

have "wt_app_eff (sup_state_opt G) (λpc. app (bs!pc) G maxs rT pc et)

(λpc. eff (bs!pc) G pc et) (map ok_val phi')"

by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)

with instrs l le bounded bounded' check_types maxr

have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"

apply (unfold wt_method_def wt_app_eff_def)

apply simp

apply (rule conjI)

apply (unfold wt_start_def)

apply (rule JVM_le_convert [THEN iffD1])

apply (simp (no_asm) add: phi0)

apply clarify

apply (erule allE, erule impE, assumption)

apply (elim conjE)

apply (clarsimp simp add: lesub_def wt_instr_def)

apply (simp add: exec_def)

apply (drule bounded_err_stepD, assumption+)

apply blast

done

thus ?thesis by blast

qed

theorem wt_kil_complete:

assumes wf: "wf_prog wf_mb G"

assumes C: "is_class G C"

assumes pTs: "set pTs ⊆ types G"

assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi"

shows "wt_kil G C pTs rT maxs mxl et bs"

proof -

let ?mxr = "1+size pTs+mxl"

from wtm obtain

instrs: "0 < length bs" and

len: "length phi = length bs" and

bounded: "check_bounded bs et" and

ck_types: "check_types G maxs ?mxr (map OK phi)" and

wt_start: "wt_start G C pTs mxl phi" and

wt_ins: "∀pc. pc < length bs -->

wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"

by (unfold wt_method_def) simp

from ck_types len

have istype_phi:

"map OK phi ∈ list (length bs) (states G maxs (1+size pTs+mxl))"

by (auto simp add: check_types_def intro!: listI)

let ?eff = "λpc. eff (bs!pc) G pc et"

let ?app = "λpc. app (bs!pc) G maxs rT pc et"

from bounded

have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"

by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)

from wt_ins

have "wt_app_eff (sup_state_opt G) ?app ?eff phi"

apply (unfold wt_app_eff_def wt_instr_def lesub_def)

apply (simp (no_asm) only: len)

apply blast

done

with bounded_exec

have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"

by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len)

hence wt_err:

"wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"

by (unfold exec_def) (simp add: len)

from wf bounded_exec

have is_bcv:

"is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs)

(size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)"

by (rule is_bcv_kiljvm)

let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))

#(replicate (size bs - 1) (OK None))"

from C pTs instrs

have start: "?start ∈ list (length bs) (states G maxs ?mxr)"

apply (unfold JVM_states_unfold)

apply (rule listI)

apply (auto intro!: list_appendI dest!: in_set_replicate)

apply force

done

let ?phi = "map OK phi"

have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi"

proof -

from len instrs

have "length ?start = length (map OK phi)" by simp

moreover

{ fix n

from wt_start

have "G \<turnstile> ok_val (?start!0) <=' phi!0"

by (simp add: wt_start_def)

moreover

from instrs len

have "0 < length phi" by simp

ultimately

have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)"

by (simp add: JVM_le_Err_conv Err.le_def lesub_def)

moreover

{ fix n'

have "JVMType.le G maxs ?mxr (OK None) (?phi!n)"

by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def

split: err.splits)

hence "[| n = Suc n'; n < length ?start |]

==> JVMType.le G maxs ?mxr (?start!n) (?phi!n)"

by simp

}

ultimately

have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)"

by (unfold lesub_def) (cases n, blast+)

}

ultimately show ?thesis by (rule le_listI)

qed

from wt_err

have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi"

by (simp add: wt_err_step_def JVM_le_Err_conv)

with start istype_phi less_phi is_bcv

have "∀p. p < length bs --> kiljvm G maxs ?mxr rT et bs ?start ! p ≠ Err"

by (unfold is_bcv_def) auto

with bounded instrs

show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp

qed

theorem jvm_kildall_sound_complete:

"wt_jvm_prog_kildall G = (∃Phi. wt_jvm_prog G Phi)"

proof

let ?Phi = "λC sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in

SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"

assume "wt_jvm_prog_kildall G"

hence "wt_jvm_prog G ?Phi"

apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)

apply (erule jvm_prog_lift)

apply (auto dest!: wt_kil_correct intro: someI)

done

thus "∃Phi. wt_jvm_prog G Phi" by fast

next

assume "∃Phi. wt_jvm_prog G Phi"

thus "wt_jvm_prog_kildall G"

apply (clarify)

apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)

apply (erule jvm_prog_lift)

apply (auto intro: wt_kil_complete)

done

qed

end