source: src/common/FrontEndOps.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 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.