source: src/common/FrontEndOps.ma @ 955

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