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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad.
Require Import Errors RTL BTL BTLmatchRTL.
(** TODO: adapt stuff RTLpathLivegen *)
Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.
Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
match rl with
| nil => true
| r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
end.
Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
match or with None => true | Some r => Regset.mem r alive end.
Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) :=
match ros with inl r => Regset.mem r alive | inr s => true end.
(* NB: definition following [regmap_setres] in [RTL.step] semantics *)
Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t :=
match res with
| BR r => Regset.add r alive
| _ => alive
end.
Definition exit_checker {A} (btl: code) (alive: Regset.t) (s: node) (v: A): option A :=
SOME next <- btl!s IN
ASSERT Regset.subset next.(input_regs) alive IN
Some v.
Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool :=
match l with
| nil => true
| s :: l' => exit_checker btl alive s true &&& exit_list_checker btl alive l'
end.
Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit :=
match fin with
| Bgoto s =>
exit_checker btl alive s tt
| Breturn oreg =>
ASSERT reg_option_mem oreg alive IN Some tt
| Bcall _ ros args res s =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN
exit_checker btl (Regset.add res alive) s tt
| Btailcall _ ros args =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN Some tt
| Bbuiltin _ args res s =>
ASSERT list_mem (params_of_builtin_args args) alive IN
exit_checker btl (reg_builtin_res res alive) s tt
| Bjumptable arg tbl =>
ASSERT Regset.mem arg alive IN
ASSERT exit_list_checker btl alive tbl IN Some tt
end.
Definition is_none {A} (oa: option A): bool :=
match oa with
| Some _ => false
| None => true
end.
Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (Regset.t*option final) :=
match ib with
| Bseq ib1 ib2 =>
SOME res <- body_checker btl ib1 alive IN
ASSERT is_none (snd res) IN
body_checker btl ib2 (fst res)
| Bnop _ => Some (alive, None)
| Bop _ args dest _ =>
ASSERT list_mem args alive IN
Some (Regset.add dest alive, None)
| Bload _ _ _ args dest _ =>
ASSERT list_mem args alive IN
Some (Regset.add dest alive, None)
| Bstore _ _ args src _ =>
ASSERT Regset.mem src alive IN
ASSERT list_mem args alive IN
Some (alive, None)
| Bcond _ args (BF (Bgoto s) _) (Bnop None) _ =>
ASSERT list_mem args alive IN
exit_checker btl alive s (alive, None)
| BF fin _ => Some (alive, Some fin)
| _ => None
end.
Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option unit :=
SOME res <- body_checker btl ib alive IN
SOME fin <- snd res IN
final_inst_checker btl (fst res) fin.
Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool :=
match l with
| nil => true
| (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l'
end.
Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.
Proof.
destruct o; simpl; intuition.
- eauto.
- firstorder. try_simplify_someHyps.
Qed.
Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
Proof.
intros; rewrite lazy_and_Some_true; firstorder.
destruct x; auto.
Qed.
Lemma list_iblock_checker_correct btl l:
list_iblock_checker btl l = true -> forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt.
Proof.
intros CHECKER e H; induction l as [|(n & ibf) l]; intuition.
simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.
Definition liveness_checker (f: BTL.function): res unit :=
match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with
| true => OK tt
| false => Error (msg "BTL_Livecheck: liveness_checker failed")
end.
Lemma liveness_checker_correct f n ibf:
liveness_checker f = OK tt ->
f.(fn_code)!n = Some ibf ->
iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt.
Proof.
unfold liveness_checker.
destruct list_iblock_checker eqn:EQL; try congruence.
intros _ P. exploit list_iblock_checker_correct; eauto.
- eapply PTree.elements_correct; eauto.
- simpl; auto.
Qed.
Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
Inductive liveness_ok_fundef: fundef -> Prop :=
| liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f)
| liveness_ok_External ef: liveness_ok_fundef (External ef).
(** TODO: adapt stuff RTLpathLivegenproof *)
Local Notation ext alive := (fun r => Regset.In r alive).
Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
Proof.
destruct (Pos.eq_dec r1 r2).
- subst. intuition; eapply Regset.add_1; auto.
- intuition.
* right. eapply Regset.add_3; eauto.
* eapply Regset.add_2; auto.
Qed.
Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
forall r, (alive r) -> rs1#r = rs2#r.
Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
| eqlive_stackframes_intro ibf res f sp pc rs1 rs2
(LIVE: liveness_ok_function f)
(ENTRY: f.(fn_code)!pc = Some ibf)
(EQUIV: forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)):
eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2).
Inductive eqlive_states: state -> state -> Prop :=
| eqlive_states_intro
ibf st1 st2 f sp pc rs1 rs2 m
(STACKS: list_forall2 eqlive_stackframes st1 st2)
(LIVE: liveness_ok_function f)
(PATH: f.(fn_code)!pc = Some ibf)
(EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2):
eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m)
| eqlive_states_call st1 st2 f args m
(LIVE: liveness_ok_fundef f)
(STACKS: list_forall2 eqlive_stackframes st1 st2):
eqlive_states (Callstate st1 f args m) (Callstate st2 f args m)
| eqlive_states_return st1 st2 v m
(STACKS: list_forall2 eqlive_stackframes st1 st2):
eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).
(* continue to adapt stuff RTLpathLivegenproof *)
Section FSEM_SIMULATES_CFGSEM.
Variable prog: BTL.program.
Let ge := Genv.globalenv prog.
Hypothesis liveness_checker_correct: forall b f, Genv.find_funct_ptr ge b = Some (Internal f) -> liveness_ok_function f.
Lemma cfgsem2fsem_step_simu s1 s1' t s2
(STEP : step tid (Genv.globalenv prog) s1 t s1')
(STATES : eqlive_states s1 s2)
:exists s2' : state,
step tr_inputs (Genv.globalenv prog) s2 t s2' /\
eqlive_states s1' s2'.
Proof.
Admitted.
Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
Proof.
eapply forward_simulation_step with eqlive_states; simpl; eauto.
- destruct 1, f; intros; eexists; intuition eauto;
repeat econstructor; eauto.
- intros s1 s2 r STATES FINAL; destruct FINAL.
inv STATES; inv STACKS; constructor.
- intros. eapply cfgsem2fsem_step_simu; eauto.
Qed.
End FSEM_SIMULATES_CFGSEM.
|
