Correctness of graph coloring.
Require Import SetoidList.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import RTLtyping.
Require Import Locations.
Require Import Conventions.
Require Import InterfGraph.
Require Import Coloring.
Correctness of the interference graph
We show that the interference graph built by interf_graph
is correct in the sense that it contains all conflict edges
that we need.
Many boring lemmas on the auxiliary functions used to construct
the interference graph follow. The lemmas are of two kinds:
the ``increasing'' lemmas show that the auxiliary functions only add
edges to the interference graph, but do not remove existing edges;
and the ``correct'' lemmas show that the auxiliary functions
correctly add the edges that we'd like them to add.
Lemma graph_incl_refl:
forall g,
graph_incl g g.
Proof.
intros; split; auto.
Qed.
Lemma add_interf_live_incl_aux:
forall (
filter:
reg ->
bool)
res live g,
graph_incl g
(
List.fold_left
(
fun g r =>
if filter r then add_interf r res g else g)
live g).
Proof.
Lemma add_interf_live_incl:
forall (
filter:
reg ->
bool)
res live g,
graph_incl g (
add_interf_live filter res live g).
Proof.
Lemma add_interf_live_correct_aux:
forall filter res r live,
InA Regset.E.eq r live ->
filter r =
true ->
forall g,
interfere r res
(
List.fold_left
(
fun g r =>
if filter r then add_interf r res g else g)
live g).
Proof.
Lemma add_interf_live_correct:
forall filter res live g r,
Regset.In r live ->
filter r =
true ->
interfere r res (
add_interf_live filter res live g).
Proof.
Lemma add_interf_op_incl:
forall res live g,
graph_incl g (
add_interf_op res live g).
Proof.
Lemma add_interf_op_correct:
forall res live g r,
Regset.In r live ->
r <>
res ->
interfere r res (
add_interf_op res live g).
Proof.
Lemma add_interf_move_incl:
forall arg res live g,
graph_incl g (
add_interf_move arg res live g).
Proof.
Lemma add_interf_move_correct:
forall arg res live g r,
Regset.In r live ->
r <>
arg ->
r <>
res ->
interfere r res (
add_interf_move arg res live g).
Proof.
Lemma add_interf_destroyed_incl_aux_1:
forall mr live g,
graph_incl g
(
List.fold_left (
fun g r =>
add_interf_mreg r mr g)
live g).
Proof.
Lemma add_interf_destroyed_incl_aux_2:
forall mr live g,
graph_incl g
(
Regset.fold (
fun r g =>
add_interf_mreg r mr g)
live g).
Proof.
Lemma add_interf_destroyed_incl:
forall live destroyed g,
graph_incl g (
add_interf_destroyed live destroyed g).
Proof.
Lemma add_interfs_indirect_call_incl:
forall rfun locs g,
graph_incl g (
add_interfs_indirect_call rfun locs g).
Proof.
Lemma add_interfs_call_incl:
forall ros locs g,
graph_incl g (
add_interf_call ros locs g).
Proof.
Lemma interfere_incl:
forall r1 r2 g1 g2,
graph_incl g1 g2 ->
interfere r1 r2 g1 ->
interfere r1 r2 g2.
Proof.
unfold graph_incl; intros. elim H; auto.
Qed.
Lemma interfere_mreg_incl:
forall r1 r2 g1 g2,
graph_incl g1 g2 ->
interfere_mreg r1 r2 g1 ->
interfere_mreg r1 r2 g2.
Proof.
unfold graph_incl; intros. elim H; auto.
Qed.
Lemma add_interf_destroyed_correct_aux_1:
forall mr r live,
InA Regset.E.eq r live ->
forall g,
interfere_mreg r mr
(
List.fold_left (
fun g r =>
add_interf_mreg r mr g)
live g).
Proof.
Lemma add_interf_destroyed_correct_aux_2:
forall mr live g r,
Regset.In r live ->
interfere_mreg r mr
(
Regset.fold (
fun r g =>
add_interf_mreg r mr g)
live g).
Proof.
Lemma add_interf_destroyed_correct:
forall live destroyed g r mr,
Regset.In r live ->
In mr destroyed ->
interfere_mreg r mr (
add_interf_destroyed live destroyed g).
Proof.
Lemma add_interfs_indirect_call_correct:
forall rfun mr locs g,
In (
R mr)
locs ->
interfere_mreg rfun mr (
add_interfs_indirect_call rfun locs g).
Proof.
Lemma add_interfs_call_correct:
forall rfun locs g mr,
In (
R mr)
locs ->
interfere_mreg rfun mr (
add_interf_call (
inl _ rfun)
locs g).
Proof.
Lemma add_prefs_call_incl:
forall args locs g,
graph_incl g (
add_prefs_call args locs g).
Proof.
Lemma add_prefs_builtin_incl:
forall ef args res g,
graph_incl g (
add_prefs_builtin ef args res g).
Proof.
Lemma add_interf_entry_incl:
forall params live g,
graph_incl g (
add_interf_entry params live g).
Proof.
Lemma add_interf_entry_correct:
forall params live g r1 r2,
In r1 params ->
Regset.In r2 live ->
r1 <>
r2 ->
interfere r1 r2 (
add_interf_entry params live g).
Proof.
Lemma add_interf_params_incl_aux:
forall p1 pl g,
graph_incl g
(
List.fold_left
(
fun g r =>
if Reg.eq r p1 then g else add_interf r p1 g)
pl g).
Proof.
Lemma add_interf_params_incl:
forall pl g,
graph_incl g (
add_interf_params pl g).
Proof.
Lemma add_interf_params_correct_aux:
forall p1 pl g p2,
In p2 pl ->
p1 <>
p2 ->
interfere p1 p2
(
List.fold_left
(
fun g r =>
if Reg.eq r p1 then g else add_interf r p1 g)
pl g).
Proof.
Lemma add_interf_params_correct:
forall pl g r1 r2,
In r1 pl ->
In r2 pl ->
r1 <>
r2 ->
interfere r1 r2 (
add_interf_params pl g).
Proof.
Lemma add_edges_instr_incl:
forall sig instr live g,
graph_incl g (
add_edges_instr sig instr live g).
Proof.
The proposition below states that graph g contains
all the conflict edges expected for instruction instr.
Definition correct_interf_instr
(
live:
Regset.t) (
instr:
instruction) (
g:
graph) :
Prop :=
match instr with
|
Iop op args res s =>
match is_move_operation op args with
|
Some arg =>
forall r,
Regset.In res live ->
Regset.In r live ->
r <>
res ->
r <>
arg ->
interfere r res g
|
None =>
forall r,
Regset.In res live ->
Regset.In r live ->
r <>
res ->
interfere r res g
end
|
Iload chunk addr args res s =>
forall r,
Regset.In res live ->
Regset.In r live ->
r <>
res ->
interfere r res g
|
Icall sig ros args res s =>
(
forall r mr,
Regset.In r live ->
In mr destroyed_at_call_regs ->
r <>
res ->
interfere_mreg r mr g)
/\ (
forall r,
Regset.In r live ->
r <>
res ->
interfere r res g)
/\ (
match ros with
|
inl rfun =>
forall mr,
In (
R mr) (
loc_arguments sig) ->
interfere_mreg rfun mr g
|
inr idfun =>
True
end)
|
Itailcall sig ros args =>
match ros with
|
inl rfun =>
forall mr,
In (
R mr) (
loc_arguments sig) ->
interfere_mreg rfun mr g
|
inr idfun =>
True
end
|
Ibuiltin ef args res s =>
forall r,
Regset.In r live ->
r <>
res ->
interfere r res g
|
_ =>
True
end.
Lemma correct_interf_instr_incl:
forall live instr g1 g2,
graph_incl g1 g2 ->
correct_interf_instr live instr g1 ->
correct_interf_instr live instr g2.
Proof.
Lemma add_edges_instr_correct:
forall sig instr live g,
correct_interf_instr live instr (
add_edges_instr sig instr live g).
Proof.
Lemma add_edges_instrs_correct:
forall f live pc i,
f.(
fn_code)!
pc =
Some i ->
correct_interf_instr live!!
pc i (
add_edges_instrs f live).
Proof.
Here are the three correctness properties of the generated
inference graph. First, it contains the conflict edges
needed by every instruction of the function.
Lemma interf_graph_correct_1:
forall f live live0 pc i,
f.(
fn_code)!
pc =
Some i ->
correct_interf_instr live!!
pc i (
interf_graph f live live0).
Proof.
Second, function parameters conflict pairwise.
Lemma interf_graph_correct_2:
forall f live live0 r1 r2,
In r1 f.(
fn_params) ->
In r2 f.(
fn_params) ->
r1 <>
r2 ->
interfere r1 r2 (
interf_graph f live live0).
Proof.
Third, function parameters conflict pairwise with pseudo-registers
live at function entry. If the function never uses a pseudo-register
before it is defined, pseudo-registers live at function entry
are a subset of the function parameters and therefore this condition
is implied by interf_graph_correct_3. However, we prefer not
to make this assumption.
Lemma interf_graph_correct_3:
forall f live live0 r1 r2,
In r1 f.(
fn_params) ->
Regset.In r2 live0 ->
r1 <>
r2 ->
interfere r1 r2 (
interf_graph f live live0).
Proof.
Correctness of the a priori checks over the result of graph coloring
We now show that the checks performed over the candidate coloring
returned by graph_coloring are correct: candidate colorings that
pass these checks are indeed correct colorings.
Section CORRECT_COLORING.
Variable g:
graph.
Variable env:
regenv.
Variable allregs:
Regset.t.
Variable coloring:
reg ->
loc.
Lemma check_coloring_1_correct:
forall r1 r2,
check_coloring_1 g coloring =
true ->
SetRegReg.In (
r1,
r2)
g.(
interf_reg_reg) ->
coloring r1 <>
coloring r2.
Proof.
Lemma check_coloring_2_correct:
forall r1 mr2,
check_coloring_2 g coloring =
true ->
SetRegMreg.In (
r1,
mr2)
g.(
interf_reg_mreg) ->
coloring r1 <>
R mr2.
Proof.
Lemma same_typ_correct:
forall t1 t2,
same_typ t1 t2 =
true ->
t1 =
t2.
Proof.
destruct t1; destruct t2; simpl; congruence.
Qed.
Lemma loc_is_acceptable_correct:
forall l,
loc_is_acceptable l =
true ->
loc_acceptable l.
Proof.
destruct l;
unfold loc_is_acceptable,
loc_acceptable.
case (
In_dec Loc.eq (
R m)
temporaries);
intro.
intro;
discriminate.
auto.
destruct s.
case (
zlt z 0);
intro.
intro;
discriminate.
auto.
intro;
discriminate.
intro;
discriminate.
Qed.
Lemma check_coloring_3_correct:
forall r,
check_coloring_3 allregs env coloring =
true ->
Regset.mem r allregs =
true ->
loc_acceptable (
coloring r) /\
env r =
Loc.type (
coloring r).
Proof.
End CORRECT_COLORING.
Correctness of clipping
We then show the correctness of the ``clipped'' coloring
returned by alloc_of_coloring applied to a candidate coloring
that passes the a posteriori checks.
Section ALLOC_OF_COLORING.
Variable g:
graph.
Variable env:
regenv.
Let allregs :=
all_interf_regs g.
Variable coloring:
reg ->
loc.
Let alloc :=
alloc_of_coloring coloring env allregs.
Lemma alloc_of_coloring_correct_1:
forall r1 r2,
check_coloring g env allregs coloring =
true ->
SetRegReg.In (
r1,
r2)
g.(
interf_reg_reg) ->
alloc r1 <>
alloc r2.
Proof.
Lemma alloc_of_coloring_correct_2:
forall r1 mr2,
check_coloring g env allregs coloring =
true ->
SetRegMreg.In (
r1,
mr2)
g.(
interf_reg_mreg) ->
alloc r1 <>
R mr2.
Proof.
Lemma alloc_of_coloring_correct_3:
forall r,
check_coloring g env allregs coloring =
true ->
loc_acceptable (
alloc r).
Proof.
unfold check_coloring,
alloc,
alloc_of_coloring;
intros.
elim (
andb_prop _ _ H);
intros.
elim (
andb_prop _ _ H1);
intros.
caseEq (
Regset.mem r allregs);
intro.
generalize (
check_coloring_3_correct _ _ _ r H3 H4).
tauto.
case (
env r);
simpl.
unfold dummy_int_reg.
intuition congruence.
unfold dummy_float_reg.
intuition congruence.
Qed.
Lemma alloc_of_coloring_correct_4:
forall r,
check_coloring g env allregs coloring =
true ->
env r =
Loc.type (
alloc r).
Proof.
End ALLOC_OF_COLORING.
Correctness of the whole graph coloring algorithm
Combining results from the previous sections, we now summarize
the correctness properties of the assignment (of locations to
registers) returned by regalloc.
Definition correct_alloc_instr
(
live:
PMap.t Regset.t) (
alloc:
reg ->
loc)
(
pc:
node) (
instr:
instruction) :
Prop :=
match instr with
|
Iop op args res s =>
match is_move_operation op args with
|
Some arg =>
forall r,
Regset.In res live!!
pc ->
Regset.In r live!!
pc ->
r <>
res ->
r <>
arg ->
alloc r <>
alloc res
|
None =>
forall r,
Regset.In res live!!
pc ->
Regset.In r live!!
pc ->
r <>
res ->
alloc r <>
alloc res
end
|
Iload chunk addr args res s =>
forall r,
Regset.In res live!!
pc ->
Regset.In r live!!
pc ->
r <>
res ->
alloc r <>
alloc res
|
Icall sig ros args res s =>
(
forall r,
Regset.In r live!!
pc ->
r <>
res ->
~(
In (
alloc r)
destroyed_at_call))
/\ (
forall r,
Regset.In r live!!
pc ->
r <>
res ->
alloc r <>
alloc res)
/\ (
match ros with
|
inl rfun => ~(
In (
alloc rfun) (
loc_arguments sig))
|
inr idfun =>
True
end)
|
Itailcall sig ros args =>
(
match ros with
|
inl rfun => ~(
In (
alloc rfun) (
loc_arguments sig))
|
inr idfun =>
True
end)
|
Ibuiltin ef args res s =>
forall r,
Regset.In r live!!
pc ->
r <>
res ->
alloc r <>
alloc res
|
_ =>
True
end.
Section REGALLOC_PROPERTIES.
Variable f:
function.
Variable env:
regenv.
Variable live:
PMap.t Regset.t.
Variable live0:
Regset.t.
Variable alloc:
reg ->
loc.
Let g :=
interf_graph f live live0.
Let allregs :=
all_interf_regs g.
Let coloring :=
graph_coloring f g env allregs.
Lemma regalloc_ok:
regalloc f live live0 env =
Some alloc ->
check_coloring g env allregs coloring =
true /\
alloc =
alloc_of_coloring coloring env allregs.
Proof.
Lemma regalloc_acceptable:
forall r,
regalloc f live live0 env =
Some alloc ->
loc_acceptable (
alloc r).
Proof.
Lemma regsalloc_acceptable:
forall rl,
regalloc f live live0 env =
Some alloc ->
locs_acceptable (
List.map alloc rl).
Proof.
Lemma regalloc_preserves_types:
forall r,
regalloc f live live0 env =
Some alloc ->
Loc.type (
alloc r) =
env r.
Proof.
Lemma correct_interf_alloc_instr:
forall pc instr,
(
forall r1 r2,
interfere r1 r2 g ->
alloc r1 <>
alloc r2) ->
(
forall r1 mr2,
interfere_mreg r1 mr2 g ->
alloc r1 <>
R mr2) ->
(
forall r,
loc_acceptable (
alloc r)) ->
correct_interf_instr live!!
pc instr g ->
correct_alloc_instr live alloc pc instr.
Proof.
intros pc instr ALL1 ALL2 ALL3.
unfold correct_interf_instr,
correct_alloc_instr;
destruct instr;
auto.
destruct (
is_move_operation o l);
auto.
intros [
A [
B C]].
split.
intros;
red;
intros.
unfold destroyed_at_call in H1.
generalize (
list_in_map_inv R _ _ H1).
intros [
mr [
EQ IN]].
generalize (
A r0 mr H IN H0).
intro.
generalize (
ALL2 _ _ H2).
contradiction.
split.
auto.
destruct s0;
auto.
red;
intros.
generalize (
ALL3 r0).
generalize (
loc_arguments_acceptable _ _ H).
unfold loc_argument_acceptable,
loc_acceptable.
caseEq (
alloc r0).
intros.
elim (
ALL2 r0 m).
apply C;
auto.
congruence.
auto.
destruct s0;
auto.
destruct s0;
auto.
red;
intros.
generalize (
ALL3 r).
generalize (
loc_arguments_acceptable _ _ H0).
unfold loc_argument_acceptable,
loc_acceptable.
caseEq (
alloc r).
intros.
elim (
ALL2 r m).
apply H;
auto.
congruence.
auto.
destruct s0;
auto.
Qed.
Lemma regalloc_correct_1:
forall pc instr,
regalloc f live live0 env =
Some alloc ->
f.(
fn_code)!
pc =
Some instr ->
correct_alloc_instr live alloc pc instr.
Proof.
Lemma regalloc_correct_2:
regalloc f live live0 env =
Some alloc ->
list_norepet f.(
fn_params) ->
list_norepet (
List.map alloc f.(
fn_params)).
Proof.
Lemma regalloc_correct_3:
forall r1 r2,
regalloc f live live0 env =
Some alloc ->
In r1 f.(
fn_params) ->
Regset.In r2 live0 ->
r1 <>
r2 ->
alloc r1 <>
alloc r2.
Proof.
End REGALLOC_PROPERTIES.