Commit 3486da4e authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

progress in pre_output_regs_correct

parent de4b95c1
......@@ -260,21 +260,65 @@ 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).
Proof.
induction path; simpl.
+ try_simplify_someHyps.
+ intros alive pc res.
inversion_SOME i; intros INST.
inversion_SOME res0; intros ICHK IPCHK.
rewrite INST.
erewrite iinst_checker_default_succ; eauto.
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 ->
(* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *) (* NB: should be useless *)
sexec f pc0 = Some st ->
icontinue is = true ->
(* icontinue is = true -> *)
list_forall2 match_stackframes stk stk' ->
ssem_internal ge sp st rs0 m0 is ->
(* 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 *)
intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE.
(* start decomposing path_checker *)
generalize (LIVE pc0 path0 PATH0).
unfold path_checker.
inversion_SOME res; intros IPCHK.
inversion_SOME i; intros INST ICHK.
exploit ipath_checker_default_succ; eauto. intros DEFSUCC.
(* start decomposing SEXEC *)
generalize SEXEC; clear SEXEC.
unfold sexec; rewrite PATH0.
inversion_SOME st0; intros SEXEC_PATH.
exploit siexec_path_default_succ; eauto.
simpl. rewrite DEFSUCC.
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.
......@@ -282,6 +326,9 @@ Proof.
- (* 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 *.
+ (* Scall *)
eexists; split.
* econstructor; eauto.
......@@ -319,6 +366,7 @@ Proof.
* 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 ->
......
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