Library extract
Require Export analysis2.
Require Export List.
Require Export collect.
Require Export Lattice.
Import FiniteSetLattice.
Inductive Constraint : Set :=
C1 : MethodName ->
MethodName ->
(FiniteSetLattice.Pos.set -> FiniteSetLattice.Pos.set) ->
Constraint.
Inductive I (Rec: MRec.Pos.set) : Constraint -> Prop :=
Interpret_C1 : forall m1 m2 F,
order (F (Rec m1)) (Rec m2) ->
I Rec (C1 m1 m2 F).
Definition gen_constr (P:Program) (m:MethodName) (pc:progCount) (i:Instruction) : list Constraint :=
match i with
invokevirtual mID =>
map (fun m' => C1 m m' (fun s => (add_set m s))) (implem P mID)
| _ => nil
end.
Lemma in_map_inv :
forall (A B : Set) (f : A -> B) (l : list A) (y : B),
In y (map f l) ->
exists x, In x l /\ y = f x.
Proof.
induction l; simpl; intros.
elim H.
destruct H; eauto.
elim (IHl y H); intros.
exists x; intuition.
Qed.
Lemma gen_constr_respect_eq : forall P m1 m2 pc1 pc2 i Rec,
eq_word m1 m2 ->
eq_word pc1 pc2 ->
(forall c, In c (gen_constr P m1 pc1 i) -> I Rec c) ->
(forall c, In c (gen_constr P m2 pc2 i) -> I Rec c).
Proof.
destruct i; simpl; intros; try (elim H2; fail).
elim (in_map_inv _ _ _ _ _ H2); intros m' (H3,H4); subst.
constructor.
apply order_trans with (add_set m1 (Rec m1)).
apply order_refl.
apply add_set_eq; auto.
rewrite (MRec.apply_eq_word Rec m1 m2); auto.
apply eq_refl.
assert (I Rec (C1 m1 m' (fun s : set => add_set m1 s))).
apply H1.
apply in_map with (f:=(fun m' : MethodName => C1 m1 m' (fun s : set => add_set m1 s))); auto.
inversion_clear H4; auto.
Qed.
Definition collectRec : Program -> list Constraint :=
collect _ gen_constr.
Lemma verif_all_gen_constr_Rec : forall P Rec m pc r,
(forall c, In c (gen_constr P m pc (rule2instr r)) -> I Rec c) ->
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r.
Proof.
intros.
destruct r; constructor; intros.
simpl in H.
generalize (in_map (fun m' : MethodName => C1 m m' (fun s : set => add_set m s)) _ _ H1); intros.
generalize (H _ H2); clear H2; intro.
inversion_clear H2; auto.
Qed.
Lemma verif_all_collected_Rec : forall P Rec,
(forall c, In c (collectRec P) -> I Rec c) ->
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r.
Proof.
intros.
apply verif_all_gen_constr_Rec; auto; intros.
destruct (in_collect_intro _ gen_constr _ _ _ _ H0)
as [m' (pc',(H4,(H2,H3)))].
apply (gen_constr_respect_eq P m' m pc' pc (rule2instr r) Rec); auto.
Qed.
Definition F (c:Constraint) : MRec.Pos.set -> MRec.Pos.set :=
match c with
(C1 m1 m2 f) => fun s => MRec.subst s m2 (f (s m1))
end.
Module LFP := Iter_fix MRec.
Inductive Mon : Constraint -> Prop :=
Mon_C1 : forall m1 m2 F,
(forall s1 s2, order s1 s2 -> order (F s1) (F s2)) ->
Mon (C1 m1 m2 F).
Lemma F_monotone : forall c, Mon c -> LFP.monotone (F c).
Proof.
destruct c; simpl; intros H s1 s2 H0.
inversion_clear H.
apply MRec.subst_monotone; auto.
apply H1.
apply MRec.apply_monotone; auto.
Qed.
Lemma collected_monotones : forall P c,
In c (collectRec P) -> Mon c.
Proof.
unfold collectRec; intros.
apply prop_on_collect with (P:=P) (gen:=gen_constr); auto.
intros.
destruct i; simpl in H1; try (inversion_clear H1; fail).
destruct (in_map_inv _ _ _ _ _ H1) as [M (H3,H4)]; subst.
constructor; intros.
apply add_set_monotone; auto.
Qed.
Lemma postfix_F_to_I : forall c Rec,
MRec.Pos.order (F c Rec) Rec -> I Rec c.
Proof.
destruct c; simpl; intros; constructor.
apply order_trans with (MRec.subst Rec m0 (s (Rec m)) m0).
apply MRec.apply_subst1; auto.
apply MRec.apply_monotone; auto.
Qed.
Lemma solveRec : forall P,
{ Rec: MRec.Pos.set |
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrRec P Rec m pc r}.
Proof.
intros P.
assert (forall f : MRec.Pos.set -> MRec.Pos.set,
In f (map F (collectRec P)) -> LFP.monotone f).
intros.
elim (in_map_inv _ _ F (collectRec P) f); intros.
destruct H0; subst.
apply F_monotone.
apply collected_monotones with P.
auto.
auto.
exists (LFP.lfp_list (map F (collectRec P)) H).
apply verif_all_collected_Rec.
intros.
apply postfix_F_to_I.
elim (LFP.lfp_list_is_lifp (map F (collectRec P)) H); intros.
apply H1.
apply in_map; auto.
Qed.
Inductive ConstraintMutRec : Set :=
C2 : MethodName -> (FiniteSetLattice.Pos.set -> MMutRec.Pos.set -> bool) ->
ConstraintMutRec
| C3 : MethodName -> (FiniteSetLattice.Pos.set -> bool) ->
ConstraintMutRec.
Inductive IMutRec (Rec : MRec.Pos.set) (MutRec: MMutRec.Pos.set) : ConstraintMutRec -> Prop :=
Interpret_C2 : forall m F,
orderB (F (Rec m) MutRec) (MutRec m) ->
IMutRec Rec MutRec (C2 m F)
| Interpret_C3 : forall m F,
orderB (F (Rec m)) (MutRec m) ->
IMutRec Rec MutRec (C3 m F).
Definition not_empty : set -> bool := fun s =>
match order_dec s bottom with
left _ => false
| right _ => true
end.
Lemma not_empty_monotone : forall s1 s2,
order s1 s2 -> orderB (not_empty s1) (not_empty s2).
unfold not_empty; intros.
case order_dec; intros.
case order_dec; intros; constructor.
case order_dec; intros; try constructor.
elim n; apply L.Pos.order_trans with s2; auto.
Qed.
Definition gen_cMutRec (P:Program) (m:MethodName) : list ConstraintMutRec :=
(C2 m (fun s1 s2 => not_empty (inter s1 s2)))::
(C3 m (fun s => in_set m s))::
nil.
Definition collectMutRec : Program -> list ConstraintMutRec :=
collectM _ gen_cMutRec.
Lemma verif_all_gen_constr_MutRec : forall P Rec MutRec m,
(forall c, In c (gen_cMutRec P m) -> IMutRec Rec MutRec c) ->
ConstrMutRec P Rec MutRec m.
Proof.
intros.
assert (IMutRec Rec MutRec (C3 m (fun s : set => in_set m s))).
apply H; right; left; auto.
assert (IMutRec Rec MutRec (C2 m (fun s1 s2 => not_empty (inter s1 s2)))).
apply H; left; auto.
inversion_clear H0.
inversion_clear H1.
split; auto.
intros.
CaseEq (MutRec m'); intros; try constructor.
assert (order (singleton m') (inter (Rec m) MutRec)).
apply inter_greater_bound; apply in_set_singleton1; auto.
generalize H0; unfold not_empty.
case order_dec; intros; auto.
assert (in_set m' bottom = true).
apply in_set_monotone with (singleton m').
eapply order_trans; eauto.
apply in_singleton.
discriminate H6.
Qed.
Lemma verif_all_collected_MutRec : forall P Rec MutRec,
(forall c, In c (collectMutRec P) -> IMutRec Rec MutRec c) ->
forall M,
In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M).
Proof.
intros.
apply verif_all_gen_constr_MutRec; auto; intros.
apply H.
apply (in_collectM_intro _ gen_cMutRec _ _ H0); auto.
Qed.
Definition F_MutRec (Rec:MRec.Pos.set) (c:ConstraintMutRec) : MMutRec.Pos.set -> MMutRec.Pos.set :=
match c with
(C2 m f) => fun s => MMutRec.subst s m (f (Rec m) s)
| (C3 m f) => fun s => MMutRec.subst s m (f (Rec m))
end.
Module LFP_MutRec := Iter_fix MMutRec.
Inductive Mon_MutRec : ConstraintMutRec -> Prop :=
Mon_C2 : forall m F,
(forall Rec s1 s2, MMutRec.Pos.order s1 s2 -> orderB (F Rec s1) (F Rec s2)) ->
Mon_MutRec (C2 m F)
| Mon_C3 : forall m F, Mon_MutRec (C3 m F).
Lemma F_MutRec_monotone : forall Rec c, Mon_MutRec c -> LFP_MutRec.monotone (F_MutRec Rec c).
Proof.
destruct c; simpl; intros H s1 s2 H0.
inversion_clear H.
apply MMutRec.subst_monotone; auto.
apply H1; auto.
apply MMutRec.subst_monotone; auto.
apply BoolLattice.Pos.order_refl.
apply BoolLattice.Pos.eq_refl.
Qed.
Lemma collected_MutRec_monotones : forall P c,
In c (collectMutRec P) -> Mon_MutRec c.
Proof.
unfold collectMutRec; intros.
apply prop_on_collectM with (P:=P) (gen:=gen_cMutRec).
intros.
unfold gen_cMutRec in H1.
destruct H1.
rewrite <- H1; constructor; intros.
apply not_empty_monotone.
apply inter_greater_bound.
apply inter_bound1.
apply order_trans with s1; auto.
apply inter_bound2.
inversion_clear H2; constructor.
intro; apply H3.
destruct H1.
rewrite <- H1; constructor; intros.
elim H1.
auto.
Qed.
Lemma postfix_F_to_I_MutRec : forall c Rec MutRec,
MMutRec.Pos.order (F_MutRec Rec c MutRec) MutRec -> IMutRec Rec MutRec c.
Proof.
destruct c; simpl; intros; constructor.
apply BoolLattice.Pos.order_trans with (MMutRec.subst MutRec m (b (Rec m) MutRec) m).
apply MMutRec.apply_subst1; auto.
apply MMutRec.apply_monotone; auto.
apply BoolLattice.Pos.order_trans with (MMutRec.subst MutRec m (b (Rec m)) m).
apply MMutRec.apply_subst1; auto.
apply MMutRec.apply_monotone; auto.
Qed.
Lemma solveMutRec : forall P Rec,
{ MutRec: MMutRec.Pos.set |
forall M, In M (main P :: methods P) ->
ConstrMutRec P Rec MutRec (nameMethod M) }.
Proof.
intros P Rec.
assert (forall f : MMutRec.Pos.set -> MMutRec.Pos.set,
In f (map(F_MutRec Rec) (collectMutRec P)) -> LFP_MutRec.monotone f).
intros.
elim (in_map_inv _ _ (F_MutRec Rec) (collectMutRec P) f); intros.
destruct H0; subst.
apply F_MutRec_monotone.
apply collected_MutRec_monotones with P.
auto.
auto.
exists (LFP_MutRec.lfp_list (map(F_MutRec Rec) (collectMutRec P)) H).
apply verif_all_collected_MutRec.
intros.
apply postfix_F_to_I_MutRec.
elim (LFP_MutRec.lfp_list_is_lifp (map(F_MutRec Rec) (collectMutRec P)) H); intros.
apply H1.
apply in_map; auto.
Qed.
Inductive ConstraintPred : Set :=
C4 : MethodName -> progCount -> progCount ->
(FiniteSetLattice.Pos.set -> FiniteSetLattice.Pos.set) ->
ConstraintPred.
Inductive I_Pred (Pred: MPred.Pos.set) : ConstraintPred -> Prop :=
Interpret_C4 : forall m pc1 pc2 F,
order (F (Pred m pc1)) (Pred m pc2) ->
I_Pred Pred (C4 m pc1 pc2 F).
Definition genPred (P:Program) (m:MethodName) (pc:progCount) (i:Instruction) : list ConstraintPred :=
match i with
return_v => nil
| goto pc' => (C4 m pc pc' (fun s => (add_set pc s)))::nil
| If pc' => (C4 m pc pc' (fun s => (add_set pc s)))::(C4 m pc (nextAddress P pc) (fun s => (add_set pc s)))::nil
| _ => (C4 m pc (nextAddress P pc) (fun s => (add_set pc s)))::nil
end.
Lemma genPred_respect_eq : forall P m1 m2 pc1 pc2 i Pred,
eq_word m1 m2 ->
eq_word pc1 pc2 ->
(forall c, In c (genPred P m1 pc1 i) -> I_Pred Pred c) ->
(forall c, In c (genPred P m2 pc2 i) -> I_Pred Pred c).
Proof.
destruct i; simpl; intros; destruct H2; try (elim H2; fail);
try (rewrite <- H2; constructor); try
(apply order_trans with (Pred m1 (nextAddress P pc1)); [
apply order_trans with (add_set pc1 (Pred m1 pc1)); [
apply order_refl;
apply add_set_eq; auto;
apply MPred'.apply_eq; auto;
apply MPred.apply_eq; auto;
apply MPred.Pos.eq_refl |
assert (I_Pred Pred (C4 m1 pc1 (nextAddress P pc1) (fun s : set => add_set pc1 s))); auto;
inversion_clear H3; auto] |
apply order_refl;
apply MPred'.apply_eq; auto;
[apply MPred.apply_eq; auto; apply MPred.Pos.eq_refl |
apply nextAddress_eq_word; auto]]; fail).
apply order_trans with (Pred m1 p); [
apply order_trans with (add_set pc1 (Pred m1 pc1)); [
apply order_refl;
apply add_set_eq; auto;
apply MPred'.apply_eq; auto;
apply MPred.apply_eq; auto;
apply MPred.Pos.eq_refl |
assert (I_Pred Pred (C4 m1 pc1 p (fun s : set => add_set pc1 s))); auto;
inversion_clear H3; auto] |
apply order_refl;
apply MPred'.apply_eq; auto;
apply MPred.apply_eq; auto; apply MPred.Pos.eq_refl].
destruct H2.
rewrite <- H2; constructor.
(apply order_trans with (Pred m1 (nextAddress P pc1)); [
apply order_trans with (add_set pc1 (Pred m1 pc1)); [
apply order_refl;
apply add_set_eq; auto;
apply MPred'.apply_eq; auto;
apply MPred.apply_eq; auto;
apply MPred.Pos.eq_refl |
assert (I_Pred Pred (C4 m1 pc1 (nextAddress P pc1) (fun s : set => add_set pc1 s))); auto;
inversion_clear H3; auto] |
apply order_refl;
apply MPred'.apply_eq; auto;
[apply MPred.apply_eq; auto; apply MPred.Pos.eq_refl |
apply nextAddress_eq_word; auto]]; fail).
destruct H2.
apply order_trans with (Pred m1 p); [
apply order_trans with (add_set pc1 (Pred m1 pc1)); [
apply order_refl;
apply add_set_eq; auto;
apply MPred'.apply_eq; auto;
apply MPred.apply_eq; auto;
apply MPred.Pos.eq_refl |
assert (I_Pred Pred (C4 m1 pc1 p (fun s : set => add_set pc1 s))); auto;
inversion_clear H3; auto] |
apply order_refl;
apply MPred'.apply_eq; auto;
apply MPred.apply_eq; auto; apply MPred.Pos.eq_refl].
Qed.
Definition collectPred : Program -> list ConstraintPred :=
collect _ genPred.
Lemma verif_all_gen_constr_Pred : forall P MutRec Pred m pc r,
(forall c, In c (genPred P m pc (rule2instr r)) -> I_Pred Pred c) ->
instructionAt P m pc = Some (rule2instr r) ->
ConstrPred P MutRec Pred m pc r.
Proof.
intros.
destruct r; constructor; intros;
solve
[assert (I_Pred Pred (C4 m pc (nextAddress P pc) (fun s : set => add_set pc s)));
[apply H; simpl; auto| inversion_clear H1; auto] |
assert (I_Pred Pred (C4 m pc p (fun s : set => add_set pc s)));
[apply H; simpl; auto| inversion_clear H1; auto]].
Qed.
Lemma verif_all_collected_Pred : forall P MutRec Pred,
(forall c, In c (collectPred P) -> I_Pred Pred c) ->
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrPred P MutRec Pred m pc r.
Proof.
intros.
apply verif_all_gen_constr_Pred; auto; intros.
destruct (in_collect_intro _ genPred _ _ _ _ H0)
as [m' (pc',(H4,(H2,H3)))].
apply (genPred_respect_eq P m' m pc' pc (rule2instr r) Pred); auto.
Qed.
Definition update (X:MPred.Pos.set) (m:MethodName) (pc:progCount)
(v:FiniteSetLattice.Pos.set) :=
MPred.modify X m (fun s' => MPred'.subst s' pc v).
Definition F_Pred (c:ConstraintPred) : MPred.Pos.set -> MPred.Pos.set :=
match c with
(C4 m pc1 pc2 f) => fun s => update s m pc2 (f (s m pc1))
end.
Module LFPPred := Iter_fix MPred.
Inductive Mon_Pred : ConstraintPred -> Prop :=
Mon_C4 : forall m pc1 pc2 F,
(forall s1 s2, order s1 s2 -> order (F s1) (F s2)) ->
Mon_Pred (C4 m pc1 pc2 F).
Lemma F_Pred_monotone : forall c, Mon_Pred c -> LFPPred.monotone (F_Pred c).
Proof.
destruct c; simpl; intros H s1 s2 H0; unfold update.
inversion_clear H.
apply MPred.modify_monotone; auto.
intros; apply MPred'.subst_monotone; auto.
apply H1.
apply MPred'.apply_monotone.
apply MPred.apply_monotone; auto.
Qed.
Lemma collectedPred_monotones : forall P c,
In c (collectPred P) -> Mon_Pred c.
Proof.
unfold collectPred; intros.
apply prop_on_collect with (P:=P) (gen:=genPred).
intros.
destruct i; simpl in H1; try (inversion_clear H1; fail);
destruct H1; try (inversion_clear H1; fail);
try (rewrite <- H1; constructor; intros;
apply add_set_monotone; auto).
destruct H1; try (inversion_clear H1; fail);
try (rewrite <- H1; constructor; intros;
apply add_set_monotone; auto).
auto.
Qed.
Lemma postfix_F_to_I_Pred : forall c Pred,
MPred.Pos.order (F_Pred c Pred) Pred -> I_Pred Pred c.
Proof.
destruct c; simpl; intros; constructor.
apply order_trans with
((MPred.modify Pred m
(fun s' : MPred'.Pos.set => MPred'.subst s' p0 (s (Pred m p))))
m p0).
apply order_trans with
(MPred'.subst (Pred m) p0 (s (Pred m p)) p0).
apply MPred'.apply_subst1; auto.
apply MPred'.apply_monotone.
apply MPred.apply_modify1 with (v:=(fun s' : MPred'.Pos.set => MPred'.subst s' p0 (s (Pred m p)))); auto.
apply MPred'.apply_monotone; auto.
apply MPred.apply_monotone; auto.
Qed.
Lemma solvePred : forall P MutRec,
{ Pred: MPred.Pos.set |
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrPred P MutRec Pred m pc r}.
Proof.
intros P.
assert (forall f : MPred.Pos.set -> MPred.Pos.set,
In f (map F_Pred (collectPred P)) -> LFPPred.monotone f).
intros.
elim (in_map_inv _ _ F_Pred (collectPred P) f); intros.
destruct H0; subst.
apply F_Pred_monotone.
apply collectedPred_monotones with P.
auto.
auto.
exists (LFPPred.lfp_list (map F_Pred (collectPred P)) H).
apply verif_all_collected_Pred.
intros.
apply postfix_F_to_I_Pred.
elim (LFPPred.lfp_list_is_lifp (map F_Pred (collectPred P)) H); intros.
apply H1.
apply in_map; auto.
Qed.
Inductive ConstraintBC : Set :=
C5 : MethodName -> bool -> ConstraintBC
| C6 : MethodName -> (FiniteSetLattice.Pos.set -> bool) ->
ConstraintBC.
Inductive IBC (BC: MBC.Pos.set) : ConstraintBC -> Prop :=
Interpret_C5 : forall m b,
orderB b (BC m) ->
IBC BC (C5 m b)
| Interpret_C6 : forall m F,
orderB (F BC) (BC m) ->
IBC BC (C6 m F).
Definition gen_cBC1 (Rec:MRec.Pos.set) (P:Program) (m:MethodName) : list ConstraintBC :=
(C6 m (fun s => not_empty (inter (Rec m) s)))::nil.
Definition collectBC1 (Rec:MRec.Pos.set) : Program -> list ConstraintBC :=
collectM _ (gen_cBC1 Rec).
Lemma verif_all_gen_constr_BC1 : forall P Rec BC M,
In M (main P :: methods P) ->
(forall c, In c (gen_cBC1 Rec P (nameMethod M)) -> IBC BC c) ->
(forall m', in_set m' (Rec (nameMethod M)) = true ->
orderB (BC m') (BC (nameMethod M))).
Proof.
intros.
assert (IBC BC (C6 (nameMethod M) (fun s => not_empty (inter (Rec (nameMethod M)) s)))).
apply H0; left; auto.
inversion_clear H2.
CaseEq (BC m'); intros; try constructor.
assert (order (singleton m') (inter (Rec (nameMethod M)) BC)).
apply inter_greater_bound; apply in_set_singleton1; auto.
generalize H3; unfold not_empty.
case order_dec; intros; auto.
assert (in_set m' bottom = true).
apply in_set_monotone with (singleton m').
eapply order_trans; eauto.
apply in_singleton.
discriminate H6.
Qed.
Lemma verif_all_collected_BC1 : forall P Rec BC,
(forall c, In c (collectBC1 Rec P) -> IBC BC c) ->
forall M,
In M (main P :: methods P) ->
(forall m', in_set m' (Rec (nameMethod M)) = true ->
orderB (BC m') (BC (nameMethod M))).
Proof.
intros.
apply verif_all_gen_constr_BC1 with P Rec; auto; intros.
apply H.
apply (in_collectM_intro _ (gen_cBC1 Rec) _ _ H0); auto.
Qed.
Definition F_BC (c:ConstraintBC) : MBC.Pos.set -> MBC.Pos.set :=
match c with
(C5 m b) => fun s => MBC.subst s m b
| (C6 m f) => fun s => MBC.subst s m (f s)
end.
Module LFP_BC := Iter_fix MBC.
Inductive Mon_BC : ConstraintBC -> Prop :=
Mon_C5 : forall m b, Mon_BC (C5 m b)
| Mon_C6 : forall m f,
(forall s1 s2, MBC.Pos.order s1 s2 -> orderB (f s1) (f s2)) ->
Mon_BC (C6 m f).
Lemma F_BC_monotone : forall c, Mon_BC c -> LFP_BC.monotone (F_BC c).
Proof.
destruct c; simpl; intros H s1 s2 H0.
inversion_clear H.
apply MBC.subst_monotone; auto.
apply BoolLattice.Pos.order_refl; apply BoolLattice.Pos.eq_refl; auto.
apply MBC.subst_monotone; auto.
inversion_clear H.
apply H1; auto.
Qed.
Lemma collected_BC_monotones : forall Rec P c,
In c (collectBC1 Rec P) -> Mon_BC c.
Proof.
unfold collectBC1; intros.
apply prop_on_collectM with (P:=P) (gen:=(gen_cBC1 Rec)).
intros.
unfold gen_cBC1 in H1.
destruct H1.
rewrite <- H1; constructor; intros.
apply not_empty_monotone.
apply inter_greater_bound.
apply inter_bound1.
apply order_trans with s1; auto.
apply inter_bound2.
inversion_clear H2; constructor.
intro; apply H3.
destruct H1.
auto.
Qed.
Lemma postfix_F_to_I_BC1 : forall c BC,
MBC.Pos.order (F_BC c BC) BC -> IBC BC c.
Proof.
destruct c; simpl; intros; constructor.
apply BoolLattice.Pos.order_trans with (MBC.subst BC m b m).
apply MBC.apply_subst1; auto.
apply MBC.apply_monotone; auto.
apply BoolLattice.Pos.order_trans with (MBC.subst BC m (b BC) m).
apply MBC.apply_subst1; auto.
apply MBC.apply_monotone; auto.
Qed.
Definition gen_cBC2 (Pred:MPred.Pos.set) (P:Program) (m:MethodName) (pc:progCount) (i:Instruction) : list ConstraintBC :=
match i with
invokevirtual mID =>
map (fun m' => C5 m' (in_set pc (Pred m pc))) (implem P mID)
| _ => nil
end.
Lemma gen_cBC2_respect_eq : forall Pred P m1 m2 pc1 pc2 i BC,
eq_word m1 m2 ->
eq_word pc1 pc2 ->
(forall c, In c (gen_cBC2 Pred P m1 pc1 i) -> IBC BC c) ->
(forall c, In c (gen_cBC2 Pred P m2 pc2 i) -> IBC BC c).
Proof.
destruct i; simpl; intros; try (elim H2; fail).
elim (in_map_inv _ _ _ _ _ H2); intros m' (H3,H4); subst.
constructor.
assert (IBC BC (C5 m' (in_set pc1 (Pred m1 pc1)))).
apply H1.
apply in_map with (f:=(fun m'0 : MethodName => C5 m'0 (in_set pc1 (Pred m1 pc1)))).
auto.
inversion_clear H4.
apply BoolLattice.Pos.order_trans with (in_set pc1 (Pred m1 pc1)); auto.
CaseEq (in_set pc2 (Pred m2 pc2)); intros; try constructor.
rewrite (in_set_eq' pc1 pc2 (Pred m1 pc1) (Pred m2 pc2)); auto.
rewrite H4; constructor.
apply MPred'.apply_eq; auto.
apply MPred.apply_eq; auto.
apply MPred.Pos.eq_refl.
Qed.
Definition collectBC2 (Pred:MPred.Pos.set) : Program -> list ConstraintBC :=
collect _ (gen_cBC2 Pred).
Lemma verif_all_gen_constr_BC2 : forall P Pred BC m pc r,
(forall c, In c (gen_cBC2 Pred P m pc (rule2instr r)) -> IBC BC c) ->
instructionAt P m pc = Some (rule2instr r) ->
ConstrBC P Pred BC m pc r.
Proof.
intros.
destruct r; constructor; intros.
simpl in H.
generalize (in_map (fun m' : MethodName => C5 m' (in_set pc (Pred m pc))) _ _ H1); intros.
generalize (H _ H2); clear H2; intro.
inversion_clear H2; auto.
Qed.
Lemma verif_all_collected_BC2 : forall Pred P BC,
(forall c, In c (collectBC2 Pred P) -> IBC BC c) ->
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrBC P Pred BC m pc r.
Proof.
intros.
apply verif_all_gen_constr_BC2; auto; intros.
destruct (in_collect_intro _ (gen_cBC2 Pred) _ _ _ _ H0)
as [m' (pc',(H4,(H2,H3)))].
apply (gen_cBC2_respect_eq Pred P m' m pc' pc (rule2instr r) BC); auto.
Qed.
Lemma collected_monotones_BC2 : forall Pred P c,
In c (collectBC2 Pred P) -> Mon_BC c.
Proof.
unfold collectBC2; intros.
apply prop_on_collect with (P:=P) (gen:=(gen_cBC2 Pred)).
intros.
destruct i; simpl in H1; try (inversion_clear H1; fail).
destruct (in_map_inv _ _ _ _ _ H1) as [M (H3,H4)]; subst.
constructor; intros.
auto.
Qed.
Lemma map_app: forall (A B:Set) (f : A->B) (l1 l2 : list A),
map f (l1++l2) = (map f l1)++(map f l2).
Proof.
induction l1; simpl; intros; auto.
rewrite IHl1; auto.
Qed.
Lemma solveBC : forall P (Rec:MRec.Pos.set) (Pred:MPred.Pos.set),
{ BC: MBC.Pos.set |
(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 r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrBC P Pred BC m pc r }.
Proof.
intros P Rec Pred.
assert (forall f : MBC.Pos.set -> MBC.Pos.set,
In f ((map F_BC (collectBC1 Rec P))++(map F_BC (collectBC2 Pred P))) ->
LFP_BC.monotone f).
intros.
destruct (in_app_or _ _ _ H); clear H; intros.
elim (in_map_inv _ _ F_BC (collectBC1 Rec P) f); intros.
destruct H; subst.
apply F_BC_monotone.
apply collected_BC_monotones with Rec P.
auto.
auto.
elim (in_map_inv _ _ F_BC (collectBC2 Pred P) f); intros.
destruct H; subst.
apply F_BC_monotone.
apply collected_monotones_BC2 with Pred P.
auto.
auto.
rewrite <- map_app in H.
exists (LFP_BC.lfp_list (map F_BC ((collectBC1 Rec P)++(collectBC2 Pred P))) H).
split; intros.
apply verif_all_collected_BC1 with P Rec; auto.
intros.
apply postfix_F_to_I_BC1.
elim (LFP_BC.lfp_list_is_lifp (map F_BC (collectBC1 Rec P ++ collectBC2 Pred P)) H); intros.
apply H3.
apply in_map; auto with datatypes.
apply verif_all_collected_BC2; auto.
intros.
apply postfix_F_to_I_BC1.
elim (LFP_BC.lfp_list_is_lifp (map F_BC (collectBC1 Rec P ++ collectBC2 Pred P)) H); intros.
apply H2.
apply in_map; auto with datatypes.
Qed.
Module MMB := BoolLattice.
Inductive ConstraintMB : Set :=
C7 : bool -> ConstraintMB.
Inductive I_MB (MB: MMB.Pos.set) : ConstraintMB -> Prop :=
Interpret_C7 : forall b,
orderB b MB ->
I_MB MB (C7 b).
Definition genMB (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set) (P:Program) (m:MethodName) (pc:progCount) (i:Instruction) : list ConstraintMB :=
match i with
new_o cl => (C7 (in_set pc (Pred m pc)))::
(C7 (MutRec m))::
(C7 (BC m))::nil
| _ => nil
end.
Lemma genMB_respect_eq : forall MutRec Pred BC P m1 m2 pc1 pc2 i MB,
eq_word m1 m2 ->
eq_word pc1 pc2 ->
(forall c, In c (genMB MutRec Pred BC P m1 pc1 i) -> I_MB MB c) ->
(forall c, In c (genMB MutRec Pred BC P m2 pc2 i) -> I_MB MB c).
Proof.
destruct i; simpl; intros; destruct H2; try (elim H2; fail);
try (rewrite <- H2; constructor).
assert (I_MB MB (C7 (in_set pc1 (Pred m1 pc1)))).
apply H1; auto.
inversion_clear H3.
rewrite <- (in_set_eq' pc1 pc2 (Pred m1 pc1) (Pred m2 pc2)); auto.
apply MPred'.apply_eq; auto.
apply MPred.apply_eq; auto.
apply MPred.Pos.eq_refl.
decompose [or] H2; clear H2.
rewrite <- H3; constructor.
assert (I_MB MB (C7 (MutRec m1))); auto.
inversion_clear H2.
rewrite <- (MMutRec.apply_eq_word MutRec _ _ H); auto.
rewrite <- H4; constructor.
assert (I_MB MB (C7 (BC m1))); auto.
inversion_clear H2.
rewrite <- (MBC.apply_eq_word BC _ _ H); auto.
elim H4.
Qed.
Definition collectMB (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set) : Program -> list ConstraintMB :=
collect _ (genMB MutRec Pred BC).
Inductive ConstrMB (P:Program) (MutRec:MMutRec.Pos.set)
(Pred:MPred.Pos.set) (BC:MBC.Pos.set)
(MB:MMB.Pos.set) (m:MethodName) (pc:progCount) : rule -> Prop :=
| constr_mb_invokevirtual : forall mID, ConstrMB P MutRec Pred BC MB m pc (invokevirtual1 mID)
| constr_mb_nop : ConstrMB P MutRec Pred BC MB m pc nop1
| constr_mb_push : forall c, ConstrMB P MutRec Pred BC MB m pc (push1 c)
| constr_mb_push2 : forall c, ConstrMB P MutRec Pred BC MB m pc (push21 c)
| constr_mb_pop : ConstrMB P MutRec Pred BC MB m pc pop1
| constr_mb_numop : forall op, ConstrMB P MutRec Pred BC MB m pc (numop1 op)
| constr_mb_load : forall x, ConstrMB P MutRec Pred BC MB m pc (load1 x)
| constr_mb_store : forall x, ConstrMB P MutRec Pred BC MB m pc (store1 x)
| constr_mb_if1 : forall pc', ConstrMB P MutRec Pred BC MB m pc (If1 pc')
| constr_mb_if2 : forall pc', ConstrMB P MutRec Pred BC MB m pc (If2 pc')
| constr_mb_new_o : forall cl,
orderB (in_set pc (Pred m pc)) MB ->
orderB (MutRec m) MB ->
orderB (BC m) MB ->
ConstrMB P MutRec Pred BC MB m pc (new_o1 cl)
| constr_mb_putfield : forall f, ConstrMB P MutRec Pred BC MB m pc (putfield1 f)
| constr_mb_getfield : forall f, ConstrMB P MutRec Pred BC MB m pc (getfield1 f)
| constr_mb_goto1 : forall pc', ConstrMB P MutRec Pred BC MB m pc (goto1 pc')
| constr_mb_new_a1 : forall t, ConstrMB P MutRec Pred BC MB m pc (new_a1 t)
| constr_mb_arraylength : ConstrMB P MutRec Pred BC MB m pc arraylength1
| constr_mb_arrayload : ConstrMB P MutRec Pred BC MB m pc arrayload1
| constr_mb_arraystore : ConstrMB P MutRec Pred BC MB m pc arraystore1
| constr_mb_return : ConstrMB P MutRec Pred BC MB m pc return_v1.
Lemma verif_all_gen_constr_MB : forall P MutRec Pred BC MB m pc r,
(forall c, In c (genMB MutRec Pred BC P m pc (rule2instr r)) -> I_MB MB c) ->
instructionAt P m pc = Some (rule2instr r) ->
ConstrMB P MutRec Pred BC MB m pc r.
Proof.
intros.
destruct r; constructor; intros.
assert (I_MB MB (C7 (in_set pc (Pred m pc)))).
apply H; unfold genMB; simpl; auto.
inversion_clear H1; auto.
assert (I_MB MB (C7 (MutRec m))); auto.
apply H; unfold genMB; simpl; auto.
inversion_clear H1; auto.
assert (I_MB MB (C7 (BC m))); auto.
apply H; unfold genMB; simpl; auto.
inversion_clear H1; auto.
Qed.
Lemma verif_all_collected_MB : forall P MutRec Pred BC MB,
(forall c, In c (collectMB MutRec Pred BC P) -> I_MB MB c) ->
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrMB P MutRec Pred BC MB m pc r.
Proof.
intros.
apply verif_all_gen_constr_MB; auto; intros.
destruct (in_collect_intro _ (genMB MutRec Pred BC) _ _ _ _ H0)
as [m' (pc',(H4,(H2,H3)))].
apply (genMB_respect_eq MutRec Pred BC P m' m pc' pc (rule2instr r) MB); auto.
Qed.
Definition F_MB (c:ConstraintMB) : MMB.Pos.set -> MMB.Pos.set :=
match c with
(C7 b) => fun s => b
end.
Module LFPMB := Iter_fix MMB.
Inductive Mon_MB : ConstraintMB -> Prop :=
Mon_C7 : forall b, Mon_MB (C7 b).
Lemma F_MB_monotone : forall c, Mon_MB c -> LFPMB.monotone (F_MB c).
Proof.
destruct c; simpl; intros H s1 s2 H0.
apply MMB.Pos.order_refl.
apply MMB.Pos.eq_refl.
Qed.
Lemma collectedMB_monotones (MutRec:MMutRec.Pos.set) (Pred:MPred.Pos.set) (BC:MBC.Pos.set) : forall P c,
In c (collectMB MutRec Pred BC P) -> Mon_MB c.
Proof.
unfold collectMB; intros.
apply prop_on_collect with (P:=P) (gen:=(genMB MutRec Pred BC)).
intros.
destruct i; simpl in H1; try (inversion_clear H1; fail).
decompose [or] H1; clear H1.
rewrite <- H2; constructor.
rewrite <- H3; constructor.
rewrite <- H2; constructor.
elim H2.
auto.
Qed.
Lemma postfix_F_to_I_MB : forall c MB,
MMB.Pos.order (F_MB c MB) MB -> I_MB MB c.
Proof.
destruct c; simpl; intros; constructor; auto.
Qed.
Lemma solveMB : forall P MutRec Pred BC,
{ MB: MMB.Pos.set |
forall m pc r,
instructionAt P m pc = Some (rule2instr r) ->
ConstrMB P MutRec Pred BC MB m pc r}.
Proof.
intros.
assert (forall f : MMB.Pos.set -> MMB.Pos.set,
In f (map F_MB (collectMB MutRec Pred BC P)) -> LFPMB.monotone f).
intros.
elim (in_map_inv _ _ F_MB (collectMB MutRec Pred BC P) f); intros.
destruct H0; subst.
apply F_MB_monotone.
apply collectedMB_monotones with MutRec Pred BC P.
auto.
auto.
exists (LFPMB.lfp_list (map F_MB (collectMB MutRec Pred BC P)) H).
apply verif_all_collected_MB.
intros.
apply postfix_F_to_I_MB.
elim (LFPMB.lfp_list_is_lifp (map F_MB (collectMB MutRec Pred BC P)) H); intros.
apply H1.
apply in_map; auto.
Qed.
Record AnalyseResult : Set := result {
anc : MRec.Pos.set;
mutrec : MMutRec.Pos.set;
pred : MPred.Pos.set;
bc : MBC.Pos.set;
mb : MMB.Pos.set}.
Lemma analyse : forall P,
{ res: AnalyseResult |
mb res = false ->
exists N, forall t, valid_trace P t -> nb_new P t <= N }.
Proof.
intros P.
destruct (solveRec P) as [Rec Hrec].
destruct (solveMutRec P Rec) as [MutRec Hmutrec].
destruct (solvePred P MutRec) as [Pred Hpred].
destruct (solveBC P Rec Pred) as [BC (Hbc1,Hbc2)].
destruct (solveMB P MutRec Pred BC) as [MB Hmb].
exists (result Rec MutRec Pred BC MB).
intros.
apply (big_bound2 P Rec MutRec Pred BC); constructor; auto; intros.
replace (new_o cl) with (rule2instr (new_o1 cl)) in H0; auto.
generalize (Hmb _ _ _ H0); intros.
inversion_clear H1.
simpl in H; subst.
inversion_clear H2.
inversion_clear H3.
inversion_clear H4.
auto.
Qed.
Extract Inlined Constant physical_eq => "(fun x y -> if x==y then Left else Right)".
Extraction "../OCaml/extracted.ml" analyse.
Index
This page has been generated by coqdoc