1 | include "Clight/Csyntax.ma". |
---|
2 | include "Clight/fresh.ma". |
---|
3 | include "basics/lists/list.ma". |
---|
4 | include "common/Identifiers.ma". |
---|
5 | include "Clight/Cexec.ma". |
---|
6 | include "Clight/CexecInd.ma". |
---|
7 | |
---|
8 | (* ----------------------------------------------------------------------------- |
---|
9 | ----------------------------------------------------------------------------*) |
---|
10 | |
---|
11 | (* ----------------------------------------------------------------------------- |
---|
12 | Documentation |
---|
13 | ----------------------------------------------------------------------------*) |
---|
14 | |
---|
15 | (* This file implements transformation of switches to linear sequences of |
---|
16 | * if/then/else. The implementation roughly follows the lines of the prototype. |
---|
17 | * /!\ We assume that the program is well-typed (the type of the evaluated |
---|
18 | * expression must match the constants on each branch of the switch). /!\ *) |
---|
19 | |
---|
20 | (* Documentation. Let the follwing be our input switch construct: |
---|
21 | // --------------------------------- |
---|
22 | switch(e) { |
---|
23 | case v1: |
---|
24 | stmt1 |
---|
25 | case v2: |
---|
26 | stmt2 |
---|
27 | . |
---|
28 | . |
---|
29 | . |
---|
30 | default: |
---|
31 | stmt_default |
---|
32 | } |
---|
33 | // --------------------------------- |
---|
34 | |
---|
35 | Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting |
---|
36 | the switch statement. In the absence of break, the execution falls through each case sequentially. |
---|
37 | |
---|
38 | Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos: |
---|
39 | |
---|
40 | // --------------------------------- |
---|
41 | fresh = e; |
---|
42 | if(fresh == v1) { |
---|
43 | stmt1'; |
---|
44 | goto lbl_case2; |
---|
45 | } |
---|
46 | if(fresh == v2) { |
---|
47 | lbl_case2: |
---|
48 | stmt2'; |
---|
49 | goto lbl_case2; |
---|
50 | } |
---|
51 | ... |
---|
52 | stmt_default'; |
---|
53 | exit_label: |
---|
54 | // --------------------------------- |
---|
55 | |
---|
56 | where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements |
---|
57 | were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels. |
---|
58 | *) |
---|
59 | |
---|
60 | |
---|
61 | (* ----------------------------------------------------------------------------- |
---|
62 | Definitions allowing to state that the program resulting of the transformation |
---|
63 | is switch-free. The actual proof is done using Russell. |
---|
64 | ----------------------------------------------------------------------------*) |
---|
65 | |
---|
66 | (* Property of a Clight statement of containing no switch. Could be generalized into a kind of |
---|
67 | * statement_P, if useful elsewhere. *) |
---|
68 | let rec switch_free (st : statement) : Prop ≝ |
---|
69 | match st with |
---|
70 | [ Sskip ⇒ True |
---|
71 | | Sassign _ _ ⇒ True |
---|
72 | | Scall _ _ _ ⇒ True |
---|
73 | | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
74 | | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
75 | | Swhile e body ⇒ switch_free body |
---|
76 | | Sdowhile e body ⇒ switch_free body |
---|
77 | | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3 |
---|
78 | | Sbreak ⇒ True |
---|
79 | | Scontinue ⇒ True |
---|
80 | | Sreturn _ ⇒ True |
---|
81 | | Sswitch _ _ ⇒ False |
---|
82 | | Slabel _ body ⇒ switch_free body |
---|
83 | | Sgoto _ ⇒ True |
---|
84 | | Scost _ body ⇒ switch_free body |
---|
85 | ]. |
---|
86 | |
---|
87 | definition sf_statement ≝ Σs:statement. switch_free s. |
---|
88 | |
---|
89 | definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement). |
---|
90 | |
---|
91 | (* Property of a list of labeled statements of being switch-free *) |
---|
92 | let rec branches_switch_free (sts : labeled_statements) : Prop ≝ |
---|
93 | match sts with |
---|
94 | [ LSdefault st => |
---|
95 | switch_free st |
---|
96 | | LScase _ _ st tl => |
---|
97 | switch_free st ∧ branches_switch_free tl |
---|
98 | ]. |
---|
99 | |
---|
100 | let rec branch_switch_free_ind |
---|
101 | (sts : labeled_statements) |
---|
102 | (H : labeled_statements → Prop) |
---|
103 | (defcase : ∀st. H (LSdefault st)) |
---|
104 | (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝ |
---|
105 | match sts with |
---|
106 | [ LSdefault st ⇒ |
---|
107 | defcase st |
---|
108 | | LScase sz int st tl ⇒ |
---|
109 | indcase sz int st tl (branch_switch_free_ind tl H defcase indcase) |
---|
110 | ]. |
---|
111 | |
---|
112 | |
---|
113 | (* ----------------------------------------------------------------------------- |
---|
114 | Switch-removal code for statements, functions and fundefs. |
---|
115 | ----------------------------------------------------------------------------*) |
---|
116 | |
---|
117 | (* Given a list of switch cases, prefixes each case by a fresh goto label. It is |
---|
118 | assumed as an hypothesis that each sub-statement is already switch-free |
---|
119 | (argument [H]). The whole function returns a list of labelled switch-free switch |
---|
120 | cases, along the particular label of the default statement and its associated |
---|
121 | statement. A fresh label generator [uv] is threaded through the function. *) |
---|
122 | let rec add_starting_lbl_list |
---|
123 | (l : labeled_statements) |
---|
124 | (H : branches_switch_free l) |
---|
125 | (uv : universe SymbolTag) |
---|
126 | (acc : stlist) : stlist × (label × sf_statement) × (universe SymbolTag) ≝ |
---|
127 | match l return λl'. l = l' → stlist × (label × sf_statement) × (universe SymbolTag) with |
---|
128 | [ LSdefault st ⇒ λEq. |
---|
129 | let 〈default_lab, uv'〉 ≝ fresh ? uv in |
---|
130 | 〈rev ? acc, 〈default_lab, «st, ?»〉, uv'〉 |
---|
131 | | LScase sz tag st other_cases ⇒ λEq. |
---|
132 | let 〈lab, uv'〉 ≝ fresh ? uv in |
---|
133 | let acc' ≝ 〈lab, (mk_DPair ?? sz tag), «st, ?»〉 :: acc in |
---|
134 | add_starting_lbl_list other_cases ? uv' acc' |
---|
135 | ] (refl ? l). |
---|
136 | [ 1: destruct whd in H; // |
---|
137 | | 2: letin H1 ≝ H >Eq in H1; |
---|
138 | #H' normalize in H'; elim H' // |
---|
139 | | 3: >Eq in H; normalize * // |
---|
140 | ] qed. |
---|
141 | |
---|
142 | (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) |
---|
143 | let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ |
---|
144 | match st with |
---|
145 | [ Sbreak ⇒ |
---|
146 | Sgoto lab |
---|
147 | | Ssequence s1 s2 ⇒ |
---|
148 | Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab) |
---|
149 | | Sifthenelse e iftrue iffalse ⇒ |
---|
150 | Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab) |
---|
151 | | Sfor init e update body ⇒ |
---|
152 | Sfor (convert_break_to_goto init lab) e update body |
---|
153 | | Slabel l body ⇒ |
---|
154 | Slabel l (convert_break_to_goto body lab) |
---|
155 | | Scost cost body ⇒ |
---|
156 | Scost cost (convert_break_to_goto body lab) |
---|
157 | | _ ⇒ st |
---|
158 | ]. |
---|
159 | |
---|
160 | (* Converting breaks preserves switch-freeness. *) |
---|
161 | lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). |
---|
162 | #s elim s // |
---|
163 | [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
164 | | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
165 | | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize |
---|
166 | try @conj try @conj /3/ |
---|
167 | | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/ |
---|
168 | | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ |
---|
169 | ] qed. |
---|
170 | |
---|
171 | (* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *) |
---|
172 | let rec produce_cond |
---|
173 | (e : expr) |
---|
174 | (switch_cases : stlist) |
---|
175 | (def_case : ident × sf_statement) |
---|
176 | (exit : label) on switch_cases : sf_statement × label ≝ |
---|
177 | match switch_cases with |
---|
178 | [ nil ⇒ |
---|
179 | match def_case with |
---|
180 | [ mk_Prod default_label default_statement ⇒ |
---|
181 | 〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉 |
---|
182 | ] |
---|
183 | | cons switch_case tail ⇒ |
---|
184 | let 〈case_label, case_value, case_statement〉 ≝ switch_case in |
---|
185 | match case_value with |
---|
186 | [ mk_DPair sz val ⇒ |
---|
187 | let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in |
---|
188 | (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *) |
---|
189 | (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed) in *) |
---|
190 | let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in |
---|
191 | let result ≝ |
---|
192 | Sifthenelse test |
---|
193 | (Slabel case_label |
---|
194 | (Ssequence (convert_break_to_goto (pi1 … case_statement) exit) |
---|
195 | (Sgoto sub_label))) |
---|
196 | (pi1 … sub_statement) |
---|
197 | in |
---|
198 | 〈«result, ?», case_label〉 |
---|
199 | ] |
---|
200 | ]. |
---|
201 | [ 1: normalize @convert_break_lift elim default_statement // |
---|
202 | | 2: whd @conj normalize try @conj try // |
---|
203 | [ 1: @convert_break_lift elim case_statement // |
---|
204 | | 2: elim sub_statement // ] |
---|
205 | ] qed. |
---|
206 | |
---|
207 | (* We assume that the expression e is consistely typed w.r.t. the switch branches *) |
---|
208 | let rec produce_cond2 |
---|
209 | (e : expr) |
---|
210 | (switch_cases : stlist) |
---|
211 | (def_case : ident × sf_statement) |
---|
212 | (exit : label) on switch_cases : sf_statement × label ≝ |
---|
213 | match switch_cases with |
---|
214 | [ nil ⇒ |
---|
215 | let 〈default_label, default_statement〉 ≝ def_case in |
---|
216 | 〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉 |
---|
217 | | cons switch_case tail ⇒ |
---|
218 | let 〈case_label, case_value, case_statement〉 ≝ switch_case in |
---|
219 | match case_value with |
---|
220 | [ mk_DPair sz val ⇒ |
---|
221 | let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in |
---|
222 | let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in |
---|
223 | let case_statement_res ≝ |
---|
224 | Sifthenelse test |
---|
225 | (Slabel case_label |
---|
226 | (Ssequence (convert_break_to_goto (pi1 … case_statement) exit) |
---|
227 | (Sgoto sub_label))) |
---|
228 | Sskip |
---|
229 | in |
---|
230 | 〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉 |
---|
231 | ] |
---|
232 | ]. |
---|
233 | [ 1: normalize @convert_break_lift elim default_statement // |
---|
234 | | 2: whd @conj |
---|
235 | [ 1: whd @conj try // whd in match (switch_free ?); @conj |
---|
236 | [ 1: @convert_break_lift elim case_statement // |
---|
237 | | 2: // ] |
---|
238 | | 2: elim sub_statement // ] |
---|
239 | ] qed. |
---|
240 | |
---|
241 | (* takes an expression, a list of switch-free cases and a freshgen and returns a |
---|
242 | * switch-free equivalent, along an updated freshgen and a new local variable |
---|
243 | * (for storing the value of the expr). *) |
---|
244 | definition simplify_switch : |
---|
245 | expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝ |
---|
246 | λe.λswitch_cases.λH.λuv. |
---|
247 | let 〈exit_label, uv1〉 ≝ fresh ? uv in |
---|
248 | let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in |
---|
249 | let 〈result, useless_label〉 ≝ produce_cond2 e switch_cases defcase exit_label in |
---|
250 | 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉. |
---|
251 | [ 1: normalize try @conj try @conj try // elim result // |
---|
252 | | 2: @H ] |
---|
253 | qed. |
---|
254 | |
---|
255 | (* recursively convert a statement into a switch-free one. *) |
---|
256 | let rec switch_removal |
---|
257 | (st : statement) |
---|
258 | (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝ |
---|
259 | match st return λs.s = st → ? with |
---|
260 | [ Sskip ⇒ λEq. 〈«st,?», [ ], uv〉 |
---|
261 | | Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉 |
---|
262 | | Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉 |
---|
263 | | Ssequence s1 s2 ⇒ λEq. |
---|
264 | let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in |
---|
265 | let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in |
---|
266 | 〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉 |
---|
267 | | Sifthenelse e s1 s2 ⇒ λEq. |
---|
268 | let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in |
---|
269 | let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in |
---|
270 | 〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉 |
---|
271 | | Swhile e body ⇒ λEq. |
---|
272 | let 〈body', vars', uv'〉 ≝ switch_removal body uv in |
---|
273 | 〈«Swhile e (pi1 … body'),?», vars', uv'〉 |
---|
274 | | Sdowhile e body ⇒ λEq. |
---|
275 | let 〈body', vars', uv'〉 ≝ switch_removal body uv in |
---|
276 | 〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 |
---|
277 | | Sfor s1 e s2 s3 ⇒ λEq. |
---|
278 | let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in |
---|
279 | let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in |
---|
280 | let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 uv'' in |
---|
281 | 〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars1 @ vars2 @ vars3, uv'''〉 |
---|
282 | | Sbreak ⇒ λEq. |
---|
283 | 〈«st,?», [ ], uv〉 |
---|
284 | | Scontinue ⇒ λEq. |
---|
285 | 〈«st,?», [ ], uv〉 |
---|
286 | | Sreturn _ ⇒ λEq. |
---|
287 | 〈«st,?», [ ], uv〉 |
---|
288 | | Sswitch e branches ⇒ λEq. |
---|
289 | let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in |
---|
290 | match sf_branches with |
---|
291 | [ mk_Sig branches' H ⇒ |
---|
292 | let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in |
---|
293 | let ident ≝ Expr (Evar switch_tmp) (typeof e) in |
---|
294 | let assign ≝ Sassign ident e in |
---|
295 | let 〈result, uv3〉 ≝ simplify_switch ident branches' H uv2 in |
---|
296 | 〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉 |
---|
297 | ] |
---|
298 | | Slabel label body ⇒ λEq. |
---|
299 | let 〈body', vars', uv'〉 ≝ switch_removal body uv in |
---|
300 | 〈«Slabel label (pi1 … body'), ?», vars', uv'〉 |
---|
301 | | Sgoto _ ⇒ λEq. |
---|
302 | 〈«st, ?», [ ], uv〉 |
---|
303 | | Scost cost body ⇒ λEq. |
---|
304 | let 〈body', vars', uv'〉 ≝ switch_removal body uv in |
---|
305 | 〈«Scost cost (pi1 … body'),?», vars', uv'〉 |
---|
306 | ] (refl ? st) |
---|
307 | |
---|
308 | and switch_removal_branches |
---|
309 | (l : labeled_statements) |
---|
310 | (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝ |
---|
311 | match l with |
---|
312 | [ LSdefault st ⇒ |
---|
313 | let 〈st, vars', uv'〉 ≝ switch_removal st uv in |
---|
314 | 〈«LSdefault (pi1 … st), ?», vars', uv'〉 |
---|
315 | | LScase sz int st tl => |
---|
316 | let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl uv in |
---|
317 | let 〈st', vars'', uv''〉 ≝ switch_removal st uv' in |
---|
318 | 〈«LScase sz int st' (pi1 … tl_result), ?», vars' @ vars'', uv''〉 |
---|
319 | ]. |
---|
320 | try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try // |
---|
321 | [ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj // |
---|
322 | | 2: elim result // |
---|
323 | | 3: elim st // |
---|
324 | | 4: elim st' // |
---|
325 | | 5: elim tl_result // |
---|
326 | ] qed. |
---|
327 | |
---|
328 | definition function_switch_removal : function → universe SymbolTag → function × (universe SymbolTag) ≝ |
---|
329 | λf,u. |
---|
330 | let 〈body, new_vars, u'〉 ≝ switch_removal (fn_body f) u in |
---|
331 | let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (pi1 … body) in |
---|
332 | 〈f, u'〉. |
---|
333 | |
---|
334 | let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝ |
---|
335 | match f with |
---|
336 | [ CL_Internal f ⇒ |
---|
337 | let 〈f',u'〉 ≝ function_switch_removal f u in |
---|
338 | 〈CL_Internal f', u'〉 |
---|
339 | | CL_External _ _ _ ⇒ |
---|
340 | 〈f, u〉 |
---|
341 | ]. |
---|
342 | |
---|
343 | |
---|
344 | (* ----------------------------------------------------------------------------- |
---|
345 | Switch-removal code for programs. |
---|
346 | ----------------------------------------------------------------------------*) |
---|
347 | |
---|
348 | (* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to |
---|
349 | * name clashes for labels. We have no choice but to actually run through the function and to |
---|
350 | * compute the maximum of labels+identifiers. This way we can generate both fresh variables and |
---|
351 | * fresh labels using the same univ. While we're at it we also consider record fields. |
---|
352 | * Cost labels are not considered, though. They already live in a separate universe. |
---|
353 | * |
---|
354 | * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes, |
---|
355 | * but in the end it might be good to move the following functions into fresh.ma. |
---|
356 | *) |
---|
357 | |
---|
358 | (* This is certainly overkill: variables adressed in an expression should be declared in the |
---|
359 | * enclosing function's prototype. *) |
---|
360 | let rec max_of_expr (e : expr) (current : ident) : ident ≝ |
---|
361 | match e with |
---|
362 | [ Expr ed _ ⇒ |
---|
363 | match ed with |
---|
364 | [ Econst_int _ _ ⇒ current |
---|
365 | | Econst_float _ ⇒ current |
---|
366 | | Evar id ⇒ max_id id current |
---|
367 | | Ederef e1 ⇒ max_of_expr e1 current |
---|
368 | | Eaddrof e1 ⇒ max_of_expr e1 current |
---|
369 | | Eunop _ e1 ⇒ max_of_expr e1 current |
---|
370 | | Ebinop _ e1 e2 ⇒ max_of_expr e1 (max_of_expr e2 current) |
---|
371 | | Ecast _ e1 ⇒ max_of_expr e1 current |
---|
372 | | Econdition e1 e2 e3 ⇒ |
---|
373 | max_of_expr e1 (max_of_expr e2 (max_of_expr e3 current)) |
---|
374 | | Eandbool e1 e2 ⇒ |
---|
375 | max_of_expr e1 (max_of_expr e2 current) |
---|
376 | | Eorbool e1 e2 ⇒ |
---|
377 | max_of_expr e1 (max_of_expr e2 current) |
---|
378 | | Esizeof _ ⇒ current |
---|
379 | | Efield r f ⇒ max_id f (max_of_expr r current) |
---|
380 | | Ecost _ e1 ⇒ max_of_expr e1 current |
---|
381 | ] |
---|
382 | ]. |
---|
383 | |
---|
384 | (* Reeasoning about this promises to be a serious pain. Especially the Scall case. *) |
---|
385 | let rec max_of_statement (s : statement) (current : ident) : ident ≝ |
---|
386 | match s with |
---|
387 | [ Sskip ⇒ current |
---|
388 | | Sassign e1 e2 ⇒ max_of_expr e2 (max_of_expr e1 current) |
---|
389 | | Scall ret f args ⇒ |
---|
390 | let retmax ≝ |
---|
391 | match ret with |
---|
392 | [ None ⇒ current |
---|
393 | | Some e ⇒ max_of_expr e current ] |
---|
394 | in |
---|
395 | foldl ?? (λacc,elt. max_of_expr elt acc) (max_of_expr f retmax) args |
---|
396 | | Ssequence s1 s2 ⇒ |
---|
397 | max_of_statement s1 (max_of_statement s2 current) |
---|
398 | | Sifthenelse e s1 s2 ⇒ |
---|
399 | max_of_expr e (max_of_statement s1 (max_of_statement s2 current)) |
---|
400 | | Swhile e body ⇒ |
---|
401 | max_of_expr e (max_of_statement body current) |
---|
402 | | Sdowhile e body ⇒ |
---|
403 | max_of_expr e (max_of_statement body current) |
---|
404 | | Sfor init test incr body ⇒ |
---|
405 | max_of_statement init (max_of_expr test (max_of_statement incr (max_of_statement body current))) |
---|
406 | | Sbreak ⇒ current |
---|
407 | | Scontinue ⇒ current |
---|
408 | | Sreturn opt ⇒ |
---|
409 | match opt with |
---|
410 | [ None ⇒ current |
---|
411 | | Some e ⇒ max_of_expr e current |
---|
412 | ] |
---|
413 | | Sswitch e ls ⇒ |
---|
414 | max_of_expr e (max_of_ls ls current) |
---|
415 | | Slabel lab body ⇒ |
---|
416 | max_id lab (max_of_statement body current) |
---|
417 | | Sgoto lab ⇒ |
---|
418 | max_id lab current |
---|
419 | | Scost _ body ⇒ |
---|
420 | max_of_statement body current |
---|
421 | ] |
---|
422 | and max_of_ls (ls : labeled_statements) (current : ident) : ident ≝ |
---|
423 | match ls with |
---|
424 | [ LSdefault s ⇒ max_of_statement s current |
---|
425 | | LScase _ _ s ls' ⇒ max_of_ls ls' (max_of_statement s current) |
---|
426 | ]. |
---|
427 | |
---|
428 | definition max_id_of_function : function → ident ≝ |
---|
429 | λf. max_of_statement (fn_body f) (max_id_of_fn f). |
---|
430 | |
---|
431 | definition max_id_of_fundef_deep : clight_fundef → ident ≝ |
---|
432 | λf. match f with |
---|
433 | [ CL_Internal f ⇒ max_id_of_function f |
---|
434 | | CL_External id _ _ ⇒ id |
---|
435 | ]. |
---|
436 | |
---|
437 | let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝ |
---|
438 | let func_max ≝ |
---|
439 | foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs |
---|
440 | in max_id func_max current. |
---|
441 | |
---|
442 | definition max_id_of_program_deep : clight_program → ident ≝ |
---|
443 | λp. |
---|
444 | max_id |
---|
445 | (max_id_of_functs_deep (prog_funct ?? p) (prog_main ?? p)) |
---|
446 | (max_id_of_globvars (prog_vars ?? p)). |
---|
447 | |
---|
448 | (* The previous functions compute an (over?)-approximation of the identifiers and labels. |
---|
449 | The following function builds a "good" universe for a complete clight program. *) |
---|
450 | definition universe_for_program_deep : clight_program → universe SymbolTag ≝ |
---|
451 | λp. universe_of_max (max_id_of_program_deep p). |
---|
452 | |
---|
453 | |
---|
454 | let rec program_switch_removal (p : clight_program) : clight_program ≝ |
---|
455 | let uv ≝ universe_for_program_deep p in |
---|
456 | let prog_funcs ≝ prog_funct ?? p in |
---|
457 | let 〈sf_funcs, final_uv〉 ≝ |
---|
458 | foldr ?? (λcl_fundef.λacc. |
---|
459 | let 〈fundefs, uv1〉 ≝ acc in |
---|
460 | let 〈fun_id, fun_def〉 ≝ cl_fundef in |
---|
461 | let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in |
---|
462 | 〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉 |
---|
463 | ) 〈[ ], uv〉 prog_funcs |
---|
464 | in |
---|
465 | mk_program ?? |
---|
466 | (prog_vars … p) |
---|
467 | sf_funcs |
---|
468 | (prog_main … p). |
---|
469 | |
---|
470 | (* ----------------------------------------------------------------------------- |
---|
471 | Simulation proof and related voodoo. |
---|
472 | ----------------------------------------------------------------------------*) |
---|
473 | |
---|
474 | (* Copied from SimplifyCasts.ma. Might be good to create a new file for shared stuff. *) |
---|
475 | inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ |
---|
476 | | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2 |
---|
477 | | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2. |
---|
478 | |
---|
479 | definition expr_lvalue_ind_combined ≝ |
---|
480 | λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. |
---|
481 | conj ?? |
---|
482 | (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) |
---|
483 | (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). |
---|
484 | |
---|
485 | let rec expr_ind2 |
---|
486 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
487 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
488 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
489 | (Iconst_float : ∀f, t. Q (Econst_float f) t) |
---|
490 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
491 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
492 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
493 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
494 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
495 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
496 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
497 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
498 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
499 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
500 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
501 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
502 | (e : expr) on e : P e ≝ |
---|
503 | match e with |
---|
504 | [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ] |
---|
505 | |
---|
506 | and expr_desc_ind2 |
---|
507 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
508 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
509 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
510 | (Iconst_float : ∀f, t. Q (Econst_float f) t) |
---|
511 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
512 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
513 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
514 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
515 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
516 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
517 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
518 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
519 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
520 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
521 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
522 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
523 | (ed : expr_descr) (t : type) on ed : Q ed t ≝ |
---|
524 | match ed with |
---|
525 | [ Econst_int sz i ⇒ Iconst_int sz i t |
---|
526 | | Econst_float f ⇒ Iconst_float f t |
---|
527 | | Evar id ⇒ Ivar id t |
---|
528 | | Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
529 | | Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
530 | | Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
531 | | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
532 | | Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
533 | | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) |
---|
534 | | Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
535 | | Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
536 | | Esizeof sizeoft ⇒ Isizeof sizeoft t |
---|
537 | | Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
538 | | Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
539 | ]. |
---|
540 | |
---|
541 | (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched |
---|
542 | by a non-constant number of evaluations in the converted program. More precisely, |
---|
543 | [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps |
---|
544 | necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *) |
---|
545 | |
---|
546 | (* A version of simplify_switch hiding the ugly proj *) |
---|
547 | definition sw_rem : statement → (universe SymbolTag) → statement ≝ |
---|
548 | λs,u. |
---|
549 | \fst (\fst (switch_removal s u)). |
---|
550 | |
---|
551 | definition fresh_for_expression ≝ |
---|
552 | λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u. |
---|
553 | |
---|
554 | definition fresh_for_statement ≝ |
---|
555 | λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u. |
---|
556 | |
---|
557 | definition fresh_for_function ≝ |
---|
558 | λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. |
---|
559 | |
---|
560 | let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝ |
---|
561 | match k with |
---|
562 | [ Kstop ⇒ True |
---|
563 | | Kseq s k0 ⇒ (fresh_for_statement s u) ∧ (fresh_for_continuation k0 u) |
---|
564 | | Kwhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u) |
---|
565 | | Kdowhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u) |
---|
566 | | Kfor2 e s1 s2 k0 ⇒ |
---|
567 | (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧ |
---|
568 | (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u) |
---|
569 | | Kfor3 e s1 s2 k0 ⇒ |
---|
570 | (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧ |
---|
571 | (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u) |
---|
572 | | Kswitch k0 ⇒ fresh_for_continuation k0 u |
---|
573 | | Kcall _ f e k ⇒ (fresh_for_function f u) ∧ (fresh_for_continuation k u) |
---|
574 | ]. |
---|
575 | |
---|
576 | inductive switch_cont_sim : cont → cont → Prop ≝ |
---|
577 | | swc_stop : |
---|
578 | switch_cont_sim Kstop Kstop |
---|
579 | | swc_seq : ∀s,k,k',u. |
---|
580 | fresh_for_statement s u → |
---|
581 | switch_cont_sim k k' → |
---|
582 | switch_cont_sim (Kseq s k) (Kseq (sw_rem s u) k') |
---|
583 | | swc_while : ∀e,s,k,k',u. |
---|
584 | fresh_for_expression e u → |
---|
585 | fresh_for_statement s u → |
---|
586 | switch_cont_sim k k' → |
---|
587 | switch_cont_sim (Kwhile e s k) (Kwhile e (sw_rem s u) k') |
---|
588 | | swc_dowhile : ∀e,s,k,k',u. |
---|
589 | fresh_for_expression e u → |
---|
590 | fresh_for_statement s u → |
---|
591 | switch_cont_sim k k' → |
---|
592 | switch_cont_sim (Kdowhile e s k) (Kdowhile e (sw_rem s u) k') |
---|
593 | | swc_for1 : ∀e,s1,s2,k,k',u1,u2. |
---|
594 | fresh_for_statement s1 u1 → |
---|
595 | fresh_for_statement s2 u2 → |
---|
596 | switch_cont_sim k k' → |
---|
597 | switch_cont_sim (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip e (sw_rem s1 u1) (sw_rem s2 u2)) k') |
---|
598 | | swc_for2 : ∀e,s1,s2,k,k',u1,u2. |
---|
599 | fresh_for_statement s1 u1 → |
---|
600 | fresh_for_statement s2 u2 → |
---|
601 | switch_cont_sim k k' → |
---|
602 | switch_cont_sim (Kfor2 e s1 s2 k) (Kfor2 e (sw_rem s1 u1) (sw_rem s2 u2) k') |
---|
603 | | swc_for3 : ∀e,s1,s2,k,k',u1,u2. |
---|
604 | fresh_for_statement s1 u1 → |
---|
605 | fresh_for_statement s2 u2 → |
---|
606 | switch_cont_sim k k' → |
---|
607 | switch_cont_sim (Kfor3 e s1 s2 k) (Kfor3 e (sw_rem s1 u1) (sw_rem s2 u2) k') |
---|
608 | | swc_switch : ∀k,k'. |
---|
609 | switch_cont_sim k k' → |
---|
610 | switch_cont_sim (Kswitch k) (Kswitch k') |
---|
611 | | swc_call : ∀r,f,en,k,k',u. |
---|
612 | fresh_for_function f u → |
---|
613 | switch_cont_sim k k' → |
---|
614 | switch_cont_sim (Kcall r f en k) (Kcall r (\fst (function_switch_removal f u)) en k'). |
---|
615 | |
---|
616 | |
---|
617 | inductive switch_state_sim : state → state → Prop ≝ |
---|
618 | | sws_state : ∀uf,us,uk,f,s,k,k',e,m. |
---|
619 | fresh_for_function f uf → |
---|
620 | fresh_for_statement s us → |
---|
621 | fresh_for_continuation k' uk → |
---|
622 | switch_cont_sim k k' → |
---|
623 | switch_state_sim (State f s k e m) (State (\fst (function_switch_removal f uf)) (sw_rem s us) k' e m) |
---|
624 | (* Extra matching states that we can reach that don't quite correspond to the |
---|
625 | labelling function *) |
---|
626 | (* |
---|
627 | | sws_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → |
---|
628 | switch_state_sim (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
629 | | sws_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → |
---|
630 | switch_state_sim (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
631 | | sws_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → |
---|
632 | switch_state_sim (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
633 | *) |
---|
634 | (* and the rest *) |
---|
635 | | sws_callstate : ∀ufd,fd,args,k,k',m. |
---|
636 | switch_cont_sim k k' → |
---|
637 | switch_state_sim (Callstate fd args k m) (Callstate (\fst (fundef_switch_removal fd ufd)) args k' m) |
---|
638 | | sws_returnstate : ∀res,k,k',m. |
---|
639 | switch_cont_sim k k' → |
---|
640 | switch_state_sim (Returnstate res k m) (Returnstate res k' m) |
---|
641 | | sws_finalstate : ∀r. |
---|
642 | switch_state_sim (Finalstate r) (Finalstate r) |
---|
643 | . |
---|
644 | |
---|
645 | inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ |
---|
646 | | eventually_base : ∀s,t,s'. |
---|
647 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
648 | P s' → |
---|
649 | eventually ge P s t |
---|
650 | | eventually_step : ∀s,t,s',t'. |
---|
651 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
652 | eventually ge P s' t' → |
---|
653 | eventually ge P s (t ⧺ t'). |
---|
654 | |
---|
655 | (* [eventually] is not so nice to use directly, we would like to make the mandatory |
---|
656 | * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not |
---|
657 | to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) |
---|
658 | lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → |
---|
659 | eventually ge P s t. |
---|
660 | #ge #P #s #t * #s' * #Hexec #HP %1{? Hexec HP} |
---|
661 | qed. |
---|
662 | |
---|
663 | record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { |
---|
664 | rg_find_symbol: ∀s. |
---|
665 | find_symbol ? ge s = find_symbol ? ge' s; |
---|
666 | rg_find_funct: ∀v,f. |
---|
667 | find_funct ? ge v = Some ? f → |
---|
668 | find_funct ? ge' v = Some ? (t f); |
---|
669 | rg_find_funct_ptr: ∀b,f. |
---|
670 | find_funct_ptr ? ge b = Some ? f → |
---|
671 | find_funct_ptr ? ge' b = Some ? (t f) |
---|
672 | }. |
---|
673 | |
---|
674 | (* TODO ... fundef_switch_removal wants a universe which is fresh-for-its argument. *) |
---|
675 | (* |
---|
676 | lemma sim_related_globals : ∀ge,ge',en,m,u. related_globals ? fundef_switch_removal ge ge' → |
---|
677 | (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ |
---|
678 | (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). |
---|
679 | *) |
---|
680 | |
---|
681 | (* The return type of any function is invariant under switch removal *) |
---|
682 | lemma fn_return_simplify : ∀f,u. fn_return (\fst (function_switch_removal f u)) = fn_return f. |
---|
683 | #f #u elim f #ret #args #vars #body normalize elim (switch_removal body u) |
---|
684 | * * #body' #Hswitch_free #new_vars #u' normalize // |
---|
685 | qed. |
---|
686 | |
---|
687 | lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0). |
---|
688 | #e0 #s0 #us0 normalize |
---|
689 | cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize // |
---|
690 | qed. |
---|
691 | |
---|
692 | lemma max_one_neutral : ∀v. max v one = v. |
---|
693 | * // qed. |
---|
694 | |
---|
695 | lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. |
---|
696 | * #p whd in ⊢ (??%?); >max_one_neutral // qed. |
---|
697 | |
---|
698 | lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1. |
---|
699 | * #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%); |
---|
700 | >commutative_max // qed. |
---|
701 | |
---|
702 | lemma transitive_le : transitive ? le. // qed. |
---|
703 | |
---|
704 | lemma le_S_weaken : ∀a,b. le (succ a) b → le a b. |
---|
705 | #a #b /2/ qed. |
---|
706 | |
---|
707 | (* cycle of length 1 *) |
---|
708 | lemma le_S_contradiction_1 : ∀a. le (succ a) a → False. |
---|
709 | * /2 by absurd/ qed. |
---|
710 | |
---|
711 | (* cycle of length 2 *) |
---|
712 | lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False. |
---|
713 | #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) |
---|
714 | #Heq @(le_S_contradiction_1 a) destruct // qed. |
---|
715 | |
---|
716 | (* cycle of length 3 *) |
---|
717 | lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False. |
---|
718 | #a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4 |
---|
719 | @(le_S_contradiction_2 … H3 H4) |
---|
720 | qed. |
---|
721 | |
---|
722 | lemma reflexive_leb : ∀a. leb a a = true. |
---|
723 | #a @(le_to_leb_true a a) // qed. |
---|
724 | |
---|
725 | (* |
---|
726 | lemma le_S_contradiction : ∀a,b. le (succ a) b → le (succ b) a → False. |
---|
727 | #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) #Heq |
---|
728 | destruct inversion H2 |
---|
729 | [ 2: #m #H1 #H2 #H3 |
---|
730 | elim b; normalize in match (succ ?); |
---|
731 | [ 1: #H destruct (H) |
---|
732 | | 2: #p #H |
---|
733 | *) |
---|
734 | (* This should be somewhere else. *) |
---|
735 | lemma associative_max : associative ? max. |
---|
736 | #a #b #c |
---|
737 | whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c); |
---|
738 | lapply (pos_compare_to_Prop a b) |
---|
739 | cases (pos_compare a b) whd in ⊢ (% → ?); #Hab |
---|
740 | [ 1: >(le_to_leb_true a b) normalize nodelta /2/ |
---|
741 | lapply (pos_compare_to_Prop b c) |
---|
742 | cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc |
---|
743 | [ 1: >(le_to_leb_true b c) normalize nodelta |
---|
744 | lapply (pos_compare_to_Prop a c) |
---|
745 | cases (pos_compare a c) whd in ⊢ (% → ?); #Hac |
---|
746 | [ 1: >(le_to_leb_true a c) /2/ |
---|
747 | | 2: destruct cases (leb c c) // |
---|
748 | | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *) |
---|
749 | @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac)) |
---|
750 | ] |
---|
751 | @le_S_weaken // |
---|
752 | | 2: destruct |
---|
753 | cases (leb c c) normalize nodelta |
---|
754 | >(le_to_leb_true a c) /2/ |
---|
755 | | 3: >(not_le_to_leb_false b c) normalize nodelta /2/ |
---|
756 | >(le_to_leb_true a b) /2/ |
---|
757 | ] |
---|
758 | | 2: destruct (Hab) >reflexive_leb normalize nodelta |
---|
759 | lapply (pos_compare_to_Prop b c) |
---|
760 | cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc |
---|
761 | [ 1: >(le_to_leb_true b c) normalize nodelta |
---|
762 | >(le_to_leb_true b c) normalize nodelta |
---|
763 | /2/ |
---|
764 | | 2: destruct >reflexive_leb normalize nodelta |
---|
765 | >reflexive_leb // |
---|
766 | | 3: >(not_le_to_leb_false b c) normalize nodelta |
---|
767 | >reflexive_leb /2/ ] |
---|
768 | | 3: >(not_le_to_leb_false a b) normalize nodelta /2/ |
---|
769 | lapply (pos_compare_to_Prop b c) |
---|
770 | cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc |
---|
771 | [ 1: >(le_to_leb_true b c) normalize nodelta /2/ |
---|
772 | | 2: destruct >reflexive_leb normalize nodelta @refl |
---|
773 | | 3: >(not_le_to_leb_false b c) normalize nodelta |
---|
774 | >(not_le_to_leb_false a b) normalize nodelta |
---|
775 | >(not_le_to_leb_false a c) normalize nodelta |
---|
776 | lapply (transitive_le … Hbc (le_S_weaken … Hab)) |
---|
777 | #Hca /2/ |
---|
778 | ] |
---|
779 | ] qed. |
---|
780 | |
---|
781 | lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). |
---|
782 | * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // |
---|
783 | qed. |
---|
784 | |
---|
785 | lemma max_of_expr_rewrite : |
---|
786 | ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id. |
---|
787 | @(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id)) |
---|
788 | [ 1: #ed #t // ] |
---|
789 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
790 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
791 | #ty |
---|
792 | [ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta |
---|
793 | whd in match (max_id ??) in ⊢ (???%); |
---|
794 | >max_one_neutral // ] |
---|
795 | [ 1,2,11: * * // |
---|
796 | | 3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind |
---|
797 | | 6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); |
---|
798 | >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one))) |
---|
799 | >max_id_associative |
---|
800 | >Hind1 |
---|
801 | cases (max_of_expr e1 ?) |
---|
802 | #v1 <Hind2 @refl |
---|
803 | | 8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); |
---|
804 | >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?); |
---|
805 | >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%); |
---|
806 | >max_id_associative >max_id_associative @refl |
---|
807 | | 12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); |
---|
808 | cases field #p normalize nodelta |
---|
809 | >Hind cases (max_of_expr e1 ?) #e' |
---|
810 | cases id #id' |
---|
811 | whd in match (max_id ??); normalize nodelta |
---|
812 | whd in match (max_id ??); >associative_max @refl |
---|
813 | ] qed. |
---|
814 | |
---|
815 | lemma expr_fresh_lift : |
---|
816 | ∀e,u,id. |
---|
817 | fresh_for_expression e u → |
---|
818 | fresh_for_univ SymbolTag id u → |
---|
819 | fresh_for_univ SymbolTag (max_of_expr e id) u. |
---|
820 | #e #u #id |
---|
821 | normalize in match (fresh_for_expression e u); |
---|
822 | #H1 #H2 |
---|
823 | >max_of_expr_rewrite |
---|
824 | normalize in match (fresh_for_univ ???); |
---|
825 | cases (max_of_expr e ?) in H1; #p #H1 |
---|
826 | cases id in H2; #p' #H2 |
---|
827 | normalize nodelta |
---|
828 | cases (leb p p') normalize nodelta |
---|
829 | [ 1: @H2 | 2: @H1 ] |
---|
830 | qed. |
---|
831 | |
---|
832 | |
---|
833 | lemma while_fresh_lift : ∀e,s,u. |
---|
834 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u. |
---|
835 | #e #s #u normalize #Hfresh_expr |
---|
836 | elim (max_of_statement s (an_identifier SymbolTag one)) #p |
---|
837 | #Hfresh_p |
---|
838 | @expr_fresh_lift |
---|
839 | [ 2: // |
---|
840 | | 1: @Hfresh_expr ] |
---|
841 | qed. |
---|
842 | |
---|
843 | (* |
---|
844 | theorem switch_removal_correction : ∀ge, ge', u. |
---|
845 | related_globals ? (λclfd.\fst (fundef_switch_removal clfd u)) ge ge' → |
---|
846 | ∀s1, s1', tr, s2. |
---|
847 | switch_state_sim s1 s1' → |
---|
848 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
849 | eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr. |
---|
850 | #ge #ge' #u #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step |
---|
851 | inversion Hsim_state |
---|
852 | [ 1: (* regular state *) |
---|
853 | #uf #us #uk #f #s #k #k' #e #m #Huf_fresh #Hus_fresh #Huk_fresh #Hsim_cont #Hs1_eq #Hs1_eq' #_ |
---|
854 | >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?); |
---|
855 | cases s in Hus_fresh; |
---|
856 | (* Perform the intros for the statements*) |
---|
857 | [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body |
---|
858 | | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body |
---|
859 | | 14: #lab | 15: #cost #body ] |
---|
860 | #Hus_fresh |
---|
861 | [ 1: (* Skip *) |
---|
862 | whd in match (sw_rem ??); |
---|
863 | inversion Hsim_cont normalize nodelta |
---|
864 | [ 1: #Hk #Hk' #_ #Hexec_step |
---|
865 | @(eventually_base … (Returnstate Vundef Kstop (free_list m (blocks_of_env e)))) |
---|
866 | [ 1: whd in match (exec_step ??); >fn_return_simplify ] |
---|
867 | cases (fn_return f) in Hexec_step; |
---|
868 | [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain |
---|
869 | | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ] |
---|
870 | normalize nodelta |
---|
871 | [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) // %3 destruct // |
---|
872 | | *: #H destruct (H) ] |
---|
873 | | 2: #s0 #k0 #k0' #us0 #Hus0_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
874 | whd in match (ret ??) in Heq; destruct (Heq) |
---|
875 | @(eventually_now ????) whd in match (exec_step ??); |
---|
876 | %{(State (\fst (function_switch_removal f uf)) (sw_rem s0 us0) k0' e m)} @conj try // |
---|
877 | %1{uf us0 uk} // |
---|
878 | >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); >Hk' |
---|
879 | whd in ⊢ (% → ?); * #_ // |
---|
880 | | 3: #e0 #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
881 | @(eventually_now ????) whd in match (exec_step ??); |
---|
882 | whd in match (ret ??) in Heq; destruct (Heq) |
---|
883 | %{(State (\fst (function_switch_removal f uf)) (Swhile e0 (sw_rem s0 us0)) k0' e m)} @conj try // |
---|
884 | >while_commute %1{uf us0 uk} // |
---|
885 | [ 1: @while_fresh_lift assumption |
---|
886 | | 2: >Hk' in Huk_fresh; whd in ⊢ (% → ?); * #_ // ] |
---|
887 | | 4: #eO #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
888 | @(eventually_now ????) whd in match (exec_step ??); |
---|
889 | |
---|
890 | |
---|
891 | |
---|
892 | [ 1: @uk |
---|
893 | | 2: >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); * * // ] |
---|
894 | |
---|
895 | whd |
---|
896 | normalize |
---|
897 | |
---|
898 | cut (Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0)) |
---|
899 | [ 1: whd in match (sw_rem (Swhile ??) ?); |
---|
900 | whd in match (switch_removal ??); |
---|
901 | whd in match (exec_step ??); |
---|
902 | |
---|
903 | (* foireux pour le (Expr (Econst_int sz n) ?) *) |
---|
904 | lemma convert : |
---|
905 | ∀uv. |
---|
906 | ∀sz,n,sl. |
---|
907 | seq_of_labeled_statements (select_switch sz n sl) |
---|
908 | ~~~u |
---|
909 | let 〈exit_label, uv1〉 ≝ fresh ? uv in |
---|
910 | let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list sl ? uv1 [ ] in |
---|
911 | Ssequence (pi1 … (produce_cond2 (Expr (Econst_int sz n)) sl defcase exit_label)) (Slabel exit_label Sskip) |
---|
912 | |
---|
913 | |
---|
914 | lemma convert : |
---|
915 | ∀f,cond,ls,k,ge,e,m. |
---|
916 | ∀t. |
---|
917 | ∀sz,n. exec_step ge (State f (Sswitch cond ls) k e m) = Value ??? 〈t,State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m〉 → |
---|
918 | ∀uf,us. |
---|
919 | fresh_for_function f uf → |
---|
920 | fresh_for_statement (Sswitch cond ls) us → |
---|
921 | ∃s',k'. |
---|
922 | (exec_plus ge |
---|
923 | E0 (State (\fst (function_switch_removal f uf)) (sw_rem (Sswitch cond ls) us) k' e m) |
---|
924 | t s') |
---|
925 | ∧ switch_cont_sim k k' |
---|
926 | ∧ switch_state_sim |
---|
927 | (State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m) |
---|
928 | s'. |
---|
929 | #f #cond #ls #k #ge #e #m #t #sz #n #Hexec #uf #us #Huf #Hus |
---|
930 | whd in match (sw_rem ??); |
---|
931 | whd in match (switch_removal ??); |
---|
932 | check eq_ind |
---|
933 | |
---|
934 | |
---|
935 | |
---|
936 | whd in Hexec:(??%?); cases (exec_expr ge e m cond) in Hexec; |
---|
937 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
938 | * #cond_val #cond_trace |
---|
939 | whd in match (bindIO ??????); |
---|
940 | cases cond_val |
---|
941 | [ 1: | 2: #sz' #n' | 3: #fl | 4: #rg | 5: #ptr ] |
---|
942 | [ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
943 | normalize nodelta #Heq whd in match (ret ??) in Heq; |
---|
944 | |
---|
945 | |
---|
946 | |
---|
947 | |
---|
948 | ! 〈v,tr〉 ← exec_expr ge e m a : IO ???; |
---|
949 | match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉 |
---|
950 | | _ ⇒ Wrong ??? (msg TypeMismatch) ] |
---|
951 | |
---|
952 | theorem step_with_labels : ∀ge,ge'. |
---|
953 | related_globals ? label_fundef ge ge' → |
---|
954 | state_with_labels s1 s1' → |
---|
955 | exec_expr ge en m e = OK ? 〈Vint sz v, tr〉 → |
---|
956 | (seq_of_labeled_statement (select_switch sz n sl) ~ simplify_switch |
---|
957 | (exec_step ge st (Sswitch e ls) |
---|
958 | |
---|
959 | |
---|
960 | ∃tr',s2'. plus ge' s1' tr' s2' ∧ |
---|
961 | trace_with_extra_labels tr tr' ∧ |
---|
962 | state_with_labels s2 s2'). |
---|
963 | |
---|
964 | |
---|
965 | *) |
---|
966 | |
---|