diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 12:55:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 12:55:03 +0100 |
| commit | 2638a022276c932ed00dc3f64b0e58bc0114a3d7 (patch) | |
| tree | bc8beeb8f99d55ac3bf7012e858a0fae2d38bc31 /backend | |
| parent | 3718f2f520fc9a4dec2e9c1ac6eaf71f36f4f8a1 (diff) | |
| download | compcert-kvx-2638a022276c932ed00dc3f64b0e58bc0114a3d7.tar.gz compcert-kvx-2638a022276c932ed00dc3f64b0e58bc0114a3d7.zip | |
la division flottante fonctionne
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/SelectDiv.vp | 8 | ||||
| -rw-r--r-- | backend/SelectDivproof.v | 8 | ||||
| -rw-r--r-- | backend/Selection.v | 5 |
3 files changed, 12 insertions, 9 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 662162e8..7241d028 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -316,25 +316,25 @@ Definition modls (e1 e2: expr) := Definition divfimm (e: expr) (n: float) := match Float.exact_inverse n with | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil) - | None => divfbase e (Eop (Ofloatconst n) Enil) + | None => divf_base e (Eop (Ofloatconst n) Enil) end. Nondetfunction divf (e1: expr) (e2: expr) := match e2 with | Eop (Ofloatconst n2) Enil => divfimm e1 n2 - | _ => divfbase e1 e2 + | _ => divf_base e1 e2 end. Definition divfsimm (e: expr) (n: float32) := match Float32.exact_inverse n with | Some n' => Eop Omulfs (e ::: Eop (Osingleconst n') Enil ::: Enil) - | None => Eop Odivfs (e ::: Eop (Osingleconst n) Enil ::: Enil) + | None => divfs_base e (Eop (Osingleconst n) Enil) end. Nondetfunction divfs (e1: expr) (e2: expr) := match e2 with | Eop (Osingleconst n2) Enil => divfsimm e1 n2 - | _ => Eop Odivfs (e1 ::: e2 ::: Enil) + | _ => divfs_base e1 e2 end. End SELECT.
\ No newline at end of file diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 9b99fcbf..dbd3f58d 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -949,8 +949,8 @@ Proof. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. - + TrivialExists. -- TrivialExists. + + apply eval_divf_base; trivial. +- apply eval_divf_base; trivial. Qed. Theorem eval_divfs: @@ -965,8 +965,8 @@ Proof. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto. - + TrivialExists. -- TrivialExists. + + apply eval_divfs_base; trivial. +- apply eval_divfs_base; trivial. Qed. End CMCONSTRS. diff --git a/backend/Selection.v b/backend/Selection.v index fc9315dc..aba84049 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -395,12 +395,15 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ; do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ; do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ; + do f64_div <- lookup_helper globs "__compcert_f64_div" sig_ff_f ; + do f32_div <- lookup_helper globs "__compcert_f32_div" sig_ss_s ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod i64_shl i64_shr i64_sar i64_umulh i64_smulh - i32_sdiv i32_udiv i32_smod i32_umod). + i32_sdiv i32_udiv i32_smod i32_umod + f64_div f32_div). (** Conversion of programs. *) |