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
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
|
(** Syntax and Sequential Semantics of Abstract Basic Blocks.
*)
Module Type PseudoRegisters.
Parameter t: Type.
Parameter eq_dec: forall (x y: t), { x = y } + { x<>y }.
End PseudoRegisters.
(** * Parameters of the language of Basic Blocks *)
Module Type LangParam.
Declare Module R: PseudoRegisters.
Parameter value: Type.
(** Declare the type of operations *)
Parameter op: Type. (* type of operations *)
Parameter genv: Type. (* environment to be used for evaluating an op *)
(* NB: possible generalization
- relation after/before.
*)
Parameter op_eval: genv -> op -> list value -> option value.
Parameter is_constant: op -> bool.
Parameter is_constant_correct:
forall ge o, is_constant o = true -> op_eval ge o nil <> None.
End LangParam.
(** * Syntax and (sequential) semantics of "basic blocks" *)
Module MkSeqLanguage(P: LangParam).
Export P.
Local Open Scope list.
Section SEQLANG.
Variable ge: genv.
Definition mem := R.t -> value.
Definition assign (m: mem) (x:R.t) (v: value): mem
:= fun y => if R.eq_dec x y then v else m y.
Inductive exp :=
| PReg (x:R.t)
| Op (o:op) (le: list_exp)
| Old (e: exp)
with list_exp :=
| Enil
| Econs (e:exp) (le:list_exp)
| LOld (le: list_exp)
.
Fixpoint exp_eval (e: exp) (m old: mem): option value :=
match e with
| PReg x => Some (m x)
| Op o le =>
match list_exp_eval le m old with
| Some lv => op_eval ge o lv
| _ => None
end
| Old e => exp_eval e old old
end
with list_exp_eval (le: list_exp) (m old: mem): option (list value) :=
match le with
| Enil => Some nil
| Econs e le' =>
match exp_eval e m old, list_exp_eval le' m old with
| Some v, Some lv => Some (v::lv)
| _, _ => None
end
| LOld le => list_exp_eval le old old
end.
Definition inst := list (R.t * exp). (* = a sequence of assignments *)
Fixpoint inst_run (i: inst) (m old: mem): option mem :=
match i with
| nil => Some m
| (x, e)::i' =>
match exp_eval e m old with
| Some v' => inst_run i' (assign m x v') old
| None => None
end
end.
Definition bblock := list inst.
Fixpoint run (p: bblock) (m: mem): option mem :=
match p with
| nil => Some m
| i::p' =>
match inst_run i m m with
| Some m' => run p' m'
| None => None
end
end.
(* A few useful lemma *)
Lemma assign_eq m x v:
(assign m x v) x = v.
Proof.
unfold assign. destruct (R.eq_dec x x); try congruence.
Qed.
Lemma assign_diff m x y v:
x<>y -> (assign m x v) y = m y.
Proof.
unfold assign. destruct (R.eq_dec x y); try congruence.
Qed.
Lemma assign_skips m x y:
(assign m x (m x)) y = m y.
Proof.
unfold assign. destruct (R.eq_dec x y); try congruence.
Qed.
Lemma assign_swap m x1 v1 x2 v2 y:
x1 <> x2 -> (assign (assign m x1 v1) x2 v2) y = (assign (assign m x2 v2) x1 v1) y.
Proof.
intros; destruct (R.eq_dec x2 y).
- subst. rewrite assign_eq, assign_diff; auto. rewrite assign_eq; auto.
- rewrite assign_diff; auto.
destruct (R.eq_dec x1 y).
+ subst; rewrite! assign_eq. auto.
+ rewrite! assign_diff; auto.
Qed.
(** A small theory of bblock equality *)
(* equalities on bblock outputs *)
Definition res_eq (om1 om2: option mem): Prop :=
match om1 with
| Some m1 => exists m2, om2 = Some m2 /\ forall x, m1 x = m2 x
| None => om2 = None
end.
Scheme exp_mut := Induction for exp Sort Prop
with list_exp_mut := Induction for list_exp Sort Prop.
Lemma exp_equiv e old1 old2:
(forall x, old1 x = old2 x) ->
forall m1 m2, (forall x, m1 x = m2 x) ->
(exp_eval e m1 old1) = (exp_eval e m2 old2).
Proof.
intros H1.
induction e using exp_mut with (P0:=fun l => forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); simpl; try congruence; auto.
- intros; erewrite IHe; eauto.
- intros; erewrite IHe, IHe0; auto.
Qed.
Definition bblock_simu (p1 p2: bblock): Prop
:= forall m, (run p1 m) <> None -> res_eq (run p1 m) (run p2 m).
Lemma inst_equiv_refl i old1 old2:
(forall x, old1 x = old2 x) ->
forall m1 m2, (forall x, m1 x = m2 x) ->
res_eq (inst_run i m1 old1) (inst_run i m2 old2).
Proof.
intro H; induction i as [ | [x e]]; simpl; eauto.
intros m1 m2 H1. erewrite exp_equiv; eauto.
destruct (exp_eval e m2 old2); simpl; auto.
apply IHi.
unfold assign; intro y. destruct (R.eq_dec x y); auto.
Qed.
Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2).
Proof.
induction p as [ | i p']; simpl; eauto.
intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto.
intros X; lapply (X m1 m2); auto; clear X.
destruct (inst_run i m1 m1); simpl.
- intros [m3 [H1 H2]]; rewrite H1; simpl; auto.
- intros H1; rewrite H1; simpl; auto.
Qed.
Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1.
Proof.
destruct om1; simpl.
- intros [m2 [H1 H2]]; subst; simpl. eauto.
- intros; subst; simpl; eauto.
Qed.
Lemma res_eq_trans (om1 om2 om3: option mem):
(res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3).
Proof.
destruct om1; simpl.
- intros [m2 [H1 H2]]; subst; simpl.
intros [m3 [H3 H4]]; subst; simpl.
eapply ex_intro; intuition eauto. rewrite H2; auto.
- intro; subst; simpl; auto.
Qed.
Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)).
Proof.
unfold bblock_simu; intuition.
intros; eapply res_eq_trans. eauto.
eapply bblock_equiv_refl; eauto.
Qed.
Lemma run_app p1: forall m1 p2,
run (p1++p2) m1 =
match run p1 m1 with
| Some m2 => run p2 m2
| None => None
end.
Proof.
induction p1; simpl; try congruence.
intros; destruct (inst_run _ _ _); simpl; auto.
Qed.
Lemma run_app_None p1 m1 p2:
run p1 m1 = None ->
run (p1++p2) m1 = None.
Proof.
intro H; rewrite run_app. rewrite H; auto.
Qed.
Lemma run_app_Some p1 m1 m2 p2:
run p1 m1 = Some m2 ->
run (p1++p2) m1 = run p2 m2.
Proof.
intros H; rewrite run_app. rewrite H; auto.
Qed.
End SEQLANG.
End MkSeqLanguage.
Module Type SeqLanguage.
Declare Module LP: LangParam.
Include MkSeqLanguage LP.
End SeqLanguage.
|
