Changeset 757 for src/LIN/LINToASM.ma
 Timestamp:
 Apr 18, 2011, 12:30:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LINToASM.ma
r734 r757 4 4 include "LIN/LIN.ma". 5 5 6 let rec association (i: Identifier) (l: list (Identifier× nat))7 on l: member i (eq_ bv?) (map ? ? (fst ? ?) l) → nat ≝8 match l return λl. member i (eq_ bv?) (map ? ? (fst ? ?) l) → nat with6 let rec association (i: ident) (l: list (ident × nat)) 7 on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝ 8 match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with 9 9 [ nil ⇒ λabsd. ? 10 10  cons hd tl ⇒ 11 λprf: member i (eq_ bv?) (map ? ? (fst ? ?) (cons ? hd tl)).12 (match eq_ bv ? (\fst hd) i return λb. eq_bv? (\fst hd) i = b → nat with11 λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)). 12 (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with 13 13 [ true ⇒ λeq_prf. \snd hd 14 14  false ⇒ λeq_prf. association i tl ? 15 ]) (refl ? (eq_ bv? (\fst hd) i))15 ]) (refl ? (eq_identifier ? (\fst hd) i)) 16 16 ]. 17 17 [ cases absd … … 27 27 28 28 definition statement_labels ≝ 29 λg: list Identifier.30 λs: LINStatement g.29 λg: list ident. 30 λs: lin_statement g. 31 31 let 〈label, instr〉 ≝ s in 32 32 let generated ≝ 33 33 match instr with 34 [ Joint_St_Sequential instr' _ ⇒34 [ joint_st_sequential instr' _ ⇒ 35 35 match instr' with 36 [ Joint_Instr_CostLabel lbl ⇒ set_insert ? lbl(set_empty ?)37  Joint_Instr_CondAcc lbl ⇒ set_insert ? lbl(set_empty ?)36 [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 37  joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 38 38  _ ⇒ set_empty ? 39 39 ] 40  Joint_St_Goto lbl ⇒ set_insert ? lbl(set_empty ?)41  Joint_St_Return ⇒ set_empty ?40  joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 41  joint_st_return ⇒ set_empty ? 42 42 ] in 43 43 match label with 44 44 [ None ⇒ generated 45  Some lbl ⇒ set_insert ? lblgenerated45  Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated 46 46 ]. 47 47 48 48 definition function_labels_internal ≝ 49 λglobals: list Identifier.49 λglobals: list ident. 50 50 λlabels: BitVectorTrieSet ?. 51 λstatement: LINStatement globals.51 λstatement: lin_statement globals. 52 52 set_union ? labels (statement_labels globals statement). 53 53 … … 55 55 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝ 56 56 λA: Type[0]. 57 λglobals: list Identifier.58 λf: A × ( LINFunctionDefinition globals).57 λglobals: list ident. 58 λf: A × (lin_function_definition globals). 59 59 let 〈ignore, fun_def〉 ≝ f in 60 60 match fun_def return λ_. BitVectorTrieSet ? with 61 [ LIN_Fu_Internal stmts proof ⇒61 [ lin_fu_internal stmts proof ⇒ 62 62 foldl ? ? (function_labels_internal globals) (set_empty ?) stmts 63  LIN_Fu_External _ ⇒ set_empty ?63  lin_fu_external _ ⇒ set_empty ? 64 64 ]. 65 65 66 66 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝ 67 67 λA: Type[0]. 68 λglobals: list Identifier.68 λglobals: list ident. 69 69 λlabels: BitVectorTrieSet ?. 70 λfunct: A × ( LINFunctionDefinition globals).70 λfunct: A × (lin_function_definition globals). 71 71 set_union ? labels (function_labels ? globals funct). 72 72 73 73 definition program_labels ≝ 74 74 λprogram. 75 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) ( LIN_Pr_vars program)))76 (set_empty ?) ( LIN_Pr_funs program).75 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program))) 76 (set_empty ?) (lin_pr_funcs program). 77 77 78 78 definition data_of_int ≝ λbv. DATA bv. … … 83 83 84 84 definition translate_statements ≝ 85 λglobals: list ( Identifier× nat).86 λglobals_old: list Identifier.87 λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv?) (map ? ? (fst ? ?) globals).88 λstatement: PreLINStatement globals_old.85 λglobals: list (ident × nat). 86 λglobals_old: list ident. 87 λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals). 88 λstatement: pre_lin_statement globals_old. 89 89 match statement with 90 [ Joint_St_Return ⇒ Instruction (RET ?)91  Joint_St_Goto lbl ⇒ Jmp lbl92  Joint_St_Sequential instr _ ⇒90 [ joint_st_return ⇒ Instruction (RET ?) 91  joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl) 92  joint_st_sequential instr _ ⇒ 93 93 match instr with 94 [ Joint_Instr_Comment comment ⇒ Comment comment95  Joint_Instr_CostLabel lbl ⇒ Cost lbl96  Joint_Instr_Pop ⇒ Instruction (POP ? accumulator_address)97  Joint_Instr_Push ⇒ Instruction (PUSH ? accumulator_address)98  Joint_Instr_ClearCarry ⇒ Instruction (CLR ? CARRY)99  Joint_Instr_CallId f ⇒ Call f100  Joint_Instr_OpAccs accs ⇒94 [ joint_instr_comment comment ⇒ Comment comment 95  joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl) 96  joint_instr_pop ⇒ Instruction (POP ? accumulator_address) 97  joint_instr_push ⇒ Instruction (PUSH ? accumulator_address) 98  joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY) 99  joint_instr_call_id f ⇒ Call (word_of_identifier ? f) 100  joint_instr_opaccs accs ⇒ 101 101 match accs with 102 102 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) … … 104 104  Modu ⇒ ? 105 105 ] 106  Joint_Instr_Op1 op1 ⇒106  joint_instr_op1 op1 ⇒ 107 107 match op1 with 108 108 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 109 109  Inc ⇒ Instruction (INC ? ACC_A) 110 110 ] 111  Joint_Instr_Op2 op2 reg ⇒111  joint_instr_op2 op2 reg ⇒ 112 112 match op2 with 113 113 [ Add ⇒ 114 let reg' ≝ register_address regin115 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 116 direct; 117 regist er ]] x) → ? with114 let reg' ≝ register_address (Register_of_register reg) in 115 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 116 direct; 117 registr ]] x) → ? with 118 118 [ ACC_A ⇒ λacc_a: True. 119 119 Instruction (ADD ? ACC_A accumulator_address) … … 125 125 ] (subaddressing_modein … reg') 126 126  Addc ⇒ 127 let reg' ≝ register_address regin128 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 129 direct; 130 regist er ]] x) → ? with127 let reg' ≝ register_address (Register_of_register reg) in 128 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 129 direct; 130 registr ]] x) → ? with 131 131 [ ACC_A ⇒ λacc_a: True. 132 132 Instruction (ADDC ? ACC_A accumulator_address) … … 138 138 ] (subaddressing_modein … reg') 139 139  Sub ⇒ 140 let reg' ≝ register_address regin141 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 142 direct; 143 regist er ]] x) → ? with140 let reg' ≝ register_address (Register_of_register reg) in 141 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 142 direct; 143 registr ]] x) → ? with 144 144 [ ACC_A ⇒ λacc_a: True. 145 145 Instruction (SUBB ? ACC_A accumulator_address) … … 151 151 ] (subaddressing_modein … reg') 152 152  And ⇒ 153 let reg' ≝ register_address regin154 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 155 direct; 156 regist er ]] x) → ? with153 let reg' ≝ register_address (Register_of_register reg) in 154 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 155 direct; 156 registr ]] x) → ? with 157 157 [ ACC_A ⇒ λacc_a: True. 158 158 Instruction (NOP ?) … … 164 164 ] (subaddressing_modein … reg') 165 165  Or ⇒ 166 let reg' ≝ register_address regin167 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 168 direct; 169 regist er ]] x) → ? with166 let reg' ≝ register_address (Register_of_register reg) in 167 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 168 direct; 169 registr ]] x) → ? with 170 170 [ ACC_A ⇒ λacc_a: True. 171 171 Instruction (NOP ?) … … 177 177 ] (subaddressing_modein … reg') 178 178  Xor ⇒ 179 let reg' ≝ register_address regin180 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 181 direct; 182 regist er ]] x) → ? with179 let reg' ≝ register_address (Register_of_register reg) in 180 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 181 direct; 182 registr ]] x) → ? with 183 183 [ ACC_A ⇒ λacc_a: True. 184 184 Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) … … 190 190 ] (subaddressing_modein … reg') 191 191 ] 192  Joint_Instr_Int reg byte ⇒193 let reg' ≝ register_address regin194 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 195 direct; 196 regist er ]] x) → ? with192  joint_instr_int reg byte ⇒ 193 let reg' ≝ register_address (Register_of_register reg) in 194 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 195 direct; 196 registr ]] x) → ? with 197 197 [ REGISTER r ⇒ λregister7: True. 198 198 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) … … 203 203  _ ⇒ λother: False. ⊥ 204 204 ] (subaddressing_modein … reg') 205  Joint_Instr_FromAcc reg ⇒206 let reg' ≝ register_address regin207 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 208 direct; 209 regist er ]] x) → ? with205  joint_instr_from_acc reg ⇒ 206 let reg' ≝ register_address (Register_of_register reg) in 207 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 208 direct; 209 registr ]] x) → ? with 210 210 [ REGISTER r ⇒ λregister8: True. 211 211 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) … … 216 216  _ ⇒ λother: False. ⊥ 217 217 ] (subaddressing_modein … reg') 218  Joint_Instr_ToAcc reg ⇒219 let reg' ≝ register_address regin220 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 221 direct; 222 regist er ]] x) → ? with218  joint_instr_to_acc reg ⇒ 219 let reg' ≝ register_address (Register_of_register reg) in 220 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 221 direct; 222 registr ]] x) → ? with 223 223 [ REGISTER r ⇒ λregister9: True. 224 224 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) … … 229 229  _ ⇒ λother: False. ⊥ 230 230 ] (subaddressing_modein … reg') 231  Joint_Instr_Load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))232  Joint_Instr_Store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))233  Joint_Instr_Address addr proof ⇒231  joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 232  joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 233  joint_instr_address addr proof ⇒ 234 234 let look ≝ association addr globals (prf ? proof) in 235 235 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 236  Joint_Instr_CondAcc lbl ⇒236  joint_instr_cond_acc lbl ⇒ 237 237 (* dpm: this should be handled in translate_code! *) 238 WithLabel (JNZ ? lbl)238 WithLabel (JNZ ? (word_of_identifier ? lbl)) 239 239 ] 240 240 ]. … … 248 248 λglobals_old. 249 249 λprf. 250 λstatement: LINStatement globals_old.250 λstatement: lin_statement globals_old. 251 251 〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉. 252 252 253 253 definition translate_code ≝ 254 λglobals: list ( Identifier× nat).255 λglobals_old: list Identifier.254 λglobals: list (ident × nat). 255 λglobals_old: list ident. 256 256 λprf. 257 λcode: list ( LINStatement globals_old).257 λcode: list (lin_statement globals_old). 258 258 map ? ? (build_translated_statement globals globals_old prf) code. 259 259 260 260 lemma translate_code_preserves_WellFormedP: 261 261 ∀globals, globals_old, prf, code. 262 WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code).262 well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code). 263 263 #G #GO #P #C 264 264 elim C … … 279 279 let 〈id, def〉 ≝ id_def in 280 280 match def with 281 [ LIN_Fu_Internal code proof ⇒282 match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with281 [ lin_fu_internal code proof ⇒ 282 match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with 283 283 [ nil ⇒ λprf2. ⊥ 284  cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl 284  cons hd tl ⇒ λ_. 285 let rest ≝ 〈Some ? id, \snd hd〉 :: tl in 286 map ? ? ( 287 λr. 288 match fst ? ? r with 289 [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉 290  None ⇒ 〈None ?, \snd r〉 291 ]) rest 285 292 ] (translate_code_preserves_WellFormedP globals globals_old prf code proof) 286 293  _ ⇒ [ ]
Note: See TracChangeset
for help on using the changeset viewer.