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
|
(* *************************************************************)
(* *)
(* 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.
Fixpoint ldp_rep (insns : list basic) : list basic :=
match insns with
| nil => nil
| h0 :: t0 =>
match t0 with
| h1 :: t1 =>
match h0, h1 with
| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)),
(PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) =>
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
(* TODO This could be insteresting to add if compatible with the checker
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 :: (ldp_rep t0)
(* When two consec mem addr are loading two different dest. *)
else*)
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
(PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))) :: Pnop :: (ldp_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (ldp_rep t0)
| (PLd_rd_a Pldrx (IR (RR1 rd1)) (ADimm b1 n1)),
(PLd_rd_a Pldrx (IR (RR1 rd2)) (ADimm b2 n2)) =>
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
(*if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
Pnop :: (ldp_rep t0)
else*)
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
(PLoad (Pldp Pldpx rd1 rd2 (ADimm b1 n1))) :: Pnop :: (ldp_rep t1)
else
h0 :: (ldp_rep t0)
(*| (PLd_rd_a Pldrw rd1 (ADimm b1 n1)), h1 => ldpw_follow rd1 b1 n1*)
(*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
| _, _ => h0 :: (ldp_rep t0)
end
| nil => h0 :: nil
end
end.
Fixpoint stp_rep (insns : list basic) : list basic :=
match insns with
| nil => nil
| h0 :: t0 =>
match t0 with
| h1 :: t1 =>
match h0, h1 with
| (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) =>
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
(* When both store at the same addr, same ofs. *)
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (stp_rep t0)
(* When two consec mem addr are targeted by two store. *)
else*)
if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then
(PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (stp_rep t0)
| (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) =>
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (stp_rep t0)
else*)
if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then
(PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1)
else
h0 :: (stp_rep t0)
(*| (PLd_rd_a Pldrw rd1 (ADimm b1 n1)), h1 => ldpw_follow rd1 b1 n1*)
(*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
| _, _ => h0 :: (stp_rep t0)
end
| nil => h0 :: nil
end
end.
Definition optimize_body (insns : list basic) :=
(* TODO ADD A FLAG TO ENABLE PEEPHOLE *)
if Compopts.optim_coalesce_mem tt
then stp_rep (ldp_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.
|
