From 8d1640310eaa21a612366a793ae01d0480989e27 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Mon, 9 Dec 2019 16:43:25 +0100
Subject: [PATCH] [MPFR] add more functions and better treatment of print
output variables in main.c
---
include/mpfr_lustre.c | 48 ++++++++++++++++++++++++++++++
include/mpfr_lustre.lusi | 4 +++
src/backends/C/c_backend_common.ml | 17 ++++++-----
src/plugins/mpfr/mpfr.ml | 12 +++++++-
4 files changed, 73 insertions(+), 8 deletions(-)
diff --git a/include/mpfr_lustre.c b/include/mpfr_lustre.c
index bea22e57..b8f427b2 100644
--- a/include/mpfr_lustre.c
+++ b/include/mpfr_lustre.c
@@ -101,6 +101,54 @@ void MPFRint_to_real_step (int i, mpfr_t out)
{
mpfr_set_si(out, i, MPFR_RNDN);
}
+
+void MPFRreal_to_int_step (mpfr_t in1, int *out)
+{
+ *out = mpfr_get_sj (in1, MPFR_RNDN);
+}
+
+void MPFRFloor (mpfr_t in1, int *out)
+{
+ mpfr_t tmp;
+ int prec;
+ mpfr_init (tmp); // would be better to avoid local init
+ prec = mpfr_get_prec (in1);
+ mpfr_set_prec(tmp, prec);
+
+ mpfr_floor(tmp, in1);
+ *out = mpfr_get_sj (tmp, MPFR_RNDN);
+
+ mpfr_clear(tmp);
+}
+
+void MPFRCeiling (mpfr_t in1, int *out)
+{
+ mpfr_t tmp;
+ int prec;
+ mpfr_init (tmp); // would be better to avoid local init
+ prec = mpfr_get_prec (in1);
+ mpfr_set_prec(tmp, prec);
+
+ mpfr_ceil(tmp, in1);
+ *out = mpfr_get_sj (tmp, MPFR_RNDN);
+
+ mpfr_clear(tmp);
+}
+
+void MPFRRound (mpfr_t in1, int *out)
+{
+ mpfr_t tmp;
+ int prec;
+ mpfr_init (tmp); // would be better to avoid local init
+ prec = mpfr_get_prec (in1);
+ mpfr_set_prec(tmp, prec);
+
+ mpfr_round(tmp, in1);
+ *out = mpfr_get_sj (tmp, MPFR_RNDN);
+
+ mpfr_clear(tmp);
+}
+
// functions of lustrec_math
void MPFRacos_step (mpfr_t i,
mpfr_t out
diff --git a/include/mpfr_lustre.lusi b/include/mpfr_lustre.lusi
index 801d53af..6e7f0f9b 100644
--- a/include/mpfr_lustre.lusi
+++ b/include/mpfr_lustre.lusi
@@ -22,6 +22,10 @@ function MPFRNeq(i1, i2: real) returns (out: bool);
-- Functions already available in conv
function MPFRint_to_real (x: int) returns (y: real);
+function MPFRreal_to_int (in1: real) returns (out: int);
+function MPFRFloor (in1: real) returns (out: int);
+function MPFRCeiling (in1: real) returns (out: int);
+function MPFRRound (in1: real) returns (out: int);
-- Functions already available in lustrec_math
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 9536034d..462de54d 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -723,13 +723,16 @@ let print_put_var fmt file_suffix name var_type var_id =
pp_file fmt "i" var_id
)
else if Types.is_real_type unclocked_t then
- let _ =
- if !Options.mpfr then
- fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@ " name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double
- else
- fprintf fmt "_put_double(\"%s\", %s, %i);@ " name var_id !Options.print_prec_double
- in
- pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", " ^ var_id)
+
+ if !Options.mpfr then (
+ fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@ " name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double;
+ pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", mpfr_get_d(" ^ var_id ^ ", MPFR_RNDN)")
+ )
+ else (
+ fprintf fmt "_put_double(\"%s\", %s, %i);@ " name var_id !Options.print_prec_double;
+ pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", " ^ var_id)
+ )
+
else
(Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false)
diff --git a/src/plugins/mpfr/mpfr.ml b/src/plugins/mpfr/mpfr.ml
index 76ea13bf..0f43e6d7 100644
--- a/src/plugins/mpfr/mpfr.ml
+++ b/src/plugins/mpfr/mpfr.ml
@@ -16,6 +16,8 @@ open Corelang
open Normalization
open Machine_code_common
+let report = Log.report ~plugin:"MPFR"
+
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
let cpt_fresh = ref 0
@@ -99,6 +101,14 @@ let base_inject_op id =
| "!=" -> "MPFRNeq"
(* Conv functions *)
| "int_to_real" -> "MPFRint_to_real"
+ | "real_to_int" -> "MPFRreal_to_int"
+ | "_floor" -> "MPFRfloor"
+ | "_ceil" -> "MPFRceil"
+ | "_round" -> "MPFRround"
+ | "_Floor" -> "MPFRFloor"
+ | "_Ceiling" -> "MPFRCeiling"
+ | "_Round" -> "MPFRRound"
+
(* Math library functions *)
| "acos" -> "MPFRacos"
| "acosh" -> "MPFRacosh"
@@ -128,7 +138,7 @@ let base_inject_op id =
| _ -> raise Not_found
let inject_op id =
- Format.eprintf "trying to inject mpfr into function %s@." id;
+ report ~level:3 (fun fmt -> Format.fprintf fmt "trying to inject mpfr into function %s@." id);
try
base_inject_op id
with Not_found -> id
--
GitLab