Changeset 343 for Deliverables/D4.1/Matita/Interpret.ma
 Timestamp:
 Nov 30, 2010, 4:56:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r341 r343 45 45 let s ≝ set_arg_8 s ACC_A result in 46 46 set_flags s cy_flag (Just Bit ac_flag) ov_flag 47  ANL addr ⇒ 48 match addr with 49 [ Left l ⇒ 50 match l with 51 [ Left l' ⇒ 52 let 〈addr1, addr2〉 ≝ l' in 53 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 54 set_arg_8 s addr1 and_val 55  Right r ⇒ 56 let 〈addr1, addr2〉 ≝ r in 57 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 58 set_arg_8 s addr1 and_val 59 ] 60  Right r ⇒ 61 let 〈addr1, addr2〉 ≝ r in 62 let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in 63 set_flags s and_val (Nothing ?) (get_ov_flag s) 64 ] 65  ORL addr ⇒ 66 match addr with 67 [ Left l ⇒ 68 match l with 69 [ Left l' ⇒ 70 let 〈addr1, addr2〉 ≝ l' in 71 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 72 set_arg_8 s addr1 or_val 73  Right r ⇒ 74 let 〈addr1, addr2〉 ≝ r in 75 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 76 set_arg_8 s addr1 or_val 77 ] 78  Right r ⇒ 79 let 〈addr1, addr2〉 ≝ r in 80 let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in 81 set_flags s or_val (Nothing ?) (get_ov_flag s) 82 ] 83  XRL addr ⇒ 84 match addr with 85 [ Left l' ⇒ 86 let 〈addr1, addr2〉 ≝ l' in 87 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 88 set_arg_8 s addr1 xor_val 89  Right r ⇒ 90 let 〈addr1, addr2〉 ≝ r in 91 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 92 set_arg_8 s addr1 xor_val 93 ] 47 94  INC addr ⇒ 48 95 match addr return λx. bool_to_Prop (is_in … [[ acc_a; … … 185 232 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in 186 233 set_arg_8 s addr2 new_arg 234  RET ⇒ 235 let high_bits ≝ read_at_stack_pointer s in 236 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in 237 let s ≝ set_8051_sfr s SFR_SP new_sp in 238 let low_bits ≝ read_at_stack_pointer s in 239 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in 240 let s ≝ set_8051_sfr s SFR_SP new_sp in 241 let new_pc ≝ high_bits @@ low_bits in 242 set_program_counter s new_pc 243  RETI ⇒ 244 let high_bits ≝ read_at_stack_pointer s in 245 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in 246 let s ≝ set_8051_sfr s SFR_SP new_sp in 247 let low_bits ≝ read_at_stack_pointer s in 248 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in 249 let s ≝ set_8051_sfr s SFR_SP new_sp in 250 let new_pc ≝ high_bits @@ low_bits in 251 set_program_counter s new_pc 187 252  Jump j ⇒ 188 253 match j with … … 258 323  _ ⇒ λother: False. ? 259 324 ] (subaddressing_modein … addr) 260  CJNE addr1 addr2 ⇒ ? 261 match addr1 with 262 [ Left l ⇒ ? 263  Right r ⇒ ? 264 ] 325  CJNE addr1 addr2 ⇒ 326 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 327 [ RELATIVE r ⇒ λrelative: True. 328 match addr1 with 329 [ Left l ⇒ 330 let 〈addr1, addr2〉 ≝ l in 331 let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1)) 332 (nat_of_bitvector ? (get_arg_8 s false addr2)) in 333 if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then 334 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 335 let s ≝ set_program_counter s new_pc in 336 set_flags s new_cy (Nothing ?) (get_ov_flag s) 337 else 338 (set_flags s new_cy (Nothing ?) (get_ov_flag s)) 339  Right r' ⇒ 340 let 〈addr1, addr2〉 ≝ r' in 341 let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1)) 342 (nat_of_bitvector ? (get_arg_8 s false addr2)) in 343 if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then 344 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 345 let s ≝ set_program_counter s new_pc in 346 set_flags s new_cy (Nothing ?) (get_ov_flag s) 347 else 348 (set_flags s new_cy (Nothing ?) (get_ov_flag s)) 349 ] 350  _ ⇒ λother: False. ? 351 ] (subaddressing_modein … addr2) 265 352  DJNZ addr1 addr2 ⇒ 266 353 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with … … 276 363 ] (subaddressing_modein … addr2) 277 364 ] 365  JMP _ ⇒ (* DPM: always indirect_dptr *) 366 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 367 let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in 368 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 369 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in 370 set_program_counter s new_pc 371  LJMP addr ⇒ 372 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 373 [ ADDR16 a ⇒ λaddr16: True. 374 set_program_counter s a 375  _ ⇒ λother: False. ? 376 ] (subaddressing_modein … addr) 377  SJMP addr ⇒ 378 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 379 [ RELATIVE r ⇒ λrelative: True. 380 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 381 set_program_counter s new_pc 382  _ ⇒ λother: False. ? 383 ] (subaddressing_modein … addr) 384  AJMP addr ⇒ 385 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 386 [ ADDR11 a ⇒ λaddr11: True. 387 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in 388 let 〈nu, nl〉 ≝ split ? four four pc_bu in 389 let bit ≝ cic:/matita/ng/Vector/get_index.fix(0,3,2) ? ? nl Z ? in 390 let 〈relevant1, relevant2〉 ≝ split ? three eight a in 391 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 392 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in 393 set_program_counter s new_pc 394  _ ⇒ λother: False. ? 395 ] (subaddressing_modein … addr) 396  MOVC addr1 addr2 ⇒ 397 match addr2 return λx. bool_to_Prop (is_in [[ acc_dptr; acc_pc ]] x) → ? with 398 [ ACC_DPTR ⇒ λacc_dptr: True. ? 399  ACC_PC ⇒ λacc_pc: True. ? 400  _ ⇒ λother: False. ? 401 ] (subaddressing_modein … ?) 278 402  NOP ⇒ s 279 403  _ ⇒ s
Note: See TracChangeset
for help on using the changeset viewer.