Changeset 2048 for src/ASM/Assembly.ma
 Timestamp:
 Jun 12, 2012, 2:46:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2047 r2048 14 14  medium_jump: jump_length 15 15  long_jump: jump_length. 16 17 (* Functions that define the conditions under which jumps are possible *) 18 definition short_jump_cond: Word → Word → (*pseudo_instruction →*) 19 bool × (BitVector 8) ≝ 20 λpc_plus_jmp_length.λaddr.(*λinstr.*) 21 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 22 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 23 if get_index' ? 2 0 flags then 24 〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉 25 else 26 〈eq_bv 8 upper (zero 8), zero 8〉. 27 28 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*) 29 bool × (BitVector 11) ≝ 30 λpc_plus_jmp_length.λaddr.(*λinstr.*) 31 let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in 32 let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in 33 〈eq_bv 5 fst_5_addr fst_5_pc, rest_addr〉. 16 34 17 35 definition assembly_preinstruction ≝ … … 430 448 let lookup_address ≝ sigma (lookup_labels lbl) in 431 449 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 432 let 〈 result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length falsein433 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in434 if eq_bv ? upper (zero 8)then435 let address ≝ RELATIVE lowerin450 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 451 if sj_possible 452 then 453 let address ≝ RELATIVE disp in 436 454 [ RealInstruction (i address) ] 437 455 else … … 535 553  Comment comment ⇒ [ ] 536 554  Call call ⇒ 537 let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in538 555 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 556 let lookup_address ≝ sigma (lookup_labels call) in 557 let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in 539 558 let do_a_long ≝ policy ppc in 540 let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 541 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then 542 let address ≝ ADDR11 resta in 559 if mj_possible ∧ ¬ do_a_long then 560 let address ≝ ADDR11 disp in 543 561 [ ACALL address ] 544 562 else 545 let address ≝ ADDR16 (sigma (lookup_labels call))in563 let address ≝ ADDR16 lookup_address in 546 564 [ LCALL address ] 547 565  Mov d trgt ⇒ … … 553 571 let do_a_long ≝ policy ppc in 554 572 let lookup_address ≝ sigma (lookup_labels jmp) in 555 let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in 556 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 557 if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then 558 let address ≝ RELATIVE lower in 573 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 574 if sj_possible ∧ ¬ do_a_long then 575 let address ≝ RELATIVE disp in 559 576 [ SJMP address ] 560 577 else 561 let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in 562 let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 563 if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then 564 let address ≝ ADDR11 rest_addr in 578 let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in 579 if mj_possible ∧ ¬ do_a_long then 580 let address ≝ ADDR11 disp2 in 565 581 [ AJMP address ] 566 582 else
Note: See TracChangeset
for help on using the changeset viewer.