Ignore:
Timestamp:
Jun 12, 2012, 2:18:16 PM (7 years ago)
Author:
mulligan
Message:

Big bugs in policy calculations found. Waiting for Jaap's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2034 r2047  
    324324  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    325325  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
    326   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length addr false in
     326  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    327327  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    328328  if eq_bv ? upper (zero 8)
     
    356356  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    357357  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
    358   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length addr false in
     358  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    359359  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    360360  if eq_bv ? upper (zero 8)
     
    748748definition short_jump_cond: Word → Word → pseudo_instruction → Prop ≝
    749749  λpc_plus_jmp_length.λaddr.λinstr.
    750   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length addr false in
     750  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    751751  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    752   eq_bv 8 upper (zero 8) = true.
     752    if flags then
     753      eq_bv 8 upper [[true;true;true;true;true;true;true;true]] = true
     754    else
     755      eq_bv 8 upper (zero 8) = true.
    753756
    754757definition medium_jump_cond: Word → Word → pseudo_instruction → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.