diff options
| -rw-r--r-- | lib/real.sail | 51 | ||||
| -rw-r--r-- | lib/sail.c | 50 | ||||
| -rw-r--r-- | lib/sail.h | 5 | ||||
| -rw-r--r-- | src/bytecode_util.ml | 6 | ||||
| -rw-r--r-- | src/c_backend.ml | 6 | ||||
| -rw-r--r-- | src/value2.lem | 13 | ||||
| -rw-r--r-- | test/c/real.expect | 12 | ||||
| -rw-r--r-- | test/c/real.sail | 22 |
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 @@ -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 ***** */ @@ -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 |