From ecdbf28f72860cdb44ce9dc0bdd811b64572fd90 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 13 Oct 2017 16:06:24 +0100 Subject: Add support for real numbers to Lem backend Requires version of Lem with real number support, currently at https://bitbucket.org/bauereiss/lem/branch/reals --- src/gen_lib/sail_operators.lem | 12 +----------- src/gen_lib/sail_operators_mwords.lem | 12 +----------- src/gen_lib/sail_values.lem | 20 ++++++++++++++++++++ src/pretty_print_lem.ml | 17 ++++++++++++++++- 4 files changed, 38 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 7b117726..f14ef2e4 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -197,18 +197,8 @@ let extz_bl (start, len, bits) = Vector bits start false let exts_bl (start, len, bits) = Vector bits start false -let add (l,r) = integerAdd l r -let add_signed (l,r) = integerAdd l r -let sub (l,r) = integerMinus l r -let mult (l,r) = integerMult l r -let quotient (l,r) = integerDiv l r -let modulo (l,r) = hardware_mod l r let quot = hardware_quot -let power (l,r) = integerPow l r - -let add_int = add -let sub_int = sub -let mult_int = mult +let modulo (l,r) = hardware_mod l r let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = let (l',r') = (to_num sign l, to_num sign r) in diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index b4d1c9a4..4d1cc713 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -240,18 +240,8 @@ let extz_big (start, len, vec) = to_vec_big (unsigned_big vec) let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) -let add (l,r) = integerAdd l r -let add_signed (l,r) = integerAdd l r -let sub (l,r) = integerMinus l r -let mult (l,r) = integerMult l r -let quotient (l,r) = integerDiv l r -let modulo (l,r) = hardware_mod l r let quot = hardware_quot -let power (l,r) = integerPow l r - -let add_int = add -let sub_int = sub -let mult_int = mult +let modulo (l,r) = hardware_mod l r (* TODO: this, and the definitions that use it, currently require Size for to_vec, which I'd rather avoid in favour of library versions; the diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 1e7dc2b9..95a61eca 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -13,6 +13,26 @@ let pow m n = m ** (natFromInteger n) let pow2 n = pow 2 n +let add_int (l,r) = integerAdd l r +let add_signed (l,r) = integerAdd l r +let sub_int (l,r) = integerMinus l r +let mult_int (l,r) = integerMult l r +let quotient_int (l,r) = integerDiv l r +let quotient_nat (l,r) = natDiv l r +let power_int_nat (l,r) = integerPow l r +let power_int_int (l, r) = integerPow l (natFromInteger r) +let negate_int i = integerNegate i +let min_int (l, r) = integerMin l r +let max_int (l, r) = integerMax l r + +let add_real (l, r) = realAdd l r +let sub_real (l, r) = realMinus l r +let mult_real (l, r) = realMult l r +let div_real (l, r) = realDiv l r +let negate_real r = realNegate r +let abs_real r = realAbs r +let power_real (b, e) = realPowInteger b e + let bool_or (l, r) = (l || r) let bool_and (l, r) = (l && r) let bool_xor (l, r) = xor l r diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c74cceb9..451be476 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -289,7 +289,22 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a = (doc_tannot_lem sequential mwords false typ))) | _ -> utf8string "(failwith \"undefined value of unsupported type\")") | L_string s -> utf8string ("\"" ^ s ^ "\"") - | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *) + | L_real s -> + (* Lem does not support decimal syntax, so we translate a string + of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y). + The OCaml library has a conversion function from strings to floats, but + not from floats to ratios. ZArith's Q library does have the latter, but + using this would require adding a dependency on ZArith to Sail. *) + let parts = Util.split_on_char '.' s in + let (num, denom) = match parts with + | [i] -> (big_int_of_string i, unit_big_int) + | [i;f] -> + let denom = power_int_positive_int 10 (String.length f) in + (add_big_int (mult_big_int (big_int_of_string i) denom) (big_int_of_string f), denom) + | _ -> + raise (Reporting_basic.Fatal_error + (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in + separate space (List.map string ["realFromFrac"; string_of_big_int num; string_of_big_int denom]) (* typ_doc is the doc for the type being quantified *) let doc_quant_item (QI_aux (qi, _)) = match qi with -- cgit v1.2.3