Correctness proof for the program slicing.
Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.
Require Import FSetProperties.
Require Import Program.
Require Import Coqlib.
Require Import Integers.
Require Import Errors.
Require Import Globalenvs.
Require Import AST.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Op.
Module RegsetF :=
FSetFacts.Facts(
Regset).
Require Import Utils.
Require Import ValueAnalysis.
Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import VarsUseDef.
Require Import SliceObs.
Require Import SliceRelVar.
Require Import SliceGen.
Require Import SliceObs_proof.
Require Import SliceRelVar_proof.
Require Import SliceScopeExits_proof.
Require Import Scope.
Require Import Sliceproof.
Require Import SliceRegVint.
Require Import SliceAgree.
Require Import Counter.
Require Import WeakSimulation.
Require Import CountingSem.
Require Import SliceCFG.
Require Import HeaderBounds.
Notation all_counters := (
counter *
counter)%
type.
Definition counter_eq (
nc :
t_criterion) (
cs cs' :
counter) :=
cs #
nc =
cs' #
nc.
Lemma counter_eq_refl:
forall nc cs,
counter_eq nc cs cs.
Proof.
unfold counter_eq; auto.
Qed.
Lemma counter_eq_sym:
forall nc cs cs',
counter_eq nc cs cs' ->
counter_eq nc cs'
cs.
Proof.
unfold counter_eq; auto.
Qed.
Lemma counter_eq_trans:
forall nc cs cs'
cs'',
counter_eq nc cs cs' ->
counter_eq nc cs'
cs'' ->
counter_eq nc cs cs''.
Proof.
unfold counter_eq; intros.
rewrite H; auto.
Qed.
Inductive initial_state rs m (
f :
function) (
nc :
t_criterion) :
cstate ->
Prop :=
|
i_init:
initial_state rs m f nc (
init_st f rs m).
Inductive final_state (
f :
function) (
crit :
t_criterion) :
cstate ->
all_counters ->
Prop :=
|
i_final:
forall
pc cs cs'
rcs rcs'
rs m
(
COUNTERS:
counter_eq crit cs cs')
(
RCOUNTERS:
counter_eq crit rcs rcs'),
final_state f crit (
CST (
State pc rs m)
cs rcs) (
cs',
rcs').
Definition i_semantics rs m (
f :
function) (
crit :
t_criterion) (
fsc :
Scope.family f) (
sp :
val) (
ge :
Genv.t fundef unit) :
T_semantics (
all_counters) :=
Semantics (
fun ge =>
cstep ge f fsc sp) (
initial_state rs m f crit) (
final_state f crit)
ge.
Section PRESERVATION.
Variable f :
function.
Variable exit_n :
node.
Variable reg_vint :
reg.
Hypothesis WFF:
check_wf f =
OK (
exit_n,
reg_vint).
Variable live :
PMap.t Regset.t.
Variable fsc :
Scope.family f.
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 counter_eq' := (
counter_eq nc).
Notation rvs of := (
_rvs of).
Notation s_obs of n := (
obs (
_s_dobs of)
n).
Notation entry f :=
f.(
fn_entrypoint).
Notation nobs'
of := (
nobs (
_s_dobs of)).
Notation nexit'
of := (
nexit (
_dexit of)).
Notation succ_node' := (
succ_node f).
Notation exit_n' := (
_exit of).
Notation reg_vint' := (
_reg_vint of).
Notation icond_true' := (
icond_true reg_vint').
Notation icond_false' := (
icond_false reg_vint').
Notation valid_rs' := (
valid_rs f reg_vint').
Notation valid_rs_t' := (
valid_rs tf reg_vint').
Let EXIT_NO_SUCC :
forall s :
RTL.node, ~
succ_node'
exit_n'
s.
Proof.
Lemma exit_no_entry:
entry f <>
exit_n'.
Proof.
intro CONTRA.
exploit entry_inst;
eauto.
intros EINST.
destruct EINST as (
s &
EINST).
rewrite CONTRA in EINST.
exploit exit_no_succ;
eauto.
eexists;
eauto.
Qed.
Notation in_slice_dec pc of := (
List.In_dec positive_eq_dec pc of.(
_slice_nodes)).
Definition tfsc :
Scope.family tf := (
transf_family FOK).
Lemma transf_exited_scopes:
exited_scopes tfsc =
exited_scopes fsc.
Proof.
Notation inc_r_counter' := (
inc_r_counter f fsc).
Notation inc_r_counter_t' := (
inc_r_counter tf tfsc).
Notation inc_r'
_counter' := (
inc_r'
_counter f fsc).
Notation inc_r'
_counter_t' := (
inc_r'
_counter tf tfsc).
Definition update_state_counters (
f :
function) (
fsc :
Scope.family f) (
pc :
node) (
s :
cstate) :
cstate :=
match s with
|
CST (
State pc'
rs m)
cs rcs =>
let cs' :=
inc_counter pc cs in
let rcs' :=
inc_r_counter f fsc pc pc'
rcs in
(
CST (
State pc'
rs m)
cs'
rcs')
end.
Notation update_state_counters' := (
update_state_counters f fsc).
Notation update_state_counters_t' := (
update_state_counters tf tfsc).
Variable ge :
genv.
Variable sp :
val.
Notation cstep' := (
fun ge =>
cstep ge f fsc sp).
Notation cstep_t' := (
fun ge =>
cstep ge tf tfsc sp).
Hint Immediate counter_eq_refl.
Hint Immediate counter_eq_sym.
Hint Immediate counter_eq_trans.
Notation rvs_agree' := (
rvs_agree f of).
Inductive match_states :
cstate ->
cstate ->
Prop :=
|
ms1:
forall pc cs rcs cs'
rcs'
rs rs'
o m m'
(
COUNTERS:
counter_eq'
cs cs')
(
RCOUNTERS:
counter_eq'
rcs rcs')
(
PC_IN:
In pc of.(
_slice_nodes))
(
OBSPC:
s_obs of pc =
Some o)
(
VRS:
pc = (
fn_entrypoint f) ->
rs =
rs')
(
AGREE:
rvs_agree'
pc (
rvs of pc)
rs rs'
m m'),
match_states (
CST (
State pc rs m)
cs rcs) (
CST (
State pc rs'
m')
cs'
rcs')
|
ms2:
forall pc pc'
cs rcs cs'
rcs'
rs rs'
o m m'
(
COUNTERS:
counter_eq'
cs cs')
(
RCOUNTERS:
counter_eq'
rcs rcs')
(
PC_OUT: ~
In pc of.(
_slice_nodes))
(
PC'
_OUT: ~
In pc'
of.(
_slice_nodes))
(
OBSPC:
s_obs of pc =
Some o)
(
OBSPC':
s_obs of pc' =
Some o)
(
AGREE:
rvs_agree'
pc' (
rvs of pc)
rs rs'
m m')
(
VRS:
rs #
reg_vint' =
Vint Int.zero)
(
VRS':
rs' #
reg_vint' =
Vint Int.zero),
match_states (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs')
|
ms3:
forall pc rs rs'
m m'
cs rcs cs'
rcs'
(
COUNTERS:
counter_eq'
cs cs')
(
RCOUNTERS:
counter_eq'
rcs rcs')
(
VRS:
rs #
reg_vint' =
Vint Int.zero)
(
VRS':
rs' #
reg_vint' =
Vint Int.zero)
(
OBS:
s_obs of pc =
None),
match_states (
CST (
State pc rs m)
cs rcs) (
CST (
State exit_n'
rs'
m')
cs'
rcs').
Section PRES_FUNCTION.
Lemma f_unique_return:
forall n n'
o1 o2,
f.(
fn_code) !
n =
Some (
Ireturn o1) ->
f.(
fn_code) !
n' =
Some (
Ireturn o2) ->
n =
n'.
Proof.
Lemma transf_entry:
tf.(
fn_entrypoint) =
f.(
fn_entrypoint).
Proof.
Lemma match_states_init_st:
forall rs m,
match_states (
init_st f rs m) (
init_st tf rs m).
Proof.
Lemma transf_initial_states:
forall rs m st1,
initial_state rs m f nc st1 ->
exists st2,
initial_state rs m tf nc st2 /\
match_states st1 st2.
Proof.
Lemma transf_init_st:
forall rs m,
init_st tf rs m =
init_st f rs m.
Proof.
Lemma transf_valid_rs:
forall pc rs,
valid_rs'
pc rs ->
valid_rs_t'
pc rs.
Proof.
Lemma transf_valid_rs':
forall pc rs,
valid_rs_t'
pc rs ->
valid_rs'
pc rs.
Proof.
intros.
unfold valid_rs in H.
rewrite transf_entry in H;
auto.
Qed.
Let s_dobs_checker_ok:
checked_nobs f nc exit_n' (
_slice_nodes of) (
nobs'
of) (
nexit'
of).
Proof.
Lemma transf_final_states:
forall st1 st2 cs1 cs2 rcs1 rcs2
(
MS:
match_states st1 st2)
(
CSEQ:
counter_eq'
cs1 cs2)
(
RCSEQ:
counter_eq'
rcs1 rcs2)
(
FINAL:
final_state f nc st1 (
cs1,
rcs1)),
final_state tf nc st2 (
cs2,
rcs2).
Proof.
Lemma transf_wf_cond_acc:
wf_cond_acc f =
true ->
wf_cond_acc tf =
true.
Proof.
unfold wf_cond_acc.
intros.
apply ptree_forall_true;
intros.
assert (
FIN:
f_In i tf).
unfolds;
intro;
trim.
rewrite forallb_forall;
intros n INS.
unfold Pmem in *.
optDecGN INST;
trim.
assert (
SUCC:
succ_node tf i n).
unfold succ_node.
eexists;
eauto.
eapply transf_succ'
in SUCC;
eauto.
eapply succ_f_In'
in SUCC;
eauto.
eapply transf_f_In'
in SUCC;
eauto.
Qed.
Lemma transf_wf_cond_entry:
wf_cond_entry f =
true ->
wf_cond_entry tf =
true.
Proof.
Definition transf_instr (
p :
node) (
i :
instruction) :
instruction :=
if TheoryList.mem positive_eq_dec p (
_slice_nodes of)
then i else
match i with
|
Icond cond args ifso ifnot =>
update_succs_icond reg_vint'
p ifso ifnot (
_s_dobs of) (
_dexit of)
|
Ireturn o =>
Ireturn o
|
Itailcall sg fn args =>
Ireturn None
|
Ijumptable arg tbl =>
i
|
_ =>
match successor_instr i with
|
Some s =>
Inop s
|
None =>
i
end
end.
Lemma transf_f_instr:
forall p i,
(
fn_code f) !
p =
Some i ->
(
fn_code tf) !
p =
Some (
transf_instr p i).
Proof.
monadInv FOK.
intros.
simpl.
unfold transf_instr.
unfold compute_bs_code;
rewrite PTree.gmap;
unfold option_map;
rewrite H;
auto.
Qed.
Notation in_slice_dec pc of := (
List.In_dec positive_eq_dec pc of.(
_slice_nodes)).
Lemma transf_inc_r_counter:
inc_r_counter_t' =
inc_r_counter'.
Proof.
Lemma inc_r_counter_no_reset_in_slice_eq:
forall pc pc'
cs,
(
forall n,
In n (
exited_scopes fsc pc pc') ->
n <>
nc) ->
pc <>
nc ->
counter_eq' (
inc_r_counter'
pc pc'
cs)
cs.
Proof.
Lemma inc_r_counter_no_reset_in_slice_eq':
forall pc pc'
cs,
(
forall n,
In n (
exited_scopes fsc pc pc') ->
n <>
nc) ->
pc <>
nc ->
counter_eq' (
inc_r_counter_t'
pc pc'
cs)
cs.
Proof.
Lemma silent_step_reset_none_in_slice:
forall pc pc'
(
SUCC:
succ_node f pc pc')
(
PC_OUT : ~
In pc (
_slice_nodes of)),
forall n,
In n (
exited_scopes fsc pc pc') ->
n <>
nc.
Proof.
intros.
intro.
subst n.
eapply scopes_wf_nc with (
f :=
f) (
fsc :=
fsc) (
nc :=
nc) (
pc' :=
pc')
in PC_OUT;
auto.
unfolds in FOK.
monadInv FOK;
auto.
apply EQ.
unfolds in FOK.
monadInv FOK;
auto.
unfolds in EQ.
monadInv EQ.
optDecN EQ1 DOBS;
trim.
optDecN EQ1 RVS;
trim.
optDecN EQ1 SCEX;
trim.
inv EQ1;
auto.
Qed.
Lemma silent_step_reset_none_in_slice':
forall pc pc'
(
SUCC:
succ_node f pc pc')
(
PC_OUT : ~
In pc (
_slice_nodes of)),
forall n,
In n (
exited_scopes tfsc pc pc') ->
n <>
nc.
Proof.
intros.
intro.
subst n.
eapply scopes_wf_nc with (
f :=
f) (
fsc :=
fsc) (
nc :=
nc) (
pc' :=
pc')
in PC_OUT;
auto.
rewrite transf_exited_scopes in H;
trim.
unfolds in FOK.
monadInv FOK.
apply EQ.
generalize FOK;
intros FOK'.
monadInv FOK'.
unfolds in EQ.
monadInv EQ.
optDecN EQ1 DOBS;
trim.
optDecN EQ1 RVS;
trim.
optDecN EQ1 SCEX;
trim.
subst x.
injection EQ1.
intros E;
rewrite <-
E;
simpl.
auto.
Qed.
Lemma inc_counter_silent_step_eq:
forall pc pc'
cs
(
SUCC:
succ_node f pc pc')
(
PC_OUT : ~
In pc (
_slice_nodes of)),
counter_eq nc (
inc_counter pc cs)
cs.
Proof.
Lemma inc_r_counter_silent_step_eq:
forall pc pc'
cs
(
SUCC:
succ_node f pc pc')
(
PC_OUT : ~
In pc (
_slice_nodes of)),
counter_eq nc (
inc_r_counter'
pc pc'
cs)
cs.
Proof.
Lemma inc_r_counter_silent_step_eq':
forall pc pc'
cs
(
SUCC:
succ_node f pc pc')
(
PC_OUT : ~
In pc (
_slice_nodes of)),
counter_eq nc (
inc_r_counter_t'
pc pc'
cs)
cs.
Proof.
Lemma inc_r_counter_silent_step_eq_inv:
forall pc pc'
cs cs'
(
SUCC:
succ_node f pc pc')
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
CEQ:
counter_eq' (
inc_r_counter'
pc pc'
cs)
cs'),
counter_eq'
cs cs'.
Proof.
Ltac MakeUse H :=
match type of H with
| (
fn_code _) !
_ =
Some (
Inop _) =>
exploit use_Inop;
exploit def_Inop;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Iop _ _ _ _) =>
exploit def_Iop;
eauto;
intros DEF
| (
fn_code _) !
_ =
Some (
Iload _ _ _ _ _) =>
exploit use_Iload;
exploit def_Iload;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Istore _ _ _ _ _) =>
exploit use_Istore;
exploit def_Istore;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Icall _ _ _ _ _) =>
exploit use_Icall;
exploit def_Icall;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Itailcall _ _ _) =>
exploit use_Itailcall;
exploit def_Itailcall;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Ibuiltin _ _ _ _) =>
exploit use_Ibuiltin;
exploit def_Ibuiltin;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Icond _ _ _ _) =>
exploit def_Icond;
eauto;
intros DEF
| (
fn_code _) !
_ =
Some (
Ijumptable _ _) =>
exploit use_Ijumptable;
exploit def_Ijumptable;
eauto;
intros DEF USE
| (
fn_code _) !
_ =
Some (
Ireturn _ ) =>
exploit use_Ireturn;
exploit def_Ireturn;
eauto;
intros DEF USE
end.
Ltac renInst :=
match goal with
| [
H: (
fn_code _) !
_ =
Some _ |-
_ ] =>
let N :=
fresh "
INST"
in rename H into N
end.
Lemma transf_icond_true_not_in_slice:
forall pc cond args ifso ifnot d dc dc'
o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
INST' : (
fn_code f) !
pc =
Some (
Icond cond args ifso ifnot))
(
NOBS : (
nobs'
of) !
pc =
Some (
S d,
dc,
o))
(
NOBS' : (
nobs'
of) !
ifso =
Some (
d,
dc',
o)),
(
fn_code tf) !
pc =
Some (
icond_true'
ifso ifnot).
Proof.
Local Open Scope nat_scope.
Lemma transf_icond_false_not_in_slice:
forall pc cond args ifso ifnot d dc dc''
o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
INST' : (
fn_code f) !
pc =
Some (
Icond cond args ifso ifnot))
(
NOBS : (
nobs'
of) !
pc =
Some (
S d,
dc,
o))
(
NOBcstate :
exists d',
exists dc', (
nobs'
of) !
ifso =
Some (
d',
dc',
o) /\ (
d' >
d) \/ (
nobs'
of) !
ifso =
None)
(
NOBS' : (
nobs'
of) !
ifnot =
Some (
d,
dc'',
o)),
(
fn_code tf) !
pc =
Some (
icond_false'
ifso ifnot).
Proof.
Ltac SlicePreserves H :=
match type of H with
| (
fn_code _) !
_ =
Some (
Inop _) =>
eapply slice_preserves_Inop;
eauto
| (
fn_code _) !
_ =
Some (
Iop _ _ _ _) =>
eapply slice_transforms_Iop;
eauto
| (
fn_code _) !
_ =
Some (
Iload _ _ _ _ _) =>
eapply slice_transforms_Iload;
eauto
| (
fn_code _) !
_ =
Some (
Istore _ _ _ _ _) =>
eapply slice_transforms_Istore;
eauto
| (
fn_code _) !
_ =
Some (
Icall _ _ _ _ _) =>
eapply slice_transforms_Icall;
eauto
| (
fn_code _) !
_ =
Some (
Itailcall _ _ _) =>
eapply slice_transforms_Itailcall;
eauto
| (
fn_code _) !
_ =
Some (
Ibuiltin _ _ _ _) =>
eapply slice_transforms_Ibuiltin;
eauto
| (
fn_code _) !
_ =
Some (
Icond _ _ _ _) =>
solve [
eapply slice_transforms_Icond_true;
eauto |
eapply slice_transforms_Icond_false;
eauto]
end.
Ltac FinishCsEq :=
apply counter_eq_sym;
eapply inc_counter_silent_step_eq;
eauto;
unfolds;
eexists;
split;
eauto;
simpl;
auto.
Ltac FinishRcsEq :=
apply counter_eq_sym;
eapply inc_r_counter_silent_step_eq';
eauto;
unfolds;
eexists;
split;
eauto;
simpl;
auto.
Ltac FinishCountersEq :=
split; [
FinishCsEq |
FinishRcsEq].
Lemma silent_step_succ_in_slice:
forall
i m pc pc'
cs rcs rs o dc dc'
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
SUCC'' :
In pc' (
successors_instr i))
(
INST : (
fn_code f) !
pc =
Some i)
(
IN' :
In pc' (
_slice_nodes of))
(
VRS:
valid_rs'
pc rs)
(
NOBS : (
nobs'
of) !
pc =
Some (1,
dc,
o))
(
NOBSPC' : (
nobs'
of) !
pc' =
Some (0,
dc',
o)),
exists cs' :
counter,
exists rcs' :
counter,
plus cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State o rs m)
cs'
rcs') /\
counter_eq'
cs cs' /\
counter_eq'
rcs rcs'.
Proof.
Lemma cstep_succ:
forall f fsc s a,
cstep ge f fsc sp s a ->
succ_node f (
get_pc s) (
get_pc a).
Proof.
Lemma counter_eq_silent_step:
forall
pc pc'
rs rs'
m m'
cs rcs cs'
rcs'
cs''
rcs''
(
CEQS :
counter_eq'
cs cs'')
(
RCEQS:
counter_eq'
rcs rcs'')
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
STEP :
cstep'
ge (
CST (
State pc rs m)
cs rcs)
(
CST (
State pc'
rs'
m')
cs'
rcs')),
counter_eq'
cs'
cs'' /\
counter_eq'
rcs'
rcs''.
Proof.
Lemma counter_eq_silent_step':
forall
pc pc'
rs m cs rcs cs'
rcs'
(
CEQS :
counter_eq' (
inc_counter pc cs)
cs' /\
counter_eq' (
inc_r_counter_t'
pc pc'
rcs)
rcs')
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
SUCC:
succ_node f pc pc')
(
STEP :
cstep_t'
ge (
CST (
State pc rs m)
cs rcs)
(
update_state_counters_t'
pc (
CST (
State pc'
rs m)
cs rcs))),
counter_eq'
cs cs' /\
counter_eq'
rcs rcs'.
Proof.
Lemma cs_eq_step_eq:
forall cs cs'
pc,
counter_eq'
cs cs' ->
counter_eq' (
inc_counter pc cs) (
inc_counter pc cs').
Proof.
Lemma rcs_eq_step_eq:
forall rcs rcs'
pc pc',
counter_eq'
rcs rcs' ->
counter_eq' (
inc_r_counter'
pc pc'
rcs) (
inc_r_counter'
pc pc'
rcs').
Proof.
Lemma rcs_eq_step_eq':
forall rcs rcs'
pc pc',
counter_eq'
rcs rcs' ->
counter_eq' (
inc_r_counter'
pc pc'
rcs) (
inc_r_counter_t'
pc pc'
rcs').
Proof.
Lemma cs_eq_inc_eq:
forall cs cs'
cs''
pc,
counter_eq'
cs cs' ->
counter_eq' (
inc_counter pc cs)
cs'' ->
counter_eq' (
inc_counter pc cs')
cs''.
Proof.
intros cs cs'
cs''
pc EQ EQ'.
unfold inc_counter in *.
unfold counter_eq in *.
destruct (
positive_eq_dec nc pc).
subst pc.
repeat rewrite PMap.gss in *;
auto.
rewrite <-
EQ.
auto.
rewrite <-
EQ'.
repeat rewrite PMap.gso;
auto.
Qed.
Lemma rcs_eq_inc_eq:
forall rcs rcs'
rcs''
pc pc',
counter_eq'
rcs''
rcs ->
counter_eq' (
inc_r_counter_t'
pc pc'
rcs)
rcs' ->
counter_eq' (
inc_r_counter'
pc pc'
rcs'')
rcs'.
Proof.
Lemma valid_rs_ne:
forall pc pc'
rs,
valid_rs'
pc rs ->
pc <>
f.(
fn_entrypoint) ->
valid_rs'
pc'
rs.
Proof.
intros.
unfolds in H.
unfolds.
intro; trim.
Qed.
Lemma silent_steps:
forall
d dc m pc cs rcs rs o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
VRS:
valid_rs'
pc rs)
(
NOBSPC : (
nobs'
of) !
pc =
Some (
d,
dc,
o)),
exists cs',
exists rcs',
(
plus cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State o rs m)
cs'
rcs')) /\
counter_eq'
cs cs' /\
counter_eq'
rcs rcs'.
Proof.
induction d;
intros.
Case "
d = 0 :
distance until observable is zero =>
contradiction".
eapply nobs_zero_in_slice with (
f :=
f) (
nc :=
nc)
in NOBSPC;
eauto.
contra.
Case "
d =
S n".
assert (
NENTRY:
pc <> (
fn_entrypoint f)).
intro.
subst pc.
apply PC_OUT.
eapply entry_in_slice;
eauto.
dup NOBSPC NOBS.
eapply nobs_non_zero_ex_succ in NOBSPC;
eauto.
destruct NOBSPC as [
pc' [
dc' [
SUCC'
NOBSPC']]].
destruct (
in_slice_dec pc'
of).
SCase "
succ in slice => 1
step".
clear IHd.
dup NOBSPC'
DIcstate.
eapply nobs_in_slice_zero in DIcstate;
eauto;
trim.
subst d.
unfolds in SUCC'.
destruct SUCC'
as [
i' [
INST'
SUCC'']].
eapply silent_step_succ_in_slice;
eauto.
SCase "
succ not in slice =>
plus step".
dup SUCC'
SUCCI.
unfolds in SUCCI.
destruct SUCCI as [
i [
I SUCCS]].
destruct i;
simpl in SUCCS;
trim;
try (
destruct SUCCS;
trim;
subst n0;
dup n HI;
eapply IHd in HI;
eauto);
try (
destruct HI as [
cs' [
rcs' [
STEPS CEQS]]];
assert (
STEP_EX:
cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
update_state_counters_t'
pc (
CST (
State pc'
rs m)
cs rcs)))
by
(
eapply cstep_def;
eauto;
apply exec_Inop;
SlicePreserves I);
eexists;
eexists;
split;
[
eapply plus_left'; [
apply STEP_EX |
apply STEPS]
|
eapply counter_eq_silent_step';
eauto]
);
try solve [
apply STEP_EX];
try (
eapply valid_rs_ne;
eauto).
SSCase "
Icond".
destruct SUCCS.
SSSCase "
Icond_true".
subst n0.
dup PC_OUT H'.
eapply transf_icond_true_not_in_slice in H';
eauto.
dup n HI;
eapply IHd in HI;
eauto.
destruct HI as [
cs' [
rcs' [
STEPS CEQS]]];
assert (
STEP_EX:
cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
update_state_counters_t'
pc (
CST (
State pc'
rs m)
cs rcs))).
eapply cstep_def;
eauto.
eapply exec_Icond;
eauto.
eapply eval_icond_true;
eauto.
auto.
eexists;
eexists;
split;
[
eapply plus_left'; [
apply STEP_EX |
apply STEPS]
|
eapply counter_eq_silent_step';
eauto].
apply STEP_EX.
eapply valid_rs_ne;
eauto.
SSSCase "
Icond_false".
destruct H;
trim.
subst n1.
dup SUCC'
SUCC'
_.
rename n0 into ifso,
pc'
into ifnot.
assert (
SUCC:
succ_node f pc ifso).
now (
exists (
Icond c l ifso ifnot);
split;
simpl;
auto).
case_eq ((
nobs'
of) !
ifso);
introsv NOBS'.
destruct p as [[
d'
dc'']
o'].
assert (
o' =
o).
eapply nobs_some_succ_eq with (
pc :=
pc);
eauto.
subst o'.
exploit nobs_succ_minus_one;
eauto;
introsv N1.
unfolds in N1.
destruct N1.
SSSSCase "
nobs ifso =
nobs ifnot".
destruct d.
SSSSSCase "
nobs(
ifnot) = 0 (
contradiction)".
eapply nobs_zero_in_slice in NOBSPC';
eauto.
contra.
SSSSSCase "
nobs(
ifnot) > 0 ->
ifso choisie".
assert (
IFSO_OUT: ~
In ifso (
_slice_nodes of)).
now (
eapply nobs_not_zero_not_in_slice;
eauto).
assert (
ITRANSF: (
fn_code tf) !
pc =
Some (
icond_true'
ifso ifnot)).
eapply transf_icond_true_not_in_slice;
eauto.
dup IFSO_OUT HI;
eapply IHd in HI;
eauto;
try (
eapply valid_rs_ne;
eauto);
destruct HI as [
cs' [
rcs' [
STEPS CEQS]]].
assert (
STEP_EX:
cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
update_state_counters_t'
pc (
CST (
State ifso rs m)
cs rcs))).
eapply cstep_def;
eauto.
eapply exec_Icond;
eauto.
eapply eval_icond_true;
eauto.
auto.
eexists;
eexists;
split;
[
eapply plus_left'; [
apply STEP_EX |
apply STEPS]
|
eapply counter_eq_silent_step';
eauto].
apply STEP_EX.
SSSSCase "
nobs ifso >
nobs ifnot ->
ifnot chosen".
assert (
ITRANSF: (
fn_code tf) !
pc =
Some (
icond_false'
ifso ifnot)).
eapply transf_icond_false_not_in_slice;
eauto.
exists (
S m0).
exists dc''.
left.
split;
auto.
lia2.
dup n HI;
eapply IHd in HI;
eauto;
try (
eapply valid_rs_ne;
eauto);
destruct HI as [
cs' [
rcs' [
STEPS CEQS]]].
assert (
STEP_EX:
cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
update_state_counters_t'
pc (
CST (
State ifnot rs m)
cs rcs))).
eapply cstep_def;
eauto.
eapply exec_Icond;
eauto.
eapply eval_icond_false;
eauto.
auto.
eexists;
eexists;
split;
[
eapply plus_left'; [
apply STEP_EX |
apply STEPS]
|
eapply counter_eq_silent_step';
eauto].
apply STEP_EX.
SSSSCase "
obs ifso =
None =>
Inop ifnot".
assert (
ITRANSF: (
fn_code tf) !
pc =
Some (
icond_false'
ifso ifnot)).
eapply transf_icond_false_not_in_slice;
eauto.
Existential 1 := 0.
Existential 1 := 0.
dup n HI;
eapply IHd in HI;
eauto;
try (
eapply valid_rs_ne;
eauto);
destruct HI as [
cs' [
rcs' [
STEPS CEQS]]].
assert (
STEP_EX:
cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
update_state_counters_t'
pc (
CST (
State ifnot rs m)
cs rcs))).
eapply cstep_def;
eauto.
eapply exec_Icond;
eauto.
eapply eval_icond_false;
eauto.
auto.
eexists;
eexists;
split;
[
eapply plus_left'; [
apply STEP_EX |
apply STEPS]
|
eapply counter_eq_silent_step';
eauto].
apply STEP_EX.
SSCase "
Ijumptable (
contradiction:
should be in the slice)".
eapply slice_includes_Ijumptable in I;
eauto.
contra.
Qed.
Hint Immediate succ_no_def_agree.
Lemma no_step_entry:
forall f fsc pc rs m cs rcs rs'
m'
cs'
rcs'
exit_n reg_vint
(
WFF:
check_wf f =
OK (
exit_n,
reg_vint)),
~
cstep ge f fsc sp (
CST (
State pc rs m)
cs rcs) (
CST (
State (
entry f)
rs'
m')
cs'
rcs').
Proof.
Lemma no_step_t_entry:
forall pc rs m cs rcs rs'
m'
cs'
rcs',
~
cstep ge tf tfsc sp (
CST (
State pc rs m)
cs rcs) (
CST (
State (
entry tf)
rs'
m')
cs'
rcs').
Proof.
Lemma star_step_entry:
forall f fsc s s'
exit_n reg_vint
(
WFF:
check_wf f =
OK (
exit_n,
reg_vint)),
star (
fun ge =>
cstep ge f fsc sp)
ge s s' ->
get_pc s' =
entry f ->
s =
s'.
Proof.
induction 2;
intros;
trim.
destruct s3.
simpls.
rewrite H1 in *.
specialize (
IHstar eq_refl).
subst s2.
destruct get_st.
simpls.
subst pc.
destruct s1.
destruct get_st.
eapply no_step_entry in H;
eauto;
trim.
Qed.
Lemma star_step_t_entry:
forall s s'
exit_n reg_vint
(
WFF:
check_wf f =
OK (
exit_n,
reg_vint)),
star (
fun ge =>
cstep ge tf tfsc sp)
ge s s' ->
get_pc s' =
entry tf ->
s =
s'.
Proof.
induction 2;
intros;
trim.
destruct s3.
simpls.
rewrite H1 in *.
specialize (
IHstar eq_refl).
subst s2.
destruct get_st.
simpls.
subst pc.
destruct s1.
destruct get_st.
eapply no_step_t_entry in H;
eauto;
trim.
Qed.
Lemma no_plus_step_entry:
forall pc rs m cs rcs rs'
m'
cs'
rcs',
~
plus cstep'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State (
entry f)
rs'
m')
cs'
rcs').
Proof.
Lemma no_plus_step_t_entry:
forall pc rs m cs rcs rs'
m'
cs'
rcs',
~
plus cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State (
entry f)
rs'
m')
cs'
rcs').
Proof.
Lemma no_entry_step:
forall pc rs m cs rcs pc'
rs'
m'
cs'
rcs',
cstep'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs') ->
pc' <>
entry f.
Proof.
Auxiliary lemma for Iconds and Inops.
Lemma nobs_no_def_step:
forall cs rcs pc pc0 cs'
rcs'
pc'
rs rs'
m m'
o
(
PC_OUT : ~
In pc (
_slice_nodes of))
(
OBSPC :
s_obs of pc =
Some o)
(
VRS:
rs #
reg_vint' =
Vint Int.zero)
(
SUCC :
succ_node f pc pc')
(
PC'
_OUT : ~
In pc0 (
_slice_nodes of))
(
OBSPC' :
s_obs of pc0 =
Some o)
(
AGREE :
rvs_agree'
pc (
rvs of pc)
rs'
rs m'
m)
(
COUNTERS :
counter_eq'
cs cs')
(
RCOUNTERS :
counter_eq'
rcs rcs')
(
DEF :
def f pc =
Regset.empty),
exists s2' :
cstate,
star cstep_t'
ge
(
CST (
State pc0 rs m)
cs'
rcs')
s2' /\
match_states (
update_state_counters'
pc (
CST (
State pc'
rs'
m')
cs rcs))
s2'.
Proof.
Lemma transf_f_preserves_instructions:
forall pc i
(
INST : (
fn_code f) !
pc =
Some i)
(
PC_IN :
In pc (
_slice_nodes of)),
(
fn_code tf) !
pc =
Some i.
Proof.
Lemma step_nexit_ge_minus_one:
forall
dx pc cs rcs rs m pc'
cs'
rcs'
rs'
m'
(
NEXIT : (
nexit'
of) !
pc =
Some (
S dx))
(
STEP :
cstep'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs')),
exists dx',
(
nexit'
of) !
pc' =
Some dx' /\
dx' >=
dx.
Proof.
Lemma none_step_t_nexit_minus_one:
forall
dx pc cs rcs rs m
(
FIN :
f_In pc f)
(
NEXIT : (
nexit'
of) !
pc =
Some (
S dx))
(
VRS:
valid_rs'
pc rs)
(
OBS :
s_obs of pc =
None),
exists s' :
cstate,
cstep_t'
ge (
CST (
State pc rs m)
cs rcs)
s' /\
s_obs of (
get_pc s') =
None /\ (
nexit'
of) ! (
get_pc s') =
Some dx.
Proof.
Lemma transf_inst_preserved:
forall n i
(
TINST: (
fn_code tf) !
n =
Some i)
(
NOTR:
match i with
|
Inop _ =>
False
|
Icond _ _ _ _ =>
False
|
Ireturn _ =>
False
|
_ =>
True
end),
(
fn_code f) !
n =
Some i.
Proof.
intros.
monadInv FOK;
monadInv EQ;
optDecN EQ1 DOBS;
trim;
optDecN EQ1 RVS;
trim;
optDecN EQ1 SCEX;
trim.
simpl in TINST.
unfold compute_bs_code in TINST.
rewrite PTree.gmap in TINST;
unfold option_map in TINST.
optDecN TINST TINST';
optDecN TINST TINST'';
trim.
inv TINST.
destruct i0;
simpls;
trim.
unfold update_succs_icond in NOTR.
repeat optDec NOTR;
destruct_pairs;
try optDec NOTR;
simpls;
trim.
Qed.
Lemma valid_rs_function_step_t:
forall
pc rs m cs rcs pc'
rs'
m'
cs'
rcs'
(
NE:
pc <>
entry f)
(
VRS:
valid_rs'
pc rs)
(
STEP:
cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs')),
valid_rs'
pc'
rs'.
Proof.
Lemma none_star_step_nexit_zero:
forall
dx pc cs rcs rs m
(
FIN :
f_In pc f)
(
NEXIT : (
nexit'
of) !
pc =
Some dx)
(
OBS :
s_obs of pc =
None)
(
VRS:
valid_rs'
pc rs),
exists pc',
exists cs',
exists rcs',
exists rs',
exists m',
star cstep_t'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs') /\
s_obs of pc' =
None /\
pc' =
exit_n' /\
valid_rs'
pc'
rs' /\
counter_eq'
cs cs' /\
counter_eq'
rcs rcs'.
Proof.
Lemma star_step_t_f_In':
forall s s',
f_In (
get_pc (
get_st s))
tf ->
star cstep_t'
ge s s' ->
f_In (
get_pc (
get_st s'))
tf.
Proof.
induction 2;
intros;
trim.
apply IHstar.
apply cstep_succ in H0.
eapply transf_succ'
in H0;
eauto.
eapply succ_f_In'
in H0;
eauto.
eapply transf_f_In';
eauto.
Qed.
Lemma succ_no_entry:
forall pc pc',
succ_node'
pc pc' ->
pc' <>
entry f.
Proof.
intros.
intro.
subst pc'.
eapply wf_entry in H;
eauto.
Qed.
Lemma nexit_eq:
exit_n =
exit_n'.
Proof.
Lemma none_steps:
forall
dx pc cs rcs cs'0
rcs'0
pc'
cs'
rcs'
rs rs'
rs'0
m m'
m'0
(
COUNTERS :
counter_eq'
cs cs'0)
(
RCOUNTERS :
counter_eq'
rcs rcs'0)
(
STEP :
cstep'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs'))
(
NEXIT : (
nexit'
of) !
pc =
Some dx)
(
VRS:
valid_rs'
pc rs)
(
VRS':
valid_rs'
pc rs'0)
(
OBS :
s_obs of pc =
None),
exists s2' :
cstate,
star cstep_t'
ge (
CST (
State exit_n rs'0
m'0)
cs'0
rcs'0)
s2' /\
match_states (
CST (
State pc'
rs'
m')
cs'
rcs')
s2'.
Proof.
Ltac AutoStep H :=
match type of H with
| (
fn_code _) !
_ =
Some (
Inop _) =>
eapply exec_Inop;
eauto
| (
fn_code _) !
_ =
Some (
Iop _ _ _ _) =>
eapply exec_Iop;
eauto
| (
fn_code _) !
_ =
Some (
Iload _ _ _ _ _) =>
eapply exec_Iload;
eauto
| (
fn_code _) !
_ =
Some (
Istore _ _ _ _ _) =>
eapply exec_Istore;
eauto
| (
fn_code _) !
_ =
Some (
Icall _ _ _ _ _) =>
eapply exec_Icall;
eauto
| (
fn_code _) !
_ =
Some (
Itailcall _ _ _) =>
eapply exec_Itailcall;
eauto
| (
fn_code _) !
_ =
Some (
Ibuiltin _ _ _ _) =>
eapply exec_Ibuiltin;
eauto
| (
fn_code _) !
_ =
Some (
Icond _ _ _ _) =>
eapply exec_Icond;
eauto
| (
fn_code _) !
_ =
Some (
Ijumptable _ _) =>
eapply exec_Ijumptable;
eauto
| (
fn_code _) !
_ =
Some (
Ireturn _ ) =>
eapply exec_Ireturn;
eauto
end.
Ltac AutoAgreePreserves H pc :=
match type of H with
| (
fn_code _) !
_ =
Some (
Iop _ _ _ _) =>
erewrite agree_preserves_slice_eval_op;
eauto
| (
fn_code _) !
_ =
Some (
Iload _ _ _ _ _) =>
erewrite agree_preserves_slice_load_eval_addr;
eauto
| (
fn_code _) !
_ =
Some (
Istore _ _ _ _ _) =>
erewrite agree_preserves_slice_store_eval_addr;
eauto
| (
fn_code _) !
_ =
Some (
Ibuiltin _ _ _ _) =>
eapply agree_preserves_external_call'
with (
pc :=
pc);
eauto
| (
fn_code _) !
_ =
Some (
Icond _ _ _ _) =>
erewrite agree_preserves_slice_eval_cond;
eauto
end.
Lemma in_slice_iop_agree:
forall pc rs m'
cs rcs pc'
op args res v rs'0
m'0
(
PC_IN :
In pc (
_slice_nodes of))
(
INST : (
fn_code f) !
pc =
Some (
Iop op args res pc'))
(
EVAL :
eval_operation ge sp op rs ##
args m' =
Some v)
(
AGREE :
rvs_agree'
pc ((
rvs of)
pc)
rs rs'0
m'
m'0)
(
_STEP_ :
cstep'
ge (
CST (
State pc rs m')
cs rcs)
(
CST (
State pc'
rs #
res <-
v m') (
inc_counter pc cs)
(
inc_r_counter'
pc pc'
rcs)))
(
DEF :
def f pc =
Regset.singleton (
reg_to_var res)),
rvs_agree'
pc' ((
rvs of)
pc')
rs #
res <-
v rs'0 #
res <-
v m'
m'0.
Proof.
Definition def_r (
i :
instruction) :
option reg :=
match i with
|
Iop _ _ res _ =>
Some res
|
Iload _ _ _ dst _ =>
Some dst
|
Icall _ _ _ res _ =>
Some res
|
Ibuiltin _ _ res _ =>
Some res
|
_ =>
None
end.
Lemma def_r_in_def:
forall n i r,
(
fn_code f) !
n =
Some i ->
def_r i =
Some r ->
Regset.In (
reg_to_var r) (
def f n).
Proof.
Lemma valid_rs_after:
forall
pc rs i m res v
(
VRS :
valid_rs'
pc rs)
(
INST : (
fn_code f) !
pc =
Some i)
(
DEFR:
def_r i =
Some res)
(
NENTRY:
pc =
entry f ->
match i with
|
Iop op args res'
_ =>
res' =
res /\
eval_operation ge sp op rs ##
args m =
Some v
|
_ =>
False
end),
rs #
res <-
v #
reg_vint' =
Vint Int.zero.
Proof.
Lemma valid_rs_assigned:
forall
pc rs v d
(
FIN:
f_In pc f)
(
VRS:
valid_rs'
pc rs)
(
IN_DEF:
Regset.In (
reg_to_var d) (
def f pc)),
valid_rs'
pc rs #
d <-
v.
Proof.
intros pc rs v d FIN VRS IN_DEF NOTE.
dup NOTE NOTE'.
apply VRS in NOTE.
dup WFF DNE.
apply def_not_entry with (
n :=
pc)
in DNE;
auto.
rewrite PMap.gso;
auto.
intro.
subst d.
elim DNE.
erewrite reg_vint_eq in IN_DEF;
eauto.
Qed.
Lemma agree_ne_pc:
forall
pc pc'
rs rs'
m m'
pc''
(
NE:
pc' <>
entry f)
(
NE':
pc'' <>
entry f)
(
AGREE :
rvs_agree'
pc' ((
rvs of)
pc)
rs rs'
m m'),
rvs_agree'
pc'' ((
rvs of)
pc)
rs rs'
m m'.
Proof.
intros.
unfold rvs_agree in *.
destruct AGREE as [RVS [RVS' AGREE]].
unfold valid_rs in *.
trim.
Qed.
Ltac ConditionalClear INST IN_SC :=
match type of INST with
| (
fn_code _) !
_ =
Some (
Icond _ _ _ _) =>
idtac
|
_ =>
clear IN_SC
end.
Ltac ApplyButToIbuiltin INST tac :=
match type of INST with
| (
fn_code _) !
_ =
Some (
Ibuiltin _ _ _ _) =>
idtac
|
_ =>
tac
end.
Lemma transf_step:
forall cs rcs pc rs m cs'
rcs'
pc'
rs'
m',
cstep'
ge (
CST (
State pc rs m)
cs rcs) (
CST (
State pc'
rs'
m')
cs'
rcs') ->
forall s1' (
MS:
match_states (
CST (
State pc rs m)
cs rcs)
s1'),
exists s2',
star cstep_t'
ge s1'
s2' /\
match_states (
CST (
State pc'
rs'
m')
cs'
rcs')
s2'.
Proof.
introsv STEP MS.
assert (
FIN' :
f_In pc'
f).
dup STEP SUCC.
apply cstep_succ in SUCC.
eapply succ_f_In'
in SUCC;
eauto.
dup STEP _STEP_.
exploit cstep_succ;
eauto.
intro SUCC.
simpl in SUCC.
inv_clear MS;
subst pc0 rs0 m0 cs0 rcs0 s1'.
Case "
ms1".
simpl in AGREE.
destruct (
in_slice_dec pc'
of)
as [
IN_SC|
OUT_SC].
SCase "
succ in slice =>
step +
ms1".
Ltac SolveStarStep'
INST :=
eexists;
split; [
apply star_one;
simpls;
eapply cstep_def;
eauto;
AutoStep INST; [
eapply transf_f_preserves_instructions;
eauto|..]|..].
Ltac AutoStepOne INST :=
apply star_one;
simpls;
eapply cstep_def;
eauto;
AutoStep INST;
[
eapply transf_f_preserves_instructions;
eauto|..].
Ltac SolveEntry pc' :=
intro;
subst pc';
exploit no_step_entry;
eauto;
trim.
Ltac CountersEq'' :=
try solve [
apply cs_eq_step_eq;
auto |
apply rcs_eq_step_eq';
auto].
inv STEP.
Ltac MatchRvsAgree INST :=
match type of INST with
| (
fn_code _) ! ?
p =
Some (
Iop _ _ _ _) =>
eapply in_slice_iop_agree with (
pc :=
p);
eauto
| (
fn_code _) ! ?
p =
Some (
Iload _ _ _ _ _) =>
eapply load_in_preserves_agree with (
pc :=
p);
eauto
| (
fn_code _) !
_ =
Some (
Istore _ _ _ _ _) =>
eapply store_preserves_agree;
eauto
| (
fn_code _) !
_ =
Some (
Ibuiltin _ _ _ _) =>
eapply builtin_preserves_agree;
eauto
end.
Ltac StepAgreeIop p :=
eapply in_slice_iop_agree with (
pc :=
p);
eauto.
Ltac StepAgreeIload AGREE USE :=
eapply agree_preserves_used_mem in AGREE;
eauto;
subst;
eauto;
rewrite USE;
apply Regset.add_1;
auto.
Ltac StepAgreeIstore :=
eapply agree_preserves_storev;
eauto.
Ltac StepAgreeIbuiltin e :=
eapply agree_preserves_external_call'
with (
ef :=
e);
eauto.
Ltac StepAgreeIjumptable :=
erewrite jumptable_preserves_agree;
eauto.
Ltac SolveMs1 INST pc pc' :=
eexists;
split;
try AutoStepOne INST;
try AutoAgreePreserves INST pc;
try eapply ms1 with (
o :=
pc');
eauto;
try CountersEq'';
try SolveEntry pc';
try MatchRvsAgree INST.
assert (
EXO:
s_obs of pc' =
Some pc')
by (
eapply in_slice_s_obs_refl;
eauto).
inv H3;
renInst;
MakeUse INST;
try ApplyButToIbuiltin INST ltac:(
SolveMs1 INST pc pc').
SSCase "
Iload".
StepAgreeIload AGREE USE.
SSCase "
Istore".
StepAgreeIstore.
SSCase "
Ibuiltin".
destruct (
is_builtin_annot_dec ef)
as [
ISA|
NOTA].
SSSCase "
is_builtin_annot".
unfolds in ISA.
destruct ef;
trim.
eexists;
split.
try AutoStepOne INST.
eapply agree_preserves_external_call'
with (
ef :=
EF_annot text targs) (
pc :=
pc) (
m' :=
m');
eauto;
simpl;
eauto.
eapply ms1 with (
o :=
pc');
eauto; [
CountersEq''|
CountersEq''|..].
SolveEntry pc'.
inv H8.
eapply annot_preserves_agree with (
pc :=
pc);
eauto.
eexists;
split.
try AutoStepOne INST.
eapply agree_preserves_external_call'
with (
ef :=
EF_annot_val text targ) (
pc :=
pc) (
m' :=
m');
eauto;
simpl;
eauto.
eapply ms1 with (
o :=
pc');
eauto; [
CountersEq''|
CountersEq''|..].
SolveEntry pc'.
inv H8.
eapply annot_preserves_agree with (
pc :=
pc);
eauto.
SSSCase "~
is_builtin_annot".
Ltac AutoBuiltin H :=
match type of H with
| (
fn_code _) ! ?
p =
Some (
Ibuiltin ?
e _ _ _) =>
match e with
|
_ =>
eapply agree_preserves_external_call'
with (
ef :=
e) (
pc :=
p);
eauto;
simpl;
eauto
end
end.
destruct ef;
eexists;
split;
try AutoStepOne INST;
try (
AutoBuiltin INST);
try (
eapply ms1 with (
o :=
pc');
eauto; [
CountersEq''|
CountersEq''|..]);
try SolveEntry pc';
try (
eapply builtin_preserves_agree with (
pc :=
pc);
eauto).
eelim NOTA;
simpl;
eauto.
eelim NOTA;
simpl;
eauto.
SSCase "
Icond".
destruct b;
simpls.
SSSCase "
Icond_true".
eexists.
split.
AutoStepOne INST.
AutoAgreePreserves INST pc.
eapply ms1 with (
o :=
ifso);
eauto;
CountersEq''.
SolveEntry ifso.
SSSCase "
Icond_false".
eexists.
split.
AutoStepOne INST.
AutoAgreePreserves INST pc.
eapply ms1 with (
o :=
ifnot);
eauto;
CountersEq''.
SolveEntry ifnot.
SSCase "
Ijumptable".
erewrite jumptable_preserves_agree;
eauto.
SCase "
succ not in slice => 2
cases".
Ltac CaseRegVint pc EINST INST m' :=
eapply valid_rs_after with (
m :=
m');
eauto;
intro;
subst pc;
eauto;
rewrite EINST in INST;
inv INST;
auto.
dup WFF VRSF.
case_eq (
s_obs of pc');
introsv OBSPC'.
inv STEP.
SSCase "
obs(
succ) =
Some =>
step +
ms2".
Ltac AutoStepMs2 INST pc m'
DEF AGREE VRSF :=
try AutoAgreePreserves INST pc;
dup AGREE AGREE';
unfolds in AGREE;
destruct AGREE as [
RVS [
RVS'
AGREE]];
let EINST :=
fresh "
EINST"
in
dup VRSF EINST;
eapply entry_inst in EINST;
eauto;
destruct EINST as [
s EINST];
try solve [
CaseRegVint pc EINST INST m'];
try (
assert (
NENTRY:
pc <> (
fn_entrypoint f))
by
(
intro;
subst pc;
unfold def in DEF;
rewrite EINST in DEF;
simpl in DEF;
inv DEF;
lia2));
try solve [
apply RVS;
auto |
apply RVS';
auto].
Ltac SolveMs1Ms2 INST n pc m'
DEF AGREE VRSF :=
eexists;
split;
try AutoStepOne INST;
try eapply ms2 with (
o :=
n);
eauto;
CountersEq'';
try AutoAgreePreserves INST pc;
AutoStepMs2 INST pc m'
DEF AGREE VRSF.
inv H3;
renInst;
MakeUse INST;
ApplyButToIbuiltin INST ltac:(
SolveMs1Ms2 INST n pc m'
DEF AGREE VRSF).
SSSCase "
Iop".
MatchRvsAgree INST.
SSSCase "
Iload".
StepAgreeIload AGREE'
USE.
MatchRvsAgree INST.
SSSCase "
Istore".
StepAgreeIstore.
MatchRvsAgree INST.
SSSCase "
Ibuiltin".
destruct (
is_builtin_annot_dec ef)
as [
ISA|
NOTA].
SSSSCase "
is_builtin_annot".
unfolds in ISA;
destruct ef;
trim.
eexists.
split.
AutoStepOne INST.
eapply agree_preserves_external_call'
with
(
ef :=
EF_annot text targs) (
pc :=
pc) (
m' :=
m');
eauto;
simpl;
eauto.
eapply ms2 with (
o :=
n);
eauto;
CountersEq'';
AutoStepMs2 INST pc m'
DEF AGREE VRSF.
inv H8.
eapply annot_preserves_agree with (
pc :=
pc);
eauto.
eexists;
split.
AutoStepOne INST.
eapply agree_preserves_external_call'
with
(
ef :=
EF_annot_val text targ) (
pc :=
pc) (
m' :=
m');
eauto;
simpl;
eauto.
eapply ms2 with (
o :=
n);
eauto;
CountersEq'';
AutoStepMs2 INST pc m'
DEF AGREE VRSF.
inv H8.
eapply annot_preserves_agree with (
pc :=
pc);
eauto.
SSSSCase "~
is_builtin_annot".
eexists.
split.
AutoStepOne INST.
destruct ef;
eapply agree_preserves_external_call'
in H8;
eauto.
eelim NOTA;
simpl;
eauto.
eelim NOTA;
simpl;
eauto.
eapply ms2 with (
o :=
n);
eauto;
CountersEq'';
AutoStepMs2 INST pc m'
DEF AGREE VRSF.
eapply builtin_preserves_agree;
eauto.
SSSCase "
Ijumptable".
erewrite jumptable_preserves_agree;
eauto.
Ltac SolveMs1Ms3 INST p p'
m'
DEF AGREE VRSF :=
SolveStarStep'
INST;
try (
eapply ms3 with (
pc :=
p');
eauto;
CountersEq'');
try AutoAgreePreserves INST p;
dup AGREE AGREE';
unfolds in AGREE;
destruct AGREE as [
RVS [
RVS'
AGREE]];
let EINST :=
fresh "
EINST"
in
dup VRSF EINST;
eapply entry_inst in EINST;
eauto;
destruct EINST as [
s EINST];
try solve [
CaseRegVint p EINST INST m'];
try (
assert (
NENTRY:
p <> (
fn_entrypoint f))
by
(
intro;
subst p;
unfold def in DEF;
rewrite EINST in DEF;
simpl in DEF;
inv DEF;
lia2));
try solve [
apply RVS;
auto |
apply RVS';
auto].
SSCase "
obs(
succ) =
None =>
step +
ms3".
gen s_dobs_checker_ok as OBSC.
dup OBSPC'
NOBSPC'.
apply s_obs_nobs'
in NOBSPC'.
apply checked_has_nexit with (
n :=
pc')
in OBSC;
auto.
destruct OBSC as [
dx NEXIT].
destruct (
positive_eq_dec pc (
entry f))
as [
ISE|
NOTE].
SSSCase "
pc =
entry f".
subst pc.
exploit entry_inst;
eauto;
intros (
s &
EINST).
inv STEP.
inv H3;
renInst;
rewrite EINST in INST;
inversion INST.
subst op args res s.
exploit none_star_step_nexit_zero;
eauto;
intro STEPS.
apply PMap.gss.
erewrite reg_vint_eq in STEPS;
eauto.
decs STEPS.
eexists.
split.
eapply star_left.
eapply cstep_def;
eauto.
eapply exec_Iop;
eauto.
apply transf_f_preserves_instructions;
eauto.
eauto.
simpls.
inv H8.
eauto.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq;
eauto.
erewrite reg_vint_eq;
eauto.
inv H8.
apply PMap.gss.
erewrite reg_vint_eq;
eauto.
eapply H2.
subst.
apply not_eq_sym.
apply exit_no_entry.
SSSCase "
pc <>
entry f".
Ltac StepsMs1Ms3 INST STEPS :=
eapply star_left; [
eapply cstep_def;
eauto;
AutoStep INST;
try apply transf_f_preserves_instructions;
eauto|..];
try apply STEPS.
assert (
VRS'0:
valid_rs'
pc'
rs'0).
unfolds in AGREE.
destruct AGREE as (
_ &
VRS0 &
_).
eapply valid_rs_ne;
eauto.
inv STEP;
inv H3;
renInst;
MakeUse INST.
SSSSCase "
Inop".
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq in RCS';
eauto.
apply AGREE;
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
SSSSCase "
Iop".
assert (
VRS'':
valid_rs'
pc'
rs'0 #
res <-
v).
apply valid_rs_ne with (
pc' :=
pc)
in VRS'0;
eauto.
apply valid_rs_assigned with (
v :=
v) (
d :=
res)
in VRS'0.
eapply valid_rs_ne;
eauto.
unfold f_In;
intro;
trim.
unfold def;
rewrite INST;
apply regset_in_singleton.
eapply succ_no_entry;
eauto.
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
AutoAgreePreserves INST pc.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq;
eauto.
rewrite PMap.gso.
apply AGREE;
auto.
intro.
subst res.
dup WFF DNE.
eapply def_not_entry with (
n :=
pc)
in DNE;
eauto.
elim DNE.
rewrite DEF.
erewrite reg_vint_eq;
eauto.
apply regset_in_singleton.
unfold f_In;
intros;
trim.
apply VRS0.
apply sym_not_eq.
apply exit_no_entry.
SSSSCase "
Iload".
assert (
VRS'':
valid_rs'
pc'
rs'0 #
dst <-
v).
apply valid_rs_ne with (
pc' :=
pc)
in VRS'0;
eauto.
apply valid_rs_assigned with (
v :=
v) (
d :=
dst)
in VRS'0.
eapply valid_rs_ne;
eauto.
unfold f_In;
intro;
trim.
unfold def;
rewrite INST;
apply regset_in_singleton.
eapply succ_no_entry;
eauto.
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
AutoAgreePreserves INST pc.
StepAgreeIload AGREE USE.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq;
eauto.
rewrite PMap.gso.
apply AGREE;
auto.
intro.
subst dst.
dup WFF DNE.
eapply def_not_entry with (
n :=
pc)
in DNE;
eauto.
elim DNE.
rewrite DEF.
erewrite reg_vint_eq;
eauto.
apply regset_in_singleton.
unfold f_In;
intros;
trim.
apply VRS0.
apply sym_not_eq.
apply exit_no_entry.
SSSSCase "
Istore".
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
AutoAgreePreserves INST pc.
StepAgreeIstore.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq in RCS';
eauto.
apply AGREE;
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
SSSSCase "
Ibuiltin".
assert (
VRS'':
valid_rs'
pc'
rs'0 #
res <-
v).
apply valid_rs_ne with (
pc' :=
pc)
in VRS'0;
eauto.
apply valid_rs_assigned with (
v :=
v) (
d :=
res)
in VRS'0.
eapply valid_rs_ne;
eauto.
unfold f_In;
intro;
trim.
unfold def;
rewrite INST.
destruct ef;
try apply Regset.add_2;
apply regset_in_singleton.
eapply succ_no_entry;
eauto.
destruct (
is_builtin_annot_dec ef)
as [
ISA|
NOTA].
SSSSSCase "
is_builtin_annot".
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
destruct ef;
elim ISA;
AutoBuiltin INST.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq;
eauto.
rewrite PMap.gso.
apply AGREE;
auto.
intro.
subst res.
dup WFF DNE.
eapply def_not_entry with (
n :=
pc)
in DNE;
eauto.
elim DNE.
rewrite DEF.
erewrite reg_vint_eq;
eauto.
destruct ef;
try apply Regset.add_2;
apply regset_in_singleton.
unfold f_In;
intros;
trim.
apply VRS0.
apply sym_not_eq.
apply exit_no_entry.
SSSSSCase "~
is_builtin_annot".
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
destruct ef;
try solve [
elim NOTA;
simpl;
auto];
AutoBuiltin INST.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq;
eauto.
rewrite PMap.gso.
apply AGREE;
auto.
intro.
subst res.
dup WFF DNE.
eapply def_not_entry with (
n :=
pc)
in DNE;
eauto.
elim DNE.
rewrite DEF.
erewrite reg_vint_eq;
eauto.
destruct ef;
try apply Regset.add_2;
apply regset_in_singleton.
unfold f_In;
intros;
trim.
apply VRS0.
apply sym_not_eq.
apply exit_no_entry.
SSSSCase "
Icond".
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
AutoAgreePreserves INST pc.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq in RCS';
eauto.
apply AGREE;
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
SSSSCase "
Ijumptable".
exploit none_star_step_nexit_zero;
eauto.
intros (
pc'0 &
cs' &
rcs' &
rs'' &
m'' &
STEPS &
OBSPC0 &
EXIT0 &
VRS0 &
CS0 &
RCS').
eexists;
split.
StepsMs1Ms3 INST STEPS.
StepAgreeIjumptable.
subst pc'0.
apply ms3;
auto.
eapply cs_eq_inc_eq;
eauto.
eapply rcs_eq_inc_eq in RCS';
eauto.
apply AGREE;
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
auto;
apply VRS0;
intro;
apply cstep_succ in _STEP_;
apply exit_no_entry;
eauto.
Case "
ms2".
destruct (
in_slice_dec pc'
of)
as [
IN_SC|
OUT_SC].
SCase "
succ in slice =>
plus step +
ms1".
dup OBSPC OBS.
dup OBSPC'
OBS'.
apply s_obs_nobs in OBSPC.
destruct OBSPC as [
d [
dc NOBSPC]].
apply s_obs_nobs in OBSPC'.
destruct OBSPC'
as [
d' [
dc'
NOBSPC']].
assert (
pc' =
o).
eapply in_slice_s_obs_refl in IN_SC;
eauto.
apply s_obs_nobs in OBS.
apply s_obs_nobs in IN_SC.
decs IN_SC.
decs OBS.
eapply nobs_some_succ_eq with (
pc :=
pc);
eauto.
subst o.
Ltac UseSilentSteps'
OSO VRS' :=
exploit silent_steps;
eauto;
introsv OSO;
try (
apply VRS');
eauto;
destruct OSO as [
cs' [
rcs' [
STEPS [
CEQ RCEQ]]]];
eexists;
split; [
apply plus_star;
apply STEPS |
idtac].
Ltac Counters'
cs cs'0 :=
apply counter_eq_trans with (
cs' :=
cs);
[
eapply inc_counter_silent_step_eq;
eauto;
unfolds;
eexists;
split;
eauto;
simpl;
auto |
apply counter_eq_trans with (
cs' :=
cs'0);
auto;
apply counter_eq_refl].
Ltac RCounters'
rcs rcs'0 :=
apply counter_eq_trans with (
cs' :=
rcs);
[
eapply inc_r_counter_silent_step_eq;
eauto;
unfolds;
eexists;
split;
eauto;
simpl;
auto |
apply counter_eq_trans with (
cs' :=
rcs'0);
auto;
apply counter_eq_refl].
inv STEP.
Ltac SolveMs2Ms1 AGREE OSO VRS'
pc pc'
cs cs'0
rcs rcs'0
STEPS SUCC PC_OUT PC'
_OUT :=
try (
solve [
eapply nobs_no_def_step;
eauto;
unfolds;
split; [
unfolds;
auto |
split; [
unfolds;
auto |
apply AGREE]]]);
try UseSilentSteps'
OSO VRS';
try (
apply ms1 with (
o :=
pc');
auto);
try (
solve [
Counters'
cs cs'0 |
RCounters'
rcs rcs'0 |
eapply nobs_some_onlysucc;
eauto]);
try solve [
intro;
subst pc';
apply no_plus_step_t_entry in STEPS;
trim];
let NE' :=
fresh "
NE'"
in
dup SUCC NE';
apply succ_no_entry in NE';
let NE :=
fresh "
NE"
in
dup PC_OUT NE;
eapply out_no_entry in NE;
eauto;
let NE'' :=
fresh "
NE''"
in
dup PC'
_OUT NE'';
eapply out_no_entry in NE'';
eauto;
dup AGREE AGREE';
apply agree_ne_pc with (
pc'' :=
pc)
in AGREE;
auto;
try (
apply agree_ne_pc with (
pc' :=
pc');
auto).
inv H3;
renInst;
MakeUse INST;
try ApplyButToIbuiltin INST ltac:(
SolveMs2Ms1 AGREE OSO VRS'
pc pc'
cs cs'0
rcs rcs'0
STEPS SUCC PC_OUT PC'
_OUT).
SSCase "
Iop".
eapply iop_out_preserves_agree with (
pc :=
pc);
eauto.
SSCase "
Iload".
eapply load_out_preserves_agree with (
pc :=
pc);
eauto.
SSCase "
Istore".
eapply store_preserves_agree'
with (
pc :=
pc);
eauto.
SSCase "
Ibuiltin".
destruct (
is_builtin_annot_dec ef)
as [
ISA|
NOTA].
SSSCase "
is_builtin_annot".
SolveMs2Ms1 AGREE OSO VRS'
pc pc'
cs cs'0
rcs rcs'0
STEPS SUCC PC_OUT PC'
_OUT.
eapply annot_preserves_agree'
with (
pc :=
pc);
eauto.
destruct ef;
elim ISA;
inv H8;
apply agree_ne_pc with (
pc'' :=
pc)
in AGREE;
auto.
SSSCase "~
is_builtin_annot".
SolveMs2Ms1 AGREE OSO VRS'
pc pc'
cs cs'0
rcs rcs'0
STEPS SUCC PC_OUT PC'
_OUT.
eapply not_annot_preserves_agree'
with (
pc :=
pc);
eauto.
SSCase "
Icond".
solve [
eapply nobs_no_def_step;
eauto;
unfolds;
split; [
unfolds;
auto |
split; [
unfolds;
auto |
apply AGREE]]].
SCase "
succ not in slice =>
no_step +
ms2".
inv STEP.
inv H3;
renInst;
MakeUse INST;
try (
solve [
eapply nobs_no_def_step;
eauto;
unfolds;
split; [
unfolds;
auto |
split; [
unfolds;
auto |
apply AGREE]]]);
eexists;
split;
try (
apply star_refl);
try (
apply ms2 with (
o :=
o);
auto);
try (
solve [
Counters'
cs cs'0 |
RCounters'
rcs rcs'0 |
eapply obs_some_succ with (
pc :=
pc);
eauto]);
dup SUCC NE';
apply succ_no_entry in NE';
dup PC_OUT NE;
eapply out_no_entry in NE;
eauto;
dup PC'
_OUT NE'';
eapply out_no_entry in NE'';
eauto;
dup AGREE AGREE';
apply agree_ne_pc with (
pc'' :=
pc)
in AGREE;
auto;
try (
apply agree_ne_pc with (
pc' :=
pc');
auto).
SSCase "
Iop".
eapply iop_out_preserves_agree;
eauto.
eapply valid_rs_after with (
m :=
m');
eauto;
trim.
SSCase "
Iload".
eapply load_out_preserves_agree;
eauto.
eapply valid_rs_after with (
m :=
m');
eauto;
trim.
SSCase "
Istore".
eapply store_preserves_agree';
eauto.
SSCase "
Ibuiltin".
destruct (
is_builtin_annot_dec ef)
as [
ISA|
NOTA].
SSSCase "
is_builtin_annot".
destruct ef;
elim ISA;
inv H8;
eapply annot_preserves_agree'
with (
pc :=
pc);
eauto.
SSSCase "~
is_builtin_annot".
eapply not_annot_preserves_agree'
with (
pc :=
pc);
eauto.
eapply valid_rs_after with (
m :=
m');
eauto;
trim.
Case "
ms3".
rewrite <-
nexit_eq.
dup s_dobs_checker_ok HAS_NEX.
apply checked_has_nexit with (
n :=
pc)
in HAS_NEX.
destruct HAS_NEX as (
dx &
DX);
eauto.
eapply none_steps;
eauto.
unfolds;
auto.
unfolds;
auto.
eapply succ_f_In;
eauto.
Qed.
Lemma 1 in the paper: transf_step_correct.
This is the main simulation lemma for the slicing.
Lemma transf_step_correct:
(* Lemma 1 *)
forall s1 s2,
cstep'
ge s1 s2 ->
forall s1' (
MS:
match_states s1 s1'),
exists s2',
star cstep_t'
ge s1'
s2' /\
match_states s2 s2'.
Proof.
introsv STEP MS.
generalize dependent STEP.
destruct s1,
s2.
destruct get_st,
get_st0.
intro.
exploit transf_step;
eauto;
intros.
Qed.
Definition all_counter_eq (
nc :
node) (
all_cs all_cs' :
counter *
counter) :
Prop :=
let '(
cs,
rcs) :=
all_cs in
let '(
cs',
rcs') :=
all_cs'
in
counter_eq nc cs cs' /\
counter_eq nc rcs rcs'.
Lemma all_counter_eq_refl:
forall nc all_cs,
all_counter_eq nc all_cs all_cs.
Proof.
intros.
unfold all_counter_eq.
destruct all_cs.
exploit counter_eq_refl;
eauto.
Qed.
Theorem transf_function_correct:
forall rs m,
forward_simulation (
all_counter_eq nc) (
i_semantics rs m f nc fsc sp ge) (
i_semantics rs m tf nc tfsc sp ge).
Proof.
End PRES_FUNCTION.
End PRESERVATION.
Section BEHAVIOR.
Variable f :
function.
Variable nc :
t_criterion.
Variable fsc :
Scope.family f.
Variable sp :
val.
Variable ge :
genv.
Variable rs :
regset.
Variable m :
mem.
Variable exit_n :
node.
Variable reg_vint :
reg.
Variable tf :
function.
Variable of :
obs_function.
Hypothesis FOK:
slice_function f nc fsc exit_n reg_vint =
OK (
tf,
of).
Hypothesis WFF:
check_wf f =
OK (
exit_n,
reg_vint).
Notation tfsc := (
tfsc f exit_n reg_vint fsc nc tf of FOK).
Notation original_function_behaves := (
function_behaves (
i_semantics rs m f nc fsc sp ge)).
Notation sliced_function_behaves := (
function_behaves (
i_semantics rs m tf nc tfsc sp ge)).
Theorem slicing_preserves_criterion_counters:
forall (
cs rcs :
counter),
original_function_behaves (
WeakSimulation.Terminates (
cs,
rcs)) ->
exists cs',
exists rcs',
sliced_function_behaves (
WeakSimulation.Terminates (
cs',
rcs')) /\
cs #
nc =
cs' #
nc /\
rcs #
nc =
rcs' #
nc.
Proof.
End BEHAVIOR.
Section SOUNDNESS.
Variable ge :
genv.
Variable sp :
val.
Variable f :
function.
Variable rs :
regset.
Variable m :
mem.
Variable fsc :
Scope.family f.
Variable tf :
function.
Variable exit_n :
node.
Variable reg_vint :
reg.
Hypothesis WFF:
check_wf f =
OK (
exit_n,
reg_vint).
Variable l :
t_criterion.
Definition behaves (
f :
function) (
fsc :
Scope.family f) (
crit :
t_criterion) :=
function_behaves (
i_semantics rs m f l fsc sp ge).
Lemma Trace_star_step:
forall f'
fsc'
tr s,
Trace ge f'
fsc'
sp rs m (
s ::
tr) ->
star (
fun ge =>
cstep ge f'
fsc'
sp)
ge (
init_st f'
rs m)
s.
Proof.
induction tr;
intros.
inv H.
eapply star_refl.
inv H.
apply IHtr in H2.
apply star_right with (
s2 :=
a);
auto.
Qed.
Lemma Reach_star_step:
forall f'
fsc'
s,
Reach ge f'
fsc'
sp rs m s ->
star (
fun ge =>
cstep ge f'
fsc'
sp)
ge (
init_st f'
rs m)
s.
Proof.
Lemma star_step_reach:
forall f'
fsc'
s s',
star (
fun ge =>
cstep ge f'
fsc'
sp)
ge s s' ->
Reach ge f'
fsc'
sp rs m s ->
Reach ge f'
fsc'
sp rs m s'.
Proof.
induction 1;
intros;
auto.
apply R_step with (
s' :=
s2)
in H1;
auto.
Qed.
Lemma reach_weak_sim_terminates:
forall f'
fsc'
s,
Reach ge f'
fsc'
sp rs m s ->
behaves f'
fsc'
l (
WeakSimulation.Terminates (
get_cs s,
get_rcs s)).
Proof.
Variable of:
obs_function.
Hypothesis FOK:
slice_function f l fsc exit_n reg_vint =
OK (
tf,
of).
Theorem 3 in the paper: program_slicing_is_sound.
It allows us to consider local bounds from the sliced functions,
which are much more precise than those obtained in the original
functions.
Theorem program_slicing_is_sound:
(* Theorem 3 *)
let tfsc :=
transf_family FOK in
forall M,
(
forall s (
REACH:
Reach ge tf tfsc sp rs m s), (
get_rcs s) #
l <=
M) ->
forall s' (
REACH':
Reach ge f fsc sp rs m s'), (
get_rcs s') #
l <=
M.
Proof.
We still need to do some "plumbing" to be able to use the correctness
of program slicing to prove the correctness of global bounds.
We prove some lemmas related to termination guarantees about
the original and sliced programs; namely, that whenever the original
program terminates, so does the sliced program (possibly sooner
than the original).
Require Import DLib.
Lemma Reach_simul:
let tfsc :=
transf_family FOK in
forall s,
Reach ge f fsc sp rs m s ->
exists s',
Reach ge tf tfsc sp rs m s' /\
match_states f l of s s'.
Proof.
Let EXIT_NO_SUCC :
forall s :
RTL.node, ~
succ_node f (
_exit of)
s.
Proof.
Let OBSOK:
checked_nobs f l (
_exit of) (
_slice_nodes of) (
nobs (
_s_dobs of)) (
nexit (
_dexit of)).
Proof.
One of the useful properties to ensure termination of the sliced program
is the fact that there is a unique exit node, and all branches in the slice
have been statically resolved to allow a feasible path that can always
reach this exit node. This prevents the sliced program from entering
infinite loops which would cause divergence.
Lemma Reach_exit:
let tfsc :=
transf_family FOK in
forall s,
Reach ge f fsc sp rs m s ->
get_pc s =
exit_n ->
exists s',
Reach ge tf tfsc sp rs m s' /\
get_pc s' =
exit_n.
Proof.
introsv R EXIT.
apply Reach_simul in R.
destruct R as (
s' &
R' &
MS).
exists s'.
split;
auto.
inv_clear MS;
simpls.
subst;
auto.
subst s s';
simpls.
subst pc.
dup WFF EINST.
eapply exit_is_return in EINST;
eauto.
destruct EINST as [
optarg EI].
exploit nexit_eq;
eauto;
introsv EEQ.
destruct (
positive_eq_dec o exit_n).
subst o.
apply s_obs_nobs in OBSPC.
destruct OBSPC as (
d &
dc &
NOBS).
eapply nobs_obs_in_slice in NOBS;
eauto;
trim.
rewrite EEQ;
eauto.
eapply obs_some_reaches in OBSPC;
eauto.
inv OBSPC;
trim.
eapply exit_no_succ in H0;
eauto;
trim.
rewrite EEQ;
eauto.
erewrite nexit_eq;
eauto.
Qed.
Lemma Reach_f_In:
forall s,
Reach ge f fsc sp rs m s ->
f_In (
get_pc s)
f.
Proof.
induction 1;
intros;
simpl.
eapply wf_entry_in;
eauto.
apply cstep_succ in H0.
eapply succ_f_In';
eauto.
Qed.
Lemma Reach_return:
let tfsc :=
transf_family FOK in
Reaches_final ge f fsc sp rs m ->
Reaches_final ge tf tfsc sp rs m.
Proof.
unfold Reaches_final;
intros.
destruct H as (
s &
o &
H &
H0).
dup H R.
apply Reach_f_In in R.
apply f_In_ex in R.
destruct R as [
i INST].
eapply return_is_exit in H0;
eauto.
dup WFF EI.
eapply exit_is_return in EI;
eauto.
destruct EI as [
optarg EINST].
apply Reach_exit in H;
auto.
destruct H as (
s' &
R' &
EXIT').
exists s'.
exists optarg.
split;
auto.
eapply slice_preserves_Ireturn;
eauto.
rewrite EXIT'.
exploit nexit_eq;
eauto;
introsv EEQ.
rewrite EEQ;
auto.
exploit nexit_eq;
eauto;
introsv EEQ.
rewrite EEQ;
auto.
Qed.
Require Import LocalBounds.
memcpy_deterministic is the only axiom we add to CompCert, and it is related to
the fact that slicing does not preserve CompCert's event trace, so we cannot use the
existing theorem Events.external_call_deterministic, which is defined in a
general way to be applicable to several external functions (such as volatile
memory reads, which can indeed depend on the trace).
The only difference between both is that we relax the constraint that the
same trace must be present in both situations, as long as the memory is
the same.
"Built-ins" such as memcpy have a particular semantics which is specified
in CompCert, and this axiom just adds a reasonable constraint on the
properties of the memcpy function.
All-in-all, the motivation for this particular case is a specific benchmark
(ndes) where several loops can be bounded if one considers such
determinism. A skeptical reader may reject this axiom and use a slightly
different checker in LocalBounds, which will have the same precision
everywhere except in programs containing memcpy instructions,
without impacting the correctness of the analysis.
Axiom memcpy_deterministic:
forall sz al (
F V :
Type) (
ge :
Genv.t F V)
vargs m t1 vres1 m1 t2 vres2 m2,
external_call (
EF_memcpy sz al)
ge vargs m t1 vres1 m1 ->
external_call (
EF_memcpy sz al)
ge vargs m t2 vres2 m2 ->
vres1 =
vres2 /\
m1 =
m2.
Lemma step_no_update_det:
let tfsc :=
transf_family FOK in
(
forall n, ~
contains_misc_builtins tf n) ->
forall n s1 s2,
cstep ge tf tfsc sp n s1 ->
cstep ge tf tfsc sp n s2 ->
s1 =
s2.
Proof.
intros tfsc NOBIN s1 s2 s3 S1 S2.
inv S1;
inv S2.
inv H;
inv H3;
trim;
simpls.
destruct ef;
try solve [
exfalso;
eapply NOBIN;
eapply HS;
eauto;
intros;
intro;
subst ef0;
trim].
rewrite H0 in H7.
inv H7.
eapply memcpy_deterministic in H1;
eauto.
inv H1;
auto.
rewrite H0 in H7.
inv H7.
inv H1;
inv H8;
auto.
rewrite H0 in H7.
inv H7.
inv H1.
inv H8.
rewrite <-
H in H1.
inv H1;
auto.
rewrite H0 in H5.
inv H5.
rewrite H1 in H8.
inv H8.
auto.
Qed.
Lemma reach_final_terminates_aux:
let tfsc :=
transf_family FOK in
(
forall n, ~
contains_misc_builtins tf n) ->
forall s s'
o,
star (
fun ge =>
cstep ge tf tfsc sp)
ge s s' ->
((
fn_code tf) ! (
get_pc s')) =
Some (
Ireturn o) ->
~
State_diverge ge tf tfsc sp s.
Proof.
induction 2;
red;
intros.
>
inv H1.
inv H2;
simpl in *.
inv H1;
simpl in *;
try congruence.
>
elim IHstar;
eauto.
inv H3.
replace s2 with s4;
auto.
eapply step_no_update_det;
eauto.
Qed.
Lemma reach_final_terminates:
let tfsc :=
transf_family FOK in
(
forall n, ~
contains_misc_builtins tf n) ->
Reaches_final ge tf tfsc sp rs m ->
Terminates ge tf tfsc sp rs m.
Proof.
Theorem 4 in the paper: slicing_preserves_termination.
It shows sliced programs do not introduce divergence.
Theorem slicing_preserves_termination:
(* Theorem 4 *)
let tfsc :=
transf_family FOK in
(
forall n, ~
contains_misc_builtins tf n) ->
Reaches_final ge f fsc sp rs m ->
Terminates ge tf tfsc sp rs m.
Proof.
Lemma match_states_eq_rcs:
forall s s',
match_states f l of s'
s ->
(
get_rcs s) #
l = (
get_rcs s') #
l.
Proof.
intros.
inv H; simpl; auto.
Qed.
Lemma match_states_not_l:
forall s s',
match_states f l of s s' ->
(
get_pc s') <>
l -> (
get_pc s) <>
l.
Proof.
This stronger version of program_slicing_is_sound is necessary
for the integration with the loop bound analysis.
Theorem program_slicing_is_sound_stronger_version:
let tfsc :=
transf_family FOK in
forall M,
(
forall s,
Reach ge tf tfsc sp rs m s ->
((
get_rcs s) #
l <=
M)%
nat /\
((
get_rcs s) #
l =
M -> (
get_pc s) <>
l)) ->
(
forall s,
Reach ge f fsc sp rs m s ->
((
get_rcs s) #
l <=
M)%
nat /\
((
get_rcs s) #
l =
M -> (
get_pc s) <>
l)).
Proof.
End SOUNDNESS.