Fix reading reals from strings in C lib

8 files changed, 143 insertions, 22 deletions

diff --git a/lib/real.sail b/lib/real.sail
new file mode 100644
index 00000000..47d3f9bd
--- /dev/null
+++ b/lib/real.sail
@@ -0,0 +1,51 @@
+$ifndef __REAL
+$define __REAL
+
+val "neg_real" : real -> real
+
+val "mult_real" : (real, real) -> real
+
+overload operator * = {mult_real}
+
+val "sub_real" : (real, real) -> real
+
+overload operator - = {sub_real}
+
+val "add_real" : (real, real) -> real
+
+overload operator + = {add_real}
+
+val "div_real" : (real, real) -> real
+
+overload operator / = {div_real}
+
+val sqrt = "sqrt_real" : real -> real
+
+val "abs_real" : real -> real
+
+val floor = "round_down" : real -> int
+
+val ceil = "round_up" : real -> int
+
+val "to_real" : int -> real
+
+val "eq_real" : (real, real) -> bool
+val "lt_real" : (real, real) -> bool
+val "gt_real" : (real, real) -> bool
+val "lteq_real" : (real, real) -> bool
+val "gteq_real" : (real, real) -> bool
+
+overload operator == = {eq_real}
+overload operator < = {lt_real}
+overload operator > = {gt_real}
+overload operator <= = {lteq_real}
+overload operator >= = {gteq_real}
+
+val pow_real = "real_power" : (real, int) -> real
+
+val "print_real" : (string, real) -> unit
+val "prerr_real" : (string, real) -> unit
+
+val "random_real" : unit -> real
+
+$endif
diff --git a/lib/sail.c b/lib/sail.c
index a5ddffe0..323ea7d8 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -10,14 +10,18 @@
  * Temporary mpzs for use in functions below. To avoid conflicts, only
  * use in functions that do not call other functions in this file.
  */
-static sail_int sail_lib_tmp1, sail_lib_tmp2;
+static sail_int sail_lib_tmp1, sail_lib_tmp2, sail_lib_tmp3;
+static real sail_lib_tmp_real;
 
 #define FLOAT_PRECISION 255
 
 void setup_library(void)
 {
+  srand(0x0);
   mpz_init(sail_lib_tmp1);
   mpz_init(sail_lib_tmp2);
+  mpz_init(sail_lib_tmp3);
+  mpq_init(sail_lib_tmp_real);
   mpf_set_default_prec(FLOAT_PRECISION);
 }
 
@@ -25,6 +29,8 @@ void cleanup_library(void)
 {
   mpz_clear(sail_lib_tmp1);
   mpz_clear(sail_lib_tmp2);
+  mpz_clear(sail_lib_tmp3);
+  mpq_clear(sail_lib_tmp_real);
 }
 
 bool eq_unit(const unit a, const unit b)
@@ -875,11 +881,17 @@ void sqrt_real(real *rop, const real op)
     /* if the difference is small enough, return */
     if (mpq_cmp(tmp, convergence) < 0) {
       mpq_set(*rop, n);
-      return;
+      break;
     }
 
     mpq_swap(n, p);
   }
+
+  mpq_clear(tmp);
+  mpz_clear(tmp_z);
+  mpq_clear(p);
+  mpq_clear(n);
+  mpq_clear(convergence);
 }
 
 void abs_real(real *rop, const real op)
@@ -958,7 +970,39 @@ void real_power(real *rop, const real base, const sail_int exp)
 void CREATE_OF(real, sail_string)(real *rop, const sail_string op)
 {
   mpq_init(*rop);
-  gmp_sscanf(op, "%Qf", *rop);
+  gmp_sscanf(op, "%Zd.%Zd", sail_lib_tmp1, sail_lib_tmp2);
+
+  unsigned long len = (unsigned long) mpz_sizeinbase(sail_lib_tmp2, 10);
+  mpz_ui_pow_ui(sail_lib_tmp3, 10, len);
+  mpz_set(mpq_numref(*rop), sail_lib_tmp2);
+  mpz_set(mpq_denref(*rop), sail_lib_tmp3);
+  mpq_canonicalize(*rop);
+  mpz_set(mpq_numref(sail_lib_tmp_real), sail_lib_tmp1);
+  mpz_set_ui(mpq_denref(sail_lib_tmp_real), 1);
+  mpq_add(*rop, *rop, sail_lib_tmp_real);
+}
+
+unit print_real(const sail_string str, const real op)
+{
+  gmp_printf("%s%Qd\n", str, op);
+  return UNIT;
+}
+
+unit prerr_real(const sail_string str, const real op)
+{
+  gmp_fprintf(stderr, "%s%Qd\n", str, op);
+  return UNIT;
+}
+
+void random_real(real *rop, const unit u)
+{
+  if (rand() & 1) {
+    mpz_set_si(mpq_numref(*rop), rand());
+  } else {
+    mpz_set_si(mpq_numref(*rop), -rand());
+  }
+  mpz_set_si(mpq_denref(*rop), rand());
+  mpq_canonicalize(*rop);
 }
 
 /* ***** Printing functions ***** */
