source: src/common/BackEndOps.ma @ 2989

Last change on this file since 2989 was 2975, checked in by tranquil, 8 years ago
  • RTL premain fixed
  • fixed bug in back end ops (subtracting to a porinter was reversed)
  • fixed globals initialization in LINToASM
File size: 12.1 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 op_of_add_or_sub : add_or_sub → Op2 ≝
133λwhat.match what with [ do_add ⇒ Addc | do_sub ⇒ Sub ].
134
135definition be_add_sub_byte : add_or_sub → bebit → beval → Byte → res (beval × bebit) ≝
136  λis_add,carry,a1,b2.
137  let op ≝ op_of_add_or_sub is_add in
138  match a1 with
139  [ BVByte b1 ⇒
140    ! carry' ← Bit_of_val UnsupportedOp carry ;
141    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
142    return 〈BVByte rslt, BBbit carry''〉
143  | BVptr ptr p ⇒
144    match ptype ptr with
145    [ Code ⇒ Error … [MSG UnsupportedOp]
146    | XData ⇒
147      match p with
148      [ O ⇒
149        ! carry' ← Bit_of_val UnsupportedOp carry ;
150        if carry' then Error … [MSG UnsupportedOp]
151        else
152          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
153          let 〈rslt,carry〉 ≝ op2 eval false op (\snd o1o0) b2 in
154          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
155          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
156          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
157      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
158        match carry with
159        [ BBptrcarry is_add' ptr' p' by' ⇒
160          if eq_add_or_sub is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
161            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
162          then If eqb p' 0 then with  prf do
163            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
164            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
165            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
166            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
167            let part1 ≝ mk_part 1 (le_n …) in
168            let ptr'' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
169            OK … 〈BVptr ptr'' part1,
170                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
171          else Error … [MSG UnsupportedOp]
172          else Error … [MSG UnsupportedOp]
173        | _ ⇒ Error … [MSG UnsupportedOp]
174        ]
175      ]
176    ]
177  | _ ⇒ Error … [MSG UnsupportedOp]
178  ].
179@hide_prf
180lapply prf @(eqb_elim p') #H * >H %
181qed.
182
183definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
184λn,v,p,H.
185let suffix : BitVector (8 + 8*p) ≝
186  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
187\fst (vsplit … suffix).
188>(commutative_times_fast ? p)
189change with (? = BitVector (? + S p*8))
190>(commutative_times_fast (S p))
191<distributive_times_plus_fast
192<(plus_minus_m_m … H) %
193qed.
194
195definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
196λA,eq,m,n.
197match m with
198[ Some a ⇒
199  match n with
200  [ Some b ⇒ eq a b
201  | _ ⇒ false
202  ]
203| _ ⇒
204  match m with
205  [ None ⇒ true
206  | _ ⇒ false
207  ]
208].
209
210(* This tables shows what binary ops may be defined on bevals depending on
211   the arguments (columns marked by 1st argument, rows by 2nd). Further
212   checks for definedness are done for pointer parts taking into account
213   blocks, parts and the carry value.
214   Neither BVundef nor BVpc allow any operations
215  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
216  ----------+-----------+----------------+-----------+--------+-------+-----------+
217  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
218  ----------+-----------+----------------+-----------+--------+-------+-----------+
219  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
220  ----------+-----------+----------------+-----------+--------+-------+-----------+
221  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
222  ----------+-----------+----------------+-----------+--------+-------+-----------+
223  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
224  ----------+-----------+----------------+-----------+--------+-------+-----------+
225  BVXor     | --        | --             | --        | --     | Or    | Or        |
226  ----------+-----------+----------------+-----------+--------+-------+-----------+
227  BVnonzero | Or        | --             | --        | --     | Or    | --        |
228  ----------+-----------+----------------+-----------+--------+-------+-----------+
229*)
230definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
231  λcarry,op,a1,a2.
232  match op with
233  [ Add ⇒
234    match a1 with
235    [ BVByte b1 ⇒ be_add_sub_byte do_add (BBbit false) a2 b1
236    | BVptr ptr1 p1 ⇒
237      match a2 with
238      [ BVByte b2 ⇒ be_add_sub_byte do_add (BBbit false) a1 b2
239      | _ ⇒ Error … [MSG UnsupportedOp]
240      ]
241    | _ ⇒ Error … [MSG UnsupportedOp]
242    ]
243  | Addc ⇒
244    match a1 with
245    [ BVByte b1 ⇒
246      be_add_sub_byte do_add carry a2 b1
247    | BVptr ptr1 p1 ⇒
248      match a2 with
249      [ BVByte b2 ⇒ be_add_sub_byte do_add carry a1 b2
250      | _ ⇒ Error … [MSG UnsupportedOp]
251      ]
252    | _ ⇒ Error … [MSG UnsupportedOp]
253    ]
254  | Sub ⇒
255    match a1 with
256    [ BVByte b1 ⇒
257      ! b2 ← Byte_of_val UnsupportedOp a2 ;
258      be_add_sub_byte do_sub carry a1 b2
259    | BVptr ptr1 p1 ⇒
260      match a2 with
261      [ BVByte b2 ⇒ be_add_sub_byte do_sub carry a1 b2
262      | BVptr ptr2 p2 ⇒
263        match ptype ptr1 with
264        [ Code ⇒ Error … [MSG UnsupportedOp]
265        | XData ⇒
266          if eq_block (pblock ptr1) (pblock ptr2) ∧
267             eqb p1 p2
268          then
269          ! carry ← Bit_of_val UnsupportedOp carry ;
270            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
271            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
272            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
273            return 〈BVByte result, BBbit carry〉
274          else Error … [MSG UnsupportedOp]
275        ]
276      | _ ⇒ Error … [MSG UnsupportedOp]
277      ]
278    | _ ⇒ Error … [MSG UnsupportedOp]
279    ]
280  | Or ⇒
281    match a1 with
282    [ BVByte b1 ⇒
283      match a2 with
284      [ BVByte b2 ⇒
285        let res ≝ \fst (op2 eval false Or b1 b2) in
286        return 〈BVByte res, carry〉
287      | BVnonzero ⇒ return 〈BVnonzero, carry〉
288      | _ ⇒ Error … [MSG UnsupportedOp]
289      ]
290    | BVXor ptr1_opt ptr1_opt' p1 ⇒
291      match a2 with
292      [ BVXor ptr2_opt ptr2_opt' p2 ⇒
293        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
294          let eq_at ≝ λp,ptr1,ptr2.
295            eq_block (pblock ptr1) (pblock ptr2) ∧
296            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
297                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
298          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
299             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
300          then return 〈BVByte (bv_zero …), carry〉
301          else return 〈BVnonzero, carry〉
302        else Error … [MSG UnsupportedOp]
303      | BVnonzero ⇒ return 〈BVnonzero, carry〉
304      | _ ⇒ Error … [MSG UnsupportedOp]
305      ]
306    | BVnonzero ⇒
307      match a2 with
308      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
309      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
310      | BVnonzero ⇒ return 〈BVnonzero, carry〉
311      | _ ⇒ Error … [MSG UnsupportedOp]
312      ]
313    | _ ⇒ Error … [MSG UnsupportedOp]
314    ]
315  | Xor ⇒
316    match a1 with
317    [ BVByte b1 ⇒
318      match a2 with
319      [ BVByte b2 ⇒
320        let res ≝ \fst (op2 eval false Xor b1 b2) in
321        return 〈BVByte res, carry〉
322      | _ ⇒ Error … [MSG UnsupportedOp]
323      ]
324    | BVptr ptr1 p1 ⇒
325      match a2 with
326      [ BVptr ptr2 p2 ⇒
327        if eqb p1 p2 then
328          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
329        else Error … [MSG UnsupportedOp]
330      | BVnull p2 ⇒
331        if eqb p1 p2 then
332          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
333        else
334          Error … [MSG UnsupportedOp]
335      | _ ⇒ Error … [MSG UnsupportedOp]
336      ]
337    | BVnull p1 ⇒
338      match a2 with
339      [ BVptr ptr2 p2 ⇒
340        if eqb p1 p2 then
341          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
342        else
343          Error … [MSG UnsupportedOp]
344      | BVnull p2 ⇒
345        if eqb p1 p2 then
346          return 〈BVXor (None ?) (None ?) p1, carry〉
347        else
348          Error … [MSG UnsupportedOp]
349      | _ ⇒ Error … [MSG UnsupportedOp]
350      ]
351    | _ ⇒ Error … [MSG UnsupportedOp]
352    ]
353  | And ⇒
354    ! b1 ← Byte_of_val UnsupportedOp a1 ;
355    ! b2 ← Byte_of_val UnsupportedOp a2 ;
356    let res ≝ \fst (op2 eval false And b1 b2) in
357    return 〈BVByte res, carry〉
358  ].
Note: See TracBrowser for help on using the repository browser.