1 (* Author: Tobias Nipkow *)
3 header "A Compiler for IMP"
5 theory Compiler imports Big_Step
8 subsection "List setup"
11 We are going to define a small machine language where programs are
12 lists of instructions. For nicer algebraic properties in our lemmas
13 later, we prefer @{typ int} to @{term nat} as program counter.
15 Therefore, we define notation for size and indexing for lists
18 abbreviation "isize xs == int (length xs)"
21 inth :: "'a list => int => 'a" (infixl "!!" 100) where
22 inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
25 The only additional lemma we need is indexing over append:
27 lemma inth_append [simp]:
28 "0 \<le> n \<Longrightarrow>
29 (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))"
30 by (induct xs arbitrary: n) (auto simp: algebra_simps)
32 subsection "Instructions and Stack Machine"
43 (* reads slightly nicer *)
47 type_synonym stack = "val list"
48 type_synonym config = "int\<times>state\<times>stack"
50 abbreviation "hd2 xs == hd(tl xs)"
51 abbreviation "tl2 xs == tl(tl xs)"
53 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
54 ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50)
56 "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
57 "LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
58 "ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
59 "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
60 "JMP n \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
61 "JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
62 "JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
69 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
71 "P \<turnstile> c \<rightarrow> c' =
72 (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)"
74 declare exec1_def [simp]
76 lemma exec1I [intro, code_pred_intro]:
77 "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
80 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
82 refl: "P \<turnstile> c \<rightarrow>* c" |
83 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
85 declare refl[intro] step[intro]
87 lemmas exec_induct = exec.induct[split_format(complete)]
89 code_pred exec by force
92 "{(i,map t [''x'',''y''],stk) | i t stk.
93 [LOAD ''y'', STORE ''x''] \<turnstile>
94 (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
97 subsection{* Verification infrastructure *}
99 lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
100 by (induct rule: exec.induct) fastsimp+
102 inductive_cases iexec1_cases [elim!]:
103 "LOADI n \<turnstile>i c \<rightarrow> c'"
104 "LOAD x \<turnstile>i c \<rightarrow> c'"
105 "ADD \<turnstile>i c \<rightarrow> c'"
106 "STORE n \<turnstile>i c \<rightarrow> c'"
107 "JMP n \<turnstile>i c \<rightarrow> c'"
108 "JMPFLESS n \<turnstile>i c \<rightarrow> c'"
109 "JMPFGE n \<turnstile>i c \<rightarrow> c'"
111 text {* Simplification rules for @{const iexec1}. *}
112 lemma iexec1_simps [simp]:
113 "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))"
114 "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))"
115 "ADD \<turnstile>i c \<rightarrow> c' =
116 (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
117 "STORE x \<turnstile>i c \<rightarrow> c' =
118 (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))"
119 "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
120 "JMPFLESS n \<turnstile>i c \<rightarrow> c' =
121 (\<exists>i s stk. c = (i, s, stk) \<and>
122 c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"
123 "JMPFGE n \<turnstile>i c \<rightarrow> c' =
124 (\<exists>i s stk. c = (i, s, stk) \<and>
125 c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
126 by (auto split del: split_if intro!: iexec1.intros)
129 text{* Below we need to argue about the execution of code that is embedded in
130 larger programs. For this purpose we show that execution is preserved by
131 appending code to the left or right of a program. *}
133 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
136 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
137 by (induct rule: exec.induct) (fastsimp intro: exec1_appendR)+
140 assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
141 shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
142 using assms by cases auto
145 assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
146 shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
147 using assms by cases auto
149 lemma iexec_shift [simp]:
150 "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))"
151 by (blast intro: iexec1_shiftI dest: iexec1_shiftD)
154 "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
155 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
159 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
160 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
161 by (induct rule: exec_induct) (blast intro!: exec1_appendL)+
163 text{* Now we specialise the above lemmas to enable automatic proofs of
164 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
165 pieces of code that we already know how they execute (by induction), combined
166 by @{text "@"} and @{text "#"}. Backward jumps are not supported.
167 The details should be skipped on a first reading.
169 If we have just executed the first instruction of the program, drop it: *}
171 lemma exec_Cons_1 [intro]:
172 "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
173 instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
174 by (drule exec_appendL[where P'="[instr]"]) simp
176 lemma exec_appendL_if[intro]:
178 \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
179 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
180 by (drule exec_appendL[where P'=P']) simp
182 text{* Split the execution of a compound program up into the excution of its
185 lemma exec_append_trans[intro]:
186 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
187 isize P \<le> i' \<Longrightarrow>
188 P' \<turnstile> (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
191 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
192 by(metis exec_trans[OF exec_appendR exec_appendL_if])
195 declare Let_def[simp]
198 subsection "Compilation"
200 fun acomp :: "aexp \<Rightarrow> instr list" where
201 "acomp (N n) = [LOADI n]" |
202 "acomp (V x) = [LOAD x]" |
203 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
205 lemma acomp_correct[intro]:
206 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
207 by (induct a arbitrary: stk) fastsimp+
209 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
210 "bcomp (B bv) c n = (if bv=c then [JMP n] else [])" |
211 "bcomp (Not b) c n = bcomp b (\<not>c) n" |
212 "bcomp (And b1 b2) c n =
213 (let cb2 = bcomp b2 c n;
214 m = (if c then isize cb2 else isize cb2+n);
215 cb1 = bcomp b1 False m
217 "bcomp (Less a1 a2) c n =
218 acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
221 "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
224 lemma bcomp_correct[intro]:
225 "0 \<le> n \<Longrightarrow>
226 bcomp b c n \<turnstile>
227 (0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
228 proof(induct b arbitrary: c n m)
230 from Not(1)[where c="~c"] Not(2) show ?case by fastsimp
233 from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n"
235 And(2)[of n "c"] And(3)
236 show ?case by fastsimp
239 fun ccomp :: "com \<Rightarrow> instr list" where
241 "ccomp (x ::= a) = acomp a @ [STORE x]" |
242 "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
243 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
244 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1)
245 in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
246 "ccomp (WHILE b DO c) =
247 (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
248 in cb @ cc @ [JMPB (isize cb + isize cc + 1)])"
251 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
252 ELSE ''v'' ::= V ''u'')"
254 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
257 subsection "Preservation of sematics"
260 "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
261 proof(induct arbitrary: stk rule: big_step_induct)
263 show ?case by (fastsimp simp:fun_upd_def cong: if_cong)
265 case (Semi c1 s1 s2 c2 s3)
266 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
267 have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
268 using Semi.hyps(2) by fastsimp
270 have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
271 using Semi.hyps(4) by fastsimp
272 ultimately show ?case by simp (blast intro: exec_trans)
274 case (WhileTrue b s1 c s2 s3)
276 let ?cb = "bcomp b False (isize ?cc + 1)"
277 let ?cw = "ccomp(WHILE b DO c)"
278 have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
279 using WhileTrue(1,3) by fastsimp
281 have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
284 have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
285 ultimately show ?case by(blast intro: exec_trans)