source: src/Clight/switchRemoval.ma @ 2107

Last change on this file since 2107 was 2076, checked in by garnier, 8 years ago

First steps towards a simulation proof for switch removal.

  • Property svn:executable set to *
File size: 40.7 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/fresh.ma".
3include "basics/lists/list.ma".
4include "common/Identifiers.ma".
5include "Clight/Cexec.ma".
6include "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. *)
68let rec switch_free (st : statement) : Prop ≝
69match 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
87definition sf_statement ≝ Σs:statement. switch_free s.
88
89definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement).
90
91(* Property of a list of labeled statements of being switch-free *)
92let rec branches_switch_free (sts : labeled_statements) : Prop ≝
93match sts with
94[ LSdefault st =>
95  switch_free st
96| LScase _ _ st tl =>
97  switch_free st ∧ branches_switch_free tl
98].
99
100let 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)) ≝
105match 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.  *)
122let 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) ≝
127match 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.  *)
143let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
144match 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. *)
161lemma 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. *)
172let 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 ≝
177match 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 *)
208let 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 ≝
213match 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). *)
244definition 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 ]
253qed.
254
255(* recursively convert a statement into a switch-free one. *)
256let rec switch_removal
257  (st : statement)
258  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
259match 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
308and switch_removal_branches
309  (l : labeled_statements)
310  (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝
311match 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].
320try @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
328definition 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
334let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝
335match 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. *)
360let rec max_of_expr (e : expr) (current : ident) : ident ≝
361match 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. *)
385let rec max_of_statement (s : statement) (current : ident) : ident ≝
386match 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]
422and max_of_ls (ls : labeled_statements) (current : ident) : ident ≝
423match 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
428definition max_id_of_function : function → ident ≝
429λf. max_of_statement (fn_body f) (max_id_of_fn f).
430
431definition 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
437let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝
438let func_max ≝
439  foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs
440in max_id func_max current.
441
442definition 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. *)
450definition universe_for_program_deep : clight_program → universe SymbolTag ≝
451λp. universe_of_max (max_id_of_program_deep p).
452
453
454let 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. *)
475inductive 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
479definition expr_lvalue_ind_combined ≝
480λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
481conj ??
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 
485let 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 ≝
503match 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
506and 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 ≝
524match 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 *)
547definition sw_rem : statement → (universe SymbolTag) → statement ≝
548λs,u.
549  \fst (\fst (switch_removal s u)).
550
551definition fresh_for_expression ≝
552λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u. 
553 
554definition fresh_for_statement ≝
555λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u.
556
557definition fresh_for_function ≝
558λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.
559
560let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝
561match 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
576inductive 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
617inductive 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
645inductive 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. *)     
658lemma 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}
661qed.
662
663record 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(*
676lemma 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 *)
682lemma 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 //
685qed.
686
687lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0).
688#e0 #s0 #us0 normalize
689cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize //
690qed.
691
692lemma max_one_neutral : ∀v. max v one = v.
693* // qed.
694
695lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v.
696* #p whd in ⊢ (??%?); >max_one_neutral // qed.
697
698lemma 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
702lemma transitive_le : transitive ? le. // qed.
703
704lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
705#a #b /2/ qed.
706
707(* cycle of length 1 *)
708lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
709* /2 by absurd/ qed.
710
711(* cycle of length 2 *)
712lemma 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 *)
717lemma 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)
720qed.
721
722lemma reflexive_leb : ∀a. leb a a = true.
723#a @(le_to_leb_true a a) // qed.
724
725(*
726lemma 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
728destruct inversion H2
729[ 2: #m #H1 #H2 #H3
730elim b; normalize in match (succ ?);
731[ 1: #H destruct (H)
732| 2: #p #H
733*)
734(* This should be somewhere else. *)
735lemma associative_max : associative ? max.
736#a #b #c
737whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
738lapply (pos_compare_to_Prop a b)
739cases (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
781lemma 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 //
783qed.
784
785lemma 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
815lemma 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
821normalize in match (fresh_for_expression e u);
822#H1 #H2
823>max_of_expr_rewrite
824normalize in match (fresh_for_univ ???);
825cases (max_of_expr e ?) in H1; #p #H1
826cases id in H2; #p' #H2
827normalize nodelta
828cases (leb p p') normalize nodelta
829[ 1: @H2 | 2: @H1 ]
830qed.
831
832
833lemma 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
836elim (max_of_statement s (an_identifier SymbolTag one)) #p
837#Hfresh_p
838@expr_fresh_lift
839[ 2: //
840| 1: @Hfresh_expr ]
841qed.
842
843(*   
844theorem 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
851inversion 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) ?) *)
904lemma 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
914lemma 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
930whd in match (sw_rem ??);
931whd in match (switch_removal ??);
932check eq_ind
933
934
935
936whd 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
939whd in match (bindIO ??????);
940cases cond_val
941[ 1: | 2: #sz' #n' | 3: #fl | 4: #rg | 5: #ptr ]
942[ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ]
943normalize 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
952theorem 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
Note: See TracBrowser for help on using the repository browser.