source: etc/campbell/dev-notes/2012-10-09-cost-labels-in-syntax.patch

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 114.7 KB
  • Deliverables/D2.2/8051-matita-out/src/clight/clightPrintMatita.ml

    Abandoned work on push cost labels into loop syntax.  This was meant to avoid
    putting extra skips in Cminor/RTLabs code to make the cost labelling properties
    nicer, but the Cminor skips are eliminated in the translation to RTLabs, so
    it wasn't necessary in the end.
    
    This was against r2385.  If applying you might need to undo the reversion of
    changeset 2353.
    
    commit b4bfef8bef285f11e41cff3829d5eaed9ef127a8
    Author: Brian Campbell <Brian.Campbell@ed.ac.uk>
    Date:   Tue Oct 9 14:58:31 2012 +0100
    
        Version of Csyntax with all loop cost labels embedded in syntax.
    
    diff --git a/Deliverables/D2.2/8051-matita-out/src/clight/clightPrintMatita.ml b/Deliverables/D2.2/8051-matita-out/src/clight/clightPrintMatita.ml
    index d3fc026..4e19f18 100644
    a b let rec print_stmt p s = 
    265265              print_stmt s1
    266266              print_stmt s2
    267267  | Swhile(_, e, s) ->
    268       fprintf p "@[<v 2>(Swhile %a@ %a)@]"
     268      fprintf p "@[<v 2>(Swhile %a@ (None ?)@ %a@ (None ?))@]"
    269269              print_expr e
    270270              print_stmt s
    271271  | Sdowhile(_, e, s) ->
    272       fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
     272      fprintf p "@[<v 2>S(dowhile %a@ (None ?)@ %a@ (None ?))@]"
    273273              print_expr e
    274274              print_stmt s
    275275  | Sfor(_, s_init, e, s_iter, s_body) ->
    276       fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
     276      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@ (None ?)@\n%a@;<0 -2>(None ?))@]"
    277277              print_stmt s_init
    278278              print_expr e
    279279              print_stmt s_iter
  • src/CHANGES

    diff --git a/src/CHANGES b/src/CHANGES
    index f451b84..e8007f7 100644
    a b  
    8787  to be used in is_final. In Matita, they don't. For RTL the information was
    8888  duplicated in the internal function record. I have done the same for ERTL too.
    8989  To be double checked with the OCaml semantics.
     90
     9102/10/2012:
     92  Cost labels following loops and for the body of each loop have been
     93  incorporated into the syntax of Swhile, etc.  This keeps them closely
     94  associated with the loop, allowing us to avoid placing skips before cost
     95  labels which breaks our labelling invariant.  The Cminor to RTLabs translation
     96  is also careful to avoid introducing skips at goto labels for the same reason,
     97  by backpatching the gotos after the rest of the code is generated.
  • src/Clight/Cexec.ma

    diff --git a/src/Clight/Cexec.ma b/src/Clight/Cexec.ma
    index 5b8cbc3..d509fa9 100644
    a b definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝ 
    330330λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
    331331[ Sskip ⇒ inl ?? (refl ??)
    332332| _ ⇒ inr ?? (nmk ? (λH.?))
    333 ]. destruct
     333]. lapply (eq_to_jmeq ??? H) -H #H destruct
    334334qed.
    335335
    336336
    match st with 
    389389          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
    390390          | _ ⇒ Wrong ??? (msg NonsenseState)
    391391          ]
    392       | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
    393       | Kdowhile a s' k' ⇒
     392      | Kwhile a lb s' lp k' ⇒ ret ? 〈E0, State f (Swhile a lb s' lp) k' e m〉
     393      | Kdowhile a lb s' lp k' ⇒
    394394          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    395395          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    396396          match b with
    397           [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
    398           | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
     397          [ true ⇒ ret ? 〈tr, State f (Sdowhile a lb s' lp) k' e m〉
     398          | false ⇒ ret ? 〈tr, State f (optional_cost lp Sskip) k' e m〉
    399399          ]
    400       | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
    401       | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
     400      | Kfor2 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 lb s' lp k') e m〉
     401      | Kfor3 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 lb s' lp) k' e m〉
    402402      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    403403      | _ ⇒ Wrong ??? (msg NonsenseState)
    404404      ]
    405405  | Scontinue ⇒
    406406      match k with
    407407      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
    408       | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
    409       | Kdowhile a s' k' ⇒
     408      | Kwhile a lb s' lp k' ⇒ ret ? 〈E0, State f (Swhile a lb s' lp) k' e m〉
     409      | Kdowhile a lb s' lp k' ⇒
    410410          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    411411          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    412412          match b with
    413           [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
    414           | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
     413          [ true ⇒ ret ? 〈tr, State f (Sdowhile a lb s' lp) k' e m〉
     414          | false ⇒ ret ? 〈tr, State f (optional_cost lp Sskip) k' e m〉
    415415          ]
    416       | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
     416      | Kfor2 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 lb s' lp k') e m〉
    417417      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
    418418      | _ ⇒ Wrong ??? (msg NonsenseState)
    419419      ]
    420420  | Sbreak ⇒
    421421      match k with
    422422      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
    423       | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (optional_cost cl Sskip) k' e m〉
    424       | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    425       | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     423      | Kwhile a lb s' lp k' ⇒ ret ? 〈E0, State f (optional_cost lp Sskip) k' e m〉
     424      | Kdowhile a lb s' lp k' ⇒ ret ? 〈E0, State f (optional_cost lp Sskip) k' e m〉
     425      | Kfor2 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f (optional_cost lp Sskip) k' e m〉
    426426      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    427427      | _ ⇒ Wrong ??? (msg NonsenseState)
    428428      ]
    match st with 
    430430      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    431431      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    432432      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
    433   | Swhile a s' cl
     433  | Swhile a lb s' lp
    434434      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    435435      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    436       ret ? 〈tr, if b then State f s' (Kwhile a s' cl k) e m
    437                       else State f (optional_cost cl Sskip) k e m〉
    438   | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
    439   | Sfor a1 a2 a3 s'
     436      ret ? 〈tr, if b then State f (optional_cost lb s') (Kwhile a lb s' lp k) e m
     437                      else State f (optional_cost lp Sskip) k e m〉
     438  | Sdowhile a lb s' lp ⇒ ret ? 〈E0, State f (optional_cost lb s') (Kdowhile a lb s' lp k) e m〉
     439  | Sfor a1 a2 a3 lb s' lp
    440440      match is_Sskip a1 with
    441441      [ inl _ ⇒
    442442          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
    443443          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
    444           ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
    445       | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
     444          ret ? 〈tr, State f (if b then optional_cost lb s' else optional_cost lp Sskip) (if b then (Kfor2 a2 a3 lb s' lp k) else k) e m〉
     445      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 lb s' lp) k) e m〉
    446446      ]
    447447  | Sreturn a_opt ⇒
    448448    match a_opt with
  • src/Clight/CexecComplete.ma

    diff --git a/src/Clight/CexecComplete.ma b/src/Clight/CexecComplete.ma
    index 337877b..38fcc98 100644
    a b theorem step_complete: ∀ge,s,tr,s'. 
    382382    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    383383    >(yields_eq ??? (bool_of_false ?? H2))
    384384    @refl
    385 | #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     385| #f #e #lb #s #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    386386    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    387387    >(yields_eq ??? (bool_of_false ?? H2))
    388388    @refl
    389 | #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     389| #f #e #lb #s #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    390390    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    391391    >(yields_eq ??? (bool_of_true ?? H2))
    392392    @refl
    393 | #f #s1 #e #s2 #cl #k #env #m #H cases H; #es1 >es1 @refl
    394 | 13,14: #f #e #s [#cl] #k #env #m @refl
    395 | #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
     393| #f #s1 #e #lb #s2 #lp #k #env #m #H cases H; #es1 >es1 @refl
     394| 13,14: #f #e #lb #s #lp #k #env #m @refl
     395| #f #s1 #e #lb #s2 #lp #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
    396396    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    397397    >(yields_eq ??? (bool_of_false ?? H2))
    398398    @refl
    399 | #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
     399| #f #s1 #e #lb #s2 #lp #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
    400400    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    401401    >(yields_eq ??? (bool_of_true ?? H2))
    402402    @refl
    403 | #f #e #s #k #env #m @refl
    404 | #f #s1 #e #s2 #s3 #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1);
     403| #f #e #lb #s #lp #k #env #m @refl
     404| #f #s1 #e #s2 #lb #s3 #lp #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1);
    405405    [ #H @False_ind @(absurd ? H nskip)
    406406    | #H whd in ⊢ (??%?); @refl ]
    407 | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     407| #f #e #s1 #lb #s2 #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    408408    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    409409    >(yields_eq ??? (bool_of_false ?? H2))
    410410    @refl
    411 | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     411| #f #e #s1 #lb #s2 #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    412412    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    413413    >(yields_eq ??? (bool_of_true ?? H2))
    414414    @refl
    415 | #f #s1 #e #s2 #s3 #k #env #m *; #es1 >es1 @refl
    416 | 22,23: #f #e #s1 #s2 #k #env #m @refl
     415| #f #s1 #e #s2 #lb #s3 #lp #k #env #m *; #es1 >es1 @refl
     416| 22,23: #f #e #s1 #lb #s2 #lp #k #env #m @refl
    417417| #f #k #env #m #H whd in ⊢ (??%?); >H @refl
    418418| #f #e #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    419419    @(dec_false ? (type_eq_dec (fn_return f) Tvoid) H1) #pf'
    theorem step_complete: ∀ge,s,tr,s'. 
    423423| #f #k #env #m cases k;
    424424    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    425425    | #s' #k' whd in ⊢ (% → ?); *;
    426     | 3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *;
    427     | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
     426    | 3,4: #e' #lb #s' #lp #k' whd in ⊢ (% → ?); *;
     427    | 5,6: #e' #s1' #lb #s2' #lp #k' whd in ⊢ (% → ?); *;
    428428    | #k' whd in ⊢ (% → ?); *;
    429429    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    430430    ]
  • src/Clight/CexecEquiv.ma

    diff --git a/src/Clight/CexecEquiv.ma b/src/Clight/CexecEquiv.ma
    index 725ebc1..501de00 100644
    a b lemma exec_step_interaction: 
    513513  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
    514514#ge #s cases s;
    515515[ #f #st #kk #e #m cases st;
    516   [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
    517   [ 4,5,7,8: @I ]
     516  [ 11,14: #a | 2,4,12,13,15: #a #b | 3,5: #a #b #c | 6,7: #a #b #c #d | 8: #a #b #c #d #e #f ]
     517  try @I
    518518  whd in ⊢ (???%);
    519519  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
    520520                    cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ]
    lemma exec_step_interaction: 
    527527  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    528528      | @I ]
    529529  | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //;
    530       | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
     530      | #z1 #z2 #z3 #z4 #z5 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
    531531  | cases kk; //;
    532   | cases kk; [ 4: #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
     532  | cases kk; [ 4: #z1 #z2 #z3 #z4 #z5 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
    533533      | *: // ]
    534534  ]
    535535| #f #args #kk #m cases f;
  • src/Clight/CexecSound.ma

    diff --git a/src/Clight/CexecSound.ma b/src/Clight/CexecSound.ma
    index dc7fce3..88ef64b 100644
    a b theorem exec_step_sound: ∀ge,st. 
    336336        //; #H whd;
    337337        @step_skip_call //;
    338338    | #s' #k' whd; //
    339     | #ex #s' #cl #k' @step_skip_or_continue_while % //;
    340     | #ex #s' #k'
     339    | #ex #lb #s' #lp #k' @step_skip_or_continue_while % //;
     340    | #ex #lb #s' #lp #k'
    341341        @res_bindIO2_OK #v #tr #Hv
    342342        letin bexpr ≝ (exec_bool_of_val v (typeof ex));
    343343        lapply (refl ? bexpr);
    theorem exec_step_sound: ∀ge,st. 
    351351            ]
    352352        | #msg #_ //;
    353353        ]
    354     | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
    355     | #ex #s1 #s2 #k' @step_skip_for3
     354    | #ex #s1 #lb #s2 #lp #k' @step_skip_or_continue_for2 % //;
     355    | #ex #s1 #lb #s2 #lp #k' @step_skip_for3
    356356    | #k' @step_skip_break_switch % //;
    357357    | #r #f' #e' #k' whd in ⊢ (?????%);
    358358        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
    theorem exec_step_sound: ∀ge,st. 
    384384    [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    385385    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    386386    ]
    387   | #ex #s' #cl
     387  | #ex #lb #s' #lp
    388388    @res_bindIO2_OK #v #tr #Hv
    389389    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
    390390    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
    theorem exec_step_sound: ∀ge,st. 
    392392    [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    393393    | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    394394    ]
    395   | #ex #s' //
    396   | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
     395  | #ex #lb #s' #lp //
     396  | #s1 #ex #s2 #lb #s3 #lp whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
    397397    [ >Hs1
    398398      @res_bindIO2_OK #v #tr #Hv
    399399      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
    theorem exec_step_sound: ∀ge,st. 
    406406    ]
    407407  | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
    408408  | whd in ⊢ (?????%); cases k; //;
    409     [ #ex #s' #cl #k' whd; @step_skip_or_continue_while %2 ; //;
    410     | #ex #s' #k' whd;
     409    [ #ex #lb #s' #lp #k' whd; @step_skip_or_continue_while %2 ; //;
     410    | #ex #lb #s' #lp #k' whd;
    411411      @res_bindIO2_OK #v #tr #Hv
    412412      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
    413413      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
    theorem exec_step_sound: ∀ge,st. 
    417417      | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
    418418        [ %2 ; // | @(bool_of … Hb) ]
    419419      ]
    420     | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
     420    | #ex #s1 #lb #s2 #lp #k' whd; @step_skip_or_continue_for2 %2 ; //
    421421    ]
    422422  | #r whd in ⊢ (?????%); cases r;
    423423    [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H
  • src/Clight/Csem.ma

    diff --git a/src/Clight/Csem.ma b/src/Clight/Csem.ma
    index 344de75..9685b53 100644
    a b inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → t 
    907907
    908908inductive cont: Type[0] :=
    909909  | Kstop: cont
    910   | Kseq: statement -> cont -> cont
     910  | Kseq: statement → cont → cont
    911911       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
    912   | Kwhile: expr -> statement → option costlabel -> cont -> cont
    913        (**r [Kwhile e s k] = after [s] in [while (e) s] *)
    914   | Kdowhile: expr -> statement -> cont -> cont
    915        (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
    916   | Kfor2: expr -> statement -> statement -> cont -> cont
    917        (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
    918   | Kfor3: expr -> statement -> statement -> cont -> cont
    919        (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
    920   | Kswitch: cont -> cont
     912  | Kwhile: expr → option costlabel → statement → option costlabel → cont → cont
     913       (**r [Kwhile e lb s lp k] = after [s] in [while (e) s] *)
     914  | Kdowhile: expr → option costlabel → statement → option costlabel → cont → cont
     915       (**r [Kdowhile e lb s lp k] = after [s] in [do s while (e)] *)
     916  | Kfor2: expr → statement → option costlabel → statement → option costlabel → cont → cont
     917       (**r [Kfor2 e2 e3 lb s lp k] = after [s] in [for(e1;e2;e3) s] *)
     918  | Kfor3: expr → statement → option costlabel → statement → option costlabel → cont → cont
     919       (**r [Kfor3 e2 e3 lb s lp k] = after [e3] in [for(e1;e2;e3) s] *)
     920  | Kswitch: cont cont
    921921       (**r catches [break] statements arising out of [switch] *)
    922   | Kcall: option (block × offset × type) -> (**r where to store result *)
    923            function ->                       (**r calling function *)
    924            env ->                            (**r local env of calling function *)
    925            cont -> cont.
     922  | Kcall: option (block × offset × type) (**r where to store result *)
     923           function                        (**r calling function *)
     924           env                             (**r local env of calling function *)
     925           cont cont.
    926926
    927927(* * Pop continuation until a call or stop *)
    928928
    929929let rec call_cont (k: cont) : cont :=
    930930  match k with
    931931  [ Kseq s k => call_cont k
    932   | Kwhile e s l k => call_cont k
    933   | Kdowhile e s k => call_cont k
    934   | Kfor2 e2 e3 s k => call_cont k
    935   | Kfor3 e2 e3 s k => call_cont k
     932  | Kwhile e _ s _ k => call_cont k
     933  | Kdowhile e _ s _ k => call_cont k
     934  | Kfor2 e2 e3 _ s _ k => call_cont k
     935  | Kfor3 e2 e3 _ s _ k => call_cont k
    936936  | Kswitch k => call_cont k
    937937  | _ => k
    938938  ].
    let rec find_label (lbl: label) (s: statement) (k: cont) 
    982982      [ Some sk => Some ? sk
    983983      | None => find_label lbl s2 k
    984984      ]
    985   | Swhile a s1 l =>
    986       find_label lbl s1 (Kwhile a s1 l k)
    987   | Sdowhile a s1 =>
    988       find_label lbl s1 (Kdowhile a s1 k)
    989   | Sfor a1 a2 a3 s1 =>
    990       match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with
     985  | Swhile a lb s1 lp =>
     986      find_label lbl s1 (Kwhile a lb s1 lp k)
     987  | Sdowhile a lb s1 lp =>
     988      find_label lbl s1 (Kdowhile a lb s1 lp k)
     989  | Sfor a1 a2 a3 lb s1 lp =>
     990      match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 lb s1 lp) k) with
    991991      [ Some sk => Some ? sk
    992992      | None =>
    993           match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
     993          match find_label lbl s1 (Kfor2 a2 a3 lb s1 lp k) with
    994994          [ Some sk => Some ? sk
    995           | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
     995          | None => find_label lbl a3 (Kfor3 a2 a3 lb s1 lp k)
    996996          ]
    997997      ]
    998998  | Sswitch e sl =>
    definition fun_typeof ≝ 
    10341034| Tcomp_ptr a ⇒ Tcomp_ptr a
    10351035].
    10361036
     1037(* For loops we may generate a cost label statement for the body / following
     1038   code if there's one present in the loop statement. *)
     1039
    10371040definition optional_cost : option costlabel → statement → statement ≝
    10381041λo,s. match o with [ Some cl ⇒ Scost cl s | None ⇒ s ].
    10391042
    inductive step (ge:genv) : state → trace → state → Prop ≝ 
    10891092      step ge (State f (Sifthenelse a s1 s2) k e m)
    10901093           tr (State f s2 k e m)
    10911094
    1092   | step_while_false: ∀f,a,s,cl,k,e,m,v,tr.
     1095  | step_while_false: ∀f,a,lb,s,lp,k,e,m,v,tr.
    10931096      eval_expr ge e m a v tr →
    10941097      is_false v (typeof a) →
    1095       step ge (State f (Swhile a s cl) k e m)
    1096            tr (State f (optional_cost cl Sskip) k e m)
    1097   | step_while_true: ∀f,a,s,cl,k,e,m,v,tr.
     1098      step ge (State f (Swhile a lb s lp) k e m)
     1099           tr (State f (optional_cost lp Sskip) k e m)
     1100  | step_while_true: ∀f,a,lb,s,lp,k,e,m,v,tr.
    10981101      eval_expr ge e m a v tr →
    10991102      is_true v (typeof a) →
    1100       step ge (State f (Swhile a s cl) k e m)
    1101            tr (State f s (Kwhile a s cl k) e m)
    1102   | step_skip_or_continue_while: ∀f,x,a,s,cl,k,e,m.
     1103      step ge (State f (Swhile a lb s lp) k e m)
     1104           tr (State f (optional_cost lb s) (Kwhile a lb s lp k) e m)
     1105  | step_skip_or_continue_while: ∀f,x,a,lb,s,lp,k,e,m.
    11031106      x = Sskip ∨ x = Scontinue →
    1104       step ge (State f x (Kwhile a s cl k) e m)
    1105            E0 (State f (Swhile a s cl) k e m)
    1106   | step_break_while: ∀f,a,s,cl,k,e,m.
    1107       step ge (State f Sbreak (Kwhile a s cl k) e m)
    1108            E0 (State f (optional_cost cl Sskip) k e m)
    1109 
    1110   | step_dowhile: ∀f,a,s,k,e,m.
    1111       step ge (State f (Sdowhile a s) k e m)
    1112         E0 (State f s (Kdowhile a s k) e m)
    1113   | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
     1107      step ge (State f x (Kwhile a lb s lp k) e m)
     1108           E0 (State f (Swhile a lb s lp) k e m)
     1109  | step_break_while: ∀f,a,lb,s,lp,k,e,m.
     1110      step ge (State f Sbreak (Kwhile a lb s lp k) e m)
     1111           E0 (State f (optional_cost lp Sskip) k e m)
     1112
     1113  | step_dowhile: ∀f,a,lb,s,lp,k,e,m.
     1114      step ge (State f (Sdowhile a lb s lp) k e m)
     1115        E0 (State f (optional_cost lb s) (Kdowhile a lb s lp k) e m)
     1116  | step_skip_or_continue_dowhile_false: ∀f,x,a,lb,s,lp,k,e,m,v,tr.
    11141117      x = Sskip ∨ x = Scontinue →
    11151118      eval_expr ge e m a v tr →
    11161119      is_false v (typeof a) →
    1117       step ge (State f x (Kdowhile a s k) e m)
    1118            tr (State f Sskip k e m)
    1119   | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
     1120      step ge (State f x (Kdowhile a lb s lp k) e m)
     1121           tr (State f (optional_cost lp Sskip) k e m)
     1122  | step_skip_or_continue_dowhile_true: ∀f,x,a,lb,s,lp,k,e,m,v,tr.
    11201123      x = Sskip ∨ x = Scontinue →
    11211124      eval_expr ge e m a v tr →
    11221125      is_true v (typeof a) →
    1123       step ge (State f x (Kdowhile a s k) e m)
    1124            tr (State f (Sdowhile a s) k e m)
    1125   | step_break_dowhile: ∀f,a,s,k,e,m.
    1126       step ge (State f Sbreak (Kdowhile a s k) e m)
    1127            E0 (State f Sskip k e m)
     1126      step ge (State f x (Kdowhile a lb s lp k) e m)
     1127           tr (State f (Sdowhile a lb s lp) k e m)
     1128  | step_break_dowhile: ∀f,a,lb,s,lp,k,e,m.
     1129      step ge (State f Sbreak (Kdowhile a lb s lp k) e m)
     1130           E0 (State f (optional_cost lp Sskip) k e m)
    11281131
    1129   | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
     1132  | step_for_start: ∀f,a1,a2,a3,lb,s,lp,k,e,m.
    11301133      a1 ≠ Sskip →
    1131       step ge (State f (Sfor a1 a2 a3 s) k e m)
    1132            E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
    1133   | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
     1134      step ge (State f (Sfor a1 a2 a3 lb s lp) k e m)
     1135           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 lb s lp) k) e m)
     1136  | step_for_false: ∀f,a2,a3,lb,s,lp,k,e,m,v,tr.
    11341137      eval_expr ge e m a2 v tr →
    11351138      is_false v (typeof a2) →
    1136       step ge (State f (Sfor Sskip a2 a3 s) k e m)
    1137            tr (State f Sskip k e m)
    1138   | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
     1139      step ge (State f (Sfor Sskip a2 a3 lb s lp) k e m)
     1140           tr (State f (optional_cost lp Sskip) k e m)
     1141  | step_for_true: ∀f,a2,a3,lb,s,lp,k,e,m,v,tr.
    11391142      eval_expr ge e m a2 v tr →
    11401143      is_true v (typeof a2) →
    1141       step ge (State f (Sfor Sskip a2 a3 s) k e m)
    1142            tr (State f s (Kfor2 a2 a3 s k) e m)
    1143   | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
     1144      step ge (State f (Sfor Sskip a2 a3 lb s lp) k e m)
     1145           tr (State f (optional_cost lb s) (Kfor2 a2 a3 lb s lp k) e m)
     1146  | step_skip_or_continue_for2: ∀f,x,a2,a3,lb,s,lp,k,e,m.
    11441147      x = Sskip ∨ x = Scontinue →
    1145       step ge (State f x (Kfor2 a2 a3 s k) e m)
    1146            E0 (State f a3 (Kfor3 a2 a3 s k) e m)
    1147   | step_break_for2: ∀f,a2,a3,s,k,e,m.
    1148       step ge (State f Sbreak (Kfor2 a2 a3 s k) e m)
    1149            E0 (State f Sskip k e m)
    1150   | step_skip_for3: ∀f,a2,a3,s,k,e,m.
    1151       step ge (State f Sskip (Kfor3 a2 a3 s k) e m)
    1152            E0 (State f (Sfor Sskip a2 a3 s) k e m)
     1148      step ge (State f x (Kfor2 a2 a3 lb s lp k) e m)
     1149           E0 (State f a3 (Kfor3 a2 a3 lb s lp k) e m)
     1150  | step_break_for2: ∀f,a2,a3,lb,s,lp,k,e,m.
     1151      step ge (State f Sbreak (Kfor2 a2 a3 lb s lp k) e m)
     1152           E0 (State f (optional_cost lp Sskip) k e m)
     1153  | step_skip_for3: ∀f,a2,a3,lb,s,lp,k,e,m.
     1154      step ge (State f Sskip (Kfor3 a2 a3 lb s lp k) e m)
     1155           E0 (State f (Sfor Sskip a2 a3 lb s lp) k e m)
    11531156
    11541157  | step_return_0: ∀f,k,e,m.
    11551158      fn_return f = Tvoid →
  • src/Clight/Csyntax.ma

    diff --git a/src/Clight/Csyntax.ma b/src/Clight/Csyntax.ma
    index a96a722..4bc2925 100644
    a b definition typeof : expr → type ≝ λe. 
    183183(* * Clight statements include all C statements.
    184184  Only structured forms of [switch] are supported; moreover,
    185185  the [default] case must occur last.  Blocks and block-scoped declarations
    186   are not supported. *)
     186  are not supported.
     187 
     188  The loops have optional cost labels for the body of the loop and for after
     189  the loop is complete (usually denoted lb and lp respectively in definitions).
     190  By closely associating the cost labels with the syntax it is easier to write
     191  the code to compile loops without introducing extraneous statements between
     192  control flow and cost labels.
     193   *)
    187194
    188195definition label ≝ ident.
    189196
    inductive statement : Type[0] ≝ 
    193200  | Scall: option expr → expr → list expr → statement (**r function call *)
    194201  | Ssequence : statement → statement → statement  (**r sequence *)
    195202  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
    196   | Swhile : expr → statement → option costlabel → statement   (**r [while] loop *)
    197   | Sdowhile : expr → statement → statement (**r [do] loop *)
    198   | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
     203  | Swhile : expr → option costlabel → statement → option costlabel → statement   (**r [while] loop *)
     204  | Sdowhile : expr → option costlabel → statement → option costlabel → statement (**r [do] loop *)
     205  | Sfor: statement → expr → statement → option costlabel → statement → option costlabel → statement (**r [for] loop *)
    199206  | Sbreak : statement                      (**r [break] statement *)
    200207  | Scontinue : statement                   (**r [continue] statement *)
    201208  | Sreturn : option expr → statement       (**r [return] statement *)
    let rec statement_ind2 
    225232  (Sca:∀eo,e,args. P (Scall eo e args))
    226233  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    227234  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    228   (Swh:∀e,s,l. P s → P (Swhile e s l))
    229   (Sdo:∀e,s. P s → P (Sdowhile e s))
    230   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     235  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
     236  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
     237  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
    231238  (Sbr:P Sbreak)
    232239  (Sco:P Scontinue)
    233240  (Sre:∀eo. P (Sreturn eo))
    match s with 
    248255| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    249256    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    250257    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    251 | Swhile e s cl ⇒ Swh e s cl
     258| Swhile e lb s lp ⇒ Swh e s lb lp
    252259    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    253 | Sdowhile e s ⇒ Sdo e s
     260| Sdowhile e lb s lp ⇒ Sdo e s lb lp
    254261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    255 | Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
     262| Sfor s1 e s2 lb s3 lp ⇒ Sfo s1 e s2 s3 lb lp
    256263    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    257264    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    258265    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
    and labeled_statements_ind2 
    274281  (Sca:∀eo,e,args. P (Scall eo e args))
    275282  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    276283  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    277   (Swh:∀e,s,l. P s → P (Swhile e s l))
    278   (Sdo:∀e,s. P s → P (Sdowhile e s))
    279   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     284  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
     285  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
     286  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
    280287  (Sbr:P Sbreak)
    281288  (Sco:P Scontinue)
    282289  (Sre:∀eo. P (Sreturn eo))
  • src/Clight/SimplifyCasts.ma

    diff --git a/src/Clight/SimplifyCasts.ma b/src/Clight/SimplifyCasts.ma
    index 16aff67..d9b69fc 100644
    a b match s with 
    19811981| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
    19821982| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
    19831983| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
    1984 | Swhile e s1 cl ⇒ Swhile (simplify_e e) (simplify_statement s1) cl (* TODO: try to reduce size of e *)
    1985 | Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
    1986 | Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
     1984| Swhile e lb s1 lp ⇒ Swhile (simplify_e e) lb (simplify_statement s1) lp (* TODO: try to reduce size of e *)
     1985| Sdowhile e lb s1 lp ⇒ Sdowhile (simplify_e e) lb (simplify_statement s1) lp (* TODO: try to reduce size of e *)
     1986| Sfor s1 e s2 lb s3 lp ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) lb (simplify_statement s3) lp (* TODO: reduce size of e *)
    19871987| Sbreak ⇒ Sbreak
    19881988| Scontinue ⇒ Scontinue
    19891989| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
    definition simplify_program : clight_program → clight_program ≝ 
    20142014inductive cont_cast : cont → cont → Prop ≝
    20152015| cc_stop : cont_cast Kstop Kstop
    20162016| cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
    2017 | cc_while : ∀e,s,cl,k,k'.
     2017| cc_while : ∀e,lb,s,lp,k,k'.
    20182018    cont_cast k k' →
    2019     cont_cast (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k')
    2020 | cc_dowhile : ∀e,s,k,k'.
     2019    cont_cast (Kwhile e lb s lp k) (Kwhile (simplify_e e) lb (simplify_statement s) lp k')
     2020| cc_dowhile : ∀e,lb,s,lp,k,k'.
    20212021    cont_cast k k' →
    2022     cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k')
    2023 | cc_for1 : ∀e,s1,s2,k,k'.
     2022    cont_cast (Kdowhile e lb s lp k) (Kdowhile (simplify_e e) lb (simplify_statement s) lp k')
     2023| cc_for1 : ∀e,s1,lb,s2,lp,k,k'.
    20242024    cont_cast k k' →
    2025     cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k')
    2026 | cc_for2 : ∀e,s1,s2,k,k'.
     2025    cont_cast (Kseq (Sfor Sskip e s1 lb s2 lp) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) lb (simplify_statement s2) lp) k')
     2026| cc_for2 : ∀e,s1,lb,s2,lp,k,k'.
    20272027    cont_cast k k' →
    2028     cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
    2029 | cc_for3 : ∀e,s1,s2,k,k'.
     2028    cont_cast (Kfor2 e s1 lb s2 lp k) (Kfor2 (simplify_e e) (simplify_statement s1) lb (simplify_statement s2) lp k')
     2029| cc_for3 : ∀e,s1,lb,s2,lp,k,k'.
    20302030    cont_cast k k' →
    2031     cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
     2031    cont_cast (Kfor3 e s1 lb s2 lp k) (Kfor3 (simplify_e e) (simplify_statement s1) lb (simplify_statement s2) lp k')
    20322032| cc_switch : ∀k,k'.
    20332033    cont_cast k k' → cont_cast (Kswitch k) (Kswitch k')
    20342034| cc_call : ∀r,f,en,k,k'.
    lemma cast_find_label : ∀lab,s,k,k'. 
    24232423               normalize nodelta %{kst'} /2/
    24242424          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    24252425     ] ]
    2426 | 6: #e #s #cl #Hind_s #k #k' #Hcont_cast
     2426| 6: #e #s #lb #lp #Hind_s #k #k' #Hcont_cast
    24272427     whd in match (find_label ???);
    24282428     whd in match (find_label ? (simplify_statement ?) ?);
    2429      elim (elim_IH_aux lab s (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k') ? Hind_s)
     2429     elim (elim_IH_aux lab s (Kwhile e lb s lp k) (Kwhile (simplify_e e) lb (simplify_statement s) lp k') ? Hind_s)
    24302430     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24312431          normalize nodelta %{kst'} /2/
    24322432     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    24332433     | 3: @cc_while // ]
    2434 | 7: #e #s #Hind_s #k #k' #Hcont_cast
     2434| 7: #e #s #lb #lp #Hind_s #k #k' #Hcont_cast
    24352435     whd in match (find_label ???);
    24362436     whd in match (find_label ? (simplify_statement ?) ?);
    2437      elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     2437     elim (elim_IH_aux lab s (Kdowhile e lb s lp k) (Kdowhile (simplify_e e) lb (simplify_statement s) lp k') ? Hind_s)
    24382438     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24392439          normalize nodelta %{kst'} /2/
    24402440     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    24412441     | 3: @cc_dowhile // ]
    2442 | 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
     2442| 8: #s1 #cond #s2 #s3 #lb #lp #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
    24432443     whd in match (find_label ???);
    24442444     whd in match (find_label ? (simplify_statement ?) ?);
    24452445     elim (elim_IH_aux lab s1
    2446                (Kseq (Sfor Sskip cond s2 s3) k)
    2447                (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
     2446               (Kseq (Sfor Sskip cond s2 lb s3 lp) k)
     2447               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) lb (simplify_statement s3) lp) k')
    24482448               ? Hind_s1)
    24492449     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24502450          normalize nodelta %{kst'} /2/
    24512451     | 3: @cc_for1 //
    24522452     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
    24532453          elim (elim_IH_aux lab s3
    2454                     (Kfor2 cond s2 s3 k)
    2455                     (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
     2454                    (Kfor2 cond s2 lb s3 lp k)
     2455                    (Kfor2 (simplify_e cond) (simplify_statement s2) lb (simplify_statement s3) lp k')
    24562456                      ? Hind_s3)
    24572457          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24582458                normalize nodelta %{kst'} /2/
    24592459          | 3: @cc_for2 //
    24602460          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
    24612461               elim (elim_IH_aux lab s2
    2462                          (Kfor3 cond s2 s3 k)
    2463                          (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
     2462                         (Kfor3 cond s2 lb s3 lp k)
     2463                         (Kfor3 (simplify_e cond) (simplify_statement s2) lb (simplify_statement s3) lp k')
    24642464                           ? Hind_s2)
    24652465               [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24662466                    normalize nodelta %{kst'} /2/
    inversion Hs1_sim_s1' 
    25902590     lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related
    25912591     cases stm
    25922592     (* Perform the intros for the statements*)
    2593      [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
    2594      | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
     2593     [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #lb #body #lp
     2594     | 7: #cond #lb #body #lp | 8: #init #cond #step #lb #body #lp | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
    25952595     | 14: #lab | 15: #cost #body ]
    25962596     [ 1: (* Skip *)
    25972597          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
    inversion Hs1_sim_s1' 
    26152615               %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj
    26162616               [ 1: // | 2: %1 // ]               
    26172617          | 3: (* Kwhile *)
    2618                #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2618               #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
    26192619               whd in match (ret ??) in Eq; destruct (Eq)               
    2620                %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)} @conj
     2620               %{(State (simplify_function f) (Swhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)} @conj
    26212621               [ 1: // | 2: %1 // ]
    26222622          | 4: (* Kdowhile *)
    2623                #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2623               #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
    26242624               elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond
    26252625               [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct
    26262626               | 1: cases (exec_expr ge en m cond) in Eq;
    inversion Hs1_sim_s1' 
    26352635                         | 1: * whd in match (bindIO ??????);
    26362636                                whd in match (bindIO ??????);
    26372637                                #Eq destruct (Eq)
    2638                               [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
    2639                                    @conj [ 1: // | 2: %1 // ]
    2640                               | 2: %{(State (simplify_function f) Sskip k0' en m)}
     2638                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)}
    26412639                                   @conj [ 1: // | 2: %1 // ]
     2640                              | 2: %{(State (simplify_function f) (optional_cost lp Sskip) k0' en m)}
     2641                                   @conj [ 1: // | 2: cases lp [2:#lp'] %1 // ]
    26422642                              ]
    26432643                         ]
    26442644                    ]
    26452645               ]
    26462646           | 5,6,7:
    2647                 #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2647                #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
    26482648                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
    26492649                [ 1: %{(State (simplify_function f)
    2650                               (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body))
     2650                              (Sfor Sskip (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp)
    26512651                               k0' en m)} @conj
    26522652                     [ 1: // | 2: %1 // ]
    26532653                | 2: %{(State (simplify_function f)
    26542654                              (simplify_statement step)
    2655                               (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0')
     2655                              (Kfor3 (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp k0')
    26562656                              en m)} @conj
    26572657                     [ 1: // | 2: %1 @cc_for3 // ]
    26582658                | 3: %{(State (simplify_function f)
    26592659                              (Sfor Sskip (simplify_e cond) (simplify_statement step)
    2660                               (simplify_statement body))
     2660                              lb (simplify_statement body) lp)
    26612661                              k0' en m)} @conj
    26622662                     [ 1: // | 2: %1 // ]
    26632663                ]
    inversion Hs1_sim_s1' 
    27822782                             %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj
    27832783                             [ 1: // | 2: <e0 %1 // ]
    27842784                        ] ] ] ]
    2785     | 6: #cl #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2785    | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    27862786         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
    27872787         whd in match (exec_step ??) in Heq ⊢ %;
    27882788         elim (Hsim_related cond) in Heq; *
    inversion Hs1_sim_s1' 
    27972797                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
    27982798                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
    27992799                        [ 1: destruct skip (condtrace)
    2800                              %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) cl k') en m)}
     2800                             %{(State (simplify_function f) (optional_cost lb (simplify_statement body)) (Kwhile (simplify_e cond) lb (simplify_statement body) lp k') en m)}
    28012801                             @conj
    2802                              [ 1: // | 2: <e0 %1 @cc_while // ]
     2802                             [ 1: // | 2: <e0 cases lb [2: #lb'] %1 @cc_while // ]
    28032803                        | 2: destruct skip (condtrace)
    2804                              %{(State (simplify_function f) (optional_cost cl Sskip) k' en m)} @conj
    2805                              [ 1: // | 2: <e0 cases cl [2:#cl'] %1 // ]
     2804                             %{(State (simplify_function f) (optional_cost lp Sskip) k' en m)} @conj
     2805                             [ 1: // | 2: <e0 cases lp [2:#lp'] %1 // ]
    28062806                        ] ] ] ]
    28072807    | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28082808         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
    28092809         whd in match (exec_step ??) in Heq ⊢ %;
    28102810         destruct (Heq)
    2811          %{(State (simplify_function f) (simplify_statement body)
    2812                   (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj
    2813          [ 1: // | 2: %1 @cc_dowhile // ]
     2811         %{(State (simplify_function f) (optional_cost lb (simplify_statement body))
     2812                  (Kdowhile (simplify_e cond) lb (simplify_statement body) lp k') en m)} @conj
     2813         [ 1: // | 2: cases lb [2:#lb'] %1 @cc_dowhile // ]
    28142814    | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28152815         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
    28162816         whd in match (exec_step ??) in Heq ⊢ %;
    inversion Hs1_sim_s1' 
    28202820              whd in match (ret ??) in ⊢ (% → %);
    28212821              #Eq destruct (Eq)
    28222822              %{(State (simplify_function f) (simplify_statement init)
    2823                        (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj
     2823                       (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp) k') en m)} @conj
    28242824              [ 1: // | 2: %1 @cc_for1 // ]   
    28252825         | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip
    28262826              whd in match (simplify_statement ?);
    inversion Hs1_sim_s1' 
    28372837                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
    28382838                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
    28392839                             normalize nodelta #Heq destruct (Heq)
    2840                              [ 1: %{(State (simplify_function f) (simplify_statement body)
    2841                                            (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)}
    2842                                    @conj [ 1: // | 2: %1 @cc_for2 // ]
    2843                              | 2: %{(State (simplify_function f) Sskip k' en m)} @conj
    2844                                   [ 1: // | 2: %1 // ]
     2840                             [ 1: %{(State (simplify_function f) (optional_cost lb (simplify_statement body))
     2841                                           (Kfor2 (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp k') en m)}
     2842                                   @conj [ 1: // | 2: cases lb [2:#lb'] %1 @cc_for2 // ]
     2843                             | 2: %{(State (simplify_function f) (optional_cost lp Sskip) k' en m)} @conj
     2844                                  [ 1: // | 2: cases lp [2:#lp'] %1 // ]
    28452845         ] ] ] ] ]
    28462846    | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28472847         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
    inversion Hs1_sim_s1' 
    28492849         inversion Hcont_cast in Heq; normalize nodelta
    28502850         [ 1: #Hk #Hk' #_
    28512851         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2852          | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2853          | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    2854          | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2852         | 3: #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2853         | 4: #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2854         | 5,6,7: #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28552855         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28562856         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
    28572857         #H whd in match (ret ??) in H ⊢ %;
    28582858         destruct (H)
    28592859         [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
    2860          | %{(State (simplify_function f) (optional_cost cl Sskip) k0' en m)} @conj try // cases cl [2:#cl'] %1 //
    2861          | 3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
     2860         | 2,3,5: %{(State (simplify_function f) (optional_cost lp Sskip) k0' en m)} @conj try // cases lp [2,4,6:#lp'] %1 //
     2861         | 6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
    28622862    | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28632863         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
    28642864         whd in match (exec_step ??) in Heq ⊢ %;
    28652865         inversion Hcont_cast in Heq; normalize nodelta
    28662866         [ 1: #Hk #Hk' #_
    28672867         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2868          | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2869          | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    2870          | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2868         | 3: #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2869         | 4: #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2870         | 5,6,7: #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28712871         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28722872         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
    28732873         #H whd in match (ret ??) in H ⊢ %;
    28742874         destruct (H)
    28752875         [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
    2876          | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)}
     2876         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)}
    28772877              @conj try // %1 //
    28782878         | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
    28792879              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
    inversion Hs1_sim_s1' 
    28862886                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
    28872887                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
    28882888                             normalize nodelta #Heq destruct (Heq)
    2889                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
    2890                                   @conj [ 1: // | 2: %1 // ]
    2891                              | 2: %{(State (simplify_function f) Sskip k0' en m)}
     2889                             [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)}
    28922890                                  @conj [ 1: // | 2: %1 // ]
     2891                             | 2: %{(State (simplify_function f) (optional_cost lp Sskip) k0' en m)}
     2892                                  @conj [ 1: // | 2: cases lp [2:#lp'] %1 // ]
    28932893             ] ] ] ]
    28942894         | 5: %{(State (simplify_function f) (simplify_statement step)
    2895                        (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj
     2895                       (Kfor3 (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp k0') en m)} @conj
    28962896              [ 1: // | 2: %1 @cc_for3 // ]
    28972897         ]
    28982898    | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    inversion Hs1_sim_s1' 
    30073007     inversion Hcont_cast
    30083008     [ 1: #Hk #Hk' #_
    30093009     | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    3010      | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    3011      | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    3012      | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     3010     | 3: #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     3011     | 4: #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     3012     | 5,6,7: #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    30133013     | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    30143014     | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
    30153015     normalize nodelta
  • src/Clight/addRuntime.ma

    diff --git a/src/Clight/addRuntime.ma b/src/Clight/addRuntime.ma
    index 7c69cb3..bd6f7fc 100644
    a b match s with 
    8080                   match oe with [ Some e ⇒ expr_ops e @ l | None ⇒ l ]
    8181| Ssequence s1 s2 ⇒ stmt_ops s1 @ stmt_ops s2
    8282| Sifthenelse e1 s1 s2 ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2
    83 | Swhile e1 s1  ⇒ expr_ops e1 @ stmt_ops s1
    84 | Sdowhile e1 s1 ⇒ expr_ops e1 @ stmt_ops s1
    85 | Sfor s1 e1 s2 s3 ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2 @ stmt_ops s3
     83| Swhile e1 _ s1 _ ⇒ expr_ops e1 @ stmt_ops s1
     84| Sdowhile e1 _ s1 _ ⇒ expr_ops e1 @ stmt_ops s1
     85| Sfor s1 e1 s2 _ s3 _ ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2 @ stmt_ops s3
    8686| Sreturn oe ⇒ match oe with [ Some e ⇒ expr_ops e | None ⇒ [ ] ]
    8787| Sswitch e1 ls ⇒ expr_ops e1 @ lstmt_ops ls
    8888| Slabel _ s1 ⇒ stmt_ops s1
    match s with 
    210210
    211211  (* This is particularly bad - for loops we end up duplicating the code. *)
    212212 
    213 | Swhile e1 s1
     213| Swhile e1 lb s1 lp
    214214    let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in
    215215    let 〈s1,u〉 ≝ subst_stmt s1 rs u in
    216       〈rev_prepend_stmts ls1 (Swhile e1 (append_stmts s1 ls1)), u〉
    217 | Sdowhile e1 s1
     216      〈rev_prepend_stmts ls1 (Swhile e1 lb (append_stmts s1 ls1) lp), u〉
     217| Sdowhile e1 lb s1 lp
    218218    let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in
    219219    let 〈s1,u〉 ≝ subst_stmt s1 rs u in
    220       〈Sdowhile e1 (append_stmts s1 ls1), u〉
    221 | Sfor s1 e1 s2 s3
     220      〈Sdowhile e1 lb (append_stmts s1 ls1) lp, u〉
     221| Sfor s1 e1 s2 lb s3 lp
    222222    let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in
    223223    let 〈s1,u〉 ≝ subst_stmt s1 rs u in
    224224    let 〈s2,u〉 ≝ subst_stmt s2 rs u in
    225225    let 〈s3,u〉 ≝ subst_stmt s3 rs u in
    226       〈Sfor (append_stmts s1 ls1) e1 s2 (append_stmts s3 ls1), u〉
     226      〈Sfor (append_stmts s1 ls1) e1 s2 lb (append_stmts s3 ls1) lp, u〉
    227227| Sreturn oe ⇒
    228228    match oe with
    229229    [ Some e ⇒ let 〈ls1,e,u〉 ≝ subst_expr e rs u in 〈rev_prepend_stmts ls1 (Sreturn (Some ? e)), u〉
    definition divu : universe SymbolTag → intsize → replace_op × (universe Sym 
    291291      (Ssequence
    292292        (Swhile
    293293          (Expr (Ebinop Oge (Expr (Evar x) uint) (Expr (Evar y) uint)) uint)
     294          (None ?)
    294295          (Ssequence
    295296            (Sassign (Expr (Evar x) uint) (Expr (Ebinop Osub (Expr (Evar x) uint) (Expr (Evar y) uint)) uint))
    296             (Sassign (Expr (Evar quo) uint) (Expr (Ebinop Oadd (Expr (Evar quo) uint) (Expr (Econst_int sz (repr sz 1)) uint)) uint))))
     297            (Sassign (Expr (Evar quo) uint) (Expr (Ebinop Oadd (Expr (Evar quo) uint) (Expr (Econst_int sz (repr sz 1)) uint)) uint)))
     298          (None ?) )
    297299        (Sreturn (Some ? (Expr (Evar quo) uint))))))),
    298300    u〉.
    299301       
  • src/Clight/label.ma

    diff --git a/src/Clight/label.ma b/src/Clight/label.ma
    index bbadc0e..90c8ebb 100644
    a b match e with 
    2020  ]
    2121].
    2222
     23definition is_none : ∀A:Type[0]. option A → bool ≝
     24λA,o. match o with [ None ⇒ true | Some _ ⇒ false ].
     25
    2326let rec statement_label_free (s:statement) : bool ≝
    2427match s with
    2528[ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
    2629| Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_free es
    2730| Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
    2831| Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2
    29 | Swhile e1 s1 cl ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ match cl with [ None ⇒ true | _ ⇒ false ]
    30 | Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    31 | Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3
     32| Swhile e1 lb s1 lp ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ is_none … lb ∧ is_none … lp
     33| Sdowhile e1 lb s1 lp ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ is_none … lb ∧ is_none … lp
     34| Sfor s1 e1 s2 lb s3 lp ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3 ∧ is_none … lb ∧ is_none … lp
    3235| Sreturn oe ⇒ option_map_def … expr_label_free true oe
    3336| Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_free ls
    3437| Slabel _ s1 ⇒ statement_label_free s1
    match s with 
    177180    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
    178181    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
    179182    〈Sifthenelse e s1 s2, costgen〉
    180 | Swhile e s' cl
     183| Swhile e lb s' lp
    181184    let 〈e,costgen〉 ≝ label_expr e costgen in
     185    let 〈body,costgen〉 ≝ ensure_label lb costgen in
    182186    let 〈s',costgen〉 ≝ label_statement s' costgen in
    183     let 〈s',costgen〉 ≝ add_cost_before s' costgen in
    184     let 〈after,costgen〉 ≝ ensure_label cl costgen in
    185     〈Swhile e s' (Some ? after), costgen〉
    186 | Sdowhile e s' ⇒
     187    let 〈after,costgen〉 ≝ ensure_label lp costgen in
     188    〈Swhile e (Some ? body) s' (Some ? after), costgen〉
     189| Sdowhile e lb s' lp ⇒
    187190    let 〈e,costgen〉 ≝ label_expr e costgen in
     191    let 〈body,costgen〉 ≝ ensure_label lb costgen in
    188192    let 〈s',costgen〉 ≝ label_statement s' costgen in
    189     let 〈s',costgen〉 ≝ add_cost_before s' costgen in
    190     let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
    191     〈s,costgen〉
    192 | Sfor s1 e s2 s3 ⇒
     193    let 〈after,costgen〉 ≝ ensure_label lp costgen in
     194    〈Sdowhile e (Some ? body) s' (Some ? after),costgen〉
     195| Sfor s1 e s2 lb s3 lp ⇒
    193196    let 〈e,costgen〉 ≝ label_expr e costgen in
    194197    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
    195198    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
     199    let 〈body,costgen〉 ≝ ensure_label lb costgen in
    196200    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
    197     let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
    198     let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
    199     〈s,costgen〉
     201    let 〈after,costgen〉 ≝ ensure_label lp costgen in
     202    〈Sfor s1 e s2 (Some ? body) s3 (Some ? after),costgen〉
    200203| Sbreak ⇒ 〈Sbreak,costgen〉
    201204| Scontinue ⇒ 〈Scontinue,costgen〉
    202205| Sreturn opt_e ⇒
  • src/Clight/labelSimulation.ma

    diff --git a/src/Clight/labelSimulation.ma b/src/Clight/labelSimulation.ma
    index c72ece3..f99db37 100644
    a b lemma label_exprs_ok : ∀ge,ge'. 
    257257  | /2/ ] | skip ]
    258258] qed.
    259259
     260inductive label_le : option costlabel → costlabel → Prop ≝
     261| ll_none : ∀c. label_le (None ?) c
     262| ll_some : ∀c. label_le (Some ? c) c.
    260263
    261264(* Now we move on to describe the simulation relation.  First, relate the
    262265   continuations. *)
    263266inductive cont_with_labels : cont → cont → Prop ≝
    264267| cwl_stop : cont_with_labels Kstop Kstop
    265268| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
    266 | cwl_while : ∀ue,e,us,s,cl,cs,cpost,k,k'.
     269| cwl_while : ∀ue,e,us,lb,s,lp,cs,cpost,k,k'.
    267270    cont_with_labels k k' →
    268     (cl = None ? ∨ cl = Some ? cpost) →
    269     cont_with_labels (Kwhile e s cl k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Some ? cpost) k')
    270 | cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
     271    label_le lb cs →
     272    label_le lp cpost →
     273    cont_with_labels (Kwhile e lb s lp k) (Kwhile (\fst (label_expr e ue)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost) k')
     274| cwl_dowhile : ∀ue,e,us,lb,s,lp,cs,cpost,k,k'.
    271275    cont_with_labels k k' →
    272     cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
    273 | cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
     276    label_le lb cs →
     277    label_le lp cpost →
     278    cont_with_labels (Kdowhile e lb s lp k) (Kdowhile (\fst (label_expr e ue)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost) k')
     279| cwl_for1 : ∀ue,e,us1,s1,us2,lb,s2,lp,cs,cpost,k,k'.
    274280    cont_with_labels k k' →
    275     cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
    276 | cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
    277 | cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
     281    label_le lb cs →
     282    label_le lp cpost →
     283    cont_with_labels (Kseq (Sfor Sskip e s1 lb s2 lp) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Some ? cs) (\fst (label_statement s2 us2)) (Some ? cpost)) k')
     284| cwl_for2 : ∀ue,e,us1,s1,us2,lb,s2,lp,cs,cpost,k,k'.
     285    cont_with_labels k k' →
     286    label_le lb cs →
     287    label_le lp cpost →
     288    cont_with_labels (Kfor2 e s1 lb s2 lp k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Some ? cs) (\fst (label_statement s2 us2)) (Some ? cpost) k')
     289| cwl_for3 : ∀ue,e,us1,s1,us2,lb,s2,lp,cs,cpost,k,k'.
     290    cont_with_labels k k' →
     291    label_le lb cs →
     292    label_le lp cpost →
     293    cont_with_labels (Kfor3 e s1 lb s2 lp k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Some ? cs) (\fst (label_statement s2 us2)) (Some ? cpost) k')
    278294| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
    279295| cwl_call : ∀g,r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (\fst (label_function g f)) en k')
    280296| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
    qed. 
    290306inductive state_with_labels_partial : state → state → Prop ≝
    291307| swl_state : ∀g,f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (\fst (label_function g f)) (\fst (label_statement s us)) k' e m)
    292308(* Extra matching states that we can reach that don't quite correspond to the
    293    labelling function *)
    294 | swl_whilestate : ∀g,f,ua,a,us,s,cl,cs,cpost,k,k',e,m. cont_with_labels k k' →
    295     (cl = None ? ∨ cl = Some ? cpost) →
    296     state_with_labels_partial (State f (Swhile a s cl) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us))) (Some ? cpost)) k' e m)
    297 | swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    298     state_with_labels_partial (State f (Sdowhile a s) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    299 | swl_forstate : ∀g,f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    300     state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (\fst (label_function g 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)
     309   labelling function because we've forgotten the relationship between the
     310   fresh labels *)
     311| swl_whilestate : ∀g,f,ua,a,us,lb,s,lp,cs,cpost,k,k',e,m. cont_with_labels k k' →
     312    label_le lb cs →
     313    label_le lp cpost →
     314    state_with_labels_partial (State f (Swhile a lb s lp) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost)) k' e m)
     315| swl_dowhilestate : ∀g,f,ua,a,us,lb,s,lp,cs,cpost,k,k',e,m. cont_with_labels k k' →
     316    label_le lb cs →
     317    label_le lp cpost →
     318    state_with_labels_partial (State f (Sdowhile a lb s lp) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost)) k' e m)
     319| swl_forstate : ∀g,f,ua2,a2,us3,s3,us,lb,s,lp,cs,cpost,k,k',e,m. cont_with_labels k k' →
     320    label_le lb cs →
     321    label_le lp cpost →
     322    state_with_labels_partial (State f (Sfor Sskip a2 s3 lb s lp) k e m) (State (\fst (label_function g f)) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost)) k' e m)
    301323(* and the rest *)
    302324| swl_callstate : ∀g,fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (\fst (label_fundef g fd)) args k' m)
    303325| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
    lemma labelled_not_skip : ∀s,u. 
    373395  (\fst (label_statement s u)) ≠ Sskip.
    374396* #u
    375397[ * #H cases (H (refl ??))
    376 | *: #a try #b try #c try #d try #e
     398| *: #a try #b try #c try #d try #e try #f try #g
    377399     (* Use the state-monad-like structure of the labelling function to break
    378400        it up *)
    379401     whd in match (label_statement ??);
    380402     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
    381      % #E destruct
     403     % #E lapply (eq_to_jmeq ??? E) -E #E destruct
    382404] qed.
    383405
    384406lemma labelled_is_not_skip : ∀s,u.
    lemma label_select_ls : ∀sz,i,ls,u. 
    425447  ]
    426448] qed.
    427449
     450lemma ensure_label_elim : ∀c,u. ∀P:costlabel × (universe CostTag) → Type[0].
     451  (∀c',u'. label_le c c' → P 〈c',u'〉) →
     452  P (ensure_label c u).
     453* /3/
     454qed.
     455
    428456(* Break up labelling function in one go for statements. *)
    429457lemma blindly_label : ∀u,s. ∀P:statement → Prop.
    430458match s with
    match s with 
    433461| Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3)))
    434462| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
    435463| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
    436 | Swhile e s1 cl ⇒ ∀u1,u2,cs,cpost. cl = None ? ∨ cl = Some ? cpost → P (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2))) (Some ? cpost))
    437 | Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
    438 | Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
     464| Swhile e lb s1 lp ⇒ ∀u1,u2,cs,cpost.
     465    label_le lb cs →
     466    label_le lp cpost →
     467    P (Swhile (\fst (label_expr e u1)) (Some ? cs) (\fst (label_statement s1 u2)) (Some ? cpost))
     468| Sdowhile e lb s1 lp ⇒ ∀u1,u2,cs,cpost.
     469    label_le lb cs →
     470    label_le lp cpost →
     471    P (Sdowhile (\fst (label_expr e u1)) (Some ? cs) (\fst (label_statement s1 u2)) (Some ? cpost))
     472| Sfor s1 e s2 lb s3 lp ⇒ ∀u1,u2,u3,u4,c3,c4.
     473    label_le lb c3 →
     474    label_le lp c4 →
     475    P (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Some ? c3) (\fst (label_statement s3 u4)) (Some ? c4))
    439476| Sbreak ⇒ P Sbreak
    440477| Scontinue ⇒ P Scontinue
    441478| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
    match s with 
    444481| Sgoto l ⇒ P (Sgoto l)
    445482| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
    446483] → P (\fst (label_statement s u)). 
    447 #u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
     484#u * // #A #B #C try #D try #E try #F try #G try #H whd in match (label_statement ??);
    448485@label_gen_elim #u1 //
     486[ 5,6: @ensure_label_elim #cA #uA #HA ]
    449487@label_gen_elim #u2 //
    450 [ 6: >shift_fst //
    451 | 3: @label_gen_elim #u3 >shift_fst >shift_fst
    452      cases C in E ⊢ %; /3/
    453 | *: @label_gen_elim #u3 //
    454      @label_gen_elim #u4
    455      [ @label_gen_elim #u5 >shift_fst >shift_fst //
    456      | >shift_fst >shift_fst //
    457      | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
    458      ]
     488[ 6: >shift_fst // ]
     489@label_gen_elim #u3 //
     490[ 1,2,4: @ensure_label_elim #cB #uB #HB ]
     491@label_gen_elim #u4 /2/
     492[ @label_gen_elim #u5 @ensure_label_elim #c6 #u6 #H6 >shift_fst /2/
     493| @label_gen_elim #u5 >shift_fst >shift_fst /2/
    459494] qed.
    460495
    461496(* Apply induction hypothesis in label_find_label proof below while getting
    lemma label_find_label : ∀lbl,s,k,k',u. 
    532567      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
    533568      @refl | // ] |skip ]| skip ]| skip ]
    534569  ]
    535 | #e #s0 #cl #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #CL
     570| #e #s0 #lb #lp #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #LB #LP
    536571  whd in match (find_label ?? k); normalize in match (find_label ?? k');
    537572  @(lfl_IH s0 … IH) [ /2/ ]
    538573  cases (find_label ???)
    lemma label_find_label : ∀lbl,s,k,k',u. 
    543578      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
    544579      @refl | // ]| skip ]| skip ]| skip ]
    545580  ]
    546 | #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
     581| #e #s0 #lb #lp #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #LB #LP
    547582  whd in match (find_label ?? k); normalize in match (find_label ?? k');
    548583  @(lfl_IH s0 … IH) [ /2/ ]
    549584  cases (find_label ???)
    lemma label_find_label : ∀lbl,s,k,k',u. 
    554589      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
    555590      @refl | // ]| skip ]| skip ]| skip ]
    556591  ]
    557 | #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
     592| #s1 #e #s2 #s3 #lb #lp #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4 #LB #LP
    558593  whd in match (find_label ???); normalize in match (find_label ?? k');
    559594  @(lfl_IH s1 … IH1) [ /2/ ]
    560595  cases (find_label ???)
    lapply (label_find_label lbl s (call_cont k) (call_cont k') g ?) 
    641676>FIND whd in ⊢ (% → ?); //
    642677qed.
    643678
     679lemma swl_cost_state :
     680 ∀g,f,us,s,k,k',e,m,cs.
     681 cont_with_labels k k' →
     682 state_with_labels_partial (State f (Scost cs s) k e m) (State (\fst (label_function g f)) (Scost cs (\fst (label_statement s us))) k' e m).
     683#g #f #us #s #k #k' #e #m #cs #K
     684cut (Scost cs (\fst (label_statement s us)) = \fst (label_statement (Scost cs s) us))
     685[ normalize >shift_fst % ]
     686#E >E @swl_state //
     687qed.
     688
     689lemma ffs: ∀c.
     690  None costlabel = None costlabel ∨ None costlabel = Some costlabel c.
     691/2/
     692qed.
     693
    644694
    645695(* We show the main simulation in two stages.  First, we show it for all states
    646696   in the relation *except* those for labeled_statements, then we'll show the
    lemma step_with_labels_partial : ∀ge,ge'. 
    674724      ]
    675725    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
    676726      whd in EX:(??%%); destruct /4/
    677     | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K #CL #_ #E1 #E2 #E3 destruct %{0}
     727    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct %{0}
    678728      whd in EX:(??%%); destruct whd /4/
    679     | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     729    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
    680730      cases (bindIO_inversion ??????? EX) -EX * #ve #tre * #EXe #EX
    681731      cases (bindIO_inversion ??????? EX) -EX * * #EXb #EX
    682732      normalize in EX; destruct
    lemma step_with_labels_partial : ∀ge,ge'. 
    685735        whd in ⊢ (??%?); >EXe'
    686736        whd in ⊢ (??%?); >label_expr_type >EXb
    687737        whd % /4/
    688       | %{2} whd
     738      | cases LP #E destruct [ %{1} | %{0} ] whd
    689739        whd in ⊢ (??%?); >EXe'
    690740        whd in ⊢ (??%?); >label_expr_type >EXb
    691         whd % [ <(E0_right tr) @twel_app /2/ | /4/ ]
     741        whd % [  <(E0_right tr) @twel_app /2/ | *: /4/ ]
    692742      ]
    693     | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     743    | #ue #e0 #us1 #st1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
    694744      whd in EX:(??%?); destruct
    695745      %{0} whd /4/
    696     | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     746    | #ue #e0 #us1 #st1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
    697747      whd in EX:(??%?); destruct
    698748      %{0} % /4/
    699     | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     749    | #ue #e0 #us1 #st1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
    700750      whd in EX:(??%?); destruct
    701751      %{0} % /4/
    702752    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    lemma step_with_labels_partial : ∀ge,ge'. 
    764814    whd in ⊢ (??%?); >EX1'
    765815    whd in ⊢ (??%?); >label_expr_type >EX2
    766816    whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
    767   | #a #st #cl #EX
     817  | #a #lb #st #lp #EX
    768818    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    769819    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    770820    normalize in EX; destruct
    771     @blindly_label #u1 #u2 #cs #cpost * #CL destruct
     821    @blindly_label #u1 #u2 #cs #cpost * #LB * #LP destruct
    772822    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u1) #tr1' * #EX1' #T1
    773     [ 1,2,3: %{1} | %{0} ] whd
     823    [ 1,2,5,7: %{1} | *: %{0} ] whd
    774824    whd in ⊢ (??%?); >EX1'
    775825    whd in ⊢ (??%?); >label_expr_type >EX2
    776     whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) ] /5 by twel_new, swl_partial, swl_state, cwl_while, twel_app, or_introl, or_intror/
    777   | #a #st #EX
     826    whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) @twel_app /2/ ]
     827     (* faster than /4 by _/ but still not pleasant *)
     828     try assumption try @twel_new %
     829     try ( @swl_cost_state @cwl_while // )
     830     try ( @swl_state @cwl_while // )
     831     @swl_state /2/
     832  | #a #lb #st #lp #EX
    778833    normalize in EX; destruct
    779     whd in match (label_statement ??); @label_gen_elim #u1
    780     @label_gen_elim #u2
    781     whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
    782     whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
    783     %{2} % /4/
    784   | #st1 #a #st2 #st #EX
     834    @blindly_label #u1 #u2 #cs #cpost * #LB #LP destruct
     835    [ %{1} | %{0} ] whd % /5/
     836  | #st1 #a #st2 #lb #st #lp #EX
    785837    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
    786838    whd in EX:(??%?); >Eskip in EX; #EX
    787     whd in match (label_statement ??); @label_gen_elim #u1
    788     @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
    789     whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
    790     whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
     839    @blindly_label #u1 #u2 #u3 #u4 #c3 #c4 #LB #LP
    791840    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    792841      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    793842      normalize in EX; destruct
    794       cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    795       [ %{2} | %{3} ] whd
     843      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u2) #tr1' * #EX1' #T1
     844      cases LB #LB cases LP #LP destruct
     845      [ 1,2,5,7: %{1} | 3,4,6,8: %{0} ] whd
    796846      whd in ⊢ (??%?); >EX1'
    797847      whd in ⊢ (??%?); >label_expr_type >EX2
    798       whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /4/
     848      whd in ⊢ (??%?); % [ 1,3,5,7: <(E0_right tr) ]
     849      /5 by twel_new, swl_partial, swl_state, cwl_for2, twel_app, or_introl, or_intror, swl_cost_state/
    799850    | whd in EX:(??%%); destruct
    800       %{1} whd
     851      %{0} whd
    801852      whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
    802       >Eskip' whd in ⊢ (??%?); % /4/
     853      >Eskip' whd in ⊢ (??%?); whd % /4/
    803854    ]
    804855  | #EX inversion KL
    805856    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    806857    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    807     | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    808     | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    809     | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    810     | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    811     | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     858    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     859    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     860    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     861    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     862    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    812863    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    813864    | #ux #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    814865    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    815866    ]
    816867    whd in match (label_statement ??);
    817     [ 1,3,7,8: %{0} % /3/
    818     | 2,5: %{1} whd % /3/
    819     | 4,6: %{2} whd % /3/
     868    [ 1,3,5,7,9,10,11,12,13,15,17,18,19: %{0} % /3/
     869    | 2,4,6,8,14,16: %{1} whd % /3/
    820870    ]
    821871  | #EX inversion KL
    822872    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    823873    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    824     | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    825     | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    826     | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    827     | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    828     | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     874    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     875    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     876    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     877    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     878    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    829879    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    830880    | #g #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    831881    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    832882    ]
    833883    whd in match (label_statement ??);
    834     [ 1,2,3,6,7,8: %{0} % /4/
    835     | 5: %{1} % /4/
    836     | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     884    [ 6,7,8,9:
     885      cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    837886      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    838887      normalize in EX; destruct
    839888      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
    840       [ %{0} | %{2} ] whd
     889      [ 1,3,4,5,7,8: %{0} | *: %{1} ] whd
    841890      whd in ⊢ (??%?); >EX1'
    842891      whd in ⊢ (??%?); >label_expr_type >EX2
    843       whd in ⊢ (??%?); % [ 3: <(E0_right tr) ] /3/
     892      whd in ⊢ (??%?); % [ 13,15: <(E0_right tr) ] /4/
     893    | *: %{0} whd % /5 by swl_partial, swl_state, swl_whilestate, cwl_for3, or_introl, or_intror/
    844894    ]
    845895  | * [2: #a ] #EX
    846896    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
    lemma step_with_labels_partial : ∀ge,ge'. 
    867917    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    868918    cases v1 in EX1 EX;
    869919    [ 2: #sz #i #EX1 #EX
    870     | *: normalize #A #B try #C destruct
     920    | *: [ 2,4: #x ] #EX1 #EX whd in EX:(??%%); destruct
    871921    ]
    872922    whd in EX:(??%%); destruct
    873923    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    lemma step_with_labels_partial : ∀ge,ge'. 
    896946  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
    897947    %{0} % /3/
    898948  ]
    899 | #u0 #f #ua #a #us #s #cl #cs #cpost #k #k' #e #m #K * #CL #EX
     949| #u0 #f #ua #a #us #lb #s #lp #cs #cpost #k #k' #e #m #K * #LB * #LP #EX
    900950  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    901951  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    902952  whd in EX:(??%%); destruct
    903953  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
    904   [ 4: %{0} | 1,2,3: %{1} ] whd
     954  [ 4,5,7,8: %{0} | *: %{1} ] whd
    905955  whd in ⊢ (??%?); >EX1'
    906956  whd in ⊢ (??%?); >label_expr_type >EX2
    907   whd % [ 1,3,5,7: <(E0_right tr) ] /5/
    908 | #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     957  whd % [ 9,11,13,15: <(E0_right tr) ] /5/
     958| #u0 #f #ua #a #us #lb #s #lp #cs #cpost #k #k' #e #m #K * #LB * #LP #EX
    909959  whd in EX:(??%%); destruct
    910   %{1} % /4/
    911 | #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
     960  [ 1,2: %{1} | *: %{0} ] % /5/
     961| #u0 #f #ua2 #a2 #us3 #s3 #us #lb #s #lp #cs #cpost #k #k' #e #m #K * #LB * #LP #EX
    912962  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    913963  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    914964  whd in EX:(??%%); destruct
    915965  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
    916   [ %{1} | %{2} ] whd
     966  [ 1,2,3,6: %{1} | *: %{0} ] whd
    917967  whd in ⊢ (??%?); >EX1'
    918968  whd in ⊢ (??%?); >label_expr_type >EX2
    919   % [1,3: <(E0_right tr) ] /4/
     969  % [ 1,3,5,7: <(E0_right tr) ] try @swl_partial /5/
    920970| #u0 *
    921971  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
    922972    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
    lemma step_with_labels_partial : ∀ge,ge'. 
    948998      whd in EX:(??%%); destruct
    949999      %{0} whd whd in ⊢ (??%?); >EX1 % /3/
    9501000    ]
    951   | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
     1001  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O try #P try #Q try #R
    9521002       destruct whd in EX:(??%?); destruct
    9531003  ]
    9541004| #r #EX whd in EX:(??%%); destruct
    lemma exec_step_interaction: 
    9901040  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
    9911041#ge #s cases s
    9921042[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
    993   [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
     1043  [ 11,14: #a | 2,4,12,13,15: #a #b | 3,5: #a #b #c | 6,7: #a #b #c #d | 8: #a #b #c #d #e #f ]
    9941044  whd in ⊢ (??%? → ?);
    995   [ 4,5,7,8: #EX destruct ]
     1045  [ 4,6,7,11: #EX destruct ]
    9961046  [ cases a
    9971047    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
    9981048    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
    lemma exec_step_interaction: 
    10061056  | 6,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
    10071057  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
    10081058  | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
    1009     | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
    1010     | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
    1011   | cases kk normalize #A try #B try #C try #D try #E destruct
    1012   | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
    1013     | *: normalize #A try #B try #C try #D try #E destruct
     1059    | 2,3,5,6,7: normalize #A #B try #C try #D try #E try #F try #G destruct
     1060    | #z1 #z2 #z3 #z4 #z5 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
     1061  | cases kk normalize #A try #B try #C try #D try #E try #F try #G destruct
     1062  | cases kk [ 4: #z1 #z2 #z3 #z4 #z5 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
     1063    | *: normalize #A try #B try #C try #D try #E try #F try #G destruct
    10141064    ]
    10151065  ]
    10161066| #f #args #kk #m #o #k cases f
    lemma exec_step_interaction: 
    10271077    | 8: #x1 #x2 #x3 #x4 cases x1
    10281078      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
    10291079          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
    1030     | *: normalize #A try #B try #C try #D try #E destruct ]
     1080    | *: normalize #A try #B try #C try #D try #E try #F try #G destruct ]
    10311081| #r #o #k #EX whd in EX:(??%?); destruct
    10321082] qed.
    10331083
    lemma state_with_labels_call : ∀f,a,k,m,s1. 
    10371087#f #a #k #m #s1 #S inversion S
    10381088[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
    10391089  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
    1040   | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct
    1041   | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
    1042   | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
     1090  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 destruct
     1091  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
     1092  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H66 #H67 destruct
    10431093  | #u0 #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
    10441094  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
    10451095  | #H72 #H73 #H74 #H75 destruct
  • src/Clight/switchRemoval.ma

    diff --git a/src/Clight/switchRemoval.ma b/src/Clight/switchRemoval.ma
    index 89070e4..266949d 100755
    a b match st with 
    7676| Scall _ _ _ ⇒ True
    7777| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    7878| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    79 | Swhile e body _ ⇒ switch_free body
    80 | Sdowhile e body ⇒ switch_free body
    81 | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
     79| Swhile e _ body _ ⇒ switch_free body
     80| Sdowhile e _ body _ ⇒ switch_free body
     81| Sfor s1 _ s2 _ s3 _ ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
    8282| Sbreak ⇒ True
    8383| Scontinue ⇒ True
    8484| Sreturn _ ⇒ True
    match st with 
    122122  Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
    123123| Sifthenelse e iftrue iffalse ⇒
    124124  Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
    125 | Sfor init e update body
    126   Sfor (convert_break_to_goto init lab) e update body
     125| Sfor init e update lb body lp
     126  Sfor (convert_break_to_goto init lab) e update lb body lp
    127127| Slabel l body ⇒
    128128  Slabel l (convert_break_to_goto body lab)
    129129| Scost cost body ⇒
    lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_b 
    136136#s elim s //
    137137[ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
    138138| 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
    139 | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
     139| 3: #s1 #e #s2 #lb #s3 #lp #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
    140140     try @conj try @conj /3/
    141141| 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
    142142| 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
    match st with 
    247247  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
    248248  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    249249  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
    250 | Swhile e body cl
     250| Swhile e lb body lp
    251251  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    252   ret 〈Swhile e body' cl, acc, fvs', u'〉
    253 | Sdowhile e body
     252  ret 〈Swhile e lb body' lp, acc, fvs', u'〉
     253| Sdowhile e lb body lp
    254254  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    255   ret 〈Sdowhile e body', acc, fvs', u'〉
    256 | Sfor s1 e s2 s3
     255  ret 〈Sdowhile e lb body' lp, acc, fvs', u'〉
     256| Sfor s1 e s2 lb s3 lp
    257257  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
    258258  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    259259  do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
    260   ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
     260  ret 〈Sfor s1' e s2' lb s3' lp, acc1 @ acc2 @ acc3, fvs''', u'''〉
    261261| Sbreak ⇒
    262262  ret 〈st, [ ], fvs, u〉
    263263| Scontinue ⇒
    match st with 
    316316  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
    317317  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    318318  〈fvs @ fvs', u''〉
    319 | Swhile e body cl
     319| Swhile e _ body _
    320320  mk_fresh_variables body u
    321 | Sdowhile e body
     321| Sdowhile e _ body _
    322322  mk_fresh_variables body u
    323 | Sfor s1 e s2 s3
     323| Sfor s1 e s2 _ s3 _
    324324  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
    325325  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    326326  let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
    let rec statement_indT 
    365365  (Sca:∀eo,e,args. P (Scall eo e args))
    366366  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    367367  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    368   (Swh:∀e,s,cl. P s → P (Swhile e s cl))
    369   (Sdo:∀e,s. P s → P (Sdowhile e s))
    370   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     368  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
     369  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
     370  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
    371371  (Sbr:P Sbreak)
    372372  (Sco:P Scontinue)
    373373  (Sre:∀eo. P (Sreturn eo))
    match s with 
    388388| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    389389    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    390390    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    391 | Swhile e s cl ⇒ Swh e s cl
     391| Swhile e lb s lp ⇒ Swh e s lb lp
    392392    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    393 | Sdowhile e s ⇒ Sdo e s
     393| Sdowhile e lb s lp ⇒ Sdo e s lb lp
    394394    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    395 | Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
     395| Sfor s1 e s2 lb s3 lp ⇒ Sfo s1 e s2 s3 lb lp
    396396    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    397397    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    398398    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
    and labeled_statements_indT 
    414414  (Sca:∀eo,e,args. P (Scall eo e args))
    415415  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    416416  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    417   (Swh:∀e,s,cl. P s → P (Swhile e s cl))
    418   (Sdo:∀e,s. P s → P (Sdowhile e s))
    419   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     417  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
     418  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
     419  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
    420420  (Sbr:P Sbreak)
    421421  (Sco:P Scontinue)
    422422  (Sre:∀eo. P (Sreturn eo))
    lemma switch_removal_ok : 
    470470         (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
    471471         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    472472         (ret_u statement s2')))} % try //
    473 | 6: #e #s #cl #H #u0 #u1 #post normalize
     473| 6: #e #s #lb #lp #H #u0 #u1 #post normalize
    474474     elim (H u0 u1 post) #s1' * normalize
    475475     cases (mk_fresh_variables s u0) #fvs #u'
    476476     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    477      %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
     477     %{(mk_swret statement (Swhile e lb (ret_st statement s1') lp) (ret_acc statement s1')
    478478        (ret_fvs statement s1') (ret_u statement s1'))} % try //
    479 | 7: #e #s #H #u0 #u1 #post normalize
     479| 7: #e #s #lb #lp #H #u0 #u1 #post normalize
    480480     elim (H u0 u1 post) #s1' * normalize
    481481     cases (mk_fresh_variables s u0) #fvs #u'
    482482     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    483      %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
     483     %{(mk_swret statement (Sdowhile e lb (ret_st statement s1') lp) (ret_acc statement s1')
    484484        (ret_fvs statement s1') (ret_u statement s1'))} % try //
    485 | 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
     485| 8: #s1 #e #s2 #s3 #lb #lp #H1 #H2 #H3 #u0 #u1 #post normalize
    486486     elim (H1 u0 u1
    487487                (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
    488488                (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
    lemma switch_removal_ok : 
    497497     >associative_append >associative_append >Heq1 normalize >Heq1_fvs
    498498     >Heq2 normalize >Heq2_fvs >Heq3 normalize
    499499     %{(mk_swret statement
    500         (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
     500        (Sfor (ret_st statement s1') e (ret_st statement s2') lb (ret_st statement s3') lp)
    501501        (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
    502502        (ret_fvs statement s3') (ret_u statement s3'))} % try //
    503503| 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
    match s with 
    626626  max_id (max_of_statement s1) (max_of_statement s2)
    627627| Sifthenelse e s1 s2 ⇒
    628628  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
    629 | Swhile e body _ ⇒
     629| Swhile e _ body _ ⇒
    630630  max_id (max_of_expr e) (max_of_statement body)
    631 | Sdowhile e body
     631| Sdowhile e _ body _
    632632  max_id (max_of_expr e) (max_of_statement body)
    633 | Sfor init test incr body
     633| Sfor init test incr _ body _
    634634  max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
    635635| Sbreak ⇒ least_identifier
    636636| Scontinue ⇒ least_identifier
    match s1 with 
    710710  ]
    711711| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
    712712| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
    713 | Swhile e sub _ ⇒ Q e ∧ P sub
    714 | Sdowhile e sub ⇒ Q e ∧ P sub
    715 | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
     713| Swhile e _ sub _ ⇒ Q e ∧ P sub
     714| Sdowhile e _ sub _ ⇒ Q e ∧ P sub
     715| Sfor sub1 cond sub2 _ sub3 _ ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
    716716| Sbreak ⇒ True
    717717| Scontinue ⇒ True
    718718| Sreturn r ⇒
    inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝ 
    14141414    switch_cont_sim fvs k k' →
    14151415    switch_removal s fvs u = Some ? result →
    14161416    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
    1417 | swc_while : ∀fvs,e,s,cl,k,k',u,result.
    1418     fresh_for_statement (Swhile e s cl) u →
     1417| swc_while : ∀fvs,e,lb,s,lp,k,k',u,result.
     1418    fresh_for_statement (Swhile e lb s lp) u →
    14191419    switch_cont_sim fvs k k' →
    14201420    switch_removal s fvs u = Some ? result →
    1421     switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
    1422 | swc_dowhile : ∀fvs,e,s,k,k',u,result.
    1423     fresh_for_statement (Sdowhile e s) u →
     1421    switch_cont_sim fvs (Kwhile e lb s lp k) (Kwhile e lb (ret_st ? result) lp k')
     1422| swc_dowhile : ∀fvs,e,lb,s,lp,k,k',u,result.
     1423    fresh_for_statement (Sdowhile e lb s lp) u →
    14241424    switch_cont_sim fvs k k' →
    14251425    switch_removal s fvs u = Some ? result →
    1426     switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
    1427 | swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
    1428     fresh_for_statement (Sfor Sskip e s1 s2) u →
     1426    switch_cont_sim fvs (Kdowhile e lb s lp k) (Kdowhile e lb (ret_st ? result) lp k')
     1427| swc_for1 : ∀fvs,e,s1,lb,s2,lp,k,k',u,result.
     1428    fresh_for_statement (Sfor Sskip e s1 lb s2 lp) u →
    14291429    switch_cont_sim fvs k k' →
    1430     switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
    1431     switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
    1432 | swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
    1433     fresh_for_statement (Sfor Sskip e s1 s2) u →
     1430    switch_removal (Sfor Sskip e s1 lb s2 lp) fvs u = Some ? result →
     1431    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 lb s2 lp) k) (Kseq (ret_st ? result) k')
     1432| swc_for2 : ∀fvs,e,s1,lb,s2,lp,k,k',u,result1,result2.
     1433    fresh_for_statement (Sfor Sskip e s1 lb s2 lp) u →
    14341434    switch_cont_sim fvs k k' →
    14351435    switch_removal s1 fvs u = Some ? result1 →
    14361436    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
    1437     switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
    1438 | swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
    1439     fresh_for_statement (Sfor Sskip e s1 s2) u →
     1437    switch_cont_sim fvs (Kfor2 e s1 lb s2 lp k) (Kfor2 e (ret_st ? result1) lb (ret_st ? result2) lp k')
     1438| swc_for3 : ∀fvs,e,s1,lb,s2,lp,k,k',u,result1,result2.
     1439    fresh_for_statement (Sfor Sskip e s1 lb s2 lp) u →
    14401440    switch_cont_sim fvs k k' →
    14411441    switch_removal s1 fvs u = Some ? result1 →
    14421442    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
    1443     switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
     1443    switch_cont_sim fvs (Kfor3 e s1 lb s2 lp k) (Kfor3 e (ret_st ? result1) lb (ret_st ? result2) lp k')
    14441444| swc_switch : ∀fvs,k,k'.
    14451445    switch_cont_sim fvs k k' →
    14461446    switch_cont_sim fvs (Kswitch k) (Kswitch k')
  • src/Clight/test/factorial.c.ma

    diff --git a/src/Clight/test/factorial.c.ma b/src/Clight/test/factorial.c.ma
    index fb16992..8a0d78d 100644
    a b definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    2424              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2525              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2626              (Tint I32 Signed  )))
     27          (None ?)
    2728          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    2829            (Expr (Ebinop Omul
    2930              (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    3031              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
    3132              (Tint I32 Signed  )))
    32         )
     33        (None ?))
    3334        (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    3435                              (Tint I32 Signed  )))))))
    3536     
  • src/Clight/test/insertsort.c.ma

    diff --git a/src/Clight/test/insertsort.c.ma b/src/Clight/test/insertsort.c.ma
    index 0f0c002..432f65a 100644
    a b definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    121121      (Ssequence
    122122      (Swhile (Expr (Evar (ident_of_nat 2))
    123123                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     124        (None ?)
    124125        (Ssequence
    125126        (Sassign (Expr (Evar (ident_of_nat 15))
    126127                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    141142          (Expr (Eaddrof
    142143            (Expr (Evar (ident_of_nat 16))
    143144              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    144             (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]))))
     145            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])))
     146        (None ?))
    145147      (Sassign (Expr (Ederef
    146148                 (Expr (Evar (ident_of_nat 17))
    147149                   (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
    definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    172174      (Ssequence
    173175      (Swhile (Expr (Evar (ident_of_nat 20))
    174176                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     177        (None ?)
    175178        (Ssequence
    176179        (Scall (None expr) (Expr (Evar (ident_of_nat 18))
    177180                             (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid))
    definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    186189                          (Expr (Evar (ident_of_nat 20))
    187190                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    188191                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    189             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))))
     192            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     193        (None ?))
    190194      (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    191195                            (Tint I32 Signed  )))))))
    192196   
  • src/Clight/test/runtime.c.ma

    diff --git a/src/Clight/test/runtime.c.ma b/src/Clight/test/runtime.c.ma
    index bb2a75e..6485307 100644
    a b definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    2020                   (Expr (Ecast (Tint I32 Unsigned)
    2121                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    2222                     (Tint I32 Unsigned))) (Tint I32 Unsigned))
     23           (None ?)
    2324           (Ssequence
    2425           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Unsigned))
    2526             (Expr (Ebinop Osub
    definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    3435                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    3536                   (Tint I32 Signed  ))
    3637                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    37                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))))
     38                 (Tint I32 Signed  ))) (Tint I8 Unsigned ))))
     39           (None ?))
    3840         (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    3941                               (Expr (Evar (ident_of_nat 2))
    4042                                 (Tint I8 Unsigned ))) (Tint I32 Signed  )))))))
  • src/Clight/test/search.c.ma

    diff --git a/src/Clight/test/search.c.ma b/src/Clight/test/search.c.ma
    index 6e46252..efb53cc 100644
    a b definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    2626                   (Expr (Ecast (Tint I32 Signed  )
    2727                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    2828                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
     29           (None ?)
    2930           (Ssequence
    3031           (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    3132             (Expr (Ecast (Tint I8 Unsigned )
    definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    103104                     (Tint I32 Signed  ))
    104105                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    105106                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    106              Sskip)))))
     107             Sskip))))
     108           (None ?))
    107109         (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
    108110                               (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
    109111                                                   (Tint I32 Signed  )))
  • src/Clight/test/sum.c.ma

    diff --git a/src/Clight/test/sum.c.ma b/src/Clight/test/sum.c.ma
    index 5ea484b..e79372b 100644
    a b definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    2727             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2828             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2929             (Tint I32 Signed  )))
     30         (None ?)
    3031         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    3132           (Expr (Ecast (Tint I8 Unsigned )
    3233             (Expr (Ebinop Oadd
    definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 
    4243                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
    4344                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
    4445             (Tint I8 Unsigned )))
    45        )
     46       (None ?))
    4647       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    4748                             (Expr (Evar (ident_of_nat 3))
    4849                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
  • src/Clight/toCminor.ma

    diff --git a/src/Clight/toCminor.ma b/src/Clight/toCminor.ma
    index df4f7b5..8efa403 100644
    a b match s with 
    5050| Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
    5151                         gather_mem_vars_stmt s1 ∪
    5252                         gather_mem_vars_stmt s2
    53 | Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪
    54                    gather_mem_vars_stmt s1
    55 | Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
    56                    gather_mem_vars_stmt s1
    57 | Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
    58                      gather_mem_vars_expr e1 ∪
    59                      gather_mem_vars_stmt s2 ∪
    60                      gather_mem_vars_stmt s3
     53| Swhile e1 _ s1 _ ⇒ gather_mem_vars_expr e1 ∪
     54                     gather_mem_vars_stmt s1
     55| Sdowhile e1 _ s1 _ ⇒ gather_mem_vars_expr e1 ∪
     56                       gather_mem_vars_stmt s1
     57| Sfor s1 e1 s2 _ s3 _ ⇒ gather_mem_vars_stmt s1 ∪
     58                        gather_mem_vars_expr e1 ∪
     59                        gather_mem_vars_stmt s2 ∪
     60                        gather_mem_vars_stmt s3
    6161| Sbreak ⇒ ∅
    6262| Scontinue ⇒ ∅
    6363| Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
    let rec labels_defined (s:statement) : list ident ≝ 
    925925match s with
    926926[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    927927| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    928 | Swhile _ s _ ⇒ labels_defined s
    929 | Sdowhile _ s ⇒ labels_defined s
    930 | Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     928| Swhile _ _ s _ ⇒ labels_defined s
     929| Sdowhile _ _ s _ ⇒ labels_defined s
     930| Sfor s1 _ s2 _ s3 _ ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
    931931| Sswitch _ ls ⇒ labels_defined_switch ls
    932932| Slabel l s ⇒ l::(labels_defined s)
    933933| Scost _ s ⇒ labels_defined s
    axiom ReturnMismatch : String. 
    11261126definition optional_cost : option costlabel → stmt → stmt ≝
    11271127λo,s. match o with [ Some l ⇒ St_cost l s | None ⇒ s ].
    11281128
     1129lemma optional_cost_P : ∀s,cl,P.
     1130  (∀c. P (St_cost c s)) →
     1131  stmt_P P s →
     1132  stmt_P P (optional_cost cl s).
     1133#s * /2/
     1134qed.
     1135
    11291136let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
    11301137  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
    11311138match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with
    match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s u 
    11681175        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
    11691176    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    11701177    ] e1'
    1171 | Swhile e1 s1 cl
     1178| Swhile e1 lb s1 lp
    11721179    do e1' ← translate_expr vars e1;
    11731180    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    11741181    [ ASTint _ _ ⇒ λe1'.         
    match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s u 
    11781185        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
    11791186        let converted_loop ≝
    11801187          St_label entry
    1181             (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip)))
     1188            (St_ifthenelse ?? e1' (St_seq (optional_cost lb s1') (St_goto entry)) (St_label exit (optional_cost lp St_skip)))
    11821189        in         
    11831190          OK ? «〈fgens2, converted_loop〉, ?»
    11841191    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    11851192    ] e1'
    1186 | Sdowhile e1 s1
     1193| Sdowhile e1 lb s1 lp
    11871194    do e1' ← translate_expr vars e1;
    11881195    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    11891196    [ ASTint _ _ ⇒ λe1'.
    match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s u 
    11921199        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
    11931200        let converted_loop ≝
    11941201          St_label entry
    1195            (St_seq
     1202           (optional_cost lb
    11961203             (St_seq
    11971204               s1'
    1198                (St_ifthenelse ?? e1' (St_goto entry) St_skip)
     1205               (St_ifthenelse ?? e1' (St_goto entry) (St_label exit (optional_cost lp St_skip)))
    11991206             )
    1200              (St_label exit St_skip))
     1207           )
    12011208        in
    12021209        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    12031210        OK ? «〈fgens2, converted_loop〉, ?»
    12041211    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    12051212    ] e1'
    1206 | Sfor s1 e1 s2 s3
     1213| Sfor s1 e1 s2 lb s3 lp
    12071214    do e1' ← translate_expr vars e1;
    12081215    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    12091216    [ ASTint _ _ ⇒ λe1'.
    match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s u 
    12171224          St_seq
    12181225            s1'
    12191226            (St_label entry
    1220               (St_seq
    1221                 (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
    1222                 (St_label exit St_skip)
    1223             ))
     1227              (St_ifthenelse ?? e1' (optional_cost lb (St_seq s3' (St_seq s2' (St_goto entry)))) (St_label exit (optional_cost lp St_skip)))
     1228            )
    12241229        in
    12251230          OK ? «〈fgens4, converted_loop〉, ?»
    12261231    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try ass 
    13381343     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
    13391344                | 2,5: #H %1 %2 assumption
    13401345                | 3,6: #H %2 assumption ] ]
    1341 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
    1342 [ 1,10,20: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    1343 | cases cl normalize /3/
     1346try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     1347try ( @optional_cost_P try @(λ_.I) try @conj try @conj try @conj try @conj try @conj
     1348  try ( @optional_cost_P try @(λ_.I) try @conj try @conj try @conj try @conj try @conj ))
     1349try @I try assumption
     1350[ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    13441351| (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
    1345 |*) 3,11: whd #l #H normalize in H;
     1352|*) 2,8: whd #l #H normalize in H;
    13461353         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
    13471354         @conj
    13481355         [ 1,3: @(proj1 … Hlabel)
    1349          | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
     1356         | 2,4: whd cases lb [ 2,4: #lb'] @or_intror @Exists_append_l try @Exists_append_l try @Exists_append_l
    13501357              @(proj2 … Hlabel) ]
    1351 | 30: whd %2 %2 whd /2/
    1352 | 31: whd %2 whd /2/
    1353 | cases cl normalize /3/
    1354 | 5,17: whd %1 %1 normalize /2/
    1355 | 6,13: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    1356    #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
     1358| 3,5,9,11,14: whd %1 %1 normalize /2/
     1359| 4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1360   #l * try * [ 1,5: #H %1 %1 normalize cases lb [2,4: #lb' ] %2 @Exists_append_l try @Exists_append_l try @Exists_append_l @H
    13571361              | 2,6: #H %1 %2 assumption
    13581362              | 3,7: #H <H %1 %1 normalize /2/
    1359               | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2
     1363              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize cases lb [ 2,4: #lb' ] %2
    13601364                                                 @Exists_append_r normalize /2/
    13611365                                               | 2,4: * ]
    13621366              ]
    1363 | 7: normalize %1 %1 %1 //
    1364 | 8,15: normalize %1 %1 %2 @Exists_append_r normalize /2/
    1365 | cases cl normalize /3/
    1366 | 12,14: whd %1 %1 normalize /2/
    1367 | 16: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
    1368                    | 2: #H elim (Hlabels_tr1 label H)
    1369                          #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
    1370                          [ 1: // | 2: whd %2 assumption ]
    1371                    ]
    1372 | 18: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1367| 6,10: normalize %1 %1 %2 cases lb [2,4:#lb'] @Exists_append_r normalize /2/
     1368| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
     1369               | 2: #H elim (Hlabels_tr1 label H)
     1370                     #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
     1371                     [ 1: // | 2: whd %2 assumption ]
     1372               ]
     1373| @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13731374   #l * try * [ 1: #H %1 %1 normalize %2 @H
    13741375              | 2: #H %1 %2 assumption
    13751376              | 3: #H %2 assumption ]
    1376 | 19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    1377    #H @(Htmps_pres3 … (Htmps_pres2 … H))
    1378 | 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    1379    #H @(Htmps_pres3 … H)
    1380 | 22: whd #l #H normalize in H;
    1381       cases (Exists_append … H) #Hcase
    1382       [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
    1383         [ 1: @(proj1 … Hlabel)
    1384         | 2: normalize @Exists_append_l @(proj2 … Hlabel)
    1385         ]
    1386       | 2: cases (Exists_append … Hcase) #Hcase2
    1387         [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
    1388           [ 1: @(proj1 … Hlabel)
    1389           | 2: normalize >append_nil >append_nil >append_cons
    1390                @Exists_append_r @Exists_append_l @Exists_append_r
    1391                @(proj2 … Hlabel)
    1392           ]
    1393         | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
    1394           [ 1: @(proj1 … Hlabel)
    1395           | 2: normalize >append_nil >append_nil >append_cons
    1396              @Exists_append_r @Exists_append_l @Exists_append_l
    1397              @(proj2 … Hlabel)
    1398           ]
    1399         ]
     1377| @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1378  #H @(Htmps_pres3 … (Htmps_pres2 … H))
     1379| @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1380  #H @(Htmps_pres3 … H)
     1381| whd #l #H normalize in H;
     1382  cases (Exists_append … H) #Hcase
     1383  [ elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1384    [ @(proj1 … Hlabel)
     1385    | normalize @Exists_append_l @(proj2 … Hlabel)
     1386    ]
     1387  | cases (Exists_append … Hcase) #Hcase2
     1388    [ elim (Hlabels_tr2 l Hcase2) #label #Hlabel %{label} %
     1389      [ @(proj1 … Hlabel)
     1390      | normalize cases lb [2:#lb'] normalize >append_nil >append_cons
     1391        @Exists_append_r @Exists_append_l @Exists_append_r
     1392        @(proj2 … Hlabel)
    14001393      ]
    1401 | 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
    1402 | 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1394    | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
     1395      [ 1: @(proj1 … Hlabel)
     1396      | 2: normalize cases lb [2:#lb'] normalize >append_nil >append_cons
     1397         @Exists_append_r @Exists_append_l @Exists_append_l
     1398         @(proj2 … Hlabel)
     1399      ]
     1400    ]
     1401  ]
     1402| #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
     1403| @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    14031404   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
    14041405              | 2: #H %1 %2 assumption
    14051406              | 3: #H %2 assumption ]
    1406 | 25: whd %1 %1 normalize /2/
    1407 | 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    1408    #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    1409                    @Exists_append_r @Exists_append_l @Exists_append_l
     1407| 22,23: whd %1 %1 normalize /2/
     1408| @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1409   #l * try * [ 1: #H %1 %1 normalize cases lb [2:#lb'] normalize @Exists_append_r @(Exists_add ?? (nil ?))
     1410                   @Exists_append_r @Exists_append_l @Exists_append_r
    14101411                   @Exists_append_l assumption
    14111412              | 2: #H %1 %2 assumption
    14121413              | 3: #H <H %1 %1 normalize
    14131414                   @Exists_append_r whd %1 //
    1414               | 4: * [ 1: #H <H %1 %1 normalize
    1415                        @Exists_append_r @(Exists_add ?? (nil ?))
    1416                        @Exists_append_r @Exists_append_r
    1417                        whd %1 //
     1415              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
     1416                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
     1417                       @Exists_append_r whd %1 //
    14181418                     | 2: * ]
    14191419              ]
    1420 | 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    1421    #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    1422                    @Exists_append_r @Exists_append_l @Exists_append_l                   
    1423                    @Exists_append_r @Exists_append_l assumption
     1420| @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1421   #l * try * [ 1: #H %1 %1 normalize cases lb [2:#lb'] normalize @Exists_append_r @(Exists_add ?? (nil ?))
     1422                   @Exists_append_r @Exists_append_l
     1423                   @Exists_append_l assumption
    14241424              | 2: #H %1 %2 assumption
    14251425              | 3: #H <H %1 %1 normalize
    14261426                   @Exists_append_r whd %1 //
    1427               | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
    1428                        @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
    1429                        @Exists_append_r whd %1 //
     1427              | 4: * [ 1: #H <H %1 %1 normalize
     1428                       @Exists_append_r @(Exists_add ?? (nil ?))
     1429                       @Exists_append_r @Exists_append_r
     1430                       whd %1 //
    14301431                     | 2: * ]
    14311432              ]
    1432 | 28: whd %1 %1 normalize /2/
    1433 | 29: whd %1 %1 normalize
    1434       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
    1435       whd %1 //
    1436 | 32: whd %1 %2 whd @(ex_intro … l) @E
     1433| whd %1 %1 normalize
     1434  @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
     1435  whd %1 //
     1436| whd %2 %2 whd /2/
     1437| whd %2 whd /2/
     1438| whd %1 %2 whd @(ex_intro … l) @E
    14371439] qed.
    14381440
    14391441axiom ParamGlobalMixup : String.
Note: See TracBrowser for help on using the repository browser.