source: src/common/FrontEndOps.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.
File size: 14.9 KB
Line 
1(* Operations common to the Cminor and RTLabs front end stages. *)
2
3(* Adapted from CompCert's Cminor.ma: *)
4
5(* *********************************************************************)
6(*                                                                     *)
7(*              The Compcert verified compiler                         *)
8(*                                                                     *)
9(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
10(*                                                                     *)
11(*  Copyright Institut National de Recherche en Informatique et en     *)
12(*  Automatique.  All rights reserved.  This file is distributed       *)
13(*  under the terms of the GNU General Public License as published by  *)
14(*  the Free Software Foundation, either version 2 of the License, or  *)
15(*  (at your option) any later version.  This file is also distributed *)
16(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
17(*                                                                     *)
18(* *********************************************************************)
19
20include "common/Values.ma".
21
22inductive constant : Type[0] ≝
23  | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
24  | Ofloatconst: float → constant          (**r floating-point constant *)
25  | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
26  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
27
28inductive unary_operation : Type[0] ≝
29  | Ocastint: intsize → signedness → unary_operation (**r 8-bit zero extension  *)
30  | Onegint: unary_operation               (**r integer opposite *)
31  | Onotbool: unary_operation              (**r boolean negation  *)
32  | Onotint: unary_operation               (**r bitwise complement  *)
33  | Onegf: unary_operation                 (**r float opposite *)
34  | Oabsf: unary_operation                 (**r float absolute value *)
35  | Osingleoffloat: unary_operation        (**r float truncation *)
36  | Ointoffloat: intsize → unary_operation (**r signed integer to float *)
37  | Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *)
38  | Ofloatofint: unary_operation           (**r float to signed integer *)
39  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
40  | Oid: unary_operation                   (**r identity (used to move between registers *)
41  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
42  | Ointofptr: intsize → unary_operation.  (**r pointer to int *)
43
44inductive binary_operation : Type[0] ≝
45  | Oadd: binary_operation                 (**r integer addition *)
46  | Osub: binary_operation                 (**r integer subtraction *)
47  | Omul: binary_operation                 (**r integer multiplication *)
48  | Odiv: binary_operation                 (**r integer signed division *)
49  | Odivu: binary_operation                (**r integer unsigned division *)
50  | Omod: binary_operation                 (**r integer signed modulus *)
51  | Omodu: binary_operation                (**r integer unsigned modulus *)
52  | Oand: binary_operation                 (**r bitwise ``and'' *)
53  | Oor: binary_operation                  (**r bitwise ``or'' *)
54  | Oxor: binary_operation                 (**r bitwise ``xor'' *)
55  | Oshl: binary_operation                 (**r left shift *)
56  | Oshr: binary_operation                 (**r right signed shift *)
57  | Oshru: binary_operation                (**r right unsigned shift *)
58  | Oaddf: binary_operation                (**r float addition *)
59  | Osubf: binary_operation                (**r float subtraction *)
60  | Omulf: binary_operation                (**r float multiplication *)
61  | Odivf: binary_operation                (**r float division *)
62  | Ocmp: comparison -> binary_operation   (**r integer signed comparison *)
63  | Ocmpu: comparison -> binary_operation  (**r integer unsigned comparison *)
64  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
65  | Oaddp: binary_operation                (**r add an integer to a pointer *)
66  | Osubpi: binary_operation               (**r subtract int from a pointers *)
67  | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
68  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
69
70
71(* * Evaluation of constants and operator applications.
72    [None] is returned when the computation is undefined, e.g.
73    if arguments are of the wrong types, or in case of an integer division
74    by zero. *)
75
76definition eval_constant : (ident → option block) → block → constant → option val ≝
77λfind_symbol,sp,cst.
78  match cst with
79  [ Ointconst sz n ⇒ Some ? (Vint sz n)
80  | Ofloatconst n ⇒ Some ? (Vfloat n)
81  | Oaddrsymbol s ofs ⇒
82      match find_symbol s with
83      [ None ⇒ None ?
84      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
85      ]
86  | Oaddrstack ofs ⇒
87      Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
88  ]. cases sp // qed.
89
90definition eval_unop : unary_operation → val → option val ≝
91λop,arg.
92  match op with
93  [ Ocastint sz sg ⇒
94      match sg with
95      [ Unsigned ⇒ Some ? (zero_ext sz arg)
96      |   Signed ⇒ Some ? (sign_ext sz arg)
97      ]
98  | Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
99  | Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?)))
100                              | Vptr _ _ _ _ ⇒ Some ? Vfalse
101                              | Vnull _ ⇒ Some ? Vtrue
102                              | _ ⇒ None ?
103                              ]
104  | Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
105  | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
106  | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
107  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
108  | Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
109  | Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
110  | Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
111  | Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
112  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
113  (* Only conversion of null pointers is specified. *)
114  | Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
115  | Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
116  ].
117
118(* I think this is duplicated somewhere else *)
119definition eval_compare_mismatch : comparison → option val ≝
120λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
121
122(* Individual operations, adapted from Values.  These differ in that they
123   implement the plain Cminor/RTLabs operations (e.g., with separate addition
124   for ints,floats and pointers) and use option rather than Vundef.  The ones
125   in Value are probably not needed. *)
126
127definition ev_add ≝ λv1,v2: val.
128  match v1 with
129  [ Vint sz1 n1 ⇒ match v2 with
130    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
131                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
132                    (None ?)
133    | _ ⇒ None ? ]
134  | _ ⇒ None ? ].
135
136definition ev_sub ≝ λv1,v2: val.
137  match v1 with
138  [ Vint sz1 n1 ⇒ match v2 with
139    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
140                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
141                    (None ?)
142    | _ ⇒ None ? ]
143  | _ ⇒ None ? ].
144
145(* NB: requires arguments to be presented pointer first. *)
146definition ev_addp ≝ λv1,v2: val.
147  match v1 with
148  [ Vptr r b1 p ofs1 ⇒ match v2 with
149    [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
150    | _ ⇒ None ? ]
151  | Vnull r ⇒ match v2 with
152    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
153    | _ ⇒ None ?
154    ]
155  | _ ⇒ None ? ].
156
157definition ev_subpi ≝ λv1,v2: val.
158  match v1 with
159  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
160    [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
161    | _ ⇒ None ? ]
162  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
163  | _ ⇒ None ? ].
164
165definition ev_subpp ≝ λsz. λv1,v2: val.
166  match v1 with
167  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
168    [ Vptr r2 b2 p2 ofs2 ⇒
169        if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
170    | _ ⇒ None ? ]
171  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
172  | _ ⇒ None ? ].
173
174definition ev_mul ≝ λv1, v2: val.
175  match v1 with
176  [ Vint sz1 n1 ⇒ match v2 with
177    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
178                    (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
179                    (None ?)
180    | _ ⇒ None ? ]
181  | _ ⇒ None ? ].
182
183definition ev_divs ≝ λv1, v2: val.
184  match v1 with
185  [ Vint sz1 n1 ⇒ match v2 with
186    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
187                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
188                    (None ?)
189    | _ ⇒ None ? ]
190  | _ ⇒ None ? ].
191
192definition ev_mods ≝ λv1, v2: val.
193  match v1 with
194  [ Vint sz1 n1 ⇒ match v2 with
195    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
196                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
197                    (None ?)
198    | _ ⇒ None ?
199    ]
200  | _ ⇒ None ?
201  ].
202
203definition ev_divu ≝ λv1, v2: val.
204  match v1 with
205  [ Vint sz1 n1 ⇒ match v2 with
206    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
207                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
208                    (None ?)
209    | _ ⇒ None ?
210    ]
211  | _ ⇒ None ?
212  ].
213
214definition ev_modu ≝ λv1, v2: val.
215  match v1 with
216  [ Vint sz1 n1 ⇒ match v2 with
217    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
218                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
219                    (None ?)
220    | _ ⇒ None ?
221    ]
222  | _ ⇒ None ?
223  ].
224
225definition ev_and ≝ λv1, v2: val.
226  match v1 with
227  [ Vint sz1 n1 ⇒ match v2 with
228    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
229                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
230                    (None ?)
231    | _ ⇒ None ? ]
232  | _ ⇒ None ? ].
233
234definition ev_or ≝ λv1, v2: val.
235  match v1 with
236  [ Vint sz1 n1 ⇒ match v2 with
237    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
238                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
239                    (None ?)
240    | _ ⇒ None ? ]
241  | _ ⇒ None ? ].
242
243definition ev_xor ≝ λv1, v2: val.
244  match v1 with
245  [ Vint sz1 n1 ⇒ match v2 with
246    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
247                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
248                    (None ?)
249    | _ ⇒ None ? ]
250  | _ ⇒ None ? ].
251
252definition ev_shl ≝ λv1, v2: val.
253  match v1 with
254  [ Vint sz1 n1 ⇒ match v2 with
255    [ Vint sz2 n2 ⇒
256       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
257       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
258       else None ?
259    | _ ⇒ None ? ]
260  | _ ⇒ None ? ].
261
262definition ev_shr ≝ λv1, v2: val.
263  match v1 with
264  [ Vint sz1 n1 ⇒ match v2 with
265    [ Vint sz2 n2 ⇒
266       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
267       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
268       else None ?
269    | _ ⇒ None ? ]
270  | _ ⇒ None ? ].
271
272definition ev_shru ≝ λv1, v2: val.
273  match v1 with
274  [ Vint sz1 n1 ⇒ match v2 with
275    [ Vint sz2 n2 ⇒
276       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
277       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
278       else None ?
279    | _ ⇒ None ? ]
280  | _ ⇒ None ? ].
281
282definition ev_addf ≝ λv1,v2: val.
283  match v1 with
284  [ Vfloat f1 ⇒ match v2 with
285    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
286    | _ ⇒ None ? ]
287  | _ ⇒ None ? ].
288
289definition ev_subf ≝ λv1,v2: val.
290  match v1 with
291  [ Vfloat f1 ⇒ match v2 with
292    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
293    | _ ⇒ None ? ]
294  | _ ⇒ None ? ].
295
296definition ev_mulf ≝ λv1,v2: val.
297  match v1 with
298  [ Vfloat f1 ⇒ match v2 with
299    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
300    | _ ⇒ None ? ]
301  | _ ⇒ None ? ].
302
303definition ev_divf ≝ λv1,v2: val.
304  match v1 with
305  [ Vfloat f1 ⇒ match v2 with
306    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
307    | _ ⇒ None ? ]
308  | _ ⇒ None ? ].
309
310definition ev_cmp_match : comparison → option val ≝ λc.
311  match c with
312  [ Ceq ⇒ Some ? Vtrue
313  | Cne ⇒ Some ? Vfalse
314  | _   ⇒ None ?
315  ].
316
317definition ev_cmp_mismatch : comparison → option val ≝ λc.
318  match c with
319  [ Ceq ⇒ Some ? Vfalse
320  | Cne ⇒ Some ? Vtrue
321  | _   ⇒ None ?
322  ].
323
324definition ev_cmp ≝ λc: comparison. λv1,v2: val.
325  match v1 with
326  [ Vint sz1 n1 ⇒ match v2 with
327    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
328                    (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
329                    (None ?)
330    | _ ⇒ None ? ]
331  | _ ⇒ None ? ].
332
333definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
334  match v1 with
335  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
336    [ Vptr r2 b2 p2 ofs2 ⇒
337        if eq_block b1 b2
338        then Some ? (of_bool (cmp_offset c ofs1 ofs2))
339        else ev_cmp_mismatch c
340    | Vnull r2 ⇒ ev_cmp_mismatch c
341    | _ ⇒ None ? ]
342  | Vnull r1 ⇒ match v2 with
343    [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
344    | Vnull r2 ⇒ ev_cmp_match c
345    | _ ⇒ None ?
346    ]
347  | _ ⇒ None ? ].
348
349(* TODO: check this, it isn't the cmpu used elsewhere *)
350definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
351  match v1 with
352  [ Vint sz1 n1 ⇒ match v2 with
353    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
354                    (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
355                    (None ?)
356    | _ ⇒ None ? ]
357  | _ ⇒ None ? ].
358
359definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
360  match v1 with
361  [ Vfloat f1 ⇒ match v2 with
362    [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
363    | _ ⇒ None ? ]
364  | _ ⇒ None ? ].
365
366definition eval_binop : binary_operation → val → val → option val ≝
367λop.
368  match op with
369  [ Oadd ⇒ ev_add
370  | Osub ⇒ ev_sub
371  | Omul ⇒ ev_mul
372  | Odiv ⇒ ev_divs
373  | Odivu ⇒ ev_divu
374  | Omod ⇒ ev_mods
375  | Omodu ⇒ ev_modu
376  | Oand ⇒ ev_and
377  | Oor ⇒ ev_or
378  | Oxor ⇒ ev_xor
379  | Oshl ⇒ ev_shl
380  | Oshr ⇒ ev_shr
381  | Oshru ⇒ ev_shru
382  | Oaddf ⇒ ev_addf
383  | Osubf ⇒ ev_subf
384  | Omulf ⇒ ev_mulf
385  | Odivf ⇒ ev_divf
386  | Ocmp c ⇒ ev_cmp c
387  | Ocmpu c ⇒ ev_cmpu c
388  | Ocmpf c ⇒ ev_cmpf c
389  | Oaddp ⇒ ev_addp
390  | Osubpi ⇒ ev_subpi
391  | Osubpp sz ⇒ ev_subpp sz
392  | Ocmpp c ⇒ ev_cmpp c
393  ].
394
Note: See TracBrowser for help on using the repository browser.