Lemmas related to SliceRelVar.
Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.
Require Import Coqlib.
Require Import Errors.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import VarsUseDef.
Require Import Scope.
Require Import SliceObs.
Require Import SliceRelVar.
Require Import SliceGen.
Require Import SliceObs_proof.
Require Import Utils.
Section REL_VAR_OBS.
Variable f :
function.
Variable fsc :
Scope.family f.
Variable exit_n :
node.
Variable reg_vint :
reg.
Hypothesis WFF:
check_wf f =
OK (
exit_n,
reg_vint).
Variable nc :
t_criterion.
Variable sliced_f :
function.
Variable of :
obs_function.
Hypothesis FOK:
slice_function f nc fsc exit_n reg_vint =
OK (
sliced_f,
of).
Notation nobs' := (
nobs (
_s_dobs of)).
Hypothesis exit_no_succ:
forall s, ~
succ_node f (
_exit of)
s.
Notation slice_nodes :=
of.(
_slice_nodes).
Notation succ_node' := (
succ_node f).
Notation in_slice n := (
In n of.(
_slice_nodes)).
Notation def' := (
def f).
Notation use' := (
use f).
Notation rvs' := (
_rvs of).
Ltac decSlice FOK EQ EQ1 DOBS RVS SCEX :=
unfolds in FOK;
unfold compute_slice in FOK;
monadInv FOK;
monadInv EQ;
optDecN EQ1 DOBS;
trim;
optDecN EQ1 RVS;
trim;
optDecN EQ1 SCEX;
trim;
inversion EQ1 as [
EQOF];
clear EQ1.
Lemma in_slice_use_in_rvs:
forall v n,
in_slice n ->
Regset.In v (
use'
n) ->
Regset.In v (
rvs'
n).
Proof.
intros.
decSlice FOK EQ EQ1 DOBS RVS SCEX.
simpls.
apply checked_rvs_wf in RVS;
inv RVS.
apply checked_in_slice_use_in_rvs;
auto.
apply checked_nobs_wf in DOBS;
auto.
inv DOBS.
apply checked_nobs_f_In.
Qed.
Lemma not_in_def_implies_rvs:
forall n s v,
succ_node'
n s ->
Regset.In v (
rvs'
s) ->
~
Regset.In v (
def'
n) ->
Regset.In v (
rvs'
n).
Proof.
intros.
decSlice FOK EQ EQ1 DOBS RVS SCEX.
simpl.
apply checked_rvs_wf in RVS;
inv RVS.
simpls.
unfold succ_node in H.
destruct H as [
i [
INST SUCC]].
eapply checked_not_in_def_in_rvs with (
i :=
i) (
s :=
s);
eauto.
simpls.
apply checked_nobs_wf in DOBS;
auto.
inv DOBS.
apply checked_nobs_f_In.
Qed.
Lemma not_in_slice_succ_rvs:
forall n
(
NIN: ~
in_slice n),
forall s
(
SUCC:
succ_node'
n s),
(
forall x,
Regset.In x (
rvs'
s) ->
Regset.In x (
rvs'
n)).
Proof.
intros.
dup FOK CHECK.
apply slice_ok_checked_nobs in CHECK;
auto.
decSlice FOK EQ EQ1 DOBS RVS SCEX.
simpl.
apply checked_rvs_wf in RVS;
inv RVS.
simpls.
dup SUCC FIN.
apply succ_f_In in FIN.
apply f_In_ex in FIN.
destruct FIN as [
i INST].
exploit checked_not_in_slice_succ_rvs;
eauto.
unfold succ_node in SUCC;
decs SUCC;
trim.
intros.
eapply checked_nobs_f_In;
eauto.
Qed.
Lemma not_in_slice_def_not_in_rvs:
forall n,
f_In n f ->
~
in_slice n ->
forall x,
Regset.In x (
def'
n) ->
~
Regset.In x (
rvs'
n).
Proof.
Lemma in_slice_mem_def:
forall n n'
(
MEMIN:
Regset.In memvar (
rvs'
n'))
(
SUCC:
succ_node'
n n')
(
MEMDEF:
Regset.In memvar (
def'
n))
(
MEMRVS:
Regset.In memvar (
rvs'
n)),
in_slice n.
Proof.
intros.
dup FOK CHECK.
apply slice_ok_checked_nobs in CHECK;
auto.
decSlice FOK EQ EQ1 DOBS RVS SCEX.
simpl.
apply checked_rvs_wf in RVS;
inv RVS.
simpls.
dup SUCC FIN.
apply succ_f_In in FIN;
auto.
apply f_In_ex in FIN.
destruct FIN as [
i INST].
dup SUCC FIN.
eapply succ_f_In'
in FIN;
eauto.
apply f_In_ex in FIN.
destruct FIN as [
i'
INST'].
apply checked_in_slice_mem_def with (
i :=
i) (
s :=
n');
auto.
unfold succ_node in SUCC;
decs SUCC;
trim.
intros.
eapply checked_nobs_f_In;
eauto.
Qed.
End REL_VAR_OBS.