Library analysis
Require Export AllLattice.
Require Export semantic.
Require Export Arith.
Module MRec := ArrayLattice FiniteSetLattice.
Module MMutRec := ArrayLattice BoolLattice.
Module MPred' := ArrayLattice FiniteSetLattice.
Module MPred := ArrayLattice MPred'.
Module MBC := ArrayLattice BoolLattice.
Import FiniteSetLattice.
Import Pos.
Definition orderB := BoolLattice.Pos.order.
Definition joinB := BoolLattice.join.
Inductive conc_tr : Trace -> Trace -> Trace -> Prop :=
conc_tr0 : forall tr (st:State), conc_tr tr st (tr:::st)
| conc_tr1 : forall tr1 tr2 tr3 st,
conc_tr tr1 tr2 tr3 -> conc_tr tr1 (tr2:::st) (tr3:::st).
Inductive in_trace (st:State) : Trace -> Prop :=
in_trace0 : in_trace st st
| in_trace1 : forall tr, in_trace st (tr:::st)
| in_trace2 : forall tr st',
in_trace st tr -> in_trace st (tr:::st').
Inductive m_pc_in_sf_rest : MethodName -> progCount -> CallStack -> CallStack -> Prop :=
| m_pc_in_sf_rest0 : forall m pc l s sf,
m_pc_in_sf_rest m pc ((frame m pc l s)::sf) ((frame m pc l s)::sf)
| m_pc_in_sf_rest1 : forall m' pc' m pc l s sf1 sf2,
m_pc_in_sf_rest m pc sf1 sf2 ->
m_pc_in_sf_rest m pc ((frame m' pc' l s)::sf1) sf2.
Lemma m_pc_in_sf_rest_incl : forall m pc sf1 sf2,
m_pc_in_sf_rest m pc sf1 sf2 -> incl sf2 sf1.
induction 1; intros; auto with datatypes.
Qed.
Inductive sf_rest: CallStack -> CallStack -> Prop :=
sf_rest0 : forall f sf, sf_rest sf (f::sf).
Inductive prefix_tr : Trace -> Trace -> Prop :=
| prefix_tr0 : forall tr, prefix_tr tr tr
| prefix_tr1 : forall tr1 tr2 st,
prefix_tr tr1 tr2 -> prefix_tr tr1 (tr2:::st).
Lemma prefix_conc_tr : forall tr1 tr2 tr3,
conc_tr tr1 tr2 tr3 -> prefix_tr tr1 tr3.
induction 1; constructor.
constructor.
auto.
Qed.
Lemma invoke_invariant_return : forall P tr,
valid_trace P tr ->
forall m pc sf', m_pc_in_sf_rest m pc (sfSt (currentState tr)) sf' ->
exists tr1, exists tr2,
conc_tr tr1 tr2 tr /\
m=(mSt (currentState tr1)) /\
pc=(pcSt (currentState tr1)) /\
sf_rest (sfSt (currentState tr1)) sf' /\
(exists mID, instructionAt P m pc = Some (invokevirtual mID)) /\
forall st, in_trace st tr2 -> incl sf' (sfSt st).
induction 1; intros.
inversion_clear H in H0; inversion_clear H0.
simpl in *.
CaseEq (currentState tr); intros h (m',pc',l,s) sf Heq.
rewrite Heq in H0; rewrite Heq in IHSemCol'; simpl in *.
set (st':=st).
inversion_clear H0 in st' Heq H1 IHSemCol'; simpl in *;
try (
elim (IHSemCol' m pc sf' H1); intros tr1 (tr2,(HH1,(HH2,(HH3,(HH4,(HH5,HH6))))));
exists tr1; exists (tr2:::st'); split;
[constructor 2; auto|
split; [assumption| split; [assumption | split; [assumption | split; [assumption |
intros st0 HH0; inversion_clear HH0 in st';
[unfold st'; eapply m_pc_in_sf_rest_incl; simpl; eauto |
auto]]]]]]; fail).
inversion_clear H1 in st'.
exists tr; exists (Trace_init st'); split.
constructor 1.
split.
rewrite Heq; simpl; auto.
split.
rewrite Heq; simpl; auto.
rewrite Heq; split; simpl.
constructor.
split.
exists mID; auto.
intros.
inversion_clear H0.
unfold st'; simpl.
auto with datatypes.
elim (IHSemCol' m pc _ H0); intros tr1 (tr2,(HH1,(HH2,(HH3,(HH4,(HH5,HH6)))))).
exists tr1; exists (tr2:::st'); split; [constructor 2; auto|idtac].
split; auto.
split; auto.
split; auto.
split; auto.
intros.
inversion_clear H1 in st'.
unfold st'; simpl.
generalize (m_pc_in_sf_rest_incl _ _ _ _ H0); auto with datatypes.
auto.
elim (IHSemCol' m pc sf').
intros tr1 (tr2,(HH1,(HH2,(HH3,(HH4,(HH5,HH6)))))).
exists tr1; exists (tr2:::st'); split; [constructor 2; auto|idtac].
split; auto.
split; auto.
split; auto.
split; auto.
intros st0 HH0; inversion_clear HH0 in st'.
unfold st'; simpl.
apply m_pc_in_sf_rest_incl with m pc; auto.
auto.
constructor 2; auto.
Qed.
Lemma return_invariant : forall P tr st,
valid_trace P tr ->
SmallStepSem P return_v1 (currentState tr) st ->
exists tr',
prefix_tr tr' tr /\
(mSt st)=(mSt (currentState tr')) /\
(sfSt st)=(sfSt (currentState tr')).
intros.
CaseEq (currentState tr); intros h (m,pc,l,s) sf Heq.
rewrite Heq in H0.
inversion_clear H0 in Heq; simpl in *.
elim (invoke_invariant_return P tr H m' pc' (frame m' pc' l' s' :: sf0)).
intros tr1 (tr2,(HH1,(HH2,(HH3,(HH4,(_,HH5)))))).
exists tr1; split.
apply prefix_conc_tr with tr2; auto.
split; auto.
inversion_clear HH4; auto.
rewrite Heq; simpl; constructor; auto.
Qed.
Lemma m_in_sf_eq_word : forall m1 m2 sf,
eq_word m1 m2 ->
m_in_sf m1 sf ->
m_in_sf m2 sf.
intros.
induction H0.
constructor 1; auto.
apply eq_word_trans with m1; auto.
constructor 2; auto.
Qed.
Inductive ConstrRec (P:Program) (Rec:MRec.Pos.set)
(m:MethodName) (pc:progCount) : rule -> Prop :=
| constr_rec_invokevirtual : forall mID,
(forall m', In m' (implem P mID) ->
order (add_set m (Rec m)) (Rec m')) ->
ConstrRec P Rec m pc (invokevirtual1 mID)
| constr_rec_nop : ConstrRec P Rec m pc nop1
| constr_rec_push : forall c, ConstrRec P Rec m pc (push1 c)
| constr_rec_push2 : forall c, ConstrRec P Rec m pc (push21 c)
| constr_rec_pop : ConstrRec P Rec m pc pop1
| constr_rec_numop : forall op, ConstrRec P Rec m pc (numop1 op)
| constr_rec_load : forall x, ConstrRec P Rec m pc (load1 x)
| constr_rec_store : forall x, ConstrRec P Rec m pc (store1 x)
| constr_rec_if1 : forall pc', ConstrRec P Rec m pc (If1 pc')
| constr_rec_if2 : forall pc', ConstrRec P Rec m pc (If2 pc')
| constr_rec_new_o : forall cl, ConstrRec P Rec m pc (new_o1 cl)
| constr_rec_putfield : forall f, ConstrRec P Rec m pc (putfield1 f)
| constr_rec_getfield : forall f, ConstrRec P Rec m pc (getfield1 f)
| constr_rec_goto1 : forall pc', ConstrRec P Rec m pc (goto1 pc')
| constr_rec_new_a1 : forall t, ConstrRec P Rec m pc (new_a1 t)
| constr_rec_arraylength : ConstrRec P Rec m pc arraylength1
| constr_rec_arrayload : ConstrRec P Rec m pc arrayload1
| constr_rec_arraystore : ConstrRec P Rec m pc arraystore1
| constr_rec_return : ConstrRec P Rec m pc return_v1.
Definition gammaRec : MRec.Pos.set -> Trace -> Prop :=
fun Rec tr => forall st, in_trace st tr ->
forall m', m_in_sf m' (sfSt st) -> in_set m' (Rec (mSt st)) = true.
Lemma currentState_in_trace : forall tr,
in_trace (currentState tr) tr.
destruct tr; constructor.
Qed.
Lemma in_trace_conc : forall tr tr1 tr2 st,
conc_tr tr1 tr2 tr ->
in_trace st tr1 -> in_trace st tr.
induction 1; intros; constructor; auto.
Qed.
Lemma in_trace_prefix : forall tr tr1 st,
prefix_tr tr1 tr ->
in_trace st tr1 -> in_trace st tr.
induction 1; intros; auto.
constructor; auto.
Qed.
Lemma Rec_correctness_lemma :
forall P i tr1 tr2 Rec,
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r) ->
valid_trace P tr1 ->
gammaRec Rec tr1 ->
SmallStepSemTrace P i tr1 tr2 ->
gammaRec Rec tr2.
unfold gammaRec; intros P i tr1 tr2 Rec H Hv H1 H3.
inversion_clear H3 in H1.
simpl in *.
CaseEq (currentState tr1); intros h1 (m1,pc1,l1,s1) sf1 Heq1.
rewrite Heq1 in H0; simpl in *.
set (st':=st).
intros.
inversion_clear H2 in st' H3; auto.
generalize (H1 (config h1 (frame m1 pc1 l1 s1) sf1)); simpl; intros H1'.
unfold st' in H3.
generalize H0; intros H0'.
inversion_clear H0 in st' H3 H0' Heq1 H1 H1'; simpl in *;
try (apply H1'; [rewrite <- Heq1; apply currentState_in_trace|assumption]).
assert (ConstrRec P Rec m1 pc1 (invokevirtual1 mID)).
apply H; auto.
inversion_clear H0.
elim (methodLookup_in_implem _ _ _ _ H6); intros m'' (H1'',H2').
rewrite <- (MRec.apply_eq_word Rec _ _ H2').
apply in_set_monotone with (add_set m1 (Rec m1)); auto.
inversion_clear H3.
rewrite (in_set_eq_word m1); auto.
apply in_set_add_set1.
apply in_set_add_set2; auto.
(apply H1'; [destruct tr1; simpl in Heq1; rewrite Heq1; constructor|auto]).
elim (return_invariant P tr1 (config h1 (frame m'0 (nextAddress P pc') l' (v :: s')) sf)) ;auto.
unfold st' in *; simpl; intros tr' (HH1,(HH2,HH3)).
clear st'; subst; simpl in *.
apply (H1 (currentState tr')); simpl.
apply in_trace_prefix with tr'; auto.
apply currentState_in_trace.
auto.
rewrite Heq1; auto.
Qed.
Lemma Rec_correctness :
forall P Rec,
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r) ->
forall tr,
SemCol P tr ->
gammaRec Rec tr.
intros.
destruct tr; unfold SemCol in H0; simpl in *.
induction H0.
inversion_clear H0.
intros st' H2 m; simpl.
inversion_clear H2; simpl; intros.
inversion_clear H0.
apply Rec_correctness_lemma with P i tr; auto.
constructor; auto.
Qed.
Definition ConstrMutRec (P:Program)
(Rec:MRec.Pos.set) (MutRec:MMutRec.Pos.set)
(m:MethodName) : Prop :=
(forall m', in_set m' (Rec m) = true ->
orderB (MutRec m') (MutRec m)) /\
orderB (in_set m (Rec m)) (MutRec m).
Inductive m_disticts_in_sf : CallStack -> Prop :=
| m_disticts_in_sf_nil : m_disticts_in_sf nil
| m_disticts_in_sf_cons : forall m pc l s sf,
m_disticts_in_sf sf ->
~ m_in_sf m sf ->
m_disticts_in_sf ((frame m pc l s)::sf).
Definition gammaMutRec : MMutRec.Pos.set -> Trace -> Prop :=
fun MutRec tr => forall st, in_trace st tr ->
(MutRec (mSt st)) = false ->
~ m_in_sf (mSt st) (sfSt st) /\ m_disticts_in_sf (sfSt st).
Lemma MutRec_correctness_lemma :
forall P i tr1 tr2 Rec MutRec,
(forall M, In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M)) ->
valid_trace P tr1 ->
gammaRec Rec tr2 ->
gammaMutRec MutRec tr1 ->
SmallStepSemTrace P i tr1 tr2 ->
gammaMutRec MutRec tr2.
unfold gammaMutRec; intros P i tr1 tr2 Rec MutRec H Hv H1 H2 H3.
inversion_clear H3 in H1 H2.
simpl in *.
CaseEq (currentState tr1); intros h1 (m1,pc1,l1,s1) sf1 Heq1.
rewrite Heq1 in H0; simpl in *.
generalize H0; intros H0'.
intros.
inversion_clear H3 in H4; auto.
generalize (H2 (currentState tr1) (currentState_in_trace tr1)); rewrite Heq1; simpl; intros H1'.
inversion_clear H0 in H4 H1 Heq1 H0'; simpl in *; auto.
generalize (H M (methodLookup_some_in _ _ _ _ H7)).
intros (Hc1,Hc2).
split; intros.
red; intros.
rewrite (H1 (config h1 (frame (nameMethod M) Word_1 l' nil) (frame m1 pc1 l1 s :: sf1))) in Hc2; simpl; auto.
rewrite H4 in Hc2; inversion Hc2.
constructor.
CaseEq (MutRec m1); intros.
assert (in_set m1 (Rec (nameMethod M)) = true).
apply (H1 (config h1 (frame (nameMethod M) Word_1 l' nil) (frame m1 pc1 l1 s :: sf1))).
constructor; auto.
simpl.
constructor; auto.
generalize (Hc1 _ H11).
rewrite H4; rewrite H0; intros.
inversion H12.
elim (H1' H0); clear H1'; intros.
constructor; auto.
elim (return_invariant P tr1 (config h1 (frame m' (nextAddress P pc') l' (v :: s')) sf)) ;auto.
simpl; intros tr' (HH1,(HH2,HH3)).
subst; simpl in *.
apply H2; auto.
apply in_trace_prefix with tr'; auto.
apply currentState_in_trace.
rewrite Heq1; auto.
Qed.
Lemma MutRec_correctness :
forall P Rec MutRec,
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r) ->
(forall M, In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M)) ->
forall tr,
SemCol P tr ->
gammaMutRec MutRec tr.
intros.
generalize (Rec_correctness P Rec H); clear H; intros H.
destruct tr; unfold SemCol in H1; simpl in *.
induction H1.
inversion_clear H1.
split; simpl; intros.
red; intros.
inversion_clear H1 in H4; simpl in H4.
inversion_clear H4.
inversion_clear H1; simpl; constructor.
apply MutRec_correctness_lemma with P i tr Rec; auto.
generalize (H (VTR P (tr ::: st) v)); simpl; intros; auto.
constructor; auto.
Qed.
Inductive ConstrPred (P:Program)
(MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set)
(m:MethodName) (pc:progCount) : rule -> Prop :=
| constr_pred_nop :
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc nop1
| constr_pred_push : forall c,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (push1 c)
| constr_pred_push2 : forall c,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (push21 c)
| constr_pred_pop :
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc pop1
| constr_pred_numop : forall op,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (numop1 op)
| constr_pred_load : forall x,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (load1 x)
| constr_pred_store : forall x,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (store1 x)
| constr_pred_if1 : forall pc',
order (add_set pc (Pred m pc)) (Pred m pc') ->
ConstrPred P MutRec Pred m pc (If1 pc')
| constr_pred_if2 : forall pc',
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (If2 pc')
| constr_pred_new_o : forall cl,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (new_o1 cl)
| constr_pred_putfield : forall f,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (putfield1 f)
| constr_pred_getfield : forall f,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (getfield1 f)
| constr_pred_goto : forall pc',
order (add_set pc (Pred m pc)) (Pred m pc') ->
ConstrPred P MutRec Pred m pc (goto1 pc')
| constr_pred_new_a : forall t,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (new_a1 t)
| constr_pred_arraylength :
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc arraylength1
| constr_pred_arrayload :
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc arrayload1
| constr_pred_arraystore1 :
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc arraystore1
| constr_pred_return_v1 :
ConstrPred P MutRec Pred m pc return_v1
| constr_pred_invokevirtual : forall mID,
order (add_set pc (Pred m pc)) (Pred m (nextAddress P pc)) ->
ConstrPred P MutRec Pred m pc (invokevirtual1 mID).
Inductive seq_call (P:Program) (m:MethodName) (st1 st2:State) : Prop :=
seq_call_def : forall mID,
SmallStepSem P (invokevirtual1 mID) st1 st2 ->
eq_word m (mSt st2) ->
seq_call P m st1 st2.
Inductive pc_in_current_tr (P:Program) (pc0:progCount) (m0:MethodName) : Trace -> Prop :=
| pc_in_current_tr_current : forall tr,
eq_word (pcSt (currentState tr)) pc0 ->
eq_word (mSt (currentState tr)) m0 ->
pc_in_current_tr P pc0 m0 tr
| pc_in_current_tr_next : forall st tr,
~ seq_call P m0 (currentState tr) st ->
pc_in_current_tr P pc0 m0 tr ->
pc_in_current_tr P pc0 m0 (tr:::st).
Lemma seq_call_eq_word : forall P m1 m2 st1 st2,
eq_word m1 m2 ->
seq_call P m1 st1 st2 ->
seq_call P m2 st1 st2.
intros.
inversion_clear H0.
constructor 1 with mID; auto.
apply eq_word_trans with m1; auto.
Qed.
Lemma pc_in_current_tr_eq_word : forall P pc m1 m2 tr,
eq_word m1 m2 ->
pc_in_current_tr P pc m1 tr ->
pc_in_current_tr P pc m2 tr.
intros.
induction H0.
constructor 1; auto.
apply eq_word_trans with m1; auto.
constructor 2; auto.
red; intros; elim H0; apply seq_call_eq_word with m2; auto.
Qed.
Inductive pc_in_rest_tr (P:Program) (pc0:progCount) (m0:MethodName) : Trace -> Prop :=
pc_in_rest_tr_def : forall st tr,
~ seq_call P m0 (currentState tr) st ->
pc_in_current_tr P pc0 m0 tr ->
pc_in_rest_tr P pc0 m0 (tr:::st).
Inductive prop_prefix_tr (P:Trace->Prop) : Trace -> Prop :=
| prop_prefix_tr0 : forall s:State,
P s -> prop_prefix_tr P s
| prop_prefix_tr1 : forall s tr,
prop_prefix_tr P tr ->
P (tr:::s) -> prop_prefix_tr P (tr:::s).
Lemma apply_prop_prefix : forall P tr1 tr2,
prefix_tr tr1 tr2 ->
prop_prefix_tr P tr2 ->
prop_prefix_tr P tr1.
induction 1; intuition.
inversion_clear H0; auto.
Qed.
Lemma apply_prop_tr : forall P tr,
prop_prefix_tr P tr -> P tr.
intros.
inversion_clear H; auto.
Qed.
Implicit Arguments apply_prop_tr [P tr].
Lemma pc_in_current_tr_in_trace : forall P pc m tr,
pc_in_current_tr P pc m tr ->
exists st, in_trace st tr /\
eq_word m (mSt st) /\ eq_word pc (pcSt st).
induction 1.
exists (currentState tr); repeat split; simpl; auto.
destruct tr; constructor.
elim IHpc_in_current_tr; clear IHpc_in_current_tr; intros st' (H1,(H2,H3)).
exists st'; repeat split; auto.
constructor; auto.
Qed.
Lemma conc_tr_currentState : forall tr tr1 tr2,
conc_tr tr1 tr2 tr ->
currentState tr = currentState tr2.
induction 1; simpl; auto.
Qed.
Lemma pc_in_current_tr_conc : forall P tr1 tr3 tr4 m pc,
conc_tr tr3 tr4 tr1 ->
pc_in_current_tr P pc m tr1 ->
pc_in_current_tr P pc m tr3 \/ pc_in_current_tr P pc m tr4.
induction 1; intros.
inversion_clear H.
right; constructor; auto.
auto.
inversion_clear H0.
right; constructor; auto.
elim (IHconc_tr H2); intros; auto.
right; constructor 2; auto.
rewrite <- (conc_tr_currentState _ _ _ H); auto.
Qed.
Lemma m_in_sf_In : forall m pc l s sf,
In (frame m pc l s) sf ->
m_in_sf m sf.
induction sf; intros.
inversion_clear H.
inversion_clear H.
subst; constructor 1.
apply eq_word_refl.
right; auto.
Qed.
Lemma m_in_sf_incl : forall sf1 sf2 m,
m_in_sf m sf1 -> incl sf1 sf2 -> m_in_sf m sf2.
induction 1; intros.
apply m_in_sf_eq_word with m'; auto.
apply m_in_sf_In with pc l s.
auto with datatypes.
apply IHm_in_sf.
intros s.
auto with datatypes.
Qed.
Lemma in_trace_conc_tr_r : forall st tr1 tr2 tr3,
conc_tr tr1 tr2 tr3 -> in_trace st tr2 -> in_trace st tr3.
induction 1; intros.
inversion_clear H; constructor.
inversion_clear H0; constructor; auto.
Qed.
Definition gammaPred (P:Program) (MutRec:MMutRec.Pos.set): MPred.Pos.set -> Trace -> Prop :=
fun Pred tr => prop_prefix_tr (fun tr =>
((MutRec (mSt (currentState tr))) = false ->
forall pc, pc_in_rest_tr P pc (mSt (currentState tr)) tr ->
in_set pc (Pred (mSt (currentState tr)) (pcSt (currentState tr))) = true)
) tr.
Lemma Pred_correctness_lemma :
forall P i tr1 tr2 Pred MutRec,
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrPred P MutRec Pred m pc r) ->
valid_trace P tr1 ->
gammaMutRec MutRec tr1 ->
gammaMutRec MutRec tr2 ->
gammaPred P MutRec Pred tr1 ->
SmallStepSemTrace P i tr1 tr2 ->
gammaPred P MutRec Pred tr2.
unfold gammaPred; intros P i tr1 tr2 Pred MutRec H Hv HMutRec1 HMutRec H1 H2.
inversion_clear H2 in H1 HMutRec.
constructor; auto.
intros Hyp pc Hpc.
generalize (apply_prop_tr H1); intros H1'.
simpl in *.
CaseEq (currentState tr1); intros h1 (m1,pc1,l1,s1) sf1 Heq1.
rewrite Heq1 in H0; rewrite Heq1 in H1'; simpl in *.
set (i':=i).
set (st':=st).
generalize H0; intros H0'.
inversion_clear H0 in H0' H1' Heq1 i' HMutRec Hyp Hpc st'; simpl in *;
try (
generalize (H m1 pc1 i' H2); clear H; intros H; inversion_clear H;
match goal with
| id:order _ _ |- _ => apply in_set_monotone with (1:=id)
end;
inversion_clear Hpc;
match goal with
| id:pc_in_current_tr _ _ _ _ |- _ =>
inversion_clear id in Heq1 H1'
end; [
apply (in_set_eq_word (pcSt (currentState tr1))); auto;
rewrite Heq1; simpl; apply in_set_add_set1 |
apply in_set_add_set2; apply H1'; auto; constructor; auto]).
inversion_clear Hpc.
elim H0.
rewrite Heq1; constructor 1 with mID; auto.
inversion_clear Hpc.
elim (invoke_invariant_return _ _ Hv m' pc' (frame m' pc' l' s' :: sf)).
intros tr1' (tr2',(HH1,(HH2,(HH3,(HH4,((mID,HH5),HH6)))))).
assert (prefix_tr tr1' tr1).
apply prefix_conc_tr with tr2'; auto.
generalize (apply_prop_tr (apply_prop_prefix _ _ _ H4 H1)); clear H1; intros.
generalize (H m' pc' (invokevirtual1 mID) HH5); intros.
inversion_clear H5.
apply in_set_monotone with (1:=H6).
case (eq_word_dec pc' pc); intros.
apply in_set_eq_word with pc'; auto.
apply in_set_add_set1.
apply in_set_add_set2.
clear st'; subst; simpl in *.
apply H1; auto.
clear H6.
elim (pc_in_current_tr_conc _ _ _ _ _ _ HH1 H3); intros.
inversion_clear H5 in n; simpl in *.
elim n; auto.
constructor; auto.
elim (pc_in_current_tr_in_trace _ _ _ _ H5); intros st'' (Hyp1,(Hyp2,Hyp3)).
elim (HMutRec st''); intros.
elim H6.
apply m_in_sf_eq_word with (mSt (currentState tr1')); auto.
apply m_in_sf_In with (pcSt (currentState tr1')) l' s'.
apply HH6; auto with datatypes.
constructor.
apply in_trace_conc_tr_r with tr1' tr2'; auto.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ Hyp2); auto.
rewrite Heq1; simpl; constructor.
Qed.
Lemma Pred_correctness :
forall P Rec MutRec Pred,
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r) ->
(forall M, In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M)) ->
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrPred P MutRec Pred m pc r) ->
forall tr,
SemCol P tr ->
gammaPred P MutRec Pred tr.
intros.
destruct tr; unfold SemCol in H2; simpl in *.
induction H2.
inversion_clear H2.
constructor; simpl; intros.
inversion_clear H4.
apply Pred_correctness_lemma with i tr; auto.
generalize (MutRec_correctness P Rec MutRec H H0 (VTR P tr H2));
intros HH; apply HH; simpl.
unfold SemCol; simpl; auto.
generalize (MutRec_correctness P Rec MutRec H H0 (VTR P (tr:::st) v));
intros HH; apply HH; simpl.
unfold SemCol; simpl; auto.
constructor; auto.
Qed.
Inductive remove_exec (P:Program) (m:MethodName) : Trace -> (option Trace) -> Prop :=
remove_exec_found : forall tr st,
seq_call P m (currentState tr) st ->
remove_exec P m (tr:::st) (Some tr)
| remove_exec_continue : forall tr1 tr2 st,
~ seq_call P m (currentState tr1) st ->
remove_exec P m tr1 tr2 ->
remove_exec P m (tr1:::st) tr2
| remove_exec_first : forall st,
eq_word m (mSt st) ->
remove_exec P m st None.
Lemma invoke_must_change_sf : forall P mID h1 h2 f1 f2 sf,
~ SmallStepSem P (invokevirtual1 mID) (config h1 f1 sf) (config h2 f2 sf).
red; intros.
inversion H.
assert (~(frame m pc l s) :: sf = sf).
generalize (frame m pc l s).
clear H6 H3 H; induction sf; intuition.
discriminate H.
injection H; clear H; intros.
elim (IHsf _ H).
elim H14; auto.
Qed.
Lemma app_dec : forall (A:Set) (l:list A) n,
{exists l1, exists l2, l = l1++l2 /\ n = length l1}+
{~ exists l1, exists l2, l = l1++l2 /\ n = length l1}.
induction l; intros.
destruct n.
left; exists (nil (A:=A)); exists (nil (A:=A)); auto.
right; intros (l1,(l2,(H1,H2))).
destruct l1.
discriminate H2.
discriminate H1.
destruct n.
left; exists (nil (A:=A)); exists (a::l); split; auto with datatypes.
case (IHl n); clear IHl; intros.
left; elim e; clear e; intros l1 (l2,(H1,H2)).
exists (a::l1); exists l2; subst; split; auto with datatypes.
right; red; intros (l1,(l2,(H1,H2))); elim n0.
destruct l1.
discriminate H2.
exists l1; exists l2; split; auto.
simpl in H1; injection H1; auto.
Qed.
Lemma searchClass_none : forall P cl,
searchClass P cl = None ->
forall c, In c (classes P) -> ~ eq_word (nameClass c) cl.
intros P cl; unfold searchClass.
induction (classes P); simpl; intros.
elim H0.
generalize H; clear H; case eq_word_dec; intros.
discriminate H.
elim H0; clear H0; intros; subst; auto.
Qed.
Lemma remove_exec_exists : forall P m t,
valid_trace P t ->
(eq_word m (mSt (currentState t)) \/ m_in_sf m (sfSt (currentState t))) ->
exists t', remove_exec P m t t'.
induction 1.
inversion_clear H; simpl; intros.
elim H; clear H; intros.
subst; exists (None (A:=Trace)); constructor; auto.
inversion H.
simpl.
CaseEq (currentState tr); intros h (m',pc,l,s) sf Heq.
rewrite Heq in IHSemCol'; rewrite Heq in H0.
generalize H0; intros H0'.
inversion_clear H0 in H0' IHSemCol' Heq; simpl in *;
try (
intros HH1; elim (IHSemCol' HH1); intros t' H';
exists t'; constructor; auto;
rewrite Heq; intros Hs; inversion_clear Hs as [mid Hss Heq']; simpl in *;
elim (invoke_must_change_sf _ _ _ _ _ _ _ Hss); fail).
intros HH.
case (eq_word_dec m (nameMethod M)); intros.
exists (Some tr); constructor.
constructor 1 with mID.
rewrite Heq; auto.
simpl; auto.
elim IHSemCol'.
intros t' H'.
exists t'; constructor; auto.
red; intros H''; inversion_clear H''; simpl in *.
elim n0; auto.
elim HH; clear HH; intros HH.
elim n0; subst; auto.
inversion_clear HH; auto.
intros HH1; elim IHSemCol'.
intros t' H'.
exists t'; constructor; auto.
rewrite Heq; intros Hs; inversion_clear Hs as [mid Hss Heq']; simpl in *.
inversion Hss.
right; elim HH1; intros.
constructor 1; apply eq_word_sym; auto.
constructor 2; auto.
Qed.
Import FiniteSetLattice.
Lemma remove_SemCol : forall P tr1 tr2 m,
remove_exec P m tr1 (Some tr2) ->
SemCol' P tr1 ->
SemCol' P tr2.
induction tr1; intros.
inversion_clear H in H0; auto.
inversion_clear H in H0 IHtr1; auto.
inversion_clear H0; auto.
inversion_clear H0.
apply IHtr1 with m; auto.
Qed.
Lemma remove_begin_invoke : forall P tr1 tr2 m,
remove_exec P m tr1 (Some tr2) ->
SemCol' P tr1 ->
(eq_word m (mSt (currentState tr1)) \/ m_in_sf m (sfSt (currentState tr1))) ->
exists st,
prefix_tr (tr2:::st) tr1 /\
seq_call P m (currentState tr2) st.
induction tr1; intros.
inversion_clear H.
inversion_clear H in H0 H1 IHtr1.
exists s; split; auto.
constructor.
elim (IHtr1 _ _ H3); intros.
elim H; clear H; intros.
exists x; split; auto.
constructor; auto.
inversion_clear H0; auto.
simpl in *.
inversion_clear H0.
CaseEq (currentState tr1); intros h1 (m1,pc1,l1,s1) sf1 Heq1.
rewrite Heq1 in H4.
generalize H4; intros H4'.
inversion_clear H4 in Heq1 H4' H2 H1;
simpl in *; try assumption.
elim H1; clear H1; intros.
elim H2; rewrite Heq1; constructor 1 with mID; auto.
inversion_clear H1; auto.
right; elim H1; intros.
constructor 1; apply eq_word_sym; auto.
constructor 2; auto.
Qed.
Inductive nb_m_pc_in_current_tr (P:Program) (m0:MethodName) (pc0:progCount) : Trace -> nat -> Prop :=
| m_pc_in_current_tr : forall h m pc l s sf tr,
seq_call P m0 (currentState tr) (config h (frame m pc l s) sf) ->
eq_word pc pc0 ->
eq_word m m0 ->
nb_m_pc_in_current_tr P m0 pc0 (tr:::(config h (frame m pc l s) sf)) 1
| m_pc_in_current_tr1 : forall h m pc l s sf tr,
seq_call P m0 (currentState tr) (config h (frame m pc l s) sf) ->
~eq_word pc pc0 \/ ~eq_word m m0 ->
nb_m_pc_in_current_tr P m0 pc0 (tr:::(config h (frame m pc l s) sf)) 0
| m_pc_in_current_tr2 : forall h m pc l s sf tr n,
~ seq_call P m0 (currentState tr) (config h (frame m pc l s) sf) ->
eq_word pc pc0 ->
eq_word m m0 ->
nb_m_pc_in_current_tr P m0 pc0 tr n ->
nb_m_pc_in_current_tr P m0 pc0 (tr:::(config h (frame m pc l s) sf)) (S n)
| m_pc_in_current_tr3 : forall h m pc l s sf tr n,
~ seq_call P m0 (currentState tr) (config h (frame m pc l s) sf) ->
~eq_word pc pc0 \/ ~eq_word m m0 ->
nb_m_pc_in_current_tr P m0 pc0 tr n ->
nb_m_pc_in_current_tr P m0 pc0 (tr:::(config h (frame m pc l s) sf)) n
| m_pc_in_current_tr4 : forall h m pc l s sf,
eq_word pc pc0 ->
eq_word m m0 ->
nb_m_pc_in_current_tr P m0 pc0 (config h (frame m pc l s) sf) (1)
| m_pc_in_current_tr5 : forall h m pc l s sf,
(~eq_word pc pc0 \/ ~eq_word m m0) ->
nb_m_pc_in_current_tr P m0 pc0 (config h (frame m pc l s) sf) (0).
Inductive ConstrBC (P:Program)
(Pred:MPred.Pos.set) (BC:MBC.Pos.set)
(m:MethodName) (pc:progCount) : rule -> Prop :=
| constr_bc_invokevirtual : forall mID,
(forall m', In m' (implem P mID) ->
orderB (in_set pc (Pred m pc)) (BC m')) ->
ConstrBC P Pred BC m pc (invokevirtual1 mID)
| constr_bc_nop : ConstrBC P Pred BC m pc nop1
| constr_bc_push : forall c, ConstrBC P Pred BC m pc (push1 c)
| constr_bc_push2 : forall c, ConstrBC P Pred BC m pc (push21 c)
| constr_bc_pop : ConstrBC P Pred BC m pc pop1
| constr_bc_numop : forall op, ConstrBC P Pred BC m pc (numop1 op)
| constr_bc_load : forall x, ConstrBC P Pred BC m pc (load1 x)
| constr_bc_store : forall x, ConstrBC P Pred BC m pc (store1 x)
| constr_bc_if1 : forall pc', ConstrBC P Pred BC m pc (If1 pc')
| constr_bc_if2 : forall pc', ConstrBC P Pred BC m pc (If2 pc')
| constr_bc_new_o : forall cl, ConstrBC P Pred BC m pc (new_o1 cl)
| constr_bc_putfield : forall f, ConstrBC P Pred BC m pc (putfield1 f)
| constr_bc_getfield : forall f, ConstrBC P Pred BC m pc (getfield1 f)
| constr_bc_goto1 : forall pc', ConstrBC P Pred BC m pc (goto1 pc')
| constr_bc_new_a1 : forall t, ConstrBC P Pred BC m pc (new_a1 t)
| constr_bc_arraylength : ConstrBC P Pred BC m pc arraylength1
| constr_bc_arrayload : ConstrBC P Pred BC m pc arrayload1
| constr_bc_arraystore : ConstrBC P Pred BC m pc arraystore1
| constr_bc_return : ConstrBC P Pred BC m pc return_v1.
Inductive m2_pc_in_tr (m1:MethodName) (m2:MethodName) (pc:progCount) : Trace -> Trace -> Prop :=
| m2_pc_in_tr0 : forall st tr,
eq_word m1 (mSt (currentState tr)) ->
eq_word m2 (mSt st) ->
eq_word pc (pcSt (currentState tr)) ->
m2_pc_in_tr m1 m2 pc (tr:::st) tr
| m2_pc_in_tr1 : forall st tr tr2,
m2_pc_in_tr m1 m2 pc tr tr2 ->
m2_pc_in_tr m1 m2 pc (tr:::st) tr2.
Lemma m2_pc_in_tr_eq_word1 : forall m1 m2 m2' pc tr tr',
eq_word m2 m2' ->
m2_pc_in_tr m1 m2 pc tr tr' ->
m2_pc_in_tr m1 m2' pc tr tr'.
induction 2; intros; constructor; auto.
apply eq_word_trans with m2; auto.
Qed.
Definition gammaBC (P:Program) : MMutRec.Pos.set -> MBC.Pos.set -> Trace -> Prop :=
fun MutRec BC tr =>
prop_prefix_tr
(fun tr =>
(BC (mSt (currentState tr))) = false ->
(MutRec (mSt (currentState tr))) = false ->
forall m' m pc mID tr',
(eq_word m' (mSt (currentState tr))) ->
instructionAt P m pc = Some (invokevirtual mID) ->
m2_pc_in_tr m m' pc tr tr' ->
nb_m_pc_in_current_tr P m pc tr' (1)) tr.
Lemma m_in_sf_dec: forall m sf, {m_in_sf m sf}+{~m_in_sf m sf}.
induction sf.
right; intros H; inversion H.
destruct a as [m' pc' l s].
case (eq_word_dec m' m); intros.
left; constructor 1; auto.
case IHsf; intros.
left; constructor 2; auto.
right; intros H; elim n0.
inversion_clear H; intuition.
Qed.
Lemma pc_in_current_tr_eq_word' : forall P pc1 pc2 m1 m2 tr,
eq_word pc1 pc2 ->
eq_word m1 m2 ->
pc_in_current_tr P pc1 m1 tr ->
pc_in_current_tr P pc2 m2 tr.
intros.
induction H1.
constructor 1; auto.
apply eq_word_trans with pc1; auto.
apply eq_word_trans with m1; auto.
constructor 2; auto.
red; intros; elim H1; apply seq_call_eq_word with m2; auto.
Qed.
Lemma invariant_invoke_prefix_tr : forall P tr1,
valid_trace P tr1 -> forall m' tr2 m pc,
m2_pc_in_tr m m' pc tr1 tr2 ->
exists tr3,
prefix_tr tr3 tr1
/\ eq_word m' (mSt (currentState tr3))
/\ m2_pc_in_tr m m' pc tr3 tr2.
induction 1; intros.
inversion_clear H0.
inversion_clear H1 in IHSemCol'.
exists (tr2:::st); intuition.
constructor 1.
constructor; auto.
elim (IHSemCol' _ _ _ _ H2); intros tr3' (H4,(H5,H6)).
exists tr3'; intuition.
constructor 2; auto.
Qed.
Inductive not_single_tr : Trace -> Prop :=
not_single_tr0 : forall tr st,
not_single_tr (tr:::st).
Inductive prefix_tr_strict : Trace -> Trace -> Prop :=
prefix_tr_strict0 : forall tr1 tr2 st,
prefix_tr tr1 tr2 -> prefix_tr_strict tr1 (tr2:::st).
Inductive m_in_tr : MethodName -> Trace -> Prop :=
m_in_tr0 : forall m tr,
eq_word m (mSt (currentState tr)) -> m_in_tr m tr
| m_in_tr1 : forall m st tr,
m_in_tr m tr -> m_in_tr m (tr:::st).
Lemma m_in_tr_st : forall m tr,
m_in_tr m tr -> exists st, in_trace st tr /\ eq_word m (mSt st).
induction 1.
exists (currentState tr); split; auto.
destruct tr; simpl in *; constructor.
elim IHm_in_tr; intros st' (H1,H2).
exists st'; split; auto.
constructor 3; auto.
Qed.
Lemma m2_pc_in_tr_conc : forall tr1 tr2 tr3 tr4 m m' pc,
conc_tr tr3 tr4 tr1 ->
m2_pc_in_tr m m' pc tr1 tr2 ->
m2_pc_in_tr m m' pc tr3 tr2 \/ m_in_tr m' tr4.
induction 1; intros.
inversion_clear H.
right; constructor 1; auto.
auto.
inversion_clear H0 in IHconc_tr.
right; constructor 1; auto.
elim (IHconc_tr H1); intros; auto.
right; constructor 2; auto.
Qed.
Implicit Arguments m2_pc_in_tr_conc [tr1 tr2 tr3 tr4 m m' pc].
Lemma nameMethod_invariant : forall P tr m,
valid_trace P tr ->
eq_word m (mSt (currentState tr)) \/ m_in_sf m (sfSt (currentState tr)) ->
exists M, In M (main P :: methods P)
/\ eq_word m (nameMethod M).
induction 1.
inversion_clear H; simpl; intros.
elim H; intros.
eauto.
inversion H1.
CaseEq (currentState tr); intros h (m',pc,l,s) sf Heq.
rewrite Heq in H0; rewrite Heq in IHSemCol'; simpl in IHSemCol'.
inversion_clear H0 in IHSemCol' Heq; eauto; simpl.
intros [H8|H8].
generalize (methodLookup_some_in _ _ _ _ H4); intros.
exists M; auto.
inversion_clear H8; eauto.
intros [H8|H8].
elim IHSemCol'; eauto.
right; constructor 1; auto.
elim IHSemCol'; eauto.
right; constructor 2; auto.
Qed.
Lemma seq_call_dec : forall P i m st1 st2,
SmallStepSem P i st1 st2 ->
seq_call P m st1 st2 \/ ~ seq_call P m st1 st2.
intros.
generalize H; intros H'';
inversion_clear H in H'';
try (
right; intros H'; inversion_clear H' in H''; simpl in *;
inversion_clear H in H0 H'';
match goal with
| id1 : instructionAt P _ _ = _,
id2 : instructionAt P _ _ = _ |- _ =>
rewrite id1 in id2; discriminate id2
end; fail).
case (eq_word_dec m (nameMethod M)); intros.
left; constructor 1 with mID; auto.
right; intros H'; elim n0; inversion_clear H'; auto.
Qed.
Implicit Arguments seq_call_dec [P i st1 st2].
Lemma nb_m_pc_in_current_tr_not0 : forall P m pc tr,
valid_trace P tr ->
pc_in_current_tr P pc m tr \/
nb_m_pc_in_current_tr P m pc tr 0.
induction 1; simpl; intros.
destruct st as [h (m',pc',l,s) sf].
case (eq_word_dec m' m); intros.
case (eq_word_dec pc' pc); intros.
left; constructor 1; auto.
right; constructor; auto.
right; constructor; auto.
destruct st as [h (m',pc',l,s) sf].
elim (seq_call_dec m H0); intros.
case (eq_word_dec pc' pc); intros.
left; constructor 1; auto.
inversion_clear H1; simpl in *; apply eq_word_sym; auto.
right; constructor 2; auto.
case (eq_word_dec pc' pc); intros.
case (eq_word_dec m' m); intros.
left; constructor 1; auto.
elim IHSemCol'; intros.
left; constructor 2; auto.
right; constructor 4; auto.
elim IHSemCol'; intros.
left; constructor 2; auto.
right; constructor 4; auto.
Qed.
Implicit Arguments nb_m_pc_in_current_tr_not0 [P tr].
Lemma BC_correctness_lemma :
forall P i tr1 tr2 Rec MutRec Pred (BC:MBC.Pos.set),
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r) ->
(forall M, In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M)) ->
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrBC P Pred BC m pc r) ->
valid_trace P tr2 ->
gammaRec Rec tr2 ->
gammaMutRec MutRec tr1 ->
gammaPred P MutRec Pred tr1 ->
gammaBC P MutRec BC tr1 ->
SmallStepSemTrace P i tr1 tr2 ->
gammaBC P MutRec BC tr2.
unfold gammaBC; intros P i tr1 tr2 Rec MutRec Pred BC HcRec HHH' H Hv HRec HMutRec HPred H1 Hsem.
inversion_clear Hsem in H1 HRec HMutRec HPred Hv.
simpl in *.
CaseEq (currentState tr1); intros h1 (m1,pc1,l1,s1) sf1 Heq1.
rewrite Heq1 in H0.
set (i':=i).
inversion_clear H0 in Heq1 i' HRec HPred HMutRec Hv; simpl in *;
try (
constructor; auto; simpl;
intros H1'' H1' m' m pc mID tr' HH1 HH2 HH3;
inversion_clear HH3 in Heq1 H1 H2 HMutRec; simpl in *;
[subst; match goal with
| id1:eq_word m _, id2:eq_word pc _, id3:instructionAt P m1 pc1 = _ |- _ =>
(rewrite Heq1 in id1; rewrite Heq1 in id2; simpl in id1,id2;
rewrite (instructionAt_eq_word P _ _ _ _ id1 id2) in HH2;
rewrite HH2 in id3; discriminate id3)
end |
apply (apply_prop_tr H1) with m' mID; try (rewrite Heq1; simpl);
auto]; fail).
generalize (H _ _ (invokevirtual1 mID) H2); clear H; intros H; inversion_clear H.
constructor; auto; simpl.
intros H1'' H1' m' m pc mID' tr' HH1 HH2 HH3.
inversion_clear HH3 in Hv Heq1 H1 HRec HPred HMutRec; simpl in *.
rewrite Heq1 in H10; rewrite Heq1 in H; simpl in H10,H.
rewrite (instructionAt_eq_word P _ _ _ _ H H10) in HH2.
rewrite HH2 in H2; injection H2; intros; subst.
destruct tr'; injection Heq1; simpl; intros; subst.
constructor 5.
apply eq_word_sym; auto.
apply eq_word_sym; auto.
inversion_clear Hv; simpl in *.
clear H8; inversion_clear H6.
elim (seq_call_dec m H11); intros.
constructor 1; auto.
constructor 3; auto.
elim (nb_m_pc_in_current_tr_not0 m pc H8); intros; auto.
assert (in_set pc1 ((MPred.apply Pred m1) pc1) = true).
apply in_set_eq_word with pc; auto.
apply (apply_prop_tr HPred); simpl.
CaseEq (MutRec m1); intros; try reflexivity.
elim (HHH' M (methodLookup_some_in _ _ _ _ H5)); intros.
assert (orderB (MutRec m1) (MutRec (nameMethod M))).
apply (H14 m1).
apply (HRec (config h1 (frame (nameMethod M) Word_1
(fun x : Var =>
match pred (nat_of_P (word2pos x)) with
| O => ref loc
| S m => nth m A null
end) nil) (frame m1 pc1 l1 s :: sf1))
(in_trace1 _ _) m1); simpl.
constructor 1; auto.
rewrite H1' in H16; rewrite H13 in H16; inversion H16.
constructor; auto.
red; intros; elim H6; apply seq_call_eq_word with m1; auto.
apply pc_in_current_tr_eq_word' with pc m; auto.
elim (methodLookup_in_implem _ _ _ _ H5); intros m'' (H',H2').
generalize (H0 _ H').
rewrite (MBC.apply_eq_word BC _ _ H2').
rewrite H13; rewrite H1''; intros HH; inversion HH.
inversion_clear Hv.
elim (invariant_invoke_prefix_tr _ _ H9 _ _ _ _ H); intros tr'' (H1''',(H2''',H3''')).
generalize (apply_prop_prefix _ _ _ H1''' H1); intros.
apply (apply_prop_tr H11) with (nameMethod M) mID'; auto.
rewrite <- (MBC.apply_eq_word BC _ _ H2''').
rewrite (MBC.apply_eq_word BC _ _ HH1); auto.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ H2''').
rewrite (MMutRec.apply_eq_word MutRec _ _ HH1); auto.
apply eq_word_trans with m'; auto.
apply m2_pc_in_tr_eq_word1 with m'; auto.
constructor; simpl; auto.
intros.
inversion_clear H6 in Heq1 H4 H1 Hv H0 H3 HMutRec.
rewrite Heq1 in H9; rewrite Heq1 in H7; simpl in *.
rewrite (instructionAt_eq_word P _ _ _ _ H7 H9) in H5.
rewrite H2 in H5; discriminate H5.
generalize Hv; intros.
inversion_clear Hv0; simpl in *.
generalize (invoke_invariant_return P _ H6 m' pc' (frame m' pc' l' s' :: sf)); simpl; intros.
elim H9; clear H9; try intros tr1' (tr2',(HH1,(HH2,(HH3,(HH4,(HH5,HH6)))))).
assert (prefix_tr tr1' tr1).
apply prefix_conc_tr with tr2'; auto.
generalize (apply_prop_prefix _ _ _ H9 H1); clear H1; intros.
apply (apply_prop_tr H1) with m'0 mID; auto.
rewrite <- HH2; auto.
rewrite <- HH2; auto.
rewrite <- HH2; auto.
elim (m2_pc_in_tr_conc HH1 H7); intros.
auto.
elim (m_in_tr_st _ _ H10); intros st0 (H10',H11').
generalize (HH6 _ H10'); clear HH6; intros HH6.
elim (HMutRec st0); intros.
elim H11.
apply m_in_sf_incl with (frame m' pc' l' s' :: sf); auto.
constructor 1.
apply eq_word_trans with m'0; auto.
apply (in_trace_conc_tr_r st0 _ _ _ HH1); auto.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ H11').
rewrite (MMutRec.apply_eq_word MutRec _ _ H4); auto.
rewrite Heq1; simpl; constructor 1; auto.
Qed.
Lemma BC_correctness :
forall P tr Rec MutRec Pred (BC:MBC.Pos.set),
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r) ->
(forall M, In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M)) ->
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrPred P MutRec Pred m pc r) ->
(forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrBC P Pred BC m pc r) ->
valid_trace P tr ->
gammaBC P MutRec BC tr.
intros P t Rec MutRec Pred BC HcRec HcMutRec HcPred HcBC H.
induction H.
inversion_clear H.
constructor; simpl; intros.
inversion_clear H4.
assert (valid_trace P (tr:::st)).
constructor 2 with i; auto.
eapply BC_correctness_lemma; eauto.
apply (Rec_correctness P Rec HcRec (VTR P _ H1) H1).
apply (MutRec_correctness P Rec MutRec HcRec HcMutRec (VTR P _ H) H).
apply (Pred_correctness P Rec MutRec Pred HcRec HcMutRec HcPred (VTR P _ H) H).
constructor 1; eauto.
Qed.
Inductive nb_invoke (P:Program) (m:MethodName) : Trace -> nat -> Prop :=
nb_invoke0 : forall st:State,
nb_invoke P m st 0
| nb_invoke2 : forall st tr n,
seq_call P m (currentState tr) st ->
nb_invoke P m tr n ->
nb_invoke P m (tr:::st) (S n)
| nb_invoke4 : forall st tr n,
~ seq_call P m (currentState tr) st ->
nb_invoke P m tr n ->
nb_invoke P m (tr:::st) n.
Lemma nb_instruction_prefix : forall P m tr1 tr2,
prefix_tr tr1 tr2 -> forall n,
nb_invoke P m tr2 n ->
exists n', nb_invoke P m tr1 n' /\ n' <= n.
induction 1.
eauto.
intros.
inversion_clear H0.
elim (IHprefix_tr _ H2); intros n' (H3',H4'); eauto.
elim (IHprefix_tr _ H2); intros n' (H3',H4'); eauto.
Qed.
Lemma remove_exec_prefix : forall P m tr1 tr2 st,
remove_exec P m (tr1:::st) (Some tr2) -> prefix_tr tr2 tr1.
induction tr1; intros.
inversion_clear H.
constructor.
inversion_clear H1; constructor.
inversion_clear H; constructor; auto.
eauto.
Qed.
Lemma remove_exec_prefix' : forall P m tr1 tr2,
remove_exec P m tr1 (Some tr2) -> prefix_tr tr2 tr1.
induction tr1; intros.
inversion_clear H.
inversion_clear H; constructor; auto.
constructor.
Qed.
Inductive tr_rest : Trace -> Trace -> Prop :=
tr_rest0 : forall tr st, tr_rest (tr:::st) tr.
Index
This page has been generated by coqdoc