Require syntax.
Require Lattice.
Require SumLattice.
Require func.
Require StackLattice.
Require AbVal.
Require FiniteSet.
Definition AbRef := [P:Program] (FiniteSet (max_log_ClassName P)).
Definition LatAbRef : (P:Program)(Lattice (AbRef P)) :=
[P:Program] (LatticeFiniteSet (max_log_ClassName P)).
Definition AbVal := [P:Program](lift (AbRef P)+AbNum).
Definition LatAbVal : (P:Program)(Lattice (AbVal P)) :=
[P:Program](sum_Lattice ? ? (LatAbRef P) LatAbNum).
Definition AbStack := [P:Program](stack (AbVal P)).
Definition LatAbStack : (P:Program)(Lattice (AbStack P)) :=
[P:Program](StackLattice ? (LatAbVal P)).
Definition AbLocalVar := [P:Program](funcTree (AbVal P) (max_log_Var P)).
Definition LatAbLocalVar : (P:Program)(Lattice (AbLocalVar P)) :=
[P:Program](funcTree_Lattice (AbVal P) (LatAbVal P) (max_log_Var P)).
Definition AbFuncPcStack := [P:Program](funcTree (AbStack P) (max_log_pc P)).
Definition LatAbFuncPcStack : (P:Program)(Lattice (AbFuncPcStack P)) :=
[P:Program](funcTree_Lattice (AbStack P) (LatAbStack P) (max_log_pc P)).
Definition AbFuncStack := [P:Program](funcTree (AbFuncPcStack P) (max_log_MethodName P)).
Definition LatAbFuncStack : (P:Program)(Lattice (AbFuncStack P)) :=
[P:Program](funcTree_Lattice (AbFuncPcStack P) (LatAbFuncPcStack P) (max_log_MethodName P)).
Definition AbFuncPcLocalVar := [P:Program](funcTree (AbLocalVar P) (max_log_pc P)).
Definition LatAbFuncPcLocalVar : (P:Program)(Lattice (AbFuncPcLocalVar P)) :=
[P:Program](funcTree_Lattice (AbLocalVar P) (LatAbLocalVar P) (max_log_pc P)).
Definition AbFuncLocalVar := [P:Program](funcTree (AbFuncPcLocalVar P) (max_log_MethodName P)).
Definition LatAbFuncLocalVar : (P:Program)(Lattice (AbFuncLocalVar P)) :=
[P:Program](funcTree_Lattice (AbFuncPcLocalVar P) (LatAbFuncPcLocalVar P) (max_log_MethodName P)).
Definition AbFrame := [P:Program] (AbFuncLocalVar P)*(AbFuncStack P).
Definition LatAbFrame : (P:Program)(Lattice (AbFrame P)) :=
[P:Program](prod_Lattice ? ? (LatAbFuncLocalVar P) (LatAbFuncStack P) ).
Definition AbObject := [P:Program](funcTree (AbVal P) (max_log_Field P)).
Definition LatAbObject : (P:Program)(Lattice (AbObject P)) :=
[P:Program](funcTree_Lattice (AbVal P) (LatAbVal P) (max_log_Field P)).
Definition AbHeap := [P:Program](funcTree (AbObject P) (max_log_ClassName P)).
Definition LatAbHeap : (P:Program)(Lattice (AbHeap P)) :=
[P:Program](funcTree_Lattice (AbObject P) (LatAbObject P) (max_log_ClassName P)).
Definition AbState := [P:Program] (AbHeap P)*(AbFrame P).
Definition LatAbState : (P:Program)(Lattice (AbState P)) :=
[P:Program](prod_Lattice ? ? (LatAbHeap P) (LatAbFrame P)).
Definition AbOperator : (P:Program) Operator -> (AbVal P) -> (AbVal P) -> (AbVal P) :=
[P,op]
Cases op of
| OpMult => (lift_right_binop ? ? AbMult)
| OpPlus =>(lift_right_binop ? ? AbPlus)
| OpComp =>(lift_right_binop ? ? AbComp)
| OpMinus => (lift_right_binop ? ? AbMinus)
end.
Definition AbBinop : (P:Program) Operator -> (AbStack P) -> (AbStack P) :=
[P,op,S]
let X=(AbTop (LatAbVal P) S) in
let Y=(AbTop (LatAbVal P) (AbPop S)) in
(AbPush (AbOperator P op X Y) (AbPop (AbPop S))).
Fixpoint AbPop_n [P:Program;S:(AbStack P);n:nat] : (AbStack P) :=
Cases n of
O => S
| (S p) => (AbPop (AbPop_n P S p))
end.
Fixpoint AbTop_n [P:Program;S:(AbStack P);n:nat] : (list (AbVal P)) :=
Cases n of
O => (nil ?)
| (S p) => (cons (AbTop (LatAbVal P) S) (AbTop_n P (AbPop S) p))
end.
Fixpoint subst_n_rec [P:Program;p:Var;L:(AbLocalVar P);l:(list (AbVal P))] : (AbLocalVar P) :=
Cases l of
| nil => L
| (cons v q) => (subst (LatAbVal P) (subst_n_rec P (add_un p) L q) p v)
end.
Definition subst_n : (P:Program)(list (AbVal P))->(AbLocalVar P) :=
[P,l](subst_n_rec P xH (bottom (LatAbLocalVar P)) l).
Definition betaTypeOfField : (P:Program)typeOfField->(AbVal P) :=
[P,t]Cases t of
| fieldNum => (some_sum ? (inr ? ? (const (0))))
| fieldRef => (bottom (LatAbVal P))
end.
Fixpoint AbDef_rec [P:Program;l:(list Field)] : (AbObject P) :=
Cases l of
nil => (bottom (LatAbObject P))
| (cons fi q) => (subst (LatAbVal P) (AbDef_rec P q) (nameField fi) (betaTypeOfField P (typeField fi)))
end.
Definition AbDef : (P:Program)ClassName->(AbObject P) :=
[P,cl]Cases (searchClass P cl) of
| None => (bottom (LatAbObject P))
| (Some c) => (AbDef_rec P (instanceFields c))
end.
Record Address : Set := add {
mAdd:MethodName;
pcAdd:progCount
}.
Definition applyS : (P:Program)(AbFuncStack P)->Address->(AbStack P) :=
[P,S,add]
(apply (LatAbStack P)
(apply (LatAbFuncPcStack P) S (mAdd add))
(pcAdd add)).
Coercion applyS : AbFuncStack >-> FUNCLASS.
Definition applyL : (P:Program)(AbFuncLocalVar P)->Address->(AbLocalVar P) :=
[P,L,add]
(apply (LatAbLocalVar P)
(apply (LatAbFuncPcLocalVar P) L (mAdd add))
(pcAdd add)).
Coercion applyL : AbFuncLocalVar >-> FUNCLASS.
Inductive Constraint [P:Program] : Set :=
| c2S : Address -> (AbStack P) -> (Constraint P)
| c2H : (AbHeap P) -> (Constraint P)
| S2S : Address -> Address -> ((AbStack P) -> (AbStack P)) -> (Constraint P)
| L2L : Address -> Address -> ((AbLocalVar P) -> (AbLocalVar P)) -> (Constraint P)
| SL2S : Address -> Address -> ((AbStack P) -> (AbLocalVar P) -> (AbStack P)) -> (Constraint P)
| SL2L : Address -> Address -> ((AbStack P) -> (AbLocalVar P) -> (AbLocalVar P)) -> (Constraint P)
| HS2S : Address -> Address -> ((AbHeap P) -> (AbStack P) -> (AbStack P)) -> (Constraint P)
| S2H : Address -> ((AbStack P)->(AbHeap P)) -> (Constraint P)
| S2allS : Address -> ((AbStack P) ->(AbFuncStack P)) -> (Constraint P)
| S2allL : Address -> ((AbStack P) -> (AbFuncLocalVar P)) -> (Constraint P)
| allS2S : Address -> ((AbFuncStack P) -> (AbStack P)) -> (Constraint P).
Definition validAd : (P:Program)Address->Prop :=
[P,ad]
(inf_log (mAdd ad) (max_log_MethodName P)) /\
(inf_log (pcAdd ad) (max_log_pc P)).
Definition validConstraint : (P:Program)(Constraint P)->Prop :=
[P,c]Cases c of
| (c2S add_out S0) => (validAd P add_out)
| (c2H H0) => True
| (S2S add_in add_out F) => (validAd P add_out)
| (L2L add_in add_out F) => (validAd P add_out)
| (SL2S add_in add_out F) => (validAd P add_out)
| (SL2L add_in add_out F) => (validAd P add_out)
| (HS2S add_in add_out F) => (validAd P add_out)
| (S2H add_in F) => True
| (S2allS add_in F) => True
| (S2allL add_in F) => True
| (allS2S add_out F) => (validAd P add_out)
end.
Inductive verifyContraint [P:Program] : (AbState P) -> (Constraint P) -> Prop :=
| verify_c2S : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_out:Address;S0:(AbStack P))
(order (LatAbStack P) S0 (S ad_out)) ->
(verifyContraint P (H,(L,S)) (c2S P ad_out S0))
| verify_c2H : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
H0:(AbHeap P))
(order (LatAbHeap P) H0 H) ->
(verifyContraint P (H,(L,S)) (c2H P H0))
| verify_S2S : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in,ad_out:Address;F:((AbStack P)->(AbStack P)))
(order (LatAbStack P) (F (S ad_in)) (S ad_out)) ->
(verifyContraint P (H,(L,S)) (S2S P ad_in ad_out F))
| verify_L2L : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in,ad_out:Address;F:((AbLocalVar P)->(AbLocalVar P)))
(order (LatAbLocalVar P) (F (L ad_in)) (L ad_out)) ->
(verifyContraint P (H,(L,S)) (L2L P ad_in ad_out F))
| verify_SL2S : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in,ad_out:Address;F:((AbStack P)->(AbLocalVar P)->(AbStack P)))
(order (LatAbStack P) (F (S ad_in) (L ad_in)) (S ad_out)) ->
(verifyContraint P (H,(L,S)) (SL2S P ad_in ad_out F))
| verify_SL2L : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in,ad_out:Address;F:((AbStack P)->(AbLocalVar P)->(AbLocalVar P)))
(order (LatAbLocalVar P) (F (S ad_in) (L ad_in)) (L ad_out)) ->
(verifyContraint P (H,(L,S)) (SL2L P ad_in ad_out F))
| verify_HS2S : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in,ad_out:Address;F:((AbHeap P)->(AbStack P)->(AbStack P)))
(order (LatAbStack P) (F H (S ad_in)) (S ad_out)) ->
(verifyContraint P (H,(L,S)) (HS2S P ad_in ad_out F))
| verify_S2H : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in:Address;F:((AbStack P)->(AbHeap P)))
(order (LatAbHeap P) (F (S ad_in)) H) ->
(verifyContraint P (H,(L,S)) (S2H P ad_in F))
| verify_S2allS : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in:Address;F:((AbStack P)->(AbFuncStack P)))
(order (LatAbFuncStack P) (F (S ad_in)) S) ->
(verifyContraint P (H,(L,S)) (S2allS P ad_in F))
| verify_S2allL : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_in:Address;F:((AbStack P)->(AbFuncLocalVar P)))
(order (LatAbFuncLocalVar P) (F (S ad_in)) L) ->
(verifyContraint P (H,(L,S)) (S2allL P ad_in F))
| verify_allS2S : (H:(AbHeap P);L:(AbFuncLocalVar P);S:(AbFuncStack P);
ad_out:Address;F:((AbFuncStack P)->(AbStack P)))
(order (LatAbStack P) (F S) (S ad_out)) ->
(verifyContraint P (H,(L,S)) (allS2S P ad_out F)).
Definition Flow : (P:Program) MethodName -> progCount -> Instruction -> (list (Constraint P)) :=
[P,m,pc,I]
Cases I of
| nop =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)]S)
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| (push c) =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)](AbPush (some_sum ? (inr ? ? (betaNum c))) S))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| pop =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)](AbPop S))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| (numop op) =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)](AbBinop P op S))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| (load i) =>
(cons (SL2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P);L:(AbLocalVar P)](AbPush (apply (LatAbVal P) L i) S))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| (store i) =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)](AbPop S))
(cons (SL2L P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P);L:(AbLocalVar P)](subst (LatAbVal P) L i (AbTop (LatAbVal P) S)))
(nil (Constraint P))))
| (If pc') =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)]
(lift_right_unop (LatAbStack P)
(AbIf_NZ (LatAbStack P) (AbPop S))
(AbTop (LatAbVal P) S)))
(cons (SL2L P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P);L:(AbLocalVar P)]
(lift_right_unop (LatAbLocalVar P)
(AbIf_NZ (LatAbLocalVar P) L)
(AbTop (LatAbVal P) S)))
(cons (S2S P (add m pc) (add m pc')
[S:(AbStack P)]
(lift_right_unop (LatAbStack P)
(AbIf_Z (LatAbStack P) (AbPop S))
(AbTop (LatAbVal P) S)))
(cons (SL2L P (add m pc) (add m pc')
[S:(AbStack P);L:(AbLocalVar P)]
(lift_right_unop (LatAbLocalVar P)
(AbIf_Z (LatAbLocalVar P) L)
(AbTop (LatAbVal P) S)))
(nil (Constraint P))))))
| (putfield f) =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)](AbPop (AbPop S)))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(cons (S2H P (add m pc)
[S:(AbStack P)]
let F=[cl:ClassName]
(subst (LatAbVal P) (bottom (LatAbObject P))
f (AbTop (LatAbVal P) S)) in
(lift_left_unop (LatAbHeap P)
(FiniteSet.map (LatAbObject P) F)
(AbTop (LatAbVal P) (AbPop S))))
(nil (Constraint P)))))
| (new cl) =>
(cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)](AbPush (some_sum ? (inl ? ? (singleton cl))) S))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(cons (c2H P (subst (LatAbObject P)
(bottom (LatAbHeap P))
cl (AbDef P cl)))
(nil (Constraint P)))))
| (getfield f) =>
(cons (HS2S P (add m pc) (add m (nextAddress P m pc))
[H:(AbHeap P);S:(AbStack P)]
(AbPush (lift_left_unop (LatAbVal P)
(join_on_set (LatAbVal P)
[cl](apply (LatAbVal P) (apply (LatAbObject P) H cl) f))
(AbTop (LatAbVal P) S))
(AbPop S)))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| (invokevirtual mID) =>
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(cons (S2allL P (add m pc)
[s:(AbStack P)]
(lift_left_unop (LatAbFuncLocalVar P)
(join_on_set (LatAbFuncLocalVar P)
[cl]Cases (methodLookup P mID cl) of
| None => (bottom (LatAbFuncLocalVar P))
| (Some M') => let n=(nbArguments M') in
(subst (LatAbFuncPcLocalVar P)
(bottom (LatAbFuncLocalVar P))
(nameMethod M')
(subst (LatAbLocalVar P)
(bottom (LatAbFuncPcLocalVar P))
xH
(subst_n P (cons (some_sum ? (inl ? ? (singleton cl))) (AbTop_n P (AbPop s) n)))))
end)
(AbTop (LatAbVal P) s)))
(cons (S2allS P (add m pc)
[s:(AbStack P)]
(lift_left_unop (LatAbFuncStack P)
(join_on_set (LatAbFuncStack P)
[cl]Cases (methodLookup P mID cl) of
| None => (bottom (LatAbFuncStack P))
| (Some M') =>
(subst (LatAbFuncPcStack P)
(bottom (LatAbFuncStack P))
(nameMethod M')
(subst (LatAbStack P)
(bottom (LatAbFuncPcStack P))
xH
(some ? (nil ?))))
end)
(AbTop (LatAbVal P) s)))
(cons (allS2S P (add m (nextAddress P m pc))
[SS:(AbFuncStack P)]
(lift_left_unop (LatAbStack P)
(join_on_set (LatAbStack P)
[cl]Cases (methodLookup P mID cl) of
| None => (bottom (LatAbStack P))
| (Some M') => let n=(nbArguments M') in
(AbPush (AbTop (LatAbVal P) (SS (add (nameMethod M') (END M'))))
(AbPop_n P (SS (add m pc)) (S n)))
end)
(AbTop (LatAbVal P) (SS (add m pc)))))
(nil (Constraint P))))))
| return =>
(Cases (searchMethod P m) of
| None => (nil (Constraint P))
| (Some M) => (cons (S2S P (add m pc) (add m (END M))
[S:(AbStack P)]S)
(nil (Constraint P)))
end)
| dup => (cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)] (AbPush (AbTop (LatAbVal P) S) S))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| (goto pc') =>
(cons (S2S P (add m pc) (add m pc')
[S:(AbStack P)]S)
(cons (L2L P (add m pc) (add m pc')
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| swap => (cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)]
let AbTop1 = (AbTop (LatAbVal P) S) in
let AbPop1 = (AbPop S) in
let AbTop2 = (AbTop (LatAbVal P) AbPop1) in
(AbPush AbTop2 (AbPush AbTop1 (AbPop AbPop1) )))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
| dup2 => (cons (S2S P (add m pc) (add m (nextAddress P m pc))
[S:(AbStack P)]
let AbTop1 = (AbTop (LatAbVal P) S) in
let AbPop1 = (AbPop S) in
let AbTop2 = (AbTop (LatAbVal P) AbPop1) in
(AbPush AbTop1 (AbPush AbTop2 S )))
(cons (L2L P (add m pc) (add m (nextAddress P m pc))
[L:(AbLocalVar P)]L)
(nil (Constraint P))))
end.
Definition init_flow : (P:Program) (Constraint P) :=
[P:Program]
(c2S P (add (main P) xH) (some ? (nil ?))).
Lemma valid_init_flow : (P:Program)(validConstraint P (init_flow P)).
Unfold init_flow validConstraint.
Intros; Split; Simpl.
Unfold max_log_MethodName.
Elim (hypothesis_on_main P); Intros.
Elim H; Intros.
Rewrite <- H1.
Apply in_inf_log; Auto.
Constructor.
Qed.
Definition verifyFlow : (P:Program)MethodName->progCount->Instruction->(AbState P)->Prop :=
[P,m,pc,I,St](c:(Constraint P)) (In c (Flow P m pc I)) -> (verifyContraint P St c).
Definition verifyAllFlow : (P:Program)(AbState P)->Prop :=
[P,AbS]
(verifyContraint P AbS (init_flow P)) /\
(m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some I) ->
(verifyFlow P m pc I AbS).
Lemma verifyAllFlow_hyp1 : (P:Program;AbS:(AbState P))
(verifyAllFlow P AbS) ->
(m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some I) ->
(verifyFlow P m pc I AbS).
Unfold verifyAllFlow; Intuition.
Qed.
Lemma validFlow : (P:Program;m:MethodName;pc:progCount;I:Instruction;c:(Constraint P))
(instructionAt P m pc)=(Some I) ->
(In c (Flow P m pc I)) ->
(validConstraint P c).
Intros P m pc I c H.
NewDestruct I; Simpl;
Intros H'; (Elim H'; Fail) Orelse (Decompose [or] H');
Try (Match Context With
[id:?=c|-?]->Rewrite <- id; Clear id
| [id:False|-?]->Elim id);
Try (Split;
[Apply (instructionAt_some_inf_log_MethodName ? ? ? ? H)
|Simpl; Apply (valid_nextAddress ? ? ? ? H)]).
Split.
Apply (instructionAt_some_inf_log_MethodName ? ? ? ? H).
Clear H'.
Simpl; Elim (instructionAt_some ? ? ? ? H); Intuition.
Apply inf_log_trans with (anti_convert (length (instructions x))).
Replace (anti_convert (length (instructions x))) with (END x); [Intros|Unfold END;Auto].
Unfold max_log_pc; Apply in_inf_log; Auto.
Apply (valid_if_hypothesis P x); Auto.
Split.
Apply (instructionAt_some_inf_log_MethodName ? ? ? ? H).
Clear H'.
Simpl; Elim (instructionAt_some ? ? ? ? H); Intuition.
Apply inf_log_trans with (anti_convert (length (instructions x))).
Replace (anti_convert (length (instructions x))) with (END x); [Intros|Unfold END;Auto].
Unfold max_log_pc; Apply in_inf_log; Auto.
Apply (valid_if_hypothesis P x); Auto.
Clear H'; Unfold validConstraint; Auto.
Clear H'; Unfold validConstraint; Auto.
Clear H'; Unfold validConstraint; Auto.
Clear H'; Unfold validConstraint; Auto.
Generalize H'; Clear H'.
CaseEq '(searchMethod P m); Intros.
Elim H' ; Clear H'; Intros.
Rewrite <- H1.
Split.
Simpl.
Apply (instructionAt_some_inf_log_MethodName ? ? ? ? H).
Simpl.
Unfold max_log_pc.
Apply in_inf_log.
Elim (searchMethod_some ? ? ? H0); Intros; Auto.
Elim H1.
Elim H'.
Unfold validConstraint ; Auto.
Unfold validAd ; Simpl ; Auto.
Split.
EApply instructionAt_some_inf_log_MethodName ; EAuto.
EApply valid_goto_instructionAt ; EAuto.
Unfold validConstraint ; Auto.
Unfold validAd ; Simpl ; Auto.
Split.
EApply instructionAt_some_inf_log_MethodName ; EAuto.
EApply valid_goto_instructionAt ; EAuto.
Qed.
Inductive constraint_monotone [P:Program] : (Constraint P) -> Prop :=
| monotone_c2S : (ad_out:Address;S0:(AbStack P))
(constraint_monotone P (c2S P ad_out S0))
| monotone_c2H : (H0:(AbHeap P))
(constraint_monotone P (c2H P H0))
| monotone_S2S : (ad_in,ad_out:Address;F:((AbStack P)->(AbStack P)))
((S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbStack P) (F S1) (F S2))) ->
(constraint_monotone P (S2S P ad_in ad_out F))
| monotone_L2L : (ad_in,ad_out:Address;F:((AbLocalVar P)->(AbLocalVar P)))
((L1,L2:(AbLocalVar P))
(order (LatAbLocalVar P) L1 L2) ->
(order (LatAbLocalVar P) (F L1) (F L2))) ->
(constraint_monotone P (L2L P ad_in ad_out F))
| monotone_SL2S : (ad_in,ad_out:Address;F:((AbStack P)->(AbLocalVar P)->(AbStack P)))
((L1,L2:(AbLocalVar P);S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbLocalVar P) L1 L2) ->
(order (LatAbStack P) (F S1 L1) (F S2 L2))) ->
(constraint_monotone P (SL2S P ad_in ad_out F))
| monotone_SL2L : (ad_in,ad_out:Address;F:((AbStack P)->(AbLocalVar P)->(AbLocalVar P)))
((L1,L2:(AbLocalVar P);S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbLocalVar P) L1 L2) ->
(order (LatAbLocalVar P) (F S1 L1) (F S2 L2))) ->
(constraint_monotone P (SL2L P ad_in ad_out F))
| monotone_HS2S : (ad_in,ad_out:Address;F:((AbHeap P)->(AbStack P)->(AbStack P)))
((H1,H2:(AbHeap P);S1,S2:(AbStack P))
(order (LatAbHeap P) H1 H2) ->
(order (LatAbStack P) S1 S2) ->
(order (LatAbStack P) (F H1 S1) (F H2 S2))) ->
(constraint_monotone P (HS2S P ad_in ad_out F))
| monotone_S2H : (ad_in:Address;F:((AbStack P)->(AbHeap P)))
((S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbHeap P) (F S1) (F S2))) ->
(constraint_monotone P (S2H P ad_in F))
| monotone_S2allS : (ad_in:Address;F:((AbStack P)->(AbFuncStack P)))
((S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbFuncStack P) (F S1) (F S2))) ->
(constraint_monotone P (S2allS P ad_in F))
| monotone_S2allL : (ad_in:Address;F:((AbStack P)->(AbFuncLocalVar P)))
((S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbFuncLocalVar P) (F S1) (F S2))) ->
(constraint_monotone P (S2allL P ad_in F))
| monotone_allS2S : (ad_out:Address;F:((AbFuncStack P)->(AbStack P)))
((S1,S2:(AbFuncStack P))
(order (LatAbFuncStack P) S1 S2) ->
(order (LatAbStack P) (F S1) (F S2))) ->
(constraint_monotone P (allS2S P ad_out F)).
Lemma AbBinop_monotone : (P:Program;op:Operator;s1,s2:(AbStack P))
(order (LatAbStack P) s1 s2) ->
(order (LatAbStack P) (AbBinop P op s1) (AbBinop P op s2)).
Intros P op s1 s2 H; Unfold AbBinop.
Apply (AbPush_monotone (LatAbVal P)).
Unfold AbOperator.
Case op ; Apply (lift_right_binop_keep_monotone ? ? (LatAbRef P) LatAbNum).
Intros.
Apply AbMult_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply AbPlus_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply AbComp_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply AbMinus_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply AbPop_monotone; Auto.
Qed.
Lemma subst_n_rec_monotone : (P:Program;L:(AbLocalVar P);l1,l2:(list (AbVal P));p:Var)
(order (LatAbStack P) (some ? l1) (some ? l2)) ->
(order (LatAbLocalVar P) (subst_n_rec P p L l1) (subst_n_rec P p L l2)).
NewInduction l1; Intros.
Inversion_clear H.
Auto.
Inversion_clear H.
Unfold subst_n_rec.
Apply (subst_monotone ? (LatAbVal P) (max_log_Var P)); Auto.
Qed.
Lemma subst_n_monotone : (P:Program;l1,l2:(list (AbVal P)))
(order (LatAbStack P) (some ? l1) (some ? l2)) ->
(order (LatAbLocalVar P) (subst_n P l1) (subst_n P l2)).
Unfold subst_n; Intros; Apply subst_n_rec_monotone; Auto.
Qed.
Lemma AbPop_n_monotone : (P:Program;n:nat;S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbStack P) (AbPop_n P S1 n) (AbPop_n P S2 n)).
NewInduction n; Simpl; Intros.
Auto.
Apply AbPop_monotone; Auto.
Qed.
Lemma AbTop_n_monotone : (P:Program;n:nat;S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbStack P) (some ? (AbTop_n P S1 n)) (some ? (AbTop_n P S2 n))).
NewInduction n; Intros.
Cbv Beta Iota Delta [AbTop_n]; Auto.
Unfold AbTop_n.
Constructor.
Apply AbTop_monotone; Auto.
Generalize (IHn (AbPop S1) (AbPop S2)); Unfold AbTop_n; Intros.
Apply H0.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Qed.
Lemma monotone_Flow : (P:Program;m:MethodName;pc:progCount;I:Instruction;c:(Constraint P))
(instructionAt P m pc)=(Some I) ->
(In c (Flow P m pc I)) ->
(constraint_monotone P c).
Intros P m pc I c H.
NewDestruct I; Simpl;
Intros H'; (Elim H'; Fail) Orelse (Decompose [or] H');
Try (Match Context With
[id:?=c|-?]->Rewrite <- id; Clear id
| [id:False|-?]->Elim id);
Try Constructor; Intros; Auto.
Apply (AbPush_monotone (LatAbVal P)); Auto.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Apply AbBinop_monotone; Auto.
Apply (AbPush_monotone (LatAbVal P)); Auto.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Apply (subst_monotone ? (LatAbVal P) (max_log_Var P)); Auto.
Apply AbTop_monotone; Auto.
Apply lift_right_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply AbIf_NZ_monotone; Auto.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Apply AbTop_monotone; Auto.
Apply lift_right_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply AbIf_NZ_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply lift_right_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply AbIf_Z_monotone; Auto.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Apply AbTop_monotone; Auto.
Apply lift_right_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply AbIf_Z_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply (AbPush_monotone (LatAbVal P)); Auto.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Apply (AbPop_monotone (LatAbVal P)); Auto.
Apply lift_left_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply (map_monotone (max_log_ClassName P) ? (LatAbObject P)); Intros; Auto.
Apply (subst_monotone ? (LatAbVal P) (max_log_Field P)); Auto.
Apply AbTop_monotone; Auto.
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply (AbPush_monotone (LatAbVal P)); Auto.
Apply lift_left_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply join_on_set_monotone.
Intros; Apply apply_monotone.
Apply apply_monotone.
Auto.
Auto.
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Apply lift_left_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros.
Apply join_on_set_monotone.
Intros p; CaseEq '(methodLookup P m0 p); Intros.
Apply (subst_monotone ? (LatAbFuncPcLocalVar P) (max_log_MethodName P)); Auto.
Apply (subst_monotone ? (LatAbLocalVar P) (max_log_pc P)); Auto.
Apply subst_n_monotone.
Constructor.
Constructor; Auto.
Apply (AbTop_n_monotone P (nbArguments m1) (AbPop S1) (AbPop S2)).
Apply (AbPop_monotone (LatAbVal P)); Auto.
Auto.
Auto.
Apply AbTop_monotone; Auto.
Apply lift_left_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros; Auto.
Apply join_on_set_monotone.
Intros p ; CaseEq '(methodLookup P m0 p); Intros.
Auto.
Auto.
Auto.
Apply AbTop_monotone; Auto.
Apply lift_left_unop_keep_monotone with (LatAbRef P) LatAbNum; Intros; Auto.
Apply join_on_set_monotone.
Intros p ; CaseEq '(methodLookup P m0 p); Intros.
Apply (AbPush_monotone (LatAbVal P)); Auto.
Apply AbTop_monotone; Auto.
Unfold applyS.
Apply apply_monotone.
Apply apply_monotone; Auto.
Apply AbPop_monotone.
Apply (AbPop_n_monotone P).
Unfold applyS.
Apply apply_monotone.
Apply apply_monotone; Auto.
Auto.
Auto.
Apply AbTop_monotone; Auto.
Unfold applyS.
Apply apply_monotone.
Apply apply_monotone; Auto.
Generalize H'; Clear H'.
CaseEq '(searchMethod P m); Intros.
Elim H'; Clear H'; Intros.
Rewrite <- H1; Constructor.
Intros; Auto.
Elim H1.
Elim H'.
Simpl.
Apply AbPush_monotone ; Auto.
Apply AbTop_monotone ; Auto.
Simpl.
Apply AbPush_monotone ; Auto.
Apply AbTop_monotone ; Auto.
Apply AbPop_monotone ; Auto.
Simpl.
Apply AbPush_monotone ; Auto.
Apply AbTop_monotone ; Auto.
Apply AbPop_monotone ; Auto.
Apply AbPop_monotone ; Auto.
Simpl.
Apply AbPush_monotone ; Auto.
Apply AbTop_monotone ; Auto.
Simpl.
Apply AbPush_monotone ; Auto.
Apply AbTop_monotone ; Auto.
Apply AbPop_monotone ; Auto.
Qed.