WT.thy
Back to the index of BV_ASCII
WT = Convert +
types
locvars_type = any list
opstack_type = tys list
state_type = "opstack_type * locvars_type"
constdefs
sup_loc :: "[locvars_type,locvars_type] => bool" ("_ >>= _" [71,71] 70)
"LT >>= LT' == (length LT=length LT') & (!(t,t'):set (zip LT LT'). t >= t')"
sup_state :: "state_type => state_type => bool" ("_ >>>= _" [71,71] 70)
"s >>>= s' == map US (fst s) >>= map US (fst s') & snd s >>= snd s'"
types
method_type = "state_type list"
class_type = "method_loc => method_type"
prog_type = "cname => class_type"
(************************************************************************************)
constdefs
ins_type_tys_ok :: "[ins_type,tys] => bool"
"ins_type_tys_ok X ts ==
case X of
I_ => ts = PTS Integer
| A_ => ? rs. ts = RTS rs"
consts
wt_LAS :: "[load_and_store,method_type,p_count,p_count] => bool"
primrec
"wt_LAS (X load idx) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
idx < length LT &
(? ts. (LT ! idx) = US ts & ins_type_tys_ok X ts &
phi ! (pc+1) >>>= (ts # ST , LT)))"
"wt_LAS (X store idx) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
idx < length LT &
(? ts ST'. ST = ts # ST' & ins_type_tys_ok X ts &
phi ! (pc+1) >>>= (ST' , LT[idx:=US ts])))"
"wt_LAS (Bipush i) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
phi ! (pc+1) >>>= ((PTS Integer) # ST , LT))"
"wt_LAS (Aconst_null) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
phi ! (pc+1) >>>= ((RTS [NT]) # ST , LT))"
consts
wt_MO :: "[manipulate_object,bytecode,cpool,method_type,p_count,p_count] => bool"
primrec
"wt_MO (Getfield idx) CFS cp phi max_pc pc =
(let (ST,LT) = phi ! pc;
(fc,fn,fd) = extract_Fieldref cp idx
in
pc+1 < max_pc &
is_class CFS fc &
get_fields (CFS !! fc) (fc,fn) = Some fd &
(? rs ST'. ST = (RTS rs) # ST' &
wideRefsConvertible CFS rs [CT fc] &
phi ! (pc+1) >>>= ((fd2tys CFS fd) # ST' , LT)))"
"wt_MO (Putfield idx) CFS cp phi max_pc pc =
(let (ST,LT) = phi ! pc;
(fc,fn,fd) = extract_Fieldref cp idx
in
pc+1 < max_pc &
is_class CFS fc &
get_fields (CFS !! fc) (fc,fn) = Some fd &
(? tys rs ST'. ST = tys # (RTS rs) # ST' &
wideRefsConvertible CFS rs [CT fc] &
assConvertible CFS tys (fd2tys CFS fd) &
phi ! (pc+1) >>>= (ST' , LT)))"
constdefs
ins_type_tysl_ok :: "[ins_type,tys list] => bool"
"ins_type_tysl_ok X ts ==
case X of
I_ => ts = [PTS Integer]
| A_ => ? rs. ts = map RTS rs"
tysl2tys :: "[ins_type,tys list] => tys"
"tysl2tys X ts ==
case X of
I_ => PTS Integer
| A_ => RTS (concat (@rs. ts=map RTS rs))"
consts
wt_MA :: "[manipulate_array,bytecode,method_type,p_count,p_count] => bool"
primrec
"wt_MA (X aload) CFS phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
(? ts ST'. ST = (PTS Integer) # (RTS (map AT ts)) # ST' & ins_type_tysl_ok X ts &
phi ! (pc+1) >>>= (tysl2tys X ts # ST' , LT)))"
"wt_MA (X astore) CFS phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
(? ts' ts ST'. ST = ts' # (PTS Integer) # (RTS (map AT ts)) # ST' &
ins_type_tys_ok X ts' & ins_type_tysl_ok X ts &
phi ! (pc+1) >>>= (ST' , LT)))"
consts
wt_CO :: "[create_object,bytecode,cpool,method_type,p_count,p_count] => bool"
primrec
"wt_CO (New idx) CFS cp phi max_pc pc =
(let (ST,LT) = phi ! pc;
oc = get_Id (extract_Class cp idx)
in
pc+1 < max_pc &
is_class CFS oc &
phi ! (pc+1) >>>= ((RTS [CT oc]) # ST , LT))"
"wt_CO (IAnewarray atd) CFS cp phi max_pc pc =
(let (ST,LT) = phi ! pc;
tys = fd2tys CFS (type_of_arr_type cp atd)
in
pc+1 < max_pc &
(? ST'. ST = (PTS Integer) # ST' &
phi ! (pc+1) >>>= (RTS [AT tys] # ST' , LT)))"
consts
wt_CH :: "[check_object,bytecode,cpool,method_type,p_count,p_count] => bool"
primrec
"wt_CH (Checkcast idx) CFS cp phi max_pc pc =
(let (ST,LT) = phi ! pc;
tys = fd2tys CFS (type_of_str (extract_Class cp idx))
in
pc+1 < max_pc &
(? rs rs' ST'. ST = RTS rs # ST' & tys=RTS rs' &
phi ! (pc+1) >>>= (RTS rs' # ST' , LT)))"
consts
wt_OS :: "[op_stack,method_type,p_count,p_count] => bool"
primrec
"wt_OS Pop phi max_pc pc =
(let (ST,LT) = phi ! pc
in
? ts ST'. pc+1 < max_pc &
ST = ts # ST' &
phi ! (pc+1) >>>= (ST' , LT))"
"wt_OS Dup phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
(? ts ST'. ST = ts # ST' &
phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
"wt_OS Swap phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc &
(? ts ts' ST'. ST = ts' # ts # ST' &
phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
consts
wt_CB :: "[cond_branch,method_type,p_count,p_count] => bool"
primrec
"wt_CB (If_ bop branch) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc & (nat(int pc+branch)) < max_pc &
(? ST'. ST = PTS Integer # ST' &
phi ! (pc+1) >>>= (ST' , LT) &
phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
"wt_CB (Ifnull branch) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc & (nat(int pc+branch)) < max_pc &
(? rs ST'. ST = RTS rs # ST' &
phi ! (pc+1) >>>= (ST' , LT) &
phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
"wt_CB (X Ifiacmpeq branch) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc & (nat(int pc+branch)) < max_pc &
(? ts ts' ST'. ST = ts # ts' # ST' & ins_type_tys_ok X ts & ins_type_tys_ok X ts' &
phi ! (pc+1) >>>= (ST' , LT) &
phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
consts
wt_UB :: "[uncond_branch,method_type,p_count,p_count] => bool"
primrec
Goto
"wt_UB (Goto branch) phi max_pc pc =
(let (ST,LT) = phi ! pc
in
(nat(int pc+branch)) < max_pc &
phi ! (nat(int pc+branch)) >>>= (ST , LT))"
consts
inv_methref_ok :: "[bytecode,cname,refs,meth_inv] => bool"
primrec
"inv_methref_ok CFS cn rs (Invokevirtual idx) =
(is_class CFS cn & wideRefsConvertible CFS rs [CT cn])"
"inv_methref_ok CFS cn rs (Invokeinterface idx n) =
(is_inter CFS cn & wideRefsConvertible CFS rs [IT cn])"
constdefs
push_rd :: "[bytecode,return_desc,opstack_type] => opstack_type"
"push_rd CFS rd ST == case rd of
V => ST
| FT fd => fd2tys CFS fd # ST"
constdefs
wt_MI :: "[meth_inv,bytecode,cpool,method_type,p_count,p_count] => bool"
"wt_MI inv_com CFS cp phi max_pc pc ==
(let (ST,LT) = phi ! pc;
(sc,(mn,pd),rd,n) = extract_inv_methref cp inv_com
in
pc+1 < max_pc &
n=length pd+1 &
(? ins. get_methods (CFS !! sc) (mn,pd) = Some (rd,ins)) &
(? tys_n cns ST'. ST = (rev tys_n) @ [RTS cns] @ ST' & length tys_n = length pd &
(!(t,t'):set (zip tys_n (map (fd2tys CFS) pd)). invoConvertible CFS t t') &
inv_methref_ok CFS sc cns inv_com &
phi ! (pc+1) >>>= (push_rd CFS rd ST' , LT)))"
consts
wt_MR :: "[meth_ret,bytecode,return_desc,method_type,p_count] => bool"
primrec
"wt_MR (X return) CFS rd phi pc =
(let (ST,LT) = phi ! pc
in
(? ts tys ST'. ST = ts # ST' & ins_type_tys_ok X ts &
rd2tyOrVoid CFS rd = TY tys & ins_type_tys_ok X tys &
invoConvertible CFS ts tys))"
"wt_MR Return CFS rd phi pc = (rd2tyOrVoid CFS rd = Void)"
constdefs
wt_instr :: "[instr,bytecode,return_desc,cpool,method_type,nat,p_count] => bool"
"wt_instr instr CFS rd cp phi max_pc pc ==
case instr of
LAS ins => wt_LAS ins phi max_pc pc
| CO ins => wt_CO ins CFS cp phi max_pc pc
| MO ins => wt_MO ins CFS cp phi max_pc pc
| MA ins => wt_MA ins CFS phi max_pc pc
| CH ins => wt_CH ins CFS cp phi max_pc pc
| MI ins => wt_MI ins CFS cp phi max_pc pc
| MR ins => wt_MR ins CFS rd phi pc
| OS ins => wt_OS ins phi max_pc pc
| CB ins => wt_CB ins phi max_pc pc
| UB ins => wt_UB ins phi max_pc pc"
constdefs
wt_start :: "[bytecode,cname,param_desc,method_type] => bool"
"wt_start CFS cn pd phi ==
phi ! 0 >>>= ([],(Refs [CT cn])#(map (fd2any CFS) pd))"
wt_method :: "[bytecode,cname,param_desc,return_desc,instr list,method_type] => bool"
"wt_method CFS cn pd rd ins phi ==
let cp = get_cpool (CFS !! cn);
max_pc = length ins
in
0 < max_pc & wt_start CFS cn pd phi &
(! pc. pc<max_pc --> wt_instr (ins ! pc) CFS rd cp phi max_pc pc)"
wt_class :: "[bytecode,cname,class_type] => bool"
"wt_class CFS cn phi ==
!ml rd ins. get_methods (CFS !! cn) ml = Some (rd,ins)
--> wt_method CFS cn (snd ml) rd ins (phi ml)"
wt_classfiles :: "[bytecode,prog_type] => bool"
"wt_classfiles CFS phi == (!cn. is_class CFS cn --> wt_class CFS cn (phi cn))"
end
Theorems proved in WT.ML:
sup_loc_Nil
XT >>= [] = (XT = [])
sup_loc_Cons
XT >>= (Y # YT) = (? X XT'. XT = X # XT' & X >= Y & XT' >>= YT)
map_inject
[| map f xs = map f ys; ! x y. (f x = f y) = (x = y) |] ==> xs = ys
tysl2tys_I
tysl2tys I_ [PTS Integer] = PTS Integer
tysl2tys_A
tysl2tys A_ (map RTS rs) = RTS (concat rs)
ins_type_tylist_ok_lemma
[| ins_type_tysl_ok X ts; Xa >= US (tysl2tys X ts); t : set ts |] ==> Xa >= US t
wf_cs7
[| wf_classfiles CFS; d_implements CFS cn si |] ==> method_impl_ok CFS cn si
wf_cs8
[| wf_classfiles CFS; d_implements CFS cn si'; (si, si') : (d_superinterface_rel CFS)^+ |]
==> method_impl_ok CFS cn si
method_impl_ok_method_over_ok_trans
[| wf_classfiles CFS; method_impl_ok CFS cn si; (cn, cna) : (d_superclass_rel CFS)^* |]
==> method_over_ok CFS cna si
wf_cs10
[| wf_classfiles CFS; implements (CFS, sc, si); (sc, cn) : (d_superclass_rel CFS)^* |]
==> method_over_ok CFS cn si
get_methods_super_impl_get_methods_obj
[| wf_classfiles CFS; (cn', cn) : (d_superclass_rel CFS)^*; is_class CFS cn;
get_methods CFS !! cn' (mn, pd) = Some (rd, ins') |]
==> is_class CFS (dyn_class (CFS, (mn, pd), cn)) &
(dyn_class (CFS, (mn, pd), cn), cn) : (d_superclass_rel CFS)^* &
(? ins'. get_methods CFS !! dyn_class (CFS, (mn, pd), cn) (mn, pd) = Some (rd, ins'))
method_impl_ok_imp_dyn_class_lemma
[| wf_classfiles CFS; is_class CFS cn; method_impl_ok CFS cn mi;
get_methods CFS !! mi (mn, pd) = Some (rd, ins) |]
==> is_class CFS (dyn_class (CFS, (mn, pd), cn)) &
(dyn_class (CFS, (mn, pd), cn), cn) : (d_superclass_rel CFS)^* &
(? ins'. get_methods CFS !! dyn_class (CFS, (mn, pd), cn) (mn, pd) = Some (rd, ins'))
get_methods_inter_impl_get_methods_obj
[| wf_classfiles CFS; implements (CFS, oc, mi); get_methods CFS !! mi (mn, pd) = Some (rd, ins);
dc = dyn_class (CFS, (mn, pd), oc) |]
==> is_class CFS dc &
(dc, oc) : (d_superclass_rel CFS)^* & (? ins'. get_methods CFS !! dc (mn, pd) = Some (rd, ins'))
inv_methref_ok_impl_get_methods_CT
[| wf_classfiles CFS; r : set rs; wideRefConvertible CFS (CT oc) r; inv_methref_ok CFS mci rs inv_com;
is_class CFS oc; get_methods CFS !! mci ml = Some (rd, ins); dc = dyn_class (CFS, ml, oc) |]
==> is_class CFS dc &
(dc, oc) : (d_superclass_rel CFS)^* & (? ins'. get_methods CFS !! dc ml = Some (rd, ins'))
inv_methref_ok_impl_get_methods_AT
[| wf_classfiles CFS; r : set rs; wideRefConvertible CFS (AT (fd2tys CFS fd)) r;
inv_methref_ok CFS mci rs inv_com; get_methods CFS !! mci ml = Some (rd, ins);
dc = dyn_class (CFS, ml, Object) |]
==> dc = Object & (? ins'. get_methods CFS !! dc ml = Some (rd, ins'))
inv_methref_ok_impl_get_methods_AT
[| wf_classfiles CFS; r : set rs; wideRefConvertible CFS (AT (fd2tys CFS fd)) r;
inv_methref_ok CFS mci rs inv_com; get_methods CFS !! mci ml = Some (rd, ins);
dc = dyn_class (CFS, ml, Object) |]
==> is_class CFS dc &
wideRefConvertible CFS (AT (fd2tys CFS fd)) (CT dc) &
(? ins'. get_methods CFS !! dc ml = Some (rd, ins'))