Ignore:
Timestamp:
Nov 6, 2012, 4:12:21 PM (8 years ago)
Author:
tranquil
Message:

new back end operations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/BackEndOps.ma

    r2286 r2435  
    6666    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
    6767    return 〈BVByte rslt, BBbit carry''〉
    68   | BVptr b p o ⇒
    69     match p with
    70     [ O ⇒ λ_:0<size_pointer.λo : Vector Byte 1.
    71       if eq_bebit carry (BBbit false) then
    72         let o' ≝ from_singl … o in
    73         let 〈rslt,carry〉 ≝ op2 eval false op b2 o' in
    74         let p' : part ≝ mk_part 0 ? in
    75         return 〈BVptr b p' [[rslt]], BBptrcarry is_add b p' o [[b2]]〉
    76       else
    77         Error … [MSG UnsupportedOp]
    78     | S k ⇒ λSk_ok:S k<size_pointer.λo : Vector Byte (S (S k)).
    79       match carry with
    80       [ BBptrcarry is_add' b' p' o' by' ⇒
    81         if eq_b is_add is_add' ∧ eq_block b b' ∧ vsuffix … (eq_bv 8) o' o then
    82           If eqb k p' then with prf do
    83             let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in
    84             let 〈rslt,ignore〉 ≝ op2_bytes op … false o (b2 ::: by') in
    85             let Sk_part ≝ mk_part (S k) Sk_ok in
    86             OK … 〈BVptr b Sk_part rslt,
    87                      BBptrcarry is_add b Sk_part o (b2 ::: by')〉
     68  | BVptr ptr p ⇒
     69    match ptype ptr with
     70    [ Code ⇒ Error … [MSG UnsupportedOp]
     71    | XData ⇒
     72      match p with
     73      [ O ⇒
     74        ! carry' ← Bit_of_val UnsupportedOp carry ;
     75        if carry' then Error … [MSG UnsupportedOp]
     76        else
     77          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
     78          let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
     79          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
     80          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
     81          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
     82      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
     83        match carry with
     84        [ BBptrcarry is_add' ptr' p' by' ⇒
     85          if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
     86            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
     87          then If eqb p' 0 then with prf do
     88            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
     89            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
     90            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
     91            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
     92            let part1 ≝ mk_part 1 (le_n …) in
     93            let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
     94            OK … 〈BVptr ptr' part1,
     95                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
    8896          else Error … [MSG UnsupportedOp]
    89         else Error … [MSG UnsupportedOp]
    90       | _ ⇒ Error … [MSG UnsupportedOp]
    91       ]
    92     ] (part_no_ok p) o
     97          else Error … [MSG UnsupportedOp]
     98        | _ ⇒ Error … [MSG UnsupportedOp]
     99        ]
     100      ]
     101    ]
    93102  | _ ⇒ Error … [MSG UnsupportedOp]
    94103  ].
    95 @hide_prf [//]
    96 lapply prf @(eqb_elim k) #H * >H %
     104@hide_prf
     105lapply prf @(eqb_elim p') #H * >H %
    97106qed.
     107
     108definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
     109λn,v,p,H.
     110let suffix : BitVector (8 + 8*p) ≝
     111  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
     112\fst (vsplit … suffix).
     113>(commutative_times_fast ? p)
     114change with (? = BitVector (? + S p*8))
     115>(commutative_times_fast (S p))
     116<distributive_times_plus_fast
     117<(plus_minus_m_m … H) %
     118qed.
     119
     120definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
     121λA,eq,m,n.
     122match m with
     123[ Some a ⇒
     124  match n with
     125  [ Some b ⇒ eq a b
     126  | _ ⇒ false
     127  ]
     128| _ ⇒
     129  match m with
     130  [ None ⇒ true
     131  | _ ⇒ false
     132  ]
     133].
    98134
    99135(* This tables shows what binary ops may be defined on bevals depending on
    100136   the arguments (columns marked by 1st argument, rows by 2nd). Further
    101137   checks for definedness are done for pointer parts taking into account
    102    blocks, parts and the carry value.
    103             | BVByte    | BVptr          | BVnull | BVnonzero | BVundef |
    104   ----------+-----------+----------------+--------+-----------+---------|
    105   BVByte    | all       | Add, Addc, Sub | none   | Or        | none    |
    106   ----------+-----------+----------------+--------+-----------+---------|
    107   BVptr     | Add, Addc | Sub, Xor       | Xor    | none      | none    |
    108   ----------+-----------+----------------+--------+-----------+---------|
    109   BVnull    | none      | Xor            | Xor    | none      | none    |
    110   ----------+-----------+----------------+--------+-----------+---------|
    111   BVnonzero | Or        | none           | none   | Or        | none    |
    112   ----------+-----------+----------------+--------+-----------+---------|
    113   BVundef   | none      | none           | none   | none      | none    |
    114   ----------------------------------------------------------------------+
     138   blocks, parts and the carry value. TODO update table
     139  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
     140  ----------+-----------+----------------+-----------+--------+-------+-----------+
     141  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
     142  ----------+-----------+----------------+-----------+--------+-------+-----------+
     143  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
     144  ----------+-----------+----------------+-----------+--------+-------+-----------+
     145  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
     146  ----------+-----------+----------------+-----------+--------+-------+-----------+
     147  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
     148  ----------+-----------+----------------+-----------+--------+-------+-----------+
     149  BVXor     | --        | --             | --        | --     | Or    | Or        |
     150  ----------+-----------+----------------+-----------+--------+-------+-----------+
     151  BVnonzero | Or        | --             | --        | --     | Or    | --        |
     152  ----------+-----------+----------------+-----------+--------+-------+-----------+
    115153*)
    116154definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
     
    118156  match a1 with
    119157  [ BVByte b1 ⇒
    120     match a2 with
    121     [ BVByte b2 ⇒
    122       ! carry ← Bit_of_val UnsupportedOp carry ;
    123       let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
    124       return 〈BVByte result, BBbit carry〉
    125     | BVptr bl2 p2 o2 ⇒
    126       match op with
    127       [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
    128       | Addc ⇒ be_add_sub_byte true carry a2 b1
    129       | _ ⇒ Error … [MSG UnsupportedOp]
    130       ]
    131     | BVnonzero ⇒
    132       match op with
    133       [ Or ⇒ return 〈BVnonzero, carry〉
    134       | _ ⇒ Error … [MSG UnsupportedOp]
    135       ]
    136     | _ ⇒ Error … [MSG UnsupportedOp]
    137     ]
    138   | BVptr bl1 p1 o1 ⇒
     158(*    if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then
     159      return 〈a2, carry〉
     160    else *) (* maybe it will be needed, need to see actual translations *)
     161      match a2 with
     162      [ BVByte b2 ⇒
     163        ! carry ← Bit_of_val UnsupportedOp carry ;
     164        let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
     165        return 〈BVByte result, BBbit carry〉
     166      | BVptr _ _ ⇒
     167        match op with
     168        [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
     169        | Addc ⇒ be_add_sub_byte true carry a2 b1
     170        | _ ⇒ Error … [MSG UnsupportedOp]
     171        ]
     172      | BVnonzero ⇒
     173        match op with
     174        [ Or ⇒ return 〈BVnonzero, carry〉
     175        | _ ⇒ Error … [MSG UnsupportedOp]
     176        ]
     177      | _ ⇒ Error … [MSG UnsupportedOp]
     178      ]
     179  | BVptr ptr1 p1 ⇒
    139180    match a2 with
    140181    [ BVByte b2 ⇒
     
    145186      | _ ⇒ Error … [MSG UnsupportedOp]
    146187      ]
    147     | BVptr bl2 p2 o2 ⇒
     188    | BVptr ptr2 p2 ⇒
    148189      match op with
    149190      [ Sub ⇒
    150         if eq_block bl1 bl2 ∧ eqb p1 p2 then
     191        match ptype ptr1 with
     192        [ Code ⇒ Error … [MSG UnsupportedOp]
     193        | XData ⇒
     194          if eq_block (pblock ptr1) (pblock ptr2) ∧
     195             eqb p1 p2
     196          then
    151197          ! carry ← Bit_of_val UnsupportedOp carry ;
    152           let by1 ≝ head' … o1 in
    153           let by2 ≝ head' … o2 in
    154           let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
    155           return 〈BVByte result, BBbit carry〉
    156         else Error … [MSG UnsupportedOp]
     198            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
     199            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
     200            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
     201            return 〈BVByte result, BBbit carry〉
     202          else Error … [MSG UnsupportedOp]
     203        ]
    157204      | Xor ⇒
    158         if eq_block bl1 bl2 ∧ eqb p1 p2 then
    159           if vprefix … (eq_bv 8) o1 o2 (* equivalent to equality *) then
    160             return 〈BVByte (bv_zero …), carry〉
    161           else
    162             return 〈BVnonzero, carry〉
     205        if eqb p1 p2 then
     206          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
    163207        else Error … [MSG UnsupportedOp]
    164208      | _ ⇒ Error … [MSG UnsupportedOp]
     
    168212      [ Xor ⇒
    169213        if eqb p1 p2 then
    170           return 〈BVnonzero, carry〉
     214          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
    171215        else
    172216          Error … [MSG UnsupportedOp]
     217      | _ ⇒ Error … [MSG UnsupportedOp]
     218      ]
     219    | _ ⇒ Error … [MSG UnsupportedOp]
     220    ]
     221  | BVnull p1 ⇒
     222    match op with
     223    [ Xor ⇒
     224      match a2 with
     225      [ BVptr ptr2 p2 ⇒
     226        if eqb p1 p2 then
     227          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
     228        else
     229          Error … [MSG UnsupportedOp]
     230      | BVnull p2 ⇒
     231        if eqb p1 p2 then
     232          return 〈BVXor (None ?) (None ?) p1, carry〉
     233        else
     234          Error … [MSG UnsupportedOp]
     235      | _ ⇒ Error … [MSG UnsupportedOp]
     236      ]
     237    | _ ⇒ Error … [MSG UnsupportedOp]
     238    ]
     239  | BVXor ptr1_opt ptr1_opt' p1 ⇒
     240    match op with
     241    [ Or ⇒
     242      match a2 with
     243      [ BVByte b2 ⇒
     244        if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
     245        else Error … [MSG UnsupportedOp]
     246      | BVnonzero ⇒ return 〈BVnonzero, carry〉
     247      | BVXor ptr2_opt ptr2_opt' p2 ⇒
     248        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
     249          let eq_at ≝ λp,ptr1,ptr2.
     250            eq_block (pblock ptr1) (pblock ptr2) ∧
     251            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
     252                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
     253          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
     254             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
     255          then return 〈BVByte (bv_zero …), carry〉
     256          else return 〈BVnonzero, carry〉
     257        else Error … [MSG UnsupportedOp]
    173258      | _ ⇒ Error … [MSG UnsupportedOp]
    174259      ]
     
    181266      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
    182267      | BVnonzero ⇒ return 〈BVnonzero, carry〉
    183       | _ ⇒ Error … [MSG UnsupportedOp]
    184       ]
    185     | _ ⇒ Error … [MSG UnsupportedOp]
    186     ]
    187   | BVnull p1 ⇒
    188     match op with
    189     [ Xor ⇒
    190       match a2 with
    191       [ BVptr _ p2 _ ⇒
    192         if eqb p1 p2 then
    193           return 〈BVnonzero, carry〉
    194         else
    195           Error … [MSG UnsupportedOp]
    196       | BVnull p2 ⇒
    197         if eqb p1 p2 then
    198           return 〈BVByte (bv_zero …), carry〉
    199         else
    200           Error … [MSG UnsupportedOp]
     268      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
    201269      | _ ⇒ Error … [MSG UnsupportedOp]
    202270      ]
     
    205273  | _ ⇒ Error … [MSG UnsupportedOp]
    206274  ].
    207 
Note: See TracChangeset for help on using the changeset viewer.