 Timestamp:
 Oct 5, 2012, 12:57:20 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r2335 r2390 286 286  % [ #l' @lookup_add_oblivious  //  cases (pf_labels fx f) /2/ ] 287 287 ] qed. 288 289 (* Change the entry point to the function (i.e., the successor for any new 290 instructions that we add). *) 291 definition 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 % // 301 qed. 288 302 289 303 (* Add a statement with a fresh label to the start of the function. The … … 740 754 let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in 741 755 let l2 ≝ pf_entry … f2 in 742 let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in756 let f ≝ change_entry … f2 l_next ? in 743 757 let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in 744 758 let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in … … 798 812  #l #H % [ @H  @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ] 799 813  #l whd % [2: @(pi2 ?? r)  skip ] 800  #l #H@(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I814  @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I 801 815  cases (pi2 … f) * #INC #ENV #LBLE #LBLA % 802 816 [ @INC  @ENV  @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
Note: See TracChangeset
for help on using the changeset viewer.