Changeset 2319 for src/Clight


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (8 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/Clight
Files:
3 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.
Note: See TracChangeset for help on using the changeset viewer.