Changeset 2708 for src/LIN/LINToASM.ma
 Timestamp:
 Feb 22, 2013, 7:11:30 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LINToASM.ma
r2490 r2708 3 3 include "LIN/LIN.ma". 4 4 include "ASM/ASM.ma". 5 include "utilities/state.ma". 6 7 (* utilities to provide Identifier's and addresses *) 8 record ASM_universe (globals : list ident) : Type[0] := 9 { id_univ : universe ASMTag 10 ; current_funct : ident 11 ; ident_map : identifier_map SymbolTag Identifier 12 ; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier) 13 ; address_map : identifier_map SymbolTag Word 14 ; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map 15 }. 16 17 definition new_ASM_universe : 18 ∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝ 19 λp. 20 let globals_addr_internal ≝ 21 λres_offset : identifier_map SymbolTag Word × Z. 22 λx_size: ident × region × nat. 23 let 〈res, offset〉 ≝ res_offset in 24 let 〈x, region, size〉 ≝ x_size in 25 〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in 26 let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in 27 mk_ASM_universe ? (mk_universe … one) 28 (an_identifier … one (* dummy *)) 29 (empty_map …) (empty_map …) 30 (\fst addresses) ?. 31 @hide_prf 32 normalize nodelta 33 cases p p #vars #functs #main 34 #i #H 35 letin init_val ≝ (〈empty_map ? Word, OZ〉) 36 cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars)) 37 [ %2{H} ] H 38 lapply i i lapply init_val init_val elim vars vars 39 [2: ** #id #r #v #tl #IH ] #init_val #i 40 [2: * [2: * ] #H @H ] 41 * [2: #H cases (orb_Prop_true … H) H ] #H 42 @IH 43 [ %1 cases init_val normalize nodelta #init_map #off 44 >(proj1 ?? (eqb_true ???) H) @mem_set_add_id 45  %2{H} 46  %1 cases init_val in H; normalize nodelta #init_map #off #H 47 >mem_set_add @orb_Prop_r @H 48 ] 49 qed. 50 51 definition Identifier_of_label : 52 ∀globals.label → state_monad (ASM_universe globals) Identifier ≝ 53 λg,l,u. 54 let current ≝ current_funct … u in 55 let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in 56 let 〈id, univ, lmap〉 ≝ 57 match lookup … lmap l with 58 [ Some id ⇒ 〈id, id_univ … u, lmap〉 59  None ⇒ 60 let 〈id, univ〉 ≝ fresh … (id_univ … u) in 61 〈id, univ, add … lmap l id〉 62 ] in 63 〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap) 64 (address_map … u) (globals_are_in … u), id〉. 65 66 definition Identifier_of_ident : 67 ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝ 68 λg,i,u. 69 let imap ≝ ident_map … u in 70 let 〈id, univ, imap〉 ≝ 71 match lookup … imap i with 72 [ Some id ⇒ 〈id, id_univ … u, imap〉 73  None ⇒ 74 let 〈id, univ〉 ≝ fresh … (id_univ … u) in 75 〈id, univ, add … imap i id〉 76 ] in 77 〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u) 78 (address_map … u) (globals_are_in … u), id〉. 79 80 definition start_funct_translation : 81 ∀globals.(ident × (joint_function LIN globals)) → 82 state_monad (ASM_universe globals) unit ≝ 83 λg,id_f,u. 84 〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u) 85 (address_map … u) (globals_are_in … u), it〉. 86 87 definition address_of_ident : 88 ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝ 89 λglobals,i,prf,u. 90 〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed. 91 92 definition ASM_fresh : 93 ∀globals.state_monad (ASM_universe globals) Identifier ≝ 94 λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in 95 〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u) 96 (address_map … u) (globals_are_in … u), id〉. 5 97 6 98 definition register_address: Register → [[ acc_a; direct; registr ]] ≝ … … 22 114 ]. @I qed. 23 115 24 let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))25 on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝26 match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with27 [ nil ⇒ Ⓧ28  cons hd tl ⇒29 λprf.30 If eq_A a (\fst hd) then \snd hd else with eq_prf do31 association … eq_A a tl ?32 ].33 elim (orb_Prop_true … prf)34 [ > eq_prf *35  # H36 assumption37 ]38 qed.39 40 definition association_ident ≝ association ident nat (eq_identifier ?).41 definition association_block ≝ association block Word eq_block.42 43 116 definition vector_cast : 44 117 ∀A,n,m.A → Vector A n → Vector A m ≝ … … 68 141 definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). 69 142 70 definition statement_labels ≝71 λg: list ident.72 λs: lin_statement g.73 let 〈label, instr〉 ≝ s in74 let generated ≝75 match instr with76 [ sequential instr' _ ⇒77 match instr' with78 [ step_seq instr'' ⇒79 match instr'' with80 [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }81  _ ⇒ ∅82 ]83  COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }84 ]85  final instr' ⇒86 match instr' with87 [ GOTO lbl ⇒ {(toASM_ident ? lbl)}88  _ ⇒ ∅89 ]90 ]91 in92 match label with93 [ None ⇒ generated94  Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)95 ].96 97 definition function_labels_internal ≝98 λglobals: list ident.99 λlabels: identifier_set ?.100 λstatement: lin_statement globals.101 labels ∪ (statement_labels globals statement).102 103 (* dpm: A = Identifier *)104 definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝105 λA: Type[0].106 λglobals: list ident.107 λf: A × (joint_function LIN globals).108 let 〈ignore, fun_def〉 ≝ f in109 match fun_def return λ_. identifier_set ? with110 [ Internal stmts ⇒111 foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)112  External _ ⇒ ∅113 ].114 115 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝116 λA: Type[0].117 λglobals: list ident.118 λlabels: identifier_set ?.119 λfunct: A × (joint_function LIN globals).120 labels ∪ (function_labels ? globals funct).121 122 (* CSC: here we are silently throwing away the region information *)123 definition program_labels ≝124 λprogram: lin_program.125 foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))126 ∅ (prog_funct … program).127 128 143 definition data_of_int ≝ λbv. DATA bv. 129 144 definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). … … 133 148 definition asm_other_bit ≝ BIT_ADDR (zero_byte). 134 149 135 definition translate_statements ≝136 λglobals: list (ident × nat).137 λglobals_old: list ident.138 λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).139 λ statement: joint_statement LIN globals_old.140 match statement 150 definition translate_statements : 151 ∀globals. 152 joint_statement LIN globals → 153 state_monad (ASM_universe globals) pseudo_instruction ≝ 154 λglobals,statement. 155 match statement with 141 156 [ final instr ⇒ 142 157 match instr with 143 [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) 144  RETURN ⇒ Instruction (RET ?) 158 [ GOTO lbl ⇒ 159 ! lbl' ← Identifier_of_label … lbl ; 160 return Jmp (toASM_ident ? lbl) 161  RETURN ⇒ return Instruction (RET ?) 145 162  TAILCALL abs _ _ ⇒ Ⓧabs 146 163 ] … … 152 169 match ext with 153 170 [ SAVE_CARRY ⇒ 154 Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))171 return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉)) 155 172  RESTORE_CARRY ⇒ 156 Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) 173 return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) 174  LOW_ADDRESS reg lbl ⇒ 175 ! lbl' ← Identifier_of_label … lbl ; 176 return MovSuccessor (register_address reg) LOW lbl' 177  HIGH_ADDRESS reg lbl ⇒ 178 ! lbl' ← Identifier_of_label … lbl ; 179 return MovSuccessor (register_address reg) HIGH lbl' 157 180 ] 158  COMMENT comment ⇒ Comment comment 159  COST_LABEL lbl ⇒ Cost lbl 160  POP _ ⇒ Instruction (POP ? accumulator_address) 161  PUSH _ ⇒ Instruction (PUSH ? accumulator_address) 162  CLEAR_CARRY ⇒ Instruction (CLR ? CARRY) 163  CALL f _ _ ⇒ 164 match f with 165 [ inl f_id ⇒ Call (toASM_ident ? f_id) 166  inr _ ⇒ (* TODO call from ptr in DPTR *) 167 match not_implemented in False with [ ] 168 ] 181  COMMENT comment ⇒ return Comment comment 182  POP _ ⇒ return Instruction (POP ? accumulator_address) 183  PUSH _ ⇒ return Instruction (PUSH ? accumulator_address) 184  CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY) 169 185  OPACCS accs _ _ _ _ ⇒ 170 match accs with186 return match accs with 171 187 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 172 188  DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 173 189 ] 174 190  OP1 op1 _ _ ⇒ 175 match op1 with191 return match op1 with 176 192 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 177 193  Inc ⇒ Instruction (INC ? ACC_A) … … 179 195 ] 180 196  OP2 op2 _ _ reg ⇒ 181 match arg_address … reg197 return match arg_address … reg 182 198 return λx.is_in … [[ acc_a; 183 199 direct; … … 221 237  _ ⇒ Ⓧ 222 238 ] (subaddressing_modein …) 223  LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))224  STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))239  LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 240  STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 225 241  ADDRESS addr proof _ _ ⇒ 226 let look ≝ association_ident addr globals (prf ? proof) in227 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))242 ! addr' ← address_of_ident … proof ; 243 return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉))))) 228 244  SET_CARRY ⇒ 229 Instruction (SETB ? CARRY)245 return Instruction (SETB ? CARRY) 230 246  MOVE regs ⇒ 231 match regs with247 return match regs with 232 248 [ to_acc _ reg ⇒ 233 249 match register_address reg return λx.is_in … [[ acc_a; … … 276 292 ] 277 293 ] 294  CALL f _ _ ⇒ 295 match f with 296 [ inl id ⇒ 297 ! id' ← Identifier_of_ident … id ; 298 return Call (toASM_ident ? id') 299  inr _ ⇒ 300 return Instruction (JMP … INDIRECT_DPTR) 301 ] 302  COST_LABEL lbl ⇒ return Cost lbl 278 303  COND _ lbl ⇒ 279 (* dpm: this should be handled in translate_code! *)280 Instruction (JNZ ? (toASM_ident ? lbl))304 ! l ← Identifier_of_label … lbl; 305 return Instruction (JNZ ? l) 281 306 ] 307  FCOND _ _ lbl_true lbl_false ⇒ 308 ! l1 ← Identifier_of_label … lbl_true; 309 ! l2 ← Identifier_of_label … lbl_false; 310 return Jnz ACC_A l1 l2 282 311 ]. 283 312 try @I 284 313 qed. 285 314 286 (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)287 definition ident_of_label: label → Identifier ≝288 toASM_ident LabelTag.289 315 290 316 definition build_translated_statement ≝ 291 317 λglobals. 292 λglobals_old. 293 λprf. 294 λstatement: lin_statement globals_old. 295 〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉. 318 λstatement: lin_statement globals. 319 ! stmt ← translate_statements globals (\snd statement) ; 320 match \fst statement with 321 [ Some lbl ⇒ 322 ! lbl' ← Identifier_of_label globals lbl ; 323 return 〈Some ? lbl', stmt〉 324  None ⇒ 325 return 〈None ?, stmt〉 326 ]. 296 327 297 328 definition translate_code ≝ 298 λglobals: list (ident × nat). 299 λglobals_old: list ident. 300 λprf. 301 λcode: list (lin_statement globals_old). 302 map ? ? (build_translated_statement globals globals_old prf) code. 329 λglobals. 330 λcode: list (lin_statement globals). 331 m_list_map … (build_translated_statement globals) code. 303 332 304 333 definition translate_fun_def ≝ 305 λglobals: list (ident × nat). 306 λglobals_old. 307 λprf. 308 λid_def : ident × (joint_function LIN globals_old). 309 let 〈id, def〉 ≝ id_def in 310 match def with 334 λglobals. 335 λid_def : ident × (joint_function LIN globals). 336 !_ start_funct_translation … id_def ; 337 (* ^ modify current function id ^ *) 338 match \snd id_def with 311 339 [ Internal int ⇒ 312 let code ≝ joint_if_code LIN globals_old int in 313 match translate_code globals globals_old prf code with 314 [ nil ⇒ ⊥ 340 let code ≝ joint_if_code … int in 341 ! id ← Identifier_of_ident … (\fst id_def) ; 342 ! code' ← translate_code … code ; 343 match code' with 344 [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *) 315 345  cons hd tl ⇒ 316 let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in 317 map ? ? ( 318 λr. 319 match fst ? ? r with 320 [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉 321  None ⇒ 〈None ?, \snd r〉 322 ]) rest 346 match \fst hd with 347 [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl) 348  _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *) 349 ] 323 350 ] 324  External _ ⇒ [ ]351  External _ ⇒ return [ ] 325 352 ]. 326 cases daemon (*CSC: XXX will be fixed by an invariant later *) 327 qed. 328 329 include "common/Identifiers.ma". 330 331 let rec flatten_fun_defs 332 (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat) 333 (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old))) 334 on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝ 335 match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with 336 [ cons hd tl ⇒ 337 let fun_def ≝ \snd hd in 338 let fun_id ≝ \fst hd in 339 let translated ≝ translate_fun_def globals globals_old prf hd in 340 let size_translated ≝  translated  in 341 let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in 342 let new_hd ≝ translated @ tail_trans in 343 let new_map ≝ add ? ? tail_map fun_id initial_pc in 344 〈new_hd, new_map〉 345  nil ⇒ 〈[ ], empty_map …〉 346 ]. 347 348 definition translate_functs ≝ 349 λglobals. 350 λglobals_old. 351 λprf. 352 λexit_label. 353 λmain. 354 λfuncts : list (ident × (joint_function LIN ?)). 355 let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in 356 let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in 357 〈preamble @ flattened, map〉. 358 359 (*CSC: region silently thrown away here *) 360 definition globals_addr ≝ 361 λl. 362 let globals_addr_internal ≝ 363 λres_offset. 364 λx_size: ident × region × nat. 365 let 〈res, offset〉 ≝ res_offset in 366 let 〈x, region, size〉 ≝ x_size in 367 〈〈x, offset〉 :: res, offset + size〉 368 in 369 \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l). 370 371 (* dpm: plays the role of the string "_exit" in the O'caml source *) 372 axiom identifier_prefix: Identifier. 373 (*CSC: XXXXXXX wrong anyway since labels from different functions can now 374 clash with each other and with names of functions *) 375 axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier. 376 377 (* dpm: fresh prefix stuff needs unifying with brian *) 353 378 354 definition lin_to_asm : lin_program → pseudo_assembly_program ≝ 379 355 λp. 380 let prog_lbls ≝ program_labels … p in 381 let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in 382 let global_addr ≝ globals_addr (prog_vars … p) in 383 let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in 384 let 〈translated, funct_map〉 ≝ 385 translate_functs global_addr (prog_var_names … p) ? exit_label 386 (toASM_ident … (prog_main … p)) (prog_funct ?? p) in 387 〈〈funct_map, global_addr'〉, translated〉. 388 #i normalize nodelta global_addr' global_addr exit_label prog_lbls; 389 normalize in match prog_var_names; normalize nodelta 390 elim (prog_vars … p) // 391 #hd #tl #IH whd in ⊢ (% → %); 392 whd in match globals_addr; normalize nodelta 393 whd in match (foldl ???? (hd::tl)); normalize nodelta 394 cases hd * #id #reg #size normalize nodelta 395 cases daemon (*CSC: provable using a pair of lemmas over foldl *) 396 qed. 356 state_run ?? (new_ASM_universe p) 357 (let add_translation ≝ 358 λacc,id_def. 359 ! code ← translate_fun_def … id_def ; 360 ! acc ← acc ; 361 return (code @ acc) in 362 ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ; 363 ! exit_label ← ASM_fresh … ; 364 ! main ← Identifier_of_ident … (prog_main … p) ; 365 let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in 366 (* atm no data identifier is used in the code, so preamble must be empty *) 367 return 〈[ ], code〉).
Note: See TracChangeset
for help on using the changeset viewer.