This is the liveness analysis over RTL that is used by the SSA
generation algorithm. This is based on the liveness analysis
already provided by CompCert. We adapt it so that it resemble more
the traditional liveness analysis, and that it fulfills the
requirements we demand on liveness information.
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import RTLdfs.
Require Import Kildall.
Require Import Locations.
Require Import Conventions.
Require Import RTLutils.
Unset Allow StrictProp.
Liveness analysis over RTL
Notation reg_live :=
Regset.add.
Notation reg_dead :=
Regset.remove.
Definition reg_option_live (
or:
option reg) (
lv:
Regset.t) :=
match or with None =>
lv |
Some r =>
reg_live r lv end.
Definition reg_sum_live (
ros:
reg +
ident) (
lv:
Regset.t) :=
match ros with inl r =>
reg_live r lv |
inr s =>
lv end.
Fixpoint reg_list_live
(
rl:
list reg) (
lv:
Regset.t) {
struct rl} :
Regset.t :=
match rl with
|
nil =>
lv
|
r1 ::
rs =>
reg_list_live rs (
reg_live r1 lv)
end.
Definition transfer
(
f:
RTLdfs.function) (
pc:
RTL.node) (
after:
Regset.t) :
Regset.t :=
match f.(
fn_code)!
pc with
|
None =>
Regset.empty
|
Some i =>
match i with
|
RTL.Inop s =>
after
|
RTL.Iop op args res s =>
reg_list_live args (
reg_dead res after)
|
RTL.Iload chunk addr args dst s =>
reg_list_live args (
reg_dead dst after)
|
RTL.Istore chunk addr args src s =>
reg_list_live args (
reg_live src after)
|
RTL.Icall sig ros args res s =>
reg_list_live args
(
reg_sum_live ros (
reg_dead res after))
|
RTL.Itailcall sig ros args =>
reg_list_live args (
reg_sum_live ros Regset.empty)
|
RTL.Ibuiltin ef args (
BR res)
s =>
reg_list_live (
params_of_builtin_args args) (
reg_dead res after)
|
RTL.Ibuiltin ef args _ s =>
reg_list_live (
params_of_builtin_args args)
after
|
RTL.Icond cond args ifso ifnot =>
reg_list_live args after
|
RTL.Ijumptable arg tbl =>
reg_live arg after
|
RTL.Ireturn optarg =>
reg_option_live optarg Regset.empty
end
end.
The liveness analysis is then obtained by instantiating the
general framework for backward dataflow analysis provided by
module Kildall.
Module RegsetLat :=
LFSet(
Regset).
Module DS :=
Backward_Dataflow_Solver(
RegsetLat)(
NodeSetBackward).
Definition analyze (
f:
function):
option (
PMap.t Regset.t) :=
DS.fixpoint f.(
fn_code)
successors_instr (
transfer f).
Well-formedness condition for a liveness analysis
Section WF_LIVE.
Variable f:
RTLdfs.function.
Definition Lin := (
fun pc live_out => (
transfer f pc (
live_out pc))).
Definition Lout {
A:
Type} := (
fun (
live:
PMap.t A)
pc =>
live #
pc).
Record wf_live (
live_out:
positive ->
Regset.t):=
MK_WF_LIVE {
wf_live_incl :
forall pc pc'
x,
rtl_cfg f pc pc' ->
Regset.In x (
Lin pc'
live_out) ->
(
Regset.In x (
Lin pc live_out) \/
RTLutils.assigned_code_spec (
RTLdfs.fn_code f)
pc x) ;
wf_live_use :
forall pc x,
use_rtl_code f x pc -> (
Regset.In x (
Lin pc live_out))
}.
Auxiliary lemmas about analyze
Lemma reg_list_live_incl :
forall x l s,
Regset.In x s ->
Regset.In x (
reg_list_live l s).
Proof.
induction l ;
intros ;
simpl ;
auto.
eapply IHl ;
eauto.
eapply Regset.add_2 ;
eauto.
Qed.
Lemma reg_list_live_incl_2 :
forall x l s,
In x l ->
Regset.In x (
reg_list_live l s).
Proof.
Hint Constructors RTLutils.assigned_code_spec:
core.
Lemma live_incl :
forall live,
analyze f =
Some live ->
forall pc pc'
x,
rtl_cfg f pc pc' ->
Regset.In x (
Lin pc' (
Lout live)) ->
Regset.In x (
Lin pc (
Lout live)) \/
RTLutils.assigned_code_spec (
RTLdfs.fn_code f)
pc x.
Proof.
Lemma live_use :
forall live,
analyze f =
Some live ->
forall pc x,
use_rtl_code f x pc ->
Regset.In x (
Lin pc (
Lout live)).
Proof.
analyze is well-formed with regards to wf_live
Lemma live_wf_live :
forall live,
analyze f =
Some live ->
wf_live (
Lout live).
Proof.
End WF_LIVE.
Global Hint Constructors wf_live:
core.