Commit de4b95c1 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

improve the skeleton...

parent a918b4e3
......@@ -185,7 +185,6 @@ Proof.
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 =>
......@@ -216,6 +215,29 @@ Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option
(* TODO: replace the implementation of [path_checker] above by this one in order to check [path.(pre_output_regs)]
Definition final_inst_checker (pm: path_map) (alive por: 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 por) 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 por) pc' tt
| Ijumptable arg tbl =>
ASSERT Regset.mem arg alive IN
ASSERT exit_list_checker pm por tbl IN
Some tt
| Ireturn optarg =>
ASSERT (reg_option_mem optarg) alive IN
Some tt
| _ => None
end.
Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
match iinst_checker pm alive i with
| Some res =>
......@@ -223,7 +245,7 @@ Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): o
exit_checker pm por (snd res) tt
| _ =>
ASSERT Regset.subset por alive IN
final_inst_checker pm por i
final_inst_checker pm alive por i
end.
Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
......
......@@ -143,13 +143,25 @@ Obligation 2.
erewrite symbols_preserved_RTL. eauto.
Qed.
Lemma s_find_function_fundef f sp svos rs0 m0 fd
(LIVE: liveness_ok_function f):
sfind_function pge ge sp svos rs0 m0 = Some fd ->
liveness_ok_fundef fd.
Proof.
unfold sfind_function. destruct svos; simpl.
+ destruct (seval_sval _ _ _ _); try congruence.
eapply find_funct_liveness_ok; eauto.
+ destruct (Genv.find_symbol _ _); try congruence.
intros. eapply all_fundef_liveness_ok; eauto.
Qed.
Local Hint Resolve s_find_function_fundef: core.
Lemma s_find_function_preserved f sp svos1 svos2 rs0 m0 fd
(LIVE: liveness_ok_function f):
(svident_simu f (mkctx sp rs0 m0 LIVE) svos1 svos2) ->
sfind_function pge ge sp svos1 rs0 m0 = Some fd ->
exists fd', sfind_function tpge tge sp svos2 rs0 m0 = Some fd'
/\ transf_fundef fd = OK fd'
/\ liveness_ok_fundef fd.
/\ transf_fundef fd = OK fd'.
Proof.
Local Hint Resolve symbols_preserved_RTL: core.
unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *.
......@@ -159,12 +171,8 @@ Proof.
intros; exploit functions_preserved; eauto.
intros (fd' & cunit & (X1 & X2 & X3)). eexists.
repeat split; eauto.
eapply find_funct_liveness_ok; eauto.
(* intros. eapply all_fundef_liveness_ok; eauto. *)
+ subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
intros; exploit function_ptr_preserved; eauto.
intros (fd' & X). eexists. intuition eauto.
(* intros. eapply all_fundef_liveness_ok; eauto. *)
Qed.
Lemma sistate_simu f dupmap outframe sp st st' rs m is
......@@ -211,7 +219,7 @@ Proof.
eapply eqlive_reg_refl.
- (* Scall *)
exploit s_find_function_preserved; eauto.
intros (fd' & FIND & TRANSF & LIVE').
intros (fd' & FIND & TRANSF).
erewrite <- function_sig_preserved; eauto.
exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
intros (path & PATH).
......@@ -220,7 +228,7 @@ Proof.
+ simpl. repeat (econstructor; eauto).
- (* Stailcall *)
exploit s_find_function_preserved; eauto.
intros (fd' & FIND & TRANSF & LIVE').
intros (fd' & FIND & TRANSF).
erewrite <- function_sig_preserved; eauto.
eexists; split; econstructor; eauto.
+ erewrite <- preserv_fnstacksize; eauto.
......@@ -252,19 +260,70 @@ Proof.
+ rewrite <- H. erewrite <- seval_preserved; eauto.
Qed.
Lemma pre_output_regs_correct f pc0 path0 stk sp (st:sstate) rs0 m0 t s' rs m rs':
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 ->
path_step ge pge (psize path0) stk f sp rs0 m0 pc0 t s' ->
ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs m t s' ->
eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) rs rs' ->
ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' m t s'.
sexec f pc0 = Some st ->
icontinue is = true ->
list_forall2 match_stackframes stk stk' ->
ssem_internal ge sp st rs0 m0 is ->
ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
Proof.
Local Hint Resolve eqlive_stacks_refl: core.
intros LIVE PATH SEXEC CONT STK SSEM1 SSEM2 EQLIVE.
inversion SSEM2; subst; clear SSEM2.
+ (* Snone *)
eexists; split.
* econstructor.
* econstructor; eauto.
- admit. (* wf *)
- (* TODO: condition sur pre_output_regs a revoir *)
eapply eqlive_reg_monotonic; eauto; simpl.
admit.
+ (* Scall *)
eexists; split.
* econstructor; eauto.
* econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
- admit. (* wf *)
- intros; eapply eqlive_reg_update.
(* TODO: condition sur pre_output_regs a revoir *)
eapply eqlive_reg_monotonic; eauto; simpl.
admit.
+ (* Stailcall *)
eexists; split.
* econstructor; eauto.
* econstructor; eauto.
+ (* Sbuiltin *)
eexists; split.
* econstructor; eauto.
* econstructor; eauto.
- admit. (* wf *)
- (* TODO: condition sur pre_output_regs a voir *)
(* NB: cas du [regmap_setres] à traiter *)
admit.
+ (* Sjumptable *)
eexists; split.
* econstructor; eauto.
* econstructor; eauto.
- admit. (* wf *)
- (* TODO: condition sur pre_output_regs a revoir *)
eapply eqlive_reg_monotonic; eauto; simpl.
admit.
+ (* Sreturn *)
eexists; split.
* econstructor; eauto.
* econstructor; eauto.
Admitted.
(* The main theorem on simulation of symbolic states ! *)
Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
(fn_path f) ! pc0 = Some path0 ->
path_step ge pge (psize path0) stk f sp rs m pc0 t s ->
(* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *)
sexec f pc0 = Some st ->
match_function dm f f' ->
liveness_ok_function f ->
list_forall2 match_stackframes stk stk' ->
......@@ -272,7 +331,7 @@ Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
(forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) ->
exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
Proof.
intros PATH0 STEP MFUNC LIVE STACKS SEM SIMU.
intros PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU.
destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *.
- (* sem_early *)
......@@ -286,17 +345,17 @@ Proof.
- (* sem_normal *)
exploit sistate_simu; eauto.
unfold istate_simu; rewrite CONT.
intros (is' & SEM' & (CONT' & RS' & M')(* & DMEQ *)).
exploit pre_output_regs_correct; eauto.
clear SEM2; intros SEM2.
(* exploit SIMU2; eauto. *)
intros (is' & SEM' & (CONT' & RS' & M')).
exploit pre_output_regs_correct; eauto.
clear SEM2; intros (s0 & SEM2 & EQLIVE).
exploit ssem_final_simu; eauto.
clear SEM2; intros (s0 & SEM2 & MATCH0).
clear SEM2; intros (s1 & SEM2 & MATCH0).
exploit ssem_final_equiv; eauto.
clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2).
exists s1; split.
clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s2 & EQ & SEM2).
exists s2; split.
+ eapply ssem_normal; eauto.
+ eapply match_states_equiv; eauto.
+ eapply eqlive_match_states; eauto.
eapply match_states_equiv; eauto.
Qed.
Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s:
......@@ -315,7 +374,7 @@ Proof.
exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto.
intros (st & SYMB & SEM).
exploit dupmap_correct; eauto.
clear SYMB; intros (path0 & st' & PATH0 & SYMB & SIMU).
intros (path0 & st' & PATH0 & SYMB' & SIMU).
rewrite PATH0 in PATH; inversion PATH; subst.
exploit ssem_sstate_simu; eauto.
intros (s0 & SEM0 & MATCH).
......
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