Changeset 2443 for src/LIN/LINToASM.ma
 Timestamp:
 Nov 8, 2012, 2:27:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LINToASM.ma
r2286 r2443 22 22 ]. @I qed. 23 23 24 (* TODO: 25 this should translate back end immediates (which rely on beval) to ASM 26 byte immediates. How should it work? surely needs arguments for instantiation 27 of blocks. If it's too much a fuss, we can go back to byte immediates in the 28 back end. *) 29 definition asm_byte_of_beval : beval → Byte ≝ 30 λb.match b with 31 [ BVByte b ⇒ b 32  BVundef ⇒ (* any will do *) zero_byte 33  BVnonzero ⇒ (* any will do *) maximum 7 @@ [[ true ]] 34  BVnull _ ⇒ zero_byte (* is it correct? *) 35  BVptr b p o ⇒ ? 36 ]. 37 cases daemon qed. 38 39 definition arg_address : hdw_argument → [[ acc_a ; direct ; registr ; data ]] ≝ 40 λa.match a with 41 [ Reg r ⇒ register_address r 42  Imm bv ⇒ DATA (asm_byte_of_beval bv) 43 ]. 44 cases a #x [2: normalize //] normalize nodelta 45 elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I 46 qed. 47 48 let rec association (i: ident) (l: list (ident × nat)) 49 on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝ 50 match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with 51 [ nil ⇒ λabsd. ? 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 with 27 [ nil ⇒ Ⓧ 52 28  cons hd tl ⇒ 53 λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)). 54 (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with 55 [ true ⇒ λeq_prf. \snd hd 56  false ⇒ λeq_prf. association i tl ? 57 ]) (refl ? (eq_identifier ? (\fst hd) i)) 58 ]. 59 [ cases absd 60  cases prf 61 [ > eq_prf 62 # H 63 cases H 29 λprf. 30 If eq_A a (\fst hd) then \snd hd else with eq_prf do 31 association … eq_A a tl ? 32 ]. 33 elim (orb_Prop_true … prf) 34 [ > eq_prf * 64 35  # H 65 36 assumption 66 37 ] 38 qed. 39 40 definition association_ident ≝ association ident nat (eq_identifier ?). 41 definition association_block ≝ association block Word eq_block. 42 43 definition asm_cst_well_def : 44 list (block × Word) → beval → bool ≝ 45 λglobals,bv.match bv with 46 [ BVptr b _ _ ⇒ member ? eq_block b (map ?? \fst globals) 47  _ ⇒ true 48 ]. 49 50 definition vector_cast : 51 ∀A,n,m.A → Vector A n → Vector A m ≝ 52 λA,n,m,dflt,v. 53 If leb n m then with prf do 54 replicate … (m  n) dflt @@ v ⌈Vector ?? ↦ ?⌉ 55 else with prf do 56 \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n  m + m)⌉)). 57 lapply prf @(leb_elim n) 58 [2,3: #_ * #abs elim (abs I) ] 59 #H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …)) 60 [ assumption ] 61 @(transitive_le … (not_le_to_lt … H)) %2 %1 62 qed. 63 64 definition asm_byte_of_beval : 65 ∀globals,bv.asm_cst_well_def globals bv → Byte ≝ 66 λglobals,bv.match bv return λbv.asm_cst_well_def globals bv → Byte with 67 [ BVByte b ⇒ λ_.b 68  BVundef ⇒ λ_.(* any will do *) zero_byte 69  BVnonzero ⇒ λ_.(* any will do *) maximum 7 @@ [[ true ]] 70  BVnull _ ⇒ λ_.zero_byte (* is it correct? *) 71  BVptr b p o ⇒ λprf. 72 let b_inst ≝ vector_cast … (S p) zero_byte (rvsplit … 2 8 (association_block … prf)) in 73 let 〈inst, ignore〉 ≝ op2_bytes Add … false b_inst o in 74 head' … inst 75 ]. 76 77 definition asm_arg_well_def : 78 list (block × Word) → hdw_argument → bool ≝ 79 λglobals,a.match a with 80 [ Imm bv ⇒ asm_cst_well_def globals bv 81  _ ⇒ true 82 ]. 83 84 definition arg_address : ∀globals,arg.asm_arg_well_def globals arg → 85 [[ acc_a ; direct ; registr ; data ]] ≝ 86 λglobals,a. 87 match a 88 return λa.asm_arg_well_def globals a → [[ acc_a ; direct ; registr ; data ]] 89 with 90 [ Reg r ⇒ λ_.register_address r 91  Imm bv ⇒ λprf.DATA (asm_byte_of_beval … prf) 92 ]. 93 [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I 94  @I 67 95 ] 68 96 qed. 69 97 70 98 definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). 99 100 definition asm_stmt_well_def : 101 list (block × Word) → ∀old_globals.joint_statement LIN old_globals → bool ≝ 102 λblocks,old_globals,stmt. 103 match stmt with 104 [ sequential instr _ ⇒ 105 match instr with 106 [ step_seq instr' ⇒ 107 match instr' with 108 [ OP2 _ _ _ arg ⇒ asm_arg_well_def blocks arg 109  MOVE regs ⇒ 110 match regs with 111 [ int_to_reg _ bv ⇒ asm_cst_well_def blocks bv 112  int_to_acc _ bv ⇒ asm_cst_well_def blocks bv 113  _ ⇒ true 114 ] 115  _ ⇒ true 116 ] 117  _ ⇒ true 118 ] 119  _ ⇒ true 120 ]. 71 121 72 122 definition statement_labels ≝ … … 137 187 definition translate_statements ≝ 138 188 λglobals: list (ident × nat). 189 λblocks: list (block × Word). 139 190 λglobals_old: list ident. 140 λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?)(map ? ? (fst ? ?) globals).191 λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals). 141 192 λstatement: joint_statement LIN globals_old. 142 match statement with143 [ final instr ⇒ 193 match statement return λstmt.asm_stmt_well_def blocks ? stmt → ? with 194 [ final instr ⇒ λ_. 144 195 match instr with 145 196 [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) … … 148 199 ] 149 200  sequential instr _ ⇒ 150 match instr with201 match instr return λinstr.asm_stmt_well_def blocks ? (sequential ?? instr ?) → ? with 151 202 [ step_seq instr' ⇒ 152 match instr' with153 [ extension_seq ext ⇒ 203 match instr' return λinstr'.asm_stmt_well_def ?? (sequential ?? (step_seq ?? instr') ?) → ? with 204 [ extension_seq ext ⇒ λ_. 154 205 match ext with 155 206 [ SAVE_CARRY ⇒ … … 158 209 Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) 159 210 ] 160  COMMENT comment ⇒ Comment comment161  COST_LABEL lbl ⇒ Cost lbl162  POP _ ⇒ Instruction (POP ? accumulator_address)163  PUSH _ ⇒ Instruction (PUSH ? accumulator_address)164  CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)165  CALL_ID f _ _ ⇒ Call (toASM_ident ? f)166  extension_call abs ⇒ match abs in void with [ ]167  OPACCS accs _ _ _ _ ⇒ 211  COMMENT comment ⇒ λ_.Comment comment 212  COST_LABEL lbl ⇒ λ_.Cost lbl 213  POP _ ⇒ λ_.Instruction (POP ? accumulator_address) 214  PUSH _ ⇒ λ_.Instruction (PUSH ? accumulator_address) 215  CLEAR_CARRY ⇒ λ_.Instruction (CLR ? CARRY) 216  CALL_ID f _ _ ⇒ λ_.Call (toASM_ident ? f) 217  extension_call abs ⇒ λ_.match abs in void with [ ] 218  OPACCS accs _ _ _ _ ⇒ λ_. 168 219 match accs with 169 220 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 170 221  DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 171 222 ] 172  OP1 op1 _ _ ⇒ 223  OP1 op1 _ _ ⇒ λ_. 173 224 match op1 with 174 225 [ Cmpl ⇒ Instruction (CPL ? ACC_A) … … 176 227  Rl ⇒ Instruction (RL ? ACC_A) 177 228 ] 178  OP2 op2 _ _ reg ⇒ 229  OP2 op2 _ _ reg ⇒ λprf'.? 230  _ ⇒ ?]  _ ⇒ ? ]].[12: whd in prf : (?%); 231 179 232 match op2 with 180 233 [ Add ⇒ 181 let reg' ≝ arg_address regin234 let reg' ≝ arg_address … prf' in 182 235 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 183 236 direct; … … 195 248 ] (subaddressing_modein … reg') 196 249  Addc ⇒ 197 let reg' ≝ arg_address regin250 let reg' ≝ arg_address … prf' in 198 251 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 199 252 direct; … … 211 264 ] (subaddressing_modein … reg') 212 265  Sub ⇒ 213 let reg' ≝ arg_address regin266 let reg' ≝ arg_address … prf' in 214 267 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 215 268 direct; … … 227 280 ] (subaddressing_modein … reg') 228 281  And ⇒ 229 let reg' ≝ arg_address regin282 let reg' ≝ arg_address … prf' in 230 283 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 231 284 direct; … … 243 296 ] (subaddressing_modein … reg') 244 297  Or ⇒ 245 let reg' ≝ arg_address regin298 let reg' ≝ arg_address … prf' in 246 299 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 247 300 direct; … … 258 311 ] (subaddressing_modein … reg') 259 312  Xor ⇒ 260 let reg' ≝ arg_address regin313 let reg' ≝ arg_address … prf' in 261 314 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 262 315 direct; … … 273 326 ] (subaddressing_modein … reg') 274 327 ] 275  LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))276  STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))277  ADDRESS addr proof _ _ ⇒ 278 let look ≝ association addr globals (prf ? proof) in328  LOAD _ _ _ ⇒ λ_.Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 329  STORE _ _ _ ⇒ λ_.Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 330  ADDRESS addr proof _ _ ⇒ λ_. 331 let look ≝ association_ident addr globals (prf ? proof) in 279 332 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 280  SET_CARRY ⇒ 333  SET_CARRY ⇒ λ_. 281 334 Instruction (SETB ? CARRY) 282 335  MOVE regs ⇒ 283 match regs with284 [ to_acc _ reg ⇒ 336 match regs return λregs.asm_stmt_well_def ?? (sequential ?? (step_seq ?? (MOVE regs)) ?) → ? with 337 [ to_acc _ reg ⇒ λ_. 285 338 let reg' ≝ register_address reg in 286 339 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; … … 295 348  _ ⇒ λother: False. ⊥ 296 349 ] (subaddressing_modein … reg') 297  from_acc reg _ ⇒ 350  from_acc reg _ ⇒ λ_. 298 351 let reg' ≝ register_address reg in 299 352 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; … … 308 361  _ ⇒ λother: False. ⊥ 309 362 ] (subaddressing_modein … reg') 310  int_to_reg reg bv ⇒ 311 let b ≝ asm_byte_of_beval bvin363  int_to_reg reg bv ⇒ λprf'. 364 let b ≝ asm_byte_of_beval … prf' in 312 365 let reg' ≝ register_address reg in 313 366 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; … … 322 375  _ ⇒ λother: False. ⊥ 323 376 ] (subaddressing_modein … reg') 324  int_to_acc _ bv ⇒ 325 let b ≝ asm_byte_of_beval bvin377  int_to_acc _ bv ⇒ λprf'. 378 let b ≝ asm_byte_of_beval … prf' in 326 379 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) 327 380 ] 328 381 ] 329  COND _ lbl ⇒ 382  COND _ lbl ⇒ λ_. 330 383 (* dpm: this should be handled in translate_code! *) 331 384 Instruction (JNZ ? (toASM_ident ? lbl)) 332 385 ] 333 386 ]. 334 try assumption335 try @ I387 try @I 388 assumption 336 389 qed. 337 390
Note: See TracChangeset
for help on using the changeset viewer.