source: src/common/FrontEndOps.ma @ 774

Last change on this file since 774 was 774, checked in by campbell, 9 years ago

Separate out the different forms of addition and subtraction in the frontend ops.

File size: 15.6 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: int → constant     (**r integer constant *)
24  | Ofloatconst: float → constant (**r floating-point constant *)
25  | Oaddrsymbol: ident → int → constant (**r address of the symbol plus the offset *)
26  | Oaddrstack: int → constant.   (**r stack pointer plus the given offset *)
27
28inductive unary_operation : Type[0] ≝
29  | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
30  | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
31  | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
32  | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
33  | Onegint: unary_operation               (**r integer opposite *)
34  | Onotbool: unary_operation              (**r boolean negation  *)
35  | Onotint: unary_operation               (**r bitwise complement  *)
36  | Onegf: unary_operation                 (**r float opposite *)
37  | Oabsf: unary_operation                 (**r float absolute value *)
38  | Osingleoffloat: unary_operation        (**r float truncation *)
39  | Ointoffloat: unary_operation           (**r signed integer to float *)
40  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
41  | Ofloatofint: unary_operation           (**r float to signed integer *)
42  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
43  | Oid: unary_operation                   (**r identity (used to move between registers *)
44  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
45  | Ointofptr: unary_operation.            (**r pointer to int *)
46
47inductive binary_operation : Type[0] ≝
48  | Oadd: binary_operation                 (**r integer addition *)
49  | Osub: binary_operation                 (**r integer subtraction *)
50  | Omul: binary_operation                 (**r integer multiplication *)
51  | Odiv: binary_operation                 (**r integer signed division *)
52  | Odivu: binary_operation                (**r integer unsigned division *)
53  | Omod: binary_operation                 (**r integer signed modulus *)
54  | Omodu: binary_operation                (**r integer unsigned modulus *)
55  | Oand: binary_operation                 (**r bitwise ``and'' *)
56  | Oor: binary_operation                  (**r bitwise ``or'' *)
57  | Oxor: binary_operation                 (**r bitwise ``xor'' *)
58  | Oshl: binary_operation                 (**r left shift *)
59  | Oshr: binary_operation                 (**r right signed shift *)
60  | Oshru: binary_operation                (**r right unsigned shift *)
61  | Oaddf: binary_operation                (**r float addition *)
62  | Osubf: binary_operation                (**r float subtraction *)
63  | Omulf: binary_operation                (**r float multiplication *)
64  | Odivf: binary_operation                (**r float division *)
65  | Ocmp: comparison -> binary_operation   (**r integer signed comparison *)
66  | Ocmpu: comparison -> binary_operation  (**r integer unsigned comparison *)
67  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
68  | Oaddp: binary_operation                (**r add an integer to a pointer *)
69  | Osubpi: binary_operation               (**r subtract int from a pointers *)
70  | Osubpp: binary_operation               (**r subtract two pointers *)
71  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
72
73
74(* * Evaluation of constants and operator applications.
75    [None] is returned when the computation is undefined, e.g.
76    if arguments are of the wrong types, or in case of an integer division
77    by zero. *)
78
79definition eval_constant : (ident → option block) → block → constant → option val ≝
80λfind_symbol,sp,cst.
81  match cst with
82  [ Ointconst n ⇒ Some ? (Vint n)
83  | Ofloatconst n ⇒ Some ? (Vfloat n)
84  | Oaddrsymbol s ofs ⇒
85      match find_symbol s with
86      [ None ⇒ None ?
87      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))
88      ]
89  | Oaddrstack ofs ⇒
90      Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))
91  ]. cases sp // qed.
92
93definition eval_unop : unary_operation → val → option val ≝
94λop,arg.
95  match op with
96  [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg)
97  | Ocast8signed ⇒ Some ? (sign_ext 8 arg)
98  | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg)
99  | Ocast16signed ⇒ Some ? (sign_ext 16 arg)
100  | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ]
101  | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero))
102                              | Vptr _ _ _ _ ⇒ Some ? Vfalse
103                              | Vnull _ ⇒ Some ? Vtrue
104                              | _ ⇒ None ?
105                              ]
106  | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ]
107  | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
108  | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
109  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
110  | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ]
111  | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ]
112  | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
113  | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
114  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
115  (* Only conversion of null pointers is specified. *)
116  | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
117  | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
118  ].
119
120(* I think this is duplicated somewhere else *)
121definition eval_compare_mismatch : comparison → option val ≝
122λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
123
124(* Individual operations, adapted from Values. *)
125
126definition ev_neg : val → option val ≝ λv.
127  match v with
128  [ Vint n ⇒ Some ? (Vint (neg n))
129  | _ ⇒ None ?
130  ].
131
132definition ev_negf : val → option val ≝ λv.
133  match v with
134  [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
135  | _ ⇒ None ?
136  ].
137
138definition ev_absf : val → option val ≝ λv.
139  match v with
140  [ Vfloat f ⇒ Some ? (Vfloat (Fabs f))
141  | _ ⇒ None ?
142  ].
143
144definition ev_intoffloat : val → option val ≝ λv.
145  match v with
146  [ Vfloat f ⇒ Some ? (Vint (intoffloat f))
147  | _ ⇒ None ?
148  ].
149
150definition ev_intuoffloat : val → option val ≝ λv.
151  match v with
152  [ Vfloat f ⇒ Some ? (Vint (intuoffloat f))
153  | _ ⇒ None ?
154  ].
155
156definition ev_floatofint : val → option val ≝ λv.
157  match v with
158  [ Vint n ⇒ Some ? (Vfloat (floatofint n))
159  | _ ⇒ None ?
160  ].
161
162definition ev_floatofintu : val → option val ≝ λv.
163  match v with
164  [ Vint n ⇒ Some ? (Vfloat (floatofintu n))
165  | _ ⇒ None ?
166  ].
167
168definition ev_notint : val → option val ≝ λv.
169  match v with
170  [ Vint n ⇒ Some ? (Vint (xor n mone))
171  | _ ⇒ None ?
172  ].
173 
174definition ev_notbool : val → option val ≝ λv.
175  match v with
176  [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
177  | Vptr _ b _ ofs ⇒ Some ? Vfalse
178  | Vnull _ ⇒ Some ? Vtrue
179  | _ ⇒ None ?
180  ].
181
182definition ev_zero_ext ≝ λnbits: nat. λv: val.
183  match v with
184  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
185  | _ ⇒ None ?
186  ].
187
188definition ev_sign_ext ≝ λnbits:nat. λv:val.
189  match v with
190  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
191  | _ ⇒ None ?
192  ].
193
194definition ev_singleoffloat : val → option val ≝ λv.
195  match v with
196  [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
197  | _ ⇒ None ?
198  ].
199
200definition ev_add ≝ λv1,v2: val.
201  match v1 with
202  [ Vint n1 ⇒ match v2 with
203    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
204    | _ ⇒ None ? ]
205  | _ ⇒ None ? ].
206
207definition ev_sub ≝ λv1,v2: val.
208  match v1 with
209  [ Vint n1 ⇒ match v2 with
210    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
211    | _ ⇒ None ? ]
212  | _ ⇒ None ? ].
213
214(* NB: requires arguments to be presented pointer first. *)
215definition ev_addp ≝ λv1,v2: val.
216  match v1 with
217  [ Vptr r b1 p ofs1 ⇒ match v2 with
218    [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
219    | _ ⇒ None ? ]
220  | Vnull r ⇒ match v2 with
221    [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
222    | _ ⇒ None ?
223    ]
224  | _ ⇒ None ? ].
225
226definition ev_subpi ≝ λv1,v2: val.
227  match v1 with
228  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
229    [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
230    | _ ⇒ None ? ]
231  | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
232  | _ ⇒ None ? ].
233
234definition ev_subpp ≝ λv1,v2: val.
235  match v1 with
236  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
237    [ Vptr r2 b2 p2 ofs2 ⇒
238        if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
239    | _ ⇒ None ? ]
240  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
241  | _ ⇒ None ? ].
242
243definition ev_mul ≝ λv1, v2: val.
244  match v1 with
245  [ Vint n1 ⇒ match v2 with
246    [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
247    | _ ⇒ None ? ]
248  | _ ⇒ None ? ].
249
250definition ev_divs ≝ λv1, v2: val.
251  match v1 with
252  [ Vint n1 ⇒ match v2 with
253    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
254    | _ ⇒ None ? ]
255  | _ ⇒ None ? ].
256
257definition ev_mods ≝ λv1, v2: val.
258  match v1 with
259  [ Vint n1 ⇒ match v2 with
260    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
261    | _ ⇒ None ?
262    ]
263  | _ ⇒ None ?
264  ].
265
266definition ev_divu ≝ λv1, v2: val.
267  match v1 with
268  [ Vint n1 ⇒ match v2 with
269    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
270    | _ ⇒ None ?
271    ]
272  | _ ⇒ None ?
273  ].
274
275definition ev_modu ≝ λv1, v2: val.
276  match v1 with
277  [ Vint n1 ⇒ match v2 with
278    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
279    | _ ⇒ None ?
280    ]
281  | _ ⇒ None ?
282  ].
283
284definition ev_and ≝ λv1, v2: val.
285  match v1 with
286  [ Vint n1 ⇒ match v2 with
287    [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
288    | _ ⇒ None ? ]
289  | _ ⇒ None ? ].
290
291definition ev_or ≝ λv1, v2: val.
292  match v1 with
293  [ Vint n1 ⇒ match v2 with
294    [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
295    | _ ⇒ None ? ]
296  | _ ⇒ None ? ].
297
298definition ev_xor ≝ λv1, v2: val.
299  match v1 with
300  [ Vint n1 ⇒ match v2 with
301    [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
302    | _ ⇒ None ? ]
303  | _ ⇒ None ? ].
304
305definition ev_shl ≝ λv1, v2: val.
306  match v1 with
307  [ Vint n1 ⇒ match v2 with
308    [ Vint n2 ⇒
309       if ltu n2 iwordsize
310       then Some ? (Vint (shl n1 n2))
311       else None ?
312    | _ ⇒ None ? ]
313  | _ ⇒ None ? ].
314
315definition ev_shr ≝ λv1, v2: val.
316  match v1 with
317  [ Vint n1 ⇒ match v2 with
318    [ Vint n2 ⇒
319       if ltu n2 iwordsize
320       then Some ? (Vint (shr n1 n2))
321       else None ?
322    | _ ⇒ None ? ]
323  | _ ⇒ None ? ].
324
325definition ev_shr_carry ≝ λv1, v2: val.
326  match v1 with
327  [ Vint n1 ⇒ match v2 with
328    [ Vint n2 ⇒
329       if ltu n2 iwordsize
330       then Some ? (Vint (shr_carry n1 n2))
331       else None ?
332    | _ ⇒ None ? ]
333  | _ ⇒ None ? ].
334
335definition ev_shrx ≝ λv1, v2: val.
336  match v1 with
337  [ Vint n1 ⇒ match v2 with
338    [ Vint n2 ⇒
339       if ltu n2 iwordsize
340       then Some ? (Vint (shrx n1 n2))
341       else None ?
342    | _ ⇒ None ? ]
343  | _ ⇒ None ? ].
344
345definition ev_shru ≝ λv1, v2: val.
346  match v1 with
347  [ Vint n1 ⇒ match v2 with
348    [ Vint n2 ⇒
349       if ltu n2 iwordsize
350       then Some ? (Vint (shru n1 n2))
351       else None ?
352    | _ ⇒ None ? ]
353  | _ ⇒ None ? ].
354
355definition ev_rolm ≝
356λv: val. λamount, mask: int.
357  match v with
358  [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
359  | _ ⇒ None ?
360  ].
361
362definition ev_ror ≝ λv1, v2: val.
363  match v1 with
364  [ Vint n1 ⇒ match v2 with
365    [ Vint n2 ⇒
366       if ltu n2 iwordsize
367       then Some ? (Vint (ror n1 n2))
368       else None ?
369    | _ ⇒ None ? ]
370  | _ ⇒ None ? ].
371
372definition ev_addf ≝ λv1,v2: val.
373  match v1 with
374  [ Vfloat f1 ⇒ match v2 with
375    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
376    | _ ⇒ None ? ]
377  | _ ⇒ None ? ].
378
379definition ev_subf ≝ λv1,v2: val.
380  match v1 with
381  [ Vfloat f1 ⇒ match v2 with
382    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
383    | _ ⇒ None ? ]
384  | _ ⇒ None ? ].
385
386definition ev_mulf ≝ λv1,v2: val.
387  match v1 with
388  [ Vfloat f1 ⇒ match v2 with
389    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
390    | _ ⇒ None ? ]
391  | _ ⇒ None ? ].
392
393definition ev_divf ≝ λv1,v2: val.
394  match v1 with
395  [ Vfloat f1 ⇒ match v2 with
396    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
397    | _ ⇒ None ? ]
398  | _ ⇒ None ? ].
399
400definition ev_cmp_match : comparison → option val ≝ λc.
401  match c with
402  [ Ceq ⇒ Some ? Vtrue
403  | Cne ⇒ Some ? Vfalse
404  | _   ⇒ None ?
405  ].
406
407definition ev_cmp_mismatch : comparison → option val ≝ λc.
408  match c with
409  [ Ceq ⇒ Some ? Vfalse
410  | Cne ⇒ Some ? Vtrue
411  | _   ⇒ None ?
412  ].
413
414definition ev_cmp ≝ λc: comparison. λv1,v2: val.
415  match v1 with
416  [ Vint n1 ⇒ match v2 with
417    [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
418    | _ ⇒ None ? ]
419  | _ ⇒ None ? ].
420
421definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
422  match v1 with
423  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
424    [ Vptr r2 b2 p2 ofs2 ⇒
425        if eq_block b1 b2
426        then Some ? (of_bool (cmp_offset c ofs1 ofs2))
427        else ev_cmp_mismatch c
428    | Vnull r2 ⇒ ev_cmp_mismatch c
429    | _ ⇒ None ? ]
430  | Vnull r1 ⇒ match v2 with
431    [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
432    | Vnull r2 ⇒ ev_cmp_match c
433    | _ ⇒ None ?
434    ]
435  | _ ⇒ None ? ].
436
437(* TODO: check this, it isn't the cmpu used elsewhere *)
438definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
439  match v1 with
440  [ Vint n1 ⇒ match v2 with
441    [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
442    | _ ⇒ None ? ]
443  | _ ⇒ None ? ].
444
445definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
446  match v1 with
447  [ Vfloat f1 ⇒ match v2 with
448    [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
449    | _ ⇒ None ? ]
450  | _ ⇒ None ? ].
451
452definition eval_binop : binary_operation → val → val → option val ≝
453λop.
454  match op with
455  [ Oadd ⇒ ev_add
456  | Osub ⇒ ev_sub
457  | Omul ⇒ ev_mul
458  | Odiv ⇒ ev_divs
459  | Odivu ⇒ ev_divu
460  | Omod ⇒ ev_mods
461  | Omodu ⇒ ev_modu
462  | Oand ⇒ ev_and
463  | Oor ⇒ ev_or
464  | Oxor ⇒ ev_xor
465  | Oshl ⇒ ev_shl
466  | Oshr ⇒ ev_shr
467  | Oshru ⇒ ev_shru
468  | Oaddf ⇒ ev_addf
469  | Osubf ⇒ ev_subf
470  | Omulf ⇒ ev_mulf
471  | Odivf ⇒ ev_divf
472  | Ocmp c ⇒ ev_cmp c
473  | Ocmpu c ⇒ ev_cmpu c
474  | Ocmpf c ⇒ ev_cmpf c
475  | Oaddp ⇒ ev_addp
476  | Osubpi ⇒ ev_subpi
477  | Osubpp ⇒ ev_subpp
478  | Ocmpp c ⇒ ev_cmpp c
479  ].
480
Note: See TracBrowser for help on using the repository browser.