Require Import MoreRTL Util.
Require Import Sorting.Mergesort.
Require Kildall.
Require Liveness.
Import Utf8.
Import Coqlib Maps.
Import Registers RTL.
Module NodeOrder :
Orders.TotalLeBool'
with Definition t :=
node.
Definition t :=
node.
Definition leb x y :=
match (
x ?=
y)%
positive with
|
Eq |
Gt =>
true
|
Lt =>
false
end.
Lemma leb_total x y :
leb x y =
true ∨
leb y x =
true.
Proof.
End NodeOrder.
Module Import NodeSort :=
Sort NodeOrder.
Definition list_of_set (
n:
node_set) :
list node :=
sort (
List.map fst (
PTree.elements n)).
Module RegOrder :
Orders.TotalLeBool'
with Definition t :=
reg.
Definition t :=
reg.
Definition leb :=
Pos.leb.
Lemma leb_total x y :
leb x y =
true ∨
leb y x =
true.
Proof.
End RegOrder.
Module Import RegSort :=
Sort RegOrder.
Definition list_of_regset (
s:
Regset.t) :
list reg :=
sort (
Regset.elements s).
Given two RTL functions, computes some relational annotations.
Definition rel :
Type :=
list (
reg *
reg).
Fixpoint drop {
A B} (
a:
list A) (
b:
list B) :
list B :=
match a,
b with
|
_ ::
a,
_ ::
b =>
drop a b
|
_,
_ =>
b
end.
Definition relate_regsets (
x y:
Regset.t) :
rel :=
let a :=
list_of_regset x in
let b :=
list_of_regset y in
fold_left2
(λ
r p q, (
p,
q) ::
r)
(λ
r p,
drop p r)
(λ
r q,
drop q r)
a
b
nil.
Definition guess (
p q:
RTL.function) :
list ((
node *
node) *
rel) * (
node ->
list node) * (
node ->
list node) :=
let predMp :=
Kildall.make_predecessors p.(
fn_code)
RTL.successors_instr in
let predMq :=
Kildall.make_predecessors q.(
fn_code)
RTL.successors_instr in
let pred M pc :=
match M !
pc with Some x =>
x |
None =>
nil end in
let predp :=
pred predMp in
let predq :=
pred predMq in
let livep :=
Liveness.analyze p in
let liveq :=
Liveness.analyze q in
let get_live f P M :=
match M with
|
None => (λ
_,
Regset.empty)
|
Some live =>
λ
pc,
Liveness.transfer f pc (
live !!
pc)
end
in
let bep :=
list_of_set (
back_edges p.(
fn_code))
in
let beq :=
list_of_set (
back_edges q.(
fn_code))
in
let res :=
fold_left2
(λ
r pcp pcq,
((
pcp,
pcq),
relate_regsets (
get_live p predp livep pcp) (
get_live q predq liveq pcq)) ::
r
)
(λ
_ _,
nil)
(λ
_ _,
nil)
bep
beq
nil
in (
res,
predp,
predq).