Commit 89c714ce authored by Léo Gourdin's avatar Léo Gourdin
Browse files

[Broken version] Some TODO eliminated

parent fa161ba8
......@@ -152,29 +152,6 @@ Qed.
Local Hint Resolve exit_list_checker_correct: core.
(* TODO REMOVE (REPLACED) Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
match i with
| Icall sig ros args res pc' =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN
exit_checker pm (Regset.add res alive) pc' tt
| Itailcall sig ros args =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN
Some tt
| Ibuiltin ef args res pc' =>
ASSERT list_mem (params_of_builtin_args args) alive IN
exit_checker pm (reg_builtin_res res alive) pc' tt
| Ijumptable arg tbl =>
ASSERT Regset.mem arg alive IN
ASSERT exit_list_checker pm alive tbl IN
Some tt
| Ireturn optarg =>
ASSERT (reg_option_mem optarg) alive IN
Some tt
| _ => None
end.*)
Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
match i with
| Icall sig ros args res pc' =>
......@@ -208,14 +185,6 @@ Proof.
try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
Qed.
(* TODO (REPLACED) Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
match iinst_checker pm alive i with
| Some res =>
exit_checker pm (fst res) (snd res) tt
| _ =>
final_inst_checker pm alive i
end.*)
Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
match iinst_checker pm alive i with
| Some res =>
......@@ -242,11 +211,6 @@ Proof.
generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps.
Qed.
(* TODO (REPLACED) Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN
SOME i <- f.(fn_code)!(snd res) IN
inst_checker pm (fst res) i. *)
Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN
SOME i <- f.(fn_code)!(snd res) IN
......
......@@ -280,34 +280,22 @@ Proof.
intuition.
- (* Iload *)
inversion_ASSERT; try_simplify_someHyps.
destruct t. (* TODO - simplify that proof ? *)
+ inversion_SOME a0. intros EVAL.
erewrite <- eqlive_reg_listmem; eauto.
try_simplify_someHyps.
inversion_SOME v; try_simplify_someHyps.
repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
destruct t.
inversion_SOME a0. intros EVAL.
erewrite <- eqlive_reg_listmem; eauto.
try_simplify_someHyps.
inversion_SOME v; try_simplify_someHyps.
repeat (econstructor; simpl; eauto).
2:
erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto;
destruct (eval_addressing _ _ _ _);
try destruct (Memory.Mem.loadv _ _ _);
try (intros; inv H1; repeat (econstructor; simpl; eauto)).
all:
eapply eqlive_reg_update;
eapply eqlive_reg_monotonic; eauto;
intros r0; rewrite regset_add_spec;
intuition.
+ erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto.
destruct (eval_addressing _ _ _ _).
* destruct (Memory.Mem.loadv _ _ _).
** intros. inv H1. repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
intuition.
** intros. inv H1. repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
intuition.
* intros. inv H1. repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
intuition.
- (* Istore *)
(repeat inversion_ASSERT); try_simplify_someHyps.
inversion_SOME a0. intros EVAL.
......@@ -667,81 +655,6 @@ Proof.
* eapply eqlive_states_return; eauto.
Qed.
(* TODO useless?
Lemma subset_contra: forall por alive inputs,
Regset.Subset por alive ->
Regset.subset inputs alive = false ->
Regset.subset inputs por = true ->
False.
Proof.
intros por alive inputs SUB CONTRA H.
assert (INV: Regset.Subset inputs alive).
{
apply Regset.subset_2 in H.
unfold Regset.Subset in *; intros.
auto. }
apply Regset.subset_1 in INV. congruence.
Qed.
Lemma add_subset_contra: forall r por alive inputs,
Regset.Subset por alive ->
Regset.subset inputs (Regset.add r alive) = false ->
Regset.subset inputs (Regset.add r por) = true ->
False.
Proof.
intros r por alive inputs SUB CONTRA H.
assert (INV: Regset.Subset inputs (Regset.add r alive)).
{
apply Regset.subset_2 in H.
unfold Regset.Subset in *; intros.
destruct (Pos.eq_dec r a); subst.
* apply Regset.add_1; auto.
* specialize H with a.
apply Regset.add_2.
apply SUB. apply Regset.add_3 in H; auto. }
apply Regset.subset_1 in INV. congruence.
Qed.
Lemma exit_list_checker_subset_contra: forall por alive f l,
Regset.Subset por alive ->
exit_list_checker (fn_path f) alive l = false ->
exit_list_checker (fn_path f) por l = true ->
False.
Proof.
induction l.
- simpl in *; intuition.
- simpl in *. unfold exit_checker.
simplify_SOME path. generalize H2, H3.
repeat inversion_ASSERT.
+ intuition.
+ intuition.
exploit (subset_contra por alive (input_regs path0)); eauto;
intros CONTRA; inv CONTRA.
Qed.
Lemma final_inst_checker_trans: forall alive por i f,
Regset.subset por alive = true ->
final_inst_checker (fn_path f) alive por i = Some () ->
final_inst_checker (fn_path f) alive alive i = Some ().
Proof.
intros.
destruct i; simpl in *; try congruence;
generalize H0; clear H0; unfold exit_checker;
repeat inversion_ASSERT; simplify_SOME path;
repeat inversion_ASSERT; intuition.
- exploit (add_subset_contra r por alive (input_regs path0)); eauto;
intros CONTRA; inv CONTRA.
- destruct b; simpl in *.
+ exploit (add_subset_contra x por alive (input_regs path0)); eauto;
intros CONTRA; inv CONTRA.
+ exploit (subset_contra por alive (input_regs path0)); eauto;
intros CONTRA; inv CONTRA.
+ exploit (subset_contra por alive (input_regs path0)); eauto;
intros CONTRA; inv CONTRA.
- exploit (exit_list_checker_subset_contra por alive f l); eauto;
intros CONTRA; inv CONTRA.
Qed.*)
Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
list_forall2 eqlive_stackframes stk1 stk2 ->
eqlive_reg (ext alive) rs1 rs2 ->
......
......@@ -260,21 +260,6 @@ Proof.
+ rewrite <- H. erewrite <- seval_preserved; eauto.
Qed.
(* TODO: deux lemmes à deplacer dans RTLpathLivegen ou RTLpathLivegenproof ? *)
Lemma iinst_checker_default_succ f alive i res:
iinst_checker (fn_path f) alive i = Some res -> default_succ i = Some (snd res).
Proof.
destruct i; simpl; try_simplify_someHyps.
+ destruct (list_mem _ _); try_simplify_someHyps.
+ destruct (list_mem _ _); try_simplify_someHyps.
+ destruct (Regset.mem _ _); try_simplify_someHyps.
destruct (list_mem _ _); try_simplify_someHyps.
+ destruct (list_mem _ _); try_simplify_someHyps.
unfold exit_checker.
inversion_SOME path.
destruct (Regset.subset _ _); try_simplify_someHyps.
Qed.
Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
ipath_checker path f (fn_path f) alive pc = Some res
-> nth_default_succ (fn_code f) path pc = Some (snd res).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment