Tests for (almost) all sail builtins. Many interesting things discovered. Library in need of rationalisation.

1 files changed, 351 insertions, 4 deletions

diff --git a/src/test/lib/test_lib.sail b/src/test/lib/test_lib.sail
index 1f241aa0..b362811c 100644
--- a/src/test/lib/test_lib.sail
+++ b/src/test/lib/test_lib.sail
@@ -25,8 +25,8 @@ function unit test_not () = {
   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));
+  test_assert ("bitwise_not_bit0", ((~ (bitzero)) == bitone));
+  test_assert ("bitwise_not_bit1", ((~ (bitone)) == bitzero));
 }
 
 function unit test_or () = {
@@ -223,8 +223,61 @@ function unit test_multiply () = {
   test_assert ("mult_range_vec_signed", ((bit[8])(6 *_s 0xb)) == 0xe2);
   test_assert ("mult_vec_range_signed", ((bit[8])(0x6 *_s 11)) == 0xe2);
 
-  (* XXX not sure what this should do...
-  test_assert ("mult_overflow_vec_signed", ); *)
+  (* XXX don't think it's possible to set carryout out bit *)
+  test_assert ("mult_overflow_vec_signed0", (((bit[8], bit, bit)) (0xf *_s 0x2)) == (0xfe, false, false));
+  test_assert ("mult_overflow_vec_signed1", (((bit[8], bit, bit)) (0xf *_s 0xf)) == (0x01, false, false));
+  test_assert ("mult_overflow_vec_signed2", (((bit[8], bit, bit)) (0x8 *_s 0x8)) == (0x40, true, false));
+  test_assert ("mult_overflow_vec_signed3", (((bit[8], bit, bit)) (0x7 *_s 0x7)) == (0x31, true, false));
+  test_assert ("mult_overflow_vec_signed4", (((bit[8], bit, bit)) (0x8 *_s 0x7)) == (0xc8, true, false));
+}
+
+function unit test_mod () = {
+  test_assert ("modpospos_exact", (21 mod 7) == 0);
+  test_assert ("modposneg_exact", (21 mod -7) == 0);
+  test_assert ("modnegpos_exact", (-21 mod 7) == 0);
+  test_assert ("modnegneg_exact", (-21 mod -7) == 0);
+
+  test_assert ("modpospos_approx", (21 mod 8) == 5);
+  test_assert ("modposneg_approx", (21 mod -8) == 5);
+  test_assert ("modnegpos_approx", (-21 mod 8) == -5);
+  test_assert ("modnegneg_approx", (-21 mod -8) == -5);
+ 
+  (* XXX how to test this? Type checker should catch?
+  test_assert ("mod_zero", (21 mod 0) == undefined); *)
+
+  test_assert("mod_vec_range_pos", (0x7 mod 5) == 2);
+  test_assert("mod_vec_range_neg", (0xf mod 5) == 0);
+
+  test_assert("mod_vec_pos", (0x7 mod 0x5) == 0x2);
+  test_assert("mod_vec_neg", (0xf mod 0x5) == 0x0);
+  test_assert("mod_vec_pos_neg", (0x7 mod 0x8) == 0x7);
+  test_assert("mod_vec_neg_neg", (0xf mod 0x8) == 0x7);
+}
+
+function unit test_mod_signed () = {
+  ();
+  (* XXX mod_signed does exist on ocaml shallow embedding...
+  test_assert ("mod_signed_pospos_exact", (21 mod_s 7) == 0);
+  test_assert ("mod_signed_posneg_exact", (21 mod_s -7) == 0);
+  test_assert ("mod_signed_negpos_exact", (-21 mod_s 7) == 0);
+  test_assert ("mod_signed_negneg_exact", (-21 mod_s -7) == 0);
+
+  test_assert ("mod_signed_pospos_approx", (21 mod_s 8) == 5);
+  test_assert ("mod_signed_posneg_approx", (21 mod_s -8) == 5);
+  test_assert ("mod_signed_negpos_approx", (-21 mod_s 8) == -5);
+  test_assert ("mod_signed_negneg_approx", (-21 mod_s -8) == -5);
+ 
+  (* XXX how to test this? Type checker should catch?
+  test_assert ("mod_signed_zero", (21 mod_s 0) == undefined); *)
+
+  test_assert("mod_vec_range_signed_pos", (0x7 mod_s 5) == 2);
+  test_assert("mod_vec_range_signed_neg", (0xf mod_s 5) == -1);
+
+  test_assert("mod_vec_signed_pos", (0x7 mod_s 0x5) == 0x2);
+  test_assert("mod_vec_signed_neg", (0xf mod_s 0x5) == 0xf);
+  test_assert("mod_vec_signed_pos_neg", (0x7 mod_s 0x8) == 0x7);
+  test_assert("mod_vec_signed_neg_neg", (0xf mod_s 0x8) == 0x7);
+  *)
 }
 
 function unit test_div () = {
@@ -238,11 +291,294 @@ function unit test_div () = {
   test_assert ("divnegpos_approx", (-21 div 8) == -2);
   test_assert ("divnegneg_approx", (-21 div -8) == 2);
 
+  (* quot and div are synonyms but let's check...  *)
+  test_assert ("quotpospos_exact", (21 quot 7) == 3);
+  test_assert ("quotposneg_exact", (21 quot -7) == -3);
+  test_assert ("quotnegpos_exact", (-21 quot 7) == -3);
+  test_assert ("quotnegneg_exact", (-21 quot -7) == 3);
+
+  test_assert ("quotpospos_approx", (21 quot 8) == 2);
+  test_assert ("quotposneg_approx", (21 quot -8) == -2);
+  test_assert ("quotnegpos_approx", (-21 quot 8) == -2);
+  test_assert ("quotnegneg_approx", (-21 quot -8) == 2);
+
   (* XXX currently crashes on shallow embedding
   test_assert ("div_overflow", ((bit[8])(0x80 quot_s 0xff)) == 0x80);
   *)
+  test_assert ("quot_vec_pospos_exact", ((bit[8])(0x15 quot 0x07)) == 0x03);
+  test_assert ("quot_vec_posneg_exact", ((bit[8])(0x15 quot 0xf9)) == 0x00);
+  test_assert ("quot_vec_negpos_exact", ((bit[8])(0xeb quot 0x07)) == 0x21);
+  test_assert ("quot_vec_negneg_exact", ((bit[8])(0xeb quot 0xf9)) == 0x00);
+
+  test_assert ("quot_vec_pospos_approx", ((bit[8])(0x15 quot 0x08)) == 0x02);
+  test_assert ("quot_vec_posneg_approx", ((bit[8])(0x15 quot 0xf8)) == 0x00);
+  test_assert ("quot_vec_negpos_approx", ((bit[8])(0xeb quot 0x08)) == 0x1d);
+  test_assert ("quot_vec_negneg_approx", ((bit[8])(0xeb quot 0xf8)) == 0x00);
+
+  test_assert ("quot_overflow_vec", (((bit[8], bit, bit))(0x15 quot 0x08)) == (0x02, false, false));
+  test_assert ("quot_overflow_vec", (((bit[8], bit, bit))(0x80 quot 0xff)) == (0x00, false, false));
+}
+
+function unit test_quot_signed () = {
+  test_assert ("quot_vec_signed_pospos_exact", ((bit[8])(0x15 quot_s 0x07)) == 0x03);
+  test_assert ("quot_vec_signed_posneg_exact", ((bit[8])(0x15 quot_s 0xf9)) == 0xfd);
+  test_assert ("quot_vec_signed_negpos_exact", ((bit[8])(0xeb quot_s 0x07)) == 0xfd);
+  test_assert ("quot_vec_signed_negneg_exact", ((bit[8])(0xeb quot_s 0xf9)) == 0x03);
+
+  test_assert ("quot_vec_signed_pospos_approx", ((bit[8])(0x15 quot_s 0x08)) == 0x02);
+  test_assert ("quot_vec_signed_posneg_approx", ((bit[8])(0x15 quot_s 0xf8)) == 0xfe);
+  test_assert ("quot_vec_signed_negpos_approx", ((bit[8])(0xeb quot_s 0x08)) == 0xfe);
+  test_assert ("quot_vec_signed_negneg_approx", ((bit[8])(0xeb quot_s 0xf8)) == 0x02);
+
+  test_assert ("quot_signed_overflow_vec", (((bit[8], bit, bit))(0x15 quot_s 0x08)) == (0x02, false, false));
+  (* XXX crashes shallow embedding due to undefined result
+  let (result, overflow, carry) = ((bit[8], bit, bit))(0x80 quot_s 0xff) in {
+    test_assert ("quot_signed_overflow_vec_ov", overflow);
+    test_assert ("quot_signed_overflow_vec_ca", carry);
+  };*)
+}
+
+function unit test_misc () = {
+  test_assert ("power0", (0 ** 3) == 0);
+  test_assert ("power1", (3 ** 0) == 1);
+  test_assert ("power2", (11 ** 17) == 505447028499293771);
+  (* XXX should be type error but isn't 
+  test_assert ("power-1", (1 ** -1) == 0); *)
+
+  test_assert ("abs_neg", (abs (-42)) == 42);
+  test_assert ("abs_zero", (abs (0)) == 0);
+  test_assert ("abs_pos", (abs (143)) == 143);
+
+  test_assert ("max", max(-1, 1) == 1);
+  test_assert ("min", min(-1, 1) == -1);
+
+  test_assert ("length0", length([]) == 0);
+  test_assert ("length1", length([bitzero]) == 1);
+  test_assert ("length2", length(0x1234) == 16);
 }
 
+function unit test_eq () = {
+  test_assert("eq_bit00", false == bitzero);
+  test_assert("eq_bit01", not(false == bitone));
+  test_assert("eq_bit10", not(true == bitzero));
+  test_assert("eq_bit11", true == bitone);
+
+  test_assert("eq_vec0", not (0x1 == 0x2));
+  test_assert("eq_vec1", 0x2 == 0x2);
+  test_assert("eq_vec_range0", not (0xf == 16));
+  test_assert("eq_vec_range1", 0xf == 15);
+  test_assert("eq_range_vec0", not (16 == 0xf));
+  test_assert("eq_range_vec1", 15 == 0xf);
+  test_assert("eq_range0", not(12 == 13));
+  test_assert("eq_range1", 13 == 13);
+  test_assert("eq_tup0", not ((true, false) == (bitzero, bitzero)));
+  test_assert("eq_tup1", (true, false) == (bitone, bitzero));
+}
+
+function unit test_eq () = {
+  test_assert("eq_bit00", false == bitzero);
+  test_assert("eq_bit01", not(false == bitone));
+  test_assert("eq_bit10", not(true == bitzero));
+  test_assert("eq_bit11", true == bitone);
+
+  test_assert("eq_vec0", not (0x1 == 0x2));
+  test_assert("eq_vec1", 0x2 == 0x2);
+  test_assert("eq_vec_range0", not (0xf == 16));
+  test_assert("eq_vec_range1", 0xf == 15);
+  test_assert("eq_range_vec0", not (16 == 0xf));
+  test_assert("eq_range_vec1", 15 == 0xf);
+  test_assert("eq_range0", not(12 == 13));
+  test_assert("eq_range1", 13 == 13);
+  test_assert("eq_tup0", not ((true, false) == (bitzero, bitzero)));
+  test_assert("eq_tup1", (true, false) == (bitone, bitzero));
+}
+
+function unit test_neq () = {
+  test_assert("neq_bit00", not(false != bitzero));
+  test_assert("neq_bit01", false != bitone);
+  test_assert("neq_bit10", true != bitzero);
+  test_assert("neq_bit11", not(true != bitone));
+
+  test_assert("neq_vec0", 0x1 != 0x2);
+  test_assert("neq_vec1", not(0x2 != 0x2));
+  test_assert("neq_vec_range0", 0xf != 16);
+  test_assert("neq_vec_range0", 0x7 != 8);
+  test_assert("neq_vec_range1", not(0xf != 15));
+  (* XXX not implemented for ocaml
+  test_assert("neq_range_vec0", 16 != 0xf);
+  test_assert("neq_range_vec1", not(15 != 0xf)); *)
+  test_assert("neq_range0", 12 != 13);
+  test_assert("neq_range1", not(13 != 13));
+  test_assert("neq_tup0", (true, false) != (bitzero, bitzero));
+  test_assert("neq_tup1", not((true, false) != (bitone, bitzero)));
+}
+
+function unit test_lt() = {
+  test_assert("lt0", not( 1 < -1));
+  test_assert("lt1", not(-1 < -1));
+  test_assert("lt2",    (-1 <  1));
+
+  (* XXX default is signed -- document this! *)
+  test_assert("lt_vec0", not(0x1 < 0xf));
+  test_assert("lt_vec1", not(0xf < 0xf));
+  test_assert("lt_vec2",    (0xf < 0x1));
+
+  test_assert("lt_vec_range0", not(0x1 < -1));
+  test_assert("lt_vec_range1", not(0xf < -1));
+  test_assert("lt_vec_range2",    (0xf < 1));
+  (* NB missing range_vec version *)
+
+  (* XXX missing implementations
+  test_assert("lt_unsigned0", not( 1 <_u -1));
+  test_assert("lt_unsigned1", not(-1 <_u -1));
+  test_assert("lt_unsigned2",    (-1 <_u  1)); *)
+
+  test_assert("lt_vec_unsigned0",    (0x1 <_u 0xf));
+  test_assert("lt_vec_unsigned1", not(0xf <_u 0xf));
+  test_assert("lt_vec_unsigned2", not(0xf <_u 0x1));
+
+  (* NB there is no lt_vec_range unsigned or signed *)
+
+  (* XXX missing implementations 
+  test_assert("lt_signed0", not( 1 <_s -1));
+  test_assert("lt_signed1", not(-1 <_s -1));
+  test_assert("lt_signed2",    (-1 <_s  1)); *)
+
+  test_assert("lt_vec_signed0", not(0x1 <_s 0xf));
+  test_assert("lt_vec_signed1", not(0xf <_s 0xf));
+  test_assert("lt_vec_signed2",    (0xf <_s 0x1));
+}
+
+function unit test_gt() = {
+  test_assert("gt0",    ( 1 > -1));
+  test_assert("gt1", not(-1 > -1));
+  test_assert("gt2", not(-1 >  1));
+
+  (* XXX default is signed -- document this! *)
+  test_assert("gt_vec0",    (0x1 > 0xf));
+  test_assert("gt_vec1", not(0xf > 0xf));
+  test_assert("gt_vec2", not(0xf > 0x1));
+
+  test_assert("gt_vec_range0",    (0x1 > -1));
+  test_assert("gt_vec_range1", not(0xf > -1));
+  test_assert("gt_vec_range2", not(0xf > 1));
+  (* NB missing range_vec version *)
+
+  (* XXX missing implementations
+  test_assert("gt_unsigned0",    ( 1 >_u -1));
+  test_assert("gt_unsigned1", not(-1 >_u -1));
+  test_assert("gt_unsigned2", not(-1 >_u  1)); *)
+
+  test_assert("gt_vec_unsigned0", not(0x1 >_u 0xf));
+  test_assert("gt_vec_unsigned1", not(0xf >_u 0xf));
+  test_assert("gt_vec_unsigned2",    (0xf >_u 0x1));
+
+  (* NB there is no gt_vec_range unsigned or signed *)
+
+  (* XXX missing implementations 
+  test_assert("gt_signed0",    ( 1 >_s -1));
+  test_assert("gt_signed1", not(-1 >_s -1));
+  test_assert("gt_signed2", not(-1 >_s  1)); *)
+
+  test_assert("gt_vec_signed0",    (0x1 >_s 0xf));
+  test_assert("gt_vec_signed1", not(0xf >_s 0xf));
+  test_assert("gt_vec_signed2", not(0xf >_s 0x1));
+}
+
+function unit test_lteq() = {
+  test_assert("lteq0", not( 1 <= -1));
+  test_assert("lteq1",    (-1 <= -1));
+  test_assert("lteq2",    (-1 <=  1));
+
+  (* XXX default is signed -- document this! *)
+  test_assert("lteq_vec0", not(0x1 <= 0xf));
+  test_assert("lteq_vec1",    (0xf <= 0xf));
+  test_assert("lteq_vec2",    (0xf <= 0x1));
+
+  test_assert("lteq_vec_range0", not(0x1 <= -1));
+  test_assert("lteq_vec_range1",    (0xf <= -1));
+  test_assert("lteq_vec_range2",    (0xf <= 1));
+
+  test_assert("lteq_range_vec0", not( 1 <= 0xf));
+  test_assert("lteq_range_vec1",    (-1 <= 0xf));
+  test_assert("lteq_range_vec2",    (-1 <= 0x1));
+
+  (* XXX missing implementations
+  test_assert("lteq_unsigned0", not( 1 <=_u -1));
+  test_assert("lteq_unsigned1",    (-1 <=_u -1));
+  test_assert("lteq_unsigned2",    (-1 <=_u  1)); *)
+
+  (* XXX missing type / parser
+  test_assert("lteq_unsigned_vec0",    (0x1 <=_u 0xf));
+  test_assert("lteq_unsigned_vec1",    (0xf <=_u 0xf));
+  test_assert("lteq_unsigned_vec2", not(0xf <=_u 0x1));*)
+
+  (* NB there is no lteq_vec_range unsigned or signed *)
+
+  (* XXX missing implementations 
+  test_assert("lteq_signed0", not( 1 <=_s -1));
+  test_assert("lteq_signed1",    (-1 <=_s -1));
+  test_assert("lteq_signed2",    (-1 <=_s  1)); *)
+
+  test_assert("lteq_vec_signed0", not(0x1 <=_s 0xf));
+  test_assert("lteq_vec_signed1",    (0xf <=_s 0xf));
+  test_assert("lteq_vec_signed2",    (0xf <=_s 0x1));
+}
+
+function unit test_gteq() = {
+  test_assert("gteq0",    ( 1 >= -1));
+  test_assert("gteq1",    (-1 >= -1));
+  test_assert("gteq2", not(-1 >=  1));
+
+  (* XXX default is signed -- document this! *)
+  test_assert("gteq_vec0",    (0x1 >= 0xf));
+  test_assert("gteq_vec1",    (0xf >= 0xf));
+  test_assert("gteq_vec2", not(0xf >= 0x1));
+
+  (* XXX odd type error here -- sail seems to prefer gteq_vec...
+  test_assert("gteq_vec_range0",    (0x1 >= -1)); 
+  test_assert("gteq_vec_range1",    (0xf >= -1));
+  test_assert("gteq_vec_range2", not(0xf >= 1));
+
+  test_assert("gteq_range_vec0",    ( 1 >= 0xf));
+  test_assert("gteq_range_vec1",    (-1 >= 0xf));
+  test_assert("gteq_range_vec2", not(-1 >= 0x1));*)
+
+  (* XXX missing implementations
+  test_assert("gteq_unsigned0",    ( 1 >=_u -1));
+  test_assert("gteq_unsigned1", not(-1 >=_u -1));
+  test_assert("gteq_unsigned2", not(-1 >=_u  1)); *)
+
+  (* XXX missing
+  test_assert("gteq_unsigned_vec0", not(0x1 >=_u 0xf));
+  test_assert("gteq_unsigned_vec1", not(0xf >=_u 0xf));
+  test_assert("gteq_unsigned_vec2",    (0xf >=_u 0x1)); *)
+
+  (* NB there is no gteq_vec_range unsigned or signed *)
+
+  (* XXX missing implementations 
+  test_assert("gteq_signed0",    ( 1 >=_s -1));
+  test_assert("gteq_signed1", not(-1 >=_s -1));
+  test_assert("gteq_signed2", not(-1 >=_s  1)); *)
+
+  test_assert("gteq_vec_signed0",    (0x1 >=_s 0xf));
+  test_assert("gteq_vec_signed1",    (0xf >=_s 0xf));
+  test_assert("gteq_vec_signed2", not(0xf >=_s 0x1));
+}
+
+function unit test_oddments () = {
+  (* XXX this is weird, wrong type?
+  test_assert("is_one0", not(is_one(bitzero)));
+  test_assert("is_one1", is_one(bitone)); *)
+
+  test_assert("signed-1", signed(0xf) == -1);
+  test_assert("signed0",  signed(0x0) == 0);
+  test_assert("signed1",  signed(0x1) == 1);
+
+  test_assert("unsigned-1", unsigned(0xf) == 15);
+  test_assert("unsigned0",  unsigned(0x0) == 0);
+  test_assert("unsigned1",  unsigned(0x1) == 1);
+}
 
 function (bit[64]) run ((bit[64]) x) = {
   test_not();
@@ -259,7 +595,18 @@ function (bit[64]) run ((bit[64]) x) = {
   test_minus();
   test_minus_signed();
   test_multiply();
+  test_mod();
+  test_mod_signed();
   test_div();
+  test_quot_signed();
+  test_misc();
+  test_eq();
+  test_neq();
+  test_lt();
+  test_gt();
+  test_lteq();
+  test_gteq();
+  test_oddments();
   return 0;
 }