Désactivé toutes les optim division par constante --> Omulhs etc..

2 files changed, 26 insertions, 26 deletions

diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index e1ba0bff..315e0996 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -118,8 +118,8 @@ Definition divuimm (e1: expr) (n2: int) :=
         divu_base e1 (Eop (Ointconst n2) Enil)
       else
         match divu_mul_params (Int.unsigned n2) with
-        | None => divu_base e1 (Eop (Ointconst n2) Enil)
-        | Some(p, m) => Elet e1 (divu_mul p m)
+        | _ => divu_base e1 (Eop (Ointconst n2) Enil)
+        (* | Some(p, m) => Elet e1 (divu_mul p m) *) (* FIXME - hack K1 *)
         end
   end.
 
@@ -144,8 +144,8 @@ Definition moduimm (e1: expr) (n2: int) :=
         modu_base e1 (Eop (Ointconst n2) Enil)
       else
         match divu_mul_params (Int.unsigned n2) with
-        | None => modu_base e1 (Eop (Ointconst n2) Enil)
-        | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
+        | _ => modu_base e1 (Eop (Ointconst n2) Enil)
+        (* | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) *) (* FIXME - hack K1 *)
         end
   end.
 
@@ -241,8 +241,8 @@ Definition divlu (e1 e2: expr) :=
                     divlu_base e1 e2
                   else
                     match divlu_mul_params (Int64.unsigned n2) with
-                    | None => divlu_base e1 e2
-                    | Some(p, m) => Elet e1 (divlu_mull p m)
+                    | _ => divlu_base e1 e2
+                    (* | Some(p, m) => Elet e1 (divlu_mull p m) *) (* FIXME - hack K1 *)
                     end
       end
   | _, _ => divlu_base e1 e2
@@ -258,8 +258,8 @@ Definition modlu (e1 e2: expr) :=
                     modlu_base e1 e2
                   else
                     match divlu_mul_params (Int64.unsigned n2) with
-                    | None => modlu_base e1 e2
-                    | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2)
+                    | _ => modlu_base e1 e2
+                    (* | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2) *) (* FIXME - hack K1 *)
                     end
       end
   | _, _ => modlu_base e1 e2
@@ -285,8 +285,8 @@ Definition divls (e1 e2: expr) :=
                     divls_base e1 e2
                   else
                     match divls_mul_params (Int64.signed n2) with
-                    | None => divls_base e1 e2
-                    | Some(p, m) => Elet e1 (divls_mull p m)
+                    | _ => divls_base e1 e2
+                    (* | Some(p, m) => Elet e1 (divls_mull p m) *) (* FIXME - hack K1 *)
                     end
       end
   | _, _ => divls_base e1 e2
@@ -304,8 +304,8 @@ Definition modls (e1 e2: expr) :=
                     modls_base e1 e2
                   else
                     match divls_mul_params (Int64.signed n2) with
-                    | None => modls_base e1 e2
-                    | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2)
+                    | _ => modls_base e1 e2
+                    (* | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2) *) (* FIXME - hack K1 *)
                     end
       end
   | _, _ => modls_base e1 e2
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index aa6750ed..401226c4 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -530,9 +530,9 @@ Proof.
   simpl. erewrite Int.is_power2_range; eauto.
 - destruct (Compopts.optim_for_size tt).
   + eapply eval_divu_base; eauto. EvalOp.
-  + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+  + (* destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
     * exists (Vint (Int.divu i n2)); split; auto.
-      econstructor; eauto. eapply eval_divu_mul; eauto.
+      econstructor; eauto. eapply eval_divu_mul; eauto. *) (* FIXME - K1 hack *)
     * eapply eval_divu_base; eauto. EvalOp.
 Qed.
 
@@ -582,13 +582,13 @@ Proof.
   apply eval_andimm. auto.
 - destruct (Compopts.optim_for_size tt).
   + eapply eval_modu_base; eauto. EvalOp.
-  + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
-    * econstructor; split.
+  + (* destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+     * econstructor; split.
       econstructor; eauto. eapply eval_mod_from_div.
       eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto.
       rewrite Int.modu_divu. auto.
-      red; intros; subst n2; discriminate.
-    * eapply eval_modu_base; eauto. EvalOp.
+      red; intros; subst n2; discriminate. *) (* FIXME - K1 hack *)
+     * eapply eval_modu_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_modu:
@@ -784,10 +784,10 @@ Proof.
 + destruct (Int64.is_power2' n2) as [l|] eqn:POW.
 * exploit Val.divlu_pow2; eauto. intros EQ; subst z. apply eval_shrluimm; auto.
 * destruct (Compopts.optim_for_size tt). eapply eval_divlu_base; eauto.
-  destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS.
+  (* destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS.
 ** destruct x; simpl in H1; try discriminate.
    destruct (Int64.eq n2 Int64.zero); inv H1.
-   econstructor; split; eauto. econstructor. eauto. eapply eval_divlu_mull; eauto.
+   econstructor; split; eauto. econstructor. eauto. eapply eval_divlu_mull; eauto. *) (* FIXME - K1 hack *)
 ** eapply eval_divlu_base; eauto.
 - eapply eval_divlu_base; eauto.
 Qed.
@@ -809,14 +809,14 @@ Proof.
 + destruct (Int64.is_power2 n2) as [l|] eqn:POW.
 * exploit Val.modlu_pow2; eauto. intros EQ; subst z. eapply eval_andl; eauto. apply eval_longconst.
 * destruct (Compopts.optim_for_size tt). eapply eval_modlu_base; eauto.
-  destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS.
+  (* destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS.
 ** destruct x; simpl in H1; try discriminate.
    destruct (Int64.eq n2 Int64.zero) eqn:Z; inv H1.
    rewrite Int64.modu_divu.
     econstructor; split; eauto. econstructor. eauto.
     eapply eval_modl_from_divl; eauto.
     eapply eval_divlu_mull; eauto.
-    red; intros; subst n2; discriminate Z.
+    red; intros; subst n2; discriminate Z. *)
 ** eapply eval_modlu_base; eauto.
 - eapply eval_modlu_base; eauto.
 Qed.
@@ -879,12 +879,12 @@ Proof.
 ** exploit Val.divls_pow2; eauto. intros EQ. eapply eval_shrxlimm; eauto.
 ** eapply eval_divls_base; eauto.
 * destruct (Compopts.optim_for_size tt). eapply eval_divls_base; eauto.
-  destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS.
+  (* destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS.
 ** destruct x; simpl in H1; try discriminate.
    destruct (Int64.eq n2 Int64.zero
              || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1.
    econstructor; split; eauto. econstructor. eauto.
-   eapply eval_divls_mull; eauto.
+   eapply eval_divls_mull; eauto. *)
 ** eapply eval_divls_base; eauto.
 - eapply eval_divls_base; eauto.
 Qed.
@@ -921,14 +921,14 @@ Proof.
   rewrite Int64.mods_divs. auto.
 **eapply eval_modls_base; eauto.
 * destruct (Compopts.optim_for_size tt). eapply eval_modls_base; eauto.
-  destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS.
+  (* destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS.
 ** destruct x; simpl in H1; try discriminate.
    destruct (Int64.eq n2 Int64.zero
              || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1.
    econstructor; split; eauto. econstructor. eauto.
    rewrite Int64.mods_divs.
    eapply eval_modl_from_divl; auto.
-   eapply eval_divls_mull; eauto.
+   eapply eval_divls_mull; eauto. *)
 ** eapply eval_modls_base; eauto.
 - eapply eval_modls_base; eauto.
 Qed.