-
Notifications
You must be signed in to change notification settings - Fork 0
/
Compiler_Template.thy
213 lines (182 loc) · 8.67 KB
/
Compiler_Template.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
theory Compiler_Template
imports "HOL-IMP.Big_Step" "HOL-IMP.Star"
begin
declare [[coercion_enabled]]
declare [[coercion "int :: nat \<Rightarrow> int"]]
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))" |
"[] !! i = undefined"
lemma inth_append [simp]: "0 \<le> i \<Longrightarrow>
(xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
by (induct xs arbitrary: i) (auto simp: algebra_simps)
abbreviation (output)
"isize xs == int (length xs)"
notation isize ("size")
datatype instr =
LOADI int | LOAD vname |
ADD |
STORE vname |
JMP int | JMPLESS int | JMPGE int
type_synonym stack = "val list"
type_synonym config = "int \<times> state \<times> stack"
abbreviation "hd2 xs == hd (tl xs)"
abbreviation "tl2 xs == tl (tl xs)"
(* note: by using hd / tl functions rather than pattern matching, we limit
reliance on the structure of stk in the behavior of iexec, allowing us
to simplify preconditions on lemmas that don't rely on the structure of
the stack
*)
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
"iexec (LOADI n) (i, s, stk) = (i + 1, s, n # stk)" |
"iexec (LOAD x) (i, s, stk) = (i + 1, s, s x # stk)" |
"iexec ADD (i, s, stk) = (i + 1, s, (hd2 stk + hd stk) # tl2 stk)" |
"iexec (STORE x) (i, s, stk) = (i + 1, s(x := hd stk), tl stk)" |
"iexec (JMP n) (i, s, stk) = (i + 1 + n, s, stk)" |
"iexec (JMPLESS n) (i, s, stk) = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk)" |
"iexec (JMPGE n) (i, s, stk) = (if hd2 stk >= hd stk then i + 1 + n else i + 1, s, tl2 stk)"
definition exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) where
"P \<turnstile> c \<rightarrow> c' \<longleftrightarrow>
(\<exists>i s stk. c = (i, s, stk) \<and> c' = iexec (P !! i) (i, s, stk) \<and> 0 \<le> i \<and> i < size P)"
(* an introduction rule that expects the LHS config parameters to already be known *)
lemma exec1I [intro, code_pred_intro]:
"c' = iexec (P !! i) (i, s, stk) \<Longrightarrow>
0 \<le> i \<Longrightarrow> i < size P \<Longrightarrow>
P \<turnstile> (i, s, stk) \<rightarrow> c'"
by (simp add: exec1_def)
code_pred exec1 by (metis exec1_def)
abbreviation exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50) where
"exec P \<equiv> star (exec1 P)"
lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
(* proof by case analysis on instructions, and that each case changes the PC relative to its
initial value
*)
lemma iexec_shift [simp]:
"(n + i', s', stk') = iexec x (n + i, s, stk) \<longleftrightarrow>
(i', s', stk') = iexec x (i, s, stk)"
by (cases x, auto)
(* trivial: iexec (P !! i) depends only on first i elements of P, and 0 \<le> i < size P *)
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P @ P' \<turnstile> c \<rightarrow> c'"
by (auto simp add: exec1_def)
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P @ P' \<turnstile> c \<rightarrow>* c'"
by (induct rule: star.induct) (blast intro: star.step exec1_appendR)+
lemma exec1_appendL:
fixes i i' :: int
shows "P \<turnstile> (i, s, stk) \<rightarrow> (i', s', stk') \<Longrightarrow>
P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow> (size P' + i', s', stk')"
by (auto simp add: exec1_def)
lemma exec_appendL:
fixes i i' :: int
shows "P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk') \<Longrightarrow>
P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow>* (size P' + i', s', stk')"
by (induct rule: exec_induct) (blast intro: star.step exec1_appendL)+
(* specialize append lemmas to discuss execution through concrete instructions
while assuming the execution of preceding and following code.
*)
lemma exec_Cons_1 [intro]:
"P \<turnstile> (0, s, stk) \<rightarrow>* (j, t, stk') \<Longrightarrow>
instr # P \<turnstile> (1, s, stk) \<rightarrow>* (1 + j, t, stk')"
by (drule exec_appendL [where P'="[instr]"]) simp
(* as exec_appendL, with (i := i - size P'), precondition necessary to satisfy exec1 precondition *)
lemma exec_appendL_if [intro]:
fixes i i' j :: int
shows "size P' <= i \<Longrightarrow>
P \<turnstile> (i - size P', s, stk) \<rightarrow>* (j, s', stk') \<Longrightarrow>
i' = size P' + j \<Longrightarrow>
P' @ P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk')"
by (drule exec_appendL [where P'=P']) simp
lemma exec_append_trans[intro]:
fixes i' i'' j'' :: int
shows "P \<turnstile> (0, s, stk) \<rightarrow>* (i', s', stk') \<Longrightarrow>
size P \<le> i' \<Longrightarrow>
P' \<turnstile> (i' - size P, s', stk') \<rightarrow>* (i'', s'', stk'') \<Longrightarrow>
j'' = size P + i'' \<Longrightarrow>
P @ P' \<turnstile> (0, s, stk) \<rightarrow>* (j'', s'', stk'')"
by(metis star_trans [OF exec_appendR exec_appendL_if])
declare Let_def[simp]
subsection "Compilation"
fun acomp :: "aexp \<Rightarrow> instr list" where
"acomp (N n) = [LOADI n]" |
"acomp (V x) = [LOAD x]" |
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
lemma acomp_correct[intro]:
"acomp a \<turnstile> (0, s, stk) \<rightarrow>* (size(acomp a), s, aval a s # stk)"
by (induction a arbitrary: stk) fastforce+
(* f = True means that we intend to jump n spaces upon the expression evaluating to True, and
step to next instruction upon the expression evaluating to False
f = False means vice versa
Suppose f = True in bcomp (And b1 b2). Then we want b1 to jump to just past b2 on False,
(we know early that the And expression evaluates to False),
and to continue with b2 on True. Thus we let cb1 = bcomp b1 False (size cb2)
suppose f = False in bcomp (And b1 b2). Then we want b1 to jump to (size cb2 + n) on False
(we know early that the And expression evaluates to False),
and to continue with b2 on True.
*)
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
"bcomp (Bc v) f n = (if v = f then [JMP n] else [])" |
"bcomp (Not b) f n = bcomp b (\<not>f) n" |
"bcomp (And b1 b2) f n = (let
cb2 = bcomp b2 f n;
m = if f
then size cb2
else size cb2 + n;
cb1 = bcomp b1 False m in
cb1 @ cb2)" |
"bcomp (Less a1 a2) f n =
acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])"
lemma bcomp_correct[intro]:
fixes n :: int
shows
"0 \<le> n \<Longrightarrow>
bcomp b f n \<turnstile>
(0, s, stk) \<rightarrow>* (size (bcomp b f n) + (if f = bval b s then n else 0), s, stk)"
proof (induct b arbitrary: f n)
case Not
from Not(1) [where f="\<not>f"] Not(2) show ?case by fastforce
next
case (And b1 b2)
from And(1)
[of "if f then size (bcomp b2 f n) else size (bcomp b2 f n) + n" "False"]
And(2) [of n f] And(3)
show ?case by fastforce
qed fastforce+
fun ccomp :: "com \<Rightarrow> instr list" where
"ccomp SKIP = []" |
"ccomp (x ::= a) = acomp a @ [STORE x]" |
"ccomp (c\<^sub>1;; c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = (let
cc\<^sub>1 = ccomp c\<^sub>1;
cc\<^sub>2 = ccomp c\<^sub>2;
cb = bcomp b False (size cc\<^sub>1 + 1) in
cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
"ccomp (WHILE b DO c) = (let
cc = ccomp c;
cb = bcomp b False (size cc + 1) in
cb @ cc @ [JMP (-(size cb + size cc + 1))])"
lemma ccomp_bigstep:
"(c, s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c), t, stk)"
proof(induct arbitrary: stk rule: big_step_induct)
case (Assign x a s)
show ?case by (fastforce simp:fun_upd_def cong: if_cong)
next
case (Seq c1 s1 s2 c2 s3)
let ?cc1 = "ccomp c1" and ?cc2 = "ccomp c2"
have "?cc1 @ ?cc2 \<turnstile> (0, s1 ,stk) \<rightarrow>* (size ?cc1, s2, stk)"
using Seq(2) by fastforce
moreover
have "?cc1 @ ?cc2 \<turnstile> (size ?cc1, s2, stk) \<rightarrow>* (size (?cc1 @ ?cc2), s3, stk)"
using Seq(4) by fastforce
ultimately show ?case by simp (blast intro: star_trans)
next
case (WhileTrue b s1 c s2 s3)
let ?cc = "ccomp c"
let ?cb = "bcomp b False (size ?cc + 1)"
and ?cw = "ccomp (WHILE b DO c)"
have "?cw \<turnstile> (0, s1, stk) \<rightarrow>* (size ?cb, s1, stk)" using \<open>bval b s1\<close> by fastforce
moreover have "?cw \<turnstile> (size ?cb, s1, stk) \<rightarrow>* (size ?cb + size ?cc, s2, stk)"
using WhileTrue(3) by fastforce
moreover have "?cw \<turnstile> (size ?cb + size ?cc, s2, stk) \<rightarrow>* (0, s2, stk)" by fastforce
ultimately show ?case using WhileTrue(5) by(blast intro: star_trans)
qed fastforce+
end