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 type_synonym stack = "val list"
44 type_synonym config = "int\<times>state\<times>stack"
46 abbreviation "hd2 xs == hd(tl xs)"
47 abbreviation "tl2 xs == tl(tl xs)"
49 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
50 ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
52 "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
53 "LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
54 "ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
55 "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
56 "JMP n \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
57 "JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
58 "JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
65 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)
67 "P \<turnstile> c \<rightarrow> c' =
68 (\<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)"
70 declare exec1_def [simp]
72 lemma exec1I [intro, code_pred_intro]:
73 assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P"
74 shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
77 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
79 refl: "P \<turnstile> c \<rightarrow>* c" |
80 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
82 declare refl[intro] step[intro]
84 lemmas exec_induct = exec.induct[split_format(complete)]
86 code_pred exec by force
89 "{(i,map t [''x'',''y''],stk) | i t stk.
90 [LOAD ''y'', STORE ''x''] \<turnstile>
91 (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
94 subsection{* Verification infrastructure *}
96 lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
97 by (induct rule: exec.induct) fastforce+
99 inductive_cases iexec1_cases [elim!]:
100 "LOADI n \<turnstile>i c \<rightarrow> c'"
101 "LOAD x \<turnstile>i c \<rightarrow> c'"
102 "ADD \<turnstile>i c \<rightarrow> c'"
103 "STORE n \<turnstile>i c \<rightarrow> c'"
104 "JMP n \<turnstile>i c \<rightarrow> c'"
105 "JMPFLESS n \<turnstile>i c \<rightarrow> c'"
106 "JMPFGE n \<turnstile>i c \<rightarrow> c'"
108 text {* Simplification rules for @{const iexec1}. *}
109 lemma iexec1_simps [simp]:
110 "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))"
111 "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))"
112 "ADD \<turnstile>i c \<rightarrow> c' =
113 (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
114 "STORE x \<turnstile>i c \<rightarrow> c' =
115 (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
116 "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
117 "JMPFLESS n \<turnstile>i c \<rightarrow> c' =
118 (\<exists>i s stk. c = (i, s, stk) \<and>
119 c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"
120 "JMPFGE n \<turnstile>i c \<rightarrow> c' =
121 (\<exists>i s stk. c = (i, s, stk) \<and>
122 c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
123 by (auto split del: split_if intro!: iexec1.intros)
126 text{* Below we need to argue about the execution of code that is embedded in
127 larger programs. For this purpose we show that execution is preserved by
128 appending code to the left or right of a program. *}
130 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
133 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
134 by (induct rule: exec.induct) (fastforce intro: exec1_appendR)+
137 assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
138 shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
139 using assms by cases auto
142 assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
143 shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
144 using assms by cases auto
146 lemma iexec_shift [simp]:
147 "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))"
148 by (blast intro: iexec1_shiftI dest: iexec1_shiftD)
151 "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
152 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
156 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
157 P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
158 by (induct rule: exec_induct) (blast intro!: exec1_appendL)+
160 text{* Now we specialise the above lemmas to enable automatic proofs of
161 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
162 pieces of code that we already know how they execute (by induction), combined
163 by @{text "@"} and @{text "#"}. Backward jumps are not supported.
164 The details should be skipped on a first reading.
166 If we have just executed the first instruction of the program, drop it: *}
168 lemma exec_Cons_1 [intro]:
169 "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
170 instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
171 by (drule exec_appendL[where P'="[instr]"]) simp
173 lemma exec_appendL_if[intro]:
175 \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
176 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
177 by (drule exec_appendL[where P'=P']) simp
179 text{* Split the execution of a compound program up into the excution of its
182 lemma exec_append_trans[intro]:
183 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
184 isize P \<le> i' \<Longrightarrow>
185 P' \<turnstile> (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
188 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
189 by(metis exec_trans[OF exec_appendR exec_appendL_if])
192 declare Let_def[simp]
195 subsection "Compilation"
197 fun acomp :: "aexp \<Rightarrow> instr list" where
198 "acomp (N n) = [LOADI n]" |
199 "acomp (V x) = [LOAD x]" |
200 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
202 lemma acomp_correct[intro]:
203 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
204 by (induct a arbitrary: stk) fastforce+
206 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
207 "bcomp (B bv) c n = (if bv=c then [JMP n] else [])" |
208 "bcomp (Not b) c n = bcomp b (\<not>c) n" |
209 "bcomp (And b1 b2) c n =
210 (let cb2 = bcomp b2 c n;
211 m = (if c then isize cb2 else isize cb2+n);
212 cb1 = bcomp b1 False m
214 "bcomp (Less a1 a2) c n =
215 acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
218 "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
221 lemma bcomp_correct[intro]:
222 "0 \<le> n \<Longrightarrow>
223 bcomp b c n \<turnstile>
224 (0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
225 proof(induction b arbitrary: c n)
227 from Not(1)[where c="~c"] Not(2) show ?case by fastforce
230 from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n"
232 And(2)[of n "c"] And(3)
233 show ?case by fastforce
236 fun ccomp :: "com \<Rightarrow> instr list" where
238 "ccomp (x ::= a) = acomp a @ [STORE x]" |
239 "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
240 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
241 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1)
242 in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
243 "ccomp (WHILE b DO c) =
244 (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
245 in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
249 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
250 ELSE ''v'' ::= V ''u'')"
252 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
255 subsection "Preservation of semantics"
258 "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
259 proof(induction arbitrary: stk rule: big_step_induct)
261 show ?case by (fastforce simp:fun_upd_def cong: if_cong)
263 case (Semi c1 s1 s2 c2 s3)
264 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
265 have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
266 using Semi.IH(1) by fastforce
268 have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
269 using Semi.IH(2) by fastforce
270 ultimately show ?case by simp (blast intro: exec_trans)
272 case (WhileTrue b s1 c s2 s3)
274 let ?cb = "bcomp b False (isize ?cc + 1)"
275 let ?cw = "ccomp(WHILE b DO c)"
276 have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
277 using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
279 have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
282 have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
283 ultimately show ?case by(blast intro: exec_trans)