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
eb35c300
Commit
eb35c300
authored
Mar 02, 2021
by
Léo Gourdin
Browse files
Adding a flag to test fp_init_exp
parent
6f71a2a3
Changes
3
Hide whitespace changes
Inline
Side-by-side
driver/Clflags.ml
View file @
eb35c300
...
...
@@ -106,6 +106,7 @@ let option_div_i32 = ref "stsud"
let
option_div_i64
=
ref
"stsud"
let
option_fcoalesce_mem
=
ref
true
let
option_fexpanse_rtlcond
=
ref
true
let
option_fexpanse_fpconst
=
ref
true
let
option_fforward_moves
=
ref
false
let
option_fmove_loop_invariants
=
ref
false
let
option_fnontrap_loads
=
ref
true
...
...
driver/Driver.ml
View file @
eb35c300
...
...
@@ -445,6 +445,7 @@ let cmdline_actions =
@
f_opt
"nontrap-loads"
option_fnontrap_loads
@
f_opt
"coalesce-mem"
option_fcoalesce_mem
@
f_opt
"expanse-rtlcond"
option_fexpanse_rtlcond
@
f_opt
"expanse-fpconst"
option_fexpanse_fpconst
@
f_opt
"all-loads-nontrap"
option_all_loads_nontrap
@
f_opt
"forward-moves"
option_fforward_moves
(* Code generation options *)
...
...
riscV/ExpansionOracle.ml
View file @
eb35c300
...
...
@@ -389,156 +389,163 @@ let expanse (sb : superblock) code pm =
let
pm'
=
ref
pm
in
Array
.
iter
(
fun
n
->
was_branch
:=
false
;
was_exp
:=
false
;
let
inst
=
get_some
@@
PTree
.
get
n
code
in
(
match
inst
with
(* Expansion of conditions - Ocmp *)
|
Iop
(
Ocmp
(
Ccomp
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccomp
\n
"
;
exp
:=
cond_int32s
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompu
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompu
\n
"
;
exp
:=
cond_int32u
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompimm
\n
"
;
exp
:=
expanse_condimm_int32s
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompuimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompuimm
\n
"
;
exp
:=
expanse_condimm_int32u
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompl
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompl
\n
"
;
exp
:=
cond_int64s
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccomplu
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccomplu
\n
"
;
exp
:=
cond_int64u
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccomplimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccomplimm
\n
"
;
exp
:=
expanse_condimm_int64s
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompluimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompluimm
\n
"
;
exp
:=
expanse_condimm_int64u
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompf
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompf
\n
"
;
exp
:=
expanse_cond_fp
false
cond_float
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Cnotcompf
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Cnotcompf
\n
"
;
exp
:=
expanse_cond_fp
true
cond_float
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompfs
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompfs
\n
"
;
exp
:=
expanse_cond_fp
false
cond_single
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Cnotcompfs
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Cnotcompfs
\n
"
;
exp
:=
expanse_cond_fp
true
cond_single
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
(* Expansion of branches - Ccomp *)
|
Icond
(
Ccomp
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccomp
\n
"
;
exp
:=
cbranch_int32s
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompu
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompu
\n
"
;
exp
:=
cbranch_int32u
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompimm
\n
"
;
exp
:=
expanse_cbranchimm_int32s
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompuimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompuimm
\n
"
;
exp
:=
expanse_cbranchimm_int32u
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompl
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompl
\n
"
;
exp
:=
cbranch_int64s
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccomplu
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccomplu
\n
"
;
exp
:=
cbranch_int64u
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccomplimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccomplimm
\n
"
;
exp
:=
expanse_cbranchimm_int64s
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompluimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompluimm
\n
"
;
exp
:=
expanse_cbranchimm_int64u
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompf
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompf
\n
"
;
exp
:=
expanse_cbranch_fp
false
cond_float
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Cnotcompf
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Cnotcompf
\n
"
;
exp
:=
expanse_cbranch_fp
true
cond_float
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompfs
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompfs
\n
"
;
exp
:=
expanse_cbranch_fp
false
cond_single
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Cnotcompfs
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Cnotcompfs
\n
"
;
exp
:=
expanse_cbranch_fp
true
cond_single
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
(* Expansion of fp constants *)
|
Iop
(
Ofloatconst
f
,
nil
,
dest
,
succ
)
->
debug
"Iop/Ofloatconst
\n
"
;
let
r
=
r2pi
()
in
exp
:=
[
Iop
(
Olongconst
(
Floats
.
Float
.
to_bits
f
)
,
[]
,
r
,
n2pi
()
);
Iop
(
Ofloat_of_bits
,
[
r
]
,
dest
,
succ
);
];
was_exp
:=
true
|
Iop
(
Osingleconst
f
,
nil
,
dest
,
succ
)
->
debug
"Iop/Osingleconst
\n
"
;
let
r
=
r2pi
()
in
exp
:=
[
Iop
(
Ointconst
(
Floats
.
Float32
.
to_bits
f
)
,
[]
,
r
,
n2pi
()
);
Iop
(
Osingle_of_bits
,
[
r
]
,
dest
,
succ
);
];
was_exp
:=
true
|
_
->
new_order
:=
n
::
!
new_order
);
if
!
was_exp
then
(
node
:=
!
node
+
1
;
(
if
!
was_branch
then
let
lives
=
PTree
.
get
n
!
liveins
in
match
lives
with
|
Some
lives
->
let
new_branch_pc
=
Camlcoq
.
P
.
of_int
(
!
node
-
(
List
.
length
!
exp
-
1
))
in
liveins
:=
PTree
.
set
new_branch_pc
lives
!
liveins
;
liveins
:=
PTree
.
remove
n
!
liveins
|
_
->
()
);
write_pathmap
sb
.
instructions
.
(
0
)
(
List
.
length
!
exp
)
pm'
;
write_initial_node
n
code'
new_order
;
write_tree
!
exp
!
node
code'
new_order
))
begin
(
was_branch
:=
false
;
was_exp
:=
false
;
let
inst
=
get_some
@@
PTree
.
get
n
code
in
if
!
Clflags
.
option_fexpanse_rtlcond
then
(
match
inst
with
(* Expansion of conditions - Ocmp *)
|
Iop
(
Ocmp
(
Ccomp
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccomp
\n
"
;
exp
:=
cond_int32s
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompu
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompu
\n
"
;
exp
:=
cond_int32u
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompimm
\n
"
;
exp
:=
expanse_condimm_int32s
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompuimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompuimm
\n
"
;
exp
:=
expanse_condimm_int32u
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompl
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompl
\n
"
;
exp
:=
cond_int64s
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccomplu
c
)
,
a1
::
a2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccomplu
\n
"
;
exp
:=
cond_int64u
false
c
a1
a2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccomplimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccomplimm
\n
"
;
exp
:=
expanse_condimm_int64s
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompluimm
(
c
,
imm
))
,
a1
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompluimm
\n
"
;
exp
:=
expanse_condimm_int64u
c
a1
imm
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompf
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompf
\n
"
;
exp
:=
expanse_cond_fp
false
cond_float
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Cnotcompf
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Cnotcompf
\n
"
;
exp
:=
expanse_cond_fp
true
cond_float
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Ccompfs
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Ccompfs
\n
"
;
exp
:=
expanse_cond_fp
false
cond_single
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
|
Iop
(
Ocmp
(
Cnotcompfs
c
)
,
f1
::
f2
::
nil
,
dest
,
succ
)
->
debug
"Iop/Cnotcompfs
\n
"
;
exp
:=
expanse_cond_fp
true
cond_single
c
f1
f2
dest
succ
[]
;
was_exp
:=
true
(* Expansion of branches - Ccomp *)
|
Icond
(
Ccomp
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccomp
\n
"
;
exp
:=
cbranch_int32s
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompu
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompu
\n
"
;
exp
:=
cbranch_int32u
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompimm
\n
"
;
exp
:=
expanse_cbranchimm_int32s
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompuimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompuimm
\n
"
;
exp
:=
expanse_cbranchimm_int32u
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompl
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompl
\n
"
;
exp
:=
cbranch_int64s
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccomplu
c
,
a1
::
a2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccomplu
\n
"
;
exp
:=
cbranch_int64u
false
c
a1
a2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccomplimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccomplimm
\n
"
;
exp
:=
expanse_cbranchimm_int64s
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompluimm
(
c
,
imm
)
,
a1
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompluimm
\n
"
;
exp
:=
expanse_cbranchimm_int64u
c
a1
imm
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompf
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompf
\n
"
;
exp
:=
expanse_cbranch_fp
false
cond_float
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Cnotcompf
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Cnotcompf
\n
"
;
exp
:=
expanse_cbranch_fp
true
cond_float
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Ccompfs
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Ccompfs
\n
"
;
exp
:=
expanse_cbranch_fp
false
cond_single
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
Icond
(
Cnotcompfs
c
,
f1
::
f2
::
nil
,
succ1
,
succ2
,
info
)
->
debug
"Icond/Cnotcompfs
\n
"
;
exp
:=
expanse_cbranch_fp
true
cond_single
c
f1
f2
info
succ1
succ2
[]
;
was_branch
:=
true
;
was_exp
:=
true
|
_
->
()
);
if
(
!
Clflags
.
option_fexpanse_fpconst
&&
not
!
was_exp
)
then
(
match
inst
with
(* Expansion of fp constants *)
|
Iop
(
Ofloatconst
f
,
nil
,
dest
,
succ
)
->
debug
"Iop/Ofloatconst
\n
"
;
let
r
=
r2pi
()
in
exp
:=
[
Iop
(
Olongconst
(
Floats
.
Float
.
to_bits
f
)
,
[]
,
r
,
n2pi
()
);
Iop
(
Ofloat_of_bits
,
[
r
]
,
dest
,
succ
);
];
was_exp
:=
true
|
Iop
(
Osingleconst
f
,
nil
,
dest
,
succ
)
->
debug
"Iop/Osingleconst
\n
"
;
let
r
=
r2pi
()
in
exp
:=
[
Iop
(
Ointconst
(
Floats
.
Float32
.
to_bits
f
)
,
[]
,
r
,
n2pi
()
);
Iop
(
Osingle_of_bits
,
[
r
]
,
dest
,
succ
);
];
was_exp
:=
true
|
_
->
()
);
if
!
was_exp
then
(
node
:=
!
node
+
1
;
(
if
!
was_branch
then
let
lives
=
PTree
.
get
n
!
liveins
in
match
lives
with
|
Some
lives
->
let
new_branch_pc
=
Camlcoq
.
P
.
of_int
(
!
node
-
(
List
.
length
!
exp
-
1
))
in
liveins
:=
PTree
.
set
new_branch_pc
lives
!
liveins
;
liveins
:=
PTree
.
remove
n
!
liveins
|
_
->
()
);
write_pathmap
sb
.
instructions
.
(
0
)
(
List
.
length
!
exp
)
pm'
;
write_initial_node
n
code'
new_order
;
write_tree
!
exp
!
node
code'
new_order
)
else
new_order
:=
n
::
!
new_order
)
end
)
sb
.
instructions
;
sb
.
instructions
<-
Array
.
of_list
(
List
.
rev
!
new_order
);
sb
.
liveins
<-
!
liveins
;
...
...
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