blob: d4439efaca6031f893e94141172822ebe08b4cf2 (
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
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Op.
(** ** Machine registers *)
(** The following type defines the machine registers that can be referenced
as locations. These include:
- Integer registers that can be allocated to RTL pseudo-registers ([Rxx]).
- Floating-point registers that can be allocated to RTL pseudo-registers
([Fxx]).
The type [mreg] does not include reserved machine registers
such as the stack pointer, the link register, and the condition codes. *)
Inductive mreg: Type :=
(** Allocatable integer regs *)
| R0: mreg | R1: mreg | R2: mreg | R3: mreg
| R4: mreg | R5: mreg | R6: mreg | R7: mreg
| R8: mreg | R9: mreg | R10: mreg | R11: mreg
| R12: mreg
(** Allocatable double-precision float regs *)
| F0: mreg | F1: mreg | F2: mreg | F3: mreg
| F4: mreg | F5: mreg | F6: mreg | F7: mreg
| F8: mreg | F9: mreg | F10: mreg | F11: mreg
| F12: mreg | F13: mreg | F14: mreg | F15: mreg.
Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
Proof. decide equality. Defined.
Global Opaque mreg_eq.
Definition mreg_type (r: mreg): typ :=
match r with
| R0 => Tint | R1 => Tint | R2 => Tint | R3 => Tint
| R4 => Tint | R5 => Tint | R6 => Tint | R7 => Tint
| R8 => Tint | R9 => Tint | R10 => Tint | R11 => Tint
| R12 => Tint
| F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat
| F4 => Tfloat| F5 => Tfloat | F6 => Tfloat | F7 => Tfloat
| F8 => Tfloat | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat
| F12 => Tfloat | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat
end.
Open Scope positive_scope.
Module IndexedMreg <: INDEXED_TYPE.
Definition t := mreg.
Definition eq := mreg_eq.
Definition index (r: mreg): positive :=
match r with
| R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4
| R4 => 5 | R5 => 6 | R6 => 7 | R7 => 8
| R8 => 9 | R9 => 10 | R10 => 11 | R11 => 12
| R12 => 13
| F0 => 14 | F1 => 15 | F2 => 16 | F3 => 17
| F4 => 18 | F5 => 19 | F6 => 20 | F7 => 21
| F8 => 22 | F9 => 23 | F10 => 24 | F11 => 25
| F12 => 26 | F13 => 27 | F14 => 28 | F15 => 29
end.
Lemma index_inj:
forall r1 r2, index r1 = index r2 -> r1 = r2.
Proof.
destruct r1; destruct r2; simpl; intro; discriminate || reflexivity.
Qed.
End IndexedMreg.
(** ** Destroyed registers, preferred registers *)
Definition destroyed_by_op (op: operation): list mreg :=
match op with
| Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil
| Ointoffloat | Ointuoffloat => F6 :: nil
| _ => nil
end.
Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg :=
nil.
Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
match chunk with
| Mfloat32 => F6 :: nil
| _ => nil
end.
Definition destroyed_by_cond (cond: condition): list mreg :=
nil.
Definition destroyed_by_jumptable: list mreg :=
nil.
Definition destroyed_by_builtin (ef: external_function): list mreg :=
match ef with
| EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil
| EF_vstore Mfloat32 => F6 :: nil
| EF_vstore_global Mfloat32 _ _ => F6 :: nil
| _ => nil
end.
Definition destroyed_by_setstack (ty: typ): list mreg :=
match ty with
| Tsingle => F6 :: nil
| _ => nil
end.
Definition destroyed_at_function_entry: list mreg :=
R12 :: nil.
Definition temp_for_parent_frame: mreg :=
R12.
Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
match op with
| Odiv | Odivu => (Some R0 :: Some R1 :: nil, Some R0)
| _ => (nil, None)
end.
Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) :=
match ef with
| EF_memcpy sz al =>
if zle sz 32 then (nil, nil) else (Some R3 :: Some R2 :: nil, nil)
| _ => (nil, nil)
end.
Global Opaque
destroyed_by_op destroyed_by_load destroyed_by_store
destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
mregs_for_operation mregs_for_builtin.
(** Two-address operations. Return [true] if the first argument and
the result must be in the same location *and* are unconstrained
by [mregs_for_operation]. There are none for ARM. *)
Definition two_address_op (op: operation) : bool :=
false.
Global Opaque two_address_op.
|
