summaryrefslogtreecommitdiff
path: root/arm/SelectOp.vp
blob: 255c97c102dac9c894d22da60cc916e6d73ba0b0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Instruction selection for operators *)

(** The instruction selection pass recognizes opportunities for using
  combined arithmetic and logical operations and addressing modes
  offered by the target processor.  For instance, the expression [x + 1]
  can take advantage of the "immediate add" instruction of the processor,
  and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
  into a "rotate and mask" instruction.

  This file defines functions for building CminorSel expressions and
  statements, especially expressions consisting of operator
  applications.  These functions examine their arguments to choose
  cheaper forms of operators whenever possible.

  For instance, [add e1 e2] will return a CminorSel expression semantically
  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
  [Oaddimm] operator if one of the arguments is an integer constant,
  or suppress the addition altogether if one of the arguments is the
  null integer.  In passing, we perform operator reassociation
  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
  of constant propagation.

  On top of the "smart constructor" functions defined below,
  module [Selection] implements the actual instruction selection pass.
*)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Cminor.
Require Import Op.
Require Import CminorSel.

Open Local Scope cminorsel_scope.

(** ** Constants **)

Definition addrsymbol (id: ident) (ofs: int) :=
  Eop (Oaddrsymbol id ofs) Enil.

Definition addrstack (ofs: int) :=
  Eop (Oaddrstack ofs) Enil.

(** ** Integer logical negation *)

Nondetfunction notint (e: expr) :=
  match e with
  | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil)
  | Eop Onot (t1:::Enil) => t1
  | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil)
  | _ => Eop Onot (e:::Enil)
  end.

(** ** Integer addition and pointer addition *)

Nondetfunction addimm (n: int) (e: expr) :=
  if Int.eq n Int.zero then e else
  match e with
  | Eop (Ointconst m) Enil       => Eop (Ointconst(Int.add n m)) Enil
  | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Int.add n m)) Enil
  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Int.add n m)) Enil
  | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
  | _                            => Eop (Oaddimm n) (e ::: Enil)
  end.

Nondetfunction add (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
  | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
  | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
  | _, _ => Eop Oadd (e1:::e2:::Enil)
  end.

(** ** Integer and pointer subtraction *)

Nondetfunction sub (e1: expr) (e2: expr) :=
  match e1, e2 with
  | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil)
  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil)
  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil)
  | _, _ => Eop Osub (e1:::e2:::Enil)
  end.

Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil).

(** ** Immediate shifts *)

Nondetfunction shlimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) Enil
    | Eop (Oshift (Slsl n1)) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int.iwordsize
        then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil)
        else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
    | _ => Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
    end.

Nondetfunction shruimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) Enil
    | Eop (Oshift (Slsr n1)) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int.iwordsize
        then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
        else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
    | _ => Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
    end.

Nondetfunction shrimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else
    match e1 with
    | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) Enil
    | Eop (Oshift (Sasr n1)) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int.iwordsize
        then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
        else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
    | _ => Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
    end.

(** ** Integer multiply *)

Definition mulimm_base (n1: int) (e2: expr) :=
  match Int.one_bits n1 with
  | i :: nil =>
      shlimm e2 i
  | i :: j :: nil =>
      Elet e2
        (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
  | _ =>
      Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil)
  end.

Nondetfunction mulimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
  else if Int.eq n1 Int.one then e2
  else match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil
  | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2)
  | _ => mulimm_base n1 e2
  end.

Nondetfunction mul (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2
  | t1, Eop (Ointconst n2) Enil => mulimm n2 t1
  | _, _ => Eop Omul (e1:::e2:::Enil)
  end.

(** ** Bitwise and, or, xor *)

Nondetfunction andimm (n1: int) (e2: expr) := 
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
  match e2 with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.and n1 n2)) Enil
  | Eop (Oandimm n2) (t2:::Enil) =>
      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | _ =>
      Eop (Oandimm n1) (e2:::Enil)
  end.

Nondetfunction and (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
  | t1, Eop (Ointconst n2) Enil => andimm n2 t1
  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil)
  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil)
  | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil)
  | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil)
  | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil)
  | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil)
  | _, _ => Eop Oand (e1:::e2:::Enil)
  end.

Definition same_expr_pure (e1 e2: expr) :=
  match e1, e2 with
  | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false
  | _, _ => false
  end.

Nondetfunction orimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then e2 else
  match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
  | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
  | _ => Eop (Oorimm n1) (e2:::Enil)
  end.

