Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
608fea7e
Commit
608fea7e
authored
Dec 09, 2020
by
Léo Gourdin
Browse files
Non conseq stores
parent
aa66e021
Changes
1
Hide whitespace changes
Inline
Side-by-side
aarch64/PeepholeOracle.ml
View file @
608fea7e
...
...
@@ -33,7 +33,7 @@ let is_valid_ldrw rd1 rd2 b1 b2 n1 n2 =
(
not
(
ireg_eq
rd1
rd2
))
&&
iregsp_eq
b1
b2
&&
(
not
(
iregsp_eq
(
RR1
rd1
)
b2
))
&&
(
(
z2
=
z1
+
4
)
||
(
z2
=
z1
-
4
)
)
&&
(
z2
=
z1
+
4
||
z2
=
z1
-
4
)
&&
is_valid_immofs_32
z1
then
true
else
false
...
...
@@ -45,7 +45,7 @@ let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
(
not
(
ireg_eq
rd1
rd2
))
&&
iregsp_eq
b1
b2
&&
(
not
(
iregsp_eq
(
RR1
rd1
)
b2
))
&&
(
(
z2
=
z1
+
8
)
||
(
z2
=
z1
-
8
)
)
&&
(
z2
=
z1
+
8
||
z2
=
z1
-
8
)
&&
is_valid_immofs_64
z1
then
true
else
false
...
...
@@ -77,6 +77,14 @@ let rec affect_symb_mem reg insta pot_rep stype =
|
PLoad
(
PLd_rd_a
(
Pldrx
,
IR
(
RR1
rd
)
,
ADimm
(
b
,
n
)))
,
"ldrx"
->
if
dreg_eq
reg
(
IR
b
)
then
affect_symb_mem
reg
insta
t0
stype
else
h0
::
affect_symb_mem
reg
insta
t0
stype
|
PStore
(
PSt_rs_a
(
Pstrw
,
IR
(
RR1
rs
)
,
ADimm
(
b
,
n
)))
,
"strw"
->
if
dreg_eq
reg
(
IR
b
)
||
dreg_eq
reg
(
dreg_of_ireg
rs
)
then
affect_symb_mem
reg
insta
t0
stype
else
h0
::
affect_symb_mem
reg
insta
t0
stype
|
PStore
(
PSt_rs_a
(
Pstrx
,
IR
(
RR1
rs
)
,
ADimm
(
b
,
n
)))
,
"strx"
->
if
dreg_eq
reg
(
IR
b
)
||
dreg_eq
reg
(
dreg_of_ireg
rs
)
then
affect_symb_mem
reg
insta
t0
stype
else
h0
::
affect_symb_mem
reg
insta
t0
stype
|
_
,
_
->
failwith
"affect_symb_mem: Found an inconsistent inst in pot_rep"
)
...
...
@@ -93,12 +101,15 @@ let rec read_symb_mem reg insta pot_rep stype =
|
PLoad
(
PLd_rd_a
(
Pldrx
,
IR
(
RR1
rd
)
,
ADimm
(
b
,
n
)))
,
"ldrx"
->
if
dreg_eq
reg
(
IR
(
RR1
rd
))
then
read_symb_mem
reg
insta
t0
stype
else
h0
::
read_symb_mem
reg
insta
t0
stype
|
PStore
(
PSt_rs_a
(
Pstrw
,
IR
(
RR1
rs
)
,
ADimm
(
b
,
n
)))
,
"strw"
->
h0
::
affect_symb_mem
reg
insta
t0
stype
|
PStore
(
PSt_rs_a
(
Pstrx
,
IR
(
RR1
rs
)
,
ADimm
(
b
,
n
)))
,
"strx"
->
h0
::
affect_symb_mem
reg
insta
t0
stype
|
_
,
_
->
failwith
"read_symb_mem: Found an inconsistent inst in pot_rep"
)
let
update_pot_rep_addressing
a
insta
pot_rep
stype
=
match
a
with
|
ADimm
(
base
,
_
)
->
pot_rep
:=
read_symb_mem
(
IR
base
)
insta
!
pot_rep
stype
|
ADimm
(
base
,
_
)
->
pot_rep
:=
read_symb_mem
(
IR
base
)
insta
!
pot_rep
stype
|
ADreg
(
base
,
r
)
->
pot_rep
:=
read_symb_mem
(
IR
base
)
insta
!
pot_rep
stype
;
pot_rep
:=
read_symb_mem
(
dreg_of_ireg
r
)
insta
!
pot_rep
stype
...
...
@@ -175,14 +186,17 @@ let update_pot_rep_basic inst insta pot_rep stype =
pot_rep
:=
read_symb_mem
rs2
insta
!
pot_rep
stype
|
Pfnmul
(
_
,
rd
,
rs1
,
rs2
)
->
()
)
|
PLoad
i
->
(
match
i
with
|
PLd_rd_a
(
_
,
rd
,
a
)
->
pot_rep
:=
affect_symb_mem
rd
insta
!
pot_rep
stype
;
update_pot_rep_addressing
a
insta
pot_rep
stype
|
Pldp
(
_
,
rd1
,
rd2
,
a
)
->
pot_rep
:=
affect_symb_mem
(
dreg_of_ireg
rd1
)
insta
!
pot_rep
stype
;
pot_rep
:=
affect_symb_mem
(
dreg_of_ireg
rd2
)
insta
!
pot_rep
stype
;
update_pot_rep_addressing
a
insta
pot_rep
stype
)
match
stype
with
|
"ldrw"
|
"ldrx"
->
(
match
i
with
|
PLd_rd_a
(
_
,
rd
,
a
)
->
pot_rep
:=
affect_symb_mem
rd
insta
!
pot_rep
stype
;
update_pot_rep_addressing
a
insta
pot_rep
stype
|
Pldp
(
_
,
rd1
,
rd2
,
a
)
->
pot_rep
:=
affect_symb_mem
(
dreg_of_ireg
rd1
)
insta
!
pot_rep
stype
;
pot_rep
:=
affect_symb_mem
(
dreg_of_ireg
rd2
)
insta
!
pot_rep
stype
;
update_pot_rep_addressing
a
insta
pot_rep
stype
)
|
_
->
pot_rep
:=
[]
)
|
PStore
_
->
pot_rep
:=
[]
|
Pallocframe
(
_
,
_
)
->
pot_rep
:=
[]
|
Pfreeframe
(
_
,
_
)
->
pot_rep
:=
[]
...
...
@@ -201,17 +215,23 @@ let update_pot_rep_basic inst insta pot_rep stype =
(* Try to find the index of the first previous compatible
* replacement in a given symbolic memory *)
let
rec
search_compat_rep
r
d
2
b2
n2
insta
pot_rep
stype
=
let
rec
search_compat_rep
r2
b2
n2
insta
pot_rep
stype
=
match
pot_rep
with
|
[]
->
None
|
h0
::
t0
->
(
match
(
insta
.
(
h0
)
,
stype
)
with
|
PLoad
(
PLd_rd_a
(
Pldrw
,
IR
(
RR1
rd1
)
,
ADimm
(
b1
,
n1
)))
,
"ldrw"
->
if
is_valid_ldrw
rd1
r
d
2
b1
b2
n1
n2
then
Some
(
h0
,
rd1
,
b1
,
n1
)
else
search_compat_rep
r
d
2
b2
n2
insta
t0
stype
if
is_valid_ldrw
rd1
r2
b1
b2
n1
n2
then
Some
(
h0
,
rd1
,
b1
,
n1
)
else
search_compat_rep
r2
b2
n2
insta
t0
stype
|
PLoad
(
PLd_rd_a
(
Pldrx
,
IR
(
RR1
rd1
)
,
ADimm
(
b1
,
n1
)))
,
"ldrx"
->
if
is_valid_ldrx
rd1
rd2
b1
b2
n1
n2
then
Some
(
h0
,
rd1
,
b1
,
n1
)
else
search_compat_rep
rd2
b2
n2
insta
t0
stype
if
is_valid_ldrx
rd1
r2
b1
b2
n1
n2
then
Some
(
h0
,
rd1
,
b1
,
n1
)
else
search_compat_rep
r2
b2
n2
insta
t0
stype
|
PStore
(
PSt_rs_a
(
Pstrw
,
IR
(
RR1
rs1
)
,
ADimm
(
b1
,
n1
)))
,
"strw"
->
if
is_valid_strw
b1
b2
n1
n2
then
Some
(
h0
,
rs1
,
b1
,
n1
)
else
search_compat_rep
r2
b2
n2
insta
t0
stype
|
PStore
(
PSt_rs_a
(
Pstrx
,
IR
(
RR1
rs1
)
,
ADimm
(
b1
,
n1
)))
,
"strx"
->
if
is_valid_strx
b1
b2
n1
n2
then
Some
(
h0
,
rs1
,
b1
,
n1
)
else
search_compat_rep
r2
b2
n2
insta
t0
stype
|
_
,
_
->
failwith
"search_compat_rep: Found an inconsistent inst in pot_rep"
)
...
...
@@ -229,9 +249,16 @@ let pair_rep insta =
* are the indices of insts in the main array "insta". *)
let
pot_ldrw_rep
=
ref
[]
in
let
pot_ldrx_rep
=
ref
[]
in
let
pot_strw_rep
=
ref
[]
in
let
pot_strx_rep
=
ref
[]
in
for
i
=
0
to
Array
.
length
insta
-
2
do
let
h0
=
insta
.
(
i
)
in
let
h1
=
insta
.
(
i
+
1
)
in
(* Here we need to update every symbolic memory according to the matched inst *)
update_pot_rep_basic
h0
insta
pot_ldrw_rep
"ldrw"
;
update_pot_rep_basic
h0
insta
pot_ldrx_rep
"ldrx"
;
update_pot_rep_basic
h0
insta
pot_strw_rep
"strw"
;
update_pot_rep_basic
h0
insta
pot_strx_rep
"strx"
;
match
(
h0
,
h1
)
with
(* Consecutive ldrw *)
|
(
PLoad
(
PLd_rd_a
(
Pldrw
,
IR
(
RR1
rd1
)
,
ADimm
(
b1
,
n1
)))
,
...
...
@@ -242,10 +269,11 @@ let pair_rep insta =
insta
.
(
i
)
<-
Pnop
(* When two consec mem addr are loading two different dest. *)
)
else
if
is_valid_ldrw
rd1
rd2
b1
b2
n1
n2
then
(
if
debug
then
eprintf
"LDP_WPEEP
\n
"
;
(
if
min_is_rev
n1
n2
then
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpw
,
rd1
,
rd2
,
ADimm
(
b1
,
n1
)))
else
if
min_is_rev
n1
n2
then
(
if
debug
then
eprintf
"LDP_W_CONSEC_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpw
,
rd1
,
rd2
,
ADimm
(
b1
,
n1
))))
else
(
if
debug
then
eprintf
"LDP_W_CONSEC_PEEP_BACKWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpw
,
rd2
,
rd1
,
ADimm
(
b1
,
n2
))));
insta
.
(
i
+
1
)
<-
Pnop
)
(* Consecutive ldrx *)
...
...
@@ -255,10 +283,11 @@ let pair_rep insta =
if
debug
then
eprintf
"LDP_XOPT
\n
"
;
insta
.
(
i
)
<-
Pnop
)
else
if
is_valid_ldrx
rd1
rd2
b1
b2
n1
n2
then
(
if
debug
then
eprintf
"LDP_XPEEP
\n
"
;
(
if
min_is_rev
n1
n2
then
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpx
,
rd1
,
rd2
,
ADimm
(
b1
,
n1
)))
else
if
min_is_rev
n1
n2
then
(
if
debug
then
eprintf
"LDP_X_CONSEC_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpx
,
rd1
,
rd2
,
ADimm
(
b1
,
n1
))))
else
(
if
debug
then
eprintf
"LDP_X_CONSEC_PEEP_BACKWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpx
,
rd2
,
rd1
,
ADimm
(
b1
,
n2
))));
insta
.
(
i
+
1
)
<-
Pnop
)
(* Non-consecutive ldrw *)
...
...
@@ -269,27 +298,29 @@ let pair_rep insta =
|
None
->
pot_ldrw_rep
:=
i
::
!
pot_ldrw_rep
(* Else, perform the peephole *)
|
Some
(
rep
,
r
,
b
,
n
)
->
eprintf
"LDP_WCPEEP
\n
"
;
(* The two lines below are used to filter the elected candidate *)
let
filt
x
=
x
!=
rep
in
pot_ldrw_rep
:=
List
.
filter
filt
!
pot_ldrw_rep
;
insta
.
(
rep
)
<-
Pnop
;
(
if
min_is_rev
n
n1
then
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpw
,
r
,
rd1
,
ADimm
(
b
,
n
)))
else
if
min_is_rev
n
n1
then
(
if
debug
then
eprintf
"LDP_W_SPACED_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpw
,
r
,
rd1
,
ADimm
(
b
,
n
))))
else
(
if
debug
then
eprintf
"LDP_W_SPACED_PEEP_BACKWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpw
,
rd1
,
r
,
ADimm
(
b
,
n1
)))))
(* Non-consecutive ldrx *)
|
PLoad
(
PLd_rd_a
(
Pldrx
,
IR
(
RR1
rd1
)
,
ADimm
(
b1
,
n1
)))
,
_
->
(
match
search_compat_rep
rd1
b1
n1
insta
!
pot_ldrx_rep
"ldrx"
with
|
None
->
pot_ldrx_rep
:=
i
::
!
pot_ldrx_rep
|
Some
(
rep
,
r
,
b
,
n
)
->
eprintf
"LDP_XCPEEP
\n
"
;
let
filt
x
=
x
!=
rep
in
pot_ldrx_rep
:=
List
.
filter
filt
!
pot_ldrx_rep
;
insta
.
(
rep
)
<-
Pnop
;
(
if
min_is_rev
n
n1
then
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpx
,
r
,
rd1
,
ADimm
(
b
,
n
)))
else
if
min_is_rev
n
n1
then
(
if
debug
then
eprintf
"LDP_X_SPACED_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpx
,
r
,
rd1
,
ADimm
(
b
,
n
))))
else
(
if
debug
then
eprintf
"LDP_X_SPACED_PEEP_BACKWARD
\n
"
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
Pldpx
,
rd1
,
r
,
ADimm
(
b
,
n1
)))))
(* Consecutive strw *)
|
(
PStore
(
PSt_rs_a
(
Pstrw
,
IR
(
RR1
rs1
)
,
ADimm
(
b1
,
n1
)))
,
...
...
@@ -300,7 +331,7 @@ let pair_rep insta =
(* When two consec mem addr are targeted by two store. *)
else*)
if
is_valid_strw
b1
b2
n1
n2
then
(
if
debug
then
eprintf
"STP_W
PEEP
\n
"
;
if
debug
then
eprintf
"STP_W
_CONSEC_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PStore
(
Pstp
(
Pstpw
,
rs1
,
rs2
,
ADimm
(
b1
,
n1
)));
insta
.
(
i
+
1
)
<-
Pnop
(* When nothing can be optimized. *)
)
(* Consecutive strx *)
...
...
@@ -310,14 +341,31 @@ let pair_rep insta =
Pnop :: (pair_rep insta t0)
else*)
if
is_valid_strx
b1
b2
n1
n2
then
(
if
debug
then
eprintf
"STP_X
PEEP
\n
"
;
if
debug
then
eprintf
"STP_X
_CONSEC_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PStore
(
Pstp
(
Pstpx
,
rs1
,
rs2
,
ADimm
(
b1
,
n1
)));
insta
.
(
i
+
1
)
<-
Pnop
)
(* Non-consecutive stpw *)
|
PStore
(
PSt_rs_a
(
Pstrw
,
IR
(
RR1
rs1
)
,
ADimm
(
b1
,
n1
)))
,
_
->
(
match
search_compat_rep
rs1
b1
n1
insta
!
pot_strw_rep
"strw"
with
|
None
->
pot_strw_rep
:=
i
::
!
pot_strw_rep
|
Some
(
rep
,
r
,
b
,
n
)
->
let
filt
x
=
x
!=
rep
in
pot_strw_rep
:=
List
.
filter
filt
!
pot_strw_rep
;
insta
.
(
rep
)
<-
Pnop
;
if
debug
then
eprintf
"STP_W_SPACED_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PStore
(
Pstp
(
Pstpw
,
r
,
rs1
,
ADimm
(
b
,
n
))))
(* Non-consecutive stpx *)
|
PStore
(
PSt_rs_a
(
Pstrx
,
IR
(
RR1
rs1
)
,
ADimm
(
b1
,
n1
)))
,
_
->
(
match
search_compat_rep
rs1
b1
n1
insta
!
pot_strx_rep
"strx"
with
|
None
->
pot_strx_rep
:=
i
::
!
pot_strx_rep
|
Some
(
rep
,
r
,
b
,
n
)
->
let
filt
x
=
x
!=
rep
in
pot_strx_rep
:=
List
.
filter
filt
!
pot_strx_rep
;
insta
.
(
rep
)
<-
Pnop
;
if
debug
then
eprintf
"STP_X_SPACED_PEEP_FORWARD
\n
"
;
insta
.
(
i
)
<-
PStore
(
Pstp
(
Pstpx
,
r
,
rs1
,
ADimm
(
b
,
n
))))
(* Any other inst *)
|
h0
,
_
->
(* Here we need to update every symbolic memory according to the matched inst *)
update_pot_rep_basic
h0
insta
pot_ldrw_rep
"ldrw"
;
update_pot_rep_basic
h0
insta
pot_ldrx_rep
"ldrx"
|
_
,
_
->
()
done
(* Calling peephole if flag is set *)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment