Definitions used by RTLReaches.
Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Registers.
Require Import Op.
Require Import RTL.
Require Import Kildall.
Require Import Utils.
The cfg predicate
Inductive cfg (
code:
code) (
i j:
node) :
Prop :=
|
CFG :
forall ins
(
HCFG_ins:
code!
i =
Some ins)
(
HCFG_in :
In j (
successors_instr ins)),
cfg code i j.
Inductive cfg_star (
code:
code) (
i:
node) :
node ->
Prop :=
|
cfg_star0 :
cfg_star code i i
|
cfg_star1 :
forall j k,
cfg_star code i j ->
cfg code j k ->
cfg_star code i k.
Lemma cfg_star_same :
forall code i j,
cfg_star code i j <-> (
cfg code)**
i j.
Proof.
split.
induction 1.
constructor 2.
constructor 3
with j;
auto.
assert (
forall i j, (
cfg code**)
i j ->
forall k,
cfg_star code k i ->
cfg_star code k j).
clear i j;
induction 1;
auto.
intros.
constructor 2
with x;
auto.
intros;
apply H with i;
auto.
constructor 1.
Qed.
Lemma cfg_star_same_code:
forall code1 code2 i,
(
forall k,
cfg_star code1 i k ->
code1!
k =
code2!
k) ->
forall j,
cfg_star code1 i j ->
cfg_star code2 i j.
Proof.
induction 2.
constructor 1.
constructor 2 with j; auto.
inv H1.
rewrite H in *; auto.
econstructor; eauto.
Qed.
Ltac simpl_succs :=
match goal with
| [
H1 : (
RTL.fn_code ?
f) ! ?
pc =
Some _ |-
_ ] =>
unfold successors_list,
RTL.successors ;
rewrite PTree.gmap1 ;
(
rewrite H1;
simpl;
auto)
end.
Lemma rtl_cfg_succs :
forall f pc pc',
cfg (
fn_code f)
pc pc' ->
In pc' (
RTL.successors f) !!!
pc.
Proof.
intros.
inv H.
unfold successors_list,
RTL.successors.
rewrite PTree.gmap1.
unfold option_map.
rewrite HCFG_ins ;
auto.
Qed.
Hint Resolve rtl_cfg_succs.
Hint Extern 4 (
In _ (
successors_instr _)) =>
simpl successors_instr.
Hint Constructors cfg.
Lemmas about successors and make_predecessors
Lemma succ_code_incl :
forall f1 f2,
(
forall i ins, (
RTL.fn_code f1)!
i =
Some ins -> (
RTL.fn_code f2)!
i =
Some ins) ->
forall i,
incl ((
RTL.successors f1)!!!
i) ((
RTL.successors f2)!!!
i).
Proof.
intros.
unfold successors_list.
unfold RTL.successors.
repeat rewrite PTree.gmap1.
case_eq ((
RTL.fn_code f1) !
i);
simpl;
intros.
rewrite (
H _ _ H0);
simpl.
intro;
auto.
intro;
simpl;
intuition.
Qed.
Lemma add_successors_correct_inv:
forall tolist from pred n s,
In n (
add_successors pred from tolist)!!!
s ->
In n pred!!!
s \/ (
n =
from /\
In s tolist).
Proof.
induction tolist;
simpl;
intros.
tauto.
elim IHtolist with (1:=
H);
eauto.
unfold successors_list at 1.
rewrite PTree.gsspec.
destruct (
peq s a).
subst a.
simpl.
destruct 1.
auto with coqlib.
auto.
fold (
successors_list pred s).
intuition congruence.
intuition congruence.
Qed.
Lemma make_predecessors_correct_inv:
forall m n s,
In n (
make_predecessors m)!!!
s ->
In s m !!!
n.
Proof.
set (
P :=
fun pred succ =>
forall s n,
In s succ!!!
n ->
In n pred!!!
s).
unfold make_predecessors.
intros m.
apply PTree_Properties.fold_rec with (
P:=
P).
unfold P;
unfold successors_list;
intros.
rewrite <-
H.
auto.
red;
unfold successors_list.
intros n s.
repeat rewrite PTree.gempty.
auto.
unfold P;
intros.
elim add_successors_correct_inv with (1:=
H2);
auto;
intros.
unfold successors_list.
rewrite PTree.gsspec.
destruct (
peq s k).
subst.
generalize (
H1 _ _ H3).
unfold successors_list;
rewrite H;
simpl;
intuition.
fold (
successors_list m0 s).
auto.
unfold successors_list.
rewrite PTree.gsspec.
destruct (
peq s k).
subst;
intuition.
intuition.
Qed.
Lemma make_predecessors_incl :
forall m1 m2,
(
forall i,
incl (
m1!!!
i) (
m2!!!
i)) ->
(
forall i,
incl (
make_predecessors m1)!!!
i (
make_predecessors m2)!!!
i).
Proof.