1 (* Author: Tobias Nipkow *)
3 header "A Compiler for IMP"
5 theory Compiler imports Big_Step
8 subsection "Instructions and Stack Machine"
11 LOADI int | LOAD string | ADD |
18 type_synonym stack = "int list"
19 type_synonym config = "nat\<times>state\<times>stack"
21 abbreviation "hd2 xs == hd(tl xs)"
22 abbreviation "tl2 xs == tl(tl xs)"
24 inductive exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
25 ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
28 "\<lbrakk> i < size P; P!i = LOADI n \<rbrakk> \<Longrightarrow>
29 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
30 "\<lbrakk> i < size P; P!i = LOAD x \<rbrakk> \<Longrightarrow>
31 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
32 "\<lbrakk> i < size P; P!i = ADD \<rbrakk> \<Longrightarrow>
33 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
34 "\<lbrakk> i < size P; P!i = STORE n \<rbrakk> \<Longrightarrow>
35 P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
36 "\<lbrakk> i < size P; P!i = JMPF n \<rbrakk> \<Longrightarrow>
37 P \<turnstile> (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
38 "\<lbrakk> i < size P; P!i = JMPB n; n \<le> i+1 \<rbrakk> \<Longrightarrow>
39 P \<turnstile> (i,s,stk) \<rightarrow> (i+1-n,s,stk)" |
40 "\<lbrakk> i < size P; P!i = JMPFLESS n \<rbrakk> \<Longrightarrow>
41 P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
42 "\<lbrakk> i < size P; P!i = JMPFGE n \<rbrakk> \<Longrightarrow>
43 P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
47 declare exec1.intros[intro]
49 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
51 refl: "P \<turnstile> c \<rightarrow>* c" |
52 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
54 declare exec.intros[intro]
56 lemmas exec_induct = exec.induct[split_format(complete)]
61 "{(i,map t [''x'',''y''],stk) | i t stk.
62 [LOAD ''y'', STORE ''x''] \<turnstile>
63 (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
66 subsection{* Verification infrastructure *}
68 lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
69 apply(induct rule: exec.induct)
73 lemma exec1_subst: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> c' = c'' \<Longrightarrow> P \<turnstile> c \<rightarrow> c''"
76 lemmas exec1_simps = exec1.intros[THEN exec1_subst]
78 text{* Below we need to argue about the execution of code that is embedded in
79 larger programs. For this purpose we show that execution is preserved by
80 appending code to the left or right of a program. *}
82 lemma exec1_appendR: assumes "P \<turnstile> c \<rightarrow> c'" shows "P@P' \<turnstile> c \<rightarrow> c'"
84 from assms show ?thesis
85 by cases (simp_all add: exec1_simps nth_append)
86 -- "All cases proved with the final simp-all"
89 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
90 apply(induct rule: exec.induct)
92 by (metis exec1_appendR exec.step)
95 assumes "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk')"
96 shows "P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
98 from assms show ?thesis
99 by cases (simp_all add: exec1_simps)
103 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
104 P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
105 apply(induct rule: exec_induct)
107 by (blast intro: exec1_appendL exec.step)
109 text{* Now we specialise the above lemmas to enable automatic proofs of
110 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
111 pieces of code that we already know how they execute (by induction), combined
112 by @{text "@"} and @{text "#"}. Backward jumps are not supported.
113 The details should be skipped on a first reading.
115 If the pc points beyond the first instruction or part of the program, drop it: *}
117 lemma exec_Cons_Suc[intro]:
118 "P \<turnstile> (i,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
119 instr#P \<turnstile> (Suc i,s,stk) \<rightarrow>* (Suc j,t,stk')"
120 apply(drule exec_appendL[where P'="[instr]"])
124 lemma exec_appendL_if[intro]:
126 \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
127 \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
128 apply(drule exec_appendL[where P'=P'])
132 text{* Split the execution of a compound program up into the excution of its
135 lemma exec_append_trans[intro]:
136 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
137 size P \<le> i' \<Longrightarrow>
138 P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
141 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
142 by(metis exec_trans[OF exec_appendR exec_appendL_if])
145 declare Let_def[simp] eval_nat_numeral[simp]
148 subsection "Compilation"
150 fun acomp :: "aexp \<Rightarrow> instr list" where
151 "acomp (N n) = [LOADI n]" |
152 "acomp (V x) = [LOAD x]" |
153 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
155 lemma acomp_correct[intro]:
156 "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
157 apply(induct a arbitrary: stk)
161 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> instr list" where
162 "bcomp (B bv) c n = (if bv=c then [JMPF n] else [])" |
163 "bcomp (Not b) c n = bcomp b (\<not>c) n" |
164 "bcomp (And b1 b2) c n =
165 (let cb2 = bcomp b2 c n;
166 m = (if c then size cb2 else size cb2+n);
167 cb1 = bcomp b1 False m
169 "bcomp (Less a1 a2) c n =
170 acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
173 "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
176 lemma bcomp_correct[intro]:
177 "bcomp b c n \<turnstile>
178 (0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
179 proof(induct b arbitrary: c n m)
181 from Not[of "~c"] show ?case by fastsimp
184 from And(1)[of "False"] And(2)[of "c"] show ?case by fastsimp
188 fun ccomp :: "com \<Rightarrow> instr list" where
190 "ccomp (x ::= a) = acomp a @ [STORE x]" |
191 "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
192 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
193 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
194 in cb @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" |
195 "ccomp (WHILE b DO c) =
196 (let cc = ccomp c; cb = bcomp b False (size cc + 1)
197 in cb @ cc @ [JMPB (size cb + size cc + 1)])"
200 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
201 ELSE ''v'' ::= V ''u'')"
203 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
206 subsection "Preservation of sematics"
209 "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
210 proof(induct arbitrary: stk rule: big_step_induct)
212 show ?case by (fastsimp simp:fun_upd_def)
214 case (Semi c1 s1 s2 c2 s3)
215 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
216 have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
217 using Semi.hyps(2) by (fastsimp)
219 have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
220 using Semi.hyps(4) by (fastsimp)
221 ultimately show ?case by simp (blast intro: exec_trans)
223 case (WhileTrue b s1 c s2 s3)
225 let ?cb = "bcomp b False (size ?cc + 1)"
226 let ?cw = "ccomp(WHILE b DO c)"
227 have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
228 using WhileTrue(1,3) by fastsimp
230 have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
233 have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue(5))
234 ultimately show ?case by(blast intro: exec_trans)