Require ResultList.
Require Export TabTree.
Require Export Arith.
Require Export PolyList.
Require Max.
Require Omega.
Definition integer := nat.
Definition Var := positive.
Definition progCount := positive.
Definition Var_dec := positive_dec.
Definition ClassName := positive.
Definition FieldName := positive.
Definition Field_dec := positive_dec.
Definition MethodID := positive.
Definition MethodName := positive.
Definition MethodName_dec := positive_dec.
Inductive Operator : Set :=
| OpMult : Operator
| OpPlus : Operator
| OpComp : Operator
| OpMinus : Operator.
Inductive Instruction : Set :=
| nop : Instruction
| push : integer -> Instruction
| pop : Instruction
| numop : Operator -> Instruction
| load : Var -> Instruction
| store : Var -> Instruction
| If : progCount -> Instruction
| new : ClassName -> Instruction
| putfield : FieldName -> Instruction
| getfield : FieldName -> Instruction
| invokevirtual : MethodID -> Instruction
| return : Instruction
| dup : Instruction
| goto : progCount -> Instruction
| swap : Instruction
| dup2 : Instruction.
Inductive typeOfField : Set :=
| fieldNum : typeOfField
| fieldRef : typeOfField.
Record Field : Set := Field_constr {
nameField : FieldName;
typeField : typeOfField
}.
Record Method : Set := Method_constr {
nameMethod : MethodName;
instructions : (list Instruction);
nbArguments : nat
}.
Inductive allNameMethodsDistincts : (list Method)->Prop :=
| allNameMethodsDistincts1 : (allNameMethodsDistincts (nil ?))
| allNameMethodsDistincts2 : (m:Method;l:(list Method))
~(EX m':Method | (In m' l)/\(nameMethod m)=(nameMethod m')) ->
(allNameMethodsDistincts l) ->
(allNameMethodsDistincts (cons m l)).
Record Class : Set := Class_constr {
nameClass : ClassName;
list_methods_lookup : (list (MethodID*MethodName));
instanceFields : (list Field)
}.
Record Program : Set := Program_constr {
classes : (list Class);
methods : (list Method);
methodsValid : (allNameMethodsDistincts methods);
main : MethodName;
hypothesis_on_main : (EX M:Method | (In M methods)/\(nameMethod M)=main);
valid_if_hypothesis : (m:Method;pc:progCount)
(In m methods) ->
(In (If pc) (instructions m)) ->
(compare pc (anti_convert (length (instructions m))) EGAL)=INFERIEUR;
valid_goto_hypothesis : (m:Method;pc:progCount)
(In m methods) ->
(In (goto pc) (instructions m)) ->
(compare pc (anti_convert (length (instructions m))) EGAL)=INFERIEUR;
no_return_in_main_hypothesis :
(m:Method)(nameMethod m)=main -> ~(In return (instructions m))
}.
Definition append_instructions :=
[P:Program](append_list (map instructions (methods P))).
Lemma append_instructions_correct :
(P:Program;m:Method;i:Instruction)
(In m (methods P)) ->
(In i (instructions m)) -> (In i (append_instructions P)).
Intros; Unfold append_instructions.
Generalize (in_append_list ? (instructions m)); Intros.
Apply H1; Auto.
Apply in_map; Auto.
Qed.
Definition max_log_ClassName := [P:Program]
(max_log_list ? nameClass (classes P)).
Definition max_log_MethodName := [P:Program]
(max_log_list ? nameMethod (methods P)).
Definition extract_Var :=
[i:Instruction]Cases i of
(load x) => x
| (store x) => x
| _ => xH
end.
Definition max_log_Var := [P:Program]
(max (max_log_list ? extract_Var (append_instructions P))
(max_log_list ? [m](anti_convert (S (nbArguments m))) (methods P))).
Lemma valid_nbArguments :
(P:Program;m:Method)
(In m (methods P)) ->
(inf_log (anti_convert (S (nbArguments m))) (max_log_Var P)).
Intros; Unfold max_log_Var.
Apply inf_log_trans' with (max_log_list Method [m0:Method](anti_convert (S (nbArguments m0)))
(methods P)).
Apply in_inf_log with f:=[m0:Method](anti_convert (S (nbArguments m0))); Auto.
Apply le_max_r.
Qed.
Definition append_fields :=
[P:Program](map nameField (append_list (map instanceFields (classes P)))).
Lemma append_fields_correct :
(P:Program;c:Class;f:Field)
(In c (classes P)) ->
(In f (instanceFields c)) -> (In (nameField f) (append_fields P)).
Intros; Unfold append_fields.
Generalize (in_append_list ? (instanceFields c)); Intros.
Apply in_map.
Apply H1; Auto.
Apply in_map; Auto.
Qed.
Definition extract_Field :=
[i:Instruction]Cases i of
(putfield x) => x
| (getfield x) => x
| _ => xH
end.
Definition max_log_Field := [P:Program]
(max (max_log_list ? extract_Field (append_instructions P))
(max_log_list ? [x]x (append_fields P))).
Lemma valid_instanceField : (P:Program;c:Class;f:Field)
(In c (classes P)) -> (In f (instanceFields c)) ->
(inf_log (nameField f) (max_log_Field P)).
Intros; Unfold max_log_Field.
Apply inf_log_trans' with (max_log_list positive [x:positive]x (append_fields P)).
Apply in_inf_log with f:=[x:FieldName]x.
Apply append_fields_correct with c; Auto.
Apply le_max_r.
Qed.
Lemma valid_putfield :
(P:Program;m:Method;f:FieldName)
(In m (methods P)) ->
(In (putfield f) (instructions m)) -> (inf_log f (max_log_Field P)).
Intros.
Replace f with (extract_Field (putfield f)).
Unfold max_log_Field.
Apply inf_log_trans' with (max_log_list Instruction extract_Field (append_instructions P)).
Intros; Apply in_inf_log.
Apply (append_instructions_correct P m); Auto.
Apply le_max_l.
Auto.
Qed.
Lemma valid_getfield :
(P:Program;m:Method;f:FieldName)
(In m (methods P)) ->
(In (getfield f) (instructions m)) -> (inf_log f (max_log_Field P)).
Intros.
Replace f with (extract_Field (getfield f)).
Unfold max_log_Field.
Apply inf_log_trans' with (max_log_list Instruction extract_Field (append_instructions P)).
Intros; Apply in_inf_log.
Apply (append_instructions_correct P m); Auto.
Apply le_max_l.
Auto.
Qed.
Lemma valid_load :
(P:Program;m:Method;x:Var)
(In m (methods P)) ->
(In (load x) (instructions m)) -> (inf_log x (max_log_Var P)).
Intros.
Replace x with (extract_Var (load x)).
Unfold max_log_Var.
Apply inf_log_trans' with (max_log_list Instruction extract_Var (append_instructions P)).
Intros; Apply in_inf_log.
Apply (append_instructions_correct P m); Auto.
Apply le_max_l.
Auto.
Qed.
Lemma valid_store :
(P:Program;m:Method;x:Var)
(In m (methods P)) ->
(In (store x) (instructions m)) -> (inf_log x (max_log_Var P)).
Intros.
Replace x with (extract_Var (store x)).
Unfold max_log_Var.
Apply inf_log_trans' with (max_log_list Instruction extract_Var (append_instructions P)).
Intros; Apply in_inf_log.
Apply (append_instructions_correct P m); Auto.
Apply le_max_l.
Auto.
Qed.
Definition END : Method -> progCount :=
[m](anti_convert (length (instructions m))).
Definition max_log_pc := [P:Program]
(max_log_list ? END (methods P)).
Definition nth_positive := [l:(list Instruction);pc:positive]
Cases pc of
xH => (nth_error l (0))
| _ => (nth_error l (convert (sub_un pc)))
end.
Tactic Definition CaseEq a :=
Generalize (refl_equal ? a); Pattern -1 a; Case a.
Lemma nth_error_some : (A:Set;l:(list A);n:nat;x:A)
(nth_error l n)=(Some ? x) -> (In x l).
NewInduction l; Destruct n; Simpl; Intros.
Discriminate H.
Discriminate H.
Injection H; Auto.
Right; Apply IHl with n0; Auto.
Qed.
Lemma nth_error_some_inf : (A:Set;l:(list A);n:nat;x:A)
(nth_error l n)=(Some ? x) -> (lt n (length l)).
NewInduction l; Destruct n; Simpl; Intros.
Discriminate H.
Discriminate H.
Omega.
Apply lt_n_S.
Apply IHl with x; Auto.
Qed.
Lemma nth_positive_some : (I:Instruction;l:(list Instruction);pc:positive)
(nth_positive l pc)=(Some ? I) ->
(In I l).
Unfold nth_positive; Destruct pc; Intros.
Apply nth_error_some with (convert (sub_un (xI p))); Auto.
Apply nth_error_some with (convert (sub_un (xO p))); Auto.
Apply nth_error_some with (0); Auto.
Qed.
Lemma nth_positive_some_inf : (I:Instruction;l:(list Instruction);pc:positive)
(nth_positive l pc)=(Some ? I) ->
(compare pc (anti_convert (length l)) EGAL)=INFERIEUR.
Unfold nth_positive; Intros.
Elim (ZL11 pc); Intros.
Subst.
Generalize H; Clear H.
Case l; Simpl; Intros.
Discriminate H.
Apply convert_compare_INFERIEUR.
Unfold convert; Simpl.
Rewrite convert_add_un.
Generalize (bij1 (length l0)); Unfold convert; Intros H'; Rewrite H'.
Simpl.
Omega.
Apply convert_compare_INFERIEUR.
Rewrite bij1.
Replace (convert pc) with (S (convert (sub_un pc))).
Apply lt_n_S.
Generalize H0 H; Clear H0 H; Case pc; Intros.
Apply nth_error_some_inf with I; Auto.
Apply nth_error_some_inf with I; Auto.
Elim H0; Reflexivity.
Replace (S (convert (sub_un pc))) with (convert (add_un (sub_un pc))).
Elim (add_sub_one pc); Intros.
Elim H0; Auto.
Rewrite H1; Auto.
Unfold convert; Simpl.
Rewrite convert_add_un.
Auto.
Qed.
Fixpoint searchMethod_rec [m0:MethodName;l:(list Method)] : (option Method):=
Cases l of
nil => (None ?)
| (cons m q) =>
Cases (MethodName_dec m0 (nameMethod m)) of
| (left _) => (Some ? m)
| (right _) => (searchMethod_rec m0 q)
end
end.
Definition searchMethod := [P:Program;m:MethodName]
(searchMethod_rec m (methods P)).
Definition instructionAt := [P:Program;m:MethodName;pc:progCount]
Cases (searchMethod P m) of
| None => (None ?)
| (Some meth) => (nth_positive (instructions meth) pc)
end.
Lemma searchMethod_rec_some : (m:MethodName;l:(list Method);M:Method)
(searchMethod_rec m l)=(Some ? M) ->
(In M l)/\(nameMethod M)=m.
NewInduction l; Simpl; Intros.
Discriminate H.
Generalize H; Clear H.
Case MethodName_dec; Intros.
Injection H; Intros; Subst; Auto.
Elim (IHl ? H); Intros; Auto.
Qed.
Lemma searchMethod_rec_some_inv : (m:MethodName;l:(list Method);M:Method)
(allNameMethodsDistincts l) ->
(In M l) -> (nameMethod M)=m ->
(searchMethod_rec m l)=(Some ? M).
NewInduction l; Simpl; Intros.
Elim H0.
Inversion_clear H.
Elim H0; Clear H0; Intros.
Subst.
Case MethodName_dec; Intros; Auto.
Elim n; Auto.
Case MethodName_dec; Intros.
Elim H2; Exists M.
Rewrite <- e; Auto.
Auto.
Qed.
Lemma searchMethod_some : (P:Program;m:MethodName;M:Method)
(searchMethod P m)=(Some ? M) ->
(In M (methods P))/\(nameMethod M)=m.
Unfold searchMethod; Intros.
Apply searchMethod_rec_some; Auto.
Qed.
Lemma searchMethod_some_inv : (P:Program;M:Method)
(In M (methods P))->
(searchMethod P (nameMethod M))=(Some ? M).
Unfold searchMethod; Intros.
Apply searchMethod_rec_some_inv; Auto.
Apply (methodsValid P).
Qed.
Lemma instructionAt_some : (P:Program;m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some ? I) ->
(EX M:Method | (In M (methods P)) /\ (nameMethod M)=m /\
(In I (instructions M)) /\ (compare pc (END M) EGAL)=INFERIEUR).
Intros P m pc I; Unfold instructionAt.
Generalize (searchMethod_some P m).
Case (searchMethod P m); Intros.
Exists m0.
Elim (H m0); Auto; Intros.
Do 2 Try Split; Auto.
Split.
Apply nth_positive_some with pc; Auto.
Unfold END; Apply nth_positive_some_inf with I; Auto.
Discriminate H0.
Qed.
Lemma instructionAt_some_inf_log_pc : (P:Program;m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some ? I) ->
(inf_log pc (max_log_pc P)).
Intros P m pc I; Unfold instructionAt max_log_pc.
Generalize (searchMethod_some P m).
Case (searchMethod P m); Intros.
Apply inf_log_trans with (END m0).
Apply in_inf_log.
Elim (H m0); Intuition.
Unfold END.
Apply nth_positive_some_inf with I; Auto.
Discriminate H0.
Qed.
Lemma instructionAt_some_inf_log_MethodName : (P:Program;m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some ? I) ->
(inf_log m (max_log_MethodName P)).
Intros P m pc I; Unfold instructionAt max_log_MethodName.
Generalize (searchMethod_some P m).
Case (searchMethod P m); Intros.
Replace m with (nameMethod m0).
Apply in_inf_log.
Elim (H m0); Intuition.
Elim (H m0); Intuition.
Discriminate H0.
Qed.
Lemma valid_load_instructionAt :
(P:Program;m:MethodName;pc:progCount;x:Var)
(instructionAt P m pc)=(Some ? (load x)) ->
(inf_log x (max_log_Var P)).
Intros.
Elim (instructionAt_some P m pc (load x)); Intuition.
Apply valid_load with x0; Auto.
Qed.
Lemma valid_store_instructionAt :
(P:Program;m:MethodName;pc:progCount;x:Var)
(instructionAt P m pc)=(Some ? (store x)) ->
(inf_log x (max_log_Var P)).
Intros.
Elim (instructionAt_some P m pc (store x)); Intuition.
Apply valid_store with x0; Auto.
Qed.
Lemma valid_ClassName : (P:Program;cl:ClassName)
(EX c:Class | (In c (classes P)) /\ cl=(nameClass c)) ->
(inf_log cl (max_log_ClassName P)).
Intros.
Elim H; Intuition.
Rewrite H2; Unfold max_log_ClassName.
Apply in_inf_log; Auto.
Qed.
Lemma valid_putfield_instructionAt :
(P:Program;m:MethodName;pc:progCount;f:FieldName)
(instructionAt P m pc)=(Some ? (putfield f)) ->
(inf_log f (max_log_Field P)).
Intros.
Elim (instructionAt_some P m pc (putfield f)); Intuition.
Apply valid_putfield with x; Auto.
Qed.
Lemma valid_getfield_instructionAt :
(P:Program;m:MethodName;pc:progCount;f:FieldName)
(instructionAt P m pc)=(Some ? (getfield f)) ->
(inf_log f (max_log_Field P)).
Intros.
Elim (instructionAt_some P m pc (getfield f)); Intuition.
Apply valid_getfield with x; Auto.
Qed.
Lemma valid_goto_instructionAt :
(P:Program;m:MethodName;pc,pc':progCount;f:FieldName)
(instructionAt P m pc)=(Some ? (goto pc')) ->
(inf_log pc' (max_log_pc P)).
Intros.
Elim (instructionAt_some P m pc (goto pc')); Intuition.
Generalize (valid_goto_hypothesis P x pc' H1 H2);
Replace (anti_convert (length (instructions x))) with (END x);
[Intros|Unfold END;Auto].
Clear H4.
Unfold max_log_pc.
Generalize (in_inf_log ? END (methods P) x H1) ; Intros.
EApply inf_log_trans ; EAuto.
Qed.
Definition nextAddress : Program -> MethodName -> progCount -> progCount :=
[P,m,pc]
Cases (searchMethod P m) of
| None => pc
| (Some meth) =>
Cases (positive_dec pc (END meth)) of
| (left _) => pc
| (right _) => (add_un pc)
end
end.
Lemma valid_nextAddress : (P:Program;m:MethodName;pc:progCount;I:Instruction)
(instructionAt P m pc)=(Some ? I) ->
(inf_log (nextAddress P m pc) (max_log_pc P)).
Unfold nextAddress instructionAt; Intros P m pc I.
CaseEq '(searchMethod P m); Intros.
Elim (searchMethod_some ? ? ? H); Intros.
Case positive_dec; Intros.
Subst; Unfold max_log_pc.
Apply in_inf_log; Auto.
Generalize (nth_positive_some_inf ? ? ? H0); Intros.
Case (positive_dec (add_un pc) (END m0)); Intros.
Rewrite e; Unfold max_log_pc; Apply in_inf_log; Auto.
Generalize H3; Clear H3;
Replace (anti_convert (length (instructions m0))) with (END m0); [Intros|Unfold END;Auto].
Apply inf_log_trans with (END m0).
Unfold max_log_pc; Apply in_inf_log; Auto.
Apply convert_compare_INFERIEUR.
Generalize (compare_convert_INFERIEUR ? ? H3); Clear H3; Intros.
Replace (convert (add_un pc)) with (S (convert pc)).
Unfold lt in H3.
Cut ~(S (convert pc))=(convert (END m0)).
Inversion_clear H3.
Intros H'; Elim H'; Auto.
Intros.
Auto with zarith.
Red; Intros; Elim n0.
Apply convert_intro.
Rewrite <- H4; Unfold convert.
Rewrite convert_add_un; Auto.
Unfold convert; Rewrite convert_add_un; Auto.
Discriminate H0.
Qed.
Fixpoint searchField_rec [l:(list Field)] : FieldName->(option Field) :=
[f]Cases l of
nil => (None ?)
| (cons fi q) => Cases (positive_dec f (nameField fi)) of
(left _) => (Some ? fi)
| (right _) => (searchField_rec q f)
end
end.
Definition searchField : Class->FieldName->(option Field) :=
[c,f](searchField_rec (instanceFields c) f).
Lemma searchField_some : (c:Class;f:FieldName;fi:Field)
(searchField c f)=(Some ? fi) ->
(In fi (instanceFields c)) /\ f=(nameField fi).
Unfold searchField.
Intros c f fi; Generalize (instanceFields c).
NewInduction l; Simpl; Intros.
Discriminate H.
Generalize H; Clear H; Case positive_dec; Intros.
Injection H; Intros; Subst; Intuition.
Elim IHl; Intros; Auto.
Qed.
Fixpoint searchClass_rec [l:(list Class)] : ClassName->(option Class) :=
[f]Cases l of
nil => (None ?)
| (cons fi q) => Cases (positive_dec f (nameClass fi)) of
(left _) => (Some ? fi)
| (right _) => (searchClass_rec q f)
end
end.
Definition searchClass : Program->ClassName->(option Class) :=
[P,f](searchClass_rec (classes P) f).
Lemma searchClass_some : (P:Program;cl:ClassName;c:Class)
(searchClass P cl)=(Some ? c) ->
(In c (classes P)) /\ cl=(nameClass c).
Unfold searchClass.
Intros P cl; Generalize (classes P).
NewInduction l; Simpl; Intros.
Discriminate H.
Generalize H; Clear H; Case positive_dec; Intros.
Injection H; Intros; Subst; Intuition.
Elim (IHl c); Intros; Auto.
Qed.
Lemma searchClass_find : (P:Program;cl:ClassName)
(EX c:Class | (In c (classes P)) /\ cl=(nameClass c)) ->
~(searchClass P cl)=(None ?).
Intros.
Elim H; Clear H; Intros c (H1,H2).
Generalize H1; Unfold searchClass.
Generalize (classes P); Clear H1.
NewInduction l; Simpl; Intros.
Elim H1.
Case positive_dec; Intros.
Discriminate.
Elim H1; Intros.
Subst; Elim n; Auto.
Auto.
Qed.
Fixpoint searchWithMethodID [l:(list MethodID*MethodName)] : MethodID->(option MethodName) :=
[id0]Cases l of
nil => (None ?)
| (cons (id,m) q) => Cases (positive_dec id0 id) of
(left _) => (Some ? m)
| (right _) => (searchWithMethodID q id0)
end
end.
Definition methodLookup : Program -> MethodID -> ClassName -> (option Method) :=
[P,id,cl]
Cases (searchClass P cl) of
None => (None ?)
|(Some c) => Cases (searchWithMethodID (list_methods_lookup c) id) of
None => (None ?)
|(Some m) => Cases (searchMethod P m) of
None => (None ?)
|(Some M) => (Some ? M)
end
end
end.
Lemma No_return_in_main : (P : Program ; m : MethodName ; pc : progCount)
(main P) = m -> ~(instructionAt P m pc)=(Some ? return).
Red; Intros.
Elim (instructionAt_some ? ? ? ? H0).
Intros M (H1,(H2,(H3,H4))).
Elim (no_return_in_main_hypothesis P M).
Rewrite H; Auto.
Auto.
Qed.