Runtime.thy

Runtime = Classfile + 

(** locations **)

types
 loc	
arities
 loc :: term

(** values **)

datatype
 val_	= Intg int
	| Addr loc
	| Null
types	val = val_

constdefs
 get_Intg :: "val => int" 
 "get_Intg x == (@i. x =  Intg i)"

 get_Nat :: "val => nat" 
 "get_Nat == nat  o  get_Intg"

 get_Addr :: "val => loc" 
 "get_Addr x == (@a. x =  Addr a)"


(** heap **)

types	
 odata = "field_loc ~=> val"		(* defining class+field name, and value *)
 adata = "val list"			(* array elements *)


datatype 
 obj	= Obj cname odata		(* class instance with class name and fields	*)
	| Arr field_desc adata		(* array with component type and components	*)

constdefs
 get_Obj :: "obj => (cname * odata)"
 "get_Obj ob == @ (cn,od). ob = Obj cn od" 

 get_Arr :: "obj => (field_desc * adata)"
 "get_Arr ob == @ (fd,ad). ob = Arr fd ad" 

types
 heap	= "loc ~=> obj"

consts
 get_obj_type :: "obj => field_desc"
primrec
 "get_obj_type (Obj cn od) = L cn"
 "get_obj_type (Arr fd ad) = A fd"

consts
 get_obj_class :: "obj => cname"
primrec
 "get_obj_class (Obj cn od) = cn" 
 "get_obj_class (Arr fd ad) = Object"


(** object initialization **)

constdefs
 get_all_fields_term_rel :: "(('code classfiles * cname) * ('code classfiles * cname)) set" 
 "get_all_fields_term_rel == {((CFS,sc),(CFS',cn)). 
				CFS=CFS' &  wf (d_superclass_rel CFS) &  
				(sc,cn) : d_superclass_rel CFS}"
consts
 get_all_fields :: "'code classfiles * cname => field_loc ~=> field_desc"
recdef get_all_fields "get_all_fields_term_rel" 
 "get_all_fields (CFS, cn) =
     (if wf (d_superclass_rel CFS) &  is_class CFS cn  
	 then (let fs = get_fields (CFS !! cn)
	       in
	       if cn=Object then fs
		  else (let sc = get_superclass (CFS !! cn)
		        in
		        if is_class CFS sc 
			then (get_all_fields (CFS, sc)) ++ fs 
			else arbitrary))
	 else arbitrary)"
	

consts
 default_val    :: "field_desc => val"
primrec
 "default_val     I = Intg #0"
 "default_val (L i) = Null"
 "default_val (A f) = Null"


constdefs
 init_obj :: "['code classfiles,cname] => odata" 
 "init_obj CFS cn == (let fs = get_all_fields (CFS, cn)
		     in
		     map_compose default_val fs)"

 init_arr :: "[val,int] => adata"
 "init_arr val n == replicate (nat n) val"


(** frame stack **)

types
 opstack 	 = "val list"
 locvars 	 = "val list" 
 p_count 	 = nat

 frame = "opstack *			
	  locvars *		
	  cname *			
	  method_loc *			
	  p_count"

	(* operand stack *)
	(* local variables *)
	(* name of def. class defined *)
	(* meth name+param_desc *)
	(* program counter within frame *)


(** exceptions **)

datatype 
 xcpt	= NullPointer
	| NegArrSize
	| IndOutBound
	| ArrStore
	| ClassCast
	| InstantiationError
	| OutOfMemory


(** runtime state **)

types
 jvm_state = "xcpt option *		
	      heap *				
	      frame list"	


(** type compatibility **)

consts
 compatible :: "['code classfiles,field_desc,field_desc] => bool"

primrec
 "compatible CFS I t = (t=I)"

 "compatible CFS (L cn) t =
	(case t of I       => False
	 | (L cn') => if is_interface (CFS !! cn')
			 then implements (CFS, cn, cn') 
			 else (cn',cn) : (d_superclass_rel CFS)^*
	 | (A fd)  => False)"

 "compatible CFS (A fd) t =
	(case t of I       => False
	 | (L cn)  => cn=Object
	 | (A fd') => compatible CFS fd fd')"


constdefs
 fd_compatible :: "['code classfiles,heap,ins_type,val,field_desc] => bool"
 "fd_compatible CFS hp X val fd ==
	case X of
	  I_ => True
	| A_ => if val=Null then fd~=I 
		  else let fd' = get_obj_type (hp !! (get_Addr val)) 
		       in 
		       compatible CFS fd' fd"


(** dynamic method lookup **)

constdefs
 dyn_class_term_rel :: "(('code classfiles * method_loc * cname) * 
                           ('code classfiles * method_loc * cname)) set" 
 "dyn_class_term_rel == {((CFS,ml,cn),(CFS',ml',cn')). 
				CFS=CFS' &  ml=ml' &  wf (d_superclass_rel CFS) &  
				(cn,cn') : d_superclass_rel CFS}"


consts
 dyn_class	:: "'code classfiles * method_loc * cname => cname"
recdef dyn_class "dyn_class_term_rel"
 "dyn_class (CFS, ml, cn) =
   (if wf (d_superclass_rel CFS) &  is_class CFS cn
       then (let ms = get_methods (CFS !! cn)
	     in
	     if ms ml ~= None then cn
	     else if cn=Object then arbitrary
	     else (let sc = get_superclass (CFS !! cn)
	           in
	           if is_class CFS sc 
		      then dyn_class (CFS, ml, sc)
		      else arbitrary))
       else arbitrary)"

end

Theorems proved in Runtime.ML:

get_Addr (Addr a) = a

get_Intg (Intg a) = a

get_Obj (Obj cn od) = (cn, od)

get_Arr (Arr fd ad) = (fd, ad)

default_val fd = Intg i ==> fd = I

default_val fd = Addr a ==> False

default_val fd = Null ==> (? cn. fd = L cn) | (? fd'. fd = A fd')

compatible CFS fd I ==> fd = I