Changeset 2926


Ignore:
Timestamp:
Mar 21, 2013, 4:06:52 PM (4 years ago)
Author:
tranquil
Message:

corrected bug in executing Sub

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/BackEndOps.ma

    r2871 r2926  
    130130  fold_right2_i … f 〈[[ ]],carry〉 n.
    131131
    132 definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
     132definition op_of_add_or_sub : add_or_sub → Op2 ≝
     133λwhat.match what with [ do_add ⇒ Addc | do_sub ⇒ Sub ].
     134
     135definition be_add_sub_byte : add_or_sub → bebit → beval → Byte → res (beval × bebit) ≝
    133136  λis_add,carry,a1,b2.
    134   let op ≝ if is_add then Addc else Sub in
     137  let op ≝ op_of_add_or_sub is_add in
    135138  match a1 with
    136139  [ BVByte b1 ⇒
     
    155158        match carry with
    156159        [ BBptrcarry is_add' ptr' p' by' ⇒
    157           if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
     160          if eq_add_or_sub is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
    158161            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
    159           then If eqb p' 0 then with prf do
     162          then If eqb p' 0 then with  prf do
    160163            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
    161164            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
     
    163166            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
    164167            let part1 ≝ mk_part 1 (le_n …) in
    165             let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
    166             OK … 〈BVptr ptr' part1,
     168            let ptr'' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
     169            OK … 〈BVptr ptr'' part1,
    167170                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
    168171          else Error … [MSG UnsupportedOp]
     
    230233  [ Add ⇒
    231234    match a1 with
    232     [ BVByte b1 ⇒ be_add_sub_byte true (BBbit false) a2 b1
     235    [ BVByte b1 ⇒ be_add_sub_byte do_add (BBbit false) a2 b1
    233236    | BVptr ptr1 p1 ⇒
    234237      match a2 with
    235       [ BVByte b2 ⇒ be_add_sub_byte true (BBbit false) a1 b2
     238      [ BVByte b2 ⇒ be_add_sub_byte do_add (BBbit false) a1 b2
    236239      | _ ⇒ Error … [MSG UnsupportedOp]
    237240      ]
     
    240243  | Addc ⇒
    241244    match a1 with
    242     [ BVByte b1 ⇒ be_add_sub_byte true carry a2 b1
     245    [ BVByte b1 ⇒
     246      be_add_sub_byte do_add carry a2 b1
    243247    | BVptr ptr1 p1 ⇒
    244248      match a2 with
    245       [ BVByte b2 ⇒ be_add_sub_byte true carry a1 b2
     249      [ BVByte b2 ⇒ be_add_sub_byte do_add carry a1 b2
    246250      | _ ⇒ Error … [MSG UnsupportedOp]
    247251      ]
     
    250254  | Sub ⇒
    251255    match a1 with
    252     [ BVByte b1 ⇒ be_add_sub_byte false carry a2 b1
     256    [ BVByte b1 ⇒
     257      ! b2 ← Byte_of_val UnsupportedOp a2 ;
     258      be_add_sub_byte do_sub carry a1 b2
    253259    | BVptr ptr1 p1 ⇒
    254260      match a2 with
    255       [ BVByte b2 ⇒ be_add_sub_byte false carry a1 b2
     261      [ BVByte b2 ⇒ be_add_sub_byte do_sub carry a1 b2
    256262      | BVptr ptr2 p2 ⇒
    257263        match ptype ptr1 with
Note: See TracChangeset for help on using the changeset viewer.