Changeset 2076


Ignore:
Timestamp:
Jun 14, 2012, 10:30:21 AM (5 years ago)
Author:
garnier
Message:

First steps towards a simulation proof for switch removal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2016 r2076  
    22include "Clight/fresh.ma".
    33include "basics/lists/list.ma".
    4 
    5 (* This file implements transformation of switches to linear, nested sequences of
     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
    616 * if/then/else. The implementation roughly follows the lines of the prototype.
    717 * /!\ We assume that the program is well-typed (the type of the evaluated
    818 * 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   ----------------------------------------------------------------------------*)
    965
    1066(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
     
    54110].
    55111
     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.  *)
    56122let rec add_starting_lbl_list
    57123  (l : labeled_statements) 
     
    74140] qed.
    75141
     142(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
    76143let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
    77144match st with
     
    91158].
    92159
     160(* Converting breaks preserves switch-freeness. *)
    93161lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label).
    94162#s elim s //
     
    101169] qed.
    102170
    103 (* We assume that the expression e is consistely typed w.r.t. the switch branches *)
     171(* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
    104172let rec produce_cond
    105173  (e : expr)
     
    137205] qed.
    138206
     207(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
    139208let rec produce_cond2
    140209  (e : expr)
     
    169238     | 2: elim sub_statement // ]
    170239] qed.     
    171          
    172 
    173240
    174241(* takes an expression, a list of switch-free cases and a freshgen and returns a
     
    189256let rec switch_removal
    190257  (st : statement)
    191   (vars : list (ident × type))
    192258  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
    193259match st return λs.s = st → ? with
    194 [ Sskip       ⇒ λEq. 〈«st,?», vars, uv〉
    195 | Sassign _ _ ⇒ λEq. 〈«st,?», vars, uv〉
    196 | Scall _ _ _ ⇒ λEq. 〈«st,?», vars, uv〉
     260[ Sskip       ⇒ λEq. 〈«st,?», [ ], uv〉
     261| Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
     262| Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
    197263| Ssequence s1 s2 ⇒ λEq.
    198   let 〈s1', vars1, uv'〉  ≝ switch_removal s1 vars uv in
    199   let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in
    200   〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉
     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''〉
    201267| Sifthenelse e s1 s2 ⇒ λEq.
    202   let 〈s1', vars1, uv'〉  ≝ switch_removal s1 vars uv in
    203   let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in
    204   〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉
     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''〉
    205271| Swhile e body ⇒ λEq.
    206   let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
     272  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    207273  〈«Swhile e (pi1 … body'),?», vars', uv'〉
    208274| Sdowhile e body ⇒ λEq.
    209   let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
     275  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    210276  〈«Sdowhile e (pi1 … body'),?», vars', uv'〉
    211277| Sfor s1 e s2 s3 ⇒ λEq.
    212   let 〈s1', vars1, uv'〉   ≝ switch_removal s1 vars uv in
    213   let 〈s2', vars2, uv''〉  ≝ switch_removal s2 vars1 uv' in
    214   let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 vars2 uv'' in 
    215   〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars3, uv'''〉 
     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'''〉
    216282| Sbreak ⇒ λEq.
    217   〈«st,?», vars, uv〉
     283  〈«st,?», [ ], uv〉
    218284| Scontinue ⇒ λEq.
    219   〈«st,?», vars, uv〉
     285  〈«st,?», [ ], uv〉
    220286| Sreturn _ ⇒ λEq.
    221   〈«st,?», vars, uv〉
     287  〈«st,?», [ ], uv〉
    222288| Sswitch e branches ⇒ λEq.
    223    let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches vars uv in
     289   let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in
    224290   match sf_branches with
    225291   [ mk_Sig branches' H ⇒
     
    231297   ]
    232298| Slabel label body ⇒ λEq.
    233   let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
     299  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    234300  〈«Slabel label (pi1 … body'), ?», vars', uv'〉
    235301| Sgoto _ ⇒ λEq.
    236   〈«st, ?», vars, uv〉
     302  〈«st, ?», [ ], uv〉
    237303| Scost cost body ⇒ λEq.
    238   let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
     304  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    239305  〈«Scost cost (pi1 … body'),?», vars', uv'〉
    240306] (refl ? st)
     
    242308and switch_removal_branches
    243309  (l : labeled_statements)
    244   (vars : list (ident × type))
    245310  (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝
    246311match l with
    247312[ LSdefault st ⇒
    248   let 〈st, vars',  uv'〉 ≝ switch_removal st vars uv in
     313  let 〈st, vars',  uv'〉 ≝ switch_removal st uv in
    249314  〈«LSdefault (pi1 … st), ?», vars', uv'〉
    250315| LScase sz int st tl =>
    251   let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl vars uv in
    252   let 〈st', vars'', uv''〉     ≝ switch_removal st vars' uv' in
    253   〈«LScase sz int st' (pi1 … tl_result), ?», vars'', uv''〉
     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''〉
    254319].
    255320try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try //
     
    261326] qed.
    262327
     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
    263454let rec program_switch_removal (p : clight_program) : clight_program ≝
    264  let uv         ≝ universe_for_program p in
     455 let uv         ≝ universe_for_program_deep p in
    265456 let prog_funcs ≝ prog_funct ?? p in
    266457 let 〈sf_funcs, final_uv〉 ≝
    267458  foldr ?? (λcl_fundef.λacc.
    268     let 〈fundefs, uv1〉    ≝ acc in
     459    let 〈fundefs, uv1〉    ≝ acc in   
    269460    let 〈fun_id, fun_def〉 ≝ cl_fundef in
    270     match fun_def with
    271     [ CL_Internal func ⇒
    272       let 〈body', fun_vars, uv2〉 ≝ switch_removal (fn_body func) (fn_vars func) uv1 in
    273       let new_func ≝ mk_function (fn_return func) (fn_params func) fun_vars (pi1 … body') in
    274       〈(〈fun_id, CL_Internal new_func〉 :: fundefs), uv2〉
    275     | CL_External _ _ _ ⇒
    276       〈cl_fundef :: fundefs, uv1〉
    277     ]
     461    let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in
     462    〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉
    278463   ) 〈[ ], uv〉 prog_funcs
    279464 in
     
    283468  (prog_main … p).
    284469
    285 
    286 
    287 
    288 
    289 
    290 
    291 
    292 
    293 
     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 TracChangeset for help on using the changeset viewer.