Optimized selection patterns for mod: 0 % x = 0

gergo- · Sep 6, 2017 · 78555eb · 78555eb
1 parent 37e7fd1
commit 78555eb
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 4 deletions.
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
@@ -156,6 +156,10 @@ Definition modu (e1: expr) (e2: expr) :=
       then modu_base e1 e2
       else Eop (Ointconst (Int.modu n1 n2)) Enil
   | Some n2, _ => moduimm e1 n2
+  | _, Some n1 =>
+      if Int.eq n1 Int.zero
+      then Eop (Ointconst Int.zero) Enil
+      else modu_base e1 e2
   | _, _ => modu_base e1 e2
   end.
 
@@ -216,6 +220,10 @@ Definition mods (e1: expr) (e2: expr) :=
       then mods_base e1 e2
       else Eop (Ointconst (Int.mods n1 n2)) Enil
   | Some n2, _ => modsimm e1 n2
+  | _, Some n1 =>
+      if Int.eq n1 Int.zero
+      then Eop (Ointconst Int.zero) Enil
+      else mods_base e1 e2
   | _, _ => mods_base e1 e2
   end.
 
@@ -262,6 +270,10 @@ Definition modlu (e1 e2: expr) :=
                     | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2)
                     end
       end
+  | _, Some n1 =>
+      if Int64.eq n1 Int64.zero
+      then longconst Int64.zero
+      else modlu_base e1 e2
   | _, _ => modlu_base e1 e2
   end.
 
@@ -308,6 +320,10 @@ Definition modls (e1 e2: expr) :=
                     | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2)
                     end
       end
+  | _, Some n1 =>
+      if Int64.eq n1 Int64.zero
+      then longconst Int64.zero
+      else modls_base e1 e2
   | _, _ => modls_base e1 e2
   end.
 

diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
@@ -607,7 +607,14 @@ Proof.
   subst. simpl in H1. rewrite Z in H1; inv H1.
   TrivialExists.
 + subst. eapply eval_moduimm; eauto.
-- eapply eval_modu_base; eauto.
+- destruct (is_intconst a) as [n1|] eqn:A.
++ exploit is_intconst_sound; eauto. intros EA; clear A.
+  predSpec Int.eq Int.eq_spec n1 Int.zero; intros. subst.
+  simpl in H1. destruct y; inv H1.
+  destruct (Int.eq i Int.zero). inv H3.
+  TrivialExists.
+  eapply eval_modu_base; eauto.
++ eapply eval_modu_base; eauto.
 Qed.
 
 Lemma eval_divs_mul:
@@ -734,7 +741,14 @@ Proof.
   destruct (Int.eq n2 Int.zero || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H1.
   TrivialExists.
 + subst. eapply eval_modsimm; eauto.
-- eapply eval_mods_base; eauto.
+- destruct (is_intconst a) as [n1|] eqn:A.
++ exploit is_intconst_sound; eauto. intros EA; clear A.
+  predSpec Int.eq Int.eq_spec n1 Int.zero; intros. subst.
+  simpl in H1. destruct y; inv H1.
+  destruct (Int.eq i Int.zero || Int.eq Int.zero (Int.repr Int.min_signed) && Int.eq i Int.mone). inv H3.
+  TrivialExists.
+  eapply eval_mods_base; eauto.
++ eapply eval_mods_base; eauto.
 Qed.
 
 Lemma eval_modl_from_divl:
@@ -818,7 +832,14 @@ Proof.
     eapply eval_divlu_mull; eauto.
     red; intros; subst n2; discriminate Z.
 ** eapply eval_modlu_base; eauto.
-- eapply eval_modlu_base; eauto.
+- destruct (is_longconst a) as [n1|] eqn:A.
++ exploit is_longconst_sound; eauto. intros EA; clear A.
+  predSpec Int64.eq Int64.eq_spec n1 Int64.zero; intros. subst.
+  simpl in H1. destruct y; inv H1.
+  destruct (Int64.eq i Int64.zero); inv H3.
+  exploit eval_longconst; eauto.
+  eapply eval_modlu_base; eauto.
++ eapply eval_modlu_base; eauto.
 Qed.
 
 Lemma eval_divls_mull:
@@ -930,7 +951,14 @@ Proof.
    eapply eval_modl_from_divl; auto.
    eapply eval_divls_mull; eauto.
 ** eapply eval_modls_base; eauto.
-- eapply eval_modls_base; eauto.
+- destruct (is_longconst a) as [n1|] eqn:A.
++ exploit is_longconst_sound; eauto. intros EA; clear A.
+  predSpec Int64.eq Int64.eq_spec n1 Int64.zero; intros. subst.
+  simpl in H1. destruct y; inv H1.
+  destruct (Int64.eq i Int64.zero || Int64.eq Int64.zero (Int64.repr Int64.min_signed) && Int64.eq i Int64.mone); inv H3.
+  exploit eval_longconst; eauto.
+  eapply eval_modls_base; eauto.
++ eapply eval_modls_base; eauto.
 Qed.
 
 (** * Floating-point division *)