- Timestamp:
- Sep 21, 2011, 10:22:13 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/LINToASM.ma
r1179 r1245 28 28 definition statement_labels ≝ 29 29 λg: list ident. 30 λs: lin_statement g.30 λs: (option label) × (lin_statement g). 31 31 let 〈label, instr〉 ≝ s in 32 32 let generated ≝ … … 51 51 λglobals: list ident. 52 52 λlabels: BitVectorTrieSet ?. 53 λstatement: lin_statement globals.53 λstatement: (option label) × (lin_statement globals). 54 54 set_union ? labels (statement_labels globals statement). 55 55 56 (* 56 57 (* dpm: A = Identifier *) 57 58 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝ … … 61 62 let 〈ignore, fun_def〉 ≝ f in 62 63 match fun_def return λ_. BitVectorTrieSet ? with 63 [ lin_fu_internal stmts proof⇒64 [ Internal stmts ⇒ 64 65 foldl ? ? (function_labels_internal globals) (set_empty ?) stmts 65 | lin_fu_external _ ⇒ set_empty ?66 | External _ ⇒ set_empty ? 66 67 ]. 67 68 … … 77 78 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program))) 78 79 (set_empty ?) (lin_pr_funcs program). 79 80 *) 80 81 definition data_of_int ≝ λbv. DATA bv. 81 82 definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). 82 83 definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). 83 84 axiom ImplementedInRuntime: False.85 84 86 85 definition translate_statements ≝ … … 88 87 λglobals_old: list ident. 89 88 λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals). 90 λstatement: pre_lin_statement globals_old.89 λstatement: lin_statement globals_old. 91 90 match statement with 92 91 [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl) 93 | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)92 | joint_st_extension ext ⇒ ⊥ 94 93 | joint_st_return ⇒ Instruction (RET ?) 95 94 | joint_st_sequential instr _ ⇒ … … 97 96 [ joint_instr_comment comment ⇒ Comment comment 98 97 | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl) 99 | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)100 | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)98 | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address) 99 | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address) 101 100 | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY) 102 | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)103 | joint_instr_opaccs accs ⇒101 | joint_instr_call_id f _ ⇒ Call (word_of_identifier ? f) 102 | joint_instr_opaccs accs _ _ ⇒ 104 103 match accs with 105 104 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 106 105 | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 107 106 ] 108 | joint_instr_op1 op1 ⇒107 | joint_instr_op1 op1 _ ⇒ 109 108 match op1 with 110 109 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 111 110 | Inc ⇒ Instruction (INC ? ACC_A) 112 111 ] 113 | joint_instr_op2 op2 reg ⇒112 | joint_instr_op2 op2 _ reg ⇒ 114 113 match op2 with 115 114 [ Add ⇒ … … 205 204 | _ ⇒ λother: False. ⊥ 206 205 ] (subaddressing_modein … reg') 207 | joint_instr_from_acc reg ⇒ 208 let reg' ≝ register_address reg in 209 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 210 direct; 211 registr ]] x) → ? with 212 [ REGISTER r ⇒ λregister8: True. 213 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) 214 | ACC_A ⇒ λacc: True. 215 Instruction (NOP ?) 216 | DIRECT d ⇒ λdirect8: True. 217 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) 218 | _ ⇒ λother: False. ⊥ 219 ] (subaddressing_modein … reg') 220 | joint_instr_to_acc reg ⇒ 221 let reg' ≝ register_address reg in 222 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 223 direct; 224 registr ]] x) → ? with 225 [ REGISTER r ⇒ λregister9: True. 226 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 227 | DIRECT d ⇒ λdirect9: True. 228 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 229 | ACC_A ⇒ λacc_a: True. 230 Instruction (NOP ?) 231 | _ ⇒ λother: False. ⊥ 232 ] (subaddressing_modein … reg') 233 | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 234 | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 235 | joint_instr_address addr proof ⇒ 206 | joint_instr_move regs ⇒ 207 match regs with 208 [ from_acc reg ⇒ 209 let reg' ≝ register_address reg in 210 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 211 direct; 212 registr ]] x) → ? with 213 [ REGISTER r ⇒ λregister8: True. 214 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) 215 | ACC_A ⇒ λacc: True. 216 Instruction (NOP ?) 217 | DIRECT d ⇒ λdirect8: True. 218 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) 219 | _ ⇒ λother: False. ⊥ 220 ] (subaddressing_modein … reg') 221 | to_acc reg ⇒ 222 let reg' ≝ register_address reg in 223 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 224 direct; 225 registr ]] x) → ? with 226 [ REGISTER r ⇒ λregister9: True. 227 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 228 | DIRECT d ⇒ λdirect9: True. 229 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 230 | ACC_A ⇒ λacc_a: True. 231 Instruction (NOP ?) 232 | _ ⇒ λother: False. ⊥ 233 ] (subaddressing_modein … reg')] 234 | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 235 | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 236 | joint_instr_address addr proof _ _ ⇒ 236 237 let look ≝ association addr globals (prf ? proof) in 237 238 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 238 | joint_instr_cond _acclbl ⇒239 | joint_instr_cond _ lbl ⇒ 239 240 (* dpm: this should be handled in translate_code! *) 240 241 Instruction (JNZ ? (word_of_identifier ? lbl)) … … 245 246 try assumption 246 247 try @ I 247 cases ImplementedInRuntime248 248 qed. 249 249 … … 252 252 λglobals_old. 253 253 λprf. 254 λstatement: lin_statement globals_old.254 λstatement: (option label) × (lin_statement globals_old). 255 255 〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉. 256 256 … … 259 259 λglobals_old: list ident. 260 260 λprf. 261 λcode: list ( lin_statement globals_old).261 λcode: list ((option label) × (lin_statement globals_old)). 262 262 map ? ? (build_translated_statement globals globals_old prf) code. 263 263
Note: See TracChangeset
for help on using the changeset viewer.