Object.thy

Object = Runtime +

(** array types **)

datatype
 atype	= T_INT

constdefs

 type_of_atype :: "atype => field_desc"
 "type_of_atype at == I"


datatype
 arr_type = PA atype | AA cl_idx


constdefs
type_of_arr_type :: "[cpool,arr_type] => field_desc" 
"type_of_arr_type cpool aty ==
	case aty of
	  (PA at)  => type_of_atype at
	| (AA idx) => type_of_str (extract_Class cpool idx)"


(** Although both class instances and arrays are objects, the JVM creates and
    manipulates class instances and arrays using distinct sets of instructions **)


datatype 
 create_object =	
   New cl_idx			(* Create new object *)
 | IAnewarray arr_type  	(* Create new array of prim/ref type *)


consts
 exec_co :: "[create_object,'code classfiles,cpool,heap,opstack,p_count] => 
		(xcpt option * heap * opstack * p_count)"


primrec
  "exec_co (New idx) CFS cp hp stk pc = 
	(let oc		= get_Id (extract_Class cp idx);
	     oref	= newref hp;
	     hp'	= hp(oref |-> Obj oc (init_obj CFS oc));
	     xp'	= if is_interface (CFS !! oc)
			     then Some InstantiationError
			     else if !x. hp x ~= None
				     then Some OutOfMemory
				     else None
	 in (xp' , hp' , (Addr oref)#stk , pc+1))"	


  "exec_co (IAnewarray X) CFS cp hp stk pc =
	(let fd		= type_of_arr_type cp X;
	     count	= get_Intg (hd stk);
	     xp'	= if count < #0 
			     then Some NegArrSize 
			     else if !x. hp x ~= None
				     then Some OutOfMemory
				     else None;
	     aref	= newref hp;
	     hp'	= hp(aref |-> Arr fd (init_arr (default_val fd) count))
	 in
         (xp' , hp' , (Addr aref)#(tl stk) , pc+1))"	


datatype 
 manipulate_object = 
   Getfield fr_idx		(* Fetch field from object *)
 | Putfield fr_idx		(* Set field in object     *)

consts
 exec_mo :: "[manipulate_object,cpool,heap,opstack,p_count] => 
		(xcpt option * heap * opstack * p_count)"

primrec
 "exec_mo (Getfield idx) cp hp stk pc = 
	(let oref	= hd stk;
	     (oc,fs)	= get_Obj (hp !! (get_Addr oref));
	     (fc,fn,fd)	= extract_Fieldref cp idx;
	     xp'	= if oref=Null
			     then Some NullPointer
			     else None
	 in
         (xp' , hp , (fs !! (fc,fn))#(tl stk) , pc+1))"		

 "exec_mo (Putfield idx) cp hp stk pc = 
	(let (fval,oref)= (hd stk,hd (tl stk));
	     (oc,fs)	= get_Obj (hp !! (get_Addr oref));
	     (fc,fn,fd)	= extract_Fieldref cp idx;
	     hp'	= hp(get_Addr oref |-> Obj oc (fs((fc,fn) |-> fval)));
	     xp'	= if oref=Null
			     then Some  NullPointer
			     else None
	 in
         (xp' , hp' , tl (tl stk), pc+1))"				


datatype
 manipulate_array =
   IAaload  ins_type     	("_ aload" 30)	(* Load int/ref from array *)
 | IAastore ins_type	  	("_ astore" 30)	(* Store into int/ref array *)


consts
 exec_ma :: "[manipulate_array,'code classfiles,heap,opstack,p_count] => 
		(xcpt option * heap * opstack * p_count)"

primrec
 "exec_ma (X aload) CFS hp stk pc = 
	(let (idx,aref)	= (hd stk,hd (tl stk));
	     (fd,ad)	= get_Arr (hp !! (get_Addr aref));
	     xp		= if aref=Null
			     then Some NullPointer
			  else if length ad <= get_Nat idx
			     then Some IndOutBound
			  else None
	 in
         (xp , hp , (ad ! (get_Nat idx)) # (tl (tl stk)) , pc+1))"	


 "exec_ma (X astore) CFS hp stk pc = 
	(let (val,idx,aref)	= (hd stk,hd (tl stk),hd (tl (tl stk)));
	     (fd,ad)		= get_Arr (hp !! (get_Addr aref));
	     hp'	= hp(get_Addr aref |-> (Arr fd (ad[get_Nat idx := val])));
	     xp		= if aref=Null
			     then Some NullPointer
			  else if length ad <= get_Nat idx
			     then Some IndOutBound
			  else if ~ (fd_compatible CFS hp X val fd)
			     then Some ArrStore
			  else None

	 in
         (xp , hp' , tl (tl (tl stk)) , pc+1))"				


datatype
 check_object =
  Checkcast cl_idx      (* Check whether object is of given type *)

consts
 exec_ch :: "[check_object,'code classfiles,cpool,heap,opstack,p_count] 
		=> (xcpt option * p_count)"

primrec
  "exec_ch (Checkcast idx) CFS cp hp stk pc =
	(let oref	= hd stk;
	     ct		= type_of_str (extract_Class cp idx);
	     ot		= get_obj_type (hp !! (get_Addr oref));
	     xp		= if oref=Null 
			     then None
			  else if ~ (compatible CFS ot ct) 
			     then Some ClassCast
			  else None
	 in
	 (xp , pc+1))"

end