|
8011
|
1 |
(* Title: HOL/MicroJava/JVM/Method.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Cornelia Pusch
|
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
Method invocation
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Method = JVMState +
|
|
|
10 |
|
|
|
11 |
(** method invocation and return instructions **)
|
|
|
12 |
|
|
|
13 |
datatype
|
|
|
14 |
meth_inv =
|
|
|
15 |
Invokevirtual mname (ty list) (** inv. instance meth of an object **)
|
|
|
16 |
|
|
|
17 |
consts
|
|
|
18 |
exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count]
|
|
|
19 |
\\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)"
|
|
|
20 |
primrec
|
|
|
21 |
"exec_mi (Invokevirtual mn ps) G hp stk pc =
|
|
|
22 |
(let n = length ps;
|
|
|
23 |
argsoref = take (n+1) stk;
|
|
|
24 |
oref = last argsoref;
|
|
|
25 |
xp' = raise_xcpt (oref=Null) NullPointer;
|
|
|
26 |
dynT = fst(hp \\<And> (the_Addr oref));
|
|
|
27 |
(dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
|
|
|
28 |
frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
|
|
|
29 |
in
|
|
|
30 |
(xp' , frs' , drop (n+1) stk , pc+1))"
|
|
|
31 |
|
|
|
32 |
|
|
|
33 |
constdefs
|
|
|
34 |
exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
|
|
|
35 |
"exec_mr stk0 frs \\<equiv>
|
|
|
36 |
(let val = hd stk0;
|
|
|
37 |
(stk,loc,cn,met,pc) = hd frs
|
|
|
38 |
in
|
|
|
39 |
(val#stk,loc,cn,met,pc)#tl frs)"
|
|
|
40 |
|
|
|
41 |
end
|