Ressurect builtin tests, and add parallel test runner script

Add new python test runner script, which allows tests to be run in
parallel before collecting the results. This makes the tests run a lot
faster, especially for the builtins and C compilation tests. Also
handles reporting errors mushc more nicely than the previous way of
doing it in shell script.

1 files changed, 57 insertions, 61 deletions

diff --git a/test/builtins/signed.sail b/test/builtins/signed.sail
index 21524e2f..73bf9e25 100644
--- a/test/builtins/signed.sail
+++ b/test/builtins/signed.sail
@@ -3,11 +3,7 @@ default Order dec
 $include <exception_basic.sail>
 $include <vector_dec.sail>
 
-val int_of_string = {
-  ocaml: "Nat_big_num.of_string",
-  lem: "integerOfString",
-  c: "reinit_mpz_t_of_sail_string"
-} : string -> int
+overload zero_extend = {sail_zero_extend}
 
 function main (() : unit) -> unit = {
   assert(signed(zero_extend(0x0, 32)) == 0);
@@ -1358,8 +1354,8 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0x5a5a, 64)) == 23130);
   assert(signed(zero_extend(0x5a5a5a59, 64)) == 1515870809);
   assert(signed(zero_extend(0x5a5a5a5a, 64)) == 1515870810);
-  assert(signed(zero_extend(0x5a5a5a5a5a5a5a59, 64)) == int_of_string("6510615555426900569"));
-  assert(signed(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == int_of_string("6510615555426900570"));
+  assert(signed(zero_extend(0x5a5a5a5a5a5a5a59, 64)) == 6510615555426900569);
+  assert(signed(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == 6510615555426900570);
   assert(signed(zero_extend(0x5b, 64)) == 91);
   assert(signed(zero_extend(0x5c, 64)) == 92);
   assert(signed(zero_extend(0x5c000, 64)) == 376832);
@@ -1404,10 +1400,10 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0x6c, 64)) == 108);
   assert(signed(zero_extend(0x6d, 64)) == 109);
   assert(signed(zero_extend(0x6e, 64)) == 110);
-  assert(signed(zero_extend(0x6ede4cbc6ede4cbb, 64)) == int_of_string("7988907161199463611"));
+  assert(signed(zero_extend(0x6ede4cbc6ede4cbb, 64)) == 7988907161199463611);
   assert(signed(zero_extend(0x6f, 64)) == 111);
-  assert(signed(zero_extend(0x6ffffffffffffffe, 64)) == int_of_string("8070450532247928830"));
-  assert(signed(zero_extend(0x6fffffffffffffff, 64)) == int_of_string("8070450532247928831"));
+  assert(signed(zero_extend(0x6ffffffffffffffe, 64)) == 8070450532247928830);
+  assert(signed(zero_extend(0x6fffffffffffffff, 64)) == 8070450532247928831);
   assert(signed(zero_extend(0x7, 64)) == 7);
   assert(signed(zero_extend(0x70, 64)) == 112);
   assert(signed(zero_extend(0x71, 64)) == 113);
@@ -1418,10 +1414,10 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0x76, 64)) == 118);
   assert(signed(zero_extend(0x764c321, 64)) == 124044065);
   assert(signed(zero_extend(0x77, 64)) == 119);
-  assert(signed(zero_extend(0x7765554377655542, 64)) == int_of_string("8603376411415500098"));
-  assert(signed(zero_extend(0x7766554477665542, 64)) == int_of_string("8603657890687243586"));
+  assert(signed(zero_extend(0x7765554377655542, 64)) == 8603376411415500098);
+  assert(signed(zero_extend(0x7766554477665542, 64)) == 8603657890687243586);
   assert(signed(zero_extend(0x78, 64)) == 120);
-  assert(signed(zero_extend(0x789abcdef0123456, 64)) == int_of_string("8690466096661279830"));
+  assert(signed(zero_extend(0x789abcdef0123456, 64)) == 8690466096661279830);
   assert(signed(zero_extend(0x79, 64)) == 121);
   assert(signed(zero_extend(0x7a, 64)) == 122);
   assert(signed(zero_extend(0x7b, 64)) == 123);
@@ -1434,54 +1430,54 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0x7ffe, 64)) == 32766);
   assert(signed(zero_extend(0x7fff, 64)) == 32767);
   assert(signed(zero_extend(0x7fff7fff, 64)) == 2147450879);
