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
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
|
(** Refinement of BTL_SEtheory data-structures
in order to introduce (and prove correct) a lower-level specification of the simulation test.
Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing
- On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate].
- Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques,
on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct".
- Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement !
*)
Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL BTL OptionMonad BTL_SEtheory.
(** * ... *)
Record sis_ok ctx (sis: sistate): Prop := {
OK_PRE: (sis.(si_pre) ctx);
OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None
}.
Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
Local Hint Constructors sis_ok: core.
Lemma sem_sok ctx sis rs m:
sem_sistate ctx sis rs m -> sis_ok ctx sis.
Proof.
unfold sem_sistate;
econstructor;
intuition congruence.
Qed.
(* NB: refinement of (symbolic) internal state *)
Record ristate :=
{
(** [ris_smem] represents the current smem symbolic evaluations.
(we also recover the history of smem in ris_smem) *)
ris_smem: smem;
(** For the values in registers:
1) we store a list of sval evaluations
2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *)
ris_input_init: bool;
ris_ok_sval: list sval;
ris_sreg:> PTree.t sval
}.
Definition ris_sreg_get (ris: ristate) r: sval :=
match PTree.get r ris with
| None => if ris_input_init ris then Sinput r else Sundef
| Some sv => sv
end.
Coercion ris_sreg_get: ristate >-> Funclass.
Record ris_ok ctx (ris: ristate) : Prop := {
OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None;
OK_RREG: forall sv, List.In sv (ris_ok_sval ris) -> eval_sval ctx sv <> None
}.
Local Hint Resolve OK_RMEM OK_RREG: core.
Local Hint Constructors ris_ok: core.
Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris;
MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem);
REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r);
(* the below invariant allows to evaluate operations in the initial memory of the path instead of the current memory *)
VALID_PRESERV: forall m b ofs, eval_smem ctx sis.(si_smem) = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs
}.
Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core.
Local Hint Constructors ris_refines: core.
Record ris_simu ris1 ris2: Prop := {
SIMU_FAILS: forall sv, List.In sv ris2.(ris_ok_sval) -> List.In sv ris1.(ris_ok_sval);
SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
}.
Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core.
Local Hint Constructors ris_simu: core.
Local Hint Resolve sge_match: core.
Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2):
ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2.
Proof.
intros SIMU OK; econstructor; eauto.
- erewrite <- SIMU_MEM; eauto.
erewrite <- smem_eval_preserved; eauto.
- intros; erewrite <- eval_sval_preserved; eauto.
Qed.
Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2:
ris_simu ris1 ris2 ->
ris_refines (bctx1 ctx) ris1 sis1 ->
ris_refines (bctx2 ctx) ris2 sis2 ->
sistate_simu ctx sis1 sis2.
Proof.
intros RIS REF1 REF2 rs m SEM.
exploit sem_sok; eauto.
erewrite OK_EQUIV; eauto.
intros ROK1.
exploit ris_simu_ok_preserv; eauto.
intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto.
intros SOK2.
destruct SEM as (PRE & SMEM & SREG).
unfold sem_sistate; intuition eauto.
+ erewrite <- MEM_EQ, <- SIMU_MEM; eauto.
erewrite <- smem_eval_preserved; eauto.
erewrite MEM_EQ; eauto.
+ erewrite <- REG_EQ, <- SIMU_REG; eauto.
erewrite <- eval_sval_preserved; eauto.
erewrite REG_EQ; eauto.
Qed.
Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop :=
| RefSome rsv sv
(REF:eval_sval ctx rsv = eval_sval ctx sv)
:optrsv_refines ctx (Some rsv) (Some sv)
| RefNone: optrsv_refines ctx None None
.
Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop :=
| RefLeft rsv sv
(REF:eval_sval ctx rsv = eval_sval ctx sv)
:rsvident_refines ctx (inl rsv) (inl sv)
| RefRight id1 id2
(IDSIMU: id1 = id2)
:rsvident_refines ctx (inr id1) (inr id2)
.
Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop :=
eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args.
Inductive rfv_refines ctx: sfval -> sfval -> Prop :=
| RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
| RefCall sig rvos ros rargs args r pc
(SV:rsvident_refines ctx rvos ros)
(LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
:rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
| RefTailcall sig rvos ros rargs args
(SV:rsvident_refines ctx rvos ros)
(LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
:rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
| RefBuiltin ef lbra lba br pc
(BARGS: bargs_refines ctx lbra lba)
:rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
| RefJumptable rsv sv lpc
(VAL: eval_sval ctx rsv = eval_sval ctx sv)
:rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
| RefReturn orsv osv
(OPT:optrsv_refines ctx orsv osv)
:rfv_refines ctx (Sreturn orsv) (Sreturn osv)
.
Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.
Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core.
Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2:
rfv_simu rfv1 rfv2 ->
rfv_refines (bctx1 ctx) rfv1 sfv1 ->
rfv_refines (bctx2 ctx) rfv2 sfv2 ->
sfv_simu ctx sfv1 sfv2.
Proof.
unfold rfv_simu; intros X REF1 REF2. subst.
unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto.
- (* call svid *)
inv SV; inv SV0; econstructor; eauto.
rewrite <- REF, <- REF0; eauto.
- (* call args *)
rewrite <- LIST, <- LIST0; eauto.
- (* taillcall svid *)
inv SV; inv SV0; econstructor; eauto.
rewrite <- REF, <- REF0; eauto.
- (* tailcall args *)
rewrite <- LIST, <- LIST0; eauto.
- (* builtin args *)
unfold bargs_refines, bargs_simu in *.
rewrite <- BARGS, <- BARGS0; eauto.
- rewrite <- VAL, <- VAL0; eauto.
- (* return *)
inv OPT; inv OPT0; econstructor; eauto.
rewrite <- REF, <- REF0; eauto.
Qed.
(* refinement of (symbolic) state *)
Inductive rstate :=
| Rfinal (ris: ristate) (rfv: sfval)
| Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate)
| Rabort
.
Inductive rst_simu: rstate -> rstate -> Prop :=
| Rfinal_simu ris1 ris2 rfv1 rfv2
(RIS: ris_simu ris1 ris2)
(RFV: rfv_simu rfv1 rfv2)
: rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
| Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2
(IFSO: rst_simu rifso1 rifso2)
(IFNOT: rst_simu rifnot1 rifnot2)
: rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
| Rabort_simu: rst_simu Rabort Rabort
(* TODO: extension à voir dans un second temps !
| Rcond_skip cond rargs rifso1 rifnot1 rst:
rst_simu rifso1 rst ->
rst_simu rifnot1 rst ->
rst_simu (Rcond cond rargs rifso1 rifnot1) rst
*)
.
(* Comment prend on en compte le ris en cours d'execution ??? *)
Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
| Reffinal ris sis rfv sfv (*ok: Prop*)
(*OK: ris_ok ctx ris -> ok*)
(RIS: ris_refines ctx ris sis)
(RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
: rst_refines ctx (*ok*) (Rfinal ris rfv) (Sfinal sis sfv)
| Refcond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*)
(*OK1: ok2 -> ok1*)
(RCOND: (* ok2 -> *) seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm)
(REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx (*ok2*) rifso ifso)
(REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx (*ok2*) rifnot ifnot)
: rst_refines ctx (*ok1*) (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot)
| Refabort
: rst_refines ctx Rabort Sabort
.
Local Hint Resolve ris_simu_correct rvf_simu_correct: core.
Lemma rst_simu_correct rst1 rst2:
rst_simu rst1 rst2 ->
forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*),
rst_refines (*ok1*) (bctx1 ctx) rst1 st1 ->
rst_refines (*ok2*) (bctx2 ctx) rst2 st2 ->
(* ok1 -> ok2 -> *)
sstate_simu ctx st1 st2.
Proof.
induction 1; simpl; intros f1 f2 ctx st1 st2 REF1 REF2 sis1 svf1 SEM1;
inv REF1; inv REF2; simpl in *; inv SEM1; auto.
- (* final_simu *)
do 2 eexists; intuition; eauto.
exploit sem_sok; eauto.
erewrite OK_EQUIV; eauto.
intros ROK1.
exploit ris_simu_ok_preserv; eauto.
- (* cond_simu *)
destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence.
generalize RCOND0.
erewrite <- seval_condition_preserved, RCOND by eauto.
intros SCOND0; rewrite <- SCOND0 in RCOND0.
erewrite <- SCOND0.
destruct b; simpl.
* exploit IHrst_simu1; eauto.
* exploit IHrst_simu2; eauto.
Qed.
(** TODO: could be useful ?
Lemma seval_condition_valid_preserv ctx cond args sm b
(VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs)
:seval_condition ctx cond args sm = Some b ->
seval_condition ctx cond args Sinit = Some b.
Proof.
unfold seval_condition; autodestruct; simpl; try congruence.
intros EVAL_LIST.
autodestruct; try congruence.
intros MEM COND. rewrite <- COND.
eapply cond_valid_pointer_eq; intros.
exploit VALID_PRESERV; eauto.
Qed.
*)
|
