Require syntax.
Require Lattice.
Require SumLattice.
Require func.
Require StackLattice.
Require AbVal.
Require FiniteSet.
Require semantic.
Require analysis.
Require Omega.
Definition betaRef : (P:Program) Heap->ReferenceValue->(AbRef P) :=
[P,H,loc]
Cases (H loc) of
| None => (bottom (LatAbRef P))
| (Some o) => (singleton (class o))
end.
Definition R_Ref : (P:Program) Heap -> ReferenceValue -> (AbRef P) -> Prop :=
[P,H,r,R](order (LatAbRef P) (betaRef P H r) R).
Definition R_Ref_monotonicity : (P:Program;H:Heap;r:ReferenceValue;R1,R2:(AbRef P))
(R_Ref P H r R1) -> (order (LatAbRef P) R1 R2) -> (R_Ref P H r R2).
Unfold R_Ref; Intros; EAuto.
Qed.
Definition betaVal : (P:Program) Heap -> Value -> (AbVal P) :=
[P,H,v]Cases v of
| (num n) => (some_sum ? (inr ? ? (betaNum n)))
| (ref r) => (some_sum ? (inl ? ? (betaRef P H r)))
| nul => (bottom (LatAbVal P))
end.
Definition R_Val : (P:Program) Heap -> Value -> (AbVal P) -> Prop :=
[P,H,v,V](order (LatAbVal P) (betaVal P H v) V).
Definition R_Val_monotonicity : (P:Program;H:Heap;v:Value;V1,V2:(AbVal P))
(R_Val P H v V1) -> (order (LatAbVal P) V1 V2) -> (R_Val P H v V2).
Unfold R_Val; Intros; EAuto.
Qed.
Lemma betaVal_subst:
(P: Program ; h : Heap ; v,v' : Value ; loc : Location ; o : ClassInst ; f : FieldName)
(h loc)=(Some o) ->
(betaVal P h v')=(betaVal P (substHeap h loc (substField o f v)) v').
Intros.
Unfold betaVal betaRef.
CaseEq v'.
Intros.
Trivial.
Intros.
Case (Location_dec loc r).
Intros ; Subst.
Rewrite H.
Unfold substHeap ; Case Location_dec ; Intros.
Unfold substField; Simpl.
Trivial.
Elim n ; Auto.
Intros.
Unfold substHeap ; Case Location_dec ; Intros.
Elim n ; Auto.
Auto.
Auto.
Qed.
Lemma R_Val_subst : (P: Program ; h : Heap ; v : Value ; A : (AbVal P) ; loc : Location ;
o : ClassInst ; f : FieldName)
(h loc) = (Some o) ->
(R_Val P h v A) ->
(R_Val P (substHeap h loc (substField o f v)) v A).
Unfold R_Val ; Intros.
Rewrite <-betaVal_subst ; Auto.
Qed.
Definition betaStack : (P:Program) Heap -> OperandStack -> (AbStack P) :=
[P,H,s]
(some ? (PolyList.map (betaVal P H) s)).
Definition R_Stack : (P:Program) Heap -> OperandStack -> (AbStack P) -> Prop :=
[P,H,s,S](order (LatAbStack P) (betaStack P H s) S).
Definition R_Stack_monotonicity : (P:Program;H:Heap;s:OperandStack;S1,S2:(AbStack P))
(R_Stack P H s S1) -> (order (LatAbStack P) S1 S2) -> (R_Stack P H s S2).
Unfold R_Stack; Intros; EAuto.
Qed.
Lemma R_Stack_subst : (P: Program ; h : Heap ; v : Value ; s : OperandStack ; S : (AbStack P) ; loc : Location ;
o : ClassInst ; f : FieldName)
(h loc) = (Some o) ->
(R_Stack P h s S) ->
(R_Stack P (substHeap h loc (substField o f v)) s S).
NewInduction s.
Intros ; Auto.
Intros.
Inversion H0.
Constructor.
Unfold R_Stack.
Simpl.
Unfold betaStack.
Simpl.
Constructor.
Rewrite <-betaVal_subst ; Auto.
Unfold R_Stack betaStack in IHs.
Simpl in IHs.
Apply IHs ; Auto.
Qed.
Lemma R_Stack_AbPush :
(P:Program;H:Heap;v:Value;s:OperandStack;V:(AbVal P);S:(AbStack P))
(R_Val P H v V) -> (R_Stack P H s S) ->
(R_Stack P H v::s (AbPush V S)).
Unfold R_Val R_Stack AbPush betaStack; Simpl; Intros P H v s V S.
Case s; Simpl; Intros.
Inversion_clear H1.
Constructor.
Simpl; Constructor; Auto.
Constructor.
Inversion_clear H1.
Constructor.
Constructor; Auto.
Constructor; Auto.
Qed.
Lemma R_Stack_AbPop :
(P:Program;H:Heap;v:Value;s:OperandStack;S:(AbStack P))
(R_Stack P H v::s S) ->
(R_Stack P H s (AbPop S)).
Unfold R_Stack AbPop LatAbStack betaStack; Simpl; Intros.
Inversion_clear H0; Try Constructor; Auto.
Qed.
Lemma R_Stack_AbBinop :
(P:Program;H:Heap;op:Operator;n1,n2:integer;s:OperandStack;S:(AbStack P))
(R_Stack P H (num n1)::(num n2)::s S) ->
(R_Stack P H (num (sem_binop op n1 n2))::s (AbBinop P op S)).
Intros.
Case op.
Unfold R_Stack in H0.
Unfold sem_binop AbBinop.
Unfold R_Stack betaStack.
Generalize (AbPush_monotone (LatAbVal P)
(some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum (mult n1 n2))))
(AbOperator P OpMult (AbTop (LatAbVal P) S) (AbTop (LatAbVal P) (AbPop S)))
(some ?(PolyList.map (betaVal P H) s) )).
Intros.
Apply H1.
Unfold AbOperator.
Apply order_trans with
(lift_right_binop (AbRef P) AbNum AbMult
(some_sum ? (inr (AbRef P) AbNum (betaNum n1)))
(some_sum ? (inr (AbRef P) AbNum (betaNum n2)))).
Cbv Beta Iota Delta [lift_right_binop]; Constructor; Apply AbMult_correct.
Apply (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum).
Intros; Apply AbMult_monotone; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n1)))
with (AbTop (LatAbVal P) (betaStack P H (num n1)::(num n2)::s)).
Apply AbTop_monotone; Auto.
Simpl; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n2)))
with (AbTop (LatAbVal P) (AbPop (betaStack P H (num n1)::(num n2)::s))).
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Simpl; Auto.
Replace (some (AbVal P) (PolyList.map (betaVal P H) s))
with (AbPop (AbPop (betaStack P H (num n1)::(num n2)::s))); Auto.
Apply AbPop_monotone.
Apply AbPop_monotone; Auto.
Unfold R_Stack in H0.
Unfold sem_binop AbBinop.
Unfold R_Stack betaStack.
Generalize (AbPush_monotone (LatAbVal P)
(some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum (plus n1 n2))))
(AbOperator P OpPlus (AbTop (LatAbVal P) S) (AbTop (LatAbVal P) (AbPop S)))
(some ?(PolyList.map (betaVal P H) s) )).
Intros.
Apply H1.
Unfold AbOperator.
Apply order_trans with
(lift_right_binop (AbRef P) AbNum AbPlus
(some_sum ? (inr (AbRef P) AbNum (betaNum n1)))
(some_sum ? (inr (AbRef P) AbNum (betaNum n2)))).
Cbv Beta Iota Delta [lift_right_binop]; Constructor; Apply AbPlus_correct.
Generalize (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum);
Intros.
Apply (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum).
Intros; Apply AbPlus_monotone; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n1)))
with (AbTop (LatAbVal P) (betaStack P H (num n1)::(num n2)::s)).
Apply AbTop_monotone; Auto.
Simpl; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n2)))
with (AbTop (LatAbVal P) (AbPop (betaStack P H (num n1)::(num n2)::s))).
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Simpl; Auto.
Replace (some (AbVal P) (PolyList.map (betaVal P H) s))
with (AbPop (AbPop (betaStack P H (num n1)::(num n2)::s))); Auto.
Apply AbPop_monotone.
Apply AbPop_monotone; Auto.
Unfold R_Stack in H0.
Unfold sem_binop AbBinop.
Unfold R_Stack betaStack.
Generalize (AbPush_monotone (LatAbVal P)
(some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum (comp n1 n2))))
(AbOperator P OpComp (AbTop (LatAbVal P) S) (AbTop (LatAbVal P) (AbPop S)))
(some ?(PolyList.map (betaVal P H) s) )).
Intros.
Apply H1.
Unfold AbOperator.
Apply order_trans with
(lift_right_binop (AbRef P) AbNum AbComp
(some_sum ? (inr (AbRef P) AbNum (betaNum n1)))
(some_sum ? (inr (AbRef P) AbNum (betaNum n2)))).
Cbv Beta Iota Delta [lift_right_binop]; Constructor; Apply AbComp_correct.
Generalize (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum);
Intros.
Apply (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum).
Intros; Apply AbComp_monotone; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n1)))
with (AbTop (LatAbVal P) (betaStack P H (num n1)::(num n2)::s)).
Apply AbTop_monotone; Auto.
Simpl; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n2)))
with (AbTop (LatAbVal P) (AbPop (betaStack P H (num n1)::(num n2)::s))).
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Simpl; Auto.
Replace (some (AbVal P) (PolyList.map (betaVal P H) s))
with (AbPop (AbPop (betaStack P H (num n1)::(num n2)::s))); Auto.
Apply AbPop_monotone.
Apply AbPop_monotone; Auto.
Unfold R_Stack in H0.
Unfold sem_binop AbBinop.
Unfold R_Stack betaStack.
Generalize (AbPush_monotone (LatAbVal P)
(some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum (minus n1 n2))))
(AbOperator P OpMinus (AbTop (LatAbVal P) S) (AbTop (LatAbVal P) (AbPop S)))
(some ?(PolyList.map (betaVal P H) s) )).
Intros.
Apply H1.
Unfold AbOperator.
Apply order_trans with
(lift_right_binop (AbRef P) AbNum AbMinus
(some_sum ? (inr (AbRef P) AbNum (betaNum n1)))
(some_sum ? (inr (AbRef P) AbNum (betaNum n2)))).
Cbv Beta Iota Delta [lift_right_binop]; Constructor; Apply AbMinus_correct.
Generalize (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum);
Intros.
Apply (lift_right_binop_keep_monotone (AbRef P) AbNum (LatAbRef P) LatAbNum).
Intros; Apply AbMinus_monotone; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n1)))
with (AbTop (LatAbVal P) (betaStack P H (num n1)::(num n2)::s)).
Apply AbTop_monotone; Auto.
Simpl; Auto.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n2)))
with (AbTop (LatAbVal P) (AbPop (betaStack P H (num n1)::(num n2)::s))).
Apply AbTop_monotone; Auto.
Apply AbPop_monotone; Auto.
Simpl; Auto.
Replace (some (AbVal P) (PolyList.map (betaVal P H) s))
with (AbPop (AbPop (betaStack P H (num n1)::(num n2)::s))); Auto.
Apply AbPop_monotone.
Apply AbPop_monotone; Auto.
Qed.
Lemma R_Stack_AbTop :
(P:Program;H:Heap;v:Value;s:OperandStack;S:(AbStack P))
(R_Stack P H v::s S) ->
(R_Val P H v (AbTop (LatAbVal P) S)).
Unfold R_Stack R_Val; Intros.
Replace (betaVal P H v) with (AbTop (LatAbVal P) (betaStack P H v::s)); Auto.
Apply AbTop_monotone; Auto.
Qed.
Definition R_LocalVar :
(P:Program) Heap -> LocalVar -> (AbLocalVar P) -> Prop :=
[P,H,l,L]
(x:Var)
(R_Val P H (l x) (apply (LatAbVal P) L x)).
Lemma R_LocalVar_monotonicity : (P:Program;H:Heap;l:LocalVar;L1,L2:(AbLocalVar P))
(R_LocalVar P H l L1) -> (order (LatAbLocalVar P) L1 L2) ->
(R_LocalVar P H l L2).
Unfold R_LocalVar R_Val; Intros.
Apply order_trans with (apply (LatAbVal P) L1 x); Auto.
Qed.
Lemma R_LocalVar_subst : (P: Program ; h : Heap ; v : Value ; l : LocalVar ; L : (AbLocalVar P) ; loc : Location ;
o : ClassInst ; f : FieldName)
(h loc) = (Some o) ->
(R_LocalVar P h l L) ->
(R_LocalVar P (substHeap h loc (substField o f v)) l L).
Intros.
Unfold R_LocalVar.
Unfold R_LocalVar in H0.
Intros.
Generalize (H0 x) ; Clear H0 ; Intros H0.
Unfold R_Val ; Unfold R_Val in H0.
Rewrite <-betaVal_subst ; Auto.
Qed.
Definition R_Object : (P:Program)Heap->ClassInst->(AbObject P) -> Prop :=
[P,H,c,O]
(f:FieldName)
(R_Val P H (fieldValue c f) (apply (LatAbVal P) O f)).
Lemma R_Object_monotonicity : (P:Program;H:Heap;c:ClassInst;O1,O2:(AbObject P))
(R_Object P H c O1) -> (order (LatAbObject P) O1 O2) ->
(R_Object P H c O2).
Unfold R_Object R_Val; Intros.
Apply order_trans with (apply (LatAbVal P) O1 f); Auto.
Qed.
Lemma betaTypeOfField_correct : (P:Program;H:Heap;t:typeOfField)
(R_Val P H (initField t) (betaTypeOfField P t)).
Destruct t; Unfold initField betaTypeOfField R_Val betaVal betaNum; Auto.
Qed.
Lemma AbDef_rec_correct : (P:Program;H:Heap;c:Class;l:(list Field);f:FieldName)
(In c (classes P)) ->
(incl l (instanceFields c)) ->
(R_Val P H
Cases (searchField_rec l f) of
(Some fi) => (initField (typeField fi))
| None => null
end (apply (LatAbVal P) (AbDef_rec P l) f)).
NewInduction l; Intros.
Opaque LatAbObject.
Simpl.
Unfold R_Val.
Opaque LatAbVal.
Simpl.
Auto.
Simpl.
Case positive_dec; Intros.
Subst; Rewrite apply_subst1; Auto.
Apply betaTypeOfField_correct; Auto.
Apply valid_instanceField with c; Auto.
Apply H1; Auto with datatypes.
Rewrite apply_subst2; Auto.
Apply IHl; Auto.
Unfold incl; Intros.
Unfold incl in H1.
Apply H1; Auto with datatypes.
Apply valid_instanceField with c; Auto.
Apply H1; Auto with datatypes.
Qed.
Lemma AbDef_correct : (P:Program;H:Heap;c:Class;cl:ClassName)
(searchClass P cl)=(Some c) ->
(R_Object P H (def c) (AbDef P cl)).
Intros.
Unfold R_Object; Intros.
Unfold def AbDef searchField.
Cbv Beta Iota Delta [fieldValue].
Rewrite H0.
Apply AbDef_rec_correct with c; Auto.
Elim (searchClass_some P cl c); Intros; Auto.
Apply incl_refl.
Qed.
Definition R_Heap : (P:Program)Heap->(AbHeap P)->Prop :=
[P,h,H]
(loc:Location)
Cases (h loc) of
| None => True
| (Some c) => (R_Object P h c (apply (LatAbObject P) H (class c)))
end.
Lemma R_Heap_monotonicity : (P:Program;h:Heap;H1,H2:(AbHeap P))
(R_Heap P h H1) -> (order (LatAbHeap P) H1 H2) -> (R_Heap P h H2).
Unfold R_Heap; Intros.
Generalize (H loc); Case (h loc); Intros; Auto.
Apply R_Object_monotonicity with (apply (LatAbObject P) H1 (class c)).
Trivial.
Apply apply_monotone; Auto.
Qed.
Inductive R_PopCallStack [P:Program;h:Heap] : CallStack->(AbFrame P)->Prop:=
| R_PopCallStack_0 : (F:(AbFrame P))(R_PopCallStack P h (nil ?) F)
| R_PopCallStack_1 : (f:Frame;F:(AbFrame P))
(R_PopCallStack P h (cons f (nil ?)) F)
| R_PopCallStack_2 : (m,m':MethodName;pc,pc':progCount;l,l':LocalVar;s,s':OperandStack;
sf:CallStack;L:(AbFuncLocalVar P);AbS:(AbFuncStack P);M':Method)
(R_LocalVar P h l (L (add m pc))) ->
(searchMethod P m')=(Some M') ->
(R_Stack P h s (AbPop_n P (AbS (add m pc)) (S (nbArguments M')))) ->
(R_PopCallStack P h (cons (frame m pc l s) sf) (L,AbS)) ->
(R_PopCallStack P h (cons (frame m' pc' l' s') (cons (frame m pc l s) sf)) (L,AbS)).
Lemma AbPop_n_monotonicity : (P:Program;S1,S2:(AbStack P);n:nat)
(order (LatAbStack P) S1 S2) ->
(order (LatAbStack P) (AbPop_n P S1 n) (AbPop_n P S2 n)).
NewInduction n; Intros.
Cbv Beta Iota Delta [AbPop_n].
Auto.
Cbv Beta Iota Delta [AbPop_n].
Apply (AbPop_monotone (LatAbVal P)).
Auto.
Qed.
Lemma R_PopCallStack_monotonicity : (P:Program;h:Heap;sf:CallStack;F1,F2:(AbFrame P))
(R_PopCallStack P h sf F1) -> (order (LatAbFrame P) F1 F2) ->
(R_PopCallStack P h sf F2).
Intros P h sf F1 F2 H; NewInduction H; Intros.
Constructor.
Constructor.
CaseEq F2; Intros; Subst.
Constructor 3 with M'; Auto.
Apply R_LocalVar_monotonicity with (L (add m pc)).
Trivial.
Inversion_clear H3.
Unfold applyL.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Apply R_Stack_monotonicity with (AbPop_n P (AbS (add m pc)) (S (nbArguments M'))).
Trivial.
Apply AbPop_n_monotonicity.
Inversion_clear H3.
Unfold applyS.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Qed.
Inductive R_CallStack [P:Program;h:Heap] : CallStack->(AbFrame P)->Prop:=
| R_CallStack_nil : (F:(AbFrame P))(R_CallStack P h (nil ?) F)
| R_CallStack_cons : (m:MethodName;pc:progCount;l:LocalVar;s:OperandStack;
sf:CallStack;L:(AbFuncLocalVar P);S:(AbFuncStack P))
(R_LocalVar P h l (L (add m pc))) ->
(R_Stack P h s (S (add m pc))) ->
(R_PopCallStack P h (cons (frame m pc l s) sf) (L,S)) ->
(R_CallStack P h (cons (frame m pc l s) sf) (L,S)).
Lemma R_CallStack_monotonicity : (P:Program;h:Heap;sf:CallStack;F1,F2:(AbFrame P))
(R_CallStack P h sf F1) -> (order (LatAbFrame P) F1 F2) ->
(R_CallStack P h sf F2).
Intros.
Generalize H0; Clear H0; Inversion_clear H; Intros.
Constructor.
CaseEq F2; Intros; Subst.
Inversion_clear H3.
Constructor.
Apply R_LocalVar_monotonicity with (L (add m pc)); Auto.
Unfold applyL.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Apply R_Stack_monotonicity with (S (add m pc)); Auto.
Unfold applyS.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Apply R_PopCallStack_monotonicity with (L,S); Auto.
Constructor; Auto.
Qed.
Lemma R_PopCallStack_subst : (P: Program ; h : Heap ; v : Value ; c : CallStack ;
C : (AbFrame P) ; loc : Location ; o : ClassInst ; f : FieldName)
(h loc) = (Some o) ->
(R_PopCallStack P h c C) ->
(R_PopCallStack P (substHeap h loc (substField o f v)) c C).
Intros.
Generalize H; Clear H.
NewInduction H0; Intros.
Constructor.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Apply R_LocalVar_subst ; Auto.
Apply R_Stack_subst ; Auto.
Qed.
Definition R_State : (P:Program)State->(AbState P)->Prop :=
[P,st,St] let (h,sf)=st in
let (H,SF)=St in
(R_Heap P h H) /\ (R_CallStack P h sf SF).
Lemma R_State_monotonicity : (P:Program;st:State;St1,St2:(AbState P))
(R_State P st St1) -> (order (LatAbState P) St1 St2) -> (R_State P st St2).
Destruct st; Destruct St1; Destruct St2;
Unfold R_State; Intros.
Intuition.
Apply R_Heap_monotonicity with a; Auto.
Inversion H0; Auto.
Apply R_CallStack_monotonicity with a0; Auto.
Inversion H0; Auto.
Qed.
Lemma verifyAllFlow_hyp2 : (P:Program;AbS:(AbState P);st:State)
(verifyAllFlow P AbS)->
(initial_State P st) -> (R_State P st AbS).
Intros.
Elim H; Clear H; Intros H _.
Unfold init_flow in H; Inversion_clear H.
Inversion_clear H0.
Constructor.
Unfold R_Heap; Auto.
Constructor; Auto.
Unfold R_LocalVar R_Val betaVal; Intros.
Rewrite H; Auto.
Constructor.
Qed.