Changeset 2319


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (7 years ago)
Author:
campbell
Message:

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2103 r2319  
    175175].
    176176
    177 definition label_function : function → function ≝
    178 λf.
    179   let costgen ≝ new_universe CostTag in
     177definition label_function : universe CostTag → function → function × (universe CostTag) ≝
     178λcostgen,f.
    180179  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
    181180  let 〈body,costgen〉 ≝ add_cost_before body costgen in
    182     mk_function (fn_return f) (fn_params f) (fn_vars f) body.
     181    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
    183182
    184 definition label_fundef : clight_fundef → clight_fundef ≝
    185 λf. match f with
    186 [ CL_Internal f ⇒ CL_Internal (label_function f)
    187 | CL_External id args ty ⇒ CL_External id args ty
     183definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
     184λgen,f. match f with
     185[ CL_Internal f ⇒
     186    let 〈f',gen'〉 ≝ label_function gen f in
     187    〈CL_Internal f', gen'〉
     188| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
    188189].
    189190
    190 definition clight_label : clight_program → clight_program ≝
    191  λp. transform_program … p (λ_.label_fundef).
     191
     192
     193definition clight_label : clight_program → clight_program × costlabel ≝
     194λp.
     195  let costgen ≝ new_universe CostTag in
     196  let 〈init_cost, costgen〉 ≝ fresh … costgen in
     197  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
  • src/Clight/labelSimulation.ma

    r2203 r2319  
    5050
    5151theorem label_expr_ok : ∀ge,ge',en,m.
    52   related_globals … label_fundef ge ge' →
     52  related_globals_gen … label_fundef ge ge' →
    5353  (∀e,v,tr.
    5454   exec_expr ge en m e = OK … 〈v,tr〉 →
     
    8787| #v #ty #b #o #tr #EX #u %{tr} % [
    8888    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
    89     [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) //
     89    [ whd in ⊢ (??%? → ??%?); >(rgg_find_symbol … RG) //
    9090    | #b // ]
    9191  | // ]
     
    239239
    240240lemma label_exprs_ok : ∀ge,ge'.
    241    related_globals … label_fundef ge ge' →
     241   related_globals_gen … label_fundef ge ge' →
    242242   ∀en,m,es,vs,tr.
    243243   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
     
    276276| 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'))
    277277| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
    278 | cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k')
     278| 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')
    279279| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
    280280    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
     
    288288(* Now define almost all of the simulation relation... *)
    289289inductive state_with_labels_partial : state → state → Prop ≝
    290 | swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
     290| 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)
    291291(* Extra matching states that we can reach that don't quite correspond to the
    292292   labelling function *)
    293 | swl_whilestate : ∀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 (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    295 | swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    296     state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    297 | swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    298     state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     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)
     295| swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
     296    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)
     297| swl_forstate : ∀g,f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
     298    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)
    299299(* and the rest *)
    300 | swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
     300| 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)
    301301| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
    302302| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
     
    309309inductive state_with_labels : state → state → Prop ≝
    310310| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
    311 | swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
     311| swl_switchstate : ∀g,f,u,ls,k,k',e,m. cont_with_labels k k' →
    312312    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
    313                       (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
     313                      (State (\fst (label_function g f)) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
    314314.
    315315
    316316(* Some details are invariant under labelling. *)
    317 lemma label_function_return : ∀f.
    318   fn_return (label_function f) = fn_return f.
    319 * #rty #params #vars #body
    320 whd in ⊢ (??(?%)?);
     317lemma label_function_return : ∀g,f.
     318  fn_return (\fst (label_function g f)) = fn_return f.
     319#g * #rty #params #vars #body
     320whd in match (label_function ??);
    321321cases (label_statement ??) #body' #u'
    322 whd in ⊢ (??(?%)?);
     322whd in ⊢ (??(?(???%))?);
    323323cases (add_cost_before ??) #body'' #u''
    324324//
     
    330330qed.
    331331
    332 lemma label_fundef_typeof_fundef : ∀fd.
    333   type_of_fundef (label_fundef fd) = type_of_fundef fd.
    334 * //
     332lemma label_fundef_typeof_fundef : ∀g,fd.
     333  type_of_fundef (\fst (label_fundef g fd)) = type_of_fundef fd.
     334#g * //
    335335* #rty #args #vars #body
    336336normalize cases (label_statement ??) #body' #u
     
    338338qed.
    339339
    340 lemma label_fn_params : ∀f.
    341   fn_params (label_function f) = fn_params f.
    342 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
    343 qed.
    344 
    345 lemma label_fn_vars : ∀f.
    346   fn_vars (label_function f) = fn_vars f.
    347 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
     340lemma label_fn_params : ∀g,f.
     341  fn_params (\fst (label_function g f)) = fn_params f.
     342#g * #rty #params #vars #s whd in ⊢ (??(?(???%))?); @breakup_pair @breakup_pair //
     343qed.
     344
     345lemma label_fn_vars : ∀g,f.
     346  fn_vars (\fst (label_function g f)) = fn_vars f.
     347#g * #rty #params #vars #s whd in ⊢ (??(?(???%))?); @breakup_pair @breakup_pair //
    348348qed.
    349349
     
    357357
    358358lemma opt_find_funct : ∀ge,ge',m,vf,fd.
    359   related_globals … label_fundef ge ge' →
     359  related_globals_gen … label_fundef ge ge' →
    360360  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
    361   opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
     361  ∃u. opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (\fst (label_fundef u fd)).
    362362#ge #ge' #m #vf #fd #RG
    363 lapply (rg_find_funct … RG … vf fd)
     363lapply (rgg_find_funct … RG … vf fd)
    364364cases (find_funct … vf)
    365365[ #_ #E normalize in E; destruct
    366 | #fd' #H #E normalize in E; destruct >(H (refl ??)) //
     366| #fd' #H #E normalize in E; destruct cases (H (refl ??)) #u #FF %{u} >FF //
    367367] qed.
    368368
     
    624624] qed.
    625625
    626 lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
     626lemma label_find_label_fn : ∀g,lbl,f,k,k',s1,k1.
    627627  cont_with_labels k k' →
    628628  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
    629629  ∃u',cs,k1'.
    630     find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
     630    find_label lbl (fn_body (\fst (label_function g f))) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
    631631    cont_with_labels k1 k1'.
    632 #lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
    633 whd in match (label_function ?);
     632#g #lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
     633whd in match (label_function ??);
    634634@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
    635 lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
     635lapply (label_find_label lbl s (call_cont k) (call_cont k') g ?)
    636636[ /2/ ]
    637 >FIND //
     637>FIND whd in ⊢ (% → ?); //
    638638qed.
    639639
     
    644644   for labeled_statements. *)
    645645lemma step_with_labels_partial : ∀ge,ge'.
    646   related_globals … label_fundef ge ge' →
     646  related_globals_gen … label_fundef ge ge' →
    647647  ∀s1,s1',tr,s2.
    648648  state_with_labels_partial s1 s1' →
     
    658658   out the final trace and state and "skip" them afterwards. *)
    659659#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
    660 [ #f #us #s #k #k' #e #m #KL cases s
     660[ #g #f #us #s #k #k' #e #m #KL cases s
    661661  [ #EX inversion KL
    662662    [ #E1 #E2 #_ destruct %{tr}
     
    669669      ]
    670670    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
    671       %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
     671      %{(State (\fst (label_function g f)) (\fst (label_statement s0 u)) k0' e m)}
    672672      whd in EX:(??%%); destruct
    673673      % [ % [ @cl_plus_one @refl | // ] | /3/ ]
     
    708708      whd in EX:(??%?); destruct
    709709      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    710     | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     710    | #u0 #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    711711      whd in EX:(??%?);
    712712      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
     
    751751    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
    752752    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
    753     % [2,4: % [2,4: % [1,3: % [1,3:
     753      cases (opt_find_funct … RG … EX3) #ux #EFF
     754      % [2,4: % [2,4: % [1,3: % [1,3:
    754755      @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
    755756      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
    756       whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
     757      whd in ⊢ (??%?); [ >EFF in ⊢ (??%?); | >EFF in ⊢ (??%?); ]
    757758      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
    758       whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
     759      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
     760      whd in ⊢ (??%?);
    759761      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
    760762  | #st1 #st2 #EX
     
    851853    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    852854    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    853     | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     855    | #ux #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    854856    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    855857    ]
     
    871873    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    872874    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    873     | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     875    | #g #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    874876    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    875877    ]
     
    939941    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
    940942    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
    941       cases (label_find_label_fn … KL F)
     943      cases (label_find_label_fn g … KL F)
    942944      #u' * #cs * #k1' * #F' #K'
    943945      % [2: %[2: %[ %[ @cl_plus_succ
     
    948950    % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ]
    949951  ]
    950 | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     952| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    951953  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    952954  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     
    965967    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
    966968  ]
    967 | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     969| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    968970  whd in EX:(??%%); destruct
    969971  % [2: % [2: % [ % [
    970972    @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ]
    971973    | /2/ ]| /4/ ]| skip ]| skip ]
    972 | #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
     974| #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
    973975  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    974976  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     
    987989    ]
    988990  ]
    989 | *
     991| #u0 *
    990992  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
    991993    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
    992994    whd in EX:(??%%); destruct
    993     whd in match (label_fundef ?);
    994     whd in match (label_function ?);
    995     lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
     995    whd in match (label_fundef ??);
     996    whd in match (label_function ??);
     997    lapply (refl ? (\fst (label_function u0 f))) whd in ⊢ (???(???%) → ?);
    996998    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
    997999    % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
     
    10091011    ]
    10101012    % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ]
    1011   | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
     1013  | 9: #u0 #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
    10121014    [ #EX whd in EX:(??%?); destruct
    10131015      % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ]
     
    10251027
    10261028theorem step_with_labels : ∀ge,ge'.
    1027   related_globals … label_fundef ge ge' →
     1029  related_globals_gen … label_fundef ge ge' →
    10281030  ∀s1,s1',tr,s2.
    10291031  state_with_labels s1 s1' →
     
    10341036#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
    10351037[ #s1 #s1' @step_with_labels_partial //
    1036 | #f #u *
     1038| #u0 #f #u *
    10371039(* If we have LSdefault we need to smuggle the execution of the cost label in
    10381040   before the actual statement. *)
     
    10411043    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
    10421044    >shift_fst whd in match (seq_of_labeled_statement ?);
    1043     cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
     1045    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    10441046    #tr' * #s2' * * #P #T #S
    10451047    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
     
    11031105lemma state_with_labels_call : ∀f,a,k,m,s1.
    11041106 state_with_labels (Callstate f a k m) s1 →
    1105  ∃k'. cont_with_labels k k' ∧ s1 = Callstate (label_fundef f) a k' m.
     1107 ∃k'. cont_with_labels k k' ∧ ∃u0. s1 = Callstate (\fst (label_fundef u0 f)) a k' m.
    11061108#f #a #k #m #s1 #S inversion S
    11071109[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
     
    11101112  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
    11111113  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
    1112   | #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % //
     1114  | #u0 #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
    11131115  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
    11141116  | #H72 #H73 #H74 #H75 destruct
     
    11181120
    11191121lemma interactive_step_with_labels : ∀ge,ge'.
    1120   related_globals … label_fundef ge ge' →
     1122  related_globals_gen … label_fundef ge ge' →
    11211123  ∀s1,s1',o,k.
    11221124  exec_step ge s1 = Interact … o k →
     
    11351137destruct
    11361138#S cases (state_with_labels_call … S)
    1137 #k'' * #K #E2 destruct
     1139#k'' * #K * #u0 #E2 destruct
    11381140whd in EX:(??%?);
    11391141@(bindIO_res_interact ?????????? EX) -EX
     
    11591161lemma initial_state_in_simulation : ∀p,s.
    11601162  make_initial_state p = OK ? s →
    1161   ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'.
     1163  ∃s'. make_initial_state (\fst (clight_label p)) = OK ? s' ∧ state_with_labels s s'.
    11621164* #vars #fns #main #s
    11631165whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
     
    11681170whd in match (make_initial_state ?);
    11691171letin ge' ≝ (make_global ?)
    1170 cut (related_globals … label_fundef ge ge')
     1172cut (related_globals_gen … label_fundef ge ge')
    11711173[ // ] #RG
     1174cases (rgg_find_funct_ptr … RG … Emain') #u' #FFP
    11721175% [2: %
    11731176[ whd in ⊢ (??%?);
    11741177  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
    1175   >init_mem_transf >Em in ⊢ (??%?);
    1176   whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
    1177   whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
     1178  >(init_mem_transf_gen … (mk_program ?? vars fns main)) >Em in ⊢ (??%?);
     1179  whd in ⊢ (??%?); <(rgg_find_symbol … RG) >Emain in ⊢ (??%?);
     1180  whd in ⊢ (??%?); >FFP in ⊢ (??%?);
    11781181  whd in ⊢ (??%?); @refl
    11791182| /3/
     
    11941197let corec build_exec
    11951198  (ge1,ge2:genv)
    1196   (RG:related_globals … label_fundef ge1 ge2)
     1199  (RG:related_globals_gen … label_fundef ge1 ge2)
    11971200  (s1,s2:state)
    11981201  (S:state_with_labels s1 s2)
     
    12731276
    12741277whd in match (exec_inf ????);
    1275 letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p))
    1276 change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p));
     1278letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p)))
     1279change with (make_initial_state (\fst (clight_label p))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p)));
    12771280>I2
    12781281
     
    12901293@(swl_steps E0 E0)
    12911294[ 2: @steps_step | skip | // | @build_exec
    1292   [ @transform_program_related | // | inversion NW
     1295  [ @transform_program_gen_related | // | inversion NW
    12931296    [ #tr #i #s #E1 #E2 destruct
    12941297    | #trX #sX #eX #NWX #E1X #E2X destruct //
  • src/Clight/labelSpecification.ma

    r2202 r2319  
    3232∀p:clight_program.
    3333  let e1 ≝ exec_inf … clight_fullexec p in
    34   let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
     34  let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label p)) in
    3535  not_wrong state e1 →
    3636  sim_with_labels e1 e2.
  • src/Cminor/initialisation.ma

    r2252 r2319  
    7777] qed.
    7878
    79 definition add_statement : ident → (Σs:stmt. stmt_inv s) →
     79(* FIXME: we need to add a new initialisation function instead of augmenting
     80   main, because this currently breaks a recursive main function. *)
     81
     82definition add_statement : costlabel → ident → (Σs:stmt. stmt_inv s) →
    8083                              list (ident × (fundef internal_function)) →
    8184                              list (ident × (fundef internal_function)) ≝
    82 λid,s. match s with [ mk_Sig s H ⇒
     85λcost,id,s. match s with [ mk_Sig s H ⇒
    8386  map ??
    8487    (λidf.
     
    9396                                           (f_distinct f)
    9497                                           (f_stacksize f)
    95                                            (St_seq s (f_body f))
     98                                           (St_cost cost (St_seq s (f_body f)))
    9699                                           ?)〉
    97100          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
     
    101104[ % //
    102105| %
    103   [ @(stmt_P_mp … H) #s * * #V #L #R %
     106 [ % //
     107 | % [ @(stmt_P_mp … H) #s * * #V #L #R %
    104108    [ @(stmt_vars_mp … V) #i #t *
    105109    | @(stmt_labels_mp … L) #l *
     
    108112  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    109113  ]
     114 ]
    110115] qed.
    111116
     
    115120              size_init_data_list (\snd v)〉).
    116121
    117 definition replace_init : Cminor_program → Cminor_noinit_program ≝
    118 λp.
     122definition replace_init : costlabel → Cminor_program → Cminor_noinit_program ≝
     123λcost,p.
    119124  mk_program ??
    120125    (empty_vars (prog_vars ?? p))
    121     (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
     126    (add_statement cost (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
    122127    (prog_main ?? p).
  • src/Cminor/toRTLabs.ma

    r2292 r2319  
    937937include "Cminor/initialisation.ma".
    938938
    939 definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
    940 λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
     939definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
     940λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.
  • src/common/AST.ma

    r2286 r2319  
    348348    (transf_program ?? (transf ?) (prog_funct A V p))
    349349    (prog_main A V p).
     350
     351(* Versions of the above that thread a fresh name generator through the
     352   transformation. *)
     353
     354definition transf_program_gen : ∀tag,A,B. universe tag →
     355  (universe tag → A → B × (universe tag)) →
     356  list (ident × A) →
     357  list (ident × B) × (universe tag) ≝
     358λtag,A,B,gen,transf,l.
     359  foldr ?? (λid_fn,bs_gen. let 〈fn',gen'〉 ≝ transf (\snd bs_gen) (\snd id_fn) in
     360                      〈〈\fst id_fn, fn'〉::(\fst bs_gen), gen'〉) 〈[ ], gen〉 l.
     361
     362lemma transf_program_gen_step : ∀tag,A,B,gen,transf,id,fn,tl.
     363  ∃gen'.
     364    \fst (transf_program_gen tag A B gen transf (〈id,fn〉::tl)) =
     365    〈id, \fst (transf gen' fn)〉::(\fst (transf_program_gen tag A B gen transf tl)).
     366#tag #A #B #gen #transf #id #fn #tl
     367whd in ⊢ (??(λ_.??(???%)?));
     368change with (transf_program_gen ??????) in match (foldr ?????);
     369cases (transf_program_gen ??????) #tl' #gen'
     370%{gen'} cases (transf gen' fn) //
     371qed.
     372
     373definition transform_program_gen : ∀tag,A,B,V. universe tag → ∀p:program A V.
     374  (∀varnames. universe tag → A varnames → B varnames × (universe tag)) →
     375  program B V × (universe tag) ≝
     376λtag,A,B,V,gen,p,trans.
     377  let fsg ≝ transf_program_gen tag ?? gen (trans ?) (prog_funct A V p) in
     378  〈mk_program B V
     379    (prog_vars A V p)
     380    (\fst fsg)
     381    (prog_main A V p), \snd fsg〉.
     382
     383
    350384(*
    351385lemma transform_program_function:
     
    748782] qed.
    749783
     784lemma transform_program_gen_match:
     785  ∀A,B,V,tag,gen.
     786    ∀trans_function: ∀vs. universe tag → A vs → B vs × (universe tag).
     787    ∀p: program A V.
     788  match_program (mk_matching A B V V
     789    (λvs,fd,tfd. ∃g,g'. trans_function vs g fd = 〈tfd,g'〉)
     790    (λv,w. v = w))
     791    p (\fst (transform_program_gen … gen p trans_function)).
     792#A #B #V #tag #gen #tf
     793* #vars #fns #main
     794%
     795[ normalize elim vars // * * #id #r #v #tl #H % /2/
     796| whd in match (prog_var_names ???);
     797  whd in match (prog_vars ???);
     798  whd in match (transform_program_gen ???????);
     799  generalize in match gen;
     800  elim fns
     801  [ //
     802  | * #id #f #tl #IH #g
     803    cases (transf_program_gen_step tag (A ?) (B ?) g (tf ?) id f tl)
     804    #g' #E >E % /4/
     805  ]
     806| //
     807] qed.
     808
    750809(* * * External functions *)
    751810
  • src/common/Globalenvs.ma

    r2226 r2319  
    770770//
    771771qed.
     772
     773lemma
     774  init_mem_transf_gen:
     775    ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V.
     776    init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p.
     777#tag #A #B #C #iV #g #transf #p
     778@(init_mem_match … (transform_program_gen_match … transf ?))
     779//
     780qed.
    772781   
    773782
     
    791800| @(find_funct_transf A B V iV tf p)
    792801| @(find_funct_ptr_transf A B V iV p tf)
     802] qed.
     803
     804record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     805  rgg_find_symbol: ∀s.
     806    find_symbol … ge s = find_symbol … ge' s;
     807  rgg_find_funct_ptr: ∀b,f.
     808    find_funct_ptr … ge b = Some ? f →
     809    ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f));
     810  rgg_find_funct: ∀v,f.
     811    find_funct … ge v = Some ? f →
     812    ∃g. find_funct … ge' v = Some ? (\fst (t g f))
     813}.
     814
     815include "utilities/bool.ma".
     816
     817theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
     818  related_globals_gen tag (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (\fst (transform_program_gen tag A B V g p tf))).
     819#tag #A #B #V #iV #g #p #tf %
     820[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
     821  #v #w * //
     822| #b #f #FFP
     823  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
     824  [ 2: @iV
     825  | #fn' * #FFP'
     826    generalize in match (matching_vars ????);
     827    whd in match (prog_var_names ???); whd in match (prog_vars ???);
     828    #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' %
     829  | skip
     830  ]
     831| * [5: #ptr #fn whd in match (find_funct ???);
     832     @if_elim #Eoff #FFP
     833     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
     834       [ 2: @iV
     835       | #fn' * #FFP'
     836         generalize in match (matching_vars ????);
     837         whd in match (prog_var_names ???); whd in match (prog_vars ???);
     838         #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E'
     839         %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' %
     840       ]
     841     | destruct
     842     ]
     843    | *: normalize #A #B try #C try #D destruct
     844    ]
    793845] qed.
    794846
  • src/compiler.ma

    r2291 r2319  
    77include "Cminor/toRTLabs.ma".
    88
    9 definition front_end : clight_program → res (clight_program × RTLabs_program) ≝
     9definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
    1010λp.
    11   let p' ≝ clight_label p in
     11  let 〈p',init_cost〉 ≝ clight_label p in
    1212  let p ≝ simplify_program p' in
    1313(*  let p ≝ program_switch_removal p in*)
    1414  ! p ← clight_to_cminor p;
    15   let p ≝ cminor_to_rtlabs p in
    16   return 〈p',p〉.
     15  let p ≝ cminor_to_rtlabs init_cost p in
     16  return 〈init_cost,p',p〉.
    1717
    1818include "RTLabs/RTLabsToRTL.ma".
Note: See TracChangeset for help on using the changeset viewer.