Method.thy

Method = Runtime +

(** method invocation and return instructions **)

datatype 
 meth_inv = 
   Invokevirtual   mr_idx        (** inv. instance meth of an object **)
 | Invokeinterface im_idx nat    (** inv. interface method **)
 

consts
extract_inv_methref :: "[cpool,meth_inv] => (cname * method_loc * return_desc * nat)"
primrec
  "extract_inv_methref cp (Invokevirtual idx) = 
	(let (cn,mn,(pd,rd)) = extract_Methodref cp idx
	 in
	 (cn,(mn,pd),rd,length pd+1))"

"extract_inv_methref cp (Invokeinterface idx n) = 
	(let (cn,mn,(pd,rd)) = extract_InterMethref cp idx
	 in
	 (cn,(mn,pd),rd,n))"


constdefs
 exec_mi :: "[meth_inv,'code classfiles,cpool,heap,opstack,p_count] 
		=> (xcpt option * frame * opstack * p_count)" 
 "exec_mi inv_com CFS cp hp stk pc ==
	(let (sc,ml,rd,n)	= extract_inv_methref cp inv_com;
	     argsoref	= take n stk;
	     oref	= last argsoref;
	     dc		= dyn_class (CFS, ml, get_obj_class (hp !! get_Addr oref));

	     xp'	= if oref=Null
			     then Some  NullPointer
			     else None

	 in
	 (xp' , ([],rev argsoref,dc,ml,0) , drop n stk , pc+1))"



 datatype
 meth_ret = 
   IAreturn ins_type  ("_ return" 30)	(** return int/ref value **)
 | Return				(** return void	 **)

consts
 exec_mr :: "[meth_ret,opstack,frame list] => frame list" 

primrec
  "exec_mr (X return) stk0 frs =
	 (let val			= hd stk0;
	      (stk,loc,cn,met,pc) = hd frs
	  in
	  (val#stk,loc,cn,met,pc)#tl frs)"


  "exec_mr Return stk0 frs = frs"

end