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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Coqlib.
Require Import Asmblock.
Require Import Values.
Require Import Integers.
Require Import AST.
Require Compopts.
Definition is_valid_immofs_32 (z: Z) : bool :=
if (zle z 252) && (zle (-256) z) && ((Z.modulo z 4) =? 0) then true else false.
Definition is_valid_immofs_64 (z: Z) : bool :=
if (zle z 504) && (zle (-512) z) && ((Z.modulo z 8) =? 0) then true else false.
Definition is_valid_ldrw (rd1 rd2: ireg) (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1))
&& (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then true else false.
Definition is_valid_ldrx (rd1 rd2: ireg) (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1))
&& (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then true else false.
Definition is_valid_strw (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1)
then true else false.
Definition is_valid_strx (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1)
then true else false.
(* Try to find arguments of the next compatible ldrw to replace. *)
Fixpoint get_next_comp_ldpw_args (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (ireg * iregsp * int64) :=
match t1 with
| nil => None
| (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 =>
if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then Some (rd2, b2, n2)
else None
| _ :: t2 => get_next_comp_ldpw_args rd1 b1 n1 t2
end.
(* Try to delete the next compatible ldrw to replace. *)
Fixpoint del_next_comp_ldpw_args (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : list basic :=
match t1 with
| nil => nil
| (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 =>
if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then t2
else t1
| h2 :: t2 => h2 :: del_next_comp_ldpw_args rd1 b1 n1 t2
end.
Fixpoint ldpw_follow (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (basic * list basic) :=
match (get_next_comp_ldpw_args rd1 b1 n1 t1) with
| None => None
| Some (rd2, b2, n2) =>
match t1 with
| nil => None
| h2 :: t2 =>
match h2 with
| (PStore _) => None
| (PLd_rd_a Pldrw (IR (RR1 rd')) (ADimm b' n')) =>
if (ireg_eq rd' rd2) && (iregsp_eq b' b2) && (Int64.eq n' n2) then
Some ((PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))),
(del_next_comp_ldpw_args rd1 b1 n1 t1))
else ldpw_follow rd1 b1 n1 t2
| _ => ldpw_follow rd1 b1 n1 t2
end
end
end.
Fixpoint pair_rep (insns : list basic) : list basic :=
match insns with
| nil => nil
| h0 :: t0 =>
match t0 with
| h1 :: t1 =>
match h0, h1 with
(* ########################## LDP *)
| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)),
(PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) =>
(* When both load the same dest, and with no reuse of ld1 in ld2. *)
if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
Pnop :: (pair_rep t0)
(* When two consec mem addr are loading two different dest. *)
else if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then
(PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (pair_rep t0)
| (PLd_rd_a Pldrx (IR (RR1 rd1)) (ADimm b1 n1)),
(PLd_rd_a Pldrx (IR (RR1 rd2)) (ADimm b2 n2)) =>
if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
Pnop :: (pair_rep t0)
else if (is_valid_ldrx rd1 rd2 b1 b2 n1 n2) then
(PLoad (Pldp Pldpx rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
else
h0 :: (pair_rep t0)
(* When there are some insts between loads/stores *)
(*| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)), h1 =>*)
(*match ldpw_follow rd1 b1 n1 t1 with*)
(*| None => h0 :: (pair_rep t0)*)
(*| Some (ldpw, l) => ldpw :: Pnop :: (pair_rep l)*)
(*end*)
(*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
(* ########################## STP *)
| (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) =>
(* When both store at the same addr, same ofs. *)
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (pair_rep t0)
(* When two consec mem addr are targeted by two store. *)
else*)
if (is_valid_strw b1 b2 n1 n2) then
(PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (pair_rep t0)
| (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) =>
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (pair_rep t0)
else*)
if (is_valid_strx b1 b2 n1 n2) then
(PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
else
h0 :: (pair_rep t0)
| _, _ => h0 :: (pair_rep t0)
end
| nil => h0 :: nil
end
end.
Definition optimize_body (insns : list basic) :=
if Compopts.optim_coalesce_mem tt
then (pair_rep insns)
else insns.
Program Definition optimize_bblock (bb : bblock) :=
let optimized := optimize_body (body bb) in
let wf_ok := non_empty_bblockb optimized (exit bb) in
{| header := header bb;
body := if wf_ok then optimized else (body bb);
exit := exit bb |}.
Next Obligation.
destruct (non_empty_bblockb (optimize_body (body bb))) eqn:Rwf.
- rewrite Rwf. cbn. trivial.
- exact (correct bb).
Qed.
|
