Proof of CFG preservation by the program slicing.
Require Import Program.
Require Import Coqlib.
Require Import RTL.
Require Import Maps.
Require Import Errors.
Require Import Registers.
Require Import UtilTacs.
Require Import UtilBase.
Require Import RTLPaths.
Require Import SliceGen.
Require Import Scope.
Section CFG.
Variable f :
function.
Variable fsc :
Scope.family f.
Variable exit_n :
node.
Variable reg_vint :
reg.
Variable nc :
node.
Variable tf :
function.
Variable of :
obs_function.
Hypothesis FOK:
slice_function f nc fsc exit_n reg_vint =
OK (
tf,
of).
Lemma succs_update_succs_icond:
forall n s1 s2 dobs dexit n',
In n' (
successors_instr (
update_succs_icond (
_reg_vint of)
n s1 s2 dobs dexit)) ->
In n' (
s1 ::
s2 ::
nil).
Proof.
intros.
unfold successors_instr in H.
unfold update_succs_icond in H.
optDec H; optDec H; optDec H; destruct_pairs; try optDec H; try optDec H; inv H; auto.
Qed.
Lemma in_update_succs_icond:
forall n s1 s2 dobs dexit n',
In n' (
successors_instr (
update_succs_icond (
_reg_vint of)
n s1 s2 dobs dexit)) <->
In n' (
s1 ::
s2 ::
nil).
Proof.
intros.
split;
intros.
eapply succs_update_succs_icond;
eauto.
unfold successors_instr.
unfold update_succs_icond.
optDecG;
optDecG;
optDecG;
destruct_pairs;
try optDecG;
try optDecG;
auto.
Qed.
Lemma inst_succ_in:
forall f n s i
(
SUCC:
succ_node f n s)
(
INST: (
fn_code f) !
n =
Some i),
match i with
|
Inop n =>
s =
n
|
Iop _ _ _ n =>
s =
n
|
Iload _ _ _ _ n =>
s =
n
|
Istore _ _ _ _ n =>
s =
n
|
Icall _ _ _ _ n =>
s =
n
|
Itailcall _ _ _ =>
False
|
Ibuiltin _ _ _ n =>
s =
n
|
Icond _ _ n n' =>
s =
n \/
s =
n'
|
Ijumptable _ tbl =>
In s tbl
|
Ireturn _ =>
False
end.
Proof.
intros.
unfolds in SUCC.
decs SUCC.
rewrite H0 in INST.
inv INST.
destruct i; simpls; try inv H1; trim.
inv H; trim.
Qed.
Lemma transf_entry:
tf.(
fn_entrypoint) =
f.(
fn_entrypoint).
Proof.
unfolds in FOK.
monadInv FOK;
auto.
Qed.
Ltac UnOf FOK EQ EQ1 DOBS RVS SCEX :=
monadInv FOK;
monadInv EQ;
optDecN EQ1 DOBS;
trim;
optDecN EQ1 RVS;
trim;
optDecN EQ1 SCEX;
trim.
Lemma transf_f_In:
forall n,
f_In n tf ->
f_In n f.
Proof.
intros.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
inv EQ1.
simpls.
unfold f_In in *.
case_eq ((
fn_code f) !
n);
trim.
unfold compute_bs,
compute_bs_code in H.
simpls.
rewrite PTree.gmap in H;
unfold option_map in H.
optDecN H INST;
trim.
intro.
rewrite H0 in H;
trim.
intro.
rewrite H0 in H;
trim.
Qed.
Lemma transf_f_In':
forall n,
f_In n f ->
f_In n tf.
Proof.
intros.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
inv EQ1.
simpls.
unfold f_In.
simpls.
unfold compute_bs_code;
rewrite PTree.gmap;
unfold option_map.
case_eq ((
fn_code f) !
n);
trim;
intros.
Qed.
Lemma transf_succ:
forall n s,
succ_node f n s ->
succ_node tf n s.
Proof.
unfold succ_node.
intros.
decs H.
monadInv FOK.
unfold compute_bs,
compute_bs_code;
simpl.
rewrite PTree.gmap;
unfold option_map.
rewrite H1;
simpl.
optDecGN INSL;
trim.
exists x;
auto.
destruct x;
eexists;
eauto.
split;
auto.
apply in_update_succs_icond;
auto.
Qed.
Lemma transf_succ':
forall n s,
succ_node tf n s ->
succ_node f n s.
Proof.
unfold succ_node.
intros.
decs H.
monadInv FOK.
unfold compute_bs,
compute_bs_code in H1;
simpl.
simpls.
rewrite PTree.gmap in H1;
unfold option_map in H1.
optDecN H1 INSL;
optDecN H1 INST;
trim.
inv H1.
exists x;
auto.
exists i.
split;
auto.
inv H1.
destruct i;
simpls;
trim.
apply in_update_succs_icond in H2;
auto.
Qed.
Lemma transf_reaches:
forall n n',
reaches f n n' ->
reaches tf n n'.
Proof.
introsv REACH.
induction REACH.
apply r_refl.
eapply transf_f_In';
eauto.
apply r_succ with (
n' :=
n');
auto.
apply transf_succ;
auto.
Qed.
Lemma transf_reaches':
forall n n',
reaches tf n n' ->
reaches f n n'.
Proof.
introsv REACH.
induction REACH.
apply r_refl.
eapply transf_f_In;
eauto.
apply r_succ with (
n' :=
n');
auto.
apply transf_succ';
auto.
Qed.
End CFG.
Section TRANSF_FAMILY.
Variable f :
function.
Variable fsc :
Scope.family f.
Variable exit_n :
node.
Variable reg_vint :
reg.
Variable nc :
node.
Variable tf :
function.
Variable of :
obs_function.
Hypothesis FOK:
slice_function f nc fsc exit_n reg_vint =
OK (
tf,
of).
Definition transf_family :
Scope.family tf.
apply transf_family with f.
apply fsc.
split.
eapply transf_f_In';
eauto.
eapply transf_f_In;
eauto.
split.
eapply transf_succ;
eauto.
eapply transf_succ';
eauto.
erewrite <-
transf_entry;
eauto.
Defined.
Proof.
Proof.