Library analysis2
Require Export analysis.
Require Export FiniteSetLat.
Import FiniteSetLattice.
Require Import SumList.
Inductive call (P:Program) (m:MethodName) : Trace -> list (MethodName*progCount) -> Prop :=
call_0 : forall st:State,
call P m st nil
| call_1 : forall t st l,
seq_call P m (currentState t) st ->
call P m t l ->
call P m (t:::st) ((mSt (currentState t),pcSt (currentState t))::l)
| call_2 : forall t st l,
~ seq_call P m (currentState t) st ->
call P m t l ->
call P m (t:::st) l.
Lemma call_is_nb_invoke : forall P m t n l,
nb_invoke P m t n ->
call P m t l -> n = length l.
induction t; intros.
inversion_clear H in H0.
inversion_clear H0; auto.
inversion_clear H in H0.
inversion_clear H0 in H1 H2; simpl; auto.
elim H; auto.
inversion_clear H0; auto.
elim H1; auto.
Qed.
Lemma call_jump1 : forall P m m' pc' t s n1 n l0,
nb_invoke P m' (t ::: s) n1 ->
call P m t l0 ->
nb_m_pc m' pc' l0 n ->
nb_m_pc_in_current_tr P m' pc' t 0 ->
~ eq_word m m' ->
(n1=0/\n=0) \/
exists t1 : Trace, exists n1' : nat,
prefix_tr t1 t /\ nb_invoke P m' t1 n1' /\ n1 = S n1'
/\ exists l1 : list (MethodName * progCount),
call P m t1 l1 /\ nb_m_pc m' pc' l1 n.
induction t; simpl; intros.
inversion_clear H0 in H1.
inversion_clear H1.
inversion_clear H in H2.
inversion_clear H1.
right; exists (Trace_init s); exists 0; repeat constructor; auto.
exists (nil (A:=(MethodName*progCount))); repeat (constructor; auto).
inversion_clear H1; left; auto.
inversion_clear H in H0 H1 H2.
right; exists (t:::s); exists n0; repeat (constructor; auto).
eauto.
inversion_clear H0 in H1 H4 H2 H5; simpl in *.
inversion_clear H1; simpl in *.
inversion_clear H2 in H5 H4 H.
inversion_clear H5.
elim H3.
inversion_clear H2; inversion_clear H.
apply eq_word_trans with m0; auto.
elim H2; auto.
inversion_clear H10 in H0 H7; simpl in *.
elim H11; clear H11; intros H11; elim H11; apply eq_word_sym; auto.
elim H11; clear H11; intros H11; elim H11; apply eq_word_sym; auto.
elim H2; clear H2; intros H2; elim H2; apply eq_word_sym; auto.
inversion_clear H2 in H5 H4 H.
elim H3.
inversion_clear H1; inversion_clear H.
apply eq_word_trans with m0; auto.
elim (IHt _ n1 n l H5 H6 H7 H9); intros.
left; auto.
elim H2; clear H2; intros t1 (n1',(HH1,(HH2,HH3))).
right; exists t1; exists n1'; split; auto.
constructor; auto.
auto.
inversion_clear H2 in H5 H4 H.
inversion_clear H5.
right; exists t; exists n0; repeat (constructor; auto).
exists l0; auto.
elim H2; auto.
elim (IHt _ n1 n l0 H5 H6 H1 H8); intros.
left; auto.
elim H2; clear H2; intros t1 (n1',(HH1,(HH2,HH3))).
right; exists t1; exists n1'; split; auto.
constructor; auto.
auto.
Qed.
Lemma nb_m_pc_bounded : forall P BC MutRec m m' pc' t,
gammaBC P MutRec BC t ->
BC m = false ->
MutRec m = false ->
prop_prefix_tr (fun t => forall l n1 n2,
nb_invoke P m' t n1 ->
call P m t l ->
nb_m_pc m' pc' l n2 -> ~ eq_word m m' -> n2 <= S n1) t.
induction t; intros; constructor; auto; intros.
inversion_clear H3 in H4.
inversion_clear H4; auto with arith.
apply IHt; auto.
assert (prefix_tr t (t:::s)).
do 2 constructor.
apply (apply_prop_prefix _ _ _ H2 H).
assert (prefix_tr t (t:::s)).
do 2 constructor.
assert (gammaBC P MutRec BC t).
apply (apply_prop_prefix _ _ _ H6 H); clear H6.
generalize (IHt H7 H0 H1); clear IHt; intros IHt.
inversion_clear H3 in H4.
destruct t.
inversion_clear H9 in H4.
inversion_clear H4.
inversion_clear H10; omega.
inversion_clear H9; omega.
simpl in *.
clear H6.
inversion_clear H2 in IHt H9 H4 H8; simpl in *.
inversion_clear H4.
generalize (apply_prop_tr IHt _ _ _ H6 H9 H11 H5); omega.
elim H5; inversion_clear H3; inversion_clear H8;
apply eq_word_trans with (mSt s); auto.
inversion_clear H4.
assert (nb_m_pc_in_current_tr P m' pc' (t:::s0) 1); intros.
inversion_clear H8.
rewrite (MBC.apply_eq_word BC _ _ H12) in H0.
rewrite (MMutRec.apply_eq_word MutRec _ _ H12) in H1.
apply (apply_prop_tr H H0 H1) with m mID; auto.
inversion_clear H4 in H2 H10; simpl in *.
rewrite (instructionAt_eq_word P _ _ _ _ H2 H10); auto.
constructor; auto.
inversion_clear H4 in H2 H10 IHt H8 H9 H3 H6; simpl in *.
inversion_clear H6.
inversion_clear H9 in H11.
elim H5; inversion_clear H6; inversion_clear H4;
apply eq_word_trans with m0; auto.
assert (prefix_tr t (t ::: config h (frame m0 pc l1 s1) sf)).
do 2 constructor.
generalize (apply_prop_tr (apply_prop_prefix _ _ _ H9 IHt) _ _ _ H15 H16 H11 H5); omega.
elim H4; auto.
inversion_clear H9 in H11.
elim H5; apply eq_word_trans with m0; auto.
inversion_clear H4; auto.
elim (call_jump1 P m m' pc' t _ n1 n l0 H6 H16 H11 H15 H5); intros.
elim H9; intros; subst; omega.
elim H9; clear H9; intros t1 (n1',(HH1,(HH2,(HH3,(l1',(HH4,HH5)))))).
assert (prefix_tr t1 (t:::(config h (frame m0 pc l1 s1) sf))).
constructor; auto.
generalize (apply_prop_tr (apply_prop_prefix _ _ _ H9 IHt) _ _ _ HH2 HH4 HH5 H5).
subst; omega.
elim H13; clear H13; intros H13; elim H13; apply eq_word_sym; auto.
apply (apply_prop_tr IHt _ _ _ H6 H9 H10 H5).
clear H6; inversion_clear H2 in H8.
generalize (apply_prop_tr IHt _ _ _ H6 H9 H4 H5); omega.
generalize (apply_prop_tr IHt _ _ _ H6 H9 H4 H5); omega.
Qed.
Lemma majoration1 : forall P BC MutRec m m' t n1 lp l,
gammaBC P MutRec BC t ->
BC m = false ->
MutRec m = false ->
nb_invoke P m' t n1 ->
call P m t l ->
In (m',lp) (factorize l) ->
~ eq_word m m' ->
sumlist (fun pcn:(Word*nat) => let (pc,n) := pcn in n) (list2multiset lp)
<= (length (list2multiset lp))*(S n1).
intros.
apply sumlist_bound.
intros (pc',n) H'.
assert (nb_m_pc m' pc' l n).
apply nb_m_pc_in_list with lp; auto.
apply
(apply_prop_tr
(nb_m_pc_bounded P BC MutRec m m' pc' t H H0 H1)
l _ _ H2 H3 H6); auto.
Qed.
Lemma in_call_invoke : forall P m t l m' pc,
call P m t l ->
In (m',pc) l ->
exists mID, instructionAt P m' pc = Some (invokevirtual mID).
induction t; intros.
inversion_clear H in H0.
inversion H0.
inversion_clear H in H0.
elim H0; clear H0; intros.
injection H; clear H; intros; subst.
inversion_clear H1.
inversion_clear H.
simpl.
exists mID; auto.
apply IHt with l0; auto.
apply IHt with l; auto.
Qed.
Lemma in_list2multiset_invoke : forall P m t l m' lp pc n,
call P m t l ->
In (m',lp) (factorize l) ->
In (pc,n) (list2multiset lp) ->
exists mID, instructionAt P m' pc = Some (invokevirtual mID).
intros.
elim (in_list2multiset _ _ _ H1); intros pc' (H2,H3).
elim (in_factorize2 _ _ _ H0 pc' H2); intros m'' (H4,H5).
rewrite (instructionAt_eq_word P m' m'' pc pc'); auto.
apply in_call_invoke with m t l; auto.
Qed.
Fixpoint invoke_list_rec (p:positive) (l:list Instruction) {struct l} : list positive :=
match l with
nil => nil
| (invokevirtual _)::q => p::(invoke_list_rec (Psucc p) q)
| _::q => (invoke_list_rec (Psucc p) q)
end.
Definition invoke_list (P:Program) (m:MethodName) : list positive :=
match (searchMethod P m) with
None => nil
| Some M => invoke_list_rec xH (instructions M)
end.
Lemma nth_invoke_list : forall l n n' mID,
nth_error l n = Some (invokevirtual mID) ->
In (P_of_succ_nat (plus n n')) (invoke_list_rec (P_of_succ_nat n') l).
induction l; destruct n; simpl; intros.
inversion_clear H.
inversion_clear H.
injection H; clear H; intros; subst.
left; auto.
generalize (IHl _ (S n') _ H); rewrite <- plus_n_Sm ;
simpl; intros.
destruct a; auto.
right; auto.
Qed.
Lemma is_invoke_in_invoke_list : forall P m pc mID,
instructionAt P m pc = Some (invokevirtual mID) ->
In (word2pos pc) (invoke_list P m).
unfold invoke_list, instructionAt.
intros P m pc mID.
CaseEq (searchMethod P m).
intros M H H1.
assert (In (word2pos pc) (invoke_list_rec (P_of_succ_nat 0) (instructions M))); auto.
replace (word2pos pc) with (P_of_succ_nat (plus (pred (nat_of_P (word2pos pc))) 0)).
apply nth_invoke_list with mID; assumption.
rewrite <- plus_n_O.
destruct pc; simpl.
elim (Psucc_pred x); intros.
subst; auto.
pattern x at 1; rewrite <- H0.
rewrite nat_of_P_succ_morphism; simpl.
rewrite P_of_succ_nat_o_nat_of_P_eq_succ; auto.
intros.
discriminate H0.
Qed.
Lemma in_l : forall (A:Set) (a:A) l,
In a l ->
exists l',
length l = S (length l') /\
forall x, In x l -> In x (a::l').
induction l; simpl; intros.
elim H.
elim H; clear H; intros.
subst; exists l; auto.
elim (IHl H); intros l' (H1',H1).
exists (a0::l'); split; intros.
simpl; auto.
elim H0; intros.
subst; right; left; auto.
elim (H1 _ H2); intros; auto.
right; right; auto.
Qed.
Lemma pc_distincts_length_bounded : forall l1 l2,
(forall pc n, In (pc,n) l1 -> In (word2pos pc) l2) ->
pc_distincts l1 ->
length l1 <= length l2.
induction l1; simpl; intros.
omega.
destruct a as [pc1 n1].
inversion_clear H0.
assert (In (word2pos pc1) l2).
apply (H pc1 n1); auto.
elim (in_l _ _ _ H0); intros l' (H3,H4).
rewrite H3.
apply le_n_S.
apply (IHl1 l'); intros; auto.
elim (H4 pc); intros; eauto.
elim H1; exists pc; exists n; split; auto.
destruct pc; destruct pc1; simpl in *; auto.
Qed.
Lemma length_list2multiset_le_invoke : forall P m t l m' lp,
call P m t l ->
In (m',lp) (factorize l) ->
length (list2multiset lp) <= length (invoke_list P m').
intros.
apply pc_distincts_length_bounded; intros.
elim (in_list2multiset_invoke _ _ _ _ _ _ _ _ H H0 H1); intros mID H2.
apply is_invoke_in_invoke_list with mID; auto.
apply list2multiset_distinct.
Qed.
Lemma nb_invoke_exist : forall P t m,
valid_trace P t ->
exists n, nb_invoke P m t n.
induction 1.
exists 0; constructor.
case (seq_call_dec m H0); intros.
elim IHSemCol'; intros n H2.
exists (S n); constructor; auto.
elim IHSemCol'; intros n H2.
exists n; constructor; auto.
Qed.
Lemma majoration2 : forall P BC MutRec m t n1 l,
gammaBC P MutRec BC t ->
BC m = false ->
MutRec m = false ->
valid_trace P t ->
(forall m' lp n, In (m',lp) (factorize l) -> nb_invoke P m' t n -> n<=n1) ->
(forall m' lp, In (m',lp) (factorize l) -> ~ eq_word m m') ->
call P m t l ->
length l <=
sumlist (fun ml:Word*(list Word) => let (m,l):=ml in
(length (invoke_list P m))*(S n1)) (factorize l).
intros; rewrite sumlist_final.
apply sumlist_bound2; intros.
destruct x as [m' lp].
apply le_trans with (length (list2multiset lp) * S n1).
elim (nb_invoke_exist P t m' H2); intros n' H'.
apply le_trans with (length (list2multiset lp) * S n').
apply (majoration1 P BC MutRec m m' t n' lp l); eauto.
apply mult_le_compat_l.
apply le_n_S; eauto.
generalize (length_list2multiset_le_invoke _ _ _ _ _ _ H5 H6); intros.
apply mult_le_compat_r; auto.
Qed.
Lemma in_factorize3: forall l m lp,
In (m, lp) (factorize l) ->
exists pc, exists m',
eq_word m m' /\ In (m',pc) l /\ In pc lp.
induction l; simpl; intros.
elim H.
destruct a.
elim (in_insere _ _ _ _ _ H).
intros (H1,H2).
elim (IHl _ _ H1); intros pc' (m',(H3,(H4,H5))).
exists pc'; exists m'; split; auto.
intros (lp',(H1,(H2,H3))).
subst.
exists w0.
elim H1; clear H1; intros; subst.
exists w; auto with datatypes.
exists w; auto with datatypes.
apply factorize_distinct.
Qed.
Lemma in_call_cutrent_meth : forall P m t l m' pc',
call P m t l ->
In (m',pc') l ->
exists t',
prefix_tr t' t /\
eq_word m (mSt (currentState t')).
induction 1; intros.
elim H.
exists (t:::st); split.
constructor.
simpl; inversion_clear H; auto.
elim (IHcall H1); intros t' (H2,H3).
exists t'; split; auto.
constructor; auto.
Qed.
Lemma gammaRec_prefix: forall Rec t st,
gammaRec Rec (t ::: st) -> gammaRec Rec t.
unfold gammaRec; intros.
apply H; auto.
constructor; auto.
Qed.
Definition may_call (P:Program) (m' m:MethodName) : Prop :=
exists pc',
exists mID,
exists m'',
instructionAt P m' pc' = Some (invokevirtual mID)
/\ In m'' (implem P mID)
/\ eq_word m m''.
Lemma in_call : forall P Rec m t l m' pc',
gammaRec Rec t ->
call P m t l ->
In (m',pc') l ->
in_set m' (Rec m) = true /\ may_call P m' m.
induction 2; simpl; intros.
elim H0.
elim H2; clear H2; intros.
injection H2; clear H2; intros; subst.
inversion_clear H0; clear IHcall.
assert (in_trace st (t:::st)).
constructor.
generalize (H st H0); clear H H0; intros.
inversion_clear H2 in H3 H; simpl in *.
rewrite (MRec.apply_eq_word Rec _ _ H3).
split.
apply H.
constructor; auto.
exists pc; exists mID.
elim (methodLookup_in_implem _ _ _ _ H6); intros m'' (H1',H2').
exists m''; split; auto.
split; auto.
apply eq_word_trans with (nameMethod M); auto.
apply IHcall; auto.
apply gammaRec_prefix with st; auto.
apply IHcall; auto.
apply gammaRec_prefix with st; auto.
Qed.
Fixpoint max_invoke_list_rec (P:Program) (n:nat) (l:list Method) {struct l} : nat :=
match l with
nil => n
| m::q => match le_lt_dec (length (invoke_list P (nameMethod m))) (max_invoke_list_rec P n q) with
left _ => (max_invoke_list_rec P n q)
| right _ => (length (invoke_list P (nameMethod m)))
end
end.
Definition max_invoke_list (P:Program) :=
max_invoke_list_rec P (length (invoke_list P (nameMethod (main P)))) (methods P).
Lemma max_invoke_list_rec_bound1 : forall P n l M,
In M l ->
(length (invoke_list P (nameMethod M))) <= (max_invoke_list_rec P n l).
induction l; simpl; intros.
elim H.
elim H; clear H; intros.
subst.
case le_lt_dec; intros; auto.
generalize (IHl _ H); clear IHl; intros.
case le_lt_dec; intros; auto.
apply le_trans with (max_invoke_list_rec P n l); auto.
omega.
Qed.
Lemma max_invoke_list_rec_bound2 : forall P n l,
n <= (max_invoke_list_rec P n l).
induction l; simpl; intros; auto.
case le_lt_dec; intros; auto.
apply le_trans with (max_invoke_list_rec P n l); auto.
omega.
Qed.
Lemma searchMethod_eq_word : forall P m1 m2,
eq_word m1 m2 ->
searchMethod P m1 = searchMethod P m2.
unfold searchMethod; intros P.
generalize (main P :: methods P).
induction l; simpl; intros; auto.
case MethodName_dec; intros.
case MethodName_dec; intros; auto.
elim n; apply eq_word_trans with m1; auto.
case MethodName_dec; intros; auto.
elim n; apply eq_word_trans with m2; auto.
Qed.
Lemma invoke_list_eq_word : forall P m1 m2,
eq_word m1 m2 ->
invoke_list P m1 = invoke_list P m2.
unfold invoke_list; intros.
generalize (searchMethod_eq_word P _ _ H); intros.
CaseEq (searchMethod P m1); intros.
CaseEq (searchMethod P m2); intros.
rewrite H1 in H0; rewrite H2 in H0; injection H0; intros; subst.
auto.
rewrite H1 in H0; rewrite H2 in H0; discriminate H0.
rewrite H1 in H0.
CaseEq (searchMethod P m2); intros.
rewrite H2 in H0; discriminate H0.
auto.
Qed.
Lemma max_invoke_list_bound : forall P m,
(length (invoke_list P m)) <= (max_invoke_list P).
unfold max_invoke_list; intros.
CaseEq (searchMethod P m).
intros M H.
generalize (searchMethod_some _ _ _ H); intros.
generalize (searchMethod_some_in _ _ _ H); intros.
elim H1; clear H1; intros.
rewrite (invoke_list_eq_word P m (nameMethod (main P))).
apply max_invoke_list_rec_bound2.
rewrite H1; auto.
rewrite (invoke_list_eq_word P m (nameMethod M)).
apply max_invoke_list_rec_bound1; auto.
auto.
unfold invoke_list.
case (searchMethod P m); intros.
discriminate H.
simpl; omega.
Qed.
Lemma majoration3 : forall P BC MutRec m t n1 l,
gammaBC P MutRec BC t ->
BC m = false ->
MutRec m = false ->
valid_trace P t ->
(forall m' lp n, In (m',lp) (factorize l) -> nb_invoke P m' t n -> n<=n1) ->
(forall m' lp, In (m',lp) (factorize l) -> ~ eq_word m m') ->
call P m t l ->
length l <= (length (factorize l)) * ((max_invoke_list P) * (S n1)).
intros.
apply le_trans with
(sumlist (fun ml:Word*(list Word) => let (m,l):=ml in
(length (invoke_list P m))*(S n1)) (factorize l)).
eapply majoration2; eauto.
apply sumlist_bound; intros.
destruct x as [m' lp].
apply mult_le_compat_r.
apply max_invoke_list_bound.
Qed.
Lemma m_distincts_length_bounded : forall l s n,
(forall m lp, In (m,lp) l -> in_set m s = true) ->
m_distincts l ->
cardinal s = Some n ->
length l <= n.
induction l; simpl; intros.
omega.
destruct a as [m1 lp1].
inversion_clear H0.
assert (in_set m1 s = true).
apply (H m1 lp1); auto.
elim (cardinal_monotone (L.subst s m1 false) s).
rewrite H1.
CaseEq (cardinal (L.subst s m1 false)); intros.
inversion_clear H5.
assert (length l <= n0).
apply IHl with (L.subst s m1 false); auto; intros.
case (eq_word_dec m1 m); intros.
elim H2; eauto.
unfold in_set.
rewrite L.apply_subst2.
apply (H m lp); auto.
red; intros; elim n1; apply eq_word_sym; auto.
omega.
inversion_clear H5.
intros.
generalize (L.apply_monotone s (L.subst s m1 false) (order_refl _ _ (eq_sym _ _ H4)) m1).
unfold in_set in H0; rewrite H0.
assert (((L.subst s m1 false) m1)=false).
unfold L.subst.
destruct s.
unfold L.apply.
rewrite L.apply_subst1'; auto.
discriminate H1.
rewrite H5; intros H'; inversion H'.
destruct s; try constructor.
simpl; constructor.
intros p.
unfold L.substFunc; simpl.
case (positive_dec p (proj1_sig m1)); intros.
subst; unfold L.modify_tree, apply_tree; simpl.
rewrite TabTree.apply_modify_tree1.
constructor.
unfold L.modify_tree, apply_tree; simpl.
rewrite TabTree.apply_modify_tree2; auto.
apply BoolLattice.Pos.order_refl.
apply BoolLattice.Pos.eq_refl.
Qed.
Lemma may_call_eq_word : forall P m m1 m2,
eq_word m1 m2 ->
may_call P m1 m ->
may_call P m2 m.
intros.
elim H0; clear H0; intros pc (mID,(m'',H2)).
exists pc; exists mID; exists m''; intuition.
rewrite (instructionAt_eq_word P m2 m1 pc pc); auto.
Qed.
Lemma in_factorize_in_Rec : forall P Rec m t l m' lp',
gammaRec Rec t ->
call P m t l ->
In (m',lp') (factorize l) ->
in_set m' (Rec m) = true /\ may_call P m' m.
intros.
elim (in_factorize3 _ _ _ H1); intros pc' (m'',(H3,(H4,H5))).
elim (in_call P Rec m t l m'' pc' H H0 H4); intros.
split.
apply in_set_eq_word with m''; auto.
apply may_call_eq_word with m''; auto.
Qed.
Lemma majoration4 : forall P Rec BC MutRec m t n1 l n,
gammaRec Rec t ->
gammaBC P MutRec BC t ->
BC m = false ->
MutRec m = false ->
valid_trace P t ->
(forall m' n, in_set m' (Rec m) = true -> may_call P m' m -> nb_invoke P m' t n -> n<=n1) ->
(forall m', in_set m' (Rec m) = true -> may_call P m' m -> ~ eq_word m m') ->
call P m t l ->
cardinal (Rec m) = Some n ->
length l <= n * ((max_invoke_list P) * (S n1)).
intros.
apply le_trans with
((length (factorize l)) * ((max_invoke_list P) * (S n1))).
eapply majoration3; eauto; intros.
apply H4 with m'.
elim (in_factorize_in_Rec P Rec m t l m' lp); auto; intros.
elim (in_factorize_in_Rec P Rec m t l m' lp); auto; intros.
auto.
apply H5.
elim (in_factorize_in_Rec P Rec m t l m' lp); auto; intros.
elim (in_factorize_in_Rec P Rec m t l m' lp); auto; intros.
apply mult_le_compat_r.
apply m_distincts_length_bounded with (Rec m); auto; intros.
elim (in_factorize_in_Rec P Rec m t l m0 lp); auto; intros.
apply factorize_distinct.
Qed.
Lemma call_exist : forall P t m,
valid_trace P t ->
exists l, call P m t l.
induction 1; intros.
exists (nil (A:=(MethodName*progCount))); constructor.
case (seq_call_dec m H0); intros.
elim IHSemCol'; intros l H'.
exists ((mSt (currentState tr),pcSt (currentState tr))::l).
constructor; auto.
elim IHSemCol'; intros l H'.
exists l.
constructor; auto.
Qed.
Lemma bounded_calls :
forall P (Rec:MRec.Pos.set) (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (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) ->
(forall M, In M (main P :: methods P) ->
(forall m', in_set m' (Rec (nameMethod M)) = true ->
orderB (BC m') (BC (nameMethod M)))) ->
forall n,
exists N, forall k, k<=n ->
forall m, cardinal (Rec m) = Some k ->
(MutRec m)=false -> (BC m)=false ->
(exists M, In M (main P :: methods P) /\ eq_word m (nameMethod M)) ->
forall tr n',
valid_trace P tr ->
nb_invoke P m tr n' -> le n' N.
intros P Rec MutRec Pred BC HcRec HcMutRec HcPred HcBC1 HcBC2.
induction n; intros.
exists 1; intros k H.
inversion_clear H.
induction tr; intros.
inversion_clear H4 in H3; auto.
inversion_clear H3; auto.
inversion_clear H4 in H6; auto.
elim (cardinal_0_in_set (Rec m) (mSt (currentState tr))); auto.
assert (gammaRec Rec (tr:::s)).
assert (valid_trace P (tr:::s)).
constructor 2 with i; auto.
apply (Rec_correctness P Rec HcRec (VTR P _ H4) H4).
assert (in_trace s (tr:::s)).
constructor; auto.
inversion_clear H3.
rewrite (MRec.apply_eq_word Rec _ _ H10).
apply (H4 s H8).
inversion_clear H9; simpl; constructor; auto.
elim IHn; intros N H; clear IHn.
exists ((S n) * ((max_invoke_list P) * (S N))).
intros.
elim (call_exist P tr m H5); intros l Hl.
generalize (call_is_nb_invoke P m tr _ _ H6 Hl); intros.
subst.
apply le_trans with (k * (max_invoke_list P * S N)).
apply (majoration4 P Rec BC MutRec m tr N l k); auto.
apply (Rec_correctness P Rec HcRec (VTR P _ H5) H5).
apply (BC_correctness P tr Rec MutRec Pred BC HcRec HcMutRec HcPred HcBC1 H5).
intros.
elim H8; intros pc' (mID,(m'',(HH1,(HH2,HH3)))).
generalize (HcRec _ _ (invokevirtual1 mID) HH1); intros.
inversion_clear H10.
generalize (H11 _ HH2); clear H11; rewrite <- (MRec.apply_eq_word Rec _ _ HH3); intros.
assert (order (Rec m') (Rec m)).
apply order_trans with (add_set m' (Rec m')); auto.
apply order_add_set.
elim (cardinal_monotone _ _ H11); intros.
generalize H12; clear H12.
rewrite H1; CaseEq (cardinal (Rec m')); intros.
inversion_clear H13.
apply H with n1 m' tr; auto.
omega.
elim H4; intros M (HM1,HM2); clear H4.
generalize (HcMutRec M HM1); intros H4.
inversion_clear H4.
rewrite <- (MRec.apply_eq_word Rec _ _ HM2) in H13.
generalize (H13 _ H7).
rewrite <- (MMutRec.apply_eq_word MutRec _ _ HM2); rewrite H2; intros.
inversion_clear H4; auto.
elim H4; intros M (HM1,HM2); clear H4.
generalize (HcBC2 M HM1); intros H4.
rewrite <- (MRec.apply_eq_word Rec _ _ HM2) in H4.
generalize (H4 _ H7).
rewrite <- (MBC.apply_eq_word BC _ _ HM2); rewrite H3; intros.
inversion_clear H13; auto.
apply instructionAt_in_methods with pc' (invokevirtual mID); auto.
inversion_clear H13.
assert (in_set m' (Rec m') = true).
apply in_set_monotone with (Rec m); auto.
apply order_refl; apply eq_sym; auto.
assert ((MutRec m')=false).
elim H4; intros M (HM1,HM2); clear H4.
generalize (HcMutRec M HM1); intros H4.
inversion_clear H4.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ HM2) in H14.
rewrite <- (MRec.apply_eq_word Rec _ _ HM2) in H14.
generalize (H14 _ H7); rewrite H2; intros.
inversion_clear H4; auto.
elim (instructionAt_in_methods _ _ _ _ HH1); intros M (HM1,HM2).
elim (HcMutRec M HM1); intros.
assert (in_set (nameMethod M) (Rec (nameMethod M)) = true).
apply in_set_eq_word with m'; auto.
rewrite <- (MRec.apply_eq_word Rec _ _ HM2); auto.
rewrite H17 in H16; rewrite <- (MMutRec.apply_eq_word MutRec _ _ HM2) in H16.
inversion_clear H16 in H14; discriminate H14.
red; intros.
assert (in_set m' (Rec m') = true).
rewrite <- (MRec.apply_eq_word Rec _ _ H9); auto.
elim H8; clear H8; intros pc' (mID,(m'',(HH1,(HH2,HH3)))).
assert ((MutRec m')=false).
elim H4; intros M (HM1,HM2); clear H4.
generalize (HcMutRec M HM1); intros H4.
inversion_clear H4.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ HM2) in H8.
rewrite <- (MRec.apply_eq_word Rec _ _ HM2) in H8.
generalize (H8 _ H7); rewrite H2; intros.
inversion_clear H4; auto.
elim (instructionAt_in_methods _ _ _ _ HH1); intros M (HM1,HM2).
elim (HcMutRec M HM1); intros.
assert (in_set (nameMethod M) (Rec (nameMethod M)) = true).
apply in_set_eq_word with m'; auto.
rewrite <- (MRec.apply_eq_word Rec _ _ HM2); auto.
rewrite H13 in H12; rewrite <- (MMutRec.apply_eq_word MutRec _ _ HM2) in H12.
inversion_clear H12 in H8; discriminate H8.
apply mult_le_compat_r; auto.
Qed.
Definition count_new_m_pc (P:Program) (m:MethodName) (pc:progCount) (st:State) : nat :=
match eq_word_dec m (mSt st) with
left _ =>
match eq_word_dec pc (pcSt st) with
left _ =>
match (instructionAt P (mSt st) (pcSt st)) with
Some (new_o _) => 1
| _ => 0
end
| right _ => 0
end
| right _ => 0
end.
Lemma count_new_m_pc_le1 : forall P m pc st, count_new_m_pc P m pc st <= 1.
unfold count_new_m_pc; intros.
case eq_word_dec; intros; auto.
case eq_word_dec; intros; auto.
case (instructionAt P (mSt st) (pcSt st)); intros; auto.
case i; intros; auto.
Qed.
Lemma count_new_m_pc_case : forall P m pc st,
count_new_m_pc P m pc st = 0 \/
(eq_word m (mSt st) /\
eq_word pc (pcSt st) /\
exists cl, instructionAt P (mSt st) (pcSt st) = Some (new_o cl) /\
count_new_m_pc P m pc st = 1).
unfold count_new_m_pc; intros.
case eq_word_dec; intros; try (left; reflexivity).
case eq_word_dec; intros; try (left; reflexivity).
case (instructionAt P (mSt st) (pcSt st)); intros; try (left; reflexivity).
destruct i; try (left; reflexivity).
right; eauto.
Qed.
Fixpoint nb_new_m_pc (P:Program) (m:MethodName) (pc:progCount) (t:Trace) {struct t} : nat :=
match t with
Trace_init st => count_new_m_pc P m pc st
| Trace_next st t' => (count_new_m_pc P m pc st) + (nb_new_m_pc P m pc t')
end.
Lemma nb_invoke_pred : forall P t m pc n,
valid_trace P t ->
nb_invoke P m t n ->
~ pc_in_current_tr P pc m t ->
nb_new_m_pc P m pc t = 0 \/
exists t', exists n', prefix_tr t' t /\
nb_invoke P m t' n' /\ n = S n' /\
nb_new_m_pc P m pc t = nb_new_m_pc P m pc t'.
induction 1; simpl; intros.
inversion_clear H0.
elim (count_new_m_pc_case P m pc st); intros.
left; auto.
elim H1; constructor; simpl; intuition.
inversion_clear H1.
right.
exists tr; exists n0; repeat (split;auto).
do 2 constructor.
elim (count_new_m_pc_case P m pc st); intros.
rewrite H1; auto.
elim H2; constructor; simpl; intuition.
elim (count_new_m_pc_case P m pc st); intros.
rewrite H1; simpl.
elim IHSemCol'; intros; auto.
elim H5; clear H5; intros t' (n',(H6,(H7,(H8,H9)))).
right; exists t'; exists n'; repeat (split;auto).
constructor; auto.
red ;intros; elim H2; constructor 2; auto.
elim H2; constructor; simpl; intuition.
Qed.
Lemma nb_invoke_nb_new_m : forall P Rec MutRec Pred m pc t,
(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) ->
MutRec m = false ->
(forall cl, instructionAt P m pc = Some (new_o cl) ->
in_set pc (Pred m pc) = false) ->
valid_trace P t ->
prop_prefix_tr (fun t =>
forall n,
nb_invoke P m t n ->
nb_new_m_pc P m pc t <= S n) t.
intros P Rec MutRec Pred m pc t Hc1 Hc2 Hc3 HMr Hnew.
induction 1; simpl; intros; constructor; intros; simpl; auto.
generalize (count_new_m_pc_le1 P m pc st); intros; omega.
inversion_clear H1.
generalize (apply_prop_tr IHSemCol' _ H3); intros.
generalize (count_new_m_pc_le1 P m pc st); intros.
omega.
elim (count_new_m_pc_case P m pc st); intros.
generalize (apply_prop_tr IHSemCol' _ H3); intros; omega.
elim H1; clear H1; intros HH1 (HH2,(cl,(HH3,HH4))).
rewrite HH4.
elim (nb_invoke_pred P tr m pc n); intros; auto.
omega.
elim H1; clear H1; intros t' (n',(H4,(H5,(H6,H7)))); subst.
generalize (apply_prop_tr (apply_prop_prefix _ _ _ H4 IHSemCol') n' H5); intros.
omega.
assert (valid_trace P (tr:::st)).
constructor 2 with i; auto.
generalize (apply_prop_tr (Pred_correctness P _ _ _ Hc1 Hc2 Hc3 (VTR P _ H1) H1));
simpl.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ HH1); intros.
generalize (H4 HMr pc); clear H4; intros.
red ; intros.
assert (false = true).
rewrite <- (Hnew cl).
rewrite (MPred'.apply_eq_word (MPred.apply Pred m) _ _ HH2).
rewrite (MPred.apply_eq_word Pred _ _ HH1).
apply H4.
constructor.
red; intros; elim H2; apply seq_call_eq_word with (mSt st); auto.
apply pc_in_current_tr_eq_word with m; auto.
rewrite (instructionAt_eq_word P m (mSt st) pc (pcSt st)); auto.
discriminate H6.
Qed.
Definition count_new_m (P:Program) (m:MethodName) (st:State) : nat :=
match (eq_word_dec m (mSt st)) with
left _ =>
match (instructionAt P (mSt st) (pcSt st)) with
Some (new_o _) => 1
| _ => 0
end
| right_ => 0
end.
Fixpoint nb_new_m (P:Program) (m:MethodName) (t:Trace) {struct t} : nat :=
match t with
Trace_init st => count_new_m P m st
| Trace_next st t' => (count_new_m P m st) + (nb_new_m P m t')
end.
Fixpoint new_list_rec (p:positive) (l:list Instruction) {struct l} : list positive :=
match l with
nil => nil
| (new_o _)::q => p::(new_list_rec (Psucc p) q)
| _::q => (new_list_rec (Psucc p) q)
end.
Definition new_list (P:Program) (m:MethodName) : list positive :=
match (searchMethod P m) with
None => nil
| Some M => new_list_rec xH (instructions M)
end.
Lemma nth_new_list : forall l n n' cl,
nth_error l n = Some (new_o cl) ->
In (P_of_succ_nat (plus n n')) (new_list_rec (P_of_succ_nat n') l).
induction l; destruct n; simpl; intros.
inversion_clear H.
inversion_clear H.
injection H; clear H; intros; subst.
left; auto.
generalize (IHl _ (S n') _ H); rewrite <- plus_n_Sm ;
simpl; intros.
destruct a; auto.
right; auto.
Qed.
Lemma is_new_in_new_list : forall P m pc cl,
instructionAt P m pc = Some (new_o cl) ->
In (word2pos pc) (new_list P m).
unfold new_list, instructionAt.
intros P m pc mID.
CaseEq (searchMethod P m).
intros M H H1.
assert (In (word2pos pc) (new_list_rec (P_of_succ_nat 0) (instructions M))); auto.
replace (word2pos pc) with (P_of_succ_nat (plus (pred (nat_of_P (word2pos pc))) 0)).
apply nth_new_list with mID; assumption.
rewrite <- plus_n_O.
destruct pc; simpl.
elim (Psucc_pred x); intros.
subst; auto.
pattern x at 1; rewrite <- H0.
rewrite nat_of_P_succ_morphism; simpl.
rewrite P_of_succ_nat_o_nat_of_P_eq_succ; auto.
intros.
discriminate H0.
Qed.
Fixpoint insere_word (x:Word) (l:list Word) {struct l} : list Word :=
match l with
nil => x::nil
| y::q => match eq_word_dec x y with
left _ => y::q
| right _ => y::(insere_word x q)
end
end.
Inductive word_distincts : list (Word) -> Prop :=
word_distincts0 : word_distincts nil
| word_distincts1 : forall x l,
~(exists y, In y l /\ eq_word x y) ->
word_distincts l ->
word_distincts (x::l).
Lemma in_insere_word : forall l x y,
In y (insere_word x l) ->
eq_word x y \/ In y l.
induction l; simpl; intros.
intuition.
subst; auto.
generalize H; clear H; case eq_word_dec; intros.
elim H; intros; auto.
elim H; intros; auto.
elim (IHl _ _ H0); intros; auto.
Qed.
Lemma in_insere_word2 : forall l x y,
In y l ->
In y (insere_word x l).
induction l; simpl; intros.
intuition.
case eq_word_dec; intros.
elim H; intros; auto.
elim H; intros; subst; auto.
left; auto.
right; auto.
Qed.
Lemma in_insere_word3 : forall l x,
exists y, eq_word x y /\
In y (insere_word x l).
induction l; simpl; intros.
exists x; intuition.
case eq_word_dec; intros.
exists a; intuition.
elim (IHl x); intros.
exists x0; intuition.
Qed.
Lemma insere_word_distinct : forall l x,
word_distincts l ->
word_distincts (insere_word x l).
induction l; simpl; intros.
constructor.
red ; intros (y,(H1,H2)).
inversion H1.
constructor.
case eq_word_dec; intros; auto.
inversion_clear H.
constructor.
red ; intros (y,(H3,H2)).
elim H0; clear H0.
elim (in_insere_word _ _ _ H3); intros.
elim n; apply eq_word_trans with y; auto.
eauto.
auto.
Qed.
Fixpoint pc_new (P:Program) (m:MethodName) (t:Trace) {struct t}: list progCount :=
match t with
Trace_init st =>
match (count_new_m P m st) with
0 => nil
| _ => (pcSt st)::nil
end
| Trace_next st t' =>
match (count_new_m P m st) with
0 => pc_new P m t'
| _ => insere_word (pcSt st) (pc_new P m t')
end
end.
Lemma pc_new_distinct : forall P m t, word_distincts (pc_new P m t).
induction t; simpl; intros.
case (count_new_m P m s); intros; constructor.
red; intros (y,(H1,H2)).
inversion_clear H1.
constructor.
case (count_new_m P m s); intros.
auto.
apply insere_word_distinct; auto.
Qed.
Lemma count_new_m_eq_pc : forall P m s,
count_new_m P m s = count_new_m_pc P m (pcSt s) s.
unfold count_new_m, count_new_m_pc.
intros P m s.
case eq_word_dec; intro; auto.
case eq_word_dec; intro; auto.
elim n; auto.
Qed.
Lemma count_new_m_eq0_pc : forall P m pc s,
count_new_m P m s = 0 -> count_new_m_pc P m pc s = 0.
unfold count_new_m, count_new_m_pc.
intros P m pc s.
case eq_word_dec; intro; auto.
case eq_word_dec; intro; auto.
Qed.
Implicit Arguments count_new_m_eq0_pc [P m s].
Lemma insere_word_sumlist : forall (mes mes':Word->nat) x l,
word_distincts l ->
(forall x y, eq_word x y -> mes x = mes y) ->
(forall x y, eq_word x y -> mes' x = mes' y) ->
(sumlist mes (insere_word x l) = sumlist mes l + mes x
/\ (forall y, In y l -> ~ eq_word x y))
\/
exists l',
(forall y, In y l' -> ~ eq_word x y) /\
(forall y, In y l -> eq_word x y \/ In y l') /\
(forall y, In y l' -> In y l) /\
(exists y, eq_word x y /\ In y l) /\
word_distincts l' /\
sumlist mes (insere_word x l) =
sumlist mes l' + mes x /\
sumlist mes' l = sumlist mes' l' + mes' x.
induction l; simpl; intros.
left; auto.
rename H1 into H0'.
elim IHl; intros; auto.
elim H1; clear H1; intros.
case eq_word_dec; intros.
right.
exists l; split; auto.
split.
intros.
elim H3; intros; subst; auto.
simpl; split; auto.
simpl; split.
exists a; auto.
simpl; split; auto.
inversion_clear H; auto.
simpl; split; auto.
rewrite (H0 x a); auto; omega.
rewrite (H0' x a); auto; omega.
left; split; simpl; auto.
rewrite H1; omega.
intros.
elim H3; clear H3; intros; subst; auto.
elim H1; clear H1; intros l' (H1,(H2,(H3',(H4',(H5',(H3,H4)))))).
case eq_word_dec; simpl; intros.
right.
exists l; split; simpl; intros.
inversion_clear H.
red; intros; elim H6; exists y; split; auto.
apply eq_word_trans with x; auto.
split; intros.
elim H5; intros; subst; auto.
split; auto.
split; auto.
exists a; auto.
split; auto.
inversion_clear H; auto.
split; auto.
rewrite (H0 x a); auto.
omega.
rewrite (H0' x a); auto.
omega.
right.
exists (a::l'); split; simpl; intros.
elim H5; clear H5; intros; subst; auto.
split; intros.
elim H5; clear H5; intros; subst; auto.
elim (H2 _ H5); auto.
split; auto.
intros.
elim H5; auto.
split; auto.
elim H4'; intros.
exists x0; intuition.
split; auto.
inversion_clear H.
constructor; auto.
red; intros (y,(H7,H8)); elim H5.
exists y; split; auto.
split.
rewrite H3; omega.
rewrite H4; omega.
inversion_clear H; auto.
Qed.
Lemma count_new_m__0or1 : forall P m st,
count_new_m P m st = 0 \/
count_new_m P m st = 1.
unfold count_new_m; intros.
case eq_word_dec; intros; auto.
case (instructionAt P (mSt st) (pcSt st)); intros; auto.
case i; intros; auto.
Qed.
Lemma count_new_m_pc0 : forall P m pc s,
~ eq_word pc (pcSt s) ->
count_new_m_pc P m pc s = 0.
unfold count_new_m_pc; intros.
case eq_word_dec; auto.
case eq_word_dec; auto.
intros; elim H; auto.
Qed.
Lemma nb_new_m_pc0 : forall P m pc t,
(forall y : Word, In y (pc_new P m t) -> ~ eq_word pc y) ->
nb_new_m_pc P m pc t = 0.
induction t; simpl.
CaseEq (count_new_m P m s); intros.
apply count_new_m_eq0_pc; auto.
apply count_new_m_pc0.
auto with datatypes.
CaseEq (count_new_m P m s); intros.
rewrite IHt; auto.
rewrite count_new_m_eq0_pc; auto.
rewrite count_new_m_pc0; auto.
rewrite IHt; auto.
intros.
apply H0.
apply in_insere_word2; auto.
elim (in_insere_word3 (pc_new P m t) (pcSt s)); intros pc' (H1,H2).
generalize (H0 _ H2); intros.
red; intros; elim H3; apply eq_word_trans with (pcSt s); auto.
Qed.
Lemma eq_sumlist' : forall (A:Set) (f1 f2:A->nat) l,
(forall x, In x l -> f1 x = f2 x) -> sumlist f1 l = sumlist f2 l.
induction l; simpl; intros; auto.
Qed.
Lemma count_new_m_pc_eq: forall P m pc1 pc2 t,
eq_word pc1 pc2 ->
count_new_m_pc P m pc1 t = count_new_m_pc P m pc2 t.
unfold count_new_m_pc; intros.
case eq_word_dec; intros.
case eq_word_dec; intros.
case eq_word_dec; intros.
auto.
elim n; apply eq_word_trans with pc1; auto.
case eq_word_dec; intros.
elim n; apply eq_word_trans with pc2; auto.
auto.
auto.
Qed.
Lemma nb_new_m_pc_eq: forall P m pc1 pc2 t,
eq_word pc1 pc2 ->
nb_new_m_pc P m pc1 t = nb_new_m_pc P m pc2 t.
induction t; simpl; intros.
apply count_new_m_pc_eq; auto.
rewrite IHt; auto.
rewrite (count_new_m_pc_eq P m pc1 pc2); auto.
Qed.
Lemma nb_new_m_sumlist : forall P m t,
nb_new_m P m t =
sumlist (fun pc => nb_new_m_pc P m pc t) (pc_new P m t).
induction t; simpl; intros.
elim (count_new_m__0or1 P m s); intros Heq; rewrite Heq; simpl; auto.
rewrite <- count_new_m_eq_pc; omega.
elim (count_new_m__0or1 P m s); intros Heq; rewrite Heq; intros; simpl; auto.
rewrite IHt.
apply eq_sumlist; intros.
rewrite (count_new_m_eq0_pc x Heq); auto.
elim (insere_word_sumlist (fun pc : progCount => count_new_m_pc P m pc s + nb_new_m_pc P m pc t) (fun pc : progCount => nb_new_m_pc P m pc t) (pcSt s) (pc_new P m t)).
intros (H1,H2).
apply trans_eq with (sumlist
(fun pc : progCount =>
count_new_m_pc P m pc s + nb_new_m_pc P m pc t)
(pc_new P m t) +
(count_new_m_pc P m (pcSt s) s + nb_new_m_pc P m (pcSt s) t)); auto.
rewrite count_new_m_eq_pc in Heq; rewrite Heq.
rewrite nb_new_m_pc0.
replace (nb_new_m P m t) with
(sumlist
(fun pc : progCount => count_new_m_pc P m pc s + nb_new_m_pc P m pc t)
(pc_new P m t)).
omega.
rewrite IHt; apply eq_sumlist'; intros.
rewrite count_new_m_pc0; auto.
red; intros; elim (H2 x); auto.
auto.
intros (l',(H1,(H2,(H3,(H4,(H5,(H6,H7))))))).
apply trans_eq with (sumlist
(fun pc : progCount =>
count_new_m_pc P m pc s + nb_new_m_pc P m pc t) l' +
(count_new_m_pc P m (pcSt s) s + nb_new_m_pc P m (pcSt s) t)); auto.
rewrite <- count_new_m_eq_pc.
rewrite Heq.
rewrite IHt.
apply trans_eq with (S (sumlist (fun pc : progCount => nb_new_m_pc P m pc t) l' +
nb_new_m_pc P m (pcSt s) t)); auto.
replace (sumlist (fun pc : progCount => nb_new_m_pc P m pc t) l')
with (sumlist
(fun pc : progCount => count_new_m_pc P m pc s + nb_new_m_pc P m pc t)
l').
omega.
apply eq_sumlist'; intros.
rewrite count_new_m_pc0; auto.
red; intros; elim (H1 x); auto.
apply pc_new_distinct.
intros.
rewrite (nb_new_m_pc_eq P m x y); auto.
rewrite (count_new_m_pc_eq P m x y); auto.
intros.
rewrite (nb_new_m_pc_eq P m x y); auto.
Qed.
Lemma count_new_m_pc_is_new : forall P m st,
(count_new_m P m st) = 1 ->
exists cl, instructionAt P m (pcSt st) = Some (new_o cl).
unfold count_new_m; intros P m st.
case eq_word_dec; intro; try (intros H'; discriminate H').
CaseEq (instructionAt P (mSt st) (pcSt st)); intro; try (intros H'; discriminate H').
intros H.
destruct i; intros H'; try discriminate H'.
exists c.
rewrite (instructionAt_eq_word P m (mSt st) (pcSt st) (pcSt st)); auto.
Qed.
Lemma in_pc_new_is_new : forall P m t pc,
In pc (pc_new P m t) ->
exists cl, instructionAt P m pc = Some (new_o cl).
induction t; simpl; intros.
elim (count_new_m__0or1 P m s); intros.
rewrite H0 in H.
elim H.
rewrite H0 in H.
elim H; intros.
subst.
apply count_new_m_pc_is_new; auto.
elim H1.
elim (count_new_m__0or1 P m s); intros.
rewrite H0 in H.
auto.
rewrite H0 in H.
elim (in_insere_word (pc_new P m t) (pcSt s) pc); intros.
elim (count_new_m_pc_is_new P m s); auto; intros.
rewrite (instructionAt_eq_word P m m (pcSt s) pc) in H2; eauto.
auto.
auto.
Qed.
Lemma word_distincts_length_bounded : forall l1 l2,
(forall pc, In pc l1 -> In (word2pos pc) l2) ->
word_distincts l1 ->
length l1 <= length l2.
induction l1; simpl; intros.
omega.
inversion_clear H0.
assert (In (word2pos a) l2).
auto.
elim (in_l _ _ _ H0); intros l' (H3,H4).
rewrite H3.
apply le_n_S.
apply (IHl1 l'); intros; auto.
elim (H4 pc); intros; eauto.
elim H1; exists pc; split; auto.
destruct pc; destruct a; simpl in *; auto.
Qed.
Definition count_new (P:Program) (st:State) : nat :=
match (instructionAt P (mSt st) (pcSt st)) with
Some (new_o _) => 1
| _ => 0
end.
Fixpoint nb_new (P:Program) (t:Trace) {struct t} : nat :=
match t with
Trace_init st => count_new P st
| Trace_next st t' => (count_new P st) + (nb_new P t')
end.
Lemma pc_new_bounded_by_nrw_list : forall P m t,
length (pc_new P m t) <= length (new_list P m).
intros.
apply word_distincts_length_bounded.
intros.
elim (in_pc_new_is_new _ _ _ _ H); intros cl H1.
apply is_new_in_new_list with cl; auto.
apply pc_new_distinct.
Qed.
Fixpoint insereM (M:Method) (l:list Method) {struct l} : list Method :=
match l with
nil => M::nil
| M0::q =>
match eq_word_dec (nameMethod M) (nameMethod M0) with
left _ => M0::q
| right _ => M0::(insereM M q)
end
end.
Fixpoint filterM (l:list Method) : list Method :=
match l with
nil => nil
| M::q => insereM M (filterM q)
end.
Lemma in_insereM1 : forall M0 M q,
In M0 (insereM M q) ->
eq_word (nameMethod M0) (nameMethod M)
\/
In M0 q.
induction q; simpl; intros.
elim H; intros; subst; auto.
generalize H; case eq_word_dec; clear H; intros.
elim H; clear H; intros; subst; auto.
elim H; clear H; intros; subst; auto.
intuition.
Qed.
Lemma in_insereM2 : forall M l,
exists M', eq_word (nameMethod M) (nameMethod M') /\
In M' (insereM M l).
induction l; simpl.
eauto.
case eq_word_dec; intros.
exists a; split; auto with datatypes.
elim IHl; intros M' (H1,H2).
exists M'; auto with datatypes.
Qed.
Lemma in_insereM3 : forall M0 M l,
In M0 l ->
In M0 (insereM M l).
induction l; simpl; intros.
elim H.
elim H; clear H; intros; subst; case eq_word_dec; intros; auto with datatypes.
Qed.
Inductive M_distinct : list Method -> Prop :=
M_distinct0 : M_distinct nil
| M_distinct1 : forall M l,
(forall M0, In M0 l -> ~ eq_word (nameMethod M) (nameMethod M0)) ->
M_distinct l ->
M_distinct (M::l).
Lemma insereM_distinct : forall M l,
M_distinct l ->
M_distinct (insereM M l).
induction l; simpl.
repeat constructor.
intros.
elim H0.
intros H; inversion_clear H.
case eq_word_dec; intros; constructor; auto; intros.
elim (in_insereM1 _ _ _ H); intros.
red; intros; elim n; apply eq_word_sym;
apply eq_word_trans with (nameMethod M0); auto.
auto.
Qed.
Lemma filterM_distinct : forall l,
M_distinct (filterM l).
induction l; simpl.
constructor.
apply insereM_distinct; auto.
Qed.
Lemma M_distinct_permute_sumlist : forall M l,
M_distinct l ->
In M l ->
exists l',
(forall (mes:Method->nat), sumlist mes l = mes M + sumlist mes l') /\
forall M', In M' l' -> ~ eq_word (nameMethod M) (nameMethod M').
induction 1; simpl; intros.
elim H.
elim H1; clear H1; intros.
subst; exists l; split; auto.
elim (IHM_distinct H1); clear IHM_distinct; intros l' (H2,H3).
exists (M0::l'); split; intros.
rewrite H2; simpl; omega.
elim H4; clear H4; intros; subst; auto.
red; intros; elim (H _ H1); apply eq_word_sym; auto.
Qed.
Lemma sumlist0 : forall (A:Set) l, sumlist (fun (a:A) => 0) l = 0.
induction l; simpl; auto.
Qed.
Lemma count_new_m_eq : forall P st,
count_new P st = count_new_m P (mSt st) st.
unfold count_new_m, count_new.
intros P st; case eq_word_dec; intros; auto.
elim n; auto.
Qed.
Lemma count_new_m_eq_word : forall m1 m2 P st,
eq_word m1 m2 ->
count_new_m P m1 st = count_new_m P m2 st.
unfold count_new_m, count_new.
intros m1 m2 P st; case eq_word_dec; intros; auto.
case eq_word_dec; intros; auto.
elim n; apply eq_word_trans with m1; auto.
case eq_word_dec; intros; auto.
elim n; apply eq_word_trans with m2; auto.
Qed.
Lemma nb_new_m_eq_word : forall m1 m2 P t,
eq_word m1 m2 ->
nb_new_m P m1 t = nb_new_m P m2 t.
induction t; simpl; intros.
apply count_new_m_eq_word; auto.
rewrite IHt; auto.
rewrite (count_new_m_eq_word m1 m2); auto.
Qed.
Lemma count_new_m_eq0 : forall P st m,
~ eq_word (mSt st) m ->
count_new_m P m st = 0.
unfold count_new_m.
intros P st m; case eq_word_dec; intros; auto.
elim H; apply eq_word_sym; auto.
Qed.
Lemma valid_method_invariant : forall P t,
valid_trace P t ->
exists M, In M (main P :: methods P) /\ eq_word (mSt (currentState t)) (nameMethod M).
intros P t.
cut (valid_trace P t -> forall m, m_in_sf m (sfSt (currentState t)) \/ m=(mSt (currentState t)) ->
exists M, In M (main P :: methods P) /\ eq_word m (nameMethod M)).
intros H; intros; apply H; auto.
induction 1; simpl.
inversion_clear H; simpl; intros.
elim H; clear H; intros; subst; auto.
inversion H.
eauto.
inversion_clear H0 in IHSemCol'; simpl in *; auto.
intros m0 [H'|H'].
inversion_clear H'; auto.
elim (IHSemCol' m); auto; intros M' (H1',H2').
exists M'; split; auto.
apply eq_word_trans with m; auto.
subst.
exists M; split; auto.
apply methodLookup_some_in with mID (class o); auto.
intros.
apply IHSemCol'.
elim H0; clear H0; intros.
left; constructor 2; auto.
left; constructor 1; subst; auto.
Qed.
Lemma in_filterM : forall M l,
In M l ->
exists M', eq_word (nameMethod M) (nameMethod M') /\ In M' (filterM l).
induction l; simpl; intros.
elim H.
elim H; clear H; intros ;subst.
apply in_insereM2; auto.
elim (IHl H); intros M' (H1,H2).
exists M'; split; auto.
apply in_insereM3; auto.
Qed.
Lemma nb_new_sumlist : forall P t,
valid_trace P t ->
nb_new P t =
sumlist (fun M => nb_new_m P (nameMethod M) t) (filterM ((main P)::(methods P))).
induction 1; simpl; intros.
assert (mSt st = nameMethod (main P)).
inversion_clear H; auto.
elim (in_insereM2 (main P) (filterM (methods P))); intros M' (H1,H2).
elim (M_distinct_permute_sumlist M' (insereM (main P) (filterM (methods P))));
auto.
intros l' (H3,H4).
rewrite H3; clear H3.
replace (sumlist (fun M : Method => count_new_m P (nameMethod M) st) l')
with (sumlist (fun M : Method => 0) l').
rewrite sumlist0.
rewrite count_new_m_eq.
rewrite (count_new_m_eq_word (mSt st) (nameMethod (main P))); auto.
rewrite (count_new_m_eq_word (nameMethod (main P)) (nameMethod M')); auto.
rewrite H0; auto.
apply eq_sumlist'; intros.
rewrite count_new_m_eq0; auto.
rewrite H0; auto.
red; intros; elim (H4 x); auto.
apply eq_word_trans with (nameMethod (main P)); auto.
apply insereM_distinct.
apply filterM_distinct.
rewrite count_new_m_eq.
elim (valid_method_invariant P (tr:::st)).
intros M (H1,H2); simpl in *.
elim (in_filterM M ((main P)::(methods P))); auto; intros M' (H3,H4).
elim (M_distinct_permute_sumlist M' (insereM (main P) (filterM (methods P))));
auto.
intros l' (H5,H6).
rewrite H5; rewrite H5 in IHSemCol'; clear H5.
replace (sumlist (fun M : Method =>
count_new_m P (nameMethod M) st + nb_new_m P (nameMethod M) tr) l')
with (sumlist (fun M : Method => nb_new_m P (nameMethod M) tr) l').
rewrite IHSemCol'.
rewrite (count_new_m_eq_word (mSt st) (nameMethod M')).
omega.
apply eq_word_trans with (nameMethod M); auto.
apply eq_sumlist'; intros.
rewrite count_new_m_eq0; auto.
red; intros; elim (H6 x); auto.
apply eq_word_sym; apply eq_word_trans with (nameMethod M); auto.
apply eq_word_trans with (mSt st); auto.
apply insereM_distinct.
apply filterM_distinct.
constructor 2 with i; auto.
Qed.
Inductive AllConstr (P:Program) (Rec:MRec.Pos.set) (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set) : Prop :=
AllConstr_def :
(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) ->
(forall M, In M (main P :: methods P) ->
(forall m', in_set m' (Rec (nameMethod M)) = true ->
orderB (BC m') (BC (nameMethod M)))) ->
(forall m pc cl, instructionAt P m pc = Some (new_o cl) ->
in_set pc (Pred m pc) = false /\
MutRec m = false /\
BC m = false) ->
AllConstr P Rec MutRec Pred BC.
Lemma nb_new_m_pc_eq0_or_new : forall P m pc t,
nb_new_m_pc P m pc t = 0 \/ exists cl, instructionAt P m pc = Some (new_o cl).
induction t; simpl.
elim (count_new_m_pc_case P m pc s); intros; intuition.
elim H2; intros cl (H3,H4).
right; exists cl.
rewrite (instructionAt_eq_word P m (mSt s) pc (pcSt s)); eauto.
elim IHt; intros; auto.
rewrite H.
elim (count_new_m_pc_case P m pc s); intros; intuition.
elim H3; intros cl (H4,_).
right; exists cl.
rewrite (instructionAt_eq_word P m (mSt s) pc (pcSt s)); eauto.
Qed.
Lemma bounded_news :
forall P (Rec:MRec.Pos.set) (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set),
AllConstr P Rec MutRec Pred BC ->
exists N,
forall M pc tr,
In M ((main P)::(methods P)) ->
valid_trace P tr ->
nb_new_m_pc P (nameMethod M) pc tr <= N.
intros.
inversion_clear H.
elim (bounded_calls P Rec MutRec Pred BC H0 H1 H2 H3 H4 (CardMax 0)).
intros N H.
exists (S N); intros.
elim (nb_new_m_pc_eq0_or_new P (nameMethod M) pc tr); intros.
rewrite H8; omega.
elim H8; clear H8; intros cl H8.
generalize (H5 _ _ _ H8); intros (HH1,(HH2,HH3)).
elim (cardinal_max (Rec (nameMethod M))); intros.
generalize (H1 _ H6); intros (H12,H13).
rewrite H9 in H13; simpl in H13.
inversion_clear H13 in HH2; discriminate HH2.
elim H9; clear H9; intros k (H11,H12).
elim (nb_invoke_exist P tr (nameMethod M)); auto.
intros n Hn.
apply le_trans with (S n).
assert ( prop_prefix_tr (fun t =>
forall n,
nb_invoke P (nameMethod M) t n ->
nb_new_m_pc P (nameMethod M) pc t <= S n) tr).
apply (nb_invoke_nb_new_m P Rec MutRec Pred (nameMethod M) pc tr); auto.
apply (apply_prop_tr H9); auto.
apply le_n_S.
apply H with k (nameMethod M) tr; auto.
exists M; auto.
Qed.
Fixpoint max_new_list_rec (P:Program) (n:nat) (l:list Method) {struct l} : nat :=
match l with
nil => n
| m::q => match le_lt_dec (length (new_list P (nameMethod m))) (max_new_list_rec P n q) with
left _ => (max_new_list_rec P n q)
| right _ => (length (new_list P (nameMethod m)))
end
end.
Definition max_new_list (P:Program) :=
max_new_list_rec P (length (new_list P (nameMethod (main P)))) (methods P).
Lemma max_new_list_rec_bound1 : forall P n l M,
In M l ->
(length (new_list P (nameMethod M))) <= (max_new_list_rec P n l).
induction l; simpl; intros.
elim H.
elim H; clear H; intros.
subst.
case le_lt_dec; intros; auto.
generalize (IHl _ H); clear IHl; intros.
case le_lt_dec; intros; auto.
apply le_trans with (max_new_list_rec P n l); auto.
omega.
Qed.
Lemma max_new_list_rec_bound2 : forall P n l,
n <= (max_new_list_rec P n l).
induction l; simpl; intros; auto.
case le_lt_dec; intros; auto.
apply le_trans with (max_new_list_rec P n l); auto.
omega.
Qed.
Lemma new_list_eq_word : forall P m1 m2,
eq_word m1 m2 ->
new_list P m1 = new_list P m2.
unfold new_list; intros.
generalize (searchMethod_eq_word P _ _ H); intros.
CaseEq (searchMethod P m1); intros.
CaseEq (searchMethod P m2); intros.
rewrite H1 in H0; rewrite H2 in H0; injection H0; intros; subst.
auto.
rewrite H1 in H0; rewrite H2 in H0; discriminate H0.
rewrite H1 in H0.
CaseEq (searchMethod P m2); intros.
rewrite H2 in H0; discriminate H0.
auto.
Qed.
Lemma max_new_list_bound : forall P m,
(length (new_list P m)) <= (max_new_list P).
unfold max_new_list; intros.
CaseEq (searchMethod P m).
intros M H.
generalize (searchMethod_some _ _ _ H); intros.
generalize (searchMethod_some_in _ _ _ H); intros.
elim H1; clear H1; intros.
rewrite (new_list_eq_word P m (nameMethod (main P))).
apply max_new_list_rec_bound2.
rewrite H1; auto.
rewrite (new_list_eq_word P m (nameMethod M)).
apply max_new_list_rec_bound1; auto.
auto.
unfold new_list.
case (searchMethod P m); intros.
discriminate H.
simpl; omega.
Qed.
Lemma in_filterM2 : forall M l,
In M (filterM l) ->
exists M', eq_word (nameMethod M) (nameMethod M') /\ In M' l.
induction l; simpl; intros.
elim H.
elim (in_insereM1 _ _ _ H); intros.
exists a; auto.
elim (IHl H0); intros.
exists x; intuition.
Qed.
Lemma big_bound1 : forall P (Rec:MRec.Pos.set) (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set),
AllConstr P Rec MutRec Pred BC ->
exists N, forall t, valid_trace P t ->
nb_new P t <= (length (filterM ((main P)::(methods P)))) *
((max_new_list P) * N).
intros.
elim (bounded_news P Rec MutRec Pred BC H); intros N H1.
exists N; intros.
rewrite nb_new_sumlist; auto.
apply sumlist_bound; intros.
elim (in_filterM2 _ _ H2); intros M' (H3,H4).
rewrite (nb_new_m_eq_word (nameMethod x) (nameMethod M')); auto.
clear H2 H3 x.
rewrite nb_new_m_sumlist.
apply le_trans with (length (pc_new P (nameMethod M') t) * N).
apply sumlist_bound; intros.
apply H1; auto.
apply mult_le_compat_r; auto.
apply le_trans with (length (new_list P (nameMethod M'))).
apply pc_new_bounded_by_nrw_list.
apply max_new_list_bound.
Qed.
Lemma big_bound2 : forall P (Rec:MRec.Pos.set) (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set),
AllConstr P Rec MutRec Pred BC ->
exists N, forall t, valid_trace P t -> nb_new P t <= N.
intros.
elim (big_bound1 P Rec MutRec Pred BC H); intros N H1.
exists ((length (filterM ((main P)::(methods P)))) * ((max_new_list P) * N)); auto.
Qed.
Index
This page has been generated by coqdoc