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