-  assert(signed(zero_extend(0x7fff7fff7fff7ffd, 64)) == int_of_string("9223231297218904061"));
-  assert(signed(zero_extend(0x7fff7fff7fff7fff, 64)) == int_of_string("9223231297218904063"));
+  assert(signed(zero_extend(0x7fff7fff7fff7ffd, 64)) == 9223231297218904061);
+  assert(signed(zero_extend(0x7fff7fff7fff7fff, 64)) == 9223231297218904063);
   assert(signed(zero_extend(0x7fffffc, 64)) == 134217724);
   assert(signed(zero_extend(0x7ffffffe, 64)) == 2147483646);
   assert(signed(zero_extend(0x7fffffff, 64)) == 2147483647);
-  assert(signed(zero_extend(0x7fffffff00000000, 64)) == int_of_string("9223372032559808512"));
-  assert(signed(zero_extend(0x7fffffff00000001, 64)) == int_of_string("9223372032559808513"));
-  assert(signed(zero_extend(0x7fffffff7ffffffe, 64)) == int_of_string("9223372034707292158"));
-  assert(signed(zero_extend(0x7fffffff7fffffff, 64)) == int_of_string("9223372034707292159"));
-  assert(signed(zero_extend(0x7fffffff80000000, 64)) == int_of_string("9223372034707292160"));
-  assert(signed(zero_extend(0x7fffffff80000001, 64)) == int_of_string("9223372034707292161"));
-  assert(signed(zero_extend(0x7fffffffffff0000, 64)) == int_of_string("9223372036854710272"));
-  assert(signed(zero_extend(0x7fffffffffff0001, 64)) == int_of_string("9223372036854710273"));
-  assert(signed(zero_extend(0x7fffffffffff7ffe, 64)) == int_of_string("9223372036854743038"));
-  assert(signed(zero_extend(0x7fffffffffff7fff, 64)) == int_of_string("9223372036854743039"));
-  assert(signed(zero_extend(0x7fffffffffff8000, 64)) == int_of_string("9223372036854743040"));
-  assert(signed(zero_extend(0x7fffffffffff8001, 64)) == int_of_string("9223372036854743041"));
-  assert(signed(zero_extend(0x7ffffffffffffffc, 64)) == int_of_string("9223372036854775804"));
-  assert(signed(zero_extend(0x7ffffffffffffffd, 64)) == int_of_string("9223372036854775805"));
-  assert(signed(zero_extend(0x7ffffffffffffffe, 64)) == int_of_string("9223372036854775806"));
-  assert(signed(zero_extend(0x7fffffffffffffff, 64)) == int_of_string("9223372036854775807"));
+  assert(signed(zero_extend(0x7fffffff00000000, 64)) == 9223372032559808512);
+  assert(signed(zero_extend(0x7fffffff00000001, 64)) == 9223372032559808513);
+  assert(signed(zero_extend(0x7fffffff7ffffffe, 64)) == 9223372034707292158);
+  assert(signed(zero_extend(0x7fffffff7fffffff, 64)) == 9223372034707292159);
+  assert(signed(zero_extend(0x7fffffff80000000, 64)) == 9223372034707292160);
+  assert(signed(zero_extend(0x7fffffff80000001, 64)) == 9223372034707292161);
+  assert(signed(zero_extend(0x7fffffffffff0000, 64)) == 9223372036854710272);
+  assert(signed(zero_extend(0x7fffffffffff0001, 64)) == 9223372036854710273);
+  assert(signed(zero_extend(0x7fffffffffff7ffe, 64)) == 9223372036854743038);
+  assert(signed(zero_extend(0x7fffffffffff7fff, 64)) == 9223372036854743039);
+  assert(signed(zero_extend(0x7fffffffffff8000, 64)) == 9223372036854743040);
+  assert(signed(zero_extend(0x7fffffffffff8001, 64)) == 9223372036854743041);
+  assert(signed(zero_extend(0x7ffffffffffffffc, 64)) == 9223372036854775804);
+  assert(signed(zero_extend(0x7ffffffffffffffd, 64)) == 9223372036854775805);
+  assert(signed(zero_extend(0x7ffffffffffffffe, 64)) == 9223372036854775806);
+  assert(signed(zero_extend(0x7fffffffffffffff, 64)) == 9223372036854775807);
   assert(signed(zero_extend(0x8, 64)) == 8);
   assert(signed(zero_extend(0x80, 64)) == 128);
   assert(signed(zero_extend(0x800, 64)) == 2048);
   assert(signed(zero_extend(0x8000, 64)) == 32768);
   assert(signed(zero_extend(0x80000000, 64)) == 2147483648);
