nipkow@43982: (* Author: Tobias Nipkow *)
nipkow@10343: 
nipkow@43982: header "A Compiler for IMP"
nipkow@10342: 
kleing@44296: theory Compiler imports Big_Step 
nipkow@43982: begin
kleing@12429: 
kleing@44296: subsection "List setup"
kleing@44296: 
kleing@44296: text {*
kleing@44296:   We are going to define a small machine language where programs are
kleing@44296:   lists of instructions. For nicer algebraic properties in our lemmas
kleing@44296:   later, we prefer @{typ int} to @{term nat} as program counter.
kleing@44296:   
kleing@44296:   Therefore, we define notation for size and indexing for lists 
kleing@44296:   on @{typ int}:
kleing@44296: *}
kleing@44296: abbreviation "isize xs == int (length xs)" 
kleing@44296: 
kleing@44296: primrec
kleing@44296:   inth :: "'a list => int => 'a" (infixl "!!" 100) where
kleing@44296:   inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
kleing@44296: 
kleing@44296: text {*
kleing@44296:   The only additional lemma we need is indexing over append:
kleing@44296: *}
kleing@44296: lemma inth_append [simp]:
kleing@44296:   "0 \<le> n \<Longrightarrow>
kleing@44296:   (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))"
kleing@44296:   by (induct xs arbitrary: n) (auto simp: algebra_simps)
kleing@44296: 
nipkow@43982: subsection "Instructions and Stack Machine"
nipkow@43982: 
nipkow@43982: datatype instr = 
kleing@44296:   LOADI int | 
kleing@44296:   LOAD string | 
kleing@44296:   ADD |
nipkow@43982:   STORE string |
kleing@44296:   JMP int |
kleing@44296:   JMPFLESS int |
kleing@44296:   JMPFGE int
nipkow@43982: 
kleing@44296: (* reads slightly nicer *)
kleing@44296: abbreviation
kleing@44296:   "JMPB i == JMP (-i)"
kleing@44296: 
kleing@44296: type_synonym stack = "val list"
kleing@44296: type_synonym config = "int\<times>state\<times>stack"
nipkow@43982: 
nipkow@43982: abbreviation "hd2 xs == hd(tl xs)"
nipkow@43982: abbreviation "tl2 xs == tl(tl xs)"
nipkow@43982: 
kleing@44296: inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
kleing@44296:     ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50)
wenzelm@27362: where
kleing@44296: "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
kleing@44296: "LOAD x  \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
kleing@44296: "ADD     \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
kleing@44296: "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
kleing@44296: "JMP n   \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
kleing@44296: "JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
kleing@44296: "JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
kleing@44296: 
kleing@44296: code_pred iexec1 .
kleing@44296: 
kleing@44296: declare iexec1.intros
kleing@44296: 
kleing@44871: definition
kleing@44871:   exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) 
kleing@44871: where
kleing@44296:   "P \<turnstile> c \<rightarrow> c' = 
kleing@44296:    (\<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)"
kleing@44871: 
kleing@44871: declare exec1_def [simp] 
kleing@44871: 
kleing@44871: lemma exec1I [intro, code_pred_intro]:
kleing@44871:   "\<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'"
kleing@44871:   by simp
nipkow@43982: 
nipkow@43982: inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
nipkow@43982: where
nipkow@43982: refl: "P \<turnstile> c \<rightarrow>* c" |
nipkow@43982: step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
nipkow@43982: 
kleing@44296: declare refl[intro] step[intro]
nipkow@43982: 
nipkow@43982: lemmas exec_induct = exec.induct[split_format(complete)]
nipkow@43982: 
kleing@44871: code_pred exec by force
nipkow@43982: 
nipkow@43982: values
nipkow@43982:   "{(i,map t [''x'',''y''],stk) | i t stk.
nipkow@43982:     [LOAD ''y'', STORE ''x''] \<turnstile>
kleing@43999:     (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
nipkow@43982: 
nipkow@43982: 
nipkow@43982: subsection{* Verification infrastructure *}
nipkow@43982: 
nipkow@43982: lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
kleing@44296:   by (induct rule: exec.induct) fastsimp+
nipkow@43982: 
kleing@44296: inductive_cases iexec1_cases [elim!]:
kleing@44296:   "LOADI n \<turnstile>i c \<rightarrow> c'" 
kleing@44296:   "LOAD x  \<turnstile>i c \<rightarrow> c'"
kleing@44296:   "ADD     \<turnstile>i c \<rightarrow> c'"
kleing@44296:   "STORE n \<turnstile>i c \<rightarrow> c'" 
kleing@44296:   "JMP n   \<turnstile>i c \<rightarrow> c'"
kleing@44296:   "JMPFLESS n \<turnstile>i c \<rightarrow> c'"
kleing@44296:   "JMPFGE n \<turnstile>i c \<rightarrow> c'"
nipkow@43982: 
kleing@44296: text {* Simplification rules for @{const iexec1}. *}
kleing@44296: lemma iexec1_simps [simp]:
kleing@44296:   "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))"
kleing@44296:   "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))"
kleing@44296:   "ADD \<turnstile>i c \<rightarrow> c' = 
kleing@44296:   (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
kleing@44296:   "STORE x \<turnstile>i c \<rightarrow> c' = 
kleing@44296:   (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))"
kleing@44296:   "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
kleing@44296:    "JMPFLESS n \<turnstile>i c \<rightarrow> c' = 
kleing@44296:   (\<exists>i s stk. c = (i, s, stk) \<and> 
kleing@44296:              c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"  
kleing@44296:   "JMPFGE n \<turnstile>i c \<rightarrow> c' = 
kleing@44296:   (\<exists>i s stk. c = (i, s, stk) \<and> 
kleing@44296:              c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
kleing@44296:   by (auto split del: split_if intro!: iexec1.intros)
kleing@44296: 
nipkow@43982: 
nipkow@43982: text{* Below we need to argue about the execution of code that is embedded in
nipkow@43982: larger programs. For this purpose we show that execution is preserved by
nipkow@43982: appending code to the left or right of a program. *}
nipkow@43982: 
kleing@44296: lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
kleing@44296:   by auto
nipkow@11275: 
nipkow@43982: lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
kleing@44296:   by (induct rule: exec.induct) (fastsimp intro: exec1_appendR)+
nipkow@13095: 
kleing@44296: lemma iexec1_shiftI:
kleing@44296:   assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
kleing@44296:   shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
kleing@44296:   using assms by cases auto
kleing@44296: 
kleing@44296: lemma iexec1_shiftD:
kleing@44296:   assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
kleing@44296:   shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
kleing@44296:   using assms by cases auto
kleing@44296: 
kleing@44296: lemma iexec_shift [simp]: 
kleing@44296:   "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))"
kleing@44296:   by (blast intro: iexec1_shiftI dest: iexec1_shiftD)
kleing@44296:   
nipkow@43982: lemma exec1_appendL:
kleing@44296:   "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
kleing@44296:    P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
kleing@44296:   by simp
nipkow@13095: 
nipkow@43982: lemma exec_appendL:
nipkow@43982:  "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
kleing@44296:   P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
kleing@44296:   by (induct rule: exec_induct) (blast intro!: exec1_appendL)+
nipkow@43982: 
nipkow@43982: text{* Now we specialise the above lemmas to enable automatic proofs of
nipkow@43982: @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
nipkow@43982: pieces of code that we already know how they execute (by induction), combined
nipkow@43982: by @{text "@"} and @{text "#"}. Backward jumps are not supported.
nipkow@43982: The details should be skipped on a first reading.
nipkow@43982: 
kleing@44296: If we have just executed the first instruction of the program, drop it: *}
nipkow@43982: 
kleing@44296: lemma exec_Cons_1 [intro]:
kleing@44296:   "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
kleing@44296:   instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
kleing@44296:   by (drule exec_appendL[where P'="[instr]"]) simp
nipkow@10342: 
nipkow@43982: lemma exec_appendL_if[intro]:
kleing@44296:  "isize P' <= i
kleing@44296:   \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
kleing@44296:   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
kleing@44296:   by (drule exec_appendL[where P'=P']) simp
nipkow@13095: 
nipkow@43982: text{* Split the execution of a compound program up into the excution of its
nipkow@43982: parts: *}
nipkow@13095: 
nipkow@43982: lemma exec_append_trans[intro]:
nipkow@43982: "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
kleing@44296:  isize P \<le> i' \<Longrightarrow>
kleing@44296:  P' \<turnstile>  (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
kleing@44296:  j'' = isize P + i''
nipkow@43982:  \<Longrightarrow>
nipkow@43982:  P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
kleing@44296:   by(metis exec_trans[OF exec_appendR exec_appendL_if])
nipkow@13095: 
nipkow@43982: 
kleing@44296: declare Let_def[simp] 
nipkow@43982: 
nipkow@43982: 
nipkow@43982: subsection "Compilation"
nipkow@43982: 
nipkow@43982: fun acomp :: "aexp \<Rightarrow> instr list" where
nipkow@43982: "acomp (N n) = [LOADI n]" |
nipkow@43982: "acomp (V x) = [LOAD x]" |
nipkow@43982: "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
nipkow@43982: 
nipkow@43982: lemma acomp_correct[intro]:
kleing@44296:   "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
kleing@44296:   by (induct a arbitrary: stk) fastsimp+
nipkow@13095: 
kleing@44296: fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
kleing@44296: "bcomp (B bv) c n = (if bv=c then [JMP n] else [])" |
nipkow@43982: "bcomp (Not b) c n = bcomp b (\<not>c) n" |
nipkow@43982: "bcomp (And b1 b2) c n =
nipkow@43982:  (let cb2 = bcomp b2 c n;
kleing@44296:         m = (if c then isize cb2 else isize cb2+n);
nipkow@43982:       cb1 = bcomp b1 False m
nipkow@43982:   in cb1 @ cb2)" |
nipkow@43982: "bcomp (Less a1 a2) c n =
nipkow@43982:  acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
nipkow@43982: 
nipkow@43982: value
nipkow@43982:   "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
nipkow@43982:      False 3"
nipkow@43982: 
nipkow@43982: lemma bcomp_correct[intro]:
kleing@44296:   "0 \<le> n \<Longrightarrow>
kleing@44296:   bcomp b c n \<turnstile>
kleing@44296:  (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
nipkow@43982: proof(induct b arbitrary: c n m)
nipkow@43982:   case Not
kleing@44296:   from Not(1)[where c="~c"] Not(2) show ?case by fastsimp
nipkow@13095: next
nipkow@43982:   case (And b1 b2)
kleing@44296:   from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n" 
kleing@44296:                  "False"] 
kleing@44296:        And(2)[of n  "c"] And(3) 
kleing@44296:   show ?case by fastsimp
nipkow@43982: qed fastsimp+
nipkow@13095: 
nipkow@43982: fun ccomp :: "com \<Rightarrow> instr list" where
nipkow@43982: "ccomp SKIP = []" |
nipkow@43982: "ccomp (x ::= a) = acomp a @ [STORE x]" |
nipkow@43982: "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
nipkow@43982: "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
kleing@44296:   (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1)
kleing@44296:    in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
nipkow@43982: "ccomp (WHILE b DO c) =
kleing@44296:  (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
kleing@44296:   in cb @ cc @ [JMPB (isize cb + isize cc + 1)])"
nipkow@13095: 
nipkow@43982: value "ccomp
nipkow@43982:  (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
nipkow@43982:   ELSE ''v'' ::= V ''u'')"
nipkow@13095: 
nipkow@43982: value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
nipkow@13095: 
nipkow@13095: 
nipkow@43982: subsection "Preservation of sematics"
nipkow@43982: 
kleing@44296: lemma ccomp_bigstep:
kleing@44296:   "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
nipkow@43982: proof(induct arbitrary: stk rule: big_step_induct)
nipkow@43982:   case (Assign x a s)
kleing@44296:   show ?case by (fastsimp simp:fun_upd_def cong: if_cong)
nipkow@13095: next
nipkow@43982:   case (Semi c1 s1 s2 c2 s3)
nipkow@43982:   let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
kleing@44296:   have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
kleing@44296:     using Semi.hyps(2) by fastsimp
nipkow@43982:   moreover
kleing@44296:   have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
kleing@44296:     using Semi.hyps(4) by fastsimp
nipkow@43982:   ultimately show ?case by simp (blast intro: exec_trans)
nipkow@13095: next
nipkow@43982:   case (WhileTrue b s1 c s2 s3)
nipkow@43982:   let ?cc = "ccomp c"
kleing@44296:   let ?cb = "bcomp b False (isize ?cc + 1)"
nipkow@43982:   let ?cw = "ccomp(WHILE b DO c)"
kleing@44296:   have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
nipkow@43982:     using WhileTrue(1,3) by fastsimp
nipkow@43982:   moreover
kleing@44296:   have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
kleing@44296:     by fastsimp
nipkow@43982:   moreover
kleing@44296:   have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
nipkow@43982:   ultimately show ?case by(blast intro: exec_trans)
nipkow@43982: qed fastsimp+
nipkow@13095: 
webertj@20217: end