Nondetfunction or (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => orimm n1 t2
  | t1, Eop (Ointconst n2) Enil => orimm n2 t1
  | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) =>
      if Int.eq (Int.add n1 n2) Int.iwordsize
      && same_expr_pure t1 t2
      then Eop (Oshift (Sror n2)) (t1:::Enil)
      else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
  | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) =>
      if Int.eq (Int.add n2 n1) Int.iwordsize
      && same_expr_pure t1 t2
      then Eop (Oshift (Sror n1)) (t1:::Enil)
      else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil)
  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil)
  | _, _ => Eop Oor (e1:::e2:::Enil)
  end.

Nondetfunction xorimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then e2 else
  match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
  | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
  | _ => Eop (Oxorimm n1) (e2:::Enil)
  end.

Nondetfunction xor (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2
  | t1, Eop (Ointconst n2) Enil => xorimm n2 t1
  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil)
  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil)
  | _, _ => Eop Oxor (e1:::e2:::Enil)
  end.

(** ** Integer division and modulus *)

Definition mod_aux (divop: operation) (e1 e2: expr) :=
  Elet e1
    (Elet (lift e2)
      (Eop Osub (Eletvar 1 :::
                 Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
                           Eletvar 0 :::
                           Enil) :::
                 Enil))).

Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).

Definition mods := mod_aux Odiv.

Definition divuimm (e: expr) (n: int) :=
  match Int.is_power2 n with
  | Some l => shruimm e l
  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
  end.

Nondetfunction divu (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => divuimm e1 n2
  | _ => Eop Odivu (e1:::e2:::Enil)
  end.

Definition moduimm (e: expr) (n: int) :=
  match Int.is_power2 n with
  | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil)
  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
  end.

Nondetfunction modu (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => moduimm e1 n2
  | _ => mod_aux Odivu e1 e2
  end.

(** ** General shifts *)

Nondetfunction shl (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shlimm e1 n2
  | _ => Eop Oshl (e1:::e2:::Enil)
  end.

Nondetfunction shr (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shrimm e1 n2
  | _ => Eop Oshr (e1:::e2:::Enil)
  end.

Nondetfunction shru (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shruimm e1 n2
  | _ => Eop Oshru (e1:::e2:::Enil)
  end.

(** ** Floating-point arithmetic *)

Definition negf (e: expr) :=  Eop Onegf (e ::: Enil).
Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).

(** ** Comparisons *)

Nondetfunction compimm (default: comparison -> int -> condition)
                       (sem: comparison -> int -> int -> bool)
                       (c: comparison) (e1: expr) (n2: int) :=
  match c, e1 with
  | c, Eop (Ointconst n1) Enil =>
      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
  | Ceq, Eop (Ocmp c) el =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (negate_condition c)) el
      else if Int.eq_dec n2 Int.one then
        Eop (Ocmp c) el
      else 
        Eop (Ointconst Int.zero) Enil
  | Cne, Eop (Ocmp c) el =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp c) el
      else if Int.eq_dec n2 Int.one then
        Eop (Ocmp (negate_condition c)) el
      else 
        Eop (Ointconst Int.one) Enil
  | _, _ =>
       Eop (Ocmp (default c n2)) (e1 ::: Enil)
  end.

Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
  | t1, Eop (Ointconst n2) Enil =>
      compimm Ccompimm Int.cmp c t1 n2
  | _, _ =>
      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
  end.

Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
  | t1, Eop (Ointconst n2) Enil =>
      compimm Ccompuimm Int.cmpu c t1 n2
  | _, _ =>
      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
  end.

Definition compf (c: comparison) (e1: expr) (e2: expr) :=
  Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).

(** ** Integer conversions *)

Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.

Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24).

Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.

Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16).

(** ** Floating-point conversions *)

Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).

(** ** Recognition of addressing modes for load and store operations *)

(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes
    for floating-point accesses, since these are not supported
    by the hardware and emulated inefficiently in [Asmgen].
    Likewise, [Aindexed2shift] are not supported for halfword
    and signed byte accesses. *)

Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
  match chunk with
  | Mint8signed => true
  | Mint8unsigned => true
  | Mint16signed => true
  | Mint16unsigned => true
  | Mint32 => true
  | Mfloat32 => false
  | Mfloat64 => false
  | Mfloat64al32 => false
  end.

Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
  match chunk with
  | Mint8signed => false
  | Mint8unsigned => true
  | Mint16signed => false
  | Mint16unsigned => false
  | Mint32 => true
  | Mfloat32 => false
  | Mfloat64 => false
  | Mfloat64al32 => false
  end.

Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
  match e with
  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
  | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
  | Eop (Oaddshift s) (e1:::e2:::Enil) =>
      if can_use_Aindexed2shift chunk
      then (Aindexed2shift s, e1:::e2:::Enil)
      else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
  | Eop Oadd (e1:::e2:::Enil) =>
      if can_use_Aindexed2 chunk
      then (Aindexed2, e1:::e2:::Enil)
      else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
  | _ => (Aindexed Int.zero, e:::Enil)
  end.