source: src/common/BackEndOps.ma @ 2871

Last change on this file since 2871 was 2871, checked in by tranquil, 8 years ago

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 size: 11.9 KB
Line 
1include "common/ByteValues.ma".
2include "ASM/Arithmetic.ma".
3
4(* just to avoid computing div and mod separately *)
5definition divmodZ ≝ λx,y.
6  match x with
7  [ OZ ⇒ 〈OZ, OZ〉
8  | pos n ⇒
9    match y with
10    [ OZ ⇒ 〈OZ, OZ〉
11    | pos m ⇒ let 〈q, r〉 ≝ divide n m in
12              〈natp_to_Z q, natp_to_Z r〉
13    | neg m ⇒ let 〈q, r〉 ≝ divide n m in
14              match r with
15              [ pzero ⇒ 〈natp_to_negZ q, OZ〉
16              | _ ⇒ 〈Zpred (natp_to_negZ q), y+ natp_to_Z r〉
17              ]
18    ]
19  | neg n ⇒
20    match y with
21    [ OZ ⇒ 〈OZ, OZ〉
22    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
23              match r with
24              [ pzero ⇒ 〈natp_to_negZ q, OZ〉
25              | _ ⇒ 〈Zpred (natp_to_negZ q), y- natp_to_Z r〉
26              ]
27    | neg m ⇒ let 〈q, r〉 ≝ divide n m in
28              〈natp_to_Z q, natp_to_Z r〉
29    ]
30  ].
31
32(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
33        not further back in the translation chain.                            *)
34inductive OpAccs: Type[0] ≝
35  Mul: OpAccs
36| DivuModu: OpAccs.
37
38inductive Op1: Type[0] ≝
39  Cmpl: Op1
40| Inc: Op1
41| Rl: Op1.
42
43inductive Op2: Type[0] ≝
44  Add: Op2
45| Addc: Op2
46| Sub: Op2
47| And: Op2
48| Or: Op2
49| Xor: Op2.
50
51record Eval : Type[0] ≝
52{
53  opaccs: OpAccs → Byte → Byte → Byte × Byte;
54  op1: Op1 → Byte → Byte;
55  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
56}.
57
58definition opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte ≝
59λop,by1,by2.
60(* Paolo: in ASM/Interpret.ma we use nats, but using Z is more efficient, isn't it? *)
61let n1 ≝ Z_of_unsigned_bitvector … by1 in
62let n2 ≝ Z_of_unsigned_bitvector … by2 in
63match op with
64[ Mul ⇒
65  let prod ≝ vsplit … (bitvector_of_Z (8 + 8) (n1 * n2)) in
66  〈\snd prod, \fst prod〉
67| DivuModu ⇒
68  if eqZb n2 OZ then
69    (* to mimic ASM/Interpret.ma, we return the arguments *)
70    〈by1, by2〉
71  else
72    let 〈q, r〉 ≝ divmodZ n1 n2 in
73    〈bitvector_of_Z … q, bitvector_of_Z … r〉
74].
75
76definition op1_implementation: Op1 → Byte → Byte ≝
77λop,by.
78match op with
79[ Cmpl ⇒
80  negation_bv ? by
81| Inc ⇒
82  add … by (bitvector_of_nat 8 1)
83| Rl ⇒
84  rotate_left … 1 by
85].
86
87definition op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit) ≝
88λcarry,op,by1,by2.
89match op with
90[ Add ⇒
91  let 〈res, flags〉 ≝ add_8_with_carry by1 by2 false in
92  〈res, get_index' ? O  ? flags〉
93| Addc ⇒
94  let 〈res, flags〉 ≝ add_8_with_carry by1 by2 carry in
95  〈res, get_index' ? O  ? flags〉
96| Sub ⇒
97  let 〈res, flags〉 ≝ sub_8_with_carry by1 by2 carry in
98  〈res, get_index' ? O  ? flags〉
99| And ⇒
100  〈conjunction_bv ? by1 by2, carry〉
101| Or ⇒
102  〈inclusive_disjunction_bv ? by1 by2, carry〉
103| Xor ⇒
104  〈exclusive_disjunction_bv ? by1 by2, carry〉
105].
106
107definition eval : Eval ≝
108  mk_Eval opaccs_implementation
109          op1_implementation
110          op2_implementation.
111
112definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
113  λop,a,b.
114  ! a' ← Byte_of_val UnsupportedOp a ;
115  ! b' ← Byte_of_val UnsupportedOp b ;
116  let 〈a'',b''〉 ≝ opaccs eval op a' b' in
117  return 〈BVByte a'', BVByte b''〉.
118
119definition be_op1 : Op1 → beval → res beval ≝
120  λop,a.
121  ! a' ← Byte_of_val UnsupportedOp a ;
122  return BVByte (op1 eval op a').
123
124definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝
125λop,n,carry.
126  let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit.
127    let 〈res_tl, carry〉 ≝ pr in
128    let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in
129    〈res_hd ::: res_tl, carry'〉 in
130  fold_right2_i … f 〈[[ ]],carry〉 n.
131
132definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
133  λis_add,carry,a1,b2.
134  let op ≝ if is_add then Addc else Sub in
135  match a1 with
136  [ BVByte b1 ⇒
137    ! carry' ← Bit_of_val UnsupportedOp carry ;
138    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
139    return 〈BVByte rslt, BBbit carry''〉
140  | BVptr ptr p ⇒
141    match ptype ptr with
142    [ Code ⇒ Error … [MSG UnsupportedOp]
143    | XData ⇒
144      match p with
145      [ O ⇒
146        ! carry' ← Bit_of_val UnsupportedOp carry ;
147        if carry' then Error … [MSG UnsupportedOp]
148        else
149          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
150          let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
151          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
152          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
153          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
154      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
155        match carry with
156        [ BBptrcarry is_add' ptr' p' by' ⇒
157          if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
158            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
159          then If eqb p' 0 then with prf do
160            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
161            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
162            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
163            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
164            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,
167                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
168          else Error … [MSG UnsupportedOp]
169          else Error … [MSG UnsupportedOp]
170        | _ ⇒ Error … [MSG UnsupportedOp]
171        ]
172      ]
173    ]
174  | _ ⇒ Error … [MSG UnsupportedOp]
175  ].
176@hide_prf
177lapply prf @(eqb_elim p') #H * >H %
178qed.
179
180definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
181λn,v,p,H.
182let suffix : BitVector (8 + 8*p) ≝
183  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
184\fst (vsplit … suffix).
185>(commutative_times_fast ? p)
186change with (? = BitVector (? + S p*8))
187>(commutative_times_fast (S p))
188<distributive_times_plus_fast
189<(plus_minus_m_m … H) %
190qed.
191
192definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
193λA,eq,m,n.
194match m with
195[ Some a ⇒
196  match n with
197  [ Some b ⇒ eq a b
198  | _ ⇒ false
199  ]
200| _ ⇒
201  match m with
202  [ None ⇒ true
203  | _ ⇒ false
204  ]
205].
206
207(* This tables shows what binary ops may be defined on bevals depending on
208   the arguments (columns marked by 1st argument, rows by 2nd). Further
209   checks for definedness are done for pointer parts taking into account
210   blocks, parts and the carry value.
211   Neither BVundef nor BVpc allow any operations
212  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
213  ----------+-----------+----------------+-----------+--------+-------+-----------+
214  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
215  ----------+-----------+----------------+-----------+--------+-------+-----------+
216  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
217  ----------+-----------+----------------+-----------+--------+-------+-----------+
218  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
219  ----------+-----------+----------------+-----------+--------+-------+-----------+
220  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
221  ----------+-----------+----------------+-----------+--------+-------+-----------+
222  BVXor     | --        | --             | --        | --     | Or    | Or        |
223  ----------+-----------+----------------+-----------+--------+-------+-----------+
224  BVnonzero | Or        | --             | --        | --     | Or    | --        |
225  ----------+-----------+----------------+-----------+--------+-------+-----------+
226*)
227definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
228  λcarry,op,a1,a2.
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 ⇒
257        match ptype ptr1 with
258        [ Code ⇒ Error … [MSG UnsupportedOp]
259        | XData ⇒
260          if eq_block (pblock ptr1) (pblock ptr2) ∧
261             eqb p1 p2
262          then
263          ! carry ← Bit_of_val UnsupportedOp carry ;
264            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
265            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
266            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
267            return 〈BVByte result, BBbit carry〉
268          else Error … [MSG UnsupportedOp]
269        ]
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 ⇒
287        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
288          let eq_at ≝ λp,ptr1,ptr2.
289            eq_block (pblock ptr1) (pblock ptr2) ∧
290            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
291                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
292          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
293             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
294          then return 〈BVByte (bv_zero …), carry〉
295          else return 〈BVnonzero, carry〉
296        else Error … [MSG UnsupportedOp]
297      | BVnonzero ⇒ return 〈BVnonzero, carry〉
298      | _ ⇒ Error … [MSG UnsupportedOp]
299      ]
300    | BVnonzero ⇒
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〉
352  ].
Note: See TracBrowser for help on using the repository browser.