Require Import Coqlib.
Require Import Iteration.
Require Import Maps.
Require Import Lattice.
Require Import Kildall.
Require Import KildallComp.
Module Backward_Dataflow_Solver (
LAT:
SEMILATTICE) (
NS:
NODE_SET)<:
BACKWARD_DATAFLOW_SOLVER with Module L :=
LAT.
Module L :=
LAT.
Module DS :=
Dataflow_Solver L NS.
Section Kildall.
Context {
A:
Type}.
Variable code:
PTree.t A.
Variable successors:
A ->
list positive.
Variable transf:
positive ->
L.t ->
L.t.
Finding entry points for the reverse control-flow graph.
Section Exit_points.
Assuming that the nodes of the CFG code are numbered in reverse
postorder (cf. pass Renumber), an edge from n to s is a
normal edge if s < n and a back-edge otherwise.
sequential_node returns true if the given node has at least one
normal outgoing edge. It returns false if the given node is an exit
node (no outgoing edges) or the final node of a loop body
(all outgoing edges are back-edges). As we prove later, the set
of all non-sequential node is an appropriate set of entry points
for exploring the reverse CFG.
Definition sequential_node (
pc:
positive) (
instr:
A):
bool :=
existsb (
fun s =>
match code!
s with None =>
false |
Some _ =>
plt s pc end)
(
successors instr).
Definition exit_points :
NS.t :=
PTree.fold
(
fun ep pc instr =>
if sequential_node pc instr
then ep
else NS.add pc ep)
code NS.empty.
Lemma exit_points_charact:
forall n,
NS.In n exit_points <->
exists i,
code!
n =
Some i /\
sequential_node n i =
false.
Proof.
intros n.
unfold exit_points.
eapply PTree_Properties.fold_rec.
-
intros.
rewrite <-
H.
auto.
-
simpl.
split;
intros.
eelim NS.empty_spec;
eauto.
destruct H as [
i [
P Q]].
rewrite PTree.gempty in P.
congruence.
-
intros.
destruct (
sequential_node k v)
eqn:
SN.
+
rewrite H1.
rewrite PTree.gsspec.
destruct (
peq n k).
subst.
split;
intros [
i [
P Q]].
congruence.
inv P.
congruence.
tauto.
+
rewrite NS.add_spec.
rewrite H1.
rewrite PTree.gsspec.
destruct (
peq n k).
subst.
split.
intros.
exists v;
auto.
auto.
split.
intros [
P | [
i [
P Q]]].
congruence.
exists i;
auto.
intros [
i [
P Q]].
right;
exists i;
auto.
Qed.
Lemma reachable_exit_points:
forall pc i,
code!
pc =
Some i ->
exists x,
NS.In x exit_points /\
reachable code successors pc x.
Proof.
The crucial property of exit points is that any nonempty node in the
CFG is reverse-reachable from an exit point.
Lemma reachable_exit_points_predecessor:
forall pc i,
code!
pc =
Some i ->
exists x,
NS.In x exit_points /\
reachable (
make_predecessors code successors) (
fun l =>
l)
x pc.
Proof.
End Exit_points.
The efficient backward solver.
Definition fixpoint :=
DS.fixpoint_nodeset
(
make_predecessors code successors) (
fun l =>
l)
transf exit_points.
Theorem fixpoint_solution:
forall res n instr s,
fixpoint =
Some res ->
code!
n =
Some instr ->
In s (
successors instr) ->
(
forall n a,
code!
n =
None ->
L.eq (
transf n a)
L.bot) ->
L.ge res!!
n (
transf s res!!
s).
Proof.
The alternate solver that starts with all nodes of the CFG instead
of just the exit points.
Definition fixpoint_allnodes :=
DS.fixpoint_allnodes
(
make_predecessors code successors) (
fun l =>
l)
transf.
Theorem fixpoint_allnodes_solution:
forall res n instr s,
fixpoint_allnodes =
Some res ->
code!
n =
Some instr ->
In s (
successors instr) ->
L.ge res!!
n (
transf s res!!
s).
Proof.
Lemma propagate_succ_no_succ :
forall s out n pc,
pc <>
n ->
(
DS.propagate_succ s out n).(
DS.aval) !
pc =
s.(
DS.aval) !
pc.
Proof.
Lemma propagate_succ_list_no_succ :
forall s out l pc,
~
In pc l ->
(
DS.propagate_succ_list s out l).(
DS.aval) !
pc =
s.(
DS.aval) !
pc.
Proof.
intros s out l.
revert s.
induction l;
intros.
-
simpl.
reflexivity.
-
simpl.
rewrite IHl.
apply propagate_succ_no_succ.
intros contra.
apply H.
left.
congruence.
intros contra.
apply H.
right.
assumption.
Qed.
Theorem fixpoint_no_succ :
forall res pc i,
fixpoint =
Some res ->
code !
pc =
Some i ->
successors i =
nil ->
L.eq res!!
pc L.bot.
Proof.
Theorem fixpoint_some :
forall res pc,
fixpoint =
Some res ->
code !
pc =
None ->
L.eq res!!
pc L.bot.
Proof.
End Kildall.
End Backward_Dataflow_Solver.