source: src/common/FrontEndOps.ma @ 702

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

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File size: 14.3 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
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.