refactorize inst_checker for checking pre_output_regs

1 files changed, 47 insertions, 9 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.