Correct.thy

Back to the index of BV_ASCII

Correct = WT +

constdefs
 approx_val :: "[bytecode,heap,val,any] => bool"
"approx_val CFS hp val any == 
 case any of 
   Unusable => True
 | US tys => 
  (case val of
     Intg i => tys = PTS Integer
   | Addr a => ?  obj rt rs. tys = RTS rs & 
			hp a = Some obj &  
		        fd2tys CFS (get_obj_type obj) = RTS [rt] &  
		        wideRefsConvertible CFS [rt] rs
   | Null   => ? rs. tys = RTS rs)"


 approx_loc :: "[bytecode,heap,val list,locvars_type] => bool"
"approx_loc CFS hp loc LT == 
   length loc=length LT &  (!(val,any):set (zip loc LT). approx_val CFS hp val any)" 

 approx_stk :: "[bytecode,heap,opstack,opstack_type] => bool"
"approx_stk CFS hp stk ST == approx_loc CFS hp stk (map US ST)"


 correct_obj :: "[bytecode,heap,obj] => bool"
"correct_obj CFS hp obj ==
    case obj of
      Obj cn od => (is_class CFS cn) & 
	  (!fl fd. (get_all_fields (CFS,cn)) fl = Some fd
			--> (? val. od fl = Some val &  
				  approx_val CFS hp val (fd2any CFS fd)))
    | Arr fd ad =>  !val:set ad. approx_val CFS hp val (fd2any CFS fd)"

 correct_heap :: "[bytecode,heap] => bool"
"correct_heap CFS hp ==
   !a obj. hp a = Some obj --> correct_obj CFS hp obj"


 correct_frame  :: "[bytecode,heap,state_type] => frame => bool"
"correct_frame CFS hp == (%(ST,LT) (stk,loc,cn,ml,pc).
   approx_stk CFS hp stk ST  &  approx_loc CFS hp loc LT &  correct_heap CFS hp &  is_class CFS cn &  
   (? rd ins. get_methods (CFS !! cn) ml = Some (rd,ins) &  pc < length ins))"


constdefs
pop_rd :: "[bytecode,return_desc,opstack_type] => opstack_type"
"pop_rd CFS rd ST == case rd of
		    V    => ST
		 | FT fd => tl ST"
consts
correct_frames  :: "[bytecode,heap,prog_type,return_desc,method_loc,frame list] => bool"
primrec
"correct_frames CFS hp phi rd0 ml0 [] = (rd0=V)"

"correct_frames CFS hp phi rd0 ml0 (f#frs) = 
	(let (stk,loc,cn,ml,pc) = f;
	     (rd,ins) = get_methods (CFS !! cn) !! ml;
	     cp	= get_cpool (CFS !! cn);
	     (ST,LT) = (phi cn ml) ! pc
	 in
	 (? ic c k l. pc = k+1 &  
                     ins ! k = MI ic & 
		     extract_inv_methref cp ic = (c,ml0,rd0,l))  &  
	 correct_frame CFS hp (pop_rd CFS rd0 ST, LT) f &  
	 correct_frames CFS hp phi rd ml frs)"

