34 "isRef v \<equiv> v = Null \<or> isAddr v" |
34 "isRef v \<equiv> v = Null \<or> isAddr v" |
35 |
35 |
36 |
36 |
37 consts |
37 consts |
38 check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, |
38 check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, |
39 cname, sig, p_count, frame list] \<Rightarrow> bool" |
39 cname, sig, p_count, nat, frame list] \<Rightarrow> bool" |
40 primrec |
40 primrec |
41 "check_instr (Load idx) G hp stk vars C sig pc frs = |
41 "check_instr (Load idx) G hp stk vars C sig pc mxs frs = |
42 (idx < length vars)" |
42 (idx < length vars \<and> size stk < mxs)" |
43 |
43 |
44 "check_instr (Store idx) G hp stk vars Cl sig pc frs = |
44 "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs = |
45 (0 < length stk \<and> idx < length vars)" |
45 (0 < length stk \<and> idx < length vars)" |
46 |
46 |
47 "check_instr (LitPush v) G hp stk vars Cl sig pc frs = |
47 "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs = |
48 (\<not>isAddr v)" |
48 (\<not>isAddr v \<and> size stk < mxs)" |
49 |
49 |
50 "check_instr (New C) G hp stk vars Cl sig pc frs = |
50 "check_instr (New C) G hp stk vars Cl sig pc mxs frs = |
51 is_class G C" |
51 (is_class G C \<and> size stk < mxs)" |
52 |
52 |
53 "check_instr (Getfield F C) G hp stk vars Cl sig pc frs = |
53 "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs frs = |
54 (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> |
54 (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> |
55 (let (C', T) = the (field (G,C) F); ref = hd stk in |
55 (let (C', T) = the (field (G,C) F); ref = hd stk in |
56 C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> |
56 C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> |
57 hp (the_Addr ref) \<noteq> None \<and> |
57 hp (the_Addr ref) \<noteq> None \<and> |
58 (let (D,vs) = the (hp (the_Addr ref)) in |
58 (let (D,vs) = the (hp (the_Addr ref)) in |
59 G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" |
59 G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" |
60 |
60 |
61 "check_instr (Putfield F C) G hp stk vars Cl sig pc frs = |
61 "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs frs = |
62 (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> |
62 (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> |
63 (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in |
63 (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in |
64 C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> |
64 C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> |
65 hp (the_Addr ref) \<noteq> None \<and> |
65 hp (the_Addr ref) \<noteq> None \<and> |
66 (let (D,vs) = the (hp (the_Addr ref)) in |
66 (let (D,vs) = the (hp (the_Addr ref)) in |
67 G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" |
67 G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" |
68 |
68 |
69 "check_instr (Checkcast C) G hp stk vars Cl sig pc frs = |
69 "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs = |
70 (0 < length stk \<and> is_class G C \<and> isRef (hd stk))" |
70 (0 < length stk \<and> is_class G C \<and> isRef (hd stk))" |
71 |
71 |
72 "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs = |
72 "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs = |
73 (length ps < length stk \<and> |
73 (length ps < length stk \<and> |
74 (let n = length ps; v = stk!n in |
74 (let n = length ps; v = stk!n in |
75 isRef v \<and> (v \<noteq> Null \<longrightarrow> |
75 isRef v \<and> (v \<noteq> Null \<longrightarrow> |
76 hp (the_Addr v) \<noteq> None \<and> |
76 hp (the_Addr v) \<noteq> None \<and> |
77 method (G,cname_of hp v) (mn,ps) \<noteq> None \<and> |
77 method (G,cname_of hp v) (mn,ps) \<noteq> None \<and> |
78 list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))" |
78 list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))" |
79 |
79 |
80 "check_instr Return G hp stk0 vars Cl sig0 pc frs = |
80 "check_instr Return G hp stk0 vars Cl sig0 pc mxs frs = |
81 (0 < length stk0 \<and> (0 < length frs \<longrightarrow> |
81 (0 < length stk0 \<and> (0 < length frs \<longrightarrow> |
82 method (G,Cl) sig0 \<noteq> None \<and> |
82 method (G,Cl) sig0 \<noteq> None \<and> |
83 (let v = hd stk0; (C, rT, body) = the (method (G,Cl) sig0) in |
83 (let v = hd stk0; (C, rT, body) = the (method (G,Cl) sig0) in |
84 Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))" |
84 Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))" |
85 |
85 |
86 "check_instr Pop G hp stk vars Cl sig pc frs = |
86 "check_instr Pop G hp stk vars Cl sig pc mxs frs = |
87 (0 < length stk)" |
87 (0 < length stk)" |
88 |
88 |
89 "check_instr Dup G hp stk vars Cl sig pc frs = |
89 "check_instr Dup G hp stk vars Cl sig pc mxs frs = |
90 (0 < length stk)" |
90 (0 < length stk \<and> size stk < mxs)" |
91 |
91 |
92 "check_instr Dup_x1 G hp stk vars Cl sig pc frs = |
92 "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs = |
|
93 (1 < length stk \<and> size stk < mxs)" |
|
94 |
|
95 "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs = |
|
96 (2 < length stk \<and> size stk < mxs)" |
|
97 |
|
98 "check_instr Swap G hp stk vars Cl sig pc mxs frs = |
93 (1 < length stk)" |
99 (1 < length stk)" |
94 |
100 |
95 "check_instr Dup_x2 G hp stk vars Cl sig pc frs = |
101 "check_instr IAdd G hp stk vars Cl sig pc mxs frs = |
96 (2 < length stk)" |
|
97 |
|
98 "check_instr Swap G hp stk vars Cl sig pc frs = |
|
99 (1 < length stk)" |
|
100 |
|
101 "check_instr IAdd G hp stk vars Cl sig pc frs = |
|
102 (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))" |
102 (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))" |
103 |
103 |
104 "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc frs = |
104 "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs = |
105 (1 < length stk \<and> 0 \<le> int pc+b)" |
105 (1 < length stk \<and> 0 \<le> int pc+b)" |
106 |
106 |
107 "check_instr (Goto b) G hp stk vars Cl sig pc frs = |
107 "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs = |
108 (0 \<le> int pc+b)" |
108 (0 \<le> int pc+b)" |
109 |
109 |
110 "check_instr Throw G hp stk vars Cl sig pc frs = |
110 "check_instr Throw G hp stk vars Cl sig pc mxs frs = |
111 (0 < length stk \<and> isRef (hd stk))" |
111 (0 < length stk \<and> isRef (hd stk))" |
112 |
112 |
113 constdefs |
113 constdefs |
114 check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool" |
114 check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool" |
115 "check G s \<equiv> let (xcpt, hp, frs) = s in |
115 "check G s \<equiv> let (xcpt, hp, frs) = s in |
116 (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> |
116 (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> |
117 (let ins = fifth (the (method (G,C) sig)); i = ins!pc in |
117 (let (C',rt,mxs,mxl,ins,et) = the (method (G,C) sig); i = ins!pc in |
118 pc < size ins \<and> |
118 pc < size ins \<and> |
119 check_instr i G hp stk loc C sig pc frs'))" |
119 check_instr i G hp stk loc C sig pc mxs frs'))" |
120 |
120 |
121 |
121 |
122 exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error" |
122 exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error" |
123 "exec_d G s \<equiv> case s of |
123 "exec_d G s \<equiv> case s of |
124 TypeError \<Rightarrow> TypeError |
124 TypeError \<Rightarrow> TypeError |