19 primrec |
19 primrec |
20 "exec_co (New C) G hp stk pc = |
20 "exec_co (New C) G hp stk pc = |
21 (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory; |
21 (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory; |
22 oref = newref hp; |
22 oref = newref hp; |
23 fs = init_vars (fields(G,C)); |
23 fs = init_vars (fields(G,C)); |
24 hp' = xcpt_update xp' (hp(oref \\<mapsto> (C,fs))) hp; |
24 hp' = if xp'=None then hp(oref \\<mapsto> (C,fs)) else hp; |
25 stk' = xcpt_update xp' ((Addr oref)#stk) stk |
25 stk' = if xp'=None then (Addr oref)#stk else stk |
26 in (xp' , hp' , stk' , pc+1))" |
26 in (xp' , hp' , stk' , pc+1))" |
27 |
27 |
28 |
28 |
29 datatype |
29 datatype |
30 manipulate_object = |
30 manipulate_object = |
37 |
37 |
38 primrec |
38 primrec |
39 "exec_mo (Getfield F C) hp stk pc = |
39 "exec_mo (Getfield F C) hp stk pc = |
40 (let oref = hd stk; |
40 (let oref = hd stk; |
41 xp' = raise_xcpt (oref=Null) NullPointer; |
41 xp' = raise_xcpt (oref=Null) NullPointer; |
42 (oc,fs) = hp \\<And> (the_Addr oref); |
42 (oc,fs) = hp !! (the_Addr oref); |
43 stk' = xcpt_update xp' ((fs\\<And>(F,C))#(tl stk)) (tl stk) |
43 stk' = if xp'=None then (fs!!(F,C))#(tl stk) else tl stk |
44 in |
44 in |
45 (xp' , hp , stk' , pc+1))" |
45 (xp' , hp , stk' , pc+1))" |
46 |
46 |
47 "exec_mo (Putfield F C) hp stk pc = |
47 "exec_mo (Putfield F C) hp stk pc = |
48 (let (fval,oref)= (hd stk, hd(tl stk)); |
48 (let (fval,oref)= (hd stk, hd(tl stk)); |
49 xp' = raise_xcpt (oref=Null) NullPointer; |
49 xp' = raise_xcpt (oref=Null) NullPointer; |
50 a = the_Addr oref; |
50 a = the_Addr oref; |
51 (oc,fs) = hp \\<And> a; |
51 (oc,fs) = hp !! a; |
52 hp' = xcpt_update xp' (hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval)))) hp |
52 hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp |
53 in |
53 in |
54 (xp' , hp' , tl (tl stk), pc+1))" |
54 (xp' , hp' , tl (tl stk), pc+1))" |
55 |
55 |
56 |
56 |
57 datatype |
57 datatype |