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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* TODO: Proper author information *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Correctness proof for the branch tunneling optimization for RTL. *)
(* This is a port of Tunnelingproof.v, the same optimisation for LTL. *)
Require Import Coqlib Maps Errors.
Require Import AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations RTL.
Require Import RTLTunneling.
Require Import Conventions1.
Local Open Scope nat.
(** Preservation of semantics *)
Definition match_prog (p tp: program) :=
match_program (fun _ f tf => tunnel_fundef f = OK tf) eq p tp.
(* rq: `(fun _ ...)` est la fonction pour matcher des fonctions
* `eq` la fonction pour matcher les variables ? (`varinfo` dans la def)
* `p` et `tp` sont les programmes donc on doit dire s'ils match
*)
Section PRESERVATION.
Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog. (* rq: on suppose que les programmes match *)
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
(* rq: pour les deux lemmes suivants, j'ai recopié les preuves, mais je ne les comprends pas du tout... D'où vient `exploit` ?? *)
Lemma functions_translated:
forall (v: val) (f: fundef),
Genv.find_funct ge v = Some f ->
exists tf, tunnel_fundef f = OK tf /\ Genv.find_funct tge v = Some tf.
Proof.
intros. exploit (Genv.find_funct_match TRANSL). eauto.
intros (cu & tf & A & B & C).
repeat eexists; intuition eauto.
Qed.
Lemma function_ptr_translated:
forall v f,
Genv.find_funct_ptr ge v = Some f ->
exists tf,
Genv.find_funct_ptr tge v = Some tf /\ tunnel_fundef f = OK tf.
Proof.
intros.
exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.
Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
rewrite (Genv.find_symbol_match TRANSL). auto.
Qed.
Lemma sig_preserved:
forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f.
Proof.
intros. destruct f.
- simpl in H. monadInv H. (* rq: c'est une tactique maison... *)
unfold tunnel_function in EQ.
destruct (check_included _ _) as [_|] in EQ; try congruence.
monadInv EQ. auto.
- simpl in H. monadInv H. auto.
Qed.
Lemma senv_preserved:
Senv.equiv ge tge.
Proof.
eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve, je ne vais pas réinventer la roue ici *)
Qed.
(* TODO: vérifier s'il faut faire quelque chose avec le `res` ? *)
Inductive match_stackframes: stackframe -> stackframe -> Prop :=
| match_stackframes_intro:
forall res f tf sp pc rs trs
(TF: tunnel_function f = OK tf)
(RS: Registers.regs_lessdef rs trs),
match_stackframes
(Stackframe res f sp pc rs)
(Stackframe res tf sp (branch_target f pc) trs).
(* rq: `match_states s1 s2` correspond à s1 ~ s2 *)
Inductive match_states: state -> state -> Prop :=
| match_states_intro:
forall s ts f tf sp pc rs trs m tm
(STK: list_forall2 match_stackframes s ts)
(TF: tunnel_function f = OK tf)
(RS: Registers.regs_lessdef rs trs)
(MEM: Mem.extends m tm),
match_states
(State s f sp pc rs m)
(State ts tf sp (branch_target f pc) trs tm)
| match_states_call:
forall s ts f tf a ta m tm
(STK: list_forall2 match_stackframes s ts)
(TF: tunnel_fundef f = OK tf)
(ARGS: list_forall2 Val.lessdef a ta)
(MEM: Mem.extends m tm),
match_states
(Callstate s f a m)
(Callstate ts tf ta tm)
| match_states_return:
forall s ts v tv m tm
(STK: list_forall2 match_stackframes s ts)
(VAL: Val.lessdef v tv)
(MEM: Mem.extends m tm),
match_states
(Returnstate s v m)
(Returnstate ts tv tm).
Lemma transf_initial_states:
forall s1: state, initial_state prog s1 ->
exists s2: state, initial_state tprog s2 /\ match_states s1 s2.
Proof.
intros. inversion H.
exploit function_ptr_translated; eauto.
intro Htf. destruct Htf as (tf & Htf & Hf).
exists (Callstate nil tf nil m0). split.
- econstructor.
+ apply (Genv.init_mem_transf_partial TRANSL). auto.
+ rewrite (match_program_main TRANSL).
rewrite symbols_preserved. eauto.
+ apply Htf.
+ rewrite <- H3. apply sig_preserved. apply Hf.
- constructor.
+ constructor.
+ apply Hf.
+ constructor.
+ apply Mem.extends_refl.
Qed.
Lemma transf_final_states:
forall (s1 : state)
(s2 : state) (r : Integers.Int.int),
match_states s1 s2 ->
final_state s1 r ->
final_state s2 r.
Proof.
intros s1 s2 r HM H1. inv H1. inv HM. inv STK. inv VAL. constructor.
Qed.
(* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
(*
Theorem transf_program_correct:
forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
eapply forward_simulation_opt.
apply senv_preserved.
apply transf_initial_states.
apply transf_final_states.
apply tunnel_step_correct.
Qed.
*)
End PRESERVATION.
|
