source: src/common/BackEndOps.ma @ 2783

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

implemented back end ops that were still axioms

File size: 12.3 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 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 ⇒
264        match ptype ptr1 with
265        [ Code ⇒ Error … [MSG UnsupportedOp]
266        | XData ⇒
267          if eq_block (pblock ptr1) (pblock ptr2) ∧
268             eqb p1 p2
269          then
270          ! carry ← Bit_of_val UnsupportedOp carry ;
271            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
272            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
273            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
274            return 〈BVByte result, BBbit carry〉
275          else Error … [MSG UnsupportedOp]
276        ]
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 ⇒
334        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
335          let eq_at ≝ λp,ptr1,ptr2.
336            eq_block (pblock ptr1) (pblock ptr2) ∧
337            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
338                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
339          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
340             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
341          then return 〈BVByte (bv_zero …), carry〉
342          else return 〈BVnonzero, carry〉
343        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〉
353      | _ ⇒ Error … [MSG UnsupportedOp]
354      ]
355    | 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]
368  ].
Note: See TracBrowser for help on using the repository browser.