generalize entrypoint normalization checker + low-cost error messages

2 files changed, 70 insertions, 33 deletions

diff --git a/midend/RTLnorm.v b/midend/RTLnorm.v
index a1b36d0f..0a026286 100644
--- a/midend/RTLnorm.v
+++ b/midend/RTLnorm.v
@@ -87,7 +87,7 @@ Definition add_nop (pc':node) : mon node :=
   fun s =>
     let pc_new := s.(st_nextnode) in
       if peq pc' s.(st_entry)
-      then Error (Errors.msg "")
+      then Error (Errors.msg "RTLnorm - 1")
       else OK pc_new
               (mkstate (Pos.succ pc_new) 
                        (st_entry s) 
@@ -126,7 +126,7 @@ Definition upd_pred (preds_pc : list node) (pc pcnew: node) : mon unit :=
                     OK tt (mkstate (st_nextnode s)
                                    (st_entry s)
                                    (PTree.set pred (ch_successors i pc pcnew) (st_code s))) 
-                  | None => Error (Errors.msg "")
+                  | None => Error (Errors.msg "RTLnorm - 2")
                 end) 
              preds_pc.
 
@@ -189,7 +189,7 @@ Definition upd_succ (pc: node) (newsucc:node) (k: nat): mon nat :=
                      (mkstate (st_nextnode s)
                               (st_entry s)
                               (PTree.set pc (ins_newsucc i newsucc k) s.(st_code)))
-      | None => Error (Errors.msg "")
+      | None => Error (Errors.msg "RTLnorm - 3")
     end.
 
 (** [modif_ksucc] changes the instruction at [pc] concerning its
@@ -200,7 +200,7 @@ Definition modif_ksucc (is_jp:node->bool) (pc: node) (succ:node) (k: nat) : mon
       match (st_code s) ! pc with
         | None 
         | Some (Ireturn _) 
-        | Some (Itailcall _ _ _) => (Error (Errors.msg ""))
+        | Some (Itailcall _ _ _) => (Error (Errors.msg "RTLnorm - 4"))
         | _ =>
           if is_jp succ
             then
@@ -361,9 +361,10 @@ Definition checker (c: code) (tc: code) : bool :=
   PTree.fold (fun res pc i => res && (check_pc c tc pc i)) c true. 
 
 Definition check_entry (f tf: function) : bool := 
-  match (fn_code tf) ! (fn_entrypoint tf) with 
-      | Some (Inop ts) => peq ts (fn_entrypoint f)
-      | _ => false
+  match (fn_code tf) ! (fn_entrypoint tf) with
+  | Some (Inop s) =>
+    (peq s (fn_entrypoint f)) || inop_tunel 3 (fn_code tf) (fn_entrypoint f) s
+  | _ => false
   end.
 
 Definition transl_function (f: RTL.function) : Errors.res RTL.function :=
@@ -387,9 +388,11 @@ Definition transl_function (f: RTL.function) : Errors.res RTL.function :=
                            f.(RTL.fn_stacksize)
                            s''.(st_code)
                            s''.(st_entry)) in 
-              if (checker (fn_code f) (fn_code tf) && check_entry f tf) then
-                Errors.OK tf
-              else Errors.Error (Errors.msg "")
+              if checker (fn_code f) (fn_code tf) then
+                if (check_entry f tf)
+                then Errors.OK tf
+                else Errors.Error (Errors.msg "RTLnorm - 5")
+              else Errors.Error (Errors.msg "RTLnorm - 6")
           end
       end
   end.
diff --git a/midend/RTLnormspec.v b/midend/RTLnormspec.v
index 3f975c4b..a04174f6 100644
--- a/midend/RTLnormspec.v
+++ b/midend/RTLnormspec.v
@@ -71,7 +71,55 @@ Proof.
   destruct i, i'; go. 
   simpl. intros ; boolInv; auto.
 Qed.
- 
+
+Lemma inop_tunel_reach_nops : forall code n s1 s2,
+    inop_tunel n code s1 s2 = true ->
+    (s2 = s1) \/ exists aux, reach_nops code s2 s1 aux.
+Proof.
+  unfold inop_tunel.
+  induction n; intros.
+  - rewrite orb_false_r in H.
+    destruct peq in H.
+    + subst; auto.
+    + inv H.
+  - fold inop_tunel in *.
+    destruct peq in H.
+    + subst. auto.
+    + rewrite orb_false_l in H.
+      flatten H; try congruence.
+      subst.
+      eapply IHn in H; eauto.
+      inv H.
+      * right.
+        exists nil.
+        econstructor; eauto.
+      * right.
+        destruct H0 as [aux Haux].
+        exists (n1::aux).
+        econstructor; eauto.
+Qed.
+
+Lemma check_entry_correct : forall f tf,
+    check_entry f tf = true ->
+    exists aux, reach_nops (fn_code tf) (fn_entrypoint tf) (fn_entrypoint f) aux.
+Proof.
+  unfold check_entry; intros.
+  flatten H. subst.
+  apply orb_true_iff in H. inv H.
+  - destruct peq.
+    + subst.
+      exists nil.
+      constructor; auto.
+    + inv H0.
+  - eapply inop_tunel_reach_nops in H0; eauto.
+    inv H0.
+    + exists nil.
+      constructor; auto.
+    + destruct H as [aux Haux].
+      exists (n::aux).
+      econstructor; eauto.
+Qed.
+
 Lemma check_mks_spec_correct: forall code tcode pc i ti,
   code ! pc = Some i ->
   tcode ! pc = Some ti ->
@@ -84,21 +132,8 @@ Proof.
   econstructor ; eauto.
   intros k succ succ' SUCC SUCC'.
   exploit ch_succ_same_length; eauto. intros LENGTH.
-  exploit @forall_list2_nth_error; eauto. simpl; intros.
-  destruct (peq succ succ') eqn: EQ ; subst.
-  + auto. 
-  + right.  
-    unfold inop_tunel in H.
-    flatten H; subst;
-    (repeat (match goal with 
-                | id : _ || _ = true |- _ => 
-                  eapply orb_prop in id; invh or
-              end); 
-      repeat (match goal with 
-                | id : _ = true |- _ => 
-                  apply proj_sumbool_true in id ; subst
-              end); go).
-    exists (n0::n1::nil); go.
+  exploit @forall_list2_nth_error; eauto.
+  eapply inop_tunel_reach_nops; eauto.
 Qed.
 
 Lemma checker_correct : forall code tcode pc i,
@@ -112,17 +147,16 @@ Proof.
   flatten CHECK; try congruence. boolInv.
   eapply check_mks_spec_correct ; eauto ; go.
 Qed.    
-    
+  
 Lemma transl_function_spec_ok : forall f tf, 
   transl_function f = Errors.OK tf -> 
   transl_function_spec f tf.
 Proof.
   unfold transl_function ; intros f tf TRANS. 
   flatten TRANS. boolInv. simpl in *.
-  eapply transl_function_spec_intro ; eauto. 
-  - intros. simpl in *.
-    eapply checker_correct; eauto.
-  - unfold check_entry in *. 
-    flatten H5; try congruence.
-    destruct peq; go. 
+  eapply check_entry_correct in Eq3; eauto.
+  destruct Eq3 as [aux Hentry]. 
+  eapply transl_function_spec_intro; eauto.
+  intros.
+  eapply checker_correct; eauto.
 Qed.