source: Deliverables/D3.1/C-semantics/FrontEndOps.ma @ 639

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

Preliminary work on RTLabs semantics
Will move to somewhere more appropriate soon.

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