- Timestamp:
- Apr 27, 2011, 5:25:26 PM (10 years ago)
- Location:
- src
- Files:
-
- 1 added
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/I8051.ma
r757 r777 6 6 include "ASM/Arithmetic.ma". 7 7 include "utilities/Compare.ma". 8 9 definition int_size ≝ bitvector_of_nat 8 1. 10 definition ptr_size ≝ bitvector_of_nat 8 2. 11 definition alignment ≝ None. 8 12 9 13 (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps … … 125 129 ]. 126 130 127 definition eq_ register: Register → Register → bool ≝131 definition eq_Register: Register → Register → bool ≝ 128 132 λr, s: Register. 129 133 let r_as_nat ≝ nat_of_register r in … … 178 182 [ RegisterSST; RegisterST0; RegisterST1; 179 183 RegisterSPL; RegisterSPH ]. 184 185 definition parameters: list Register ≝ 186 [ Register30; Register31; Register32; Register33; 187 Register34; Register35; Register36; Register37 ]. 180 188 181 189 record RegisterMap: Type[0] ≝ -
src/ASM/Util.ma
r764 r777 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 5 let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ 6 match n with 7 [ O ⇒ 8 match l with 9 [ nil ⇒ [ ] 10 | cons hd tl ⇒ l 11 ] 12 | S n ⇒ 13 match l with 14 [ nil ⇒ [ ] 15 | cons hd tl ⇒ 16 hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n 17 ] 18 ]. 19 20 definition nub_by ≝ 21 λA: Type[0]. 22 λf: A → A → bool. 23 λl: list A. 24 nub_by_internal A f l (length ? l). 25 26 let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝ 27 match l with 28 [ nil ⇒ false 29 | cons hd tl ⇒ orb (eq a hd) (member A eq a tl) 30 ]. 31 32 let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝ 33 match n with 34 [ O ⇒ [ ] 35 | S n ⇒ 36 match l with 37 [ nil ⇒ [ ] 38 | cons hd tl ⇒ hd :: take A n tl 39 ] 40 ]. 41 42 let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝ 43 match n with 44 [ O ⇒ l 45 | S n ⇒ 46 match l with 47 [ nil ⇒ [ ] 48 | cons hd tl ⇒ drop A n tl 49 ] 50 ]. 51 52 definition list_split ≝ 53 λA: Type[0]. 54 λn: nat. 55 λl: list A. 56 〈take A n l, drop A n l〉. 57 58 let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B) 59 (l: list A) on l: list B ≝ 60 match l with 61 [ nil ⇒ nil ? 62 | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl) 63 ]. 64 65 definition mapi ≝ 66 λA, B: Type[0]. 67 λf: nat → A → B. 68 λl: list A. 69 mapi_internal A B 0 f l. 70 71 let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ 72 match l with 73 [ nil ⇒ Some ? (nil (A × B)) 74 | cons hd tl ⇒ 75 match r with 76 [ nil ⇒ None ? 77 | cons hd' tl' ⇒ 78 match zip ? ? tl tl' with 79 [ None ⇒ None ? 80 | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail) 81 ] 82 ] 83 ]. 4 84 5 85 let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝ -
src/ERTL/ERTL.ma
r759 r777 6 6 include "common/Registers.ma". 7 7 8 inductive abstract_register: Type[0] ≝ 9 mk_abstract_register: Word → abstract_register. 10 11 definition abstract_registers ≝ list abstract_register. 12 8 definition hardware_register ≝ Register. 13 9 definition registers ≝ list register. 14 10 … … 17 13 | ertl_st_comment: String → label → ertl_statement 18 14 | ertl_st_cost: costlabel → label → ertl_statement 19 | ertl_st_get_hdw: register → abstract_register → label → ertl_statement20 | ertl_st_set_hdw: abstract_register → register → label → ertl_statement21 | ertl_st_hdw_to_hdw: register →register → label → ertl_statement15 | ertl_st_get_hdw: register → hardware_register → label → ertl_statement 16 | ertl_st_set_hdw: hardware_register → register → label → ertl_statement 17 | ertl_st_hdw_to_hdw: hardware_register → hardware_register → label → ertl_statement 22 18 | ertl_st_new_frame: label → ertl_statement 23 19 | ertl_st_del_frame: label → ertl_statement 24 | ertl_st_frame_size: abstract_register → label → ertl_statement25 | ertl_st_pop: abstract_register → label → ertl_statement26 | ertl_st_push: abstract_register → label → ertl_statement27 | ertl_st_addr_h: abstract_register → label → label → ertl_statement28 | ertl_st_addr_l: abstract_register → label → label → ertl_statement29 | ertl_st_int: abstract_register → Byte → label → ertl_statement30 | ertl_st_move: abstract_register → abstract_register → label → ertl_statement31 | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → label → ertl_statement32 | ertl_st_op1: Op1 → abstract_register → abstract_register → label → ertl_statement33 | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → label → ertl_statement20 | ertl_st_frame_size: register → label → ertl_statement 21 | ertl_st_pop: register → label → ertl_statement 22 | ertl_st_push: register → label → ertl_statement 23 | ertl_st_addr_h: register → label → label → ertl_statement 24 | ertl_st_addr_l: register → label → label → ertl_statement 25 | ertl_st_int: register → Byte → label → ertl_statement 26 | ertl_st_move: register → register → label → ertl_statement 27 | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement 28 | ertl_st_op1: Op1 → register → register → label → ertl_statement 29 | ertl_st_op2: Op2 → register → register → register → label → ertl_statement 34 30 | ertl_st_clear_carry: label → ertl_statement 35 | ertl_st_load: abstract_register → abstract_register → abstract_register → label → ertl_statement36 | ertl_st_store: abstract_register → abstract_register → abstract_register → label → ertl_statement31 | ertl_st_load: register → register → register → label → ertl_statement 32 | ertl_st_store: register → register → register → label → ertl_statement 37 33 | ertl_st_call_id: label → Byte → label → ertl_statement 38 | ertl_st_cond_acc: abstract_register → label → label → ertl_statement39 | ertl_st_return: abstract_registers → ertl_statement.34 | ertl_st_cond_acc: register → label → label → ertl_statement 35 | ertl_st_return: registers → ertl_statement. 40 36 41 37 definition ertl_statement_graph ≝ graph ertl_statement. -
src/ERTL/Uses.ma
r756 r777 9 9 λuses. 10 10 let l ≝ increment ? (lookup ? ? register uses (zero 16)) in 11 insert ? 16 registerl uses.11 insert ? 16 l uses. 12 12 13 13 definition examine_statement ≝ -
src/RTL/RTLtoERTL.ma
r763 r777 1 1 include "RTL/RTL.ma". 2 2 include "ERTL/ERTL.ma". 3 include "ASM/RegisterSet.ma". 3 4 4 5 definition change_exit_label ≝ … … 47 48 definition fresh_label ≝ 48 49 λdef. 49 fresh LabelTag (ertl_if_luniverse def). 50 match fresh LabelTag (ertl_if_luniverse def) with 51 [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ) 52 | Error ⇒ None ? 53 ]. 50 54 51 55 definition change_label ≝ … … 88 92 let tmp_lbl ≝ fresh_label def in 89 93 match tmp_lbl with 90 [ OK o ⇒ 91 let 〈lbl, univ〉 ≝ o in 92 let stmt ≝ change_label lbl hd in 94 [ Some tmp_lbl ⇒ 95 let stmt ≝ change_label tmp_lbl hd in 93 96 let def ≝ add_graph start_lbl hd def in 94 adds_graph tl lbl dest_lbl def95 | Error⇒ None ?97 adds_graph tl tmp_lbl dest_lbl def 98 | None ⇒ None ? 96 99 ] 97 100 ] 98 101 ]. 99 102 100 let rec add_translates (translate_list: list (label → label → ertl_internal_function → ertl_internal_function))103 let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function)) 101 104 (start_lbl: label) (dest_lbl: label) 102 105 (def: ertl_internal_function): option ertl_internal_function ≝ … … 105 108 | cons hd tl ⇒ 106 109 match tl with 107 [ nil ⇒ Some ? (hd start_lbl dest_lbl def)110 [ nil ⇒ hd start_lbl dest_lbl def 108 111 | _ ⇒ 109 112 let tmp_lbl ≝ fresh_label def in 110 113 match tmp_lbl with 111 [ OK o ⇒ 112 let 〈lbl, univ〉 ≝ o in 113 let def ≝ hd start_lbl lbl def in 114 add_translates tl lbl dest_lbl def 115 | Error ⇒ None ? 114 [ Some tmp_lbl ⇒ 115 match hd start_lbl tmp_lbl def with 116 [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def 117 | None ⇒ None ? 118 ] 119 | None ⇒ None ? 116 120 ] 117 121 ] … … 129 133 ]. 130 134 135 definition save_hdws_internal ≝ 136 λdestr_srcr: register × hardware_register. 137 λstart_lbl: label. 138 let 〈destr, srcr〉 ≝ destr_srcr in 139 adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl. 140 131 141 definition save_hdws ≝ 132 λ 142 λl. 143 map ? ? save_hdws_internal l. 144 145 definition restore_hdws_internal ≝ 146 λdestr_srcr: hardware_register × register. 147 λstart_lbl: label. 148 let 〈destr, srcr〉 ≝ destr_srcr in 149 adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl. 150 151 definition swap_components ≝ 152 λA, B: Type[0]. 153 λp: A × B. 154 let 〈l, r〉 ≝ p in 155 〈r, l〉. 156 157 definition restore_hdws ≝ 158 λl. 159 map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l). 160 161 definition get_params_hdw_internal ≝ 162 λstart_lbl: label. 163 adds_graph [ ertl_st_skip start_lbl ] start_lbl. 164 165 definition get_params_hdw ≝ 166 λparams: list register. 167 match length ? params with 168 [ O ⇒ Some ? [ get_params_hdw_internal ] 169 | _ ⇒ 170 match zip ? ? params parameters with 171 [ None ⇒ None ? 172 | Some l ⇒ Some ? (save_hdws l) 173 ] 174 ]. 175 176 definition get_param_stack ≝ 177 λoff: nat. 178 λdestr. 179 λstart_lbl, dest_lbl: label. 180 λdef. 181 let 〈def, addr1〉 ≝ fresh_reg def in 182 let 〈def, addr2〉 ≝ fresh_reg def in 183 let 〈def, tmpr〉 ≝ fresh_reg def in 184 let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in 185 adds_graph [ 186 ertl_st_frame_size addr1 start_lbl; 187 ertl_st_int tmpr int_offset start_lbl; 188 ertl_st_op2 Sub addr1 addr1 tmpr start_lbl; 189 ertl_st_get_hdw tmpr RegisterSPL start_lbl; 190 ertl_st_op2 Add addr1 addr1 tmpr start_lbl; 191 ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl; 192 ertl_st_get_hdw tmpr RegisterSPH start_lbl; 193 ertl_st_op2 Addc addr2 addr2 tmpr start_lbl; 194 ertl_st_load destr addr1 addr2 start_lbl 195 ] start_lbl dest_lbl def. 196 197 definition get_params_stack_internal ≝ 198 λi. 199 λr. 200 get_param_stack i r. 201 202 definition get_params_stack ≝ 203 λparams. 204 match length ? params with 205 [ O ⇒ [ get_params_hdw_internal ] 206 | _ ⇒ mapi ? ? get_params_stack_internal params 207 ]. 208 209 definition get_params ≝ 210 λparams. 211 let n ≝ min (length ? params) (length ? parameters) in 212 let 〈hdw_params, stack_params〉 ≝ list_split ? n params in 213 match get_params_hdw hdw_params with 214 [ None ⇒ None ? 215 | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params)) 216 ]. 217 218 definition add_prologue ≝ 219 λparams. 220 λsral. 221 λsrah. 222 λsregs. 223 λdef. 224 let start_lbl ≝ ertl_if_entry def in 225 let tmp_lbl ≝ fresh_label def in 226 match tmp_lbl with 227 [ None ⇒ None ? 228 | Some tmp_lbl ⇒ 229 let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in 230 let params ≝ 231 match get_params params with 232 [ Some params ⇒ params 233 | None ⇒ [ ] (* dpm: is this ok? *) 234 ] in 235 let def ≝ 236 add_translates ( 237 adds_graph [ ertl_st_new_frame start_lbl ] :: 238 adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] :: 239 save_hdws sregs @ 240 params) start_lbl tmp_lbl def in 241 match def with 242 [ Some def ⇒ 243 match last_stmt with 244 [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def) 245 | None ⇒ None ? 246 ] 247 | None ⇒ None ? 248 ] 249 ]. 250 251 definition allocate_regs_internal ≝ 252 λr: register. 253 λdef_sregs. 254 let 〈def, sregs〉 ≝ def_sregs in 255 let 〈def, r'〉 ≝ fresh_reg def in 256 〈def, 〈r', r〉 :: sregs〉. 257 258 definition allocate_regs ≝ 259 λrs: register_set. 260 λsaved: rs_set rs. 261 λdef. 262 rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. 263 264 definition save_return_internal ≝ 265 λr. 266 λstart_lbl. 267 λdest_lbl. 268 λdef. 269 let 〈def, r_tmp〉 ≝ fresh_reg def in 270 adds_graph [ 271 ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl; 272 ertl_st_set_hdw RegisterST0 r start_lbl; 273 ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def. 274 275 definition save_return_internal' ≝ 276 λr1, r2. 277 λstart_lbl. 278 adds_graph [ 279 ertl_st_set_hdw RegisterST0 r1 start_lbl; 280 ertl_st_set_hdw RegisterST1 r2 start_lbl 281 ] start_lbl. 282 283 definition save_return ≝ 284 λret_regs. 285 match ret_regs with 286 [ nil ⇒ [ get_params_hdw_internal ] 287 | cons hd tl ⇒ 288 match tl with 289 [ nil ⇒ [ save_return_internal hd ] 290 | cons hd' tl' ⇒ [ save_return_internal' hd hd' ] 291 ] 292 ]. 293 294 definition add_epilogue ≝ 295 λret_regs. 296 λsral. 297 λsrah. 298 λsregs. 299 λdef. 300 let start_lbl ≝ ertl_if_exit def in 301 let tmp_lbl ≝ fresh_label def in 302 match tmp_lbl with 303 [ None ⇒ None ? 304 | Some tmp_lbl ⇒ 305 let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in 306 match last_stmt with 307 [ None ⇒ None ? 308 | Some last_stmt ⇒ 309 let def ≝ 310 add_translates ( 311 save_return ret_regs @ 312 restore_hdws sregs @ 313 [adds_graph [ 314 ertl_st_push srah start_lbl; 315 ertl_st_push sral start_lbl 316 ]] @ 317 [adds_graph [ 318 ertl_st_del_frame start_lbl 319 ]] @ 320 [adds_graph [ 321 ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl; 322 ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl 323 ]]) start_lbl tmp_lbl def in 324 match def with 325 [ None ⇒ None ? 326 | Some def ⇒ 327 let def ≝ add_graph tmp_lbl last_stmt def in 328 Some ? (change_exit_label tmp_lbl def) 329 ] 330 ] 331 ]. 332 333 definition add_pro_and_epilogue ≝ 334 λrs: register_set. 335 λparams. 336 λret_args. 337 λdef. 338 let 〈def, sra〉 ≝ fresh_regs def 2 in 339 let sral ≝ nth ? 0 sra in 340 let srah ≝ nth sra 1 in 341 let 〈def, sregs〉 ≝ allocate_regs callee_saved def in 342 let def ≝ add_prologue params sral srah sregs def in 343 let def ≝ add_epilogue ret_args sral srah sregs def in 344 def. -
src/common/Registers.ma
r757 r777 18 18 (* dpm: fix the Register/register mismatch *) 19 19 axiom Register_of_register: register → Register. 20 axiom register_of_Register: Register → register.
Note: See TracChangeset
for help on using the changeset viewer.