source: src/common/BackEndOps.ma @ 2435

Last change on this file since 2435 was 2435, checked in by tranquil, 7 years ago

new back end operations

File size: 9.8 KB
Line 
1include "common/ByteValues.ma".
2
3(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
4        not further back in the translation chain.                            *)
5inductive OpAccs: Type[0] ≝
6  Mul: OpAccs
7| DivuModu: OpAccs.
8
9inductive Op1: Type[0] ≝
10  Cmpl: Op1
11| Inc: Op1
12| Rl: Op1. (* TODO: implement left rotation *)
13
14inductive Op2: Type[0] ≝
15  Add: Op2
16| Addc: Op2
17| Sub: Op2
18| And: Op2
19| Or: Op2
20| Xor: Op2.
21
22record Eval : Type[0] ≝
23{
24  opaccs: OpAccs → Byte → Byte → Byte × Byte;
25  op1: Op1 → Byte → Byte;
26  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
27}.
28
29axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
30axiom op1_implementation: Op1 → Byte → Byte.
31axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
32
33definition eval : Eval ≝
34  mk_Eval opaccs_implementation
35          op1_implementation
36          op2_implementation.
37
38axiom UnsupportedOp : String.
39
40definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
41  λop,a,b.
42  ! a' ← Byte_of_val UnsupportedOp a ;
43  ! b' ← Byte_of_val UnsupportedOp b ;
44  let 〈a'',b''〉 ≝ opaccs eval op a' b' in
45  return 〈BVByte a'', BVByte b''〉.
46
47definition be_op1 : Op1 → beval → res beval ≝
48  λop,a.
49  ! a' ← Byte_of_val UnsupportedOp a ;
50  return BVByte (op1 eval op a').
51
52definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝
53λop,n,carry.
54  let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit.
55    let 〈res_tl, carry〉 ≝ pr in
56    let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in
57    〈res_hd ::: res_tl, carry'〉 in
58  fold_right2_i … f 〈[[ ]],carry〉 n.
59
60definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
61  λis_add,carry,a1,b2.
62  let op ≝ if is_add then Addc else Sub in
63  match a1 with
64  [ BVByte b1 ⇒
65    ! carry' ← Bit_of_val UnsupportedOp carry ;
66    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
67    return 〈BVByte rslt, BBbit carry''〉
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')〉
96          else Error … [MSG UnsupportedOp]
97          else Error … [MSG UnsupportedOp]
98        | _ ⇒ Error … [MSG UnsupportedOp]
99        ]
100      ]
101    ]
102  | _ ⇒ Error … [MSG UnsupportedOp]
103  ].
104@hide_prf
105lapply prf @(eqb_elim p') #H * >H %
106qed.
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].
134
135(* This tables shows what binary ops may be defined on bevals depending on
136   the arguments (columns marked by 1st argument, rows by 2nd). Further
137   checks for definedness are done for pointer parts taking into account
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  ----------+-----------+----------------+-----------+--------+-------+-----------+
153*)
154definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
155  λcarry,op,a1,a2.
156  match a1 with
157  [ BVByte b1 ⇒
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 ⇒
180    match a2 with
181    [ BVByte b2 ⇒
182      match op with
183      [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
184      | Addc ⇒ be_add_sub_byte true carry a1 b2
185      | Sub ⇒ be_add_sub_byte false carry a1 b2
186      | _ ⇒ Error … [MSG UnsupportedOp]
187      ]
188    | BVptr ptr2 p2 ⇒
189      match op with
190      [ Sub ⇒
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
197          ! carry ← Bit_of_val UnsupportedOp carry ;
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        ]
204      | Xor ⇒
205        if eqb p1 p2 then
206          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
207        else Error … [MSG UnsupportedOp]
208      | _ ⇒ Error … [MSG UnsupportedOp]
209      ]
210    | BVnull p2 ⇒
211      match op with
212      [ Xor ⇒
213        if eqb p1 p2 then
214          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
215        else
216          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]
258      | _ ⇒ Error … [MSG UnsupportedOp]
259      ]
260    | _ ⇒ Error … [MSG UnsupportedOp]
261    ]
262  | BVnonzero ⇒
263    match op with
264    [ Or ⇒
265      match a2 with
266      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
267      | BVnonzero ⇒ return 〈BVnonzero, carry〉
268      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
269      | _ ⇒ Error … [MSG UnsupportedOp]
270      ]
271    | _ ⇒ Error … [MSG UnsupportedOp]
272    ]
273  | _ ⇒ Error … [MSG UnsupportedOp]
274  ].
Note: See TracBrowser for help on using the repository browser.