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

[Broken version] Intermediate local commit: proof of siexec_snone_por in scheduler proof

parent 80ae2a92
......@@ -600,14 +600,14 @@ Qed.
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 ->
Regset.Subset por alive ->
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 por i = Some tt ->
exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof. Admitted. (*
intros STACKS EQLIVE LIVENESS PC;
Proof.
intros STACKS EQLIVE SUB LIVENESS PC;
destruct 1 as [i' sp pc rs1 m st1|
sp pc rs1 m sig ros args res pc' fd|
st1 pc rs1 m sig ros args fd m'|
......@@ -621,6 +621,7 @@ Proof. Admitted. (*
+ (* Icall *)
repeat inversion_ASSERT. intros.
exploit exit_checker_eqlive_ext1; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eexists; split.
- eapply exec_Icall; eauto.
......@@ -640,6 +641,7 @@ Proof. Admitted. (*
+ (* Ibuiltin *)
repeat inversion_ASSERT. intros.
exploit exit_checker_eqlive_builtin_res; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eexists; split.
- eapply exec_Ibuiltin; eauto.
......@@ -649,6 +651,7 @@ Proof. Admitted. (*
+ (* Ijumptable *)
repeat inversion_ASSERT. intros.
exploit exit_list_checker_eqlive; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eexists; split.
- eapply exec_Ijumptable; eauto.
......@@ -662,8 +665,9 @@ Proof. Admitted. (*
* erewrite (EQLIVE r); eauto.
eapply eqlive_states_return; eauto.
* eapply eqlive_states_return; eauto.
Qed.*)
Qed.
(* TODO useless?
Lemma subset_contra: forall por alive inputs,
Regset.Subset por alive ->
Regset.subset inputs alive = false ->
......@@ -736,7 +740,7 @@ Proof.
intros CONTRA; inv CONTRA.
- exploit (exit_list_checker_subset_contra por alive f l); eauto;
intros CONTRA; inv CONTRA.
Qed.
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 ->
......@@ -774,7 +778,6 @@ Proof.
eapply eqlive_states_intro; 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:
......
......@@ -288,6 +288,61 @@ Proof.
erewrite iinst_checker_default_succ; eauto.
Qed.
Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
(SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
(irs is) (imem is) t s)
(SIEXEC : siexec_inst i st0 = Some s0)
(ICHK : inst_checker (fn_path f) alive (pre_output_regs path0) i = Some tt),
(liveness_ok_function f) ->
list_forall2 match_stackframes stk stk' ->
eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
exists s' : state,
ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone rs' (imem is) t s' /\
eqlive_states s s'.
Proof.
Local Hint Resolve eqlive_stacks_refl: core.
intros ? ? ? LIVE STK EQLIVE.
inversion SSEM2; subst; clear SSEM2.
eexists; split.
* econstructor.
* generalize ICHK.
unfold inst_checker. destruct i; simpl in *;
unfold exit_checker; try discriminate.
all:
try destruct (list_mem _ _); simpl;
try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail).
4,5:
destruct (Regset.mem _ _); destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
1,2,3,4: assert (NPC: n=(si_pc s0)).
all: try (inv SIEXEC; simpl; auto; fail).
1,2,3,4:
try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence);
simpl; inversion_SOME p;
destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence;
intros NPATH _; econstructor; eauto;
try (instantiate (1:=p); rewrite <- NPC; auto; fail).
1,2,3,4:
eapply eqlive_reg_monotonic; eauto; simpl;
intros; apply Regset.subset_2 in SUB_PATH;
unfold Regset.Subset in SUB_PATH;
apply SUB_PATH in H; auto.
assert (NPC: n0=(si_pc s0)). { inv SIEXEC; simpl; auto. }
inversion_SOME p.
2: { destruct (Regset.subset _ _) eqn:?; try congruence. }
destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
2: { destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence. }
simpl.
destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence.
inversion_SOME p'.
destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence.
intros NPATH NPATH' _. econstructor; eauto.
instantiate (1:=p'). rewrite <- NPC; auto.
eapply eqlive_reg_monotonic; eauto; simpl.
intros. apply Regset.subset_2 in SUB_PATH.
unfold Regset.Subset in SUB_PATH.
apply SUB_PATH in H; auto.
Qed.
Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
(liveness_ok_function f) ->
(fn_path f) ! pc0 = Some path0 ->
......@@ -317,18 +372,10 @@ Proof.
clear DEFSUCC. destruct res as [alive pc1]. simpl in *.
try_simplify_someHyps.
destruct (siexec_inst i st0) eqn: SIEXEC; try_simplify_someHyps; intros.
{ (* Snone *)
inversion SSEM2; subst; clear SSEM2.
eexists; split.
* econstructor.
* econstructor; eauto.
- admit. (* wf *)
- (* TODO: condition sur pre_output_regs a revoir *)
eapply eqlive_reg_monotonic; eauto; simpl.
admit.
}
destruct i; try_simplify_someHyps; try congruence;
inversion SSEM2; subst; clear SSEM2; simpl in *.
(* Snone *)
eapply siexec_snone_por_correct; eauto.
destruct i; try_simplify_someHyps; try congruence;
inversion SSEM2; subst; clear SSEM2; simpl in *.
+ (* Scall *)
eexists; split.
* econstructor; eauto.
......
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