source: src/common/FrontEndOps.ma @ 727

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

Enough fixes to let an RTLabs program run.

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