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
e265be77
Commit
e265be77
authored
Jan 20, 2021
by
David Monniaux
Browse files
Conditions now propagated by CSE3
Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
parents
fc9d9ffc
eb1121d7
Changes
17
Expand all
Hide whitespace changes
Inline
Side-by-side
aarch64/Op.v
View file @
e265be77
...
...
@@ -1202,18 +1202,26 @@ Proof.
rewrite
(
cond_depends_on_memory_correct
cond
args
m1
m2
H
).
auto
.
Qed
.
Lemma
cond_valid_pointer_eq
:
forall
cond
args
m1
m2
,
(
forall
b
z
,
Mem
.
valid_pointer
m1
b
z
=
Mem
.
valid_pointer
m2
b
z
)
->
eval_condition
cond
args
m1
=
eval_condition
cond
args
m2
.
Proof
.
intros
until
m2
.
intro
MEM
.
destruct
cond
eqn
:
COND
;
simpl
;
try
congruence
.
all:
repeat
(
destruct
args
;
simpl
;
try
congruence
);
erewrite
cmpu_bool_valid_pointer_eq
||
erewrite
cmplu_bool_valid_pointer_eq
;
eauto
.
Qed
.
Lemma
op_valid_pointer_eq
:
forall
(
F
V
:
Type
)
(
ge
:
Genv
.
t
F
V
)
sp
op
args
m1
m2
,
(
forall
b
z
,
Mem
.
valid_pointer
m1
b
z
=
Mem
.
valid_pointer
m2
b
z
)
->
eval_operation
ge
sp
op
args
m1
=
eval_operation
ge
sp
op
args
m2
.
Proof
.
intros
until
m2
.
destruct
op
eqn
:
OP
;
simpl
;
try
congruence
.
-
intros
MEM
;
destruct
cond
;
simpl
;
try
congruence
;
intros
until
m2
.
intro
MEM
.
destruct
op
eqn
:
OP
;
simpl
;
try
congruence
.
-
f_equal
;
f_equal
;
auto
using
cond_valid_pointer_eq
.
-
destruct
cond
;
simpl
;
try
congruence
;
repeat
(
destruct
args
;
simpl
;
try
congruence
);
erewrite
cmpu_bool_valid_pointer_eq
||
erewrite
cmplu_bool_valid_pointer_eq
;
eauto
.
-
intro
MEM
;
destruct
cond
;
simpl
;
try
congruence
;
repeat
(
destruct
args
;
simpl
;
try
congruence
);
erewrite
cmpu_bool_valid_pointer_eq
||
erewrite
cmplu_bool_valid_pointer_eq
;
eauto
.
Qed
.
(
**
Global
variables
mentioned
in
an
operation
or
addressing
mode
*
)
...
...
arm/Op.v
View file @
e265be77
...
...
@@ -718,7 +718,7 @@ Definition is_trivial_op (op: operation) : bool :=
(
**
Operations
that
depend
on
the
memory
state
.
*
)
Definition
cond
ition
_depends_on_memory
(
c
:
condition
)
:
bool
:=
Definition
cond_depends_on_memory
(
c
:
condition
)
:
bool
:=
match
c
with
|
Ccompu
_
|
Ccompushift
_
_
|
Ccompuimm
_
_
=>
true
|
_
=>
false
...
...
@@ -726,14 +726,14 @@ Definition condition_depends_on_memory (c: condition) : bool :=
Definition
op_depends_on_memory
(
op
:
operation
)
:
bool
:=
match
op
with
|
Ocmp
c
=>
cond
ition
_depends_on_memory
c
|
Osel
c
ty
=>
cond
ition
_depends_on_memory
c
|
Ocmp
c
=>
cond_depends_on_memory
c
|
Osel
c
ty
=>
cond_depends_on_memory
c
|
_
=>
false
end
.
Lemma
cond
ition
_depends_on_memory_correct
:
Lemma
cond_depends_on_memory_correct
:
forall
c
args
m1
m2
,
cond
ition
_depends_on_memory
c
=
false
->
cond_depends_on_memory
c
=
false
->
eval_condition
c
args
m1
=
eval_condition
c
args
m2
.
Proof
.
intros
.
destruct
c
;
simpl
;
auto
;
discriminate
.
...
...
@@ -745,12 +745,22 @@ Lemma op_depends_on_memory_correct:
eval_operation
ge
sp
op
args
m1
=
eval_operation
ge
sp
op
args
m2
.
Proof
.
intros
until
m2
.
destruct
op
;
simpl
;
try
congruence
;
intros
C
.
-
f_equal
;
f_equal
;
apply
cond
ition
_depends_on_memory_correct
;
auto
.
-
f_equal
;
f_equal
;
apply
cond_depends_on_memory_correct
;
auto
.
-
destruct
args
;
auto
.
destruct
args
;
auto
.
rewrite
(
cond
ition
_depends_on_memory_correct
c
args
m1
m2
C
).
rewrite
(
cond_depends_on_memory_correct
c
args
m1
m2
C
).
auto
.
Qed
.
Lemma
cond_valid_pointer_eq
:
forall
cond
args
m1
m2
,
(
forall
b
z
,
Mem
.
valid_pointer
m1
b
z
=
Mem
.
valid_pointer
m2
b
z
)
->
eval_condition
cond
args
m1
=
eval_condition
cond
args
m2
.
Proof
.
intros
until
m2
.
intro
MEM
.
destruct
cond
eqn
:
COND
;
simpl
;
try
congruence
.
all:
repeat
(
destruct
args
;
simpl
;
try
congruence
);
erewrite
cmpu_bool_valid_pointer_eq
||
erewrite
cmplu_bool_valid_pointer_eq
;
eauto
.
Qed
.
Lemma
op_valid_pointer_eq
:
forall
(
F
V
:
Type
)
(
ge
:
Genv
.
t
F
V
)
sp
op
args
m1
m2
,
(
forall
b
z
,
Mem
.
valid_pointer
m1
b
z
=
Mem
.
valid_pointer
m2
b
z
)
->
...
...
backend/CSE3.v
View file @
e265be77
...
...
@@ -53,6 +53,27 @@ Definition forward_move_l_b (rb : RB.t) (xl : list reg) :=
Definition
subst_args
fmap
pc
xl
:=
forward_move_l_b
(
PMap
.
get
pc
fmap
)
xl
.
Definition
find_cond_in_fmap
fmap
pc
cond
args
:=
if
Compopts
.
optim_CSE3_conditions
tt
then
match
PMap
.
get
pc
fmap
with
|
Some
rel
=>
if
is_condition_present
(
ctx
:=
ctx
)
pc
rel
cond
args
then
Some
true
else
let
ncond
:=
negate_condition
cond
in
if
is_condition_present
(
ctx
:=
ctx
)
pc
rel
ncond
args
then
Some
false
else
let
args
'
:=
subst_args
fmap
pc
args
in
if
is_condition_present
(
ctx
:=
ctx
)
pc
rel
cond
args
'
then
Some
true
else
if
is_condition_present
(
ctx
:=
ctx
)
pc
rel
ncond
args
'
then
Some
false
else
None
|
None
=>
None
end
else
None
.
Definition
transf_instr
(
fmap
:
PMap
.
t
RB
.
t
)
(
pc
:
node
)
(
instr
:
instruction
)
:=
match
instr
with
...
...
@@ -76,7 +97,11 @@ Definition transf_instr (fmap : PMap.t RB.t)
|
Itailcall
sig
ros
args
=>
Itailcall
sig
ros
(
subst_args
fmap
pc
args
)
|
Icond
cond
args
s1
s2
expected
=>
Icond
cond
(
subst_args
fmap
pc
args
)
s1
s2
expected
let
args
'
:=
subst_args
fmap
pc
args
in
match
find_cond_in_fmap
fmap
pc
cond
args
with
|
None
=>
Icond
cond
args
'
s1
s2
expected
|
Some
b
=>
Inop
(
if
b
then
s1
else
s2
)
end
|
Ijumptable
arg
tbl
=>
Ijumptable
(
subst_arg
fmap
pc
arg
)
tbl
|
Ireturn
(
Some
arg
)
=>
...
...
backend/CSE3analysis.v
View file @
e265be77
...
...
@@ -145,18 +145,17 @@ Proof.
exact
peq
.
Defined
.
Record
equation
:=
mkequation
{
eq_lhs
:
reg
;
eq_op
:
sym_op
;
eq_args
:
list
reg
}
.
Inductive
equation_or_condition
:=
|
Equ
:
reg
->
sym_op
->
list
reg
->
equation_or_condition
|
Cond
:
condition
->
list
reg
->
equation_or_condition
.
Definition
eq_dec_equation
:
forall
eq
eq
'
:
equation
,
{
eq
=
eq
'
}
+
{
eq
<>
eq
'
}
.
forall
eq
eq
'
:
equation
_or_condition
,
{
eq
=
eq
'
}
+
{
eq
<>
eq
'
}
.
Proof
.
generalize
peq
.
generalize
eq_dec_sym_op
.
generalize
eq_dec_args
.
generalize
eq_condition
.
decide
equality
.
Defined
.
...
...
@@ -168,34 +167,42 @@ Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
Definition
add_ilist_j
(
ilist
:
list
reg
)
(
j
:
eq_id
)
(
m
:
Regmap
.
t
PSet
.
t
)
:=
List
.
fold_left
(
fun
already
i
=>
add_i_j
i
j
already
)
ilist
m
.
Definition
get_reg_kills
(
eqs
:
PTree
.
t
equation
)
:
Definition
get_reg_kills
(
eqs
:
PTree
.
t
equation
_or_condition
)
:
Regmap
.
t
PSet
.
t
:=
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation
)
=>
add_i_j
(
eq_lhs
eq
)
eqno
(
add_ilist_j
(
eq_args
eq
)
eqno
already
))
eqs
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq_cond
:
equation_or_condition
)
=>
match
eq_cond
with
|
Equ
lhs
sop
args
=>
add_i_j
lhs
eqno
(
add_ilist_j
args
eqno
already
)
|
Cond
cond
args
=>
add_ilist_j
args
eqno
already
end
)
eqs
(
PMap
.
init
PSet
.
empty
).
Definition
eq_depends_on_mem
eq
:=
match
eq_op
eq
with
|
SLoad
_
_
=>
true
|
SOp
op
=>
op_depends_on_memory
op
Definition
eq_cond_depends_on_mem
eq_cond
:=
match
eq_cond
with
|
Equ
lhs
sop
args
=>
match
sop
with
|
SLoad
_
_
=>
true
|
SOp
op
=>
op_depends_on_memory
op
end
|
Cond
cond
args
=>
cond_depends_on_memory
cond
end
.
Definition
eq_depends_on_store
eq
:=
match
eq_
op
eq
with
|
SLoad
_
_
=>
true
|
SOp
op
=>
false
Definition
eq_
cond_
depends_on_store
eq
_cond
:=
match
eq_
cond
with
|
Equ
_
(
SLoad
_
_
)
_
=>
true
|
_
=>
false
end
.
Definition
get_mem_kills
(
eqs
:
PTree
.
t
equation
)
:
PSet
.
t
:=
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation
)
=>
if
eq_depends_on_mem
eq
Definition
get_mem_kills
(
eqs
:
PTree
.
t
equation
_or_condition
)
:
PSet
.
t
:=
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation
_or_condition
)
=>
if
eq_
cond_
depends_on_mem
eq
then
PSet
.
add
eqno
already
else
already
)
eqs
PSet
.
empty
.
Definition
get_store_kills
(
eqs
:
PTree
.
t
equation
)
:
PSet
.
t
:=
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation
)
=>
if
eq_depends_on_store
eq
Definition
get_store_kills
(
eqs
:
PTree
.
t
equation
_or_condition
)
:
PSet
.
t
:=
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation
_or_condition
)
=>
if
eq_
cond_
depends_on_store
eq
then
PSet
.
add
eqno
already
else
already
)
eqs
PSet
.
empty
.
...
...
@@ -215,21 +222,25 @@ Proof.
-
right
;
congruence
.
Qed
.
Definition
get_moves
(
eqs
:
PTree
.
t
equation
)
:
Definition
get_moves
(
eqs
:
PTree
.
t
equation
_or_condition
)
:
Regmap
.
t
PSet
.
t
:=
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation
)
=>
if
is_smove
(
eq_op
eq
)
then
add_i_j
(
eq_lhs
eq
)
eqno
already
else
already
)
eqs
(
PMap
.
init
PSet
.
empty
).
PTree
.
fold
(
fun
already
(
eqno
:
eq_id
)
(
eq
:
equation_or_condition
)
=>
match
eq
with
|
Equ
lhs
sop
args
=>
if
is_smove
sop
then
add_i_j
lhs
eqno
already
else
already
|
_
=>
already
end
)
eqs
(
PMap
.
init
PSet
.
empty
).
Record
eq_context
:=
mkeqcontext
{
eq_catalog
:
eq_id
->
option
equation
;
eq_find_oracle
:
node
->
equation
->
option
eq_id
;
eq_rhs_oracle
:
node
->
sym_op
->
list
reg
->
PSet
.
t
;
eq_kill_reg
:
reg
->
PSet
.
t
;
eq_kill_mem
:
unit
->
PSet
.
t
;
eq_kill_store
:
unit
->
PSet
.
t
;
eq_moves
:
reg
->
PSet
.
t
}
.
{
eq_catalog
:
eq_id
->
option
equation
_or_condition
;
eq_find_oracle
:
node
->
equation
_or_condition
->
option
eq_id
;
eq_rhs_oracle
:
node
->
sym_op
->
list
reg
->
PSet
.
t
;
eq_kill_reg
:
reg
->
PSet
.
t
;
eq_kill_mem
:
unit
->
PSet
.
t
;
eq_kill_store
:
unit
->
PSet
.
t
;
eq_moves
:
reg
->
PSet
.
t
}
.
Section
OPERATIONS
.
Context
{
ctx
:
eq_context
}
.
...
...
@@ -251,10 +262,10 @@ Section OPERATIONS.
|
None
=>
x
|
Some
eqno
=>
match
eq_catalog
ctx
eqno
with
|
Some
eq
=>
if
is_smove
(
eq_op
eq
)
&&
peq
x
(
eq_lhs
eq
)
|
Some
(
Equ
lhs
sop
args
)
=>
if
is_smove
sop
&&
peq
x
lhs
then
match
eq_
args
eq
with
match
args
with
|
src
::
nil
=>
src
|
_
=>
x
end
...
...
@@ -269,7 +280,7 @@ Section OPERATIONS.
Section
PER_NODE
.
Variable
no
:
node
.
Definition
eq_find
(
eq
:
equation
)
:=
Definition
eq_find
(
eq
:
equation
_or_condition
)
:=
match
eq_find_oracle
ctx
no
eq
with
|
Some
id
=>
match
eq_catalog
ctx
id
with
...
...
@@ -279,25 +290,29 @@ Section OPERATIONS.
|
None
=>
None
end
.
Definition
is_condition_present
(
rel
:
RELATION
.
t
)
(
cond
:
condition
)
(
args
:
list
reg
)
:=
match
eq_find
(
Cond
cond
args
)
with
|
Some
id
=>
PSet
.
contains
rel
id
|
None
=>
false
end
.
Definition
rhs_find
(
sop
:
sym_op
)
(
args
:
list
reg
)
(
rel
:
RELATION
.
t
)
:
option
reg
:=
match
pick_source
(
PSet
.
elements
(
PSet
.
inter
(
eq_rhs_oracle
ctx
no
sop
args
)
rel
))
with
|
None
=>
None
|
Some
src
=>
match
eq_catalog
ctx
src
with
|
None
=>
None
|
Some
eq
=>
if
eq_dec_sym_op
sop
(
eq_op
eq
)
&&
eq_dec_args
args
(
eq_args
eq
)
then
Some
(
eq_lhs
eq
)
|
Some
(
Equ
eq_lhs
eq_sop
eq_args
)
=>
if
eq_dec_sym_op
sop
eq_sop
&&
eq_dec_args
args
eq_args
then
Some
eq_lhs
else
None
|
_
=>
None
end
end
.
Definition
oper2
(
dst
:
reg
)
(
op
:
sym_op
)(
args
:
list
reg
)
(
rel
:
RELATION
.
t
)
:
RELATION
.
t
:=
match
eq_find
{|
eq_lhs
:=
dst
;
eq_op
:=
op
;
eq_args:
=
args
|}
with
match
eq_find
(
Equ
dst
op
args
)
with
|
Some
id
=>
if
PSet
.
contains
rel
id
then
rel
...
...
@@ -316,9 +331,7 @@ Section OPERATIONS.
if
peq
src
dst
then
rel
else
match
eq_find
{|
eq_lhs
:=
dst
;
eq_op
:=
SOp
Omove
;
eq_args:
=
src
::
nil
|}
with
match
eq_find
(
Equ
dst
(
SOp
Omove
)
(
src
::
nil
))
with
|
Some
eq_id
=>
PSet
.
add
eq_id
(
kill_reg
dst
rel
)
|
None
=>
kill_reg
dst
rel
end
.
...
...
@@ -366,13 +379,13 @@ Section OPERATIONS.
(
PSet
.
filter
(
fun
eqno
=>
match
eq_catalog
ctx
eqno
with
|
None
=>
false
|
Some
eq
=>
match
eq_op
eq
with
|
Some
(
Equ
eq_lhs
eq_sop
eq_args
)
=>
match
eq_sop
with
|
SOp
op
=>
true
|
SLoad
chunk
'
addr
'
=>
may_overlap
chunk
addr
args
chunk
'
addr
'
(
eq_args
eq
)
may_overlap
chunk
addr
args
chunk
'
addr
'
eq_args
end
|
_
=>
false
end
)
(
PSet
.
inter
rel
(
eq_kill_store
ctx
tt
))).
...
...
@@ -391,9 +404,7 @@ Section OPERATIONS.
let
rel
'
:=
store2
chunk
addr
args
src
rel
in
if
loadv_storev_compatible_type
chunk
ty
then
match
eq_find
{|
eq_lhs
:=
src
;
eq_op
:=
SLoad
chunk
addr
;
eq_args:
=
args
|}
with
match
eq_find
(
Equ
src
(
SLoad
chunk
addr
)
args
)
with
|
Some
id
=>
PSet
.
add
id
rel
'
|
None
=>
rel
'
end
...
...
@@ -450,28 +461,55 @@ Section OPERATIONS.
|
_
=>
rel
end
.
Definition
apply_instr
(
tenv
:
typing_env
)
(
instr
:
RTL
.
instruction
)
(
rel
:
RELATION
.
t
)
:
RB
.
t
:=
Definition
apply_cond1
cond
args
(
rel
:
RELATION
.
t
)
:
RB
.
t
:=
match
eq_find
(
Cond
(
negate_condition
cond
)
args
)
with
|
Some
eq_id
=>
if
PSet
.
contains
rel
eq_id
then
RB
.
bot
else
Some
rel
|
None
=>
Some
rel
end
.
Definition
apply_cond0
cond
args
(
rel
:
RELATION
.
t
)
:
RELATION
.
t
:=
match
eq_find
(
Cond
cond
args
)
with
|
Some
eq_id
=>
PSet
.
add
eq_id
rel
|
None
=>
rel
end
.
Definition
apply_cond
cond
args
(
rel
:
RELATION
.
t
)
:
RB
.
t
:=
if
Compopts
.
optim_CSE3_conditions
tt
then
match
apply_cond1
cond
args
rel
with
|
Some
rel
=>
Some
(
apply_cond0
cond
args
rel
)
|
None
=>
RB
.
bot
end
else
Some
rel
.
Definition
apply_instr
(
tenv
:
typing_env
)
(
instr
:
RTL
.
instruction
)
(
rel
:
RELATION
.
t
)
:
list
(
node
*
RB
.
t
)
:=
match
instr
with
|
Inop
_
|
Icond
_
_
_
_
_
|
Ijumptable
_
_
=>
Some
rel
|
Istore
chunk
addr
args
src
_
=>
Some
(
store
tenv
chunk
addr
args
src
rel
)
|
Iop
op
args
dst
_
=>
Some
(
oper
dst
(
SOp
op
)
args
rel
)
|
Iload
trap
chunk
addr
args
dst
_
=>
Some
(
oper
dst
(
SLoad
chunk
addr
)
args
rel
)
|
Icall
_
_
_
dst
_
=>
Some
(
kill_reg
dst
(
kill_mem
rel
))
|
Ibuiltin
ef
_
res
_
=>
Some
(
kill_builtin_res
res
(
apply_external_call
ef
rel
))
|
Itailcall
_
_
_
|
Ireturn
_
=>
RB
.
bot
|
Inop
pc
'
=>
(
pc
'
,
(
Some
rel
))
::
nil
|
Icond
cond
args
ifso
ifnot
_
=>
(
ifso
,
(
apply_cond
cond
args
rel
))
::
(
ifnot
,
(
apply_cond
(
negate_condition
cond
)
args
rel
))
::
nil
|
Ijumptable
_
targets
=>
List
.
map
(
fun
pc
'
=>
(
pc
'
,
(
Some
rel
)))
targets
|
Istore
chunk
addr
args
src
pc
'
=>
(
pc
'
,
(
Some
(
store
tenv
chunk
addr
args
src
rel
)))
::
nil
|
Iop
op
args
dst
pc
'
=>
(
pc
'
,
(
Some
(
oper
dst
(
SOp
op
)
args
rel
)))
::
nil
|
Iload
trap
chunk
addr
args
dst
pc
'
=>
(
pc
'
,
(
Some
(
oper
dst
(
SLoad
chunk
addr
)
args
rel
)))
::
nil
|
Icall
_
_
_
dst
pc
'
=>
(
pc
'
,
(
Some
(
kill_reg
dst
(
kill_mem
rel
))))
::
nil
|
Ibuiltin
ef
_
res
pc
'
=>
(
pc
'
,
(
Some
(
kill_builtin_res
res
(
apply_external_call
ef
rel
))))
::
nil
|
Itailcall
_
_
_
|
Ireturn
_
=>
nil
end
.
End
PER_NODE
.
Definition
apply_instr
'
(
tenv
:
typing_env
)
code
(
pc
:
node
)
(
ro
:
RB
.
t
)
:
RB
.
t
:=
match
ro
with
|
None
=>
None
|
Some
x
=>
match
code
!
pc
with
|
None
=>
RB
.
bot
|
Some
instr
=>
apply_instr
pc
tenv
instr
x
Definition
apply_instr
'
(
tenv
:
typing_env
)
code
(
pc
:
node
)
(
ro
:
RB
.
t
)
:
list
(
node
*
RB
.
t
)
:=
match
code
!
pc
with
|
None
=>
nil
|
Some
instr
=>
match
ro
with
|
None
=>
List
.
map
(
fun
pc
'
=>
(
pc
'
,
RB
.
bot
))
(
successors_instr
instr
)
|
Some
x
=>
apply_instr
pc
tenv
instr
x
end
end
.
...
...
@@ -493,24 +531,25 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva
match
PMap
.
get
pc
inv
with
|
None
=>
true
|
Some
rel
=>
let
rel
'
:=
apply_instr
pc
tenv
instr
rel
in
List
.
forallb
(
fun
pc
'
=>
relb_leb
rel
'
(
PMap
.
get
pc
'
inv
))
(
RTL
.
successors_instr
instr
)
(
fun
szz
=>
relb_leb
(
snd
szz
)
(
PMap
.
get
(
fst
szz
)
inv
))
(
apply_instr
pc
tenv
instr
rel
)
end
).
(
*
No
longer
used
.
Incompatible
with
transfer
functions
that
yield
a
different
result
depending
on
the
successor
.
Definition
internal_analysis
(
tenv
:
typing_env
)
(
f
:
RTL
.
function
)
:
option
invariants
:=
DS
.
fixpoint
(
RTL
.
fn_code
f
)
RTL
.
successors_instr
(
apply_instr
'
tenv
(
RTL
.
fn_code
f
))
(
RTL
.
fn_entrypoint
f
)
(
Some
RELATION
.
top
).
*
)
End
OPERATIONS
.
Record
analysis_hints
:=
mkanalysis_hints
{
hint_eq_catalog
:
PTree
.
t
equation
;
hint_eq_find_oracle
:
node
->
equation
->
option
eq_id
;
{
hint_eq_catalog
:
PTree
.
t
equation
_or_condition
;
hint_eq_find_oracle
:
node
->
equation
_or_condition
->
option
eq_id
;
hint_eq_rhs_oracle
:
node
->
sym_op
->
list
reg
->
PSet
.
t
}
.
Definition
context_from_hints
(
hints
:
analysis_hints
)
:=
...
...
backend/CSE3analysisaux.ml
View file @
e265be77
...
...
@@ -16,8 +16,15 @@ open HashedSet
open
Camlcoq
open
Coqlib
let
flatten_eq
eq
=
((
P
.
to_int
eq
.
eq_lhs
)
,
eq
.
eq_op
,
List
.
map
P
.
to_int
eq
.
eq_args
);;
type
flattened_equation_or_condition
=
|
Flat_equ
of
int
*
sym_op
*
int
list
|
Flat_cond
of
Op
.
condition
*
int
list
;;
let
flatten_eq
=
function
|
Equ
(
lhs
,
sop
,
args
)
->
Flat_equ
((
P
.
to_int
lhs
)
,
sop
,
(
List
.
map
P
.
to_int
args
))
|
Cond
(
cond
,
args
)
->
Flat_cond
(
cond
,
(
List
.
map
P
.
to_int
args
));;
let
imp_add_i_j
s
i
j
=
s
:=
PMap
.
set
i
(
PSet
.
add
j
(
PMap
.
get
i
!
s
))
!
s
;;
...
...
@@ -45,6 +52,9 @@ let print_eq channel (lhs, sop, args) =
Printf
.
printf
"%a = %s @ %a"
print_reg
lhs
(
string_of_chunk
chunk
)
(
PrintOp
.
print_addressing
print_reg
)
(
addr
,
args
);;
let
print_cond
channel
(
cond
,
args
)
=
Printf
.
printf
"cond %a"
(
PrintOp
.
print_condition
print_reg
)
(
cond
,
args
);;
let
pp_intset
oc
s
=
Printf
.
fprintf
oc
"{ "
;
List
.
iter
(
fun
i
->
Printf
.
fprintf
oc
"%d; "
(
P
.
to_int
i
))
(
PSet
.
elements
s
);
...
...
@@ -58,9 +68,14 @@ let pp_rhs oc (sop, args) =
(
PrintAST
.
name_of_chunk
chunk
)
(
PrintOp
.
print_addressing
PrintRTL
.
reg
)
(
addr
,
args
);;
let
pp_eq
oc
eq
=
Printf
.
fprintf
oc
"x%d = %a"
(
P
.
to_int
eq
.
eq_lhs
)
pp_rhs
(
eq
.
eq_op
,
eq
.
eq_args
);;
let
pp_eq
oc
eq_cond
=
match
eq_cond
with
|
Equ
(
lhs
,
sop
,
args
)
->
Printf
.
fprintf
oc
"x%d = %a"
(
P
.
to_int
lhs
)
pp_rhs
(
sop
,
args
)
|
Cond
(
cond
,
args
)
->
Printf
.
fprintf
oc
"cond %a"
(
PrintOp
.
print_condition
PrintRTL
.
reg
)
(
cond
,
args
);;
let
pp_P
oc
x
=
Printf
.
fprintf
oc
"%d"
(
P
.
to_int
x
)
...
...
@@ -68,8 +83,9 @@ let pp_option pp oc = function
|
None
->
output_string
oc
"none"
|
Some
x
->
pp
oc
x
;;
let
is_trivial
eq
=
(
eq
.
eq_op
=
SOp
Op
.
Omove
)
&&
(
eq
.
eq_args
=
[
eq
.
eq_lhs
]);;
let
is_trivial
=
function
|
Equ
(
lhs
,
(
SOp
Op
.
Omove
)
,
[
lhs'
])
->
lhs
=
lhs'
|
_
->
false
;;
let
rec
pp_list
separator
pp_item
chan
=
function
|
[]
->
()
...
...
@@ -86,7 +102,11 @@ let pp_equation hints chan x =
match
PTree
.
get
x
hints
.
hint_eq_catalog
with
|
None
->
output_string
chan
"???"
|
Some
eq
->
print_eq
chan
(
P
.
to_int
eq
.
eq_lhs
,
eq
.
eq_op
,
List
.
map
P
.
to_int
eq
.
eq_args
);;
match
eq
with
|
Equ
(
lhs
,
sop
,
args
)
->
print_eq
chan
(
P
.
to_int
lhs
,
sop
,
List
.
map
P
.
to_int
args
)
|
Cond
(
cond
,
args
)
->
print_cond
chan
(
cond
,
List
.
map
P
.
to_int
args
);;
let
pp_relation
hints
chan
rel
=
pp_set
"; "
(
pp_equation
hints
)
chan
rel
;;
...
...
@@ -114,19 +134,47 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t =
|
None
,
_
|
_
,
None
->
None
|
(
Some
x'
)
,
(
Some
y'
)
->
Some
(
RELATION
.
glb
x'
y'
);;
let
compute_invariants
(
nodes
:
RTL
.
node
list
)
(
entrypoint
:
RTL
.
node
)
(
tfr
:
RTL
.
node
->
RB
.
t
->
(
RTL
.
node
*
RB
.
t
)
list
)
=
let
todo
=
ref
IntSet
.
empty
and
invariants
=
ref
(
PMap
.
set
entrypoint
(
Some
RELATION
.
top
)
(
PMap
.
init
RB
.
bot
))
in
let
add_todo
(
pc
:
RTL
.
node
)
=
todo
:=
IntSet
.
add
(
P
.
to_int
pc
)
!
todo
in
let
update_node
(
pc
:
RTL
.
node
)
=
(
if
!
Clflags
.
option_debug_compcert
>
9
then
Printf
.
printf
"UP updating node %d
\n
"
(
P
.
to_int
pc
));
let
cur
=
PMap
.
get
pc
!
invariants
in
List
.
iter
(
fun
(
next_pc
,
next_contrib
)
->
let
previous
=
PMap
.
get
next_pc
!
invariants
in
let
next
=
RB
.
lub
previous
next_contrib
in
if
not
(
RB
.
beq
previous
next
)
then
(
invariants
:=
PMap
.
set
next_pc
next
!
invariants
;
add_todo
next_pc
))
(
tfr
pc
cur
)
in
add_todo
entrypoint
;
while
not
(
IntSet
.
is_empty
!
todo
)
do
let
nxt
=
IntSet
.
max_elt
!
todo
in
todo
:=
IntSet
.
remove
nxt
!
todo
;
update_node
(
P
.
of_int
nxt
)
done
;
!
invariants
;;
let
refine_invariants
(
nodes
:
RTL
.
node
list
)
(
entrypoint
:
RTL
.
node
)
(
successors
:
RTL
.
node
->
RTL
.
node
list
)
(
predecessors
:
RTL
.
node
->
RTL
.
node
list
)
(
tfr
:
RTL
.
node
->
RB
.
t
->
RB
.
t
)
(
invariants0
:
RB
.
t
PMap
.
t
)
=
(
tfr
:
RTL
.
node
->
RB
.
t
->
(
RTL
.
node
*
RB
.
t
)
list
)
(
invariants0
:
RB
.
t
PMap
.
t
)
=
let
todo
=
ref
IntSet
.
empty
and
invariants
=
ref
invariants0
in
let
add_todo
(
pc
:
RTL
.
node
)
=
todo
:=
IntSet
.
add
(
P
.
to_int
pc
)
!
todo
in
let
update_node
(
pc
:
RTL
.
node
)
=
(
if
!
Clflags
.
option_debug_compcert
>
9
then
Printf
.
printf
"updating node %d
\n
"
(
P
.
to_int
pc
));
then
Printf
.
printf
"
DOWN
updating node %d
\n
"
(
P
.
to_int
pc
));
if
not
(
peq
pc
entrypoint
)
then
let
cur
=
PMap
.
get
pc
!
invariants
in
...
...
@@ -134,7 +182,7 @@ let refine_invariants
(
List
.
map
(
fun
pred_pc
->
rb_glb
cur
(
tfr
pred_pc
(
PMap
.
get
pred_pc
!
invariants
)))
(
List
.
assoc
pc
(
tfr
pred_pc
(
PMap
.
get
pred_pc
!
invariants
)))
)
(
predecessors
pc
))
in
if
not
(
RB
.
beq
cur
nxt
)
then
...
...
@@ -156,6 +204,12 @@ let get_default default x ptree =
|
None
->
default
|
Some
y
->
y
;;
let
initial_analysis
ctx
tenv
(
f
:
RTL
.
coq_function
)
=
let
tfr
=
apply_instr'
ctx
tenv
f
.
RTL
.
fn_code
in
compute_invariants
(
List
.
map
fst
(
PTree
.
elements
f
.
RTL
.
fn_code
))
f
.
RTL
.
fn_entrypoint
tfr
;;
let
refine_analysis
ctx
tenv
(
f
:
RTL
.
coq_function
)
(
invariants0
:
RB
.
t
PMap
.
t
)
=
let
succ_map
=
RTL
.
successors_map
f
in
...
...
@@ -166,6 +220,13 @@ let refine_analysis ctx tenv
refine_invariants