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 ++++++++++++++++++++ 3 files changed, 22 insertions(+), 22 deletions(-) (limited to 'src/gen_lib') 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 -- cgit v1.2.3 From c97dd66c7318a0a8c79bf5674a13fb7d799e3166 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 13 Oct 2017 16:22:11 +0100 Subject: Name (bit)vector operations more explicitly Moreover, add support for pretty-printing (to Lem) vector access/update operations for vectors with non-constant, but normalized start index. --- src/gen_lib/sail_operators.lem | 8 +++++--- src/gen_lib/sail_operators_mwords.lem | 2 +- src/gen_lib/sail_values.lem | 7 +++++-- 3 files changed, 11 insertions(+), 6 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index f14ef2e4..b94257f0 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -5,7 +5,7 @@ open import Sail_values (*** Bit vector operations *) -let bvlength = length +let bitvector_length = length let set_bitvector_start = set_vector_start let reset_bitvector_start = reset_vector_start @@ -25,8 +25,10 @@ let vector_subrange_bl_dec = vector_subrange_bl let bitvector_access_inc = vector_access_inc let bitvector_access_dec = vector_access_dec -let bitvector_update_pos_dec = update_pos -let bitvector_update_subrange_dec = vector_update_dec +let bitvector_update_pos_inc = vector_update_pos_inc +let bitvector_update_pos_dec = vector_update_pos_dec +let bitvector_update_subrange_inc = vector_update_subrange_inc +let bitvector_update_subrange_dec = vector_update_subrange_dec let extract_only_bit = extract_only_element diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 4d1cc713..a1fc1fd7 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -5,7 +5,7 @@ open import Sail_values (*** Bit vector operations *) -let bvlength bs = integerFromNat (word_length bs) +let bitvector_length bs = integerFromNat (word_length bs) (*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a let set_bitvector_start (new_start, Bitvector bs _ is_inc) = diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 95a61eca..48d728bf 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -246,8 +246,8 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector ' let update (Vector bs start is_inc) i j (Vector bs' _ _) = Vector (update_aux is_inc start bs i j bs') start is_inc -let vector_update_inc (start, v, i, j, v') = update v i j v' -let vector_update_dec (start, v, i, j, v') = update v i j v' +let vector_update_subrange_inc (start, v, i, j, v') = update v i j v' +let vector_update_subrange_dec (start, v, i, j, v') = update v i j v' val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a let access_aux is_inc start xs n = @@ -264,6 +264,9 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a let update_pos v n b = update v n n (Vector [b] 0 false) +let vector_update_pos_inc (start, v, i, x) = update_pos v i x +let vector_update_pos_dec (start, v, i, x) = update_pos v i x + let extract_only_element (Vector elems _ _) = match elems with | [] -> failwith "extract_only_element called for empty vector" | [e] -> e -- cgit v1.2.3