improve the skeleton...

2 files changed, 107 insertions, 26 deletions

diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v
index f3ae29cf..7449dcc6 100644
--- a/scheduling/RTLpathLivegen.v
+++ b/scheduling/RTLpathLivegen.v
@@ -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 :=
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 23f7fa8a..61e8eae3 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -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).