1(*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
2    Author:     Gerwin Klein
3*)
4
5section \<open>A Defensive JVM\<close>
6
7theory JVMDefensive
8imports JVMExec
9begin
10
11text \<open>
12  Extend the state space by one element indicating a type error (or
13  other abnormal termination)\<close>
14datatype 'a type_error = TypeError | Normal 'a
15
16
17abbreviation
18  fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
19  where "fifth x == fst(snd(snd(snd(snd x))))"
20
21fun isAddr :: "val \<Rightarrow> bool" where
22  "isAddr (Addr loc) = True"
23| "isAddr v          = False"
24
25fun isIntg :: "val \<Rightarrow> bool" where
26  "isIntg (Intg i) = True"
27| "isIntg v        = False"
28
29definition isRef :: "val \<Rightarrow> bool" where
30  "isRef v \<equiv> v = Null \<or> isAddr v"
31
32primrec check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
33                  cname, sig, p_count, nat, frame list] \<Rightarrow> bool" where
34  "check_instr (Load idx) G hp stk vars C sig pc mxs frs = 
35  (idx < length vars \<and> size stk < mxs)"
36
37| "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs = 
38  (0 < length stk \<and> idx < length vars)"
39
40| "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs = 
41  (\<not>isAddr v \<and> size stk < mxs)"
42
43| "check_instr (New C) G hp stk vars Cl sig pc mxs frs = 
44  (is_class G C \<and> size stk < mxs)"
45
46| "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs frs = 
47  (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
48  (let (C', T) = the (field (G,C) F); ref = hd stk in 
49    C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
50      hp (the_Addr ref) \<noteq> None \<and> 
51      (let (D,vs) = the (hp (the_Addr ref)) in 
52        G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" 
53
54| "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs frs = 
55  (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
56  (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in 
57    C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
58      hp (the_Addr ref) \<noteq> None \<and> 
59      (let (D,vs) = the (hp (the_Addr ref)) in 
60        G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" 
61
62| "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs =
63  (0 < length stk \<and> is_class G C \<and> isRef (hd stk))"
64
65| "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs =
66  (length ps < length stk \<and> 
67  (let n = length ps; v = stk!n in
68  isRef v \<and> (v \<noteq> Null \<longrightarrow> 
69    hp (the_Addr v) \<noteq> None \<and>
70    method (G,cname_of hp v) (mn,ps) \<noteq> None \<and>
71    list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))"
72  
73| "check_instr Return G hp stk0 vars Cl sig0 pc mxs frs =
74  (0 < length stk0 \<and> (0 < length frs \<longrightarrow> 
75    method (G,Cl) sig0 \<noteq> None \<and>    
76    (let v = hd stk0;  (C, rT, body) = the (method (G,Cl) sig0) in
77    Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))"
78 
79| "check_instr Pop G hp stk vars Cl sig pc mxs frs = 
80  (0 < length stk)"
81
82| "check_instr Dup G hp stk vars Cl sig pc mxs frs = 
83  (0 < length stk \<and> size stk < mxs)"
84
85| "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs = 
86  (1 < length stk \<and> size stk < mxs)"
87
88| "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs = 
89  (2 < length stk \<and> size stk < mxs)"
90
91| "check_instr Swap G hp stk vars Cl sig pc mxs frs =
92  (1 < length stk)"
93
94| "check_instr IAdd G hp stk vars Cl sig pc mxs frs =
95  (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))"
96
97| "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs =
98  (1 < length stk \<and> 0 \<le> int pc+b)"
99
100| "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs =
101  (0 \<le> int pc+b)"
102
103| "check_instr Throw G hp stk vars Cl sig pc mxs frs =
104  (0 < length stk \<and> isRef (hd stk))"
105
106definition check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool" where
107  "check G s \<equiv> let (xcpt, hp, frs) = s in
108               (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> 
109                (let  (C',rt,mxs,mxl,ins,et) = the (method (G,C) sig); i = ins!pc in
110                 pc < size ins \<and> 
111                 check_instr i G hp stk loc C sig pc mxs frs'))"
112
113
114definition exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error" where
115  "exec_d G s \<equiv> case s of 
116      TypeError \<Rightarrow> TypeError 
117    | Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
118
119
120definition
121  exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
122                   ("_ \<turnstile> _ \<midarrow>jvmd\<rightarrow> _" [61,61,61]60) where
123  "G \<turnstile> s \<midarrow>jvmd\<rightarrow> t \<longleftrightarrow>
124         (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
125                  {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
126
127
128declare split_paired_All [simp del]
129declare split_paired_Ex [simp del]
130
131lemma [dest!]:
132  "(if P then A else B) \<noteq> B \<Longrightarrow> P"
133  by (cases P, auto)
134
135lemma exec_d_no_errorI [intro]:
136  "check G s \<Longrightarrow> exec_d G (Normal s) \<noteq> TypeError"
137  by (unfold exec_d_def) simp
138
139theorem no_type_error_commutes:
140  "exec_d G (Normal s) \<noteq> TypeError \<Longrightarrow> 
141  exec_d G (Normal s) = Normal (exec (G, s))"
142  by (unfold exec_d_def, auto)
143
144
145lemma defensive_imp_aggressive:
146  "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t"
147proof -
148  have "\<And>x y. G \<turnstile> x \<midarrow>jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow>  G \<turnstile> s \<midarrow>jvm\<rightarrow> t"
149    apply (unfold exec_all_d_def)
150    apply (erule rtrancl_induct)
151     apply (simp add: exec_all_def)
152    apply (fold exec_all_d_def)
153    apply simp
154    apply (intro allI impI)
155    apply (erule disjE, simp)
156    apply (elim exE conjE)
157    apply (erule allE, erule impE, assumption)
158    apply (simp add: exec_all_def exec_d_def split: type_error.splits if_split_asm)
159    apply (rule rtrancl_trans, assumption)
160    apply blast
161    done
162  moreover
163  assume "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)" 
164  ultimately
165  show "G \<turnstile> s \<midarrow>jvm\<rightarrow> t" by blast
166qed
167
168end
169