src/HOL/IMP/Compiler.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45200 1f1897ac7877
child 45322 654cc47f6115
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (* Author: Tobias Nipkow *)
     2 
     3 header "A Compiler for IMP"
     4 
     5 theory Compiler imports Big_Step 
     6 begin
     7 
     8 subsection "List setup"
     9 
    10 text {*
    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.
    14   
    15   Therefore, we define notation for size and indexing for lists 
    16   on @{typ int}:
    17 *}
    18 abbreviation "isize xs == int (length xs)" 
    19 
    20 primrec
    21   inth :: "'a list => int => 'a" (infixl "!!" 100) where
    22   inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
    23 
    24 text {*
    25   The only additional lemma we need is indexing over append:
    26 *}
    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)
    31 
    32 subsection "Instructions and Stack Machine"
    33 
    34 datatype instr = 
    35   LOADI int | 
    36   LOAD string | 
    37   ADD |
    38   STORE string |
    39   JMP int |
    40   JMPFLESS int |
    41   JMPFGE int
    42 
    43 type_synonym stack = "val list"
    44 type_synonym config = "int\<times>state\<times>stack"
    45 
    46 abbreviation "hd2 xs == hd(tl xs)"
    47 abbreviation "tl2 xs == tl(tl xs)"
    48 
    49 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
    50     ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
    51 where
    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)"
    59 
    60 code_pred iexec1 .
    61 
    62 declare iexec1.intros
    63 
    64 definition
    65   exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
    66 where
    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)"
    69 
    70 declare exec1_def [simp] 
    71 
    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'"
    75   using assms by simp
    76 
    77 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
    78 where
    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''"
    81 
    82 declare refl[intro] step[intro]
    83 
    84 lemmas exec_induct = exec.induct[split_format(complete)]
    85 
    86 code_pred exec by force
    87 
    88 values
    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)}"
    92 
    93 
    94 subsection{* Verification infrastructure *}
    95 
    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+
    98 
    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'"
   107 
   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)
   124 
   125 
   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. *}
   129 
   130 lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
   131   by auto
   132 
   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)+
   135 
   136 lemma iexec1_shiftI:
   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
   140 
   141 lemma iexec1_shiftD:
   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
   145 
   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)
   149   
   150 lemma exec1_appendL:
   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')"
   153   by simp
   154 
   155 lemma exec_appendL:
   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)+
   159 
   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.
   165 
   166 If we have just executed the first instruction of the program, drop it: *}
   167 
   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
   172 
   173 lemma exec_appendL_if[intro]:
   174  "isize P' <= i
   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
   178 
   179 text{* Split the execution of a compound program up into the excution of its
   180 parts: *}
   181 
   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>
   186  j'' = isize P + i''
   187  \<Longrightarrow>
   188  P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
   189   by(metis exec_trans[OF exec_appendR exec_appendL_if])
   190 
   191 
   192 declare Let_def[simp] 
   193 
   194 
   195 subsection "Compilation"
   196 
   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]"
   201 
   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+
   205 
   206 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
   207 "bcomp (Bc v) c n = (if v=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
   213   in cb1 @ cb2)" |
   214 "bcomp (Less a1 a2) c n =
   215  acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
   216 
   217 value
   218   "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
   219      False 3"
   220 
   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)
   226   case Not
   227   from Not(1)[where c="~c"] Not(2) show ?case by fastforce
   228 next
   229   case (And b1 b2)
   230   from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n" 
   231                  "False"] 
   232        And(2)[of n  "c"] And(3) 
   233   show ?case by fastforce
   234 qed fastforce+
   235 
   236 fun ccomp :: "com \<Rightarrow> instr list" where
   237 "ccomp SKIP = []" |
   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))])"
   246 
   247 
   248 value "ccomp
   249  (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
   250   ELSE ''v'' ::= V ''u'')"
   251 
   252 value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
   253 
   254 
   255 subsection "Preservation of semantics"
   256 
   257 lemma ccomp_bigstep:
   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)
   260   case (Assign x a s)
   261   show ?case by (fastforce simp:fun_upd_def cong: if_cong)
   262 next
   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
   267   moreover
   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)
   271 next
   272   case (WhileTrue b s1 c s2 s3)
   273   let ?cc = "ccomp c"
   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
   278   moreover
   279   have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
   280     by fastforce
   281   moreover
   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)
   284 qed fastforce+
   285 
   286 end