progress in pre_output_regs_correct

1 files changed, 53 insertions, 5 deletions

diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 61e8eae3..026c1425 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -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 ->