 Timestamp:
 Jul 15, 2011, 2:40:40 PM (9 years ago)
 Location:
 src/RTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTL.ma
r1068 r1071 35 35 rtl_if_runiverse: universe RegisterTag; 36 36 (* rtl_if_sig: signature;  dropped in front end *) 37 rtl_if_result : registers;38 rtl_if_params : registers;39 rtl_if_locals : registers;37 rtl_if_result : registers; 38 rtl_if_params : registers; 39 rtl_if_locals : registers; 40 40 rtl_if_stacksize: nat; 41 rtl_if_graph : rtl_statement_graph;42 rtl_if_entry : label;43 rtl_if_exit : label41 rtl_if_graph : rtl_statement_graph; 42 rtl_if_entry : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?; 43 rtl_if_exit : Σl: label. lookup ? ? rtl_if_graph l ≠ None ? 44 44 }. 45 45 
src/RTL/RTLtoERTL.ma
r783 r1071 1 1 include "RTL/RTL.ma". 2 include "RTL/RTLTailcall.ma". 2 (* include "RTL/RTLTailcall.ma". *) 3 3 include "ERTL/ERTL.ma". 4 include "utilities/RegisterSet.ma".5 4 6 5 definition change_exit_label ≝ … … 52 51 definition fresh_label ≝ 53 52 λdef. 54 match fresh LabelTag (ertl_if_luniverse def) with 55 [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ) 56  Error ⇒ None ? 57 ]. 53 fresh LabelTag (ertl_if_luniverse def). 58 54 59 55 definition change_label ≝ … … 76 72  ertl_st_int r i _ ⇒ ertl_st_int r i l 77 73  ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l 78  ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l 74  ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l 75  ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l 79 76  ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l 80 77  ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l 81 78  ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l 79  ertl_st_set_carry _ ⇒ ertl_st_set_carry l 82 80  ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l 83 81  ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l 84 82  ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l 85  ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2 86  ertl_st_return a ⇒ ertl_st_return a 87 ]. 88 89 let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝ 83  ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2 84  ertl_st_return ⇒ ertl_st_return 85 ]. 86 87 let rec adds_graph 88 (stmt_list: list ertl_statement) (start_lbl: label) 89 (dest_lbl: label) (def: ertl_internal_function) 90 on stmt_list ≝ 90 91 match stmt_list with 91 [ nil ⇒ Some ?def92  cons hd tl⇒93 match tlwith94 [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)92 [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def 93  cons stmt stmt_list ⇒ 94 match stmt_list with 95 [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def 95 96  _ ⇒ 96 let tmp_lbl ≝ fresh_label def in 97 match tmp_lbl with 98 [ Some tmp_lbl ⇒ 99 let stmt ≝ change_label tmp_lbl hd in 100 let def ≝ add_graph start_lbl hd def in 101 adds_graph tl tmp_lbl dest_lbl def 102  None ⇒ None ? 103 ] 104 ] 105 ]. 106 107 let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function)) 108 (start_lbl: label) (dest_lbl: label) 109 (def: ertl_internal_function): option ertl_internal_function ≝ 97 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 98 let stmt ≝ change_label tmp_lbl stmt in 99 let def ≝ add_graph start_lbl stmt def in 100 adds_graph stmt_list tmp_lbl dest_lbl def 101 ] 102 ]. 103 104 let rec add_translates 105 (translate_list: list ?) (start_lbl: label) (dest_lbl: label) 106 (def: ertl_internal_function) 107 on translate_list ≝ 110 108 match translate_list with 111 [ nil ⇒ Some ?def112  cons hd tl⇒113 match t lwith114 [ nil ⇒ hdstart_lbl dest_lbl def109 [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def 110  cons trans translate_list ⇒ 111 match translate_list with 112 [ nil ⇒ trans start_lbl dest_lbl def 115 113  _ ⇒ 116 let tmp_lbl ≝ fresh_label def in 117 match tmp_lbl with 118 [ Some tmp_lbl ⇒ 119 match hd start_lbl tmp_lbl def with 120 [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def 121  None ⇒ None ? 122 ] 123  None ⇒ None ? 124 ] 125 ] 126 ]. 127 128 axiom fresh_reg: ertl_internal_function → ertl_internal_function × register. 129 130 let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝ 114 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 115 let def ≝ trans start_lbl tmp_lbl def in 116 add_translates translate_list tmp_lbl dest_lbl def 117 ] 118 ]. 119 120 axiom register_fresh: universe RegisterTag → register. 121 122 definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝ 123 λdef. 124 let r ≝ register_fresh (ertl_if_runiverse def) in 125 let locals ≝ r :: ertl_if_locals def in 126 let ertl_if_luniverse' ≝ ertl_if_luniverse def in 127 let ertl_if_runiverse' ≝ ertl_if_runiverse def in 128 let ertl_if_params' ≝ ertl_if_params def in 129 let ertl_if_locals' ≝ locals in 130 let ertl_if_stacksize' ≝ ertl_if_stacksize def in 131 let ertl_if_graph' ≝ ertl_if_graph def in 132 let ertl_if_entry' ≝ ertl_if_entry def in 133 let ertl_if_exit' ≝ ertl_if_exit def in 134 〈mk_ertl_internal_function 135 ertl_if_luniverse' ertl_if_runiverse' ertl_if_params' 136 ertl_if_locals' ertl_if_stacksize' ertl_if_graph' 137 ertl_if_entry' ertl_if_exit', r〉. 138 139 let rec fresh_regs 140 (def: ertl_internal_function) (n: nat) 141 on n ≝ 131 142 match n with 132 143 [ O ⇒ 〈def, [ ]〉 … … 169 180 definition get_params_hdw ≝ 170 181 λparams: list register. 171 match length ?params with172 [ O ⇒ Some ? [ get_params_hdw_internal]182 match params with 183 [ nil ⇒ [get_params_hdw_internal] 173 184  _ ⇒ 174 match zip ? ? params parameters with 175 [ None ⇒ None ? 176  Some l ⇒ Some ? (save_hdws l) 177 ] 185 let l ≝ zip_pottier ? ? params parameters in 186 save_hdws l 178 187 ]. 179 188 … … 186 195 let 〈def, addr2〉 ≝ fresh_reg def in 187 196 let 〈def, tmpr〉 ≝ fresh_reg def in 188 let 〈 int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in197 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 189 198 adds_graph [ 190 199 ertl_st_frame_size addr1 start_lbl; … … 199 208 ] start_lbl dest_lbl def. 200 209 201 definition get_params_stack_internal ≝202 λi.203 λr.204 get_param_stack i r.205 206 210 definition get_params_stack ≝ 207 211 λparams. 208 match length ? params with 209 [ O ⇒ [ get_params_hdw_internal ] 210  _ ⇒ mapi ? ? get_params_stack_internal params 212 match params with 213 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ] 214  _ ⇒ 215 let f ≝ λi. λr. get_param_stack i r in 216 mapi ? ? f params 211 217 ]. 212 218 … … 215 221 let n ≝ min (length ? params) (length ? parameters) in 216 222 let 〈hdw_params, stack_params〉 ≝ list_split ? n params in 217 match get_params_hdw hdw_params with 218 [ None ⇒ None ? 219  Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params)) 220 ]. 223 let hdw_params ≝ get_params_hdw hdw_params in 224 hdw_params @ (get_params_stack stack_params). 221 225 222 226 definition add_prologue ≝ 223 λparams .227 λparams: list register. 224 228 λsral. 225 229 λsrah. … … 227 231 λdef. 228 232 let start_lbl ≝ ertl_if_entry def in 229 let tmp_lbl ≝ fresh_label def in 230 match tmp_lbl with 231 [ None ⇒ None ? 232  Some tmp_lbl ⇒ 233 let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in 234 let params ≝ 235 match get_params params with 236 [ Some params ⇒ params 237  None ⇒ [ ] (* dpm: is this ok? *) 238 ] in 233 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 234 match lookup ? ? (ertl_if_graph def) start_lbl with 235 [ None ⇒ ? 236  Some last_stmt ⇒ 239 237 let def ≝ 240 add_translates ( 241 adds_graph [ ertl_st_new_frame start_lbl ] :: 242 adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] :: 243 save_hdws sregs @ 244 params) start_lbl tmp_lbl def in 245 match def with 246 [ Some def ⇒ 247 match last_stmt with 248 [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def) 249  None ⇒ None ? 250 ] 251  None ⇒ None ? 252 ] 253 ]. 238 add_translates 239 ((adds_graph [ 240 ertl_st_new_frame start_lbl 241 ]) :: 242 (adds_graph [ 243 ertl_st_pop sral start_lbl; 244 ertl_st_pop srah start_lbl 245 ]) :: 246 (save_hdws sregs) @ 247 (get_params params)) 248 start_lbl tmp_lbl def 249 in 250 add_graph tmp_lbl last_stmt def 251 ]. 252 cases not_implemented (* until Brian gives goahead for dep. types *) 253 qed. 254 255 definition save_return ≝ 256 λret_regs. 257 λstart_lbl: label. 258 λdest_lbl: label. 259 λdef: ertl_internal_function. 260 let 〈def, tmpr〉 ≝ fresh_reg def in 261 match reduce_strong ? RegisterSTS ret_regs with 262 [ dp crl crl_proof ⇒ 263 let commonl ≝ \fst (\fst crl) in 264 let commonr ≝ \fst (\snd crl) in 265 let restl ≝ \snd (\fst crl) in 266 let restr ≝ \snd (\snd crl) in 267 let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in 268 let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in 269 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 270 let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in 271 let defaults ≝ map ? ? f_default restl in 272 adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 273 ]. 274 275 let save_return ret_regs start_lbl dest_lbl def = 276 let (def, tmpr) = fresh_reg def in 277 let ((common1, rest1), (common2, _)) = 278 MiscPottier.reduce I8051.sts ret_regs in 279 let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in 280 let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in 281 let saves = List.map2 f_save common1 common2 in 282 let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in 283 let defaults = List.map f_default rest1 in 284 adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 254 285 255 286 definition allocate_regs_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.