Commit 80ae2a92 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

[Broken version] Intermediate local commit: proof of inst_checker_eqlive OK

parent 3486da4e
......@@ -152,7 +152,7 @@ Qed.
Local Hint Resolve exit_list_checker_correct: core.
Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
(* 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
......@@ -173,47 +173,7 @@ Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction):
ASSERT (reg_option_mem optarg) alive IN
Some tt
| _ => None
end.
Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
final_inst_checker pm alive i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
intros CHECK PC. eapply wf_last_node; eauto.
clear c pc PC. intros pc PC.
destruct i; simpl in * |- *; intuition (subst; eauto);
try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
Qed.
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.
Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
inst_checker pm alive i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
unfold inst_checker.
destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
- simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
destruct i; simpl in * |- *; intuition (subst; eauto);
try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
intros PC CHECK1 CHECK2.
intros; exploit exit_checker_res; eauto.
intros X; inversion X. intros; subst; eauto.
- eapply final_inst_checker_wellformed.
Qed.
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.
(* TODO: replace the implementation of [path_checker] above by this one in order to check [path.(pre_output_regs)]
end.*)
Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
match i with
......@@ -238,6 +198,24 @@ Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instructi
| _ => None
end.
Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
final_inst_checker pm alive por i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
intros CHECK PC. eapply wf_last_node; eauto.
clear c pc PC. intros pc PC.
destruct i; simpl in * |- *; intuition (subst; eauto);
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 =>
......@@ -248,11 +226,31 @@ Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): o
final_inst_checker pm alive por i
end.
Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
inst_checker pm alive por i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
unfold inst_checker.
destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
- simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
destruct i; simpl in * |- *; intuition (subst; eauto);
try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
intros PC CHECK1 CHECK2.
intros; exploit exit_checker_res; eauto.
intros X; inversion X. intros; subst; eauto.
- simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto.
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
inst_checker pm (fst res) (path.(pre_output_regs)) i.
*)
Lemma path_checker_wellformed f pm pc path:
path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
......
......@@ -501,9 +501,9 @@ Proof.
intros H; erewrite (EQLIVE r); eauto.
Qed.
Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive:
Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive por:
istep ge i sp rs m = Some st ->
final_inst_checker pm alive i = None.
final_inst_checker pm alive por i = None.
Proof.
destruct i; simpl; try congruence.
Qed.
......@@ -597,15 +597,16 @@ Proof.
* intuition. eapply IHtbl; eauto.
Qed.
Lemma final_inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
Lemma final_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 ->
eqlive_reg (ext por) rs1 rs2 ->
liveness_ok_function f ->
(fn_code f) ! pc = Some i ->
path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
final_inst_checker (fn_path f) alive i = Some tt ->
final_inst_checker (fn_path f) alive por i = Some tt ->
exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
Proof. Admitted. (*
intros STACKS EQLIVE LIVENESS PC;
destruct 1 as [i' sp pc rs1 m st1|
sp pc rs1 m sig ros args res pc' fd|
......@@ -661,15 +662,89 @@ Proof.
* erewrite (EQLIVE r); eauto.
eapply eqlive_states_return; eauto.
* eapply eqlive_states_return; eauto.
Qed.
Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
Qed.*)
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 ->
liveness_ok_function f ->
(fn_code f) ! pc = Some i ->
path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
inst_checker (fn_path f) alive i = Some tt ->
inst_checker (fn_path f) alive por i = Some tt ->
exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
unfold inst_checker;
......@@ -677,7 +752,7 @@ Proof.
destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
+ destruct 1 as [i' sp pc rs1 m st1| | | | | ];
try_simplify_someHyps.
intros PC ISTEP.
intros IICHECKER PC ISTEP. inversion_ASSERT.
intros.
destruct (icontinue st1) eqn: CONT.
- (* CONT => true *)
......@@ -685,7 +760,9 @@ Proof.
destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
repeat (econstructor; simpl; eauto).
rewrite <- MEM, <- PC2.
apply Regset.subset_2 in H.
exploit exit_checker_eqlive; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eapply eqlive_states_intro; eauto.
erewrite <- iinst_checker_istep_continue; eauto.
......@@ -695,7 +772,9 @@ Proof.
repeat (econstructor; simpl; eauto).
rewrite <- MEM, <- PC2.
eapply eqlive_states_intro; eauto.
+ intros; exploit final_inst_checker_eqlive; eauto.
+ inversion_ASSERT.
intros; exploit final_inst_checker_eqlive; eauto.
eapply final_inst_checker_trans; eauto.
Qed.
Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
......
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