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
nipkow@43141
     1
(* Author: Tobias Nipkow *)
nipkow@43141
     2
nipkow@43141
     3
header "A Compiler for IMP"
nipkow@10343
     4
kleing@43438
     5
theory Compiler imports Big_Step 
nipkow@43141
     6
begin
kleing@12429
     7
kleing@43438
     8
subsection "List setup"
kleing@43438
     9
kleing@43438
    10
text {*
kleing@43438
    11
  We are going to define a small machine language where programs are
kleing@43438
    12
  lists of instructions. For nicer algebraic properties in our lemmas
kleing@43438
    13
  later, we prefer @{typ int} to @{term nat} as program counter.
kleing@43438
    14
  
kleing@43438
    15
  Therefore, we define notation for size and indexing for lists 
kleing@43438
    16
  on @{typ int}:
kleing@43438
    17
*}
kleing@43438
    18
abbreviation "isize xs == int (length xs)" 
kleing@43438
    19
kleing@43438
    20
primrec
kleing@43438
    21
  inth :: "'a list => int => 'a" (infixl "!!" 100) where
kleing@43438
    22
  inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
kleing@43438
    23
kleing@43438
    24
text {*
kleing@43438
    25
  The only additional lemma we need is indexing over append:
kleing@43438
    26
*}
kleing@43438
    27
lemma inth_append [simp]:
kleing@43438
    28
  "0 \<le> n \<Longrightarrow>
kleing@43438
    29
  (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))"
kleing@43438
    30
  by (induct xs arbitrary: n) (auto simp: algebra_simps)
kleing@43438
    31
nipkow@43141
    32
subsection "Instructions and Stack Machine"
nipkow@10342
    33
nipkow@43141
    34
datatype instr = 
kleing@43438
    35
  LOADI int | 
kleing@43438
    36
  LOAD string | 
kleing@43438
    37
  ADD |
nipkow@43141
    38
  STORE string |
kleing@43438
    39
  JMP int |
kleing@43438
    40
  JMPFLESS int |
kleing@43438
    41
  JMPFGE int
nipkow@10342
    42
kleing@43438
    43
type_synonym stack = "val list"
kleing@43438
    44
type_synonym config = "int\<times>state\<times>stack"
nipkow@43141
    45
nipkow@43141
    46
abbreviation "hd2 xs == hd(tl xs)"
nipkow@43141
    47
abbreviation "tl2 xs == tl(tl xs)"
nipkow@11275
    48
kleing@43438
    49
inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
kleing@44004
    50
    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
nipkow@43141
    51
where
kleing@43438
    52
"LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
kleing@43438
    53
"LOAD x  \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
kleing@43438
    54
"ADD     \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
kleing@43438
    55
"STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
kleing@43438
    56
"JMP n   \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
kleing@43438
    57
"JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
kleing@43438
    58
"JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
kleing@43438
    59
kleing@43438
    60
code_pred iexec1 .
kleing@43438
    61
kleing@43438
    62
declare iexec1.intros
kleing@43438
    63
kleing@44000
    64
definition
kleing@44004
    65
  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
kleing@44000
    66
where
kleing@43438
    67
  "P \<turnstile> c \<rightarrow> c' = 
kleing@44004
    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)"
kleing@44000
    69
kleing@44000
    70
declare exec1_def [simp] 
kleing@44000
    71
kleing@44000
    72
lemma exec1I [intro, code_pred_intro]:
kleing@44004
    73
  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" 
kleing@44004
    74
  shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
kleing@44004
    75
  using assms by simp
nipkow@43141
    76
nipkow@43141
    77
inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
nipkow@43141
    78
where
nipkow@43141
    79
refl: "P \<turnstile> c \<rightarrow>* c" |
nipkow@43141
    80
step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
nipkow@43141
    81
kleing@43438
    82
declare refl[intro] step[intro]
nipkow@43141
    83
nipkow@43141
    84
lemmas exec_induct = exec.induct[split_format(complete)]
nipkow@43141
    85
kleing@44000
    86
code_pred exec by force
nipkow@43141
    87
nipkow@43141
    88
values
nipkow@43141
    89
  "{(i,map t [''x'',''y''],stk) | i t stk.
nipkow@43141
    90
    [LOAD ''y'', STORE ''x''] \<turnstile>
kleing@44036
    91
    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
nipkow@43141
    92
nipkow@43141
    93
nipkow@43141
    94
subsection{* Verification infrastructure *}
nipkow@43141
    95
nipkow@43141
    96
lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
nipkow@44890
    97
  by (induct rule: exec.induct) fastforce+
kleing@43438
    98
kleing@43438
    99
inductive_cases iexec1_cases [elim!]:
kleing@43438
   100
  "LOADI n \<turnstile>i c \<rightarrow> c'" 
kleing@43438
   101
  "LOAD x  \<turnstile>i c \<rightarrow> c'"
kleing@43438
   102
  "ADD     \<turnstile>i c \<rightarrow> c'"
