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 +++++++++ src/test/lib/test_lib.sail | 56 +++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 61 insertions(+), 6 deletions(-) (limited to 'src') 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 diff --git a/src/test/lib/test_lib.sail b/src/test/lib/test_lib.sail index bcabe2cc..af783317 100644 --- a/src/test/lib/test_lib.sail +++ b/src/test/lib/test_lib.sail @@ -24,7 +24,6 @@ function (bit[64]) run ((bit[64]) x) = { test_assert ("not_bit0", (not (bitzero)) == bitone); test_assert ("not_bit1", (not (bitone)) == bitzero); - test_assert ("bitwise_not", (~ (0b01) == 0b10)); test_assert ("bitwise_not_bit0", (~ (bitzero) == bitone)); test_assert ("bitwise_not_bit1", (~ (bitone) == bitzero)); @@ -36,19 +35,17 @@ function (bit[64]) run ((bit[64]) x) = { test_assert ("bitwise_or_11", (bitone | bitone) == bitone); test_assert ("bitwise_xor", (0b0101 ^ 0b0011) == 0b0110); - (* - XXX something in here causes sail to infinite loop test_assert ("bitwise_xor_00", (bitzero ^ bitzero) == bitzero); test_assert ("bitwise_xor_01", (bitzero ^ bitone) == bitone); test_assert ("bitwise_xor_10", (bitone ^ bitzero) == bitone); - test_assert ("bitwise_xor_11", (bitone ^ bitone) == bitzero);*) + test_assert ("bitwise_xor_11", (bitone ^ bitone) == bitzero); test_assert ("bitwise_and", (0b0101 & 0b0011) == 0b0001); test_assert ("bitwise_and_00", (bitzero & bitzero) == bitzero); test_assert ("bitwise_and_01", (bitzero & bitone) == bitzero); test_assert ("bitwise_and_10", (bitone & bitzero) == bitzero); test_assert ("bitwise_and_11", (bitone & bitone) == bitone); - + test_assert ("divpospos_exact", (21 div 7) == 3); test_assert ("divposneg_exact", (21 div -7) == -3); test_assert ("divnegpos_exact", (-21 div 7) == -3); @@ -59,10 +56,57 @@ function (bit[64]) run ((bit[64]) x) = { test_assert ("divnegpos_approx", (-21 div 8) == -2); test_assert ("divnegneg_approx", (-21 div -8) == 2); - (* XXX currently crashes on shallow embedding + (* XXX currently crashes on shallow embedding test_assert ("div_overflow", ((bit[8])(0x80 quot_s 0xff)) == 0x80); *) + test_assert ("leftshift_small0", (0x99 << 0) == 0x99); + test_assert ("leftshift_small3", (0x99 << 3) == 0xc8); + test_assert ("leftshift_small7", (0x99 << 7) == 0x80); + test_assert ("leftshift_small8", (0x99 << 8) == 0x00); + test_assert ("leftshift_big0", (0x99999999999999999 << 0) == 0x99999999999999999); + test_assert ("leftshift_big3", (0x99999999999999999 << 3) == 0xcccccccccccccccc8); + test_assert ("leftshift_big7", (0x99999999999999999 << 7) == 0xccccccccccccccc80); + test_assert ("leftshift_big68", (0x99999999999999999 << 68) == 0x00000000000000000); + + test_assert ("rightshift_small0", (0x99 >> 0) == 0x99); + test_assert ("rightshift_small3", (0x99 >> 3) == 0x13); + test_assert ("rightshift_small7", (0x99 >> 7) == 0x01); + test_assert ("rightshift_small8", (0x99 >> 8) == 0x00); (* XXX fails on interp *) + test_assert ("rightshift_big0", (0x99999999999999999 >> 0) == 0x99999999999999999); + test_assert ("rightshift_big3", (0x99999999999999999 >> 3) == 0x13333333333333333); + test_assert ("rightshift_big7", (0x99999999999999999 >> 7) == 0x01333333333333333); + test_assert ("rightshift_big68", (0x99999999999999999 >> 68) == 0x00000000000000000); (* XXX fails on interp *) + + test_assert ("rotate0", (0x99 <<< 0) == 0x99); (* XXX fails on interp *) + test_assert ("rotate3", (0x99 <<< 3) == 0xcc); + test_assert ("rotate7", (0x99 <<< 7) == 0xcc); + test_assert ("rotate8", (0x99 <<< 8) == 0x99); + + (* XXX crashes on shallow embedding + test_assert ("duplicate_empty", (bitzero ^^ 0) == []); *) + test_assert ("duplicate0", (bitzero ^^ 8) == 0x00); + test_assert ("duplicate1", (bitone ^^ 8) == 0xff); + + (* XXX crashes on shallow embedding + test_assert ("duplicate_bits0", (0x21 ^^ 0) == []);*) + test_assert ("duplicate_bits1", (0xce ^^ 1) == 0xce); + test_assert ("duplicate_bits9", (0xce ^^ 9) == 0xcecececececececece); + test_assert ("duplicate_covfefe", (0xc0 : (0xfe ^^ 2)) == 0xc0fefe); + + test_assert ("extz0", EXTZ(0b00) == 0x00); + test_assert ("extz1", EXTZ(0b10) == 0x02); + test_assert ("extz2", EXTZ(0b10) == 0b10); + test_assert ("extz3", EXTZ(0b10) == 0b0); + + test_assert ("exts0", EXTS(0b00) == 0x00); + test_assert ("exts1", EXTS(0b10) == 0xfe); + test_assert ("exts2", EXTS(0b10) == 0b10); + test_assert ("exts3", EXTS(0b10) == 0b0); + + test_assert ("most_significant0", most_significant(0b011) == bitzero); + test_assert ("most_significant1", most_significant(0b100) == bitone); + return 0; } -- cgit v1.2.3