blob: a3be20b5b56b41df748523dce0fc1345cc068506 (
plain)
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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.
Require Import Errors Linking BTLtoRTL.
(*****************************)
(* Put this in an other file *)
Require Import Linking.
Lemma transf_function_correct f f':
transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
Proof.
unfold transf_function; unfold bind. repeat autodestruct.
intros H _ _ X. inversion X; subst; clear X.
eexists; eapply verify_function_correct; simpl; eauto.
Qed.
Lemma transf_fundef_correct f f':
transf_fundef f = OK f' -> match_fundef f f'.
Proof.
intros TRANSF; destruct f; simpl; monadInv TRANSF.
+ exploit transf_function_correct; eauto.
intros (dupmap & MATCH_F).
eapply match_Internal; eauto.
+ eapply match_External.
Qed.
Definition match_prog (p: program) (tp: RTL.program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
intros. eapply match_transform_partial_program_contextual; eauto.
Qed.
Section RTL_SIMULATES_BTL.
Variable prog: program.
Variable tprog: RTL.program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.
Lemma senv_preserved: Senv.equiv ge tge.
Proof.
eapply (Genv.senv_match TRANSL).
Qed.
Lemma functions_translated (v: val) (f: fundef):
Genv.find_funct ge v = Some f ->
exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
Proof.
intros. exploit (Genv.find_funct_match TRANSL); eauto.
intros (cu & tf & A & B & C).
repeat eexists; intuition eauto.
+ unfold incl; auto.
+ eapply linkorder_refl.
Qed.
Lemma function_ptr_translated v f:
Genv.find_funct_ptr ge v = Some f ->
exists tf,
Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof.
intros.
exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.
Lemma function_sig_translated f tf: transf_fundef f = OK tf -> RTL.funsig tf = funsig f.
Proof.
intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
erewrite preserv_fnsig; eauto.
Qed.
Lemma transf_initial_states s1:
initial_state prog s1 ->
exists s2, RTL.initial_state tprog s2 /\ match_states s1 s2.
Proof.
intros. inv H.
exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
eexists. split.
- econstructor; eauto.
+ eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+ replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
symmetry. eapply match_program_main. eauto.
+ erewrite function_sig_translated; eauto.
- constructor; eauto.
constructor.
apply transf_fundef_correct; auto.
Qed.
Lemma transf_final_states s1 s2 r:
match_states s1 s2 -> final_state s1 r -> RTL.final_state s2 r.
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
Qed.
Theorem plus_simulation s1 t s1':
step ge s1 t s1' ->
forall s2 (MS: match_states s1 s2),
exists s2',
plus RTL.step tge s2 t s2'
/\ match_states s1' s2'.
Proof.
induction 1; intros; inv MS.
- eapply dupmap_correct in DUPLIC; eauto.
destruct DUPLIC as (ib' & FNC & MIB).
inv H0. destruct H1 as (m' & fin & IBIS & FS).
admit.
(* Définir une relation inductive qui provient du MS,
et qui relie le iblock_istep avec le RTL. Il faut prendre en compte
le "isfst" pour savoir si on doit avoir du "stuttering" côté RTL. *)
(* exec_function_internal *)
- inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
+ eapply plus_one. apply RTL.exec_function_internal.
erewrite <- preserv_fnstacksize; eauto.
+ erewrite <- preserv_fnparams; eauto.
eapply match_states_intro; eauto.
apply dupmap_entrypoint. assumption.
(* exec_function_external *)
- inversion TRANSF as [|]; subst. eexists. split.
+ eapply plus_one. econstructor.
eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+ constructor. assumption.
(* exec_return *)
- inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
+ eapply plus_one. constructor.
+ inv H1. econstructor; eauto.
Admitted. (* TODO: première étape *)
Theorem transf_program_correct:
forward_simulation (semantics prog) (RTL.semantics tprog).
Proof.
eapply forward_simulation_plus with match_states.
- eapply senv_preserved.
- eapply transf_initial_states.
- eapply transf_final_states.
- eapply plus_simulation.
Qed.
End RTL_SIMULATES_BTL.
|
