blob: 81f0dc82f06655341c35043884f6b5e95b719c65 (
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
|
Require Import Coqlib.
Require Import Asmvliw.
Require Import Values.
Require Import Integers.
Require Compopts.
Definition gpreg_q_list : list gpreg_q :=
R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9
:: R10R11 :: R12R13 :: R14R15 :: R16R17 :: R18R19
:: R20R21 :: R22R23 :: R24R25 :: R26R27 :: R28R29
:: R30R31 :: R32R33 :: R34R35 :: R36R37 :: R38R39
:: R40R41 :: R42R43 :: R44R45 :: R46R47 :: R48R49
:: R50R51 :: R52R53 :: R54R55 :: R56R57 :: R58R59
:: R60R61 :: R62R63 :: nil.
Definition gpreg_o_list : list gpreg_o :=
R0R1R2R3 :: R4R5R6R7 :: R8R9R10R11 :: R12R13R14R15
:: R16R17R18R19 :: R20R21R22R23 :: R24R25R26R27 :: R28R29R30R31
:: R32R33R34R35 :: R36R37R38R39 :: R40R41R42R43 :: R44R45R46R47
:: R48R49R50R51 :: R52R53R54R55 :: R56R57R58R59 :: R60R61R62R63 :: nil.
Fixpoint gpreg_q_search_rec r0 r1 l :=
match l with
| h :: t =>
let (s0, s1) := gpreg_q_expand h in
if (gpreg_eq r0 s0) && (gpreg_eq r1 s1)
then Some h
else gpreg_q_search_rec r0 r1 t
| nil => None
end.
Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l :=
match l with
| h :: t =>
match gpreg_o_expand h with
| (((s0, s1), s2), s3) =>
if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) &&
(gpreg_eq r2 s2) && (gpreg_eq r3 s3)
then Some h
else gpreg_o_search_rec r0 r1 r2 r3 t
end
| nil => None
end.
Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q :=
gpreg_q_search_rec r0 r1 gpreg_q_list.
Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o :=
gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list.
Parameter print_found_store: forall A, Z -> A -> A.
Definition coalesce_octuples := true.
Fixpoint coalesce_mem (insns : list basic) : list basic :=
match insns with
| nil => nil
| h0 :: t0 =>
match t0 with
| h1 :: t1 =>
match h0, h1 with
| (PStoreRRO Psd_a rs0 ra0 ofs0),
(PStoreRRO Psd_a rs1 ra1 ofs1) =>
match gpreg_q_search rs0 rs1 with
| Some rs0rs1 =>
let zofs0 := Ptrofs.signed ofs0 in
let zofs1 := Ptrofs.signed ofs1 in
if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1)
then
if coalesce_octuples
then
match t1 with
| (PStoreRRO Psd_a rs2 ra2 ofs2) ::
(PStoreRRO Psd_a rs3 ra3 ofs3) :: t3 =>
match gpreg_o_search rs0 rs1 rs2 rs3 with
| Some octuple =>
let zofs2 := Ptrofs.signed ofs2 in
let zofs3 := Ptrofs.signed ofs3 in
if (zofs2 =? zofs0 + 16) && (ireg_eq ra0 ra2) &&
(zofs3 =? zofs0 + 24) && (ireg_eq ra0 ra3)
then (PStore (PStoreORRO octuple ra0 ofs0)) :: Pnop :: Pnop :: Pnop :: (coalesce_mem t3)
else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
| None => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
end
| _ => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
end
else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
else h0 :: (coalesce_mem t0)
| None => h0 :: (coalesce_mem t0)
end
| (PLoadRRO Pld_a rd0 ra0 ofs0),
(PLoadRRO Pld_a rd1 ra1 ofs1) =>
match gpreg_q_search rd0 rd1 with
| Some rd0rd1 =>
let zofs0 := Ptrofs.signed ofs0 in
let zofs1 := Ptrofs.signed ofs1 in
if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) && negb (ireg_eq ra0 rd0)
then (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1)
else h0 :: (coalesce_mem t0)
| None => h0 :: (coalesce_mem t0)
end
| _, _ => h0 :: (coalesce_mem t0)
end
| nil => h0 :: nil
end
end.
Definition optimize_body (insns : list basic) :=
if Compopts.optim_coalesce_mem tt
then coalesce_mem insns
else insns.
Program Definition optimize_bblock (bb : bblock) :=
let optimized := optimize_body (body bb) in
let wf_ok := wf_bblockb optimized (exit bb) in
{| header := header bb;
body := if wf_ok then optimized else (body bb);
exit := exit bb |}.
Next Obligation.
destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf.
- rewrite Rwf. simpl. trivial.
- exact (correct bb).
Qed.
|