From d948c0bd7c9dc0d69651e15b8e27e45f15204f08 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 15 Nov 2018 19:18:48 -0800
Subject: [PATCH] math fun lib support in MPFR
---
include/mpfr_lustre.c | 172 ++++++++++++++++++++++++++++++++
include/mpfr_lustre.lusi | 30 +++++-
src/backends/C/c_backend_src.ml | 4 +-
src/plugins/mpfr/mpfr.ml | 30 ++++++
4 files changed, 232 insertions(+), 4 deletions(-)
diff --git a/include/mpfr_lustre.c b/include/mpfr_lustre.c
index d58ca6a4..3d32f624 100644
--- a/include/mpfr_lustre.c
+++ b/include/mpfr_lustre.c
@@ -94,3 +94,175 @@ void MPFRClear(mpfr_t i)
{
mpfr_clear(i);
}
+
+// functions of lustrec_math
+void MPFRacos_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_acos(out, i, MPFR_RNDN);
+}
+
+void MPFRacosh_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_acosh(out, i, MPFR_RNDN);
+}
+void MPFRasin_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_asin(out, i, MPFR_RNDN);
+}
+void MPFRasinh_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_asinh(out, i, MPFR_RNDN);
+}
+void MPFRatan_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_atan(out, i, MPFR_RNDN);
+}
+
+void MPFRatan2_step (mpfr_t y, mpfr_t x,
+ mpfr_t out
+ )
+{
+ mpfr_atan2(out, y, x, MPFR_RNDN);
+}
+
+void MPFRatanh_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_atanh(out, i, MPFR_RNDN);
+}
+void MPFRcbrt_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_cbrt(out, i, MPFR_RNDN);
+}
+
+void MPFRcos_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_cos(out, i, MPFR_RNDN);
+}
+
+void MPFRcosh_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_cosh(out, i, MPFR_RNDN);
+}
+
+void MPFRceil_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_ceil(out, i);
+}
+
+void MPFRerf_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_erf(out, i, MPFR_RNDN);
+}
+
+void MPFRexp_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_exp(out, i, MPFR_RNDN);
+}
+
+void MPFRfabs_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_abs(out, i, MPFR_RNDN);
+}
+
+void MPFRfloor_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_floor(out, i);
+}
+
+void MPFRfmod_step (mpfr_t i1, mpfr_t i2,
+ mpfr_t out
+ )
+{
+ mpfr_fmod(out, i1, i2, MPFR_RNDN);
+}
+
+void MPFRlog_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_log(out, i, MPFR_RNDN);
+}
+
+void MPFRlog10_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_log10(out, i, MPFR_RNDN);
+}
+
+void MPFRpow_step (mpfr_t i1, mpfr_t i2,
+ mpfr_t out
+ )
+{
+ mpfr_pow(out, i1, i2, MPFR_RNDN);
+}
+
+void MPFRround_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_round(out, i);
+}
+
+void MPFRsin_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_sin(out, i, MPFR_RNDN);
+}
+
+void MPFRsinh_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_sinh(out, i, MPFR_RNDN);
+}
+
+void MPFRsqrt_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_sqrt(out, i, MPFR_RNDN);
+}
+
+void MPFRtrunc_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_trunc(out, i);
+}
+
+void MPFRtan_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_tan(out, i, MPFR_RNDN);
+}
diff --git a/include/mpfr_lustre.lusi b/include/mpfr_lustre.lusi
index e23ae136..6f0e2c3a 100644
--- a/include/mpfr_lustre.lusi
+++ b/include/mpfr_lustre.lusi
@@ -1,5 +1,3 @@
-
-
function MPFRUminus(i: real) returns (out: real) lib gmp lib mpfr;
function MPFRPlus(i1, i2: real) returns (out: real);
@@ -21,3 +19,31 @@ function MPFRGt(i1, i2: real) returns (out: bool);
function MPFREq(i1, i2: real) returns (out: bool);
function MPFRNeq(i1, i2: real) returns (out: bool);
+
+-- Functions already available in lustrec_math
+
+function MPFRacos (x: real) returns (y: real) ;
+function MPFRacosh (x: real) returns (y: real) ;
+function MPFRasin (x: real) returns (y: real) ;
+function MPFRasinh (x: real) returns (y: real) ;
+function MPFRatan (x: real) returns (y: real) ;
+function MPFRatan2(x:real; n: real) returns (y: real) ;
+function MPFRatanh (x: real) returns (y: real) ;
+function MPFRcbrt (x: real) returns (y: real) ;
+function MPFRcos (x: real) returns (y: real) ;
+function MPFRcosh (x: real) returns (y: real) ;
+function MPFRceil (x: real) returns (y: real) ;
+function MPFRerf (x: real) returns (y: real) ;
+function MPFRexp (x: real) returns (y: real) ;
+function MPFRfabs (x: real) returns (y: real) ;
+function MPFRfloor (x: real) returns (y: real) ;
+function MPFRfmod (x,y: real) returns (z: real) ;
+function MPFRlog (x: real) returns (y: real) ;
+function MPFRlog10 (x: real) returns (y: real) ;
+function MPFRpow (x:real; n: real) returns (y: real) ;
+function MPFRround (x: real) returns (y: real) ;
+function MPFRsin (x: real) returns (y: real) ;
+function MPFRsinh (x: real) returns (y: real) ;
+function MPFRsqrt (x: real) returns (y: real) ;
+function MPFRtrunc (x: real) returns (y: real) ;
+function MPFRtan (x: real) returns (y: real) ;
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index d7d1eaaa..4a00050c 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -347,13 +347,13 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
| MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
pp_machine_instr dependencies m self fmt
(update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
+ | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
+ pp_instance_call m self fmt i vl il
| MStep ([i0], i, vl) when has_c_prototype i dependencies ->
fprintf fmt "%a = %s(%a);"
(pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
i
(Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) vl
- | MStep (il, i, vl) when Mpfr.is_homomorphic_fun i ->
- pp_instance_call m self fmt i vl il
| MStep (il, i, vl) ->
pp_basic_instance_call m self fmt i vl il
| MBranch (_, []) -> (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false)
diff --git a/src/plugins/mpfr/mpfr.ml b/src/plugins/mpfr/mpfr.ml
index 1e4c6ecc..b6f1048d 100644
--- a/src/plugins/mpfr/mpfr.ml
+++ b/src/plugins/mpfr/mpfr.ml
@@ -97,9 +97,39 @@ let base_inject_op id =
| ">" -> "MPFRGt"
| "=" -> "MPFREq"
| "!=" -> "MPFRNeq"
+ (* Math library functions *)
+ | "acos" -> "MPFRacos"
+ | "acosh" -> "MPFRacosh"
+ | "asin" -> "MPFRasin"
+ | "asinh" -> "MPFRasinh"
+ | "atan" -> "MPFRatan"
+ | "atan2" -> "MPFRatan2"
+ | "atanh" -> "MPFRatanh"
+ | "cbrt" -> "MPFRcbrt"
+ | "cos" -> "MPFRcos"
+ | "cosh" -> "MPFRcosh"
+ | "ceil" -> "MPFRceil"
+ | "erf" -> "MPFRerf"
+ | "exp" -> "MPFRexp"
+ | "fabs" -> "MPFRfabs"
+ | "floor" -> "MPFRfloor"
+ | "fmod" -> "MPFRfmod"
+ | "log" -> "MPFRlog"
+ | "log10" -> "MPFRlog10"
+ | "pow" -> "MPFRpow"
+ | "round" -> "MPFRround"
+ | "sin" -> "MPFRsin"
+ | "sinh" -> "MPFRsinh"
+ | "sqrt" -> "MPFRsqrt"
+ | "trunc" -> "MPFRtrunc"
+ | "tan" -> "MPFRtan"
+
+
+ | "pow" -> "MPFRpow"
| _ -> raise Not_found
let inject_op id =
+ Format.eprintf "trying to inject mpfr into function %s@." id;
try
base_inject_op id
with Not_found -> id
--
GitLab