Require syntax.
Require Lattice.
Require SumLattice.
Require func.
Require StackLattice.
Require AbVal.
Require FiniteSet.
Require analysis.
Definition collect_list_instruction :
(P:Program)MethodName->(list Instruction)->progCount->(list (Constraint P)).
Intros P m l.
NewInduction l; Intros pc.
Exact (nil (Constraint P)).
Exact (app (Flow P m pc a) (IHl (add_un pc))).
Defined.
Lemma collect_list_instruction_all :
(P:Program;m:MethodName;l:(list Instruction);pc:progCount;n:nat;I:Instruction)
(nth_error l n)=(Some I) ->
(incl (Flow P m (sub_un (fast_integer.add (anti_convert n) pc)) I)
(collect_list_instruction P m l pc)).
NewInduction l; Simpl.
Destruct n; Simpl; Intros.
Discriminate H.
Discriminate H.
Destruct n; Simpl; Intros.
Injection H; Intros; Clear H; Subst.
Replace (sub_un (fast_integer.add xH pc)) with pc.
Unfold incl; Intros.
Apply in_or_app; Auto.
Rewrite add_sym.
Rewrite <- ZL12.
Rewrite sub_add_one; Auto.
Unfold incl; Intros.
Generalize (IHl (add_un pc) n0 I H a0); Intros.
Apply in_or_app.
Right; Apply H1.
Replace (fast_integer.add (anti_convert n0) (add_un pc)) with (fast_integer.add (add_un (anti_convert n0)) pc); Auto.
Rewrite add_sym.
Rewrite ZL14.
Rewrite ZL14.
Rewrite add_sym; Auto.
Qed.
Lemma collect_list_instruction_all_inv :
(P:Program;m:MethodName;l:(list Instruction);pc:progCount;c:(Constraint P))
(In c (collect_list_instruction P m l pc)) ->
(EX n:nat | (EX I:Instruction | (nth_error l n)=(Some I) /\
(In c (Flow P m (sub_un (fast_integer.add (anti_convert n) pc)) I)))).
NewInduction l; Simpl; Intros.
Elim H.
Elim (in_app_or H); Clear H; Intros.
Exists O; Exists a; Simpl ;Split; Auto.
Replace (sub_un (fast_integer.add xH pc)) with pc; Auto.
Rewrite add_sym.
Rewrite <- ZL12.
Rewrite sub_add_one; Auto.
Elim (IHl (add_un pc) c H); Intros n H1.
Elim H1; Clear H1; Intros I (H1,H2).
Exists (S n); Exists I; Simpl; Split; Auto.
Rewrite add_sym.
Rewrite ZL14.
Generalize H2.
Rewrite ZL14.
Rewrite add_sym; Auto.
Qed.
Definition collect_list_method :
(P:Program)(list Method)->(list (Constraint P)).
Intros P l.
NewInduction l.
Exact (nil (Constraint P)).
Exact (app (collect_list_instruction P (nameMethod a) (instructions a) xH)
IHl).
Defined.
Lemma collect_list_method_all :
(P:Program;m:Method;l:(list Method);pc:progCount;I:Instruction)
(In m l) -> (nth_positive (instructions m) pc)=(Some I) ->
(incl (Flow P (nameMethod m) pc I)
(collect_list_method P l)).
NewInduction l; Simpl; Intros.
Elim H.
Elim H; Clear H; Intros.
Subst.
Generalize H0; Clear H0; Unfold nth_positive; Case pc; Intros.
Generalize (collect_list_instruction_all P (nameMethod m) (instructions m) xH (convert (sub_un (xI p))) ? H0);
Unfold incl; Intros.
Apply in_or_app; Left; Apply H.
Rewrite add_sym.
Rewrite <- ZL12bis.
Rewrite sub_add_one.
Rewrite bij2.
Elim (add_sub_one (xI p)); Intros.
Discriminate H2.
Rewrite H2; Auto.
Generalize (collect_list_instruction_all P (nameMethod m) (instructions m) xH (convert (sub_un (xO p))) ? H0);
Unfold incl; Intros.
Apply in_or_app; Left; Apply H.
Rewrite add_sym.
Rewrite <- ZL12bis.
Rewrite sub_add_one.
Rewrite bij2.
Elim (add_sub_one (xO p)); Intros.
Discriminate H2.
Rewrite H2; Auto.
Generalize (collect_list_instruction_all P (nameMethod m) (instructions m) xH O ? H0);
Unfold incl; Intros.
Apply in_or_app; Left; Apply H.
Simpl; Auto.
Generalize (IHl pc I H H0); Unfold incl; Intros.
Apply in_or_app; Right; Auto.
Qed.
Lemma collect_list_method_all_inv :
(P:Program;l:(list Method);c:(Constraint P))
(In c (collect_list_method P l)) ->
(EX pc:progCount| (EX I:Instruction | (EX m:Method |
(In m l) /\ (nth_positive (instructions m) pc)=(Some I) /\
(In c (Flow P (nameMethod m) pc I) )))).
NewInduction l; Simpl; Intros.
Elim H.
Elim (in_app_or H); Clear H; Intros.
Elim (collect_list_instruction_all_inv ? ? ? ? ? H); Intros n; Intros (I,(H1,H2)).
Exists (sub_un (fast_integer.add (anti_convert n) xH)); Exists I; Exists a.
Split; Auto.
Split; Auto.
Rewrite <- ZL12.
Rewrite sub_add_one.
Unfold nth_positive.
Generalize H1; Clear H1.
Case n; Simpl; Auto.
Intros.
CaseEq '(add_un (anti_convert n0)).
Intros.
Rewrite <- H0; Clear H0.
Rewrite sub_add_one.
Rewrite bij1.
Simpl ;Auto.
Intros.
Rewrite <- H0; Clear H0.
Rewrite sub_add_one.
Rewrite bij1.
Simpl ;Auto.
Case (anti_convert n0); Simpl; Intros.
Discriminate H0.
Discriminate H0.
Discriminate H0.
Elim (IHl c H); Intros pc (I,(m,(H1,(H2,H3)))).
Exists pc; Exists I; Exists m; Split; Auto.
Qed.
Definition collect : (P:Program) (list (Constraint P)) :=
[P](cons (init_flow P)
(collect_list_method P (methods P))).
Lemma collect_all :
(P:Program;m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some I) ->
(incl (Flow P m pc I) (collect P)).
Unfold collect incl instructionAt; Intros P m pc I.
CaseEq '(searchMethod P m); Intros.
Elim (searchMethod_some ? ? ? H); Intros.
Simpl; Right.
Apply (collect_list_method_all P m0 (methods P) pc I); Auto.
Rewrite H3; Auto.
Discriminate H0.
Qed.
Lemma collect_all_inv :
(P:Program;c:(Constraint P))
(In c (collect P)) ->
c=(init_flow P) \/
(EX m:MethodName | (EX pc:progCount | (EX I:Instruction |
(instructionAt P m pc)=(Some I)/\
(In c (Flow P m pc I))))).
Unfold collect incl instructionAt; Intros P.
Intros c H; Elim H; Clear H; Intros; Auto.
Right.
Elim (collect_list_method_all_inv ? ? ? H).
Intros pc (I,(m,(H1,(H2,H3)))).
Exists (nameMethod m); Exists pc; Exists I.
Split; Auto.
Rewrite searchMethod_some_inv; Auto.
Qed.
Lemma collect_all_valid : (P:Program;c:(Constraint P))
(In c (collect P)) -> (validConstraint P c).
Intros.
Elim (collect_all_inv P c H); Intros.
Rewrite H0; Apply valid_init_flow.
Elim H0; Intros m (pc,(I,(H1,H2))).
Apply (validFlow P m pc I); Auto.
Qed.
Lemma verifyAllFlow_verify_collect : (P:Program;AbS:(AbState P))
((c:(Constraint P))
(In c (collect P))->
(verifyContraint P AbS c) ) ->
(verifyAllFlow P AbS).
Unfold verifyAllFlow; Intros; Split.
Apply H; Unfold collect; Left; Auto.
Unfold verifyFlow; Intros; Apply H.
Apply (collect_all ? ? ? ? H0); Auto.
Qed.
Lemma verify_collect_verifyAllFlow : (P:Program;AbS:(AbState P))
(verifyAllFlow P AbS) ->
((c:(Constraint P))
(In c (collect P))->
(verifyContraint P AbS c)).
Unfold verifyAllFlow; Intros.
Elim H; Clear H; Intros.
Elim (collect_all_inv ? ? H0); Intros.
Subst; Auto.
Do 4 (Elim H2; Clear H2; Intros).
Generalize (H1 ? ? ? H2); Unfold verifyFlow.
Auto.
Qed.
Definition substBotStack : (P:Program)Address->(AbStack P)->(AbState P):=
[P,add,s]
(bottom (LatAbHeap P),
(bottom (LatAbFuncLocalVar P),
(subst (LatAbFuncPcStack P)
(bottom (LatAbFuncStack P))
(mAdd add)
(subst (LatAbStack P)
(apply (LatAbFuncPcStack P) (bottom (LatAbFuncStack P)) (mAdd add))
(pcAdd add) s)))).
Definition substBotLocalVar : (P:Program)Address->(AbLocalVar P)->(AbState P):=
[P,add,l]
(bottom (LatAbHeap P),
((subst (LatAbFuncPcLocalVar P)
(bottom (LatAbFuncLocalVar P))
(mAdd add)
(subst (LatAbLocalVar P)
(apply (LatAbFuncPcLocalVar P) (bottom (LatAbFuncLocalVar P)) (mAdd add))
(pcAdd add) l)),bottom (LatAbFuncStack P))).
Definition apply_Constraint : (P:Program;c:(Constraint P);AbS:(AbState P))(AbState P) :=
[P,c]Cases c of
| (c2S add_out S0) => [AbS](substBotStack P add_out S0)
| (c2H H0) => [AbS](H0,(bottom (LatAbFrame P)))
| (S2S add_in add_out F) => [AbS]let (_,SF)=AbS in let (_,S)=SF in
(substBotStack P add_out (F (S add_in)))
| (L2L add_in add_out F) => [AbS]let (_,SF)=AbS in let (L,_)=SF in
(substBotLocalVar P add_out (F (L add_in)))
| (SL2S add_in add_out F) => [AbS]let (_,SF)=AbS in let (L,S)=SF in
(substBotStack P add_out (F (S add_in) (L add_in)))
| (SL2L add_in add_out F) => [AbS]let (_,SF)=AbS in let (L,S)=SF in
(substBotLocalVar P add_out (F (S add_in) (L add_in)))
| (HS2S add_in add_out F) => [AbS]let (H,SF)=AbS in let (_,S)=SF in
(substBotStack P add_out (F H (S add_in)))
| (S2H add_in F) => [AbS]let (_,SF)=AbS in let (_,S)=SF in
((F (S add_in)),bottom (LatAbFrame P))
| (S2allS add_in F) => [AbS]let (_,SF)=AbS in let (_,S)=SF in
(bottom (LatAbHeap P),(bottom (LatAbFuncLocalVar P),(F (S add_in))))
| (S2allL add_in F) => [AbS]let (_,SF)=AbS in let (_,S)=SF in
(bottom (LatAbHeap P),(F (S add_in),bottom (LatAbFuncStack P)))
| (allS2S add_out F) => [AbS]let (_,SF)=AbS in let (_,S)=SF in
(substBotStack P add_out (F S))
end.
Lemma apply_Constraint_order : (P:Program;c:(Constraint P);AbS:(AbState P))
(validConstraint P c) ->
(order (LatAbState P) (apply_Constraint P c AbS) AbS) ->
(verifyContraint P AbS c).
Intros P c (H,(L,S)).
Case c; Cbv Beta Iota Delta [apply_Constraint validConstraint];
Unfold substBotStack substBotLocalVar; Intros;
Elim H1; Cbv Beta Iota Delta [fst snd]; Clear H1; Intros;
Elim H2; Cbv Beta Iota Delta [fst snd]; Clear H2; Intros.
Elim H0; Clear H0; Intros.
Apply (verify_c2S P); Unfold applyL applyS.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H3); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Apply (verify_c2H P); Auto.
Apply (verify_S2S P); Unfold applyS.
Elim H0; Clear H0; Intros.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H3); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Apply (verify_L2L P); Unfold applyL.
Elim H0; Clear H0; Intros.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H2); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Apply (verify_SL2S P); Unfold applyL applyS.
Elim H0; Clear H0; Intros.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H3); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Apply (verify_SL2L P); Unfold applyL applyS.
Elim H0; Clear H0; Intros.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H2); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Apply (verify_HS2S P); Unfold applyL applyS.
Elim H0; Clear H0; Intros.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H3); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Apply (verify_S2H P); Auto.
Apply (verify_S2allS P); Auto.
Apply (verify_S2allL P); Auto.
Apply (verify_allS2S P); Unfold applyL applyS.
Elim H0; Clear H0; Intros.
Generalize (subst_order_inf ? ? ? ? ? ? ? H0 H3); Intros.
Apply (subst_order_inf ? ? ? ? ? ? ? H4 H5); Auto.
Qed.
Lemma apply_Constraint_order_inv : (P:Program;c:(Constraint P);AbS:(AbState P))
(verifyContraint P AbS c) ->
(order (LatAbState P) (apply_Constraint P c AbS) AbS).
Intros P c (H,(L,S)).
Case c; Cbv Beta Iota Delta [apply_Constraint]; Intros;
Inversion_clear H0; Unfold substBotLocalVar substBotStack;
Split; Cbv Beta Iota Delta [fst snd]; Auto;
Split; Cbv Beta Iota Delta [fst snd]; Auto;
Try (
Apply (subst_order ? (LatAbFuncPcStack P) (max_log_MethodName P)); Intros;
[Apply apply_monotone; Auto|
Apply (subst_order ? (LatAbStack P) (max_log_pc P)); Intros;
[Apply apply_monotone; Auto|Auto]]; Fail);
Try (
Apply (subst_order ? (LatAbFuncPcLocalVar P) (max_log_MethodName P)); Intros;
[Apply apply_monotone; Auto|
Apply (subst_order ? (LatAbLocalVar P) (max_log_pc P)); Intros;
[Apply apply_monotone; Auto|Auto]];Fail).
Qed.
Definition collect_func : (P:Program)(list (AbState P)->(AbState P)) :=
[P](PolyList.map (apply_Constraint P) (collect P)).
Lemma fix_apply_list_collect1 : (P:Program;AbS:(AbState P))
((f:(AbState P)->(AbState P)) (In f (collect_func P)) ->
(order (LatAbState P) (f AbS) AbS)) ->
(verifyAllFlow P AbS).
Intros.
Apply verifyAllFlow_verify_collect; Intros.
Apply apply_Constraint_order.
Apply collect_all_valid; Auto.
Unfold collect_func in H.
Apply H.
Apply PolyList.in_map; Auto.
Qed.
Lemma in_map2 : (A,B:Set)(l:(list A);f:A->B;y:B)
(In y (PolyList.map f l)) ->
(EX x:A | y=(f x) /\ (In x l)).
NewInduction l; Simpl; Intros; Intuition.
Exists a; Auto.
Elim (IHl f y H0); Intuition.
Exists x; Auto.
Qed.
Lemma fix_apply_list_collect2 : (P:Program;AbS:(AbState P))
(verifyAllFlow P AbS) ->
(f:(AbState P)->(AbState P)) (In f (collect_func P)) ->
(order (LatAbState P) (f AbS) AbS).
Unfold collect_func; Intros.
Elim (in_map2 ? ? ? ? ? H0); Intuition.
Subst.
Apply apply_Constraint_order_inv.
Apply verify_collect_verifyAllFlow; Auto.
Qed.
Definition apply_list_func :
(P:Program)(list (AbState P)->(AbState P))->(AbState P)->(AbState P) :=
[P,l,AbS]
(join_list ? (LatAbState P) (PolyList.map [f](f AbS) l)).
Definition Flow_func : (P:Program)(AbState P)->(AbState P) :=
[P](apply_list_func P (collect_func P)).
Lemma fix_apply_list_func1 : (P:Program;AbS:(AbState P))
(order (LatAbState P) (Flow_func P AbS) AbS) ->
(verifyAllFlow P AbS).
Unfold Flow_func apply_list_func; Intros.
Apply verifyAllFlow_verify_collect; Intros.
Apply apply_Constraint_order.
Apply collect_all_valid; Auto.
Apply order_trans with (join_list (AbState P) (LatAbState P)
(PolyList.map [f:((AbState P)->(AbState P))](f AbS)
(collect_func P))); Auto.
Apply join_list_greater.
Unfold collect_func.
Apply PolyList.in_map with f:=[f:((AbState P)->(AbState P))](f AbS).
Apply PolyList.in_map; Auto.
Qed.
Lemma fix_apply_list_func2 : (P:Program;AbS:(AbState P))
(verifyAllFlow P AbS) ->
(order (LatAbState P) (Flow_func P AbS) AbS).
Unfold Flow_func apply_list_func; Intros.
Apply join_list_least_greater; Intros.
Elim (in_map2 ? ? ? ? ? H0); Intuition.
Unfold collect_func in H3.
Elim (in_map2 ? ? ? ? ? H3); Intuition.
Subst.
Apply apply_Constraint_order_inv.
Apply verify_collect_verifyAllFlow; Auto.
Qed.
Lemma substBotStack_monotone : (P:Program;ad:Address;S1,S2:(AbStack P))
(order (LatAbStack P) S1 S2) ->
(order (LatAbState P) (substBotStack P ad S1) (substBotStack P ad S2)).
Unfold substBotStack; Intros.
Split; Auto.
Split; Auto.
Cbv Beta Iota Delta [fst snd].
Apply (subst_monotone ? (LatAbFuncPcStack P) (max_log_MethodName P)); Auto.
Apply (subst_monotone ? (LatAbStack P) (max_log_pc P)); Auto.
Qed.
Lemma substBotLocalVar_monotone : (P:Program;ad:Address;S1,S2:(AbLocalVar P))
(order (LatAbLocalVar P) S1 S2) ->
(order (LatAbState P) (substBotLocalVar P ad S1) (substBotLocalVar P ad S2)).
Unfold substBotLocalVar; Intros.
Split; Auto.
Split; Auto.
Cbv Beta Iota Delta [fst snd].
Apply (subst_monotone ? (LatAbFuncPcLocalVar P) (max_log_MethodName P)); Auto.
Apply (subst_monotone ? (LatAbLocalVar P) (max_log_pc P)); Auto.
Qed.
Lemma constraint_monotone_prop : (P:Program;c:(Constraint P))
(constraint_monotone P c) ->
(AbS1,AbS2:(AbState P))
(order (LatAbState P) AbS1 AbS2) ->
(order (LatAbState P) (apply_Constraint P c AbS1)
(apply_Constraint P c AbS2)).
Destruct AbS1; Intros H1 SF1.
Destruct AbS2; Intros H2 SF2.
Case SF1; Intros L1 S1.
Case SF2; Intros L2 S2; Intros.
Elim H0; Cbv Beta Iota Delta [fst snd].
Clear H0; Intros.
Elim H3; Cbv Beta Iota Delta [fst snd].
Clear H3; Intros.
Inversion_clear H; Unfold apply_Constraint.
Auto.
Auto.
Apply substBotStack_monotone; Apply H5.
Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Apply substBotLocalVar_monotone; Apply H5.
Unfold applyL; Do 2 Apply apply_monotone; Assumption.
Apply substBotStack_monotone; Apply H5.
Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Unfold applyL; Do 2 Apply apply_monotone; Assumption.
Apply substBotLocalVar_monotone; Apply H5.
Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Unfold applyL; Do 2 Apply apply_monotone; Assumption.
Apply substBotStack_monotone; Apply H5.
Assumption.
Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Split; Cbv Beta Iota Delta [fst snd].
Apply H5; Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Auto.
Split; Cbv Beta Iota Delta [fst snd].
Apply bottom_is_a_bottom.
Split; Cbv Beta Iota Delta [fst snd].
Apply bottom_is_a_bottom.
Apply H5; Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Split; Cbv Beta Iota Delta [fst snd].
Apply bottom_is_a_bottom.
Split; Cbv Beta Iota Delta [fst snd].
Apply H5; Unfold applyS; Do 2 Apply apply_monotone; Assumption.
Apply bottom_is_a_bottom.
Apply substBotStack_monotone; Apply H5.
Auto.
Qed.
Lemma collect_monotone : (P:Program;c:(Constraint P))
(In c (collect P)) -> (constraint_monotone P c).
Intros.
Elim (collect_all_inv ? ? H); Intros.
Subst; Unfold init_flow; Constructor.
Do 4 (Elim H0; Clear H0; Intros).
Apply monotone_Flow with x x0 x1; Auto.
Qed.
Lemma app_map : (A,B:Set;f:A->B;l1,l2:(list A))
(app (PolyList.map f l1) (PolyList.map f l2))=(PolyList.map f (app l1 l2)).
NewInduction l1; Simpl; Auto.
Intros.
Rewrite IHl1; Auto.
Qed.
Lemma rev_map : (A,B:Set;f:A->B;l:(list A))
(rev (PolyList.map f l))=(PolyList.map f (rev l)).
NewInduction l; Simpl; Auto.
Rewrite IHl.
Generalize (app_map ? ? f (rev l) (cons a (nil A))); Simpl; Intros.
Rewrite H; Auto.
Qed.
Lemma collect_func_monotone : (P:Program)(f:(AbState P)->(AbState P))
(In f (rev (collect_func P))) ->
(AbS1,AbS2:(AbState P))
(order (LatAbState P) AbS1 AbS2) ->
(order (LatAbState P) (f AbS1) (f AbS2)).
Unfold collect_func; Intros.
Generalize (in_rev ? (rev (PolyList.map (apply_Constraint P) (collect P)))).
Rewrite idempot_rev.
Intros.
Generalize (H1 ? H); Intros.
Elim (in_map2 ? ? ? ? ? H2); Intros.
Decompose [and] H3; Clear H3.
Subst.
Apply constraint_monotone_prop; Auto.
Apply collect_monotone; Auto.
Qed.
Lemma Flow_func_monotone : (P:Program;AbS1,AbS2:(AbState P))
(order (LatAbState P) AbS1 AbS2) ->
(order (LatAbState P) (Flow_func P AbS1) (Flow_func P AbS2)).
Unfold Flow_func apply_list_func; Intros.
Apply join_list_least_greater; Intros.
Elim (in_map2 ? ? ? ? ? H0); Intros.
Decompose [and] H1; Clear H1.
Unfold collect_func in H3.
Elim (in_map2 ? ? ? ? ? H3); Intros.
Decompose [and] H1; Clear H1.
Subst.
Apply order_trans with (apply_Constraint P x1 AbS2).
Apply constraint_monotone_prop; Auto.
Apply collect_monotone; Auto.
Apply join_list_greater.
Apply in_map with f:=([f:((AbState P)->(AbState P))](f AbS2)).
Unfold collect_func; Auto.
Qed.
Definition analyzer : (P:Program)(AbState P) :=
[P](lfp (AbState P) (LatAbState P) (Flow_func P) (Flow_func_monotone P)).
Definition analyzer_list : (P:Program)(AbState P) :=
[P](lfp_list (AbState P) (LatAbState P)
(collect_func P)
(collect_func_monotone P)).