refactorize inst_checker for checking pre_output_regs

2 files changed, 98 insertions, 31 deletions

diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v
index 1f0ebe3c..f3ae29cf 100644
--- a/scheduling/RTLpathLivegen.v
+++ b/scheduling/RTLpathLivegen.v
@@ -152,7 +152,7 @@ Qed.
 
 Local Hint Resolve exit_list_checker_correct: core.
 
-Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
+Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
    match i with
    | Icall sig ros args res pc' =>
       ASSERT list_mem args alive IN
@@ -170,23 +170,43 @@ Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): optio
       ASSERT exit_list_checker pm alive tbl IN
       Some tt
    | Ireturn optarg =>
-      ASSERT (reg_option_mem optarg) alive IN 
+      ASSERT (reg_option_mem optarg) alive IN
       Some tt
-   | _ => 
-      SOME res <- iinst_checker pm alive i IN
-      exit_checker pm (fst res) (snd res) tt
+   | _ => None
    end.
 
-Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
-  inst_checker pm alive i = Some tt ->
+Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
+  final_inst_checker pm alive i = Some tt ->
   c!pc = Some i -> wellformed_path c pm 0 pc.
 Proof.
   intros CHECK PC. eapply wf_last_node; eauto.
   clear c pc PC. intros pc PC.
   destruct i; simpl in * |- *; intuition (subst; eauto);
   try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
-  intros X; exploit exit_checker_res; eauto.
-  clear X. intros; subst; eauto.
+Qed.
+
+
+Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
+   match iinst_checker pm alive i with
+   | Some res =>
+      exit_checker pm (fst res) (snd res) tt
+   | _ => 
+      final_inst_checker pm alive i
+   end.
+
+Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
+  inst_checker pm alive i = Some tt ->
+  c!pc = Some i -> wellformed_path c pm 0 pc.
+Proof.
+  unfold inst_checker.
+  destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
+  - simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
+    destruct i; simpl in * |- *; intuition (subst; eauto);
+    try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
+    intros PC CHECK1 CHECK2. 
+    intros; exploit exit_checker_res; eauto.
+    intros X; inversion X. intros; subst; eauto.
+  - eapply final_inst_checker_wellformed.
 Qed.
 
 Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
@@ -194,6 +214,24 @@ Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option
    SOME i <- f.(fn_code)!(snd res) IN
    inst_checker pm (fst res) i.
 
+(* TODO: replace the implementation of [path_checker] above by this one in order to check [path.(pre_output_regs)]
+
+Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
+   match iinst_checker pm alive i with
+   | Some res =>
+      ASSERT Regset.subset por (fst res) IN
+      exit_checker pm por (snd res) tt
+   | _ => 
+      ASSERT Regset.subset por alive IN
+      final_inst_checker pm por i
+   end.
+
+Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
+   SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc  IN
+   SOME i <- f.(fn_code)!(snd res) IN
+   inst_checker pm (fst res) (path.(pre_output_regs)) i.
+*)
+
 Lemma path_checker_wellformed f pm pc path:
    path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
 Proof.
diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v
index c6125985..26a1a50a 100644
--- a/scheduling/RTLpathLivegenproof.v
+++ b/scheduling/RTLpathLivegenproof.v
@@ -501,12 +501,23 @@ Proof.
   intros H; erewrite (EQLIVE r); eauto.
 Qed.
 
+Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive:
+  istep ge i sp rs m = Some st -> 
+  final_inst_checker pm alive i = None.
+Proof.
+  destruct i; simpl; try congruence.
+Qed.
+
+(* is it useful ?
 Lemma inst_checker_from_iinst_checker i sp rs m st pm alive:
   istep ge i sp rs m = Some st -> 
   inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt).
 Proof.
-  destruct i; simpl; try congruence. 
+  unfold inst_checker.
+  destruct (iinst_checker pm alive i); simpl; auto.
+  destruct i; simpl; try congruence.
 Qed.
+*)
 
 Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2:
   exit_checker pm (Regset.add r alive) pc tt = Some tt ->  
@@ -586,13 +597,13 @@ Proof.
     * intuition. eapply IHtbl; eauto.
 Qed.
 
-Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+Lemma final_inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
   eqlive_reg (ext alive) rs1 rs2 -> 
   liveness_ok_function f ->
   (fn_code f) ! pc = Some i ->
   path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
-  inst_checker (fn_path f) alive i = Some tt -> 
+  final_inst_checker (fn_path f) alive i = Some tt -> 
   exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
 Proof.
   intros STACKS EQLIVE LIVENESS PC; 
@@ -604,25 +615,8 @@ Proof.
                  st1 pc rs1 m optr m']; 
   try_simplify_someHyps.
   + (* istate *)
-    intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
-    inversion_SOME res.
-    intros.
-    destruct (icontinue st1) eqn: CONT.
-    - (* CONT => true *)
-      exploit iinst_checker_eqlive; eauto.
-      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
-      repeat (econstructor; simpl; eauto).
-      rewrite <- MEM, <- PC2.
-      exploit exit_checker_eqlive; eauto.
-      intros (path & PATH & EQLIVE2).
-      eapply eqlive_states_intro; eauto.
-      erewrite <- iinst_checker_istep_continue; eauto.
-    - (* CONT => false *)
-      intros; exploit iinst_checker_eqlive_stopped; eauto.
-      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
-      repeat (econstructor; simpl; eauto).
-      rewrite <- MEM, <- PC2.
-      eapply eqlive_states_intro; eauto.
+    intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto.
+    congruence.
   + (* Icall *)
     repeat inversion_ASSERT. intros.
     exploit exit_checker_eqlive_ext1; eauto.
@@ -669,6 +663,41 @@ Proof.
       * eapply eqlive_states_return; eauto.
 Qed.
 
+Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+  list_forall2 eqlive_stackframes stk1 stk2 ->
+  eqlive_reg (ext alive) rs1 rs2 -> 
+  liveness_ok_function f ->
+  (fn_code f) ! pc = Some i ->
+  path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
+  inst_checker (fn_path f) alive i = Some tt -> 
+  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
+Proof.
+  unfold inst_checker;
+  intros STACKS EQLIVE LIVENESS PC.
+  destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
+  + destruct 1 as [i' sp pc rs1 m st1| | | | | ];
+    try_simplify_someHyps.
+    intros PC ISTEP.
+    intros.
+    destruct (icontinue st1) eqn: CONT.
+    - (* CONT => true *)
+      exploit iinst_checker_eqlive; eauto.
+      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
+      repeat (econstructor; simpl; eauto).
+      rewrite <- MEM, <- PC2.
+      exploit exit_checker_eqlive; eauto.
+      intros (path & PATH & EQLIVE2).
+      eapply eqlive_states_intro; eauto.
+      erewrite <- iinst_checker_istep_continue; eauto.
+    - (* CONT => false *)
+      intros; exploit iinst_checker_eqlive_stopped; eauto.
+      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
+      repeat (econstructor; simpl; eauto).
+      rewrite <- MEM, <- PC2.
+      eapply eqlive_states_intro; eauto.
+  + intros; exploit final_inst_checker_eqlive; eauto.
+Qed.
+
 Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
   path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 ->
   list_forall2 eqlive_stackframes stk1 stk2 ->