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.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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' #_
Note: See TracChangeset for help on using the changeset viewer.