Several lemmas related to program slicing.
Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.
Require Import Classical.
Require Import Program.
Require Import Coqlib.
Require Import RTL.
Require Import Maps.
Require Import Errors.
Require Import Registers.
Require Import Op.
Require Import AST.
Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import VarsUseDef.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import SliceObs.
Require Import SliceRelVar.
Require Import SliceGen.
Require Import SliceObs_proof.
Require Import SliceRelVar_proof.
Require Import Scope.
Require Import Utils.
Section INSTRUCTIONS.
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 tf :
function.
Variable of :
obs_function.
Hypothesis FOK:
slice_function f nc fsc exit_n reg_vint =
OK (
tf,
of).
Let TFOK:
transf_function nc exit_n reg_vint f fsc =
OK tf.
Proof.
unfolds; unfolds; rw; auto.
Qed.
Notation exit_n' :=
of.(
_exit).
Ltac bsCode :=
unfold compute_bs_code;
rewrite PTree.gmap;
unfold option_map.
Lemma in_list:
forall {
A :
Type} (
l l':
list A)
a,
l =
a ::
l' ->
In a l.
Proof.
induction l; intros; trim.
inv H; auto.
Qed.
Lemma in_singleton_eq:
forall {
A :
Type} (
l:
list A)
a,
l =
a ::
nil ->
forall b,
In b l ->
b =
a.
Proof.
induction l; intros; trim.
destruct l; trim.
inv H0; trim.
Qed.
Ltac UnOf FOK EQ EQ3 DOBS RVS SCEX :=
monadInv FOK;
monadInv EQ;
optDecN EQ3 DOBS;
trim;
optDecN EQ3 RVS;
trim;
optDecN EQ3 SCEX;
trim.
Lemma exit_no_succ:
forall s, ~
succ_node f exit_n'
s.
Proof.
intros.
clear TFOK.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
inv EQ1.
unfolds in WFF.
optDecN WFF CONDS;
trim.
monadInv WFF.
unfolds in EQ.
optDecN EQ HAS;
trim.
destruct l;
trim.
destruct p;
simpls.
destruct i;
trim.
inv EQ.
intro.
unfold succ_node in H.
destruct H as [
i [
INST INF]].
apply in_list in HAS.
apply filter_In in HAS.
destruct HAS.
apply PTree.elements_complete in H.
simpls.
inv EQ2;
simpls.
rewrite H in INST.
inv INST;
trim.
Qed.
Lemma exit_unique:
forall n,
f_In n f ->
(
forall s, ~
succ_node f n s) ->
n =
exit_n'.
Proof.
intros.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
unfolds in WFF.
optDecN WFF CONDS;
trim.
monadInv WFF.
unfolds in EQ.
optDecN EQ HAS;
trim.
destruct l;
trim.
destruct p;
simpls.
destruct i;
trim.
inv EQ.
apply f_In_ex in H.
destruct H as [
i'
INST'].
apply PTree.elements_correct in INST'.
unfold succ_node in H0.
dup INST'
I.
apply PTree.elements_complete in I.
destruct i';
try solve [
exfalso;
apply H0 with (
s :=
n0);
eexists;
split;
eauto;
simpls;
eauto].
apply in_singleton_eq with (
b := (
n,
Itailcall s s0 l))
in HAS;
trim.
apply filter_In.
split;
auto.
destruct l.
apply in_singleton_eq with (
b := (
n,
Ijumptable r nil))
in HAS;
trim.
apply filter_In.
split;
auto.
exfalso;
apply H0 with (
s :=
n0);
eexists;
split;
eauto;
simpls;
eauto.
inv EQ1;
simpls.
apply in_singleton_eq with (
b := (
n,
Ireturn o0))
in HAS;
trim.
apply filter_In.
split;
auto.
Qed.
Lemma exit_is_return:
exists o,
(
fn_code f) !
exit_n' =
Some (
Ireturn o).
Proof.
intros.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
unfolds in WFF.
optDecN WFF CONDS;
trim.
monadInv WFF.
unfolds in EQ.
optDecN EQ HAS;
trim.
destruct l;
trim.
destruct p;
simpls.
destruct i;
trim.
inv EQ.
exists o.
apply PTree.elements_complete.
apply in_list in HAS.
apply filter_In in HAS.
destruct HAS;
auto.
inv EQ1;
auto.
Qed.
Lemma return_no_succ:
forall n o,
f.(
fn_code) !
n =
Some (
Ireturn o) ->
forall s, ~
succ_node f n s.
Proof.
intros.
intro.
unfolds in H0.
decs H0.
rewrite H2 in H.
inv H; trim.
Qed.
Lemma return_is_exit:
forall n o,
(
fn_code f) !
n =
Some (
Ireturn o) ->
n =
exit_n'.
Proof.
Lemma slice_preserves_instructions:
forall pc,
In pc of.(
_slice_nodes) ->
tf.(
fn_code) !
pc =
f.(
fn_code) !
pc.
Proof.
introsv IN_BS.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
inv EQ1.
simpls.
bsCode.
case_eq (
fn_code f) !
pc;
introsv SOME;
auto.
rewrite <-
mem_iff_In in IN_BS.
rewrite IN_BS;
auto.
Qed.
Lemma slice_preserves_Inop:
forall pc pc',
f.(
fn_code) !
pc =
Some (
Inop pc') ->
tf.(
fn_code) !
pc =
Some (
Inop pc').
Proof.
introsv IN_BS.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
inv EQ1.
simpls.
bsCode.
case_eq (
fn_code f) !
pc;
introsv SOME;
rewrite SOME in IN_BS;
inv IN_BS.
optDecG;
trim.
Qed.
Lemma slice_transforms:
forall pc i s slice_nodes exit_n
(
INST : (
fn_code f) !
pc =
Some i)
(
SUCC:
successor_instr i =
Some s)
(
NOTIN : ~
In pc slice_nodes),
(
compute_bs_code (
_reg_vint of)
f slice_nodes (
f_dobs f nc slice_nodes) (
f_dexit f exit_n)) !
pc =
Some (
Inop s).
Proof.
intros.
bsCode.
rewrite INST.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN.
unfold successor_instr in SUCC.
destruct i;
simpl;
trim.
apply positive.
Qed.
Lemma slice_transforms_Iop:
forall pc op args res pc',
~
In pc of.(
_slice_nodes) ->
f.(
fn_code) !
pc =
Some (
Iop op args res pc') ->
tf.(
fn_code) !
pc =
Some (
Inop pc').
Proof.
introsv NOTIN INST.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN;
auto.
apply positive.
Qed.
Lemma slice_transforms_Iload:
forall pc chunk addr args dst pc',
~
In pc of.(
_slice_nodes) ->
f.(
fn_code) !
pc =
Some (
Iload chunk addr args dst pc') ->
tf.(
fn_code) !
pc =
Some (
Inop pc').
Proof.
introsv NOTIN INST.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN;
auto.
apply positive.
Qed.
Lemma slice_transforms_Istore:
forall pc chunk addr args src pc',
~
In pc of.(
_slice_nodes) ->
f.(
fn_code) !
pc =
Some (
Istore chunk addr args src pc') ->
tf.(
fn_code) !
pc =
Some (
Inop pc').
Proof.
introsv NOTIN INST.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN;
auto.
apply positive.
Qed.
Lemma slice_transforms_Icall:
forall pc sig ros args res pc',
~
In pc of.(
_slice_nodes) ->
f.(
fn_code) !
pc =
Some (
Icall sig ros args res pc') ->
tf.(
fn_code) !
pc =
Some (
Inop pc').
Proof.
introsv NOTIN INST.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN;
auto.
apply positive.
Qed.
Lemma slice_transforms_Itailcall:
forall pc sig ros args,
~
In pc of.(
_slice_nodes) ->
f.(
fn_code) !
pc =
Some (
Itailcall sig ros args) ->
tf.(
fn_code) !
pc =
Some (
Ireturn None).
Proof.
introsv NOTIN INST.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN;
auto.
apply positive.
Qed.
Lemma slice_transforms_Ibuiltin:
forall pc ef args res pc',
~
In pc of.(
_slice_nodes) ->
f.(
fn_code) !
pc =
Some (
Ibuiltin ef args res pc') ->
tf.(
fn_code) !
pc =
Some (
Inop pc').
Proof.
introsv NOTIN INST.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
rewrite NOTIN;
auto.
apply positive.
Qed.
Notation nobs' := (
nobs of.(
_s_dobs)).
Notation icond_true' := (
icond_true (
_reg_vint of)).
Notation icond_false' := (
icond_false (
_reg_vint of)).
Let EXIT_NO_SUCC :
forall s :
RTL.node, ~
succ_node f exit_n'
s.
Proof.
Lemma slice_transforms_Icond_true:
forall pc d dc dc'
o cond args ifso ifnot,
f.(
fn_code) !
pc =
Some (
Icond cond args ifso ifnot) ->
nobs' !
pc =
Some (
S d,
dc,
o) ->
nobs' !
ifso =
Some (
d,
dc',
o) ->
tf.(
fn_code) !
pc =
Some (
icond_true'
ifso ifnot).
Proof.
introsv INST OBS OBS'.
assert (
SUCC:
succ_node f pc ifnot).
eexists;
eauto;
split;
eauto;
simpl;
auto.
gen (
nobs_not_zero_not_in_slice _ _ _ _ _ _ _ FOK EXIT_NO_SUCC _ _ _ _ OBS)
as NOTIN.
gen (
nobs_succ_minus_one _ _ _ _ _ _ _ FOK EXIT_NO_SUCC _ _ _ _ OBS _ SUCC)
as MINUS.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
inv EQ1;
simpls.
rewrite NOTIN;
auto.
f_equal.
unfolds.
unfold nobs in *.
rewrite PTree.gmap in *;
unfold option_map in *.
optDecN OBS DOBSPC;
trim.
optDecN OBS'
DOBS';
trim.
destruct p as [[
d'
dc'']
o'].
destruct p0 as [[
d''
dc''']
o''].
optDecGN DOBS'';
trim.
destruct p as [[
d'''
dc'''']
o'''].
optDecG;
trim.
inv_clear OBS.
inv_clear OBS'.
rewrite DOBS''
in MINUS.
subst d dc dc'.
assert ((
Nnat.nat_of_N d''' >=
Nnat.nat_of_N d'')%
nat).
eapply MINUS;
eauto.
lia2.
apply positive.
Qed.
Lemma slice_transforms_Icond_false:
forall pc d d'
dc dc'
dc''
o cond args ifso ifnot,
f.(
fn_code) !
pc =
Some (
Icond cond args ifso ifnot) ->
nobs' !
pc =
Some (
S d,
dc,
o) ->
nobs' !
ifnot =
Some (
d,
dc',
o) ->
(
nobs' !
ifso =
Some (
d',
dc'',
o) /\ (
d' >
d)%
nat \/
nobs' !
ifso =
None) ->
tf.(
fn_code) !
pc =
Some (
icond_false'
ifso ifnot).
Proof.
introsv INST OBS OBS'
DISJ.
assert (
SUCC:
succ_node f pc ifso).
eexists;
eauto;
split;
eauto;
simpl;
auto.
assert (
SUCC':
succ_node f pc ifnot).
eexists;
eauto;
split;
eauto;
simpl;
auto.
gen (
nobs_not_zero_not_in_slice _ _ _ _ _ _ _ FOK EXIT_NO_SUCC _ _ _ _ OBS)
as NOTIN.
gen (
nobs_succ_minus_one _ _ _ _ _ _ _ FOK EXIT_NO_SUCC _ _ _ _ OBS _ SUCC)
as MINUS.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpl.
bsCode.
rewrite INST;
simpls.
rewrite <-
mem_iff_In_conv in NOTIN.
inv EQ1;
simpls.
rewrite NOTIN;
auto.
f_equal.
unfolds.
unfold nobs in *.
rewrite PTree.gmap in *;
unfold option_map in *.
optDecN OBS DOBSPC;
trim.
optDecN OBS'
DOBST;
trim.
destruct p as [[
d''
dc''']
o'].
inv_clear OBS.
subst o'
dc.
destruct p0 as [[
d'''
dc]
o'].
inv_clear OBS'.
subst d o'
dc'.
optDecGN DOBS'';
trim.
destruct p as [[
d dc']
o'].
rewrite DOBS''
in *.
optDecG;
trim.
destruct DISJ as [[
EQS IFSO] |
IFNOT];
trim.
inv_clear EQS.
subst d'
dc''
o'.
lia2.
apply positive.
Qed.
Notation nexit' := (
nexit of.(
_dexit)).
Lemma slice_transforms_Icond_none_true:
forall pc dx cond args ifso ifnot,
f.(
fn_code) !
pc =
Some (
Icond cond args ifso ifnot) ->
nobs' !
pc =
None ->
nexit' !
pc =
Some (
S dx) ->
nexit' !
ifso =
Some dx ->
tf.(
fn_code) !
pc =
Some (
icond_true'
ifso ifnot).
Proof.
introsv INST NOBS NEXIT NEXIT'.
assert (
SUCC:
succ_node f pc ifso).
eexists;
eauto;
split;
eauto;
simpl;
auto.
assert (
SUCC':
succ_node f pc ifnot).
eexists;
eauto;
split;
eauto;
simpl;
auto.
gen exit_no_succ as EXIT_OK.
gen (
nobs_none_not_in_slice _ _ _ _ _ _ _ FOK EXIT_OK _ NOBS)
as NONE.
gen (
nexit_succ_minus_one _ _ _ _ _ _ _ FOK EXIT_OK _ _ NEXIT _ SUCC')
as MINUS.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpls.
bsCode.
rewrite INST.
rewrite <-
mem_iff_In_conv in NONE.
rewrite NONE;
auto.
f_equal.
unfolds.
unfold nobs in NOBS.
rewrite PTree.gmap in NOBS;
unfold option_map in NOBS.
optDecN NOBS DOBS';
trim.
optDecGN DEXITT;
trim.
optDecGN DEXITF;
trim.
optDecG;
trim.
unfold nexit in *.
rewrite PTree.gmap in *;
unfold option_map in *.
rewrite DEXITT in NEXIT'.
optDecN NEXIT DEXIT;
trim.
inv NEXIT.
inv NEXIT'.
rewrite DEXITF in MINUS.
assert ((
Nnat.nat_of_N n0 >=
Nnat.nat_of_N n)%
nat).
eapply MINUS;
eauto.
lia2.
apply positive.
Qed.
Lemma slice_transforms_Icond_none_false:
forall pc dx dx'
cond args ifso ifnot,
f.(
fn_code) !
pc =
Some (
Icond cond args ifso ifnot) ->
nobs' !
pc =
None ->
nexit' !
pc =
Some (
S dx) ->
nexit' !
ifnot =
Some dx ->
nexit' !
ifso =
Some dx' ->
(
dx' >
dx)%
nat ->
tf.(
fn_code) !
pc =
Some (
icond_false'
ifso ifnot).
Proof.
introsv INST NOBS NEXIT NEXITF NEXITT DGT.
assert (
SUCC:
succ_node f pc ifso).
eexists;
eauto;
split;
eauto;
simpl;
auto.
assert (
SUCC':
succ_node f pc ifnot).
eexists;
eauto;
split;
eauto;
simpl;
auto.
gen exit_no_succ as EXIT_OK.
gen (
nobs_none_not_in_slice _ _ _ _ _ _ _ FOK EXIT_OK _ NOBS)
as NONE.
gen (
nexit_succ_minus_one _ _ _ _ _ _ _ FOK EXIT_OK _ _ NEXIT _ SUCC')
as MINUS.
UnOf FOK EQ EQ1 DOBS RVS SCEX.
simpls.
bsCode.
rewrite INST.
rewrite <-
mem_iff_In_conv in NONE.
rewrite NONE;
auto.
f_equal.
unfolds.
unfold nobs in NOBS.
rewrite PTree.gmap in NOBS;
unfold option_map in NOBS.
optDecN NOBS DOBS';
trim.
unfold nexit in *.
rewrite PTree.gmap in *;
unfold option_map in *.
optDecN NEXIT DEXIT;
trim.
optDecN NEXITT DEXITT;
trim.
optDecN NEXITF DEXITF;
trim.
inv NEXIT.
inv NEXITT.
inv NEXITF.
optDecG;
trim.
lia2.
apply positive.
Qed.
Lemma slice_preserves_Ireturn:
forall pc optarg,
f.(
fn_code) !
pc =
Some (
Ireturn optarg) ->
tf.(
fn_code) !
pc =
Some (
Ireturn optarg).
Proof.
Lemma slice_preserves_entry:
tf.(
fn_entrypoint) =
f.(
fn_entrypoint).
Proof.
unfolds in FOK.
monadInv FOK;
auto.
Qed.
End INSTRUCTIONS.
Local Open Scope positive_scope.
Section 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 tf :
function.
Variable of :
obs_function.
Hypothesis FOK:
slice_function f nc fsc exit_n reg_vint =
OK (
tf,
of).
Let TFOK:
transf_function nc exit_n reg_vint f fsc =
OK tf.
Proof.
unfolds; unfolds; rw; auto.
Qed.
Notation slice_nodes :=
of.(
_slice_nodes).
Notation succ_node' := (
succ_node f).
Notation in_slice n := (
In n of.(
_slice_nodes)).
Notation s_obs := (
obs of.(
_s_dobs)).
Notation nobs' := (
nobs of.(
_s_dobs)).
Notation exit_n' :=
of.(
_exit).
Notation nexit' := (
nexit of.(
_dexit)).
Lemma nobs_s_obs:
forall n d dc o,
nobs' !
n =
Some (
d,
dc,
o) ->
s_obs n =
Some o.
Proof.
intros.
unfold obs,
nobs in *.
rewrite PTree.gmap in H;
unfold option_map in H.
optDecN H DOBS;
trim.
destruct_pairs.
inv_clear H;
auto.
Qed.
Lemma s_obs_nobs:
forall n o,
s_obs n =
Some o ->
exists d,
exists dc,
nobs' !
n =
Some (
d,
dc,
o).
Proof.
intros.
unfold obs,
nobs in *.
rewrite PTree.gmap;
unfold option_map.
optDecN H DOBS;
trim.
destruct_pairs.
inv_clear H;
eauto.
Qed.
Lemma nobs_s_obs':
forall n,
nobs' !
n =
None ->
s_obs n =
None.
Proof.
intros.
unfold obs,
nobs in *.
rewrite PTree.gmap in H;
unfold option_map in H.
optDecN H DOBS;
trim.
Qed.
Lemma s_obs_nobs':
forall n,
s_obs n =
None ->
nobs' !
n =
None.
Proof.
intros.
unfold obs,
nobs in *.
rewrite PTree.gmap;
unfold option_map.
optDecN H DOBS;
trim.
destruct_pairs.
inv_clear H;
eauto.
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.
Ltac decTransf F EQ EQ0 DOBS RVS SCEX :=
unfold transf_function,
slice_function;
optDecGN F;
trim; [
monadInv F;
simpl;
unfolds in EQ;
rewrite EQ0 in EQ;
simpls;
rewrite DOBS in EQ;
simpls;
rewrite RVS in EQ;
simpls;
rewrite SCEX in EQ;
simpls;
inv EQ;
simpls | ..].
Ltac bsCode :=
unfold compute_bs_code;
rewrite PTree.gmap;
unfold option_map.
Let EXIT_NO_SUCC :
forall s :
RTL.node, ~
succ_node'
exit_n'
s.
Proof.
Let fok_nobs_checked:
checked_nobs f nc exit_n'
of.(
_slice_nodes)
nobs'
nexit'.
Proof.
Lemma in_slice_s_obs_refl:
forall n,
in_slice n ->
s_obs n =
Some n.
Proof.
Lemma succ_obs_subset:
forall n s
(
SUCC:
succ_node'
n s)
(
NIN: ~
in_slice n),
forall n',
(
s_obs s =
Some n' ->
s_obs n =
Some n') /\
(
s_obs n =
None ->
s_obs s =
None) /\
(
s_obs n =
Some n' ->
s_obs s =
Some n' \/
s_obs s =
None).
Proof.
intros.
unfold obs.
case_eq (
nobs' !
n);
introsv NOBSN;
destruct_pairs.
destruct n1.
eapply nobs_zero_in_slice in NOBSN;
eauto;
trim.
exploit nobs_some_succ_same;
eauto;
intro SOME.
destruct SOME as [
d' [
dc'
NOBSS]].
unfold nobs in *.
rewrite PTree.gmap in *;
unfold option_map in *.
optDecN NOBSN DOBSN;
trim.
optDecN NOBSS DOBSS;
trim.
destruct_pairs.
inv_clear NOBSN.
inv_clear NOBSS.
split;
intros.
inv_clear H0;
inv_clear H1;
subst;
auto.
split;
intros;
trim.
exploit nobs_none_succ_none;
eauto;
intro NOBSS.
unfold nobs in *.
rewrite PTree.gmap in *;
unfold option_map in *.
optDecN NOBSN DOBSN;
trim.
optDecN NOBSS DOBSS;
trim.
Qed.
Lemma obs_none_not_in_slice:
forall n,
s_obs n =
None -> ~
in_slice n.
Proof.
Lemma obs_none_succ_none:
forall n s,
s_obs n =
None ->
succ_node'
n s ->
s_obs s =
None.
Proof.
intros.
apply s_obs_nobs'
in H.
eapply nobs_none_succ_none in H;
eauto.
apply nobs_s_obs';
auto.
Qed.
Lemma obs_none_reaches_none:
forall n s,
s_obs n =
None ->
reaches f n s ->
s_obs s =
None.
Proof.
Lemma nobs_some_reaches:
forall d n o dc i
(
INST: (
fn_code f) !
n =
Some i)
(
OBS:
nobs' !
n =
Some (
d,
dc,
o)),
reaches f n o.
Proof.
induction d;
intros.
eapply nobs_zero_refl in OBS;
eauto.
subst o.
apply r_refl.
unfold f_In;
intro;
trim.
eapply nobs_non_zero_ex_succ in OBS;
eauto.
destruct OBS as [
s [
dc' [
SUCC NOBS']]].
dup SUCC FIN.
eapply succ_f_In'
in FIN;
eauto.
apply f_In_ex in FIN.
destruct FIN as [
i'
INST'].
apply IHd with (
i :=
i')
in NOBS';
auto.
apply r_succ with (
n' :=
s);
auto.
Qed.
Lemma obs_some_reaches:
forall n o i
(
INST: (
fn_code f) !
n =
Some i)
(
OBS:
s_obs n =
Some o),
reaches f n o.
Proof.
Lemma nobs_obs_in_slice:
forall d n o dc i
(
INST: (
fn_code f) !
n =
Some i)
(
NOBS:
nobs' !
n =
Some (
d,
dc,
o)),
in_slice o.
Proof.
induction d;
intros.
dup NOBS NOBS'.
eapply nobs_zero_refl in NOBS';
eauto.
subst n.
eapply nobs_zero_in_slice in NOBS;
eauto.
destruct d.
eapply nobs_non_zero_ex_succ in NOBS;
eauto.
decs NOBS.
eapply succ_f_In'
in H;
eauto.
unfold f_In in H.
case_eq ((
fn_code f) !
x);
intros;
trim.
eapply IHd in H1;
eauto.
eapply nobs_non_zero_ex_succ in NOBS;
eauto.
decs NOBS.
eapply succ_f_In'
in H;
eauto.
unfold f_In in H.
case_eq ((
fn_code f) !
x);
intros;
trim.
eapply IHd in H1;
eauto.
Qed.
Lemma nobs_some_succ:
forall pc pc'
d dc o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
SUCC :
succ_node f pc pc')
(
NOBS :
nobs' !
pc =
Some (
d,
dc,
o)),
s_obs pc' =
Some o.
Proof.
intros.
destruct d.
eapply nobs_zero_in_slice with (
f :=
f) (
nc :=
nc)
in NOBS;
eauto.
contra.
unfolds.
dup NOBS NOBS'.
unfold nobs in NOBS'.
rewrite PTree.gmap in NOBS';
unfold option_map in NOBS'.
optDecN NOBS'
DOBS;
trim.
destruct p as [[
d'
dc']
o'].
inv_clear NOBS'.
subst dc o'.
dup SUCC SUCCI.
destruct SUCCI as [
i [
INcstate SUCCI]].
optDecGN DOBS'.
destruct p as [[
d''
dc'']
o''].
dup FOK OBS.
apply succ_obs_subset with (
n :=
pc) (
s :=
pc') (
n' :=
o)
in SUCC;
auto.
decs OBS.
unfold obs in *.
rewrite DOBS,
DOBS'
in *.
assert (
Some o =
Some o)
by refl.
apply SUCC in H.
destruct H;
trim.
eapply nobs_non_zero_ex_succ in NOBS;
eauto.
assert (
NOBS':
nobs' !
pc' =
None).
apply s_obs_nobs'.
unfold obs;
rw;
auto.
destruct NOBS as [
s [
dc'' [
SUCC'
NOBSS]]].
eapply nobs_control_in_slice in NOBS';
eauto.
trim.
Qed.
Lemma obs_some_succ:
forall pc pc'
o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
SUCC :
succ_node f pc pc')
(
OBS :
s_obs pc =
Some o),
s_obs pc' =
Some o.
Proof.
intros.
unfold obs in OBS.
optDecN OBS DOBS;
trim.
destruct p as [[
d dc]
o'].
inv_clear OBS;
subst o'.
eapply nobs_some_succ;
eauto.
unfold nobs.
rewrite PTree.gmap;
unfold option_map.
rewrite DOBS;
auto.
Qed.
Lemma nobs_some_succ_eq:
forall pc pc'
d d'
dc dc'
o o'
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
SUCC :
succ_node f pc pc')
(
NOBSPC :
nobs' !
pc =
Some (
d,
dc,
o))
(
NOBSPC' :
nobs' !
pc' =
Some (
d',
dc',
o')),
o' =
o.
Proof.
intros.
exploit nobs_some_succ;
eauto;
intros.
unfolds in H.
unfold nobs in *.
rewrite PTree.gmap in *;
unfold option_map in *.
optDec H;
trim.
destruct p;
destruct p;
trim.
Qed.
Lemma nobs_some_succ_eq_2:
forall pc pc'
d dc o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
SUCC :
succ_node f pc pc')
(
PC'
_IN :
In pc' (
_slice_nodes of))
(
NOBSPC :
nobs' !
pc =
Some (
d,
dc,
o)),
o =
pc'.
Proof.
Lemma nobs_some_onlysucc:
forall d dc i pc pc'
(
INcstate: (
fn_code f) !
pc =
Some i)
(
SUCC :
succ_node f pc pc')
(
ONLYSUCC:
length (
successors_instr i) = 1%
nat)
(
NOBS:
nobs' !
pc =
Some (
d,
dc,
pc')),
s_obs pc' =
Some pc'.
Proof.
destruct d;
intros.
dup NOBS NOBS'.
eapply nobs_zero_refl in NOBS;
eauto.
subst pc'.
unfolds.
unfold nobs in *;
rewrite PTree.gmap in *;
unfold option_map in *.
optDecG;
trim.
destruct p;
destruct p.
inv_clear NOBS';
auto.
eapply nobs_non_zero_ex_succ'
in NOBS;
eauto.
destruct NOBS as [
s [
n' [
dc' [
S NOBSS]]]].
unfolds in SUCC.
unfolds in S.
destruct SUCC as [
i' [
INcstate'
PC']].
destruct S as [
i'' [
INcstate''
S]].
rewrite INcstate''
in INcstate'.
inv INcstate'.
rewrite INcstate''
in INcstate.
inv INcstate.
destruct (
successors_instr i);
trim.
destruct l;
simpls;
try lia2.
destruct PC';
trim;
destruct S;
trim.
subst s pc'.
eapply nobs_s_obs;
eauto.
Qed.
End OBS.