-  assert(signed(zero_extend(0x8000000000000000, 64)) == int_of_string("-9223372036854775808"));
-  assert(signed(zero_extend(0x8000000000000001, 64)) == int_of_string("-9223372036854775807"));
-  assert(signed(zero_extend(0x8000000000000002, 64)) == int_of_string("-9223372036854775806"));
-  assert(signed(zero_extend(0x8000000000000003, 64)) == int_of_string("-9223372036854775805"));
-  assert(signed(zero_extend(0x8000000000007ffe, 64)) == int_of_string("-9223372036854743042"));
-  assert(signed(zero_extend(0x8000000000007fff, 64)) == int_of_string("-9223372036854743041"));
-  assert(signed(zero_extend(0x8000000000008000, 64)) == int_of_string("-9223372036854743040"));
-  assert(signed(zero_extend(0x8000000000008001, 64)) == int_of_string("-9223372036854743039"));
-  assert(signed(zero_extend(0x800000000000fffe, 64)) == int_of_string("-9223372036854710274"));
-  assert(signed(zero_extend(0x800000000000ffff, 64)) == int_of_string("-9223372036854710273"));
-  assert(signed(zero_extend(0x800000007ffffffe, 64)) == int_of_string("-9223372034707292162"));
-  assert(signed(zero_extend(0x800000007fffffff, 64)) == int_of_string("-9223372034707292161"));
-  assert(signed(zero_extend(0x8000000080000000, 64)) == int_of_string("-9223372034707292160"));
-  assert(signed(zero_extend(0x8000000080000001, 64)) == int_of_string("-9223372034707292159"));
-  assert(signed(zero_extend(0x80000000fffffffe, 64)) == int_of_string("-9223372032559808514"));
-  assert(signed(zero_extend(0x80000000ffffffff, 64)) == int_of_string("-9223372032559808513"));
+  assert(signed(zero_extend(0x8000000000000000, 64)) == -9223372036854775808);
+  assert(signed(zero_extend(0x8000000000000001, 64)) == -9223372036854775807);
+  assert(signed(zero_extend(0x8000000000000002, 64)) == -9223372036854775806);
+  assert(signed(zero_extend(0x8000000000000003, 64)) == -9223372036854775805);
+  assert(signed(zero_extend(0x8000000000007ffe, 64)) == -9223372036854743042);
+  assert(signed(zero_extend(0x8000000000007fff, 64)) == -9223372036854743041);
+  assert(signed(zero_extend(0x8000000000008000, 64)) == -9223372036854743040);
+  assert(signed(zero_extend(0x8000000000008001, 64)) == -9223372036854743039);
+  assert(signed(zero_extend(0x800000000000fffe, 64)) == -9223372036854710274);
+  assert(signed(zero_extend(0x800000000000ffff, 64)) == -9223372036854710273);
+  assert(signed(zero_extend(0x800000007ffffffe, 64)) == -9223372034707292162);
+  assert(signed(zero_extend(0x800000007fffffff, 64)) == -9223372034707292161);
+  assert(signed(zero_extend(0x8000000080000000, 64)) == -9223372034707292160);
+  assert(signed(zero_extend(0x8000000080000001, 64)) == -9223372034707292159);
+  assert(signed(zero_extend(0x80000000fffffffe, 64)) == -9223372032559808514);
+  assert(signed(zero_extend(0x80000000ffffffff, 64)) == -9223372032559808513);
   assert(signed(zero_extend(0x80000001, 64)) == 2147483649);
   assert(signed(zero_extend(0x80000002, 64)) == 2147483650);
   assert(signed(zero_extend(0x80000003, 64)) == 2147483651);
   assert(signed(zero_extend(0x80008000, 64)) == 2147516416);
-  assert(signed(zero_extend(0x8000800080008000, 64)) == int_of_string("-9223231297218904064"));
-  assert(signed(zero_extend(0x8000800080008002, 64)) == int_of_string("-9223231297218904062"));
+  assert(signed(zero_extend(0x8000800080008000, 64)) == -9223231297218904064);
+  assert(signed(zero_extend(0x8000800080008002, 64)) == -9223231297218904062);
   assert(signed(zero_extend(0x8001, 64)) == 32769);
   assert(signed(zero_extend(0x80010003, 64)) == 2147549187);
   assert(signed(zero_extend(0x8002, 64)) == 32770);
@@ -1509,26 +1505,26 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0x86, 64)) == 134);
   assert(signed(zero_extend(0x87, 64)) == 135);
   assert(signed(zero_extend(0x87654321, 64)) == 2271560481);
-  assert(signed(zero_extend(0x876543210fedcba9, 64)) == int_of_string("-8690466096661279831"));
+  assert(signed(zero_extend(0x876543210fedcba9, 64)) == -8690466096661279831);
   assert(signed(zero_extend(0x88, 64)) == 136);
   assert(signed(zero_extend(0x8899aabb, 64)) == 2291772091);
