|
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 |