Ignore:
Timestamp:
Mar 14, 2013, 5:34:54 PM (8 years ago)
Author:
tranquil
Message:

op2 evaluation on beval's rendered oblivious to carry bit when applicable. This corrects a bug where an evaluation of a carry-oblivious op on two bytes with undefined carry would wrongly fail.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/BackEndOps.ma

    r2720 r2871  
    227227definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
    228228  λcarry,op,a1,a2.
    229   match a1 with
    230   [ BVByte b1 ⇒
    231 (*    if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then
    232       return 〈a2, carry〉
    233     else *) (* maybe it will be needed, need to see actual translations *)
    234       match a2 with
    235       [ BVByte b2 ⇒
    236         ! carry ← Bit_of_val UnsupportedOp carry ;
    237         let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
    238         return 〈BVByte result, BBbit carry〉
    239       | BVptr _ _ ⇒
    240         match op with
    241         [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
    242         | Addc ⇒ be_add_sub_byte true carry a2 b1
    243         | _ ⇒ Error … [MSG UnsupportedOp]
    244         ]
    245       | BVnonzero ⇒
    246         match op with
    247         [ Or ⇒ return 〈BVnonzero, carry〉
    248         | _ ⇒ Error … [MSG UnsupportedOp]
    249         ]
    250       | _ ⇒ Error … [MSG UnsupportedOp]
    251       ]
    252   | BVptr ptr1 p1 ⇒
    253     match a2 with
    254     [ BVByte b2 ⇒
    255       match op with
    256       [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
    257       | Addc ⇒ be_add_sub_byte true carry a1 b2
    258       | Sub ⇒ be_add_sub_byte false carry a1 b2
    259       | _ ⇒ Error … [MSG UnsupportedOp]
    260       ]
    261     | BVptr ptr2 p2 ⇒
    262       match op with
    263       [ Sub ⇒
     229  match op with
     230  [ Add ⇒
     231    match a1 with
     232    [ BVByte b1 ⇒ be_add_sub_byte true (BBbit false) a2 b1
     233    | BVptr ptr1 p1 ⇒
     234      match a2 with
     235      [ BVByte b2 ⇒ be_add_sub_byte true (BBbit false) a1 b2
     236      | _ ⇒ Error … [MSG UnsupportedOp]
     237      ]
     238    | _ ⇒ Error … [MSG UnsupportedOp]
     239    ]
     240  | Addc ⇒
     241    match a1 with
     242    [ BVByte b1 ⇒ be_add_sub_byte true carry a2 b1
     243    | BVptr ptr1 p1 ⇒
     244      match a2 with
     245      [ BVByte b2 ⇒ be_add_sub_byte true carry a1 b2
     246      | _ ⇒ Error … [MSG UnsupportedOp]
     247      ]
     248    | _ ⇒ Error … [MSG UnsupportedOp]
     249    ]
     250  | Sub ⇒
     251    match a1 with
     252    [ BVByte b1 ⇒ be_add_sub_byte false carry a2 b1
     253    | BVptr ptr1 p1 ⇒
     254      match a2 with
     255      [ BVByte b2 ⇒ be_add_sub_byte false carry a1 b2
     256      | BVptr ptr2 p2 ⇒
    264257        match ptype ptr1 with
    265258        [ Code ⇒ Error … [MSG UnsupportedOp]
    … …  
    275268          else Error … [MSG UnsupportedOp]
    276269        ]
    277       | Xor ⇒
    278         if eqb p1 p2 then
    279           return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
    280         else Error … [MSG UnsupportedOp]
    281       | _ ⇒ Error … [MSG UnsupportedOp]
    282       ]
    283     | BVnull p2 ⇒
    284       match op with
    285       [ Xor ⇒
    286         if eqb p1 p2 then
    287           return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
    288         else
    289           Error … [MSG UnsupportedOp]
    290       | _ ⇒ Error … [MSG UnsupportedOp]
    291       ]
    292     | _ ⇒ Error … [MSG UnsupportedOp]
    293     ]
    294   | BVnull p1 ⇒
    295     match a2 with
    296     [ BVptr ptr2 p2 ⇒
    297       match op with
    298       [ Xor ⇒
    299         if eqb p1 p2 then
    300           return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
    301         else
    302           Error … [MSG UnsupportedOp]
    303       | _ ⇒ Error … [MSG UnsupportedOp]
    304       ]
    305     | BVnull p2 ⇒
    306       match op with
    307       [ Xor ⇒
    308         if eqb p1 p2 then
    309           return 〈BVXor (None ?) (None ?) p1, carry〉
    310         else
    311           Error … [MSG UnsupportedOp]
    312       | _ ⇒ Error … [MSG UnsupportedOp]
    313       ]
    314     | _ ⇒ Error … [MSG UnsupportedOp]
    315     ]
    316   | BVXor ptr1_opt ptr1_opt' p1 ⇒
    317     match a2 with
    318     [ BVByte b2 ⇒
    319       match op with
    320       [ Or ⇒
    321         if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
    322         else Error … [MSG UnsupportedOp]
    323       | _ ⇒ Error … [MSG UnsupportedOp]
    324       ]
    325     | BVnonzero ⇒
    326       match op with
    327       [ Or ⇒
    328         return 〈BVnonzero, carry〉
    329       | _ ⇒ Error … [MSG UnsupportedOp]
    330       ]
    331     | BVXor ptr2_opt ptr2_opt' p2 ⇒
    332       match op with
    333       [ Or ⇒
     270      | _ ⇒ Error … [MSG UnsupportedOp]
     271      ]
     272    | _ ⇒ Error … [MSG UnsupportedOp]
     273    ]
     274  | Or ⇒
     275    match a1 with
     276    [ BVByte b1 ⇒
     277      match a2 with
     278      [ BVByte b2 ⇒
     279        let res ≝ \fst (op2 eval false Or b1 b2) in
     280        return 〈BVByte res, carry〉
     281      | BVnonzero ⇒ return 〈BVnonzero, carry〉
     282      | _ ⇒ Error … [MSG UnsupportedOp]
     283      ]
     284    | BVXor ptr1_opt ptr1_opt' p1 ⇒
     285      match a2 with
     286      [ BVXor ptr2_opt ptr2_opt' p2 ⇒
    334287        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
    335288          let eq_at ≝ λp,ptr1,ptr2.
    … …  
    342295          else return 〈BVnonzero, carry〉
    343296        else Error … [MSG UnsupportedOp]
    344       | _ ⇒ Error … [MSG UnsupportedOp]
    345       ]
    346     | _ ⇒ Error … [MSG UnsupportedOp]
    347     ]
    348   | BVnonzero ⇒
    349     match a2 with
    350     [ BVByte _ ⇒
    351       match op with
    352       [ Or ⇒ return 〈BVnonzero, carry〉
     297      | BVnonzero ⇒ return 〈BVnonzero, carry〉
    353298      | _ ⇒ Error … [MSG UnsupportedOp]
    354299      ]
    355300    | BVnonzero ⇒
    356       match op with
    357       [ Or ⇒ return 〈BVnonzero, carry〉
    358       | _ ⇒ Error … [MSG UnsupportedOp]
    359       ]
    360     | BVXor _ _ _ ⇒
    361       match op with
    362       [ Or ⇒ return 〈BVnonzero, carry〉
    363       | _ ⇒ Error … [MSG UnsupportedOp]
    364       ]
    365     | _ ⇒ Error … [MSG UnsupportedOp]
    366     ]
    367   | _ ⇒ Error … [MSG UnsupportedOp]
     301      match a2 with
     302      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
     303      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
     304      | BVnonzero ⇒ return 〈BVnonzero, carry〉
     305      | _ ⇒ Error … [MSG UnsupportedOp]
     306      ]
     307    | _ ⇒ Error … [MSG UnsupportedOp]
     308    ]
     309  | Xor ⇒
     310    match a1 with
     311    [ BVByte b1 ⇒
     312      match a2 with
     313      [ BVByte b2 ⇒
     314        let res ≝ \fst (op2 eval false Xor b1 b2) in
     315        return 〈BVByte res, carry〉
     316      | _ ⇒ Error … [MSG UnsupportedOp]
     317      ]
     318    | BVptr ptr1 p1 ⇒
     319      match a2 with
     320      [ BVptr ptr2 p2 ⇒
     321        if eqb p1 p2 then
     322          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
     323        else Error … [MSG UnsupportedOp]
     324      | BVnull p2 ⇒
     325        if eqb p1 p2 then
     326          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
     327        else
     328          Error … [MSG UnsupportedOp]
     329      | _ ⇒ Error … [MSG UnsupportedOp]
     330      ]
     331    | BVnull p1 ⇒
     332      match a2 with
     333      [ BVptr ptr2 p2 ⇒
     334        if eqb p1 p2 then
     335          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
     336        else
     337          Error … [MSG UnsupportedOp]
     338      | BVnull p2 ⇒
     339        if eqb p1 p2 then
     340          return 〈BVXor (None ?) (None ?) p1, carry〉
     341        else
     342          Error … [MSG UnsupportedOp]
     343      | _ ⇒ Error … [MSG UnsupportedOp]
     344      ]
     345    | _ ⇒ Error … [MSG UnsupportedOp]
     346    ]
     347  | And ⇒
     348    ! b1 ← Byte_of_val UnsupportedOp a1 ;
     349    ! b2 ← Byte_of_val UnsupportedOp a2 ;
     350    let res ≝ \fst (op2 eval false And b1 b2) in
     351    return 〈BVByte res, carry〉
    368352  ].
Note: See TracChangeset for help on using the changeset viewer.