-  assert(signed(zero_extend(0x8899aabb8899aabb, 64)) == int_of_string("-8603657890687243589"));
-  assert(signed(zero_extend(0x8899aabb8899aabd, 64)) == int_of_string("-8603657890687243587"));
-  assert(signed(zero_extend(0x889aaabc889aaabd, 64)) == int_of_string("-8603376411415500099"));
+  assert(signed(zero_extend(0x8899aabb8899aabb, 64)) == -8603657890687243589);
+  assert(signed(zero_extend(0x8899aabb8899aabd, 64)) == -8603657890687243587);
+  assert(signed(zero_extend(0x889aaabc889aaabd, 64)) == -8603376411415500099);
   assert(signed(zero_extend(0x89, 64)) == 137);
   assert(signed(zero_extend(0x89ab, 64)) == 35243);
   assert(signed(zero_extend(0x8a, 64)) == 138);
   assert(signed(zero_extend(0x8b, 64)) == 139);
   assert(signed(zero_extend(0x8c, 64)) == 140);
   assert(signed(zero_extend(0x8d, 64)) == 141);
-  assert(signed(zero_extend(0x8fffffffffffffff, 64)) == int_of_string("-8070450532247928833"));
+  assert(signed(zero_extend(0x8fffffffffffffff, 64)) == -8070450532247928833);
   assert(signed(zero_extend(0x9, 64)) == 9);
   assert(signed(zero_extend(0x90, 64)) == 144);
   assert(signed(zero_extend(0x90000000, 64)) == 2415919104);
-  assert(signed(zero_extend(0x9000000000000000, 64)) == int_of_string("-8070450532247928832"));
-  assert(signed(zero_extend(0x9000000000000001, 64)) == int_of_string("-8070450532247928831"));
+  assert(signed(zero_extend(0x9000000000000000, 64)) == -8070450532247928832);
+  assert(signed(zero_extend(0x9000000000000001, 64)) == -8070450532247928831);
   assert(signed(zero_extend(0x90000001, 64)) == 2415919105);
-  assert(signed(zero_extend(0x9121b3439121b344, 64)) == int_of_string("-7988907161199463612"));
+  assert(signed(zero_extend(0x9121b3439121b344, 64)) == -7988907161199463612);
   assert(signed(zero_extend(0x9200040, 64)) == 153092160);
   assert(signed(zero_extend(0x920005c, 64)) == 153092188);
   assert(signed(zero_extend(0x9200060, 64)) == 153092192);
@@ -1546,7 +1542,7 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0xa500074, 64)) == 173015156);
   assert(signed(zero_extend(0xa5a5, 64)) == 42405);
   assert(signed(zero_extend(0xa5a5a5a5, 64)) == 2779096485);
-  assert(signed(zero_extend(0xa5a5a5a5a5a5a5a5, 64)) == int_of_string("-6510615555426900571"));
+  assert(signed(zero_extend(0xa5a5a5a5a5a5a5a5, 64)) == -6510615555426900571);
   assert(signed(zero_extend(0xa8, 64)) == 168);
   assert(signed(zero_extend(0xb, 64)) == 11);
   assert(signed(zero_extend(0xb0, 64)) == 176);
@@ -1556,13 +1552,13 @@ function main (() : unit) -> unit = {
   assert(signed(zero_extend(0xc00fefff, 64)) == 3222269951);
   assert(signed(zero_extend(0xd, 64)) == 13);
   assert(signed(zero_extend(0xd0, 64)) == 208);
-  assert(signed(zero_extend(0xdddddddddddddddc, 64)) == int_of_string("-2459565876494606884"));
+  assert(signed(zero_extend(0xdddddddddddddddc, 64)) == -2459565876494606884);
   assert(signed(zero_extend(0xe, 64)) == 14);
   assert(signed(zero_extend(0xe0, 64)) == 224);
-  assert(signed(zero_extend(0xedcba9876543210e, 64)) == int_of_string("-1311768467463790322"));
+  assert(signed(zero_extend(0xedcba9876543210e, 64)) == -1311768467463790322);
   assert(signed(zero_extend(0xf, 64)) == 15);
   assert(signed(zero_extend(0xf00, 64)) == 3840);
-  assert(signed(zero_extend(0xf000000000000000, 64)) == int_of_string("-1152921504606846976"));
+  assert(signed(zero_extend(0xf000000000000000, 64)) == -1152921504606846976);
   assert(signed(zero_extend(0xff, 64)) == 255);
   assert(signed(zero_extend(0xfffe, 64)) == 65534);
   assert(signed(zero_extend(0xffff, 64)) == 65535);