source: src/common/FrontEndOps.ma @ 753

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

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File size: 15.1 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 
173definition ev_notbool : val → option val ≝ λv.
174  match v with
175  [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
176  | Vptr _ b _ ofs ⇒ Some ? Vfalse
177  | Vnull _ ⇒ Some ? Vtrue
178  | _ ⇒ None ?
179  ].
180
181definition ev_zero_ext ≝ λnbits: nat. λv: val.
182  match v with
183  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
184  | _ ⇒ None ?
185  ].
186
187definition ev_sign_ext ≝ λnbits:nat. λv:val.
188  match v with
189  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
190  | _ ⇒ None ?
191  ].
192
193definition ev_singleoffloat : val → option val ≝ λv.
194  match v with
195  [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
196  | _ ⇒ None ?
197  ].
198
199(* TODO: add zero to null? *)
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    | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1))
205    | _ ⇒ None ? ]
206  | Vptr r b1 p ofs1 ⇒ match v2 with
207    [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
208    | _ ⇒ None ? ]
209  | _ ⇒ None ? ].
210
211definition ev_sub ≝ λv1,v2: val.
212  match v1 with
213  [ Vint n1 ⇒ match v2 with
214    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
215    | _ ⇒ None ? ]
216  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
217    [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
218    | Vptr r2 b2 p2 ofs2 ⇒
219        if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
220    | _ ⇒ None ? ]
221  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
222  | _ ⇒ None ? ].
223
224definition ev_mul ≝ λv1, v2: val.
225  match v1 with
226  [ Vint n1 ⇒ match v2 with
227    [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
228    | _ ⇒ None ? ]
229  | _ ⇒ None ? ].
230
231definition ev_divs ≝ λv1, v2: val.
232  match v1 with
233  [ Vint n1 ⇒ match v2 with
234    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
235    | _ ⇒ None ? ]
236  | _ ⇒ None ? ].
237
238definition ev_mods ≝ λv1, v2: val.
239  match v1 with
240  [ Vint n1 ⇒ match v2 with
241    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
242    | _ ⇒ None ?
243    ]
244  | _ ⇒ None ?
245  ].
246
247definition ev_divu ≝ λv1, v2: val.
248  match v1 with
249  [ Vint n1 ⇒ match v2 with
250    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
251    | _ ⇒ None ?
252    ]
253  | _ ⇒ None ?
254  ].
255
256definition ev_modu ≝ λv1, v2: val.
257  match v1 with
258  [ Vint n1 ⇒ match v2 with
259    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
260    | _ ⇒ None ?
261    ]
262  | _ ⇒ None ?
263  ].
264
265definition ev_and ≝ λv1, v2: val.
266  match v1 with
267  [ Vint n1 ⇒ match v2 with
268    [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
269    | _ ⇒ None ? ]
270  | _ ⇒ None ? ].
271
272definition ev_or ≝ λv1, v2: val.
273  match v1 with
274  [ Vint n1 ⇒ match v2 with
275    [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
276    | _ ⇒ None ? ]
277  | _ ⇒ None ? ].
278
279definition ev_xor ≝ λv1, v2: val.
280  match v1 with
281  [ Vint n1 ⇒ match v2 with
282    [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
283    | _ ⇒ None ? ]
284  | _ ⇒ None ? ].
285
286definition ev_shl ≝ λv1, v2: val.
287  match v1 with
288  [ Vint n1 ⇒ match v2 with
289    [ Vint n2 ⇒
290       if ltu n2 iwordsize
291       then Some ? (Vint (shl n1 n2))
292       else None ?
293    | _ ⇒ None ? ]
294  | _ ⇒ None ? ].
295
296definition ev_shr ≝ λv1, v2: val.
297  match v1 with
298  [ Vint n1 ⇒ match v2 with
299    [ Vint n2 ⇒
300       if ltu n2 iwordsize
301       then Some ? (Vint (shr n1 n2))
302       else None ?
303    | _ ⇒ None ? ]
304  | _ ⇒ None ? ].
305
306definition ev_shr_carry ≝ λv1, v2: val.
307  match v1 with
308  [ Vint n1 ⇒ match v2 with
309    [ Vint n2 ⇒
310       if ltu n2 iwordsize
311       then Some ? (Vint (shr_carry n1 n2))
312       else None ?
313    | _ ⇒ None ? ]
314  | _ ⇒ None ? ].
315
316definition ev_shrx ≝ λv1, v2: val.
317  match v1 with
318  [ Vint n1 ⇒ match v2 with
319    [ Vint n2 ⇒
320       if ltu n2 iwordsize
321       then Some ? (Vint (shrx n1 n2))
322       else None ?
323    | _ ⇒ None ? ]
324  | _ ⇒ None ? ].
325
326definition ev_shru ≝ λv1, v2: val.
327  match v1 with
328  [ Vint n1 ⇒ match v2 with
329    [ Vint n2 ⇒
330       if ltu n2 iwordsize
331       then Some ? (Vint (shru n1 n2))
332       else None ?
333    | _ ⇒ None ? ]
334  | _ ⇒ None ? ].
335
336definition ev_rolm ≝
337λv: val. λamount, mask: int.
338  match v with
339  [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
340  | _ ⇒ None ?
341  ].
342
343definition ev_ror ≝ λv1, v2: val.
344  match v1 with
345  [ Vint n1 ⇒ match v2 with
346    [ Vint n2 ⇒
347       if ltu n2 iwordsize
348       then Some ? (Vint (ror n1 n2))
349       else None ?
350    | _ ⇒ None ? ]
351  | _ ⇒ None ? ].
352
353definition ev_addf ≝ λv1,v2: val.
354  match v1 with
355  [ Vfloat f1 ⇒ match v2 with
356    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
357    | _ ⇒ None ? ]
358  | _ ⇒ None ? ].
359
360definition ev_subf ≝ λv1,v2: val.
361  match v1 with
362  [ Vfloat f1 ⇒ match v2 with
363    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
364    | _ ⇒ None ? ]
365  | _ ⇒ None ? ].
366
367definition ev_mulf ≝ λv1,v2: val.
368  match v1 with
369  [ Vfloat f1 ⇒ match v2 with
370    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
371    | _ ⇒ None ? ]
372  | _ ⇒ None ? ].
373
374definition ev_divf ≝ λv1,v2: val.
375  match v1 with
376  [ Vfloat f1 ⇒ match v2 with
377    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
378    | _ ⇒ None ? ]
379  | _ ⇒ None ? ].
380
381definition ev_cmp_match : comparison → option val ≝ λc.
382  match c with
383  [ Ceq ⇒ Some ? Vtrue
384  | Cne ⇒ Some ? Vfalse
385  | _   ⇒ None ?
386  ].
387
388definition ev_cmp_mismatch : comparison → option val ≝ λc.
389  match c with
390  [ Ceq ⇒ Some ? Vfalse
391  | Cne ⇒ Some ? Vtrue
392  | _   ⇒ None ?
393  ].
394
395definition ev_cmp ≝ λc: comparison. λv1,v2: val.
396  match v1 with
397  [ Vint n1 ⇒ match v2 with
398    [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
399    | _ ⇒ None ? ]
400  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
401    [ Vptr r2 b2 p2 ofs2 ⇒
402        if eq_block b1 b2
403        then Some ? (of_bool (cmp_offset c ofs1 ofs2))
404        else ev_cmp_mismatch c
405    | Vnull r2 ⇒ ev_cmp_mismatch c
406    | _ ⇒ None ? ]
407  | Vnull r1 ⇒ match v2 with
408    [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
409    | Vnull r2 ⇒ ev_cmp_match c
410    | _ ⇒ None ?
411    ]
412  | _ ⇒ None ? ].
413
414(* TODO: check this, it isn't the cmpu used elsewhere *)
415definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
416  match v1 with
417  [ Vint n1 ⇒ match v2 with
418    [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
419    | _ ⇒ None ? ]
420  | _ ⇒ None ? ].
421
422definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
423  match v1 with
424  [ Vfloat f1 ⇒ match v2 with
425    [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
426    | _ ⇒ None ? ]
427  | _ ⇒ None ? ].
428
429definition eval_binop : binary_operation → val → val → option val ≝
430λop.
431  match op with
432  [ Oadd ⇒ ev_add
433  | Osub ⇒ ev_sub
434  | Omul ⇒ ev_mul
435  | Odiv ⇒ ev_divs
436  | Odivu ⇒ ev_divu
437  | Omod ⇒ ev_mods
438  | Omodu ⇒ ev_modu
439  | Oand ⇒ ev_and
440  | Oor ⇒ ev_or
441  | Oxor ⇒ ev_xor
442  | Oshl ⇒ ev_shl
443  | Oshr ⇒ ev_shr
444  | Oshru ⇒ ev_shru
445  | Oaddf ⇒ ev_addf
446  | Osubf ⇒ ev_subf
447  | Omulf ⇒ ev_mulf
448  | Odivf ⇒ ev_divf
449  | Ocmp c ⇒ ev_cmp c
450  | Ocmpu c ⇒ ev_cmpu c
451  | Ocmpf c ⇒ ev_cmpf c
452  (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)
453  | Oaddp ⇒ ev_add
454  | Osubp ⇒ ev_sub
455  | Ocmpp c ⇒ ev_cmp c
456  ].
457
Note: See TracBrowser for help on using the repository browser.