diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-08 14:39:52 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-08 14:39:52 +0100 |
commit | 0cb0e0c239f086b766a2b4eb65f79a426db49813 (patch) | |
tree | 34bbca57ba535899a7674cfe180a0cc3abbafae7 /backend | |
parent | 1d054a0f22ef3a24648af2620611ffc69e65d785 (diff) | |
download | compcert-kvx-0cb0e0c239f086b766a2b4eb65f79a426db49813.tar.gz compcert-kvx-0cb0e0c239f086b766a2b4eb65f79a426db49813.zip |
Réactivé l'optim mulhs pour 32-bits (Omulhs n'est jamais généré)
Diffstat (limited to 'backend')
-rw-r--r-- | backend/SelectDiv.vp | 16 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 16 |
2 files changed, 16 insertions, 16 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 315e0996..357fab5e 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 - | _ => divu_base e1 (Eop (Ointconst n2) Enil) - (* | Some(p, m) => Elet e1 (divu_mul p m) *) (* FIXME - hack K1 *) + | None => divu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divu_mul p m) 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 - | _ => modu_base e1 (Eop (Ointconst n2) Enil) - (* | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) *) (* FIXME - hack K1 *) + | None => modu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) end end. @@ -178,8 +178,8 @@ Definition divsimm (e1: expr) (n2: int) := divs_base e1 (Eop (Ointconst n2) Enil) else match divs_mul_params (Int.signed n2) with - | _ => divs_base e1 (Eop (Ointconst n2) Enil) - (* | Some(p, m) => Elet e1 (divs_mul p m) *) (* FIXME - hack K1 *) + | None => divs_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divs_mul p m) end end. @@ -204,8 +204,8 @@ Definition modsimm (e1: expr) (n2: int) := mods_base e1 (Eop (Ointconst n2) Enil) else match divs_mul_params (Int.signed n2) with - | _ => mods_base e1 (Eop (Ointconst n2) Enil) - (* | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) *) (* FIXME - hack K1 *) + | None => mods_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) end end. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 401226c4..b10deb5c 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. *) (* FIXME - K1 hack *) + econstructor; eauto. eapply eval_divu_mul; eauto. * eapply eval_divu_base; eauto. EvalOp. Qed. @@ -582,12 +582,12 @@ 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. + + 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. *) (* FIXME - K1 hack *) + red; intros; subst n2; discriminate. * eapply eval_modu_base; eauto. EvalOp. Qed. @@ -660,9 +660,9 @@ Proof. + eapply eval_divs_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_divs_base; eauto. EvalOp. - + (* destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * exists (Vint (Int.divs i n2)); split; auto. - econstructor; eauto. eapply eval_divs_mul; eauto. *) (* FIXME - hack K1 *) + econstructor; eauto. eapply eval_divs_mul; eauto. * eapply eval_divs_base; eauto. EvalOp. Qed. @@ -709,11 +709,11 @@ Proof. + eapply eval_mods_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_mods_base; eauto. EvalOp. - + (* destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * econstructor; split. econstructor. eauto. apply eval_mod_from_div with (x := i); auto. eapply eval_divs_mul with (x := i); eauto. - simpl. auto. *) (* FIXME - hack K1 *) + simpl. auto. * eapply eval_mods_base; eauto. EvalOp. Qed. |