kleing@43438
   103
  "STORE n \<turnstile>i c \<rightarrow> c'" 
kleing@43438
   104
  "JMP n   \<turnstile>i c \<rightarrow> c'"
kleing@43438
   105
  "JMPFLESS n \<turnstile>i c \<rightarrow> c'"
kleing@43438
   106
  "JMPFGE n \<turnstile>i c \<rightarrow> c'"
nipkow@43141
   107
kleing@43438
   108
text {* Simplification rules for @{const iexec1}. *}
kleing@43438
   109
lemma iexec1_simps [simp]:
kleing@43438
   110
  "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))"
kleing@43438
   111
  "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))"
kleing@43438
   112
  "ADD \<turnstile>i c \<rightarrow> c' = 
kleing@43438
   113
  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
kleing@43438
   114
  "STORE x \<turnstile>i c \<rightarrow> c' = 
kleing@44036
   115
  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
kleing@43438
   116
  "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
kleing@43438
   117
   "JMPFLESS n \<turnstile>i c \<rightarrow> c' = 
kleing@43438
   118
  (\<exists>i s stk. c = (i, s, stk) \<and> 
kleing@43438
   119
             c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"  
kleing@43438
   120
  "JMPFGE n \<turnstile>i c \<rightarrow> c' = 
kleing@43438
   121
  (\<exists>i s stk. c = (i, s, stk) \<and> 
kleing@43438
   122
             c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
kleing@43438
   123
  by (auto split del: split_if intro!: iexec1.intros)
nipkow@43141
   124
nipkow@43141
   125
nipkow@43141
   126
text{* Below we need to argue about the execution of code that is embedded in
nipkow@43141
   127
larger programs. For this purpose we show that execution is preserved by
nipkow@43141
   128
appending code to the left or right of a program. *}
nipkow@43141
   129
kleing@43438
   130
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
kleing@43438
   131
  by auto
nipkow@11275
   132
nipkow@43141
   133
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
nipkow@44890
   134
  by (induct rule: exec.induct) (fastforce intro: exec1_appendR)+
kleing@43438
   135
kleing@43438
   136
lemma iexec1_shiftI:
kleing@43438
   137
  assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
kleing@43438
   138
  shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
kleing@43438
   139
  using assms by cases auto
nipkow@13095
   140
kleing@43438
   141
lemma iexec1_shiftD:
kleing@43438
   142
  assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
kleing@43438
   143
  shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
kleing@43438
   144
  using assms by cases auto
kleing@43438
   145
kleing@43438
   146
lemma iexec_shift [simp]: 
kleing@43438
   147
  "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))"
kleing@43438
   148
  by (blast intro: iexec1_shiftI dest: iexec1_shiftD)
kleing@43438
   149
  
nipkow@43141
   150
lemma exec1_appendL:
kleing@43438
   151
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
kleing@43438
   152
   P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
kleing@43438
   153
  by simp
nipkow@13095
   154
nipkow@43141
   155
lemma exec_appendL:
nipkow@43141
   156
 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
kleing@43438
   157
  P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
kleing@43438
   158
  by (induct rule: exec_induct) (blast intro!: exec1_appendL)+
nipkow@13095
   159
nipkow@43141
   160
text{* Now we specialise the above lemmas to enable automatic proofs of
nipkow@43141
   161
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
nipkow@43141
   162
pieces of code that we already know how they execute (by induction), combined
nipkow@43141
   163
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
nipkow@43141
   164
The details should be skipped on a first reading.
nipkow@13095
   165
kleing@43438
   166
If we have just executed the first instruction of the program, drop it: *}
nipkow@43141
   167
kleing@43438
   168
lemma exec_Cons_1 [intro]:
kleing@43438
   169
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
kleing@43438
   170
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
kleing@43438
   171
  by (drule exec_appendL[where P'="[instr]"]) simp
nipkow@13095
   172
nipkow@43141
   173
lemma exec_appendL_if[intro]:
kleing@43438
   174
 "isize P' <= i
kleing@43438
   175
  \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
kleing@43438
   176
  \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
kleing@43438
   177
  by (drule exec_appendL[where P'=P']) simp
nipkow@10342
   178
nipkow@43141
   179
text{* Split the execution of a compound program up into the excution of its
nipkow@43141
   180
parts: *}
nipkow@13095
   181
nipkow@43141
   182
lemma exec_append_trans[intro]:
nipkow@43141
   183
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
kleing@43438
   184
 isize P \<le> i' \<Longrightarrow>
kleing@43438
   185
 P' \<turnstile>  (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
kleing@43438
   186
 j'' = isize P + i''
nipkow@43141
   187
 \<Longrightarrow>
nipkow@43141
   188
 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
kleing@43438
   189
  by(metis exec_trans[OF exec_appendR exec_appendL_if])
nipkow@13095
   190
nipkow@43141
   191
kleing@43438
   192
declare Let_def[simp] 
nipkow@13095
   193
nipkow@13095
   194
nipkow@43141
   195
subsection "Compilation"
nipkow@13095
   196
nipkow@43141
   197
fun acomp :: "aexp \<Rightarrow> instr list" where
nipkow@43141
   198
"acomp (N n) = [LOADI n]" |
nipkow@43141
   199
"acomp (V x) = [LOAD x]" |
nipkow@43141
   200
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
nipkow@43141
   201
nipkow@43141
   202
lemma acomp_correct[intro]:
kleing@43438
   203
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
nipkow@44890
   204
  by (induct a arbitrary: stk) fastforce+
nipkow@10342
   205
kleing@43438
   206
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
nipkow@45200
   207
"bcomp (Bc v) c n = (if v=c then [JMP n] else [])" |
nipkow@43141
   208
"bcomp (Not b) c n = bcomp b (\<not>c) n" |
nipkow@43141
   209
"bcomp (And b1 b2) c n =
nipkow@43141
   210
 (let cb2 = bcomp b2 c n;
kleing@43438
   211
        m = (if c then isize cb2 else isize cb2+n);
nipkow@43141
   212
      cb1 = bcomp b1 False m
nipkow@43141
   213
  in cb1 @ cb2)" |
nipkow@43141
   214
"bcomp (Less a1 a2) c n =
nipkow@43141
   215
 acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
nipkow@43141
   216
nipkow@43141
   217
value
nipkow@43141
   218
  "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
nipkow@43141
   219
     False 3"
nipkow@43141
   220
nipkow@43141
   221
lemma bcomp_correct[intro]:
kleing@43438
   222
  "0 \<le> n \<Longrightarrow>
kleing@43438
   223
  bcomp b c n \<turnstile>
kleing@43438
   224
 (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
wenzelm@45129
   225
proof(induction b arbitrary: c n)
nipkow@43141
   226
  case Not
nipkow@44890
   227
  from Not(1)[where c="~c"] Not(2) show ?case by fastforce
nipkow@13095
   228
next
nipkow@43141
   229
  case (And b1 b2)
kleing@43438
   230
  from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n" 
kleing@43438
   231
                 "False"] 
kleing@43438
   232
       And(2)[of n  "c"] And(3) 
nipkow@44890
   233
  show ?case by fastforce
nipkow@44890
   234
qed fastforce+
nipkow@43141
   235
nipkow@43141
   236
fun ccomp :: "com \<Rightarrow> instr list" where
nipkow@43141
   237
"ccomp SKIP = []" |
nipkow@43141
   238
"ccomp (x ::= a) = acomp a @ [STORE x]" |
nipkow@43141
   239
"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
nipkow@43141
   240
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
kleing@43438
   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)
kleing@43438
   242
   in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
nipkow@43141
   243
"ccomp (WHILE b DO c) =
kleing@43438
   244
 (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
kleing@44004
   245
  in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
kleing@44004
   246
nipkow@43141
   247
nipkow@43141
   248
value "ccomp
nipkow@43141
   249
 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
nipkow@43141
   250
  ELSE ''v'' ::= V ''u'')"
nipkow@43141
   251
nipkow@43141
   252
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
nipkow@43141
   253
nipkow@43141
   254
Jean@45114
   255
subsection "Preservation of semantics"
nipkow@43141
   256
kleing@43438
   257
lemma ccomp_bigstep:
kleing@43438
   258
  "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
nipkow@45015
   259
proof(induction arbitrary: stk rule: big_step_induct)
nipkow@43141
   260
  case (Assign x a s)
nipkow@44890
   261
  show ?case by (fastforce simp:fun_upd_def cong: if_cong)
nipkow@13095
   262
next
nipkow@43141
   263
  case (Semi c1 s1 s2 c2 s3)
nipkow@43141
   264
  let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
kleing@43438
   265
  have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
nipkow@45015
   266
    using Semi.IH(1) by fastforce
nipkow@43141
   267
  moreover
kleing@43438
   268
  have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
nipkow@45015
   269
    using Semi.IH(2) by fastforce
nipkow@43141
   270
  ultimately show ?case by simp (blast intro: exec_trans)
nipkow@43141
   271
next
nipkow@43141
   272
  case (WhileTrue b s1 c s2 s3)
nipkow@43141
   273
  let ?cc = "ccomp c"
kleing@43438
   274
  let ?cb = "bcomp b False (isize ?cc + 1)"
nipkow@43141
   275
  let ?cw = "ccomp(WHILE b DO c)"
kleing@43438
   276
  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
nipkow@45015
   277
    using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
nipkow@43141
   278
  moreover
kleing@43438
   279
  have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
nipkow@44890
   280
    by fastforce
nipkow@43141
   281
  moreover
nipkow@45015
   282
  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
nipkow@43141
   283
  ultimately show ?case by(blast intro: exec_trans)
nipkow@44890
   284
qed fastforce+
nipkow@13095
   285
webertj@20217
   286
end