1 (* Author: Tobias Nipkow and Gerwin Klein *)
3 header "Compiler for IMP"
5 theory Compiler imports Big_Step Star
8 subsection "List setup"
11 In the following, we use the length of lists as integers
12 instead of natural numbers. Instead of converting @{typ nat}
13 to @{typ int} explicitly, we tell Isabelle to coerce @{typ nat}
14 automatically when necessary.
16 declare [[coercion_enabled]]
17 declare [[coercion "int :: nat \<Rightarrow> int"]]
20 Similarly, we will want to access the ith element of a list,
21 where @{term i} is an @{typ int}.
23 fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
24 "(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
27 The only additional lemma we need about this function
28 is indexing over append:
30 lemma inth_append [simp]:
31 "0 \<le> i \<Longrightarrow>
32 (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
33 by (induction xs arbitrary: i) (auto simp: algebra_simps)
35 text{* We hide coercion @{const int} applied to @{const length}: *}
38 "isize xs == int (length xs)"
40 notation isize ("size")
43 subsection "Instructions and Stack Machine"
45 text_raw{*\snip{instrdef}{0}{1}{% *}
47 LOADI int | LOAD vname | ADD | STORE vname |
48 JMP int | JMPLESS int | JMPGE int
51 type_synonym stack = "val list"
52 type_synonym config = "int \<times> state \<times> stack"
54 abbreviation "hd2 xs == hd(tl xs)"
55 abbreviation "tl2 xs == tl(tl xs)"
57 fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
58 "iexec instr (i,s,stk) = (case instr of
59 LOADI n \<Rightarrow> (i+1,s, n#stk) |
60 LOAD x \<Rightarrow> (i+1,s, s x # stk) |
61 ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
62 STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
63 JMP n \<Rightarrow> (i+1+n,s,stk) |
64 JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk) |
65 JMPGE n \<Rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk))"
68 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
69 ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)
71 "P \<turnstile> c \<rightarrow> c' =
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)"
74 lemma exec1I [intro, code_pred_intro]:
75 "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
76 \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
77 by (simp add: exec1_def)
80 exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
82 "exec P \<equiv> star (exec1 P)"
84 declare star.step[intro]
86 lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
88 code_pred exec1 by (metis exec1_def)
91 "{(i,map t [''x'',''y''],stk) | i t stk.
92 [LOAD ''y'', STORE ''x''] \<turnstile>
93 (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
96 subsection{* Verification infrastructure *}
98 text{* Below we need to argue about the execution of code that is embedded in
99 larger programs. For this purpose we show that execution is preserved by
100 appending code to the left or right of a program. *}
102 lemma iexec_shift [simp]:
103 "((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
104 by(auto split:instr.split)
106 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
107 by (auto simp: exec1_def)
109 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
110 by (induction rule: star.induct) (fastforce intro: exec1_appendR)+
115 "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
116 P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
118 by (auto simp del: iexec.simps)
123 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
124 P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
125 by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
127 text{* Now we specialise the above lemmas to enable automatic proofs of
128 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
129 pieces of code that we already know how they execute (by induction), combined
130 by @{text "@"} and @{text "#"}. Backward jumps are not supported.
131 The details should be skipped on a first reading.
133 If we have just executed the first instruction of the program, drop it: *}
135 lemma exec_Cons_1 [intro]:
136 "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
137 instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
138 by (drule exec_appendL[where P'="[instr]"]) simp
140 lemma exec_appendL_if[intro]:
144 \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
145 \<Longrightarrow> i' = size P' + j
146 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
147 by (drule exec_appendL[where P'=P']) simp
149 text{* Split the execution of a compound program up into the excution of its
152 lemma exec_append_trans[intro]:
153 fixes i' i'' j'' :: int
155 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
156 size P \<le> i' \<Longrightarrow>
157 P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
160 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
161 by(metis star_trans[OF exec_appendR exec_appendL_if])
164 declare Let_def[simp]
167 subsection "Compilation"
169 fun acomp :: "aexp \<Rightarrow> instr list" where
170 "acomp (N n) = [LOADI n]" |
171 "acomp (V x) = [LOAD x]" |
172 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
174 lemma acomp_correct[intro]:
175 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
176 by (induction a arbitrary: stk) fastforce+
178 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
179 "bcomp (Bc v) f n = (if v=f then [JMP n] else [])" |
180 "bcomp (Not b) f n = bcomp b (\<not>f) n" |
181 "bcomp (And b1 b2) f n =
182 (let cb2 = bcomp b2 f n;
183 m = (if f then size cb2 else (size cb2::int)+n);
184 cb1 = bcomp b1 False m
186 "bcomp (Less a1 a2) f n =
187 acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])"
190 "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
193 lemma bcomp_correct[intro]:
196 "0 \<le> n \<Longrightarrow>
197 bcomp b f n \<turnstile>
198 (0,s,stk) \<rightarrow>* (size(bcomp b f n) + (if f = bval b s then n else 0),s,stk)"
199 proof(induction b arbitrary: f n)
201 from Not(1)[where f="~f"] Not(2) show ?case by fastforce
204 from And(1)[of "if f then size(bcomp b2 f n) else size(bcomp b2 f n) + n"
206 And(2)[of n f] And(3)
207 show ?case by fastforce
210 fun ccomp :: "com \<Rightarrow> instr list" where
212 "ccomp (x ::= a) = acomp a @ [STORE x]" |
213 "ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
214 "ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
215 (let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
216 in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
217 "ccomp (WHILE b DO c) =
218 (let cc = ccomp c; cb = bcomp b False (size cc + 1)
219 in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
223 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
224 ELSE ''v'' ::= V ''u'')"
226 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
229 subsection "Preservation of semantics"
232 "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
233 proof(induction arbitrary: stk rule: big_step_induct)
235 show ?case by (fastforce simp:fun_upd_def cong: if_cong)
237 case (Seq c1 s1 s2 c2 s3)
238 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
239 have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
240 using Seq.IH(1) by fastforce
242 have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
243 using Seq.IH(2) by fastforce
244 ultimately show ?case by simp (blast intro: star_trans)
246 case (WhileTrue b s1 c s2 s3)
248 let ?cb = "bcomp b False (size ?cc + 1)"
249 let ?cw = "ccomp(WHILE b DO c)"
250 have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)"
251 using `bval b s1` by fastforce
253 have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
254 using WhileTrue.IH(1) by fastforce
256 have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
259 have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
260 ultimately show ?case by(blast intro: star_trans)