Changeset 2390


Ignore:
Timestamp:
Oct 5, 2012, 12:57:20 PM (8 years ago)
Author:
campbell
Message:

Tidy up a corner case when generating RTLabs so that we generate
less skips.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2335 r2390  
    286286| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
    287287] qed.
     288
     289(* Change the entry point to the function (i.e., the successor for any new
     290   instructions that we add). *)
     291definition change_entry : ∀fx. ∀f:partial_fn fx.
     292  ∀l. present ?? (pf_graph … f) l →
     293  Σf':partial_fn fx. fn_contains … f f' ≝
     294λfx,f,l,PR.
     295  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
     296                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     297                (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f)
     298                (pf_labels … f) (pf_typed … f)
     299                «l, PR» (pf_exit … f).
     300% //
     301qed.
    288302
    289303(* Add a statement with a fresh label to the start of the function.  The
     
    740754    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
    741755    let l2 ≝ pf_entry … f2 in
    742     let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
     756    let f ≝ change_entry … f2 l_next ? in
    743757    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
    744758    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
     
    798812| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
    799813| #l whd % [2: @(pi2 ?? r) | skip ]
    800 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
     814| @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    801815| cases (pi2 … f) * #INC #ENV #LBLE #LBLA %
    802816  [ @INC | @ENV | @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
Note: See TracChangeset for help on using the changeset viewer.