Changeset 2353


Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

Location:
src/Clight
Files:
13 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2203 r2353  
    390390          | _ ⇒ Wrong ??? (msg NonsenseState)
    391391          ]
    392       | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     392      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
    393393      | Kdowhile a s' k' ⇒
    394394          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
     
    406406      match k with
    407407      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
    408       | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     408      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
    409409      | Kdowhile a s' k' ⇒
    410410          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
     
    421421      match k with
    422422      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
    423       | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     423      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (optional_cost cl Sskip) k' e m〉
    424424      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    425425      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     
    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'
     433  | Swhile a s' cl
    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' k) e m
    437                       else State f Sskip k e m〉
     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〉
    438438  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
    439439  | Sfor a1 a2 a3 s' ⇒
  • src/Clight/CexecComplete.ma

    r2176 r2353  
    383383    >(yields_eq ??? (bool_of_false ?? H2))
    384384    @refl
    385 | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    386     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    387     >(yields_eq ??? (bool_of_false ?? H2))
    388     @refl
    389 | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    390     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    391     >(yields_eq ??? (bool_of_true ?? H2))
    392     @refl
    393 | #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl
    394 | 13,14: #f #e #s #k #env #m @refl
     385| #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     386    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     387    >(yields_eq ??? (bool_of_false ?? H2))
     388    @refl
     389| #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     390    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     391    >(yields_eq ??? (bool_of_true ?? H2))
     392    @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
    395395| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
    396396    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     
    424424    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    425425    | #s' #k' whd in ⊢ (% → ?); *;
    426     | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *;
     426    | 3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *;
    427427    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
    428428    | #k' whd in ⊢ (% → ?); *;
  • src/Clight/CexecEquiv.ma

    r1713 r2353  
    514514#ge #s cases s;
    515515[ #f #st #kk #e #m cases st;
    516   [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
    517   [ 4,6,8,9: @I ]
     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 ]
    518518  whd in ⊢ (???%);
    519519  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
     
    521521  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
    522522  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
    523   | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    524523  | @err2_does_not_interact #x1 #x2 cases x1; //;
    525524  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
    526525      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
     526  | 6,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    527527  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    528528      | @I ]
  • src/Clight/CexecSound.ma

    r2176 r2353  
    337337        @step_skip_call //;
    338338    | #s' #k' whd; //
    339     | #ex #s' #k' @step_skip_or_continue_while % //;
     339    | #ex #s' #cl #k' @step_skip_or_continue_while % //;
    340340    | #ex #s' #k'
    341341        @res_bindIO2_OK #v #tr #Hv
     
    385385    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    386386    ]
    387   | #ex #s'
     387  | #ex #s' #cl
    388388    @res_bindIO2_OK #v #tr #Hv
    389389    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     
    407407  | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
    408408  | whd in ⊢ (?????%); cases k; //;
    409     [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
     409    [ #ex #s' #cl #k' whd; @step_skip_or_continue_while %2 ; //;
    410410    | #ex #s' #k' whd;
    411411      @res_bindIO2_OK #v #tr #Hv
  • src/Clight/Csem.ma

    r2263 r2353  
    910910  | Kseq: statement -> cont -> cont
    911911       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
    912   | Kwhile: expr -> statement -> cont -> cont
     912  | Kwhile: expr -> statement → option costlabel -> cont -> cont
    913913       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
    914914  | Kdowhile: expr -> statement -> cont -> cont
     
    930930  match k with
    931931  [ Kseq s k => call_cont k
    932   | Kwhile e s k => call_cont k
     932  | Kwhile e s l k => call_cont k
    933933  | Kdowhile e s k => call_cont k
    934934  | Kfor2 e2 e3 s k => call_cont k
     
    983983      | None => find_label lbl s2 k
    984984      ]
    985   | Swhile a s1 =>
    986       find_label lbl s1 (Kwhile a s1 k)
     985  | Swhile a s1 l =>
     986      find_label lbl s1 (Kwhile a s1 l k)
    987987  | Sdowhile a s1 =>
    988988      find_label lbl s1 (Kdowhile a s1 k)
     
    10351035].
    10361036
     1037definition optional_cost : option costlabel → statement → statement ≝
     1038λo,s. match o with [ Some cl ⇒ Scost cl s | None ⇒ s ].
     1039
    10371040(* XXX: note that cost labels in exprs expose a particular eval order. *)
    10381041
     
    10871090           tr (State f s2 k e m)
    10881091
    1089   | step_while_false: ∀f,a,s,k,e,m,v,tr.
     1092  | step_while_false: ∀f,a,s,cl,k,e,m,v,tr.
    10901093      eval_expr ge e m a v tr →
    10911094      is_false v (typeof a) →
    1092       step ge (State f (Swhile a s) k e m)
    1093            tr (State f Sskip k e m)
    1094   | step_while_true: ∀f,a,s,k,e,m,v,tr.
     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.
    10951098      eval_expr ge e m a v tr →
    10961099      is_true v (typeof a) →
    1097       step ge (State f (Swhile a s) k e m)
    1098            tr (State f s (Kwhile a s k) e m)
    1099   | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
     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.
    11001103      x = Sskip ∨ x = Scontinue →
    1101       step ge (State f x (Kwhile a s k) e m)
    1102            E0 (State f (Swhile a s) k e m)
    1103   | step_break_while: ∀f,a,s,k,e,m.
    1104       step ge (State f Sbreak (Kwhile a s k) e m)
    1105            E0 (State f Sskip k e m)
     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)
    11061109
    11071110  | step_dowhile: ∀f,a,s,k,e,m.
  • src/Clight/Csyntax.ma

    r2176 r2353  
    194194  | Ssequence : statement → statement → statement  (**r sequence *)
    195195  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
    196   | Swhile : expr → statement → statement   (**r [while] loop *)
     196  | Swhile : expr → statement → option costlabel → statement   (**r [while] loop *)
    197197  | Sdowhile : expr → statement → statement (**r [do] loop *)
    198198  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
     
    226226  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    227227  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    228   (Swh:∀e,s. P s → P (Swhile e s))
     228  (Swh:∀e,s,l. P s → P (Swhile e s l))
    229229  (Sdo:∀e,s. P s → P (Sdowhile e s))
    230230  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    249249    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    250250    (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 ⇒ Swh e s
     251| Swhile e s cl ⇒ Swh e s cl
    252252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    253253| Sdowhile e s ⇒ Sdo e s
     
    275275  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    276276  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    277   (Swh:∀e,s. P s → P (Swhile e s))
     277  (Swh:∀e,s,l. P s → P (Swhile e s l))
    278278  (Sdo:∀e,s. P s → P (Sdowhile e s))
    279279  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
  • src/Clight/SimplifyCasts.ma

    r2219 r2353  
    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 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* 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 *)
    19851985| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
    19861986| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
     
    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,k,k'.
     2017| cc_while : ∀e,s,cl,k,k'.
    20182018    cont_cast k k' →
    2019     cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k')
     2019    cont_cast (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k')
    20202020| cc_dowhile : ∀e,s,k,k'.
    20212021    cont_cast k k' →
     
    24242424          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    24252425     ] ]
    2426 | 6: #e #s #Hind_s #k #k' #Hcont_cast
     2426| 6: #e #s #cl #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 k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     2429     elim (elim_IH_aux lab s (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k') ? Hind_s)
    24302430     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24312431          normalize nodelta %{kst'} /2/
     
    26162616               [ 1: // | 2: %1 // ]               
    26172617          | 3: (* Kwhile *)
    2618                #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2618               #cond #body #cl #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)) k0' en m)} @conj
     2620               %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)} @conj
    26212621               [ 1: // | 2: %1 // ]
    26222622          | 4: (* Kdowhile *)
     
    27832783                             [ 1: // | 2: <e0 %1 // ]
    27842784                        ] ] ] ]
    2785     | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2785    | 6: #cl #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 ⊢ %;
     
    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) k') en m)}
     2800                             %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) cl k') en m)}
    28012801                             @conj
    28022802                             [ 1: // | 2: <e0 %1 @cc_while // ]
    28032803                        | 2: destruct skip (condtrace)
    2804                              %{(State (simplify_function f) Sskip k' en m)} @conj
    2805                              [ 1: // | 2: <e0 %1 // ]
     2804                             %{(State (simplify_function f) (optional_cost cl Sskip) k' en m)} @conj
     2805                             [ 1: // | 2: <e0 cases cl [2:#cl'] %1 // ]
    28062806                        ] ] ] ]
    28072807    | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     
    28502850         [ 1: #Hk #Hk' #_
    28512851         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2852          | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2852         | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    28532853         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28542854         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     
    28582858         destruct (H)
    28592859         [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
    2860          | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %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 // ]
    28612862    | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28622863         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     
    28652866         [ 1: #Hk #Hk' #_
    28662867         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2867          | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2868         | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    28682869         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28692870         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     
    28732874         destruct (H)
    28742875         [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
    2875          | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)}
     2876         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)}
    28762877              @conj try // %1 //
    28772878         | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
     
    30073008     [ 1: #Hk #Hk' #_
    30083009     | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    3009      | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     3010     | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    30103011     | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    30113012     | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
  • src/Clight/label.ma

    r2319 r2353  
    11include "Clight/Csyntax.ma".
     2
     3(* Label freedom *)
     4
     5let rec expr_label_free (e:expr) : bool ≝
     6match e with
     7[ Expr e' _ ⇒
     8  match e' with
     9  [ Ederef e1 ⇒ expr_label_free e1
     10  | Eaddrof e1 ⇒ expr_label_free e1
     11  | Eunop _ e1 ⇒ expr_label_free e1
     12  | Ebinop _ e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
     13  | Ecast _ e1 ⇒ expr_label_free e1
     14  | Econdition e1 e2 e3 ⇒ expr_label_free e1 ∧ expr_label_free e2 ∧ expr_label_free e3
     15  | Eandbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
     16  | Eorbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
     17  | Efield e1 _ ⇒ expr_label_free e1
     18  | Ecost _ _ ⇒ false
     19  | _ ⇒ true
     20  ]
     21].
     22
     23let rec statement_label_free (s:statement) : bool ≝
     24match s with
     25[ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
     26| Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_free es
     27| Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
     28| 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| Sreturn oe ⇒ option_map_def … expr_label_free true oe
     33| Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_free ls
     34| Slabel _ s1 ⇒ statement_label_free s1
     35| Scost _ _ ⇒ false
     36| _ ⇒ true
     37] and labeled_statements_label_free (ls:labeled_statements) : bool ≝
     38match ls with
     39[ LSdefault s1 ⇒ statement_label_free s1
     40| LScase _ _ s1 ls1 ⇒ statement_label_free s1 ∧ labeled_statements_label_free ls1
     41].
     42
     43definition clight_fundef_label_free : ident × clight_fundef → bool ≝
     44λifd. match \snd ifd with
     45[ CL_Internal f ⇒ statement_label_free (fn_body f)
     46| _ ⇒ true
     47].
     48
     49definition clight_label_free : clight_program → bool ≝
     50λp. all ? clight_fundef_label_free (prog_funct ?? p).
     51
     52(* Adding labels *)
    253
    354definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
     
    94145| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
    95146].
     147
     148definition ensure_label : option costlabel → universe CostTag → costlabel × (universe CostTag) ≝
     149λo,u.
     150  match o with
     151  [ Some cl ⇒ 〈cl,u〉
     152  | None ⇒ fresh … u
     153  ].
    96154
    97155
     
    120178    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
    121179    〈Sifthenelse e s1 s2, costgen〉
    122 | Swhile e s'
     180| Swhile e s' cl
    123181    let 〈e,costgen〉 ≝ label_expr e costgen in
    124182    let 〈s',costgen〉 ≝ label_statement s' costgen in
    125183    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
    126     let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
    127     〈s,costgen〉
     184    let 〈after,costgen〉 ≝ ensure_label cl costgen in
     185    〈Swhile e s' (Some ? after), costgen〉
    128186| Sdowhile e s' ⇒
    129187    let 〈e,costgen〉 ≝ label_expr e costgen in
  • src/Clight/labelSimulation.ma

    r2338 r2353  
    264264| cwl_stop : cont_with_labels Kstop Kstop
    265265| 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,cs,cpost,k,k'.
     266| cwl_while : ∀ue,e,us,s,cl,cs,cpost,k,k'.
    267267    cont_with_labels k k' →
    268     cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) 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')
    269270| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
    270271    cont_with_labels k k' →
     
    291292(* Extra matching states that we can reach that don't quite correspond to the
    292293   labelling function *)
    293 | swl_whilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    294     state_with_labels_partial (State f (Swhile a s) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     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)
    295297| swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    296298    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)
     
    432434| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
    433435| 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))))
    434 | Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
     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))
    435437| 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))
    436438| 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))
     
    447449@label_gen_elim #u2 //
    448450[ 6: >shift_fst //
     451| 3: @label_gen_elim #u3 >shift_fst >shift_fst
     452     cases C in E ⊢ %; /3/
    449453| *: @label_gen_elim #u3 //
    450454     @label_gen_elim #u4
    451455     [ @label_gen_elim #u5 >shift_fst >shift_fst //
    452      | 2,3: >shift_fst >shift_fst //
     456     | >shift_fst >shift_fst //
    453457     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
    454458     ]
     
    529533      @refl | // ] |skip ]| skip ]| skip ]
    530534  ]
    531 | #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
     535| #e #s0 #cl #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #CL
    532536  whd in match (find_label ?? k); normalize in match (find_label ?? k');
    533537  @(lfl_IH s0 … IH) [ /2/ ]
     
    671675    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
    672676      whd in EX:(??%%); destruct /4/
    673     | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0}
     677    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K #CL #_ #E1 #E2 #E3 destruct %{0}
    674678      whd in EX:(??%%); destruct whd /4/
    675679    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     
    761765    whd in ⊢ (??%?); >label_expr_type >EX2
    762766    whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
    763   | #a #st #EX
     767  | #a #st #cl #EX
    764768    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    765769    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    766770    normalize in EX; destruct
    767     whd in match (label_statement ??); @label_gen_elim #u1
    768     @label_gen_elim #u2
    769     whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
    770     >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
    771     >shift_fst
    772     cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    773     [ %{2} | %{3} ] whd
     771    @blindly_label #u1 #u2 #cs #cpost * #CL destruct
     772    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u1) #tr1' * #EX1' #T1
     773    [ 1,2,3: %{1} | %{0} ] whd
    774774    whd in ⊢ (??%?); >EX1'
    775775    whd in ⊢ (??%?); >label_expr_type >EX2
    776     whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /5/
     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/
    777777  | #a #st #EX
    778778    normalize in EX; destruct
     
    805805    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    806806    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    807     | #ue #e0 #us0 #s0 #cs #cpost #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
    808808    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    809809    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    815815    ]
    816816    whd in match (label_statement ??);
    817     [ 1,6,7: %{0} % /3/
    818     | 2,3,5: %{2} % /3/
    819     | %{1} % /3/
     817    [ 1,3,7,8: %{0} % /3/
     818    | 2,5: %{1} whd % /3/
     819    | 4,6: %{2} whd % /3/
    820820    ]
    821821  | #EX inversion KL
    822822    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    823823    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    824     | #ue #e0 #us0 #s0 #cs #cpost #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
    825825    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    826826    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    832832    ]
    833833    whd in match (label_statement ??);
    834     [ 1,2,5,6,7: %{0} % /4/
    835     | 4: %{1} % /4/
     834    [ 1,2,3,6,7,8: %{0} % /4/
     835    | 5: %{1} % /4/
    836836    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    837837      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     
    897897    %{0} % /3/
    898898  ]
    899 | #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     899| #u0 #f #ua #a #us #s #cl #cs #cpost #k #k' #e #m #K * #CL #EX
    900900  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    901901  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    902902  whd in EX:(??%%); destruct
    903903  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
    904   [ %{1} | %{2} ] whd
     904  [ 4: %{0} | 1,2,3: %{1} ] whd
    905905  whd in ⊢ (??%?); >EX1'
    906906  whd in ⊢ (??%?); >label_expr_type >EX2
    907   % [ 1,3: <(E0_right tr) ] /4/
     907  whd % [ 1,3,5,7: <(E0_right tr) ] /5/
    908908| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    909909  whd in EX:(??%%); destruct
     
    991991#ge #s cases s
    992992[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
    993   [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
     993  [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
    994994  whd in ⊢ (??%? → ?);
    995   [ 4,6,8,9: #EX destruct ]
     995  [ 4,5,7,8: #EX destruct ]
    996996  [ cases a
    997997    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
     
    10011001  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
    10021002  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
    1003   | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
    10041003  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
    10051004  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
    10061005      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
     1006  | 6,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
    10071007  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
    10081008  | 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
     
    10381038[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
    10391039  [ #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 destruct
     1040  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct
    10411041  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
    10421042  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
  • src/Clight/switchRemoval.ma

    r2332 r2353  
    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
     79| Swhile e body _ ⇒ switch_free body
    8080| Sdowhile e body ⇒ switch_free body
    8181| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
     
    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
     250| Swhile e body cl
    251251  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    252   ret 〈Swhile e body', acc, fvs', u'〉
     252  ret 〈Swhile e body' cl, acc, fvs', u'〉
    253253| Sdowhile e body ⇒
    254254  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     
    317317  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    318318  〈fvs @ fvs', u''〉
    319 | Swhile e body
     319| Swhile e body cl
    320320  mk_fresh_variables body u
    321321| Sdowhile e body ⇒
     
    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. P s → P (Swhile e s))
     368  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
    369369  (Sdo:∀e,s. P s → P (Sdowhile e s))
    370370  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    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 ⇒ Swh e s
     391| Swhile e s cl ⇒ Swh e s cl
    392392    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    393393| Sdowhile e s ⇒ Sdo e s
     
    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. P s → P (Swhile e s))
     417  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
    418418  (Sdo:∀e,s. P s → P (Sdowhile e s))
    419419  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    471471         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    472472         (ret_u statement s2')))} % try //
    473 | 6: #e #s #H #u0 #u1 #post normalize
     473| 6: #e #s #cl #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')) (ret_acc statement s1')
     477     %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
    478478        (ret_fvs statement s1') (ret_u statement s1'))} % try //
    479479| 7: #e #s #H #u0 #u1 #post normalize
     
    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)
    631631| Sdowhile e body ⇒
     
    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
     713| Swhile e sub _ ⇒ Q e ∧ P sub
    714714| Sdowhile e sub ⇒ Q e ∧ P sub
    715715| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
     
    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,k,k',u,result.
    1418     fresh_for_statement (Swhile e s) u →
     1417| swc_while : ∀fvs,e,s,cl,k,k',u,result.
     1418    fresh_for_statement (Swhile e s cl) u →
    14191419    switch_cont_sim fvs k k' →
    14201420    switch_removal s fvs u = Some ? result →
    1421     switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
     1421    switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
    14221422| swc_dowhile : ∀fvs,e,s,k,k',u,result.
    14231423    fresh_for_statement (Sdowhile e s) u →
     
    20482048qed. *)
    20492049
    2050 lemma while_fresh_lift : ∀e,s,u.
    2051    fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
    2052 #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
     2050lemma while_fresh_lift : ∀e,s,cl,u.
     2051   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
     2052#e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
    20532053cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
    20542054cases (leb e s) try /2/
  • src/Clight/test/goto-if.test.ma

    r2253 r2353  
    88include "Clight/label.ma".
    99
    10 definition myprog' ≝ clight_label myprog.
     10definition myprog' ≝ \fst (clight_label myprog).
    1111
    1212example el: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog' 1000 [ ]).
     
    3737example e2: finishes_with (repr I32 0) ? (
    3838bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
    39 (λp1. let p2 ≝ cminor_to_rtlabs p1 in
     39(λp1. let p2 ≝ cminor_to_rtlabs (\snd (clight_label myprog)) p1 in
    4040  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    4141normalize
    4242%
    4343qed.
     44
     45include "RTLabs/CostCheck.ma".
     46
     47axiom MISSING:String.
     48axiom EXTERNAL:String.
     49
     50definition readable_body ≝
     51λfn. insert_sort ?
     52       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
     53       (elements ?? (f_graph fn)).
     54(*
     55example c2: result ? (
     56  ! p1 ← clight_to_cminor (simplify_program (clight_label myprog));
     57  let p2 ≝ cminor_to_rtlabs p1 in
     58  match prog_funct … p2 with
     59  [ nil ⇒ Error ? (msg MISSING)
     60  | cons h _ ⇒
     61    match \snd h with
     62    [ External _ ⇒ Error ? (msg EXTERNAL)
     63    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
     64    ]
     65  ]).
     66normalize
     67*)
     68example c2: (
     69  let 〈p0,init〉 ≝ clight_label myprog in
     70  ! p1 ← clight_to_cminor (simplify_program p0);
     71  let p2 ≝ cminor_to_rtlabs init p1 in
     72  return (check_cost_program p2)) = OK … true.
     73normalize
     74%
     75qed.
  • src/Clight/test/sum.test.ma

    r2253 r2353  
    2525include "Cminor/toRTLabs.ma".
    2626include "RTLabs/semantics.ma".
     27include "Clight/label.ma".
    2728
    2829example e2: finishes_with (repr I32 74) ? (
    29 bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
    30 (λp1. let p2 ≝ cminor_to_rtlabs p1 in
     30let 〈p0,init〉 ≝ clight_label myprog in
     31bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
     32(λp1. let p2 ≝ cminor_to_rtlabs init p1 in
    3133  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    3234normalize
    3335%
    3436qed.
     37
     38include "RTLabs/CostCheck.ma".
     39
     40axiom MISSING:String.
     41axiom EXTERNAL:String.
     42
     43definition readable_body ≝
     44λfn. insert_sort ?
     45       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
     46       (elements ?? (f_graph fn)).
     47(*
     48example c2: result ? (
     49  let 〈p0,init〉 ≝ clight_label myprog in
     50  ! p1 ← clight_to_cminor (simplify_program p0);
     51  let p2 ≝ cminor_to_rtlabs init p1 in
     52  match prog_funct … p2 with
     53  [ nil ⇒ Error ? (msg MISSING)
     54  | cons h _ ⇒
     55    match \snd h with
     56    [ External _ ⇒ Error ? (msg EXTERNAL)
     57    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
     58    ]
     59  ]).
     60normalize
     61*)
     62example c2: (
     63  let 〈p0,init〉 ≝ clight_label myprog in
     64  ! p1 ← clight_to_cminor (simplify_program p0);
     65  let p2 ≝ cminor_to_rtlabs init p1 in
     66  return (check_cost_program p2)) = OK bool true.
     67normalize
     68%
     69qed.
     70
     71
     72
    3573(*
    3674include "RTLabs/RTLabsToRTL.ma".
  • src/Clight/toCminor.ma

    r2252 r2353  
    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
     53| Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪
     54                   gather_mem_vars_stmt s1
    5555| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
    5656                   gather_mem_vars_stmt s1
     
    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
     928| Swhile _ s _ ⇒ labels_defined s
    929929| Sdowhile _ s ⇒ labels_defined s
    930930| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     
    11241124axiom ReturnMismatch : String.
    11251125
     1126definition optional_cost : option costlabel → stmt → stmt ≝
     1127λo,s. match o with [ Some l ⇒ St_cost l s | None ⇒ s ].
     1128
    11261129let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
    11271130  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
     
    11661169    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    11671170    ] e1'
    1168 | Swhile e1 s1
     1171| Swhile e1 s1 cl
    11691172    do e1' ← translate_expr vars e1;
    11701173    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     
    11761179        let converted_loop ≝
    11771180          St_label entry
    1178           (St_seq
    1179             (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
    1180             (St_label exit St_skip))
     1181            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip)))
    11811182        in         
    11821183          OK ? «〈fgens2, converted_loop〉, ?»
     
    13391340                | 3,6: #H %2 assumption ] ]
    13401341try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
    1341 [ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1342[ 1,10,20: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1343| cases cl normalize /3/
    13421344| (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
    1343 |*) 2,8: whd #l #H normalize in H;
     1345|*) 3,11: whd #l #H normalize in H;
    13441346         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
    13451347         @conj
     
    13471349         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
    13481350              @(proj2 … Hlabel) ]
    1349 | 27: whd %2 %2 whd /2/
    1350 | 28: whd %2 whd /2/
    1351 | 3,14: whd %1 %1 normalize /2/
    1352 | 4,10: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     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)
    13531356   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
    13541357              | 2,6: #H %1 %2 assumption
     
    13581361                                               | 2,4: * ]
    13591362              ]
    1360 | 5: normalize %1 %1 %1 //                                                                                   
    1361 | 6,12: normalize %1 %1 %2 @Exists_append_r normalize /2/
    1362 | 9,11: whd %1 %1 normalize /2/
    1363 | 13: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
     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/ ]
    13641368                   | 2: #H elim (Hlabels_tr1 label H)
    13651369                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
    13661370                         [ 1: // | 2: whd %2 assumption ]
    13671371                   ]
    1368 | 15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1372| 18: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13691373   #l * try * [ 1: #H %1 %1 normalize %2 @H
    13701374              | 2: #H %1 %2 assumption
    13711375              | 3: #H %2 assumption ]
    1372 | 16: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1376| 19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13731377   #H @(Htmps_pres3 … (Htmps_pres2 … H))
    1374 | 18: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1378| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13751379   #H @(Htmps_pres3 … H)
    1376 | 19: whd #l #H normalize in H;
     1380| 22: whd #l #H normalize in H;
    13771381      cases (Exists_append … H) #Hcase
    13781382      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     
    13951399        ]
    13961400      ]
    1397 | 20: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
    1398 | 21: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     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)
    13991403   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
    14001404              | 2: #H %1 %2 assumption
    14011405              | 3: #H %2 assumption ]
    1402 | 22: whd %1 %1 normalize /2/
    1403 | 23: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1406| 25: whd %1 %1 normalize /2/
     1407| 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    14041408   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    14051409                   @Exists_append_r @Exists_append_l @Exists_append_l
     
    14141418                     | 2: * ]
    14151419              ]
    1416 | 24: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1420| 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    14171421   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    14181422                   @Exists_append_r @Exists_append_l @Exists_append_l                   
     
    14261430                     | 2: * ]
    14271431              ]
    1428 | 25: whd %1 %1 normalize /2/
    1429 | 26: whd %1 %1 normalize
     1432| 28: whd %1 %1 normalize /2/
     1433| 29: whd %1 %1 normalize
    14301434      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
    14311435      whd %1 //
    1432 | 29: whd %1 %2 whd @(ex_intro … l) @E
     1436| 32: whd %1 %2 whd @(ex_intro … l) @E
    14331437] qed.
    14341438
Note: See TracChangeset for help on using the changeset viewer.