11 |
11 |
12 types |
12 types |
13 succ_type = "(p_count \<times> state_type option) list" |
13 succ_type = "(p_count \<times> state_type option) list" |
14 |
14 |
15 text {* Program counter of successor instructions: *} |
15 text {* Program counter of successor instructions: *} |
16 consts |
16 primrec succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" where |
17 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" |
|
18 primrec |
|
19 "succs (Load idx) pc = [pc+1]" |
17 "succs (Load idx) pc = [pc+1]" |
20 "succs (Store idx) pc = [pc+1]" |
18 | "succs (Store idx) pc = [pc+1]" |
21 "succs (LitPush v) pc = [pc+1]" |
19 | "succs (LitPush v) pc = [pc+1]" |
22 "succs (Getfield F C) pc = [pc+1]" |
20 | "succs (Getfield F C) pc = [pc+1]" |
23 "succs (Putfield F C) pc = [pc+1]" |
21 | "succs (Putfield F C) pc = [pc+1]" |
24 "succs (New C) pc = [pc+1]" |
22 | "succs (New C) pc = [pc+1]" |
25 "succs (Checkcast C) pc = [pc+1]" |
23 | "succs (Checkcast C) pc = [pc+1]" |
26 "succs Pop pc = [pc+1]" |
24 | "succs Pop pc = [pc+1]" |
27 "succs Dup pc = [pc+1]" |
25 | "succs Dup pc = [pc+1]" |
28 "succs Dup_x1 pc = [pc+1]" |
26 | "succs Dup_x1 pc = [pc+1]" |
29 "succs Dup_x2 pc = [pc+1]" |
27 | "succs Dup_x2 pc = [pc+1]" |
30 "succs Swap pc = [pc+1]" |
28 | "succs Swap pc = [pc+1]" |
31 "succs IAdd pc = [pc+1]" |
29 | "succs IAdd pc = [pc+1]" |
32 "succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]" |
30 | "succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]" |
33 "succs (Goto b) pc = [nat (int pc + b)]" |
31 | "succs (Goto b) pc = [nat (int pc + b)]" |
34 "succs Return pc = [pc]" |
32 | "succs Return pc = [pc]" |
35 "succs (Invoke C mn fpTs) pc = [pc+1]" |
33 | "succs (Invoke C mn fpTs) pc = [pc+1]" |
36 "succs Throw pc = [pc]" |
34 | "succs Throw pc = [pc]" |
37 |
35 |
38 text "Effect of instruction on the state type:" |
36 text "Effect of instruction on the state type:" |
39 consts |
37 consts |
40 eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type" |
38 eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type" |
41 |
39 |
61 -- "Throw always terminates abruptly" |
59 -- "Throw always terminates abruptly" |
62 "eff' (Throw, G, s) = s" |
60 "eff' (Throw, G, s) = s" |
63 "eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST |
61 "eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST |
64 in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
62 in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
65 |
63 |
66 |
64 primrec match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" where |
67 consts |
|
68 match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" |
|
69 primrec |
|
70 "match_any G pc [] = []" |
65 "match_any G pc [] = []" |
71 "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e; |
66 | "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e; |
72 es' = match_any G pc es |
67 es' = match_any G pc es |
73 in |
68 in |
74 if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')" |
69 if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')" |
75 |
70 |
76 consts |
71 primrec match :: "jvm_prog \<Rightarrow> xcpt \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" where |
77 match :: "jvm_prog \<Rightarrow> xcpt \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" |
|
78 primrec |
|
79 "match G X pc [] = []" |
72 "match G X pc [] = []" |
80 "match G X pc (e#es) = |
73 | "match G X pc (e#es) = |
81 (if match_exception_entry G (Xcpt X) pc e then [Xcpt X] else match G X pc es)" |
74 (if match_exception_entry G (Xcpt X) pc e then [Xcpt X] else match G X pc es)" |
82 |
75 |
83 lemma match_some_entry: |
76 lemma match_some_entry: |
84 "match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])" |
77 "match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])" |
85 by (induct et) auto |
78 by (induct et) auto |
94 "xcpt_names (Throw, G, pc, et) = match_any G pc et" |
87 "xcpt_names (Throw, G, pc, et) = match_any G pc et" |
95 "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" |
88 "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" |
96 "xcpt_names (i, G, pc, et) = []" |
89 "xcpt_names (i, G, pc, et) = []" |
97 |
90 |
98 |
91 |
99 constdefs |
92 definition xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type" where |
100 xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type" |
|
101 "xcpt_eff i G pc s et == |
93 "xcpt_eff i G pc s et == |
102 map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None | Some s' \<Rightarrow> Some ([Class C], snd s'))) |
94 map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None | Some s' \<Rightarrow> Some ([Class C], snd s'))) |
103 (xcpt_names (i,G,pc,et))" |
95 (xcpt_names (i,G,pc,et))" |
104 |
96 |
105 norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option" |
97 definition norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option" where |
106 "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))" |
98 "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))" |
107 |
99 |
108 eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type" |
100 definition eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type" where |
109 "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)" |
101 "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)" |
110 |
102 |
111 constdefs |
103 definition isPrimT :: "ty \<Rightarrow> bool" where |
112 isPrimT :: "ty \<Rightarrow> bool" |
|
113 "isPrimT T == case T of PrimT T' \<Rightarrow> True | RefT T' \<Rightarrow> False" |
104 "isPrimT T == case T of PrimT T' \<Rightarrow> True | RefT T' \<Rightarrow> False" |
114 |
105 |
115 isRefT :: "ty \<Rightarrow> bool" |
106 definition isRefT :: "ty \<Rightarrow> bool" where |
116 "isRefT T == case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> True" |
107 "isRefT T == case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> True" |
117 |
108 |
118 lemma isPrimT [simp]: |
109 lemma isPrimT [simp]: |
119 "isPrimT T = (\<exists>T'. T = PrimT T')" by (simp add: isPrimT_def split: ty.splits) |
110 "isPrimT T = (\<exists>T'. T = PrimT T')" by (simp add: isPrimT_def split: ty.splits) |
120 |
111 |
175 G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> |
166 G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> |
176 list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))" |
167 list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))" |
177 |
168 |
178 "app' (i,G, pc,maxs,rT,s) = False" |
169 "app' (i,G, pc,maxs,rT,s) = False" |
179 |
170 |
180 constdefs |
171 definition xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool" where |
181 xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool" |
|
182 "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C" |
172 "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C" |
183 |
173 |
184 app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> bool" |
174 definition app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> bool" where |
185 "app i G maxs rT pc et s == case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et" |
175 "app i G maxs rT pc et s == case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et" |
186 |
176 |
187 |
177 |
188 lemma match_any_match_table: |
178 lemma match_any_match_table: |
189 "C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None" |
179 "C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None" |