author | nipkow |
Mon, 06 Dec 1999 14:23:45 +0100 | |
changeset 8048 | b7f7e18eb584 |
parent 8045 | 816f566c414f |
permissions | -rw-r--r-- |
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 = |
|
8032 | 15 |
Invoke mname (ty list) (** inv. instance meth of an object **) |
8011 | 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 |
|
8032 | 21 |
"exec_mi (Invoke mn ps) G hp stk pc = |
8011 | 22 |
(let n = length ps; |
23 |
argsoref = take (n+1) stk; |
|
24 |
oref = last argsoref; |
|
25 |
xp' = raise_xcpt (oref=Null) NullPointer; |
|
8038 | 26 |
dynT = fst(the(hp(the_Addr oref))); |
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
27 |
(dc,mh,mxl,c)= the (method (G,dynT) (mn,ps)); |
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
28 |
frs' = if xp'=None |
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
29 |
then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] |
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
30 |
else [] |
8011 | 31 |
in |
32 |
(xp' , frs' , drop (n+1) stk , pc+1))" |
|
33 |
||
34 |
||
8032 | 35 |
datatype |
36 |
meth_ret = Return |
|
37 |
||
38 |
consts |
|
39 |
exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list" |
|
40 |
primrec |
|
41 |
"exec_mr Return stk0 frs = |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8038
diff
changeset
|
42 |
(if frs=[] then [] |
8048 | 43 |
else let val = hd stk0; (stk,loc,C,sig,pc) = hd frs |
44 |
in (val#stk,loc,C,sig,pc)#tl frs)" |
|
8011 | 45 |
|
46 |
end |