 Timestamp:
 Jun 7, 2012, 10:47:07 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2021 r2022 420 420 (* XXX: pc_plus_sjmp_length used to be just sigma of ppc. This is incorrect 421 421 as relative lengths are computed from the *end* of the SJMP, not from 422 the beginning. This caused a mismatch with Jaap's code which was 423 computing the lengths correctly, and has not been fixed. 422 the beginning. 424 423 *) 425 424 definition expand_relative_jump_internal: … … 430 429 λlookup_labels.λsigma.λlbl.λppc,i. 431 430 let lookup_address ≝ sigma (lookup_labels lbl) in 432 let pc_plus_ sjmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in433 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_ sjmp_length lookup_address false in431 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 432 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in 434 433 let 〈upper, lower〉 ≝ split ? 8 8 result in 435 434 if eq_bv ? upper (zero 8) then … … 537 536  Call call ⇒ 538 537 let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in 539 let pc ≝ sigma ppcin538 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 540 539 let do_a_long ≝ policy ppc in 541 let 〈pc_5, restp〉 ≝ split ? 5 11 pc in540 let 〈pc_5, restp〉 ≝ split ? 5 11 pc_plus_jmp_length in 542 541 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then 543 542 let address ≝ ADDR11 resta in … … 551 550  Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr 552 551  Jmp jmp ⇒ 553 let pc ≝ sigma ppcin552 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 554 553 let do_a_long ≝ policy ppc in 555 554 let lookup_address ≝ sigma (lookup_labels jmp) in 556 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in555 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in 557 556 let 〈upper, lower〉 ≝ split ? 8 8 result in 558 557 if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then … … 561 560 else 562 561 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in 563 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in562 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in 564 563 if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then 565 564 let address ≝ ADDR11 rest_addr in
Note: See TracChangeset
for help on using the changeset viewer.