From 60cf08670218f114539118d9e189509bb5f18695 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 22 Jun 2017 15:53:30 +0100 Subject: add a 'print' built-in function handy for writing sail tests. --- src/gen_lib/sail_values.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index e2ddd3e9..cc1979a1 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -24,6 +24,8 @@ type value = exception Sail_exit exception Sail_return +let _print s = print_string s + let string_of_bit = function | Vone -> "1" | Vzero -> "0" -- cgit v1.2.3 From 044403657d09aed9c56a9bca6decc864ed987f69 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 22 Jun 2017 16:22:22 +0100 Subject: fix three different copies of the hardware_quot function to do proper trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0. --- src/gen_lib/sail_values.lem | 14 +++++++++----- src/gen_lib/sail_values_word.lem | 14 +++++++++----- 2 files changed, 18 insertions(+), 10 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 4fded5a1..38f7d512 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -257,12 +257,16 @@ let hardware_mod (a: integer) (b:integer) : integer = then (a mod b) - b else a mod b +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) let hardware_quot (a:integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) / (abs b) - else if (a < 0 && b > 0) - then (a/b) + 1 - else a/b + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) let quot_signed = hardware_quot diff --git a/src/gen_lib/sail_values_word.lem b/src/gen_lib/sail_values_word.lem index ef7b03b9..048bf30a 100644 --- a/src/gen_lib/sail_values_word.lem +++ b/src/gen_lib/sail_values_word.lem @@ -327,12 +327,16 @@ let hardware_mod (a: integer) (b:integer) : integer = then (a mod b) - b else a mod b +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) let hardware_quot (a:integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) / (abs b) - else if (a < 0 && b > 0) - then (a/b) + 1 - else a/b + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) let quot_signed = hardware_quot -- cgit v1.2.3 From 522e9ae14eabd09bb3e7cc2fd20a8f75df9d5870 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 30 Jun 2017 14:56:50 +0100 Subject: add more tests for sail library. Can't compile entire file due to sail performance bug or infinite loop. Add some missing shallow embedding funcitons. --- src/gen_lib/sail_values.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index cc1979a1..945a7c22 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -333,6 +333,8 @@ let most_significant = function | Vregister(array,_,_,_,_) -> !array.(0) | _ -> assert false +let _most_significant = most_significant + let bitwise_not_bit = function | Vone -> Vzero | Vzero -> Vone @@ -1053,6 +1055,15 @@ let duplicate_big (bit,length) = let duplicate = duplicate_big +let duplicate_bits_big (bits, x) = + let len = (length_int bits) * (int_of_big_int x) in + let is_inc = get_ord bits in + let bits_arr = get_barray bits in + let arr = Array.concat (Array.to_list(Array.make (int_of_big_int x) bits_arr)) in + Vvector(arr, (if is_inc then 0 else (len - 1)), is_inc) + +let duplicate_bits = duplicate_bits_big + let compare_op op (l,r) = if (op l r) then Vone -- cgit v1.2.3 From 317213a43069cac5239b760c449e100c70765aa6 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Jul 2017 11:50:41 +0100 Subject: fix dodgy get_min/max_representable functions. Looks like an attempt at optimisation went wrong. --- src/gen_lib/sail_values.ml | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 945a7c22..75de6996 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -470,22 +470,25 @@ let min_32 = big_int_of_int (-2147483648) let max_8 = big_int_of_int 127 let min_8 = big_int_of_int (-128) let max_5 = big_int_of_int 31 -let min_5 = big_int_of_int (-32) let get_max_representable_in sign n = - if (n = 64) then match sign with | true -> max_64 | false -> max_64u - else if (n=32) then match sign with | true -> max_32 | false -> max_32u - else if (n=8) then max_8 - else if (n=5) then max_5 - else match sign with | true -> power_big two_big_int (pred_big_int (big_int_of_int n)) - | false -> power_big two_big_int (big_int_of_int n) - -let get_min_representable_in _ n = - if (n = 64) then min_64 - else if (n=32) then min_32 - else if (n=8) then min_8 - else if (n=5) then min_5 - else minus_big_int (power_big two_big_int (big_int_of_int n)) + match (sign, n) with + | (true, 64) -> max_64 + | (false, 64) -> max_64u + | (true, 32) -> max_32 + | (false, 32) -> max_32u + | (true, 8) -> max_8 + | (false, 5) -> max_5 + | (true, _) -> pred_big_int (power_big two_big_int (big_int_of_int (n-1))) + | (false, _) -> pred_big_int (power_big two_big_int (big_int_of_int n)) + +let get_min_representable_in sign n = + match (sign, n) with + | (false, _) -> zero_big_int + | (true, 64) -> min_64 + | (true, 32) -> min_32 + | (true, 8) -> min_8 + | (true, _) -> minus_big_int (power_big two_big_int (big_int_of_int (n-1))) let to_vec_int ord len n = let array = Array.make len Vzero in -- cgit v1.2.3 From 4d36f113efaec653f9125192c62874009cb433f4 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Jul 2017 11:51:40 +0100 Subject: implement abs function correctly for ocaml shallow embedding. --- src/gen_lib/sail_values.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 75de6996..8332aa5c 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -610,6 +610,9 @@ let min_int = min (* the built-in version *) let min = min_big (* is overwritten here *) let max_int = max (* likewise *) let max = max_big +let abs_int = abs +let abs_big = abs_big_int +let abs = abs_big let arith_op_vec_big op sign size (l,r) = let ord = get_ord l in -- cgit v1.2.3 From ce962ff43ea0025c41735faa0df52f5546cdbec9 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Jul 2017 11:54:33 +0100 Subject: substitute all uses of mod_big_int and div_big_int for Z.rem and Z.div which have correct rounding behaviour. Missed these when changing quot and mod functions. --- src/gen_lib/sail_values.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 8332aa5c..d160e84a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -920,8 +920,8 @@ let rec arith_op_no0_big op (l,r) = then None else Some (op l r) -let modulo_no0_big = arith_op_no0_big mod_big_int -let quot_no0_big = arith_op_no0_big div_big_int +let modulo_no0_big = arith_op_no0_big (Z.rem) +let quot_no0_big = arith_op_no0_big (Z.div) let rec arith_op_no0_int op (l,r) = if r = 0 @@ -970,9 +970,9 @@ let rec arith_op_vec_no0_big op sign size (l,r) = Vvector((Array.make act_size Vundef), start, ord) | _ -> assert false -let mod_vec_big = arith_op_vec_no0_big mod_big_int false unit_big_int -let quot_vec_big = arith_op_vec_no0_big div_big_int false unit_big_int -let quot_vec_signed_big = arith_op_vec_no0_big div_big_int true unit_big_int +let mod_vec_big = arith_op_vec_no0_big (Z.rem) false unit_big_int +let quot_vec_big = arith_op_vec_no0_big (Z.div) false unit_big_int +let quot_vec_signed_big = arith_op_vec_no0_big (Z.div) true unit_big_int let mod_vec = mod_vec_big let quot_vec = quot_vec_big @@ -1031,8 +1031,8 @@ let arith_op_overflow_no0_vec_big op sign size (l,r) = let overflow = if representable then Vzero else Vone in (correct_size_num,overflow,most_significant one_more) -let quot_overflow_vec_big = arith_op_overflow_no0_vec_big div_big_int false unit_big_int -let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big div_big_int true unit_big_int +let quot_overflow_vec_big = arith_op_overflow_no0_vec_big (Z.div) false unit_big_int +let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big (Z.div) true unit_big_int let quot_overflow_vec = quot_overflow_vec_big let quot_overflow_vec_signed = quot_overflow_vec_signed_big @@ -1048,7 +1048,7 @@ let arith_op_vec_range_no0_big op sign size (l,r) = let ord = get_ord l in arith_op_vec_no0_big op sign size (l,(to_vec_big ord (length_big l) r)) -let mod_vec_range_big = arith_op_vec_range_no0_big mod_big_int false unit_big_int +let mod_vec_range_big = arith_op_vec_range_no0_big (Z.rem) false unit_big_int let mod_vec_range = mod_vec_range_big -- cgit v1.2.3