kleing@52396
|
1 |
(* Author: Tobias Nipkow and Gerwin Klein *)
|
nipkow@10343
|
2 |
|
wneuper@59180
|
3 |
section "Compiler for IMP"
|
nipkow@10342
|
4 |
|
kleing@54052
|
5 |
theory Compiler imports Big_Step Star
|
nipkow@43982
|
6 |
begin
|
kleing@12429
|
7 |
|
kleing@44296
|
8 |
subsection "List setup"
|
kleing@44296
|
9 |
|
wneuper@59451
|
10 |
text \<open>
|
kleing@52396
|
11 |
In the following, we use the length of lists as integers
|
kleing@52396
|
12 |
instead of natural numbers. Instead of converting @{typ nat}
|
kleing@52396
|
13 |
to @{typ int} explicitly, we tell Isabelle to coerce @{typ nat}
|
kleing@52396
|
14 |
automatically when necessary.
|
wneuper@59451
|
15 |
\<close>
|
kleing@52396
|
16 |
declare [[coercion_enabled]]
|
kleing@52396
|
17 |
declare [[coercion "int :: nat \<Rightarrow> int"]]
|
kleing@44296
|
18 |
|
wneuper@59451
|
19 |
text \<open>
|
kleing@52396
|
20 |
Similarly, we will want to access the ith element of a list,
|
kleing@52396
|
21 |
where @{term i} is an @{typ int}.
|
wneuper@59451
|
22 |
\<close>
|
nipkow@46501
|
23 |
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
|
nipkow@55006
|
24 |
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
|
kleing@44296
|
25 |
|
wneuper@59451
|
26 |
text \<open>
|
kleing@52396
|
27 |
The only additional lemma we need about this function
|
kleing@52396
|
28 |
is indexing over append:
|
wneuper@59451
|
29 |
\<close>
|
kleing@44296
|
30 |
lemma inth_append [simp]:
|
nipkow@55006
|
31 |
"0 \<le> i \<Longrightarrow>
|
nipkow@55006
|
32 |
(xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
|
nipkow@55006
|
33 |
by (induction xs arbitrary: i) (auto simp: algebra_simps)
|
kleing@44296
|
34 |
|
wneuper@59451
|
35 |
text\<open>We hide coercion @{const int} applied to @{const length}:\<close>
|
nipkow@55095
|
36 |
|
nipkow@55095
|
37 |
abbreviation (output)
|
nipkow@55095
|
38 |
"isize xs == int (length xs)"
|
nipkow@55095
|
39 |
|
nipkow@55095
|
40 |
notation isize ("size")
|
nipkow@55095
|
41 |
|
nipkow@55095
|
42 |
|
nipkow@43982
|
43 |
subsection "Instructions and Stack Machine"
|
nipkow@43982
|
44 |
|
wneuper@59451
|
45 |
text_raw\<open>\snip{instrdef}{0}{1}{%\<close>
|
nipkow@43982
|
46 |
datatype instr =
|
kleing@54043
|
47 |
LOADI int | LOAD vname | ADD | STORE vname |
|
kleing@54043
|
48 |
JMP int | JMPLESS int | JMPGE int
|
wneuper@59451
|
49 |
text_raw\<open>}%endsnip\<close>
|
nipkow@43982
|
50 |
|
kleing@44296
|
51 |
type_synonym stack = "val list"
|
nipkow@46501
|
52 |
type_synonym config = "int \<times> state \<times> stack"
|
nipkow@43982
|
53 |
|
nipkow@43982
|
54 |
abbreviation "hd2 xs == hd(tl xs)"
|
nipkow@43982
|
55 |
abbreviation "tl2 xs == tl(tl xs)"
|
nipkow@43982
|
56 |
|
nipkow@51075
|
57 |
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
|
nipkow@51075
|
58 |
"iexec instr (i,s,stk) = (case instr of
|
nipkow@51075
|
59 |
LOADI n \<Rightarrow> (i+1,s, n#stk) |
|
nipkow@51075
|
60 |
LOAD x \<Rightarrow> (i+1,s, s x # stk) |
|
nipkow@51075
|
61 |
ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
|
nipkow@51075
|
62 |
STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
|
nipkow@51075
|
63 |
JMP n \<Rightarrow> (i+1+n,s,stk) |
|
nipkow@51075
|
64 |
JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk) |
|
nipkow@51075
|
65 |
JMPGE n \<Rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk))"
|
kleing@44296
|
66 |
|
kleing@44871
|
67 |
definition
|
nipkow@51075
|
68 |
exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
|
nipkow@51075
|
69 |
("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)
|
kleing@44871
|
70 |
where
|
kleing@44296
|
71 |
"P \<turnstile> c \<rightarrow> c' =
|
kleing@52396
|
72 |
(\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
|
kleing@44871
|
73 |
|
kleing@44871
|
74 |
lemma exec1I [intro, code_pred_intro]:
|
kleing@52396
|
75 |
"c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
|
nipkow@51075
|
76 |
\<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
|
kleing@54052
|
77 |
by (simp add: exec1_def)
|
nipkow@43982
|
78 |
|
kleing@54052
|
79 |
abbreviation
|
kleing@54052
|
80 |
exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
|
nipkow@43982
|
81 |
where
|
kleing@54052
|
82 |
"exec P \<equiv> star (exec1 P)"
|
nipkow@43982
|
83 |
|
kleing@54052
|
84 |
lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
|
nipkow@43982
|
85 |
|
kleing@54052
|
86 |
code_pred exec1 by (metis exec1_def)
|
nipkow@43982
|
87 |
|
nipkow@43982
|
88 |
values
|
nipkow@43982
|
89 |
"{(i,map t [''x'',''y''],stk) | i t stk.
|
nipkow@43982
|
90 |
[LOAD ''y'', STORE ''x''] \<turnstile>
|
kleing@44907
|
91 |
(0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
|
nipkow@43982
|
92 |
|
nipkow@43982
|
93 |
|
wneuper@59451
|
94 |
subsection\<open>Verification infrastructure\<close>
|
nipkow@43982
|
95 |
|
wneuper@59451
|
96 |
text\<open>Below we need to argue about the execution of code that is embedded in
|
nipkow@43982
|
97 |
larger programs. For this purpose we show that execution is preserved by
|
wneuper@59451
|
98 |
appending code to the left or right of a program.\<close>
|
nipkow@43982
|
99 |
|
nipkow@51075
|
100 |
lemma iexec_shift [simp]:
|
nipkow@51075
|
101 |
"((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
|
nipkow@51075
|
102 |
by(auto split:instr.split)
|
nipkow@51075
|
103 |
|
kleing@44296
|
104 |
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
|
kleing@54052
|
105 |
by (auto simp: exec1_def)
|
nipkow@11275
|
106 |
|
nipkow@43982
|
107 |
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
|
wneuper@59324
|
108 |
by (induction rule: star.induct) (fastforce intro: star.step exec1_appendR)+
|
nipkow@13095
|
109 |
|
nipkow@43982
|
110 |
lemma exec1_appendL:
|
kleing@52396
|
111 |
fixes i i' :: int
|
kleing@52396
|
112 |
shows
|
kleing@44296
|
113 |
"P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
|
kleing@52396
|
114 |
P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
|
kleing@54052
|
115 |
unfolding exec1_def
|
kleing@54089
|
116 |
by (auto simp del: iexec.simps)
|
nipkow@13095
|
117 |
|
nipkow@43982
|
118 |
lemma exec_appendL:
|
kleing@52396
|
119 |
fixes i i' :: int
|
kleing@52396
|
120 |
shows
|
nipkow@43982
|
121 |
"P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
|
kleing@52396
|
122 |
P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
|
wneuper@59324
|
123 |
by (induction rule: exec_induct) (blast intro: star.step exec1_appendL)+
|
nipkow@43982
|
124 |
|
wneuper@59451
|
125 |
text\<open>Now we specialise the above lemmas to enable automatic proofs of
|
nipkow@43982
|
126 |
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
|
nipkow@43982
|
127 |
pieces of code that we already know how they execute (by induction), combined
|
nipkow@43982
|
128 |
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
|
nipkow@43982
|
129 |
The details should be skipped on a first reading.
|
nipkow@43982
|
130 |
|
wneuper@59451
|
131 |
If we have just executed the first instruction of the program, drop it:\<close>
|
nipkow@43982
|
132 |
|
kleing@44296
|
133 |
lemma exec_Cons_1 [intro]:
|
kleing@44296
|
134 |
"P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
|
kleing@44296
|
135 |
instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
|
nipkow@51075
|
136 |
by (drule exec_appendL[where P'="[instr]"]) simp
|
nipkow@10342
|
137 |
|
nipkow@43982
|
138 |
lemma exec_appendL_if[intro]:
|
nipkow@55801
|
139 |
fixes i i' j :: int
|
kleing@52396
|
140 |
shows
|
kleing@52396
|
141 |
"size P' <= i
|
nipkow@55801
|
142 |
\<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
|
nipkow@55801
|
143 |
\<Longrightarrow> i' = size P' + j
|
nipkow@55801
|
144 |
\<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
|
nipkow@51075
|
145 |
by (drule exec_appendL[where P'=P']) simp
|
nipkow@13095
|
146 |
|
wneuper@59451
|
147 |
text\<open>Split the execution of a compound program up into the execution of its
|
wneuper@59451
|
148 |
parts:\<close>
|
nipkow@13095
|
149 |
|
nipkow@43982
|
150 |
lemma exec_append_trans[intro]:
|
kleing@52396
|
151 |
fixes i' i'' j'' :: int
|
kleing@52396
|
152 |
shows
|
nipkow@43982
|
153 |
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
|
kleing@52396
|
154 |
size P \<le> i' \<Longrightarrow>
|
kleing@52396
|
155 |
P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
|
kleing@52396
|
156 |
j'' = size P + i''
|
nipkow@43982
|
157 |
\<Longrightarrow>
|
nipkow@43982
|
158 |
P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
|
kleing@54052
|
159 |
by(metis star_trans[OF exec_appendR exec_appendL_if])
|
nipkow@13095
|
160 |
|
nipkow@43982
|
161 |
|
nipkow@51075
|
162 |
declare Let_def[simp]
|
nipkow@43982
|
163 |
|
nipkow@43982
|
164 |
|
nipkow@43982
|
165 |
subsection "Compilation"
|
nipkow@43982
|
166 |
|
nipkow@43982
|
167 |
fun acomp :: "aexp \<Rightarrow> instr list" where
|
nipkow@43982
|
168 |
"acomp (N n) = [LOADI n]" |
|
nipkow@43982
|
169 |
"acomp (V x) = [LOAD x]" |
|
nipkow@43982
|
170 |
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
|
nipkow@43982
|
171 |
|
nipkow@43982
|
172 |
lemma acomp_correct[intro]:
|
kleing@52396
|
173 |
"acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
|
nipkow@51075
|
174 |
by (induction a arbitrary: stk) fastforce+
|
nipkow@13095
|
175 |
|
kleing@44296
|
176 |
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
|
nipkow@55017
|
177 |
"bcomp (Bc v) f n = (if v=f then [JMP n] else [])" |
|
nipkow@55017
|
178 |
"bcomp (Not b) f n = bcomp b (\<not>f) n" |
|
nipkow@55017
|
179 |
"bcomp (And b1 b2) f n =
|
nipkow@55017
|
180 |
(let cb2 = bcomp b2 f n;
|
kleing@56924
|
181 |
m = if f then size cb2 else (size cb2::int)+n;
|
nipkow@43982
|
182 |
cb1 = bcomp b1 False m
|
nipkow@43982
|
183 |
in cb1 @ cb2)" |
|
nipkow@55017
|
184 |
"bcomp (Less a1 a2) f n =
|
nipkow@55017
|
185 |
acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])"
|
nipkow@43982
|
186 |
|
nipkow@43982
|
187 |
value
|
nipkow@43982
|
188 |
"bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
|
nipkow@43982
|
189 |
False 3"
|
nipkow@43982
|
190 |
|
nipkow@43982
|
191 |
lemma bcomp_correct[intro]:
|
kleing@52396
|
192 |
fixes n :: int
|
kleing@52396
|
193 |
shows
|
kleing@44296
|
194 |
"0 \<le> n \<Longrightarrow>
|
nipkow@55017
|
195 |
bcomp b f n \<turnstile>
|
nipkow@55017
|
196 |
(0,s,stk) \<rightarrow>* (size(bcomp b f n) + (if f = bval b s then n else 0),s,stk)"
|
nipkow@55017
|
197 |
proof(induction b arbitrary: f n)
|
nipkow@43982
|
198 |
case Not
|
nipkow@55017
|
199 |
from Not(1)[where f="~f"] Not(2) show ?case by fastforce
|
nipkow@13095
|
200 |
next
|
nipkow@43982
|
201 |
case (And b1 b2)
|
nipkow@55017
|
202 |
from And(1)[of "if f then size(bcomp b2 f n) else size(bcomp b2 f n) + n"
|
kleing@44296
|
203 |
"False"]
|
nipkow@55017
|
204 |
And(2)[of n f] And(3)
|
nipkow@45761
|
205 |
show ?case by fastforce
|
nipkow@45761
|
206 |
qed fastforce+
|
nipkow@13095
|
207 |
|
nipkow@43982
|
208 |
fun ccomp :: "com \<Rightarrow> instr list" where
|
nipkow@43982
|
209 |
"ccomp SKIP = []" |
|
nipkow@43982
|
210 |
"ccomp (x ::= a) = acomp a @ [STORE x]" |
|
wenzelm@54152
|
211 |
"ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
|
wenzelm@54152
|
212 |
"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
|
wenzelm@54152
|
213 |
(let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
|
wenzelm@54152
|
214 |
in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
|
nipkow@43982
|
215 |
"ccomp (WHILE b DO c) =
|
kleing@52396
|
216 |
(let cc = ccomp c; cb = bcomp b False (size cc + 1)
|
kleing@52396
|
217 |
in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
|
kleing@44875
|
218 |
|
nipkow@13095
|
219 |
|
nipkow@43982
|
220 |
value "ccomp
|
nipkow@43982
|
221 |
(IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
|
nipkow@43982
|
222 |
ELSE ''v'' ::= V ''u'')"
|
nipkow@13095
|
223 |
|
nipkow@43982
|
224 |
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
|
nipkow@13095
|
225 |
|
nipkow@13095
|
226 |
|
Jean@45966
|
227 |
subsection "Preservation of semantics"
|
nipkow@43982
|
228 |
|
kleing@44296
|
229 |
lemma ccomp_bigstep:
|
kleing@52396
|
230 |
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
|
nipkow@45886
|
231 |
proof(induction arbitrary: stk rule: big_step_induct)
|
nipkow@43982
|
232 |
case (Assign x a s)
|
nipkow@45761
|
233 |
show ?case by (fastforce simp:fun_upd_def cong: if_cong)
|
nipkow@13095
|
234 |
next
|
nipkow@48689
|
235 |
case (Seq c1 s1 s2 c2 s3)
|
nipkow@43982
|
236 |
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
|
kleing@52396
|
237 |
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
|
nipkow@48689
|
238 |
using Seq.IH(1) by fastforce
|
nipkow@43982
|
239 |
moreover
|
kleing@52396
|
240 |
have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
|
nipkow@48689
|
241 |
using Seq.IH(2) by fastforce
|
kleing@54052
|
242 |
ultimately show ?case by simp (blast intro: star_trans)
|
nipkow@13095
|
243 |
next
|
nipkow@43982
|
244 |
case (WhileTrue b s1 c s2 s3)
|
nipkow@43982
|
245 |
let ?cc = "ccomp c"
|
kleing@52396
|
246 |
let ?cb = "bcomp b False (size ?cc + 1)"
|
nipkow@43982
|
247 |
let ?cw = "ccomp(WHILE b DO c)"
|
kleing@52396
|
248 |
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)"
|
wneuper@59451
|
249 |
using \<open>bval b s1\<close> by fastforce
|
nipkow@51148
|
250 |
moreover
|
kleing@52396
|
251 |
have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
|
nipkow@51148
|
252 |
using WhileTrue.IH(1) by fastforce
|
nipkow@43982
|
253 |
moreover
|
kleing@52396
|
254 |
have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
|
nipkow@45761
|
255 |
by fastforce
|
nipkow@43982
|
256 |
moreover
|
kleing@52396
|
257 |
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
|
kleing@54052
|
258 |
ultimately show ?case by(blast intro: star_trans)
|
nipkow@45761
|
259 |
qed fastforce+
|
nipkow@13095
|
260 |
|
webertj@20217
|
261 |
end
|