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
0bc5b0f9
Commit
0bc5b0f9
authored
Jan 21, 2021
by
Léo Gourdin
Browse files
printer and freg bugfix
parent
30fb0f14
Changes
1
Hide whitespace changes
Inline
Side-by-side
aarch64/PeepholeOracle.ml
View file @
0bc5b0f9
...
...
@@ -64,6 +64,7 @@ let is_valid_str64 b1 b2 n1 n2 =
else
false
let
dreg_of_ireg
r
=
IR
(
RR1
r
)
let
dreg_of_freg
r
=
FR
r
(* Return true if an intermediate
* affectation eliminates the potential
...
...
@@ -85,6 +86,28 @@ let verify_store_affect reg rs b rev =
let
b
=
IR
b
in
dreg_eq
reg
b
||
dreg_eq
reg
rs
type
ph_type
=
|
P32
|
P32f
|
P64
|
P64f
type
inst_type
=
|
Ldr
of
ph_type
|
Str
of
ph_type
let
ph_ty_to_string
=
function
|
Ldr
P32
->
"ldr32"
|
Ldr
P32f
->
"ldr32f"
|
Ldr
P64
->
"ldr64"
|
Ldr
P64f
->
"ldr64f"
|
Str
P32
->
"str32"
|
Str
P32f
->
"str32f"
|
Str
P64
->
"str64"
|
Str
P64f
->
"str64f"
let
print_ph_ty
chan
v
=
output_string
chan
(
ph_ty_to_string
v
)
(* Affect a symbolic memory list of potential replacements
* for a given write in reg *)
let
rec
affect_symb_mem
reg
insta
pot_rep
stype
rev
=
...
...
@@ -92,11 +115,11 @@ let rec affect_symb_mem reg insta pot_rep stype rev =
|
[]
->
[]
|
h0
::
t0
->
(
match
(
insta
.
(
h0
)
,
stype
)
with
|
PLoad
(
PLd_rd_a
(
_
,
rd
,
ADimm
(
b
,
n
)))
,
"ldr"
->
|
PLoad
(
PLd_rd_a
(
_
,
rd
,
ADimm
(
b
,
n
)))
,
Ldr
_
->
if
verify_load_affect
reg
rd
b
rev
then
affect_symb_mem
reg
insta
t0
stype
rev
else
h0
::
affect_symb_mem
reg
insta
t0
stype
rev
|
PStore
(
PSt_rs_a
(
_
,
rs
,
ADimm
(
b
,
n
)))
,
"str"
->
|
PStore
(
PSt_rs_a
(
_
,
rs
,
ADimm
(
b
,
n
)))
,
Str
_
->
if
verify_store_affect
reg
rs
b
rev
then
affect_symb_mem
reg
insta
t0
stype
rev
else
h0
::
affect_symb_mem
reg
insta
t0
stype
rev
...
...
@@ -110,11 +133,11 @@ let rec read_symb_mem reg insta pot_rep stype rev =
|
[]
->
[]
|
h0
::
t0
->
(
match
(
insta
.
(
h0
)
,
stype
)
with
|
PLoad
(
PLd_rd_a
(
_
,
rd
,
ADimm
(
b
,
n
)))
,
"ldr"
->
|
PLoad
(
PLd_rd_a
(
_
,
rd
,
ADimm
(
b
,
n
)))
,
Ldr
_
->
if
verify_load_read
reg
rd
b
rev
then
read_symb_mem
reg
insta
t0
stype
rev
else
h0
::
read_symb_mem
reg
insta
t0
stype
rev
|
PStore
(
PSt_rs_a
(
_
,
rs
,
ADimm
(
b
,
n
)))
,
"str"
->
|
PStore
(
PSt_rs_a
(
_
,
rs
,
ADimm
(
b
,
n
)))
,
Str
_
->
h0
::
read_symb_mem
reg
insta
t0
stype
rev
|
_
,
_
->
failwith
"read_symb_mem: Found an inconsistent inst in pot_rep"
)
...
...
@@ -194,7 +217,8 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
pot_rep
:=
read_symb_mem
rs1
insta
!
pot_rep
stype
rev
|
Pcset
(
rd
,
_
)
->
pot_rep
:=
affect_symb_mem
(
dreg_of_ireg
rd
)
insta
!
pot_rep
stype
rev
|
Pfmovi
(
_
,
_
,
rs
)
->
(
|
Pfmovi
(
_
,
rd
,
rs
)
->
(
pot_rep
:=
affect_symb_mem
(
dreg_of_freg
rd
)
insta
!
pot_rep
stype
rev
;
match
rs
with
|
RR0
rs
->
pot_rep
:=
...
...
@@ -204,12 +228,15 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
pot_rep
:=
affect_symb_mem
rd
insta
!
pot_rep
stype
rev
;
pot_rep
:=
read_symb_mem
rs1
insta
!
pot_rep
stype
rev
;
pot_rep
:=
read_symb_mem
rs2
insta
!
pot_rep
stype
rev
|
Pfnmul
(
_
,
rd
,
rs1
,
rs2
)
->
()
)
|
Pfnmul
(
_
,
rd
,
rs1
,
rs2
)
->
pot_rep
:=
affect_symb_mem
(
dreg_of_freg
rd
)
insta
!
pot_rep
stype
rev
;
pot_rep
:=
read_symb_mem
(
dreg_of_freg
rs1
)
insta
!
pot_rep
stype
rev
;
pot_rep
:=
read_symb_mem
(
dreg_of_freg
rs2
)
insta
!
pot_rep
stype
rev
)
|
PLoad
i
->
(
(* Here, we consider a different behavior for load and store potential candidates:
* a load does not obviously cancel the ldp candidates, but it does for any stp candidate. *)
match
stype
with
|
"ldr"
->
(
|
Ldr
_
->
(
match
i
with
|
PLd_rd_a
(
_
,
rd
,
a
)
->
pot_rep
:=
affect_symb_mem
rd
insta
!
pot_rep
stype
rev
;
...
...
@@ -225,7 +252,7 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
(* Here, we consider that a store cancel all ldp candidates, but it is far more complicated for stp ones :
* if we cancel stp candidates here, we would prevent ourselves to apply the non-consec store peephole.
* To solve this issue, the store candidates cleaning is managed directly in the peephole function below. *)
match
stype
with
"ldr"
->
pot_rep
:=
[]
|
_
->
()
)
match
stype
with
Ldr
_
->
pot_rep
:=
[]
|
_
->
()
)
|
Pallocframe
(
_
,
_
)
->
pot_rep
:=
[]
|
Pfreeframe
(
_
,
_
)
->
pot_rep
:=
[]
|
Ploadsymbol
(
rd
,
_
)
->
...
...
@@ -288,30 +315,30 @@ let are_compat_store (sti1 : store_rs_a) (sti2 : store_rs_a) =
|
Pstrd
|
Pstrd_a
->
(
match
sti2
with
Pstrd
|
Pstrd_a
->
true
|
_
->
false
)
|
_
->
false
let
get_load_
string
(
ldi
:
load_rd_a
)
=
let
get_load_
pht
(
ldi
:
load_rd_a
)
=
match
ldi
with
|
Pldrw
|
Pldrw_a
->
"ldr
32
"
|
Pldrs
->
"ldr
32f
"
|
Pldrx
|
Pldrx_a
->
"ldr
64
"
|
Pldrd
|
Pldrd_a
->
"ldr
64f
"
|
Pldrw
|
Pldrw_a
->
Ldr
P
32
|
Pldrs
->
Ldr
P
32f
|
Pldrx
|
Pldrx_a
->
Ldr
P
64
|
Pldrd
|
Pldrd_a
->
Ldr
P
64f
|
_
->
failwith
"get_load_string: Found a non compatible load to translate"
let
get_store_
string
(
sti
:
store_rs_a
)
=
let
get_store_
pht
(
sti
:
store_rs_a
)
=
match
sti
with
|
Pstrw
|
Pstrw_a
->
"str
32
"
|
Pstrs
->
"str
32f
"
|
Pstrx
|
Pstrx_a
->
"str
64
"
|
Pstrd
|
Pstrd_a
->
"str
64f
"
|
Pstrw
|
Pstrw_a
->
Str
P
32
|
Pstrs
->
Str
P
32f
|
Pstrx
|
Pstrx_a
->
Str
P
64
|
Pstrd
|
Pstrd_a
->
Str
P
64f
|
_
->
failwith
"get_store_string: Found a non compatible store to translate"
let
is_valid_ldr
rd1
rd2
b1
b2
n1
n2
stype
=
match
stype
with
|
"ldr
32
"
|
"ldr
32f
"
->
is_valid_ldr32
rd1
rd2
b1
b2
n1
n2
|
Ldr
P
32
|
Ldr
P
32f
->
is_valid_ldr32
rd1
rd2
b1
b2
n1
n2
|
_
->
is_valid_ldr64
rd1
rd2
b1
b2
n1
n2
let
is_valid_str
b1
b2
n1
n2
stype
=
match
stype
with
|
"str
32
"
|
"str
32f
"
->
is_valid_str32
b1
b2
n1
n2
|
Str
P
32
|
Str
P
32f
->
is_valid_str32
b1
b2
n1
n2
|
_
->
is_valid_str64
b1
b2
n1
n2
(* Try to find the index of the first previous compatible
...
...
@@ -368,14 +395,14 @@ let pair_rep_inv insta =
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
"ldr"
true
;
update_pot_rep_basic
h0
insta
pot_ldrx_rep
"ldr"
true
;
update_pot_rep_basic
h0
insta
pot_ldrs_rep
"ldr"
true
;
update_pot_rep_basic
h0
insta
pot_ldrd_rep
"ldr"
true
;
update_pot_rep_basic
h0
insta
pot_strw_rep
"str"
true
;
update_pot_rep_basic
h0
insta
pot_strx_rep
"str"
true
;
update_pot_rep_basic
h0
insta
pot_strs_rep
"str"
true
;
update_pot_rep_basic
h0
insta
pot_strd_rep
"str"
true
;
update_pot_rep_basic
h0
insta
pot_ldrw_rep
(
Ldr
P32
)
true
;
update_pot_rep_basic
h0
insta
pot_ldrx_rep
(
Ldr
P64
)
true
;
update_pot_rep_basic
h0
insta
pot_ldrs_rep
(
Ldr
P32f
)
true
;
update_pot_rep_basic
h0
insta
pot_ldrd_rep
(
Ldr
P64f
)
true
;
update_pot_rep_basic
h0
insta
pot_strw_rep
(
Str
P32
)
true
;
update_pot_rep_basic
h0
insta
pot_strx_rep
(
Str
P64
)
true
;
update_pot_rep_basic
h0
insta
pot_strs_rep
(
Str
P32f
)
true
;
update_pot_rep_basic
h0
insta
pot_strd_rep
(
Str
P64f
)
true
;
match
(
h0
,
h1
)
with
(* Non-consecutive ldr *)
|
PLoad
(
PLd_rd_a
(
ldi
,
rd1
,
ADimm
(
b1
,
n1
)))
,
_
->
(
...
...
@@ -388,9 +415,9 @@ let pair_rep_inv insta =
|
_
->
pot_ldrd_rep
in
(* Search a previous compatible load *)
let
ld_
string
=
get_load_
string
ldi
in
let
ld_
t
=
get_load_
pht
ldi
in
match
search_compat_rep_inv
rd1
b1
n1
insta
!
pot_rep
ld_
string
search_compat_rep_inv
rd1
b1
n1
insta
!
pot_rep
ld_
t
with
(* If we can't find a candidate, add the current load as a potential future one *)
|
None
->
pot_rep
:=
i
::
!
pot_rep
...
...
@@ -401,13 +428,13 @@ let pair_rep_inv insta =
pot_rep
:=
List
.
filter
filt
!
pot_rep
;
insta
.
(
rep
)
<-
Pnop
;
if
min_is_rev
n
n1
then
(
if
debug
then
eprintf
"LDP_BACK_SPACED_PEEP_IMM_INC_%
s
\n
"
ld_string
;
if
debug
then
eprintf
"LDP_BACK_SPACED_PEEP_IMM_INC_%
a
\n
"
print_ph_ty
ld_t
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
trans_ldi
ldi
,
r
,
rd1
,
c
,
chunk_load
ldi
,
ADimm
(
b
,
n
))))
else
(
if
debug
then
eprintf
"LDP_BACK_SPACED_PEEP_IMM_DEC_%
s
\n
"
ld_string
;
if
debug
then
eprintf
"LDP_BACK_SPACED_PEEP_IMM_DEC_%
a
\n
"
print_ph_ty
ld_t
;
insta
.
(
i
)
<-
PLoad
(
Pldp
...
...
@@ -424,9 +451,9 @@ let pair_rep_inv insta =
|
_
->
pot_strd_rep
in
(* Search a previous compatible store *)
let
st_
string
=
get_store_
string
sti
in
let
st_
t
=
get_store_
pht
sti
in
match
search_compat_rep_inv
rd1
b1
n1
insta
!
pot_rep
st_
string
search_compat_rep_inv
rd1
b1
n1
insta
!
pot_rep
st_
t
with
(* If we can't find a candidate, clean and add the current store as a potential future one *)
|
None
->
...
...
@@ -441,7 +468,7 @@ let pair_rep_inv insta =
let
filt
x
=
x
!=
rep
in
pot_rep
:=
List
.
filter
filt
!
pot_rep
;
insta
.
(
rep
)
<-
Pnop
;
if
debug
then
eprintf
"STP_BACK_SPACED_PEEP_IMM_INC_%
s
\n
"
st_string
;
if
debug
then
eprintf
"STP_BACK_SPACED_PEEP_IMM_INC_%
a
\n
"
print_ph_ty
st_t
;
insta
.
(
i
)
<-
PStore
(
Pstp
...
...
@@ -475,23 +502,23 @@ let pair_rep insta =
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
"ldr"
fals
e
;
update_pot_rep_basic
h0
insta
pot_ldrx_rep
"ldr"
fals
e
;
update_pot_rep_basic
h0
insta
pot_ldrs_rep
"ldr"
fals
e
;
update_pot_rep_basic
h0
insta
pot_ldrd_rep
"ldr"
fals
e
;
update_pot_rep_basic
h0
insta
pot_strw_rep
"str"
fals
e
;
update_pot_rep_basic
h0
insta
pot_strx_rep
"str"
fals
e
;
update_pot_rep_basic
h0
insta
pot_strs_rep
"str"
fals
e
;
update_pot_rep_basic
h0
insta
pot_strd_rep
"str"
fals
e
;
update_pot_rep_basic
h0
insta
pot_ldrw_rep
(
Ldr
P32
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_ldrx_rep
(
Ldr
P64
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_ldrs_rep
(
Ldr
P32f
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_ldrd_rep
(
Ldr
P64f
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_strw_rep
(
Str
P32
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_strx_rep
(
Str
P64
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_strs_rep
(
Str
P32f
)
tru
e
;
update_pot_rep_basic
h0
insta
pot_strd_rep
(
Str
P64f
)
tru
e
;
match
(
h0
,
h1
)
with
(* Consecutive ldr *)
|
(
PLoad
(
PLd_rd_a
(
ldi1
,
rd1
,
ADimm
(
b1
,
n1
)))
,
PLoad
(
PLd_rd_a
(
ldi2
,
rd2
,
ADimm
(
b2
,
n2
)))
)
->
if
are_compat_load
ldi1
ldi2
then
let
ld_
string
=
get_load_
string
ldi1
in
if
is_valid_ldr
rd1
rd2
b1
b2
n1
n2
ld_
string
then
(
let
ld_
t
=
get_load_
pht
ldi1
in
if
is_valid_ldr
rd1
rd2
b1
b2
n1
n2
ld_
t
then
(
if
min_is_rev
n1
n2
then
(
if
debug
then
eprintf
"LDP_CONSEC_PEEP_IMM_INC_%
s
\n
"
ld_string
;
if
debug
then
eprintf
"LDP_CONSEC_PEEP_IMM_INC_%
a
\n
"
print_ph_ty
ld_t
;
insta
.
(
i
)
<-
PLoad
(
Pldp
...
...
@@ -502,7 +529,7 @@ let pair_rep insta =
chunk_load
ldi2
,
ADimm
(
b1
,
n1
)
)))
else
(
if
debug
then
eprintf
"LDP_CONSEC_PEEP_IMM_DEC_%
s
\n
"
ld_string
;
if
debug
then
eprintf
"LDP_CONSEC_PEEP_IMM_DEC_%
a
\n
"
print_ph_ty
ld_t
;
insta
.
(
i
)
<-
PLoad
(
Pldp
...
...
@@ -524,9 +551,9 @@ let pair_rep insta =
|
_
->
pot_ldrd_rep
in
(* Search a previous compatible load *)
let
ld_
string
=
get_load_
string
ldi
in
let
ld_
t
=
get_load_
pht
ldi
in
match
search_compat_rep
rd1
b1
n1
insta
!
pot_rep
ld_
string
search_compat_rep
rd1
b1
n1
insta
!
pot_rep
ld_
t
with
(* If we can't find a candidate, add the current load as a potential future one *)
|
None
->
pot_rep
:=
i
::
!
pot_rep
...
...
@@ -537,13 +564,13 @@ let pair_rep insta =
pot_rep
:=
List
.
filter
filt
!
pot_rep
;
insta
.
(
rep
)
<-
Pnop
;
if
min_is_rev
n
n1
then
(
if
debug
then
eprintf
"LDP_FORW_SPACED_PEEP_IMM_INC_%
s
\n
"
ld_string
;
if
debug
then
eprintf
"LDP_FORW_SPACED_PEEP_IMM_INC_%
a
\n
"
print_ph_ty
ld_t
;
insta
.
(
i
)
<-
PLoad
(
Pldp
(
trans_ldi
ldi
,
r
,
rd1
,
c
,
chunk_load
ldi
,
ADimm
(
b
,
n
))))
else
(
if
debug
then
eprintf
"LDP_FORW_SPACED_PEEP_IMM_DEC_%
s
\n
"
ld_string
;
if
debug
then
eprintf
"LDP_FORW_SPACED_PEEP_IMM_DEC_%
a
\n
"
print_ph_ty
ld_t
;
insta
.
(
i
)
<-
PLoad
(
Pldp
...
...
@@ -560,9 +587,9 @@ let pair_rep insta =
pot_strs_rep
:=
[]
;
pot_strd_rep
:=
[]
;
if
are_compat_store
sti1
sti2
then
let
st_
string
=
get_store_
string
sti1
in
if
is_valid_str
b1
b2
n1
n2
st_
string
then
(
if
debug
then
eprintf
"STP_CONSEC_PEEP_IMM_INC_%
s
\n
"
st_string
;
let
st_
t
=
get_store_
pht
sti1
in
if
is_valid_str
b1
b2
n1
n2
st_
t
then
(
if
debug
then
eprintf
"STP_CONSEC_PEEP_IMM_INC_%
a
\n
"
print_ph_ty
st_t
;
insta
.
(
i
)
<-
PStore
(
Pstp
...
...
@@ -584,9 +611,9 @@ let pair_rep insta =
|
_
->
pot_strd_rep
in
(* Search a previous compatible store *)
let
st_
string
=
get_store_
string
sti
in
let
st_
t
=
get_store_
pht
sti
in
match
search_compat_rep
rd1
b1
n1
insta
!
pot_rep
st_
string
search_compat_rep
rd1
b1
n1
insta
!
pot_rep
st_
t
with
(* If we can't find a candidate, clean and add the current store as a potential future one *)
|
None
->
...
...
@@ -601,7 +628,7 @@ let pair_rep insta =
let
filt
x
=
x
!=
rep
in
pot_rep
:=
List
.
filter
filt
!
pot_rep
;
insta
.
(
rep
)
<-
Pnop
;
if
debug
then
eprintf
"STP_FORW_SPACED_PEEP_IMM_INC_%
s
\n
"
st_string
;
if
debug
then
eprintf
"STP_FORW_SPACED_PEEP_IMM_INC_%
a
\n
"
print_ph_ty
st_t
;
insta
.
(
i
)
<-
PStore
(
Pstp
(
trans_sti
sti
,
r
,
rd1
,
c
,
chunk_store
sti
,
ADimm
(
b
,
n
)))
...
...
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