diff --git a/lib/sail.h b/lib/sail.h
index 3f141ec7..dce4eea0 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -301,6 +301,11 @@ bool gteq_real(const real op1, const real op2);
 
 void real_power(real *rop, const real base, const sail_int exp);
 
+unit print_real(const sail_string, const real);
+unit prerr_real(const sail_string, const real);
+
+void random_real(real *rop, unit);
+
 /* ***** Printing ***** */
 
 void string_of_int(sail_string *str, const sail_int i);
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 2e6e1e29..139763b1 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -135,14 +135,14 @@ let rec frag_rename from_id to_id = function
 (**************************************************************************)
 
 let string_of_value = function
-  | V_bits bs -> Sail2_values.show_bitlist bs ^ "ul"
+  | V_bits bs -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | V_int i -> Big_int.to_string i ^ "l"
   | V_bool true -> "true"
   | V_bool false -> "false"
   | V_null -> "NULL"
   | V_unit -> "UNIT"
-  | V_bit Sail2_values.B0 -> "0ul"
-  | V_bit Sail2_values.B1 -> "1ul"
+  | V_bit Sail2_values.B0 -> "UINT64_C(0)"
+  | V_bit Sail2_values.B1 -> "UINT64_C(1)"
   | V_string str -> "\"" ^ str ^ "\""
   | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
   | _ -> failwith "Cannot convert value to string"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index ef2d9a58..c2c1fd39 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -273,8 +273,8 @@ let mask m =
   if Big_int.less_equal m (Big_int.of_int 64) then
     let n = Big_int.to_int m in
     if n mod 4 == 0
-    then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "ul"
-    else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "ul"
+    then "UINT64_C(0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ ")"
+    else "UINT64_C(" ^ String.make (64 - n) '0' ^ String.make n '1' ^ ")"
   else
     failwith "Tried to create a mask literal for a vector greater than 64 bits."
 
@@ -1872,7 +1872,7 @@ let sgen_cval_param (frag, ctyp) =
   | CT_bits direction ->
      string_of_fragment frag ^ ", " ^ string_of_bool direction
   | CT_bits64 (len, direction) ->
-     string_of_fragment frag ^ ", " ^ string_of_int len ^ "ul , " ^ string_of_bool direction
+     string_of_fragment frag ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction
   | _ ->
      string_of_fragment frag
 
diff --git a/src/value2.lem b/src/value2.lem
index d14dd87d..33416503 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -70,19 +70,6 @@ type vl =
   | V_record of list (string * vl)
   | V_null (* Used for unitialized values and null pointers in C compilation *)
 
-let string_of_value = function
-  | V_bits bs -> show_bitlist bs ^ "ul"
-  | V_int i -> show i ^ "l"
-  | V_bool true -> "true"
-  | V_bool false -> "false"
-  | V_null -> "NULL"
-  | V_unit -> "UNIT"
-  | V_bit B0 -> "0ul"
-  | V_bit B1 -> "1ul"
-  | V_string str -> "\"" ^ str ^ "\""
-  | _ -> failwith "Cannot convert value to string"
-end
-
 let primops extern args =
   match (extern, args) with
   | ("and_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 && b2)
diff --git a/test/c/real.expect b/test/c/real.expect
new file mode 100644
index 00000000..81587184
--- /dev/null
+++ b/test/c/real.expect
@@ -0,0 +1,12 @@
+1: 16
+1: 16
+1: 16
+1: 4
+1: 4
+1: 4
+2: 17
+2: 17
+2: 17
+2: 8340353015645794683299462704812268882126086134656108363777/2022832731673317417391502561215986991699553462632778473728
+2: 4
+2: 5
diff --git a/test/c/real.sail b/test/c/real.sail
new file mode 100644
index 00000000..32e58af6
--- /dev/null
+++ b/test/c/real.sail
@@ -0,0 +1,22 @@
+
+$include <arith.sail>
+$include <real.sail>
+
+val main : unit -> unit
+
+function main() = {
+  let x : real = 16.0;
+  print_real("1: ", x);
+  print_int("1: ", floor(x));
+  print_int("1: ", ceil(x));
+  print_real("1: ", sqrt(x));
+  print_int("1: ", floor(sqrt(x)));
+  print_int("1: ", ceil(sqrt(x)));
+  let x : real = 17.0;
+  print_real("2: ", x);
+  print_int("2: ", floor(x));
+  print_int("2: ", ceil(x));
+  print_real("2: ", sqrt(x));
+  print_int("2: ", floor(sqrt(x)));
+  print_int("2: ", ceil(sqrt(x)));
+}
\ No newline at end of file