--- a/src/HOL/MicroJava/BV/BVExample.thy Fri Jun 14 13:24:32 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Fri Jun 14 23:25:36 2002 +0200
@@ -252,11 +252,27 @@
( [], [Class list_name, Class list_name]),
( [PrimT Void], [Class list_name, Class list_name])]"
+
+lemma bounded_append [simp]:
+ "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
+ apply (simp add: check_bounded_def)
+ apply (simp add: nat_number append_ins_def)
+ apply (rule allI, rule impI)
+ apply (elim pc_end pc_next pc_0)
+ apply auto
+ done
+
+lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"
+ apply (auto simp add: check_types_def phi_append_def JVM_states_unfold)
+ apply (unfold list_def)
+ apply auto
+ done
+
lemma wt_append [simp]:
"wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
[(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
- apply (simp add: wt_method_def append_ins_def phi_append_def
- wt_start_def wt_instr_def)
+ apply (simp add: wt_method_def wt_start_def wt_instr_def)
+ apply (simp add: phi_append_def append_ins_def)
apply clarify
apply (elim pc_end pc_next pc_0)
apply simp
@@ -277,42 +293,57 @@
text {* Some abbreviations for readability *}
syntax
- list :: ty
- test :: ty
+ Clist :: ty
+ Ctest :: ty
translations
- "list" == "Class list_name"
- "test" == "Class test_name"
+ "Clist" == "Class list_name"
+ "Ctest" == "Class test_name"
constdefs
phi_makelist :: method_type ("\<phi>\<^sub>m")
"\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [
- ( [], [OK test, Err , Err ]),
- ( [list], [OK test, Err , Err ]),
- ( [list, list], [OK test, Err , Err ]),
- ( [list], [OK list, Err , Err ]),
- ( [PrimT Integer, list], [OK list, Err , Err ]),
- ( [], [OK list, Err , Err ]),
- ( [list], [OK list, Err , Err ]),
- ( [list, list], [OK list, Err , Err ]),
- ( [list], [OK list, OK list, Err ]),
- ( [PrimT Integer, list], [OK list, OK list, Err ]),
- ( [], [OK list, OK list, Err ]),
- ( [list], [OK list, OK list, Err ]),
- ( [list, list], [OK list, OK list, Err ]),
- ( [list], [OK list, OK list, OK list]),
- ( [PrimT Integer, list], [OK list, OK list, OK list]),
- ( [], [OK list, OK list, OK list]),
- ( [list], [OK list, OK list, OK list]),
- ( [list, list], [OK list, OK list, OK list]),
- ( [PrimT Void], [OK list, OK list, OK list]),
- ( [], [OK list, OK list, OK list]),
- ( [list], [OK list, OK list, OK list]),
- ( [list, list], [OK list, OK list, OK list]),
- ( [PrimT Void], [OK list, OK list, OK list])]"
+ ( [], [OK Ctest, Err , Err ]),
+ ( [Clist], [OK Ctest, Err , Err ]),
+ ( [Clist, Clist], [OK Ctest, Err , Err ]),
+ ( [Clist], [OK Clist, Err , Err ]),
+ ( [PrimT Integer, Clist], [OK Clist, Err , Err ]),
+ ( [], [OK Clist, Err , Err ]),
+ ( [Clist], [OK Clist, Err , Err ]),
+ ( [Clist, Clist], [OK Clist, Err , Err ]),
+ ( [Clist], [OK Clist, OK Clist, Err ]),
+ ( [PrimT Integer, Clist], [OK Clist, OK Clist, Err ]),
+ ( [], [OK Clist, OK Clist, Err ]),
+ ( [Clist], [OK Clist, OK Clist, Err ]),
+ ( [Clist, Clist], [OK Clist, OK Clist, Err ]),
+ ( [Clist], [OK Clist, OK Clist, OK Clist]),
+ ( [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]),
+ ( [], [OK Clist, OK Clist, OK Clist]),
+ ( [Clist], [OK Clist, OK Clist, OK Clist]),
+ ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
+ ( [PrimT Void], [OK Clist, OK Clist, OK Clist]),
+ ( [], [OK Clist, OK Clist, OK Clist]),
+ ( [Clist], [OK Clist, OK Clist, OK Clist]),
+ ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
+ ( [PrimT Void], [OK Clist, OK Clist, OK Clist])]"
+
+lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
+ apply (simp add: check_bounded_def)
+ apply (simp add: nat_number make_list_ins_def)
+ apply (rule allI, rule impI)
+ apply (elim pc_end pc_next pc_0)
+ apply auto
+ done
+
+lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)"
+ apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)
+ apply (unfold list_def)
+ apply auto
+ done
lemma wt_makelist [simp]:
"wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
- apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
+ apply (simp add: wt_method_def)
+ apply (simp add: make_list_ins_def phi_makelist_def)
apply (simp add: wt_start_def nat_number)
apply (simp add: wt_instr_def)
apply clarify
@@ -375,8 +406,8 @@
section "Example for code generation: inferring method types"
constdefs
- test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty List.list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
- exception_table \<Rightarrow> instr List.list \<Rightarrow> JVMType.state List.list"
+ test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
+ exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list"
"test_kil G C pTs rT mxs mxl et instr ==
(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
start = OK first#(replicate (size instr - 1) (OK None))
--- a/src/HOL/MicroJava/BV/BVSpec.thy Fri Jun 14 13:24:32 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Jun 14 23:25:36 2002 +0200
@@ -16,29 +16,70 @@
*}
constdefs
+ -- "The program counter will always be inside the method:"
+ check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
+ "check_bounded ins et \<equiv>
+ (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
+ (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
+
+ -- "The method type only contains declared classes:"
+ check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
+ "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
+
+ -- "An instruction is welltyped if it is applicable and its effect"
+ -- "is compatible with the type at all successor instructions:"
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
exception_table,p_count] \<Rightarrow> bool"
- "wt_instr i G rT phi mxs max_pc et pc ==
+ "wt_instr i G rT phi mxs max_pc et pc \<equiv>
app i G mxs rT pc et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
+ -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
"wt_start G C pTs mxl phi ==
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
+ -- "A method is welltyped if the body is not empty, if execution does not"
+ -- "leave the body, if the method type covers all instructions and mentions"
+ -- "declared classes only, if the method calling convention is respected, and"
+ -- "if all instructions are welltyped."
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
exception_table,method_type] \<Rightarrow> bool"
- "wt_method G C pTs rT mxs mxl ins et phi ==
+ "wt_method G C pTs rT mxs mxl ins et phi \<equiv>
let max_pc = length ins in
- 0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
+ 0 < max_pc \<and>
+ length phi = length ins \<and>
+ check_bounded ins et \<and>
+ check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
+ wt_start G C pTs mxl phi \<and>
+ (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc)"
+ -- "A program is welltyped if it is wellformed and all methods are welltyped"
wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
"wt_jvm_prog G phi ==
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
+lemma check_boundedD:
+ "\<lbrakk> check_bounded ins et; pc < length ins;
+ (pc',s') \<in> set (eff (ins!pc) G pc et s) \<rbrakk> \<Longrightarrow>
+ pc' < length ins"
+ apply (unfold eff_def)
+ apply simp
+ apply (unfold check_bounded_def)
+ apply clarify
+ apply (erule disjE)
+ apply blast
+ apply (erule allE, erule impE, assumption)
+ apply (unfold xcpt_eff_def)
+ apply clarsimp
+ apply (drule xcpt_names_in_et)
+ apply clarify
+ apply (drule bspec, assumption)
+ apply simp
+ done
+
lemma wt_jvm_progD:
"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
@@ -46,10 +87,28 @@
lemma wt_jvm_prog_impl_wt_instr:
"\<lbrakk> wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk>
- \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
+ \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
+text {*
+ We could leave out the check @{term "pc' < max_pc"} in the
+ definition of @{term wt_instr} in the context of @{term wt_method}.
+*}
+lemma wt_instr_def2:
+ "\<lbrakk> wt_jvm_prog G Phi; is_class G C;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins;
+ i = ins!pc; phi = Phi C sig; max_pc = length ins \<rbrakk>
+ \<Longrightarrow> wt_instr i G rT phi maxs max_pc et pc =
+ (app i G maxs rT pc et (phi!pc) \<and>
+ (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). G \<turnstile> s' <=' phi!pc'))"
+apply (simp add: wt_instr_def)
+apply (unfold wt_jvm_prog_def)
+apply (drule method_wf_mdecl)
+apply (simp, simp, simp add: wf_mdecl_def wt_method_def)
+apply (auto dest: check_boundedD)
+done
+
lemma wt_jvm_prog_impl_wt_start:
"\<lbrakk> wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow>
--- a/src/HOL/MicroJava/BV/JVM.thy Fri Jun 14 13:24:32 2002 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy Fri Jun 14 23:25:36 2002 +0200
@@ -10,10 +10,6 @@
constdefs
- check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
- "check_bounded ins et \<equiv> (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
- (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
-
exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
"exec G maxs rT et bs ==
err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
@@ -78,23 +74,8 @@
*}
lemma check_bounded_is_bounded:
- "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
- apply (unfold bounded_def eff_def)
- apply clarify
- apply simp
- apply (unfold check_bounded_def)
- apply clarify
- apply (erule disjE)
- apply blast
- apply (erule allE, erule impE, assumption)
- apply (unfold xcpt_eff_def)
- apply clarsimp
- apply (drule xcpt_names_in_et)
- apply clarify
- apply (drule bspec, assumption)
- apply simp
- done
-
+ "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
+ by (unfold bounded_def) (blast dest: check_boundedD)
lemma special_ex_swap_lemma [iff]:
"(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
@@ -315,6 +296,8 @@
apply (erule exec_mono, assumption)
done
+lemma map_id: "\<forall>x \<in> set xs. f (g x) = x \<Longrightarrow> map f (map g xs) = xs"
+ by (induct xs) auto
theorem wt_kil_correct:
"\<lbrakk> wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G;
@@ -367,7 +350,7 @@
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
- l: "phi' \<in> list (length bs) (states G maxs maxr)" and
+ phi': "phi' \<in> 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
@@ -378,10 +361,22 @@
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 l have l: "size phi' = size bs" by simp
+ from phi' have l: "size phi' = size bs" by simp
with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
- by (clarsimp simp add: not_Err_eq)
+ by (clarsimp simp add: not_Err_eq)
+
+ 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')"
+ apply (clarsimp simp add: wt_step_def)
+ apply (rule map_id [symmetric])
+ apply (clarsimp simp add: in_set_conv_decomp)
+ apply (erule_tac x = "length ys" in allE)
+ apply (clarsimp simp add: nth_append not_Err_eq)
+ done
+ finally
+ have check_types:
+ "check_types G maxs maxr (map OK (map ok_val phi'))" .
from l bounded
have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
@@ -392,7 +387,7 @@
have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et)
(\<lambda>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'
+ 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
@@ -415,26 +410,32 @@
theorem wt_kil_complete:
"\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G;
- check_bounded bs et; length phi = length bs; is_class G C;
- \<forall>x \<in> set pTs. is_type G x;
- map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
+ is_class G C;
+ \<forall>x \<in> set pTs. is_type G x \<rbrakk>
\<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
proof -
assume wf: "wf_prog wf_mb G"
assume isclass: "is_class G C"
assume istype: "\<forall>x \<in> set pTs. is_type G x"
- assume length: "length phi = length bs"
- assume istype_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
- assume bounded: "check_bounded bs et"
-
+
+ let ?mxr = "1+size pTs+mxl"
+
assume "wt_method G C pTs rT maxs mxl bs et phi"
then 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: "\<forall>pc. pc < length bs \<longrightarrow>
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 \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
+ by (auto simp add: check_types_def intro!: listI)
+
let ?eff = "\<lambda>pc. eff (bs!pc) G pc et"
let ?app = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
@@ -445,15 +446,15 @@
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: length)
+ 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 length)
+ 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: length)
+ by (unfold exec_def) (simp add: len)
let ?maxr = "1+size pTs+mxl"
from wf bounded_exec
@@ -487,7 +488,7 @@
let ?phi = "map OK phi"
have less_phi: "?start <=[JVMType.le G maxs ?maxr] ?phi"
proof -
- from length instrs
+ from len instrs
have "length ?start = length (map OK phi)" by simp
moreover
{ fix n
@@ -495,7 +496,7 @@
have "G \<turnstile> ok_val (?start!0) <=' phi!0"
by (simp add: wt_start_def)
moreover
- from instrs length
+ from instrs len
have "0 < length phi" by simp
ultimately
have "JVMType.le G maxs ?maxr (?start!0) (?phi!0)"
@@ -525,35 +526,7 @@
with bounded instrs
show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
qed
-text {*
- The above theorem @{text wt_kil_complete} is all nice'n shiny except
- for one assumption: @{term "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"}
- It does not hold for all @{text phi} that satisfy @{text wt_method}.
- The assumption states mainly that all entries in @{text phi} are legal
- types in the program context, that the stack size is bounded by @{text maxs},
- and that the register sizes are exactly @{term "1+size pTs+mxl"}.
- The BV specification, i.e.~@{text wt_method}, only gives us this
- property for \emph{reachable} code. For unreachable code,
- e.g.~unused registers may contain arbitrary garbage. Even the stack
- and register sizes can be different from the rest of the program (as
- long as they are consistent inside each chunk of unreachable code).
-
- All is not lost, though: for each @{text phi} that satisfies
- @{text wt_method} there is a @{text phi'} that also satisfies
- @{text wt_method} and that additionally satisfies our assumption.
- The construction is quite easy: the entries for reachable code
- are the same in @{text phi} and @{text phi'}, the entries for
- unreachable code are all @{text None} in @{text phi'} (as it would
- be produced by Kildall's algorithm).
-
- Although this is proved easily by comment, it requires some more
- overhead (i.e.~talking about reachable instructions) if you try
- it the hard way. Thus it is missing here for the time being.
-
- The other direction (@{text wt_kil_correct}) can be lifted to
- programs without problems:
-*}
lemma is_type_pTs:
"\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls;
t \<in> set (snd sig) \<rbrakk>
@@ -573,9 +546,9 @@
qed
-theorem jvm_kildall_correct:
- "wt_jvm_prog_kildall G \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
-proof -
+theorem jvm_kildall_sound_complete:
+ "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
+proof
assume wtk: "wt_jvm_prog_kildall G"
then obtain wf_mb where
@@ -605,8 +578,34 @@
apply (auto intro: someI)
done
- thus ?thesis by blast
+ thus "\<exists>Phi. wt_jvm_prog G Phi" by blast
+next
+ assume "\<exists>Phi. wt_jvm_prog G Phi"
+ then obtain Phi where wt: "wt_jvm_prog G Phi" ..
+
+ then obtain wf_mb where
+ wf: "wf_prog wf_mb G"
+ by (auto simp add: wt_jvm_prog_def)
+
+ { fix C S fs mdecls sig rT code
+ assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
+ with wf
+ have "method (G,C) sig = Some (C,rT,code) \<and> is_class G C \<and> (\<forall>t \<in> set (snd sig). is_type G t)"
+ by (simp add: methd is_type_pTs)
+ } note this [simp]
+
+ from wt
+ show "wt_jvm_prog_kildall G"
+ apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def)
+ apply clarsimp
+ apply (drule bspec, assumption)
+ apply (unfold wf_mdecl_def)
+ apply clarsimp
+ apply (drule bspec, assumption)
+ apply clarsimp
+ apply (drule wt_kil_complete [OF _ wf])
+ apply (auto intro: someI)
+ done
qed
-
end