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/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
Note: See TracChangeset for help on using the changeset viewer.