Changeset 1070 for src/Cminor
 Timestamp:
 Jul 15, 2011, 12:56:48 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r1056 r1070 26 26 mk_internal_function (f_labgen f) (f_reggen f) 27 27 (f_result f) (f_params f) (f_locals f) 28 (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f). 28 (f_stacksize f) (add ?? (f_graph f) l s) 29 (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). 30 @lookup_add_oblivious [ cases (f_entry f)  cases (f_exit f) ] // 31 qed. 29 32 30 33 (* Add a statement to the graph, making it the entry label. *) … … 33 36 mk_internal_function (f_labgen f) (f_reggen f) 34 37 (f_result f) (f_params f) (f_locals f) 35 (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f). 38 (f_stacksize f) (add ?? (f_graph f) l s) 39 (dp ?? l ?) (dp ?? (f_exit f) ?). 40 [ %{s} @lookup_add_hit 41  @lookup_add_oblivious cases (f_exit f) // 42 ] qed. 36 43 37 44 (* Add a statement with a fresh label to the start of the function. The … … 43 50 (mk_internal_function g (f_reggen f) 44 51 (f_result f) (f_params f) (f_locals f) 45 (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)). 46 52 (f_stacksize f) (add ?? (f_graph f) l s') 53 (dp ?? l ?) (dp ?? (f_exit f) ?)). 54 [ %{s'} @lookup_add_hit 55  @lookup_add_oblivious cases (f_exit f) // 56 ] qed. 57 (* 47 58 (* Generate a fresh label and use it as a dangling entry point, to be filled in 48 59 later with the loop head. *) … … 53 64 (f_result f) (f_params f) (f_locals f) 54 65 (f_stacksize f) (f_graph f) l (f_exit f)). 55 66 *) 56 67 definition fresh_reg : internal_function → typ → register × internal_function ≝ 57 68 λf,ty. … … 189 200 add_expr env ? e r f 190 201  St_loop s ⇒ 191 let f ≝ add_ loop_label_to_graph f in202 let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *) 192 203 let l_loop ≝ f_entry f in 193 204 do f ← add_stmt env label_env s exits f; … … 235 246 [ @(λ_. St_skip l_next) 236 247  @(St_skip (f_entry f)) 248  @St_skip 237 249  @(λ_. St_skip l) 238 250  @(λ_. St_skip l_default) … … 284 296 OK ? f 285 297 . 298 % [2,4: @lookup_add_hit  *: skip ] 299 qed. 286 300 287 301 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
Note: See TracChangeset
for help on using the changeset viewer.