constdefs
correct_state :: "[bytecode,prog_type,jvm_state] => bool"
"correct_state CFS phi == %(xp,hp,frs). 
   case xp of
     None => (case frs of 
	           [] => True
             | (f#fs) => (let (stk,loc,cn,ml,pc) = f;
			     (rd,ins) = get_methods (CFS !! cn) !! ml
		         in
		         correct_frame CFS hp ((phi cn ml) ! pc) f &  
		         correct_frames CFS hp phi rd ml fs))
   | Some x => True" 


 sup_heap :: "[heap,heap] => bool"
 "sup_heap hp hp' ==
   (!a obj. hp a = Some obj
	--> (case obj of
	      Obj cn od => (? od'. hp' a = Some (Obj cn od'))
	    | Arr fd ad => (? ad'. hp' a = Some (Arr fd ad'))))"	


end

Theorems proved in Correct.ML:

correct_heap_imp_is_class

[| correct_heap CFS hp; hp a = Some (Obj cn od) |] ==> is_class CFS cn

sup_heap_newref

hp x = None ==> sup_heap hp (hp(newref hp|->obj))

sup_heap_update_value

hp a = Some (Obj cn od') ==> sup_heap hp (hp(a|->Obj cn od))

sup_heap_update_array

hp a = Some (Arr fd ad') ==> sup_heap hp (hp(a|->Arr fd ad))

approx_val_imp_approx_val_wideRefConvertible

[| wf_classfiles CFS; approx_val CFS hp v (Refs rs); wideRefsConvertible CFS rs rs' |]
==> approx_val CFS hp v (Refs rs')

approx_val_imp_approx_val_invoConvertible

[| wf_classfiles CFS; approx_val CFS hp v (US ts); invoConvertible CFS ts ts' |]
==> approx_val CFS hp v (US ts')

approx_val_imp_approx_val_assConvertible

[| wf_classfiles CFS; assConvertible CFS tys at; approx_val CFS hp s (US tys) |]
==> approx_val CFS hp s (US at)

approx_val_imp_approx_val_sup_heap

[| approx_val CFS hp val at; sup_heap hp hp' |] ==> approx_val CFS hp' val at

approx_val_imp_approx_val_heap_update

hp a = Some obj' & approx_val CFS hp val at & get_obj_type obj = get_obj_type obj'
==> approx_val CFS (hp(a|->obj)) val at

approx_val_imp_approx_val_sup

[| approx_val CFS hp val us; us' >= us |] ==> approx_val CFS hp val us'

approx_val_RTS

approx_val CFS hp val (Refs rs) =
((? a obj rt.
     val = Addr a &
     hp a = Some obj & fd2tys CFS (get_obj_type obj) = RTS [rt] & wideRefsConvertible CFS [rt] rs) |
 val = Null)

approx_val_RTS_AT

approx_val CFS hp val (Refs (map AT ts)) =
((? a fd ad.
     val = Addr a & hp a = Some (Arr fd ad) & Bex (set ts) (invoConvertible CFS (fd2tys CFS fd))) |
 val = Null)

approx_loc_imp_approx_val_sup

[| approx_loc CFS hp loc LT; idx < length LT; val = loc ! idx; at >= LT ! idx |]
==> approx_val CFS hp val at

approx_loc_Cons

approx_loc CFS hp (s # xs) (l # ls) =
(length xs = length ls & approx_val CFS hp s l & approx_loc CFS hp xs ls)

invoConv_approx_stk_imp_approx_loc

[| wf_classfiles CFS; Ball (set (zip tys_n ts)) (split (invoConvertible CFS)); length tys_n = length ts;
   approx_stk CFS hp s tys_n |]
==> approx_loc CFS hp s (map US ts)

approx_loc_imp_approx_loc_sup_heap

[| approx_loc CFS hp lvars lt; sup_heap hp hp' |] ==> approx_loc CFS hp' lvars lt  [term]

approx_loc_imp_approx_loc_sup

[| approx_loc CFS hp lvars lt; lt' >>= lt |] ==> approx_loc CFS hp lvars lt'

approx_loc_imp_approx_loc_subst

[| approx_loc CFS hp loc LT; approx_val CFS hp x X |]
==> approx_loc CFS hp (loc[idx := x]) (LT[idx := X])
  [term]

approx_stk_rev_lem

approx_stk CFS hp (rev s) (rev t) = approx_stk CFS hp s t

approx_stk_rev

approx_stk CFS hp (rev s) t = approx_stk CFS hp s (rev t)

approx_stk_imp_approx_stk_sup_heap

[| approx_stk CFS hp lvars lt; sup_heap hp hp' |] ==> approx_stk CFS hp' lvars lt  [term]

approx_stk_imp_approx_stk_sup

[| approx_stk CFS hp lvars st; map US st' >>= map US st |] ==> approx_stk CFS hp lvars st'  [term]

approx_stk_Nil

approx_stk CFS hp [] []

approx_stk_Cons

approx_stk CFS hp (x # stk) (S # ST) = (approx_stk CFS hp stk ST & approx_val CFS hp x (US S))

approx_stk_Cons_lemma

approx_stk CFS hp stk (S # ST')
==> ? s stk'. stk = s # stk' & approx_stk CFS hp stk' ST' & approx_val CFS hp s (US S)

approx_stk_append_lemma

approx_stk CFS hp stk (S @ ST')
==> ? s stk'.
       stk = s @ stk' &
       length s = length S &
       length stk' = length ST' & approx_stk CFS hp s S & approx_stk CFS hp stk' ST'
  [term]

approx_stk_imp_approx_stk_pop_sup_push

[| approx_stk CFS hp stk ST'; map US ST >>= map US (push_rd CFS rd ST') |]
==> approx_stk CFS hp stk (pop_rd CFS rd ST)

correct_init_obj

is_class CFS cn ==> correct_obj CFS hp (Obj cn (init_obj CFS cn))

correct_init_arr

correct_obj CFS hp (Arr fd (init_arr (default_val fd) n))

correct_obj_imp_correct_obj_field_update

[| get_all_fields (CFS, cn) fl = Some fd; approx_val CFS hp val (fd2any CFS fd);
   correct_obj CFS hp (Obj cn od) |]
==> correct_obj CFS hp (Obj cn (od(fl|->val)))

correct_obj_imp_correct_obj_array_update

[| i < length ad; approx_val CFS hp val (fd2any CFS fd); correct_obj CFS hp (Arr fd ad) |]
==> correct_obj CFS hp (Arr fd (ad[i := val]))

correct_obj_imp_correct_obj_heap_newref

[| hp x = None; correct_obj CFS hp obj; correct_obj CFS hp obj' |]
==> correct_obj CFS (hp(newref hp|->obj')) obj

correct_obj_imp_correct_obj_heap_update

[| hp a = Some obj'; get_obj_type obj' = get_obj_type obj''; correct_obj CFS hp obj |]
==> correct_obj CFS (hp(a|->obj'')) obj

correct_heap_imp_correct_heap_newref

[| hp x = None; correct_heap CFS hp; correct_obj CFS hp obj |] ==> correct_heap CFS (hp(newref hp|->obj))

correct_heap_imp_correct_heap_field_update

get_all_fields (CFS, cn) fl = Some fd &
hp a = Some (Obj cn od) & approx_val CFS hp val (fd2any CFS fd) & correct_heap CFS hp
==> correct_heap CFS (hp(a|->Obj cn (od(fl|->val))))

correct_heap_imp_correct_heap_array_update

i < length ad & hp a = Some (Arr fd ad) & approx_val CFS hp val (fd2any CFS fd) & correct_heap CFS hp
==> correct_heap CFS (hp(a|->Arr fd (ad[i := val])))

correct_frames_imp_correct_frames_field_update

correct_frames CFS hp phi cl ml frs &
hp a = Some (Obj cn od) & get_all_fields (CFS, cn) fl = Some fd & approx_val CFS hp val (fd2any CFS fd)
==> correct_frames CFS (hp(a|->Obj cn (od(fl|->val)))) phi cl ml frs
  [term]

correct_frames_imp_correct_frames_array_update

correct_frames CFS hp phi cl ml frs &
hp a = Some (Arr fd ad) & i < length ad & approx_val CFS hp val (fd2any CFS fd)
==> correct_frames CFS (hp(a|->Arr fd (ad[i := val]))) phi cl ml frs
  [term]

correct_frames_imp_correct_frames_newref

[| hp x = None; correct_frames CFS hp phi cl ml frs & correct_obj CFS hp obj |]
==> correct_frames CFS (hp(newref hp|->obj)) phi cl ml frs
  [term]

wRC_lemma0

[| correct_heap CFS hp; hp a = Some obj; fd2tys CFS (get_obj_type obj) = RTS [rt];
   wideRefConvertible CFS rt (CT cn) |]
==> (? od cn'. obj = Obj cn' od & is_class CFS cn' & wideRefConvertible CFS (CT cn') (CT cn)) |
    (? ad fd. obj = Arr fd ad & cn = Object)

wRC_lemma1

[| wf_classfiles CFS; correct_heap CFS hp; hp a = Some obj; fd2tys CFS (get_obj_type obj) = RTS [rt];
   get_fields CFS !! cn (cn, fn) = Some fd; wideRefConvertible CFS rt (CT cn) |]
==> ? od cn'. obj = Obj cn' od & is_class CFS cn' & wideRefConvertible CFS (CT cn') (CT cn)

is_class_get_obj_class

[| wf_classfiles CFS; hp a = Some obj; correct_heap CFS hp |] ==> is_class CFS (get_obj_class obj)

fd_compatible_imp_approx_val

[| wf_classfiles CFS; t : set ts; invoConvertible CFS (fd2tys CFS fd) t; ins_type_tysl_ok X ts;
   ins_type_tys_ok X ts'; approx_val CFS hp s (US ts'); fd_compatible CFS hp X s fd |]
==> approx_val CFS hp s (fd2any CFS fd)

get_fields_imp_approx_val

[| wf_classfiles CFS; hp a = Some (Obj cn od); correct_heap CFS hp;
   wideRefConvertible CFS (CT cn) (CT fc); get_fields CFS !! fc (fc, fn) = Some fd |]
==> approx_val CFS hp od !! (fc, fn) (fd2any CFS fd)

inv_methref_ok_impl_get_methods

[| wf_classfiles CFS; correct_obj CFS hp obj; r : set rs; oc = get_obj_class obj;
   fd2tys CFS (get_obj_type obj) = RTS [rt]; wideRefConvertible CFS rt 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 &
    wideRefConvertible CFS rt (CT dc) & (? ins'. get_methods CFS !! dc ml = Some (rd, ins'))