|
8011
|
1 |
(* Title: HOL/MicroJava/JVM/Object.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Cornelia Pusch
|
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
Get and putfield instructions
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Object = JVMState +
|
|
|
10 |
|
|
|
11 |
datatype
|
|
|
12 |
create_object = New cname
|
|
|
13 |
|
|
|
14 |
consts
|
|
|
15 |
exec_co :: "[create_object,'code prog,aheap,opstack,p_count] \\<Rightarrow>
|
|
|
16 |
(xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
|
|
|
17 |
|
|
|
18 |
|
|
|
19 |
primrec
|
|
|
20 |
"exec_co (New C) G hp stk pc =
|
|
|
21 |
(let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
|
|
|
22 |
oref = newref hp;
|
|
|
23 |
fs = init_vars (fields(G,C));
|
|
|
24 |
hp' = xcpt_update xp' (hp(oref \\<mapsto> (C,fs))) hp;
|
|
|
25 |
stk' = xcpt_update xp' ((Addr oref)#stk) stk
|
|
|
26 |
in (xp' , hp' , stk' , pc+1))"
|
|
|
27 |
|
|
|
28 |
|
|
|
29 |
datatype
|
|
|
30 |
manipulate_object =
|
|
|
31 |
Getfield vname cname (* Fetch field from object *)
|
|
|
32 |
| Putfield vname cname (* Set field in object *)
|
|
|
33 |
|
|
|
34 |
consts
|
|
|
35 |
exec_mo :: "[manipulate_object,aheap,opstack,p_count] \\<Rightarrow>
|
|
|
36 |
(xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
|
|
|
37 |
|
|
|
38 |
primrec
|
|
|
39 |
"exec_mo (Getfield F C) hp stk pc =
|
|
|
40 |
(let oref = hd stk;
|
|
|
41 |
xp' = raise_xcpt (oref=Null) NullPointer;
|
|
|
42 |
(oc,fs) = hp \\<And> (the_Addr oref);
|
|
|
43 |
stk' = xcpt_update xp' ((fs\\<And>(F,C))#(tl stk)) (tl stk)
|
|
|
44 |
in
|
|
|
45 |
(xp' , hp , stk' , pc+1))"
|
|
|
46 |
|
|
|
47 |
"exec_mo (Putfield F C) hp stk pc =
|
|
|
48 |
(let (fval,oref)= (hd stk, hd(tl stk));
|
|
|
49 |
xp' = raise_xcpt (oref=Null) NullPointer;
|
|
|
50 |
a = the_Addr oref;
|
|
|
51 |
(oc,fs) = hp \\<And> a;
|
|
|
52 |
hp' = xcpt_update xp' (hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval)))) hp
|
|
|
53 |
in
|
|
|
54 |
(xp' , hp' , tl (tl stk), pc+1))"
|
|
|
55 |
|
|
|
56 |
|
|
|
57 |
datatype
|
|
|
58 |
check_object =
|
|
|
59 |
Checkcast cname (* Check whether object is of given type *)
|
|
|
60 |
|
|
|
61 |
consts
|
|
|
62 |
exec_ch :: "[check_object,'code prog,aheap,opstack,p_count]
|
|
|
63 |
\\<Rightarrow> (xcpt option \\<times> opstack \\<times> p_count)"
|
|
|
64 |
|
|
|
65 |
primrec
|
|
|
66 |
"exec_ch (Checkcast C) G hp stk pc =
|
|
|
67 |
(let oref = hd stk;
|
|
|
68 |
xp' = raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
|
|
|
69 |
stk' = xcpt_update xp' stk (tl stk)
|
|
|
70 |
in
|
|
|
71 |
(xp' , stk' , pc+1))"
|
|
|
72 |
|
|
|
73 |
end
|