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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
(** RTL node duplication using external oracle. Used to form superblock
structures *)
Require Import AST RTL Maps Globalenvs.
Require Import Coqlib Errors Op.
Module Type DuplicateOracle.
(** External oracle returning the new RTL code (entry point unchanged),
along with the new entrypoint, and a mapping of new nodes to old nodes *)
Parameter duplicate_aux: function -> code * node * (PTree.t node).
End DuplicateOracle.
Module Duplicate (D: DuplicateOracle).
Export D.
Definition duplicate_aux := duplicate_aux.
(* Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". *)
Local Open Scope error_monad_scope.
Local Open Scope positive_scope.
(** * Verification of node duplications *)
Definition verify_is_copy dupmap n n' :=
match dupmap!n' with
| None => Error(msg "verify_is_copy None")
| Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
end.
Fixpoint verify_is_copy_list dupmap ln ln' :=
match ln with
| n::ln => match ln' with
| n'::ln' => do u <- verify_is_copy dupmap n n';
verify_is_copy_list dupmap ln ln'
| nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end
| nil => match ln' with
| n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'")
| nil => OK tt end
end.
Definition verify_mapping_entrypoint dupmap (f f': function): res unit :=
verify_is_copy dupmap (fn_entrypoint f) (fn_entrypoint f').
Lemma product_eq {A B: Type} :
(forall (a b: A), {a=b} + {a<>b}) ->
(forall (c d: B), {c=d} + {c<>d}) ->
forall (x y: A+B), {x=y} + {x<>y}.
Proof.
intros H H'. intros. decide equality.
Qed.
(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application"
* error when doing so *)
Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}.
Proof.
intros.
apply (builtin_arg_eq Pos.eq_dec).
Defined.
Global Opaque builtin_arg_eq_pos.
Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed.
Global Opaque builtin_res_eq_pos.
Definition verify_match_inst dupmap inst tinst :=
match inst with
| Inop n => match tinst with Inop n' => verify_is_copy dupmap n n' | _ => Error(msg "verify_match_inst Inop") end
| Iop op lr r n => match tinst with
Iop op' lr' r' n' =>
do u <- verify_is_copy dupmap n n';
if (eq_operation op op') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then
OK tt
else Error (msg "Different r in Iop")
else Error (msg "Different lr in Iop")
else Error(msg "Different operations in Iop")
| _ => Error(msg "verify_match_inst Inop") end
| Iload tm m a lr r n => match tinst with
| Iload tm' m' a' lr' r' n' =>
do u <- verify_is_copy dupmap n n';
if (trapping_mode_eq tm tm') then
if (chunk_eq m m') then
if (eq_addressing a a') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then OK tt
else Error (msg "Different r in Iload")
else Error (msg "Different lr in Iload")
else Error (msg "Different addressing in Iload")
else Error (msg "Different mchunk in Iload")
else Error (msg "Different trapping_mode in Iload")
| _ => Error (msg "verify_match_inst Iload") end
| Istore m a lr r n => match tinst with
| Istore m' a' lr' r' n' =>
do u <- verify_is_copy dupmap n n';
if (chunk_eq m m') then
if (eq_addressing a a') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then OK tt
else Error (msg "Different r in Istore")
else Error (msg "Different lr in Istore")
else Error (msg "Different addressing in Istore")
else Error (msg "Different mchunk in Istore")
| _ => Error (msg "verify_match_inst Istore") end
| Icall s ri lr r n => match tinst with
| Icall s' ri' lr' r' n' =>
do u <- verify_is_copy dupmap n n';
if (signature_eq s s') then
if (product_eq Pos.eq_dec ident_eq ri ri') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then OK tt
else Error (msg "Different r r' in Icall")
else Error (msg "Different lr in Icall")
else Error (msg "Different ri in Icall")
else Error (msg "Different signatures in Icall")
| _ => Error (msg "verify_match_inst Icall") end
| Itailcall s ri lr => match tinst with
| Itailcall s' ri' lr' =>
if (signature_eq s s') then
if (product_eq Pos.eq_dec ident_eq ri ri') then
if (list_eq_dec Pos.eq_dec lr lr') then OK tt
else Error (msg "Different lr in Itailcall")
else Error (msg "Different ri in Itailcall")
else Error (msg "Different signatures in Itailcall")
| _ => Error (msg "verify_match_inst Itailcall") end
| Ibuiltin ef lbar brr n => match tinst with
| Ibuiltin ef' lbar' brr' n' =>
do u <- verify_is_copy dupmap n n';
if (external_function_eq ef ef') then
if (list_eq_dec builtin_arg_eq_pos lbar lbar') then
if (builtin_res_eq_pos brr brr') then OK tt
else Error (msg "Different brr in Ibuiltin")
else Error (msg "Different lbar in Ibuiltin")
else Error (msg "Different ef in Ibuiltin")
| _ => Error (msg "verify_match_inst Ibuiltin") end
| Icond cond lr n1 n2 i => match tinst with
| Icond cond' lr' n1' n2' i' =>
if (list_eq_dec Pos.eq_dec lr lr') then
if (eq_condition cond cond') then
do u1 <- verify_is_copy dupmap n1 n1';
verify_is_copy dupmap n2 n2'
else if (eq_condition (negate_condition cond) cond') then
do u1 <- verify_is_copy dupmap n1 n2';
verify_is_copy dupmap n2 n1'
else Error (msg "Incompatible conditions in Icond")
else Error (msg "Different lr in Icond")
| _ => Error (msg "verify_match_inst Icond") end
| Ijumptable r ln => match tinst with
| Ijumptable r' ln' =>
do u <- verify_is_copy_list dupmap ln ln';
if (Pos.eq_dec r r') then OK tt
else Error (msg "Different r in Ijumptable")
| _ => Error (msg "verify_match_inst Ijumptable") end
| Ireturn or => match tinst with
| Ireturn or' =>
if (option_eq Pos.eq_dec or or') then OK tt
else Error (msg "Different or in Ireturn")
| _ => Error (msg "verify_match_inst Ireturn") end
end.
Definition verify_mapping_mn dupmap f f' (m: positive*positive) :=
let (tn, n) := m in
match (fn_code f)!n with
| None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n")
| Some inst => match (fn_code f')!tn with
| None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn")
| Some tinst => verify_match_inst dupmap inst tinst
end
end.
Fixpoint verify_mapping_mn_rec dupmap f f' lm :=
match lm with
| nil => OK tt
| m :: lm => do u <- verify_mapping_mn dupmap f f' m;
verify_mapping_mn_rec dupmap f f' lm
end.
Definition verify_mapping_match_nodes dupmap (f f': function): res unit :=
verify_mapping_mn_rec dupmap f f' (PTree.elements dupmap).
(** Verifies that the [dupmap] of the translated function [f'] is giving correct information in regards to [f] *)
Definition verify_mapping dupmap (f f': function) : res unit :=
do u <- verify_mapping_entrypoint dupmap f f';
verify_mapping_match_nodes dupmap f f'.
(** * Entry points *)
Definition transf_function (f: function) : res function :=
let (tcte, dupmap) := duplicate_aux f in
let (tc, te) := tcte in
let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in
do u <- verify_mapping dupmap f f';
OK f'.
Definition transf_fundef (f: fundef) : res fundef :=
transf_partial_fundef transf_function f.
Definition transf_program (p: program) : res program :=
transform_partial_program transf_fundef p.
End Duplicate.
|
