diff options
| -rw-r--r-- | test/builtins/get_slice_int.sail | 34 | ||||
| -rwxr-xr-x | test/builtins/run_tests.py | 38 | ||||
| -rw-r--r-- | test/builtins/signed.sail | 118 | ||||
| -rw-r--r-- | test/builtins/unsigned2.sail | 2 | ||||
| -rw-r--r-- | test/builtins/unsigned4.sail | 2 | ||||
| -rw-r--r-- | test/builtins/unsigned5.sail | 2 | ||||
| -rw-r--r-- | test/builtins/unsigned6.sail | 392 | ||||
| -rw-r--r-- | test/builtins/zeros.sail | 2 | ||||
| -rwxr-xr-x | test/c/run_tests.py | 42 | ||||
| -rw-r--r-- | test/sailtest.py | 51 |
10 files changed, 404 insertions, 279 deletions
diff --git a/test/builtins/get_slice_int.sail b/test/builtins/get_slice_int.sail index 73c495fa..b64526d2 100644 --- a/test/builtins/get_slice_int.sail +++ b/test/builtins/get_slice_int.sail @@ -4,12 +4,6 @@ $include <exception_basic.sail> $include <flow.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 - function main (() : unit) -> unit = { assert(get_slice_int(1, -10, 6) == 1^0x1, "get_slice_int(1, -10, 6) == 1^0x1"); assert(get_slice_int(1, -1, 6) == 1^0x1, "get_slice_int(1, -1, 6) == 1^0x1"); @@ -257,20 +251,20 @@ function main (() : unit) -> unit = { assert(get_slice_int(64, 173015152, 0) == 64^0xa500070, "get_slice_int(64, 173015152, 0) == 64^0xa500070"); assert(get_slice_int(64, 173015156, 0) == 64^0xa500074, "get_slice_int(64, 173015156, 0) == 64^0xa500074"); assert(get_slice_int(64, 180224, 0) == 64^0x2c000, "get_slice_int(64, 180224, 0) == 64^0x2c000"); - assert(get_slice_int(64, int_of_string("18446708893632421888"), 0) == 64^0xffffe000ffffe000, "get_slice_int(64, 18446708893632421888, 0) == 64^0xffffe000ffffe000"); - assert(get_slice_int(64, int_of_string("18446744073658712064"), 0) == 64^0xfffffffffcf84000, "get_slice_int(64, 18446744073658712064, 0) == 64^0xfffffffffcf84000"); - assert(get_slice_int(64, int_of_string("18446744073658777600"), 0) == 64^0xfffffffffcf94000, "get_slice_int(64, 18446744073658777600, 0) == 64^0xfffffffffcf94000"); - assert(get_slice_int(64, int_of_string("18446744073658843136"), 0) == 64^0xfffffffffcfa4000, "get_slice_int(64, 18446744073658843136, 0) == 64^0xfffffffffcfa4000"); - assert(get_slice_int(64, int_of_string("18446744073660252160"), 0) == 64^0xfffffffffd0fc000, "get_slice_int(64, 18446744073660252160, 0) == 64^0xfffffffffd0fc000"); - assert(get_slice_int(64, int_of_string("18446744073660317696"), 0) == 64^0xfffffffffd10c000, "get_slice_int(64, 18446744073660317696, 0) == 64^0xfffffffffd10c000"); - assert(get_slice_int(64, int_of_string("18446744073660465152"), 0) == 64^0xfffffffffd130000, "get_slice_int(64, 18446744073660465152, 0) == 64^0xfffffffffd130000"); - assert(get_slice_int(64, int_of_string("18446744073660530688"), 0) == 64^0xfffffffffd140000, "get_slice_int(64, 18446744073660530688, 0) == 64^0xfffffffffd140000"); - assert(get_slice_int(64, int_of_string("18446744073660727296"), 0) == 64^0xfffffffffd170000, "get_slice_int(64, 18446744073660727296, 0) == 64^0xfffffffffd170000"); - assert(get_slice_int(64, int_of_string("18446744073660841984"), 0) == 64^0xfffffffffd18c000, "get_slice_int(64, 18446744073660841984, 0) == 64^0xfffffffffd18c000"); - assert(get_slice_int(64, int_of_string("18446744073708961792"), 0) == 64^0xfffffffffff70000, "get_slice_int(64, 18446744073708961792, 0) == 64^0xfffffffffff70000"); - assert(get_slice_int(64, int_of_string("18446744073709027328"), 0) == 64^0xfffffffffff80000, "get_slice_int(64, 18446744073709027328, 0) == 64^0xfffffffffff80000"); - assert(get_slice_int(64, int_of_string("18446744073709289472"), 0) == 64^0xfffffffffffc0000, "get_slice_int(64, 18446744073709289472, 0) == 64^0xfffffffffffc0000"); - assert(get_slice_int(64, int_of_string("18446744073709355008"), 0) == 64^0xfffffffffffd0000, "get_slice_int(64, 18446744073709355008, 0) == 64^0xfffffffffffd0000"); + assert(get_slice_int(64, 18446708893632421888, 0) == 64^0xffffe000ffffe000, "get_slice_int(64, 18446708893632421888, 0) == 64^0xffffe000ffffe000"); + assert(get_slice_int(64, 18446744073658712064, 0) == 64^0xfffffffffcf84000, "get_slice_int(64, 18446744073658712064, 0) == 64^0xfffffffffcf84000"); + assert(get_slice_int(64, 18446744073658777600, 0) == 64^0xfffffffffcf94000, "get_slice_int(64, 18446744073658777600, 0) == 64^0xfffffffffcf94000"); + assert(get_slice_int(64, 18446744073658843136, 0) == 64^0xfffffffffcfa4000, "get_slice_int(64, 18446744073658843136, 0) == 64^0xfffffffffcfa4000"); + assert(get_slice_int(64, 18446744073660252160, 0) == 64^0xfffffffffd0fc000, "get_slice_int(64, 18446744073660252160, 0) == 64^0xfffffffffd0fc000"); + assert(get_slice_int(64, 18446744073660317696, 0) == 64^0xfffffffffd10c000, "get_slice_int(64, 18446744073660317696, 0) == 64^0xfffffffffd10c000"); + assert(get_slice_int(64, 18446744073660465152, 0) == 64^0xfffffffffd130000, "get_slice_int(64, 18446744073660465152, 0) == 64^0xfffffffffd130000"); + assert(get_slice_int(64, 18446744073660530688, 0) == 64^0xfffffffffd140000, "get_slice_int(64, 18446744073660530688, 0) == 64^0xfffffffffd140000"); + assert(get_slice_int(64, 18446744073660727296, 0) == 64^0xfffffffffd170000, "get_slice_int(64, 18446744073660727296, 0) == 64^0xfffffffffd170000"); + assert(get_slice_int(64, 18446744073660841984, 0) == 64^0xfffffffffd18c000, "get_slice_int(64, 18446744073660841984, 0) == 64^0xfffffffffd18c000"); + assert(get_slice_int(64, 18446744073708961792, 0) == 64^0xfffffffffff70000, "get_slice_int(64, 18446744073708961792, 0) == 64^0xfffffffffff70000"); + assert(get_slice_int(64, 18446744073709027328, 0) == 64^0xfffffffffff80000, "get_slice_int(64, 18446744073709027328, 0) == 64^0xfffffffffff80000"); + assert(get_slice_int(64, 18446744073709289472, 0) == 64^0xfffffffffffc0000, "get_slice_int(64, 18446744073709289472, 0) == 64^0xfffffffffffc0000"); + assert(get_slice_int(64, 18446744073709355008, 0) == 64^0xfffffffffffd0000, "get_slice_int(64, 18446744073709355008, 0) == 64^0xfffffffffffd0000"); assert(get_slice_int(64, 75248, 0) == 64^0x125f0, "get_slice_int(64, 75248, 0) == 64^0x125f0"); assert(get_slice_int(64, 75252, 0) == 64^0x125f4, "get_slice_int(64, 75252, 0) == 64^0x125f4"); assert(get_slice_int(64, 75256, 0) == 64^0x125f8, "get_slice_int(64, 75256, 0) == 64^0x125f8"); diff --git a/test/builtins/run_tests.py b/test/builtins/run_tests.py new file mode 100755 index 00000000..1561712c --- /dev/null +++ b/test/builtins/run_tests.py @@ -0,0 +1,38 @@ +#!/usr/bin/env python + +import os +import re +import sys +import hashlib + +sail_dir = os.environ['SAIL_DIR'] +os.chdir(os.path.dirname(__file__)) +sys.path.insert(0, os.path.join(sail_dir, 'test')) + +from sailtest import * + +def test_builtins(name, sail_opts): + banner('Testing builtins: {} Sail options: {}'.format(name, sail_opts)) + tests = {} + for filename in os.listdir('.'): + if re.match('.+\.sail', filename): + basename = os.path.splitext(os.path.basename(filename))[0] + tests[filename] = os.fork() + if tests[filename] == 0: + step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename)) + step('gcc {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(basename, sail_dir, sail_dir, basename)) + step('./{}'.format(basename)) + print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) + sys.exit() + return collect_results(name, tests) + +xml = '<testsuites>\n' + +test_builtins('No optimisations', '') +test_builtins('Optimisations', '-O') + +xml += '</testsuites>\n' + +output = open('tests.xml', 'w') +output.write(xml) +output.close() 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); diff --git a/test/builtins/unsigned2.sail b/test/builtins/unsigned2.sail index dea6d9c5..9d0482b3 100644 --- a/test/builtins/unsigned2.sail +++ b/test/builtins/unsigned2.sail @@ -3,6 +3,8 @@ default Order dec $include <exception_basic.sail> $include <vector_dec.sail> +overload zero_extend = {sail_zero_extend} + function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x21ad18, 52)) == 2207000); assert(unsigned(zero_extend(0x21ad1c, 52)) == 2207004); diff --git a/test/builtins/unsigned4.sail b/test/builtins/unsigned4.sail index c92e568f..5736d671 100644 --- a/test/builtins/unsigned4.sail +++ b/test/builtins/unsigned4.sail @@ -3,6 +3,8 @@ default Order dec $include <exception_basic.sail> $include <vector_dec.sail> +overload zero_extend = {sail_zero_extend} + function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x104ef4, 64)) == 1068788); assert(unsigned(zero_extend(0x104ef8, 64)) == 1068792); diff --git a/test/builtins/unsigned5.sail b/test/builtins/unsigned5.sail index 5c6a181a..6e1be59c 100644 --- a/test/builtins/unsigned5.sail +++ b/test/builtins/unsigned5.sail @@ -3,6 +3,8 @@ default Order dec $include <exception_basic.sail> $include <vector_dec.sail> +overload zero_extend = {sail_zero_extend} + function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x1cdf8, 64)) == 118264); assert(unsigned(zero_extend(0x1cdfc, 64)) == 118268); diff --git a/test/builtins/unsigned6.sail b/test/builtins/unsigned6.sail index ec2635d6..0f0d884a 100644 --- a/test/builtins/unsigned6.sail +++ b/test/builtins/unsigned6.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(unsigned(zero_extend(0x2e015f0, 64)) == 48240112); @@ -2063,8 +2059,8 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x5a5a, 64)) == 23130); assert(unsigned(zero_extend(0x5a5a5a59, 64)) == 1515870809); assert(unsigned(zero_extend(0x5a5a5a5a, 64)) == 1515870810); - assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a59, 64)) == int_of_string("6510615555426900569")); - assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == int_of_string("6510615555426900570")); + assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a59, 64)) == 6510615555426900569); + assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == 6510615555426900570); assert(unsigned(zero_extend(0x5b, 64)) == 91); assert(unsigned(zero_extend(0x5c, 64)) == 92); assert(unsigned(zero_extend(0x5c000, 64)) == 376832); @@ -2153,10 +2149,10 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x6c, 64)) == 108); assert(unsigned(zero_extend(0x6d, 64)) == 109); assert(unsigned(zero_extend(0x6e, 64)) == 110); - assert(unsigned(zero_extend(0x6ede4cbc6ede4cbb, 64)) == int_of_string("7988907161199463611")); + assert(unsigned(zero_extend(0x6ede4cbc6ede4cbb, 64)) == 7988907161199463611); assert(unsigned(zero_extend(0x6f, 64)) == 111); - assert(unsigned(zero_extend(0x6ffffffffffffffe, 64)) == int_of_string("8070450532247928830")); - assert(unsigned(zero_extend(0x6fffffffffffffff, 64)) == int_of_string("8070450532247928831")); + assert(unsigned(zero_extend(0x6ffffffffffffffe, 64)) == 8070450532247928830); + assert(unsigned(zero_extend(0x6fffffffffffffff, 64)) == 8070450532247928831); assert(unsigned(zero_extend(0x7, 64)) == 7); assert(unsigned(zero_extend(0x70, 64)) == 112); assert(unsigned(zero_extend(0x71, 64)) == 113); @@ -2167,10 +2163,10 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x76, 64)) == 118); assert(unsigned(zero_extend(0x764c321, 64)) == 124044065); assert(unsigned(zero_extend(0x77, 64)) == 119); - assert(unsigned(zero_extend(0x7765554377655542, 64)) == int_of_string("8603376411415500098")); - assert(unsigned(zero_extend(0x7766554477665542, 64)) == int_of_string("8603657890687243586")); + assert(unsigned(zero_extend(0x7765554377655542, 64)) == 8603376411415500098); + assert(unsigned(zero_extend(0x7766554477665542, 64)) == 8603657890687243586); assert(unsigned(zero_extend(0x78, 64)) == 120); - assert(unsigned(zero_extend(0x789abcdef0123456, 64)) == int_of_string("8690466096661279830")); + assert(unsigned(zero_extend(0x789abcdef0123456, 64)) == 8690466096661279830); assert(unsigned(zero_extend(0x79, 64)) == 121); assert(unsigned(zero_extend(0x7a, 64)) == 122); assert(unsigned(zero_extend(0x7b, 64)) == 123); @@ -2183,54 +2179,54 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x7ffe, 64)) == 32766); assert(unsigned(zero_extend(0x7fff, 64)) == 32767); assert(unsigned(zero_extend(0x7fff7fff, 64)) == 2147450879); - assert(unsigned(zero_extend(0x7fff7fff7fff7ffd, 64)) == int_of_string("9223231297218904061")); - assert(unsigned(zero_extend(0x7fff7fff7fff7fff, 64)) == int_of_string("9223231297218904063")); + assert(unsigned(zero_extend(0x7fff7fff7fff7ffd, 64)) == 9223231297218904061); + assert(unsigned(zero_extend(0x7fff7fff7fff7fff, 64)) == 9223231297218904063); assert(unsigned(zero_extend(0x7fffffc, 64)) == 134217724); assert(unsigned(zero_extend(0x7ffffffe, 64)) == 2147483646); assert(unsigned(zero_extend(0x7fffffff, 64)) == 2147483647); - assert(unsigned(zero_extend(0x7fffffff00000000, 64)) == int_of_string("9223372032559808512")); - assert(unsigned(zero_extend(0x7fffffff00000001, 64)) == int_of_string("9223372032559808513")); - assert(unsigned(zero_extend(0x7fffffff7ffffffe, 64)) == int_of_string("9223372034707292158")); - assert(unsigned(zero_extend(0x7fffffff7fffffff, 64)) == int_of_string("9223372034707292159")); - assert(unsigned(zero_extend(0x7fffffff80000000, 64)) == int_of_string("9223372034707292160")); - assert(unsigned(zero_extend(0x7fffffff80000001, 64)) == int_of_string("9223372034707292161")); - assert(unsigned(zero_extend(0x7fffffffffff0000, 64)) == int_of_string("9223372036854710272")); - assert(unsigned(zero_extend(0x7fffffffffff0001, 64)) == int_of_string("9223372036854710273")); - assert(unsigned(zero_extend(0x7fffffffffff7ffe, 64)) == int_of_string("9223372036854743038")); - assert(unsigned(zero_extend(0x7fffffffffff7fff, 64)) == int_of_string("9223372036854743039")); - assert(unsigned(zero_extend(0x7fffffffffff8000, 64)) == int_of_string("9223372036854743040")); - assert(unsigned(zero_extend(0x7fffffffffff8001, 64)) == int_of_string("9223372036854743041")); - assert(unsigned(zero_extend(0x7ffffffffffffffc, 64)) == int_of_string("9223372036854775804")); - assert(unsigned(zero_extend(0x7ffffffffffffffd, 64)) == int_of_string("9223372036854775805")); - assert(unsigned(zero_extend(0x7ffffffffffffffe, 64)) == int_of_string("9223372036854775806")); - assert(unsigned(zero_extend(0x7fffffffffffffff, 64)) == int_of_string("9223372036854775807")); + assert(unsigned(zero_extend(0x7fffffff00000000, 64)) == 9223372032559808512); + assert(unsigned(zero_extend(0x7fffffff00000001, 64)) == 9223372032559808513); + assert(unsigned(zero_extend(0x7fffffff7ffffffe, 64)) == 9223372034707292158); + assert(unsigned(zero_extend(0x7fffffff7fffffff, 64)) == 9223372034707292159); + assert(unsigned(zero_extend(0x7fffffff80000000, 64)) == 9223372034707292160); + assert(unsigned(zero_extend(0x7fffffff80000001, 64)) == 9223372034707292161); + assert(unsigned(zero_extend(0x7fffffffffff0000, 64)) == 9223372036854710272); + assert(unsigned(zero_extend(0x7fffffffffff0001, 64)) == 9223372036854710273); + assert(unsigned(zero_extend(0x7fffffffffff7ffe, 64)) == 9223372036854743038); + assert(unsigned(zero_extend(0x7fffffffffff7fff, 64)) == 9223372036854743039); + assert(unsigned(zero_extend(0x7fffffffffff8000, 64)) == 9223372036854743040); + assert(unsigned(zero_extend(0x7fffffffffff8001, 64)) == 9223372036854743041); + assert(unsigned(zero_extend(0x7ffffffffffffffc, 64)) == 9223372036854775804); + assert(unsigned(zero_extend(0x7ffffffffffffffd, 64)) == 9223372036854775805); + assert(unsigned(zero_extend(0x7ffffffffffffffe, 64)) == 9223372036854775806); + assert(unsigned(zero_extend(0x7fffffffffffffff, 64)) == 9223372036854775807); assert(unsigned(zero_extend(0x8, 64)) == 8); assert(unsigned(zero_extend(0x80, 64)) == 128); assert(unsigned(zero_extend(0x800, 64)) == 2048); assert(unsigned(zero_extend(0x8000, 64)) == 32768); assert(unsigned(zero_extend(0x80000000, 64)) == 2147483648); - assert(unsigned(zero_extend(0x8000000000000000, 64)) == int_of_string("9223372036854775808")); - assert(unsigned(zero_extend(0x8000000000000001, 64)) == int_of_string("9223372036854775809")); - assert(unsigned(zero_extend(0x8000000000000002, 64)) == int_of_string("9223372036854775810")); - assert(unsigned(zero_extend(0x8000000000000003, 64)) == int_of_string("9223372036854775811")); - assert(unsigned(zero_extend(0x8000000000007ffe, 64)) == int_of_string("9223372036854808574")); - assert(unsigned(zero_extend(0x8000000000007fff, 64)) == int_of_string("9223372036854808575")); - assert(unsigned(zero_extend(0x8000000000008000, 64)) == int_of_string("9223372036854808576")); - assert(unsigned(zero_extend(0x8000000000008001, 64)) == int_of_string("9223372036854808577")); - assert(unsigned(zero_extend(0x800000000000fffe, 64)) == int_of_string("9223372036854841342")); - assert(unsigned(zero_extend(0x800000000000ffff, 64)) == int_of_string("9223372036854841343")); - assert(unsigned(zero_extend(0x800000007ffffffe, 64)) == int_of_string("9223372039002259454")); - assert(unsigned(zero_extend(0x800000007fffffff, 64)) == int_of_string("9223372039002259455")); - assert(unsigned(zero_extend(0x8000000080000000, 64)) == int_of_string("9223372039002259456")); - assert(unsigned(zero_extend(0x8000000080000001, 64)) == int_of_string("9223372039002259457")); - assert(unsigned(zero_extend(0x80000000fffffffe, 64)) == int_of_string("9223372041149743102")); - assert(unsigned(zero_extend(0x80000000ffffffff, 64)) == int_of_string("9223372041149743103")); + assert(unsigned(zero_extend(0x8000000000000000, 64)) == 9223372036854775808); + assert(unsigned(zero_extend(0x8000000000000001, 64)) == 9223372036854775809); + assert(unsigned(zero_extend(0x8000000000000002, 64)) == 9223372036854775810); + assert(unsigned(zero_extend(0x8000000000000003, 64)) == 9223372036854775811); + assert(unsigned(zero_extend(0x8000000000007ffe, 64)) == 9223372036854808574); + assert(unsigned(zero_extend(0x8000000000007fff, 64)) == 9223372036854808575); + assert(unsigned(zero_extend(0x8000000000008000, 64)) == 9223372036854808576); + assert(unsigned(zero_extend(0x8000000000008001, 64)) == 9223372036854808577); + assert(unsigned(zero_extend(0x800000000000fffe, 64)) == 9223372036854841342); + assert(unsigned(zero_extend(0x800000000000ffff, 64)) == 9223372036854841343); + assert(unsigned(zero_extend(0x800000007ffffffe, 64)) == 9223372039002259454); + assert(unsigned(zero_extend(0x800000007fffffff, 64)) == 9223372039002259455); + assert(unsigned(zero_extend(0x8000000080000000, 64)) == 9223372039002259456); + assert(unsigned(zero_extend(0x8000000080000001, 64)) == 9223372039002259457); + assert(unsigned(zero_extend(0x80000000fffffffe, 64)) == 9223372041149743102); + assert(unsigned(zero_extend(0x80000000ffffffff, 64)) == 9223372041149743103); assert(unsigned(zero_extend(0x80000001, 64)) == 2147483649); assert(unsigned(zero_extend(0x80000002, 64)) == 2147483650); assert(unsigned(zero_extend(0x80000003, 64)) == 2147483651); assert(unsigned(zero_extend(0x80008000, 64)) == 2147516416); - assert(unsigned(zero_extend(0x8000800080008000, 64)) == int_of_string("9223512776490647552")); - assert(unsigned(zero_extend(0x8000800080008002, 64)) == int_of_string("9223512776490647554")); + assert(unsigned(zero_extend(0x8000800080008000, 64)) == 9223512776490647552); + assert(unsigned(zero_extend(0x8000800080008002, 64)) == 9223512776490647554); assert(unsigned(zero_extend(0x8001, 64)) == 32769); assert(unsigned(zero_extend(0x80010003, 64)) == 2147549187); assert(unsigned(zero_extend(0x8002, 64)) == 32770); @@ -2258,26 +2254,26 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x86, 64)) == 134); assert(unsigned(zero_extend(0x87, 64)) == 135); assert(unsigned(zero_extend(0x87654321, 64)) == 2271560481); - assert(unsigned(zero_extend(0x876543210fedcba9, 64)) == int_of_string("9756277977048271785")); + assert(unsigned(zero_extend(0x876543210fedcba9, 64)) == 9756277977048271785); assert(unsigned(zero_extend(0x88, 64)) == 136); assert(unsigned(zero_extend(0x8899aabb, 64)) == 2291772091); - assert(unsigned(zero_extend(0x8899aabb8899aabb, 64)) == int_of_string("9843086183022308027")); - assert(unsigned(zero_extend(0x8899aabb8899aabd, 64)) == int_of_string("9843086183022308029")); - assert(unsigned(zero_extend(0x889aaabc889aaabd, 64)) == int_of_string("9843367662294051517")); + assert(unsigned(zero_extend(0x8899aabb8899aabb, 64)) == 9843086183022308027); + assert(unsigned(zero_extend(0x8899aabb8899aabd, 64)) == 9843086183022308029); + assert(unsigned(zero_extend(0x889aaabc889aaabd, 64)) == 9843367662294051517); assert(unsigned(zero_extend(0x89, 64)) == 137); assert(unsigned(zero_extend(0x89ab, 64)) == 35243); assert(unsigned(zero_extend(0x8a, 64)) == 138); assert(unsigned(zero_extend(0x8b, 64)) == 139); assert(unsigned(zero_extend(0x8c, 64)) == 140); assert(unsigned(zero_extend(0x8d, 64)) == 141); - assert(unsigned(zero_extend(0x8fffffffffffffff, 64)) == int_of_string("10376293541461622783")); + assert(unsigned(zero_extend(0x8fffffffffffffff, 64)) == 10376293541461622783); assert(unsigned(zero_extend(0x9, 64)) == 9); assert(unsigned(zero_extend(0x90, 64)) == 144); assert(unsigned(zero_extend(0x90000000, 64)) == 2415919104); - assert(unsigned(zero_extend(0x9000000000000000, 64)) == int_of_string("10376293541461622784")); - assert(unsigned(zero_extend(0x9000000000000001, 64)) == int_of_string("10376293541461622785")); + assert(unsigned(zero_extend(0x9000000000000000, 64)) == 10376293541461622784); + assert(unsigned(zero_extend(0x9000000000000001, 64)) == 10376293541461622785); assert(unsigned(zero_extend(0x90000001, 64)) == 2415919105); - assert(unsigned(zero_extend(0x9121b3439121b344, 64)) == int_of_string("10457836912510088004")); + assert(unsigned(zero_extend(0x9121b3439121b344, 64)) == 10457836912510088004); assert(unsigned(zero_extend(0x9200000, 64)) == 153092096); assert(unsigned(zero_extend(0x9200004, 64)) == 153092100); assert(unsigned(zero_extend(0x9200008, 64)) == 153092104); @@ -2361,7 +2357,7 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0xa500074, 64)) == 173015156); assert(unsigned(zero_extend(0xa5a5, 64)) == 42405); assert(unsigned(zero_extend(0xa5a5a5a5, 64)) == 2779096485); - assert(unsigned(zero_extend(0xa5a5a5a5a5a5a5a5, 64)) == int_of_string("11936128518282651045")); + assert(unsigned(zero_extend(0xa5a5a5a5a5a5a5a5, 64)) == 11936128518282651045); assert(unsigned(zero_extend(0xa8, 64)) == 168); assert(unsigned(zero_extend(0xb, 64)) == 11); assert(unsigned(zero_extend(0xb0, 64)) == 176); @@ -2371,160 +2367,160 @@ function main (() : unit) -> unit = { assert(unsigned(zero_extend(0xc00fefff, 64)) == 3222269951); assert(unsigned(zero_extend(0xd, 64)) == 13); assert(unsigned(zero_extend(0xd0, 64)) == 208); - assert(unsigned(zero_extend(0xdddddddddddddddc, 64)) == int_of_string("15987178197214944732")); + assert(unsigned(zero_extend(0xdddddddddddddddc, 64)) == 15987178197214944732); assert(unsigned(zero_extend(0xe, 64)) == 14); assert(unsigned(zero_extend(0xe0, 64)) == 224); - assert(unsigned(zero_extend(0xedcba9876543210e, 64)) == int_of_string("17134975606245761294")); + assert(unsigned(zero_extend(0xedcba9876543210e, 64)) == 17134975606245761294); assert(unsigned(zero_extend(0xf, 64)) == 15); assert(unsigned(zero_extend(0xf00, 64)) == 3840); - assert(unsigned(zero_extend(0xf000000000000000, 64)) == int_of_string("17293822569102704640")); + assert(unsigned(zero_extend(0xf000000000000000, 64)) == 17293822569102704640); assert(unsigned(zero_extend(0xff, 64)) == 255); assert(unsigned(zero_extend(0xfffe, 64)) == 65534); assert(unsigned(zero_extend(0xffff, 64)) == 65535); assert(unsigned(zero_extend(0xffff8000, 64)) == 4294934528); assert(unsigned(zero_extend(0xffffc, 64)) == 1048572); - assert(unsigned(zero_extend(0xffffe000ffffe000, 64)) == int_of_string("18446708893632421888")); + assert(unsigned(zero_extend(0xffffe000ffffe000, 64)) == 18446708893632421888); assert(unsigned(zero_extend(0xfffffff, 64)) == 268435455); assert(unsigned(zero_extend(0xfffffffe, 64)) == 4294967294); - assert(unsigned(zero_extend(0xfffffffe77665544, 64)) == int_of_string("18446744067122812228")); - assert(unsigned(zero_extend(0xfffffffe7fffffff, 64)) == int_of_string("18446744067267100671")); - assert(unsigned(zero_extend(0xfffffffe80000000, 64)) == int_of_string("18446744067267100672")); - assert(unsigned(zero_extend(0xfffffffef89b3cde, 64)) == int_of_string("18446744069290540254")); - assert(unsigned(zero_extend(0xfffffffefffffffe, 64)) == int_of_string("18446744069414584318")); - assert(unsigned(zero_extend(0xfffffffeffffffff, 64)) == int_of_string("18446744069414584319")); + assert(unsigned(zero_extend(0xfffffffe77665544, 64)) == 18446744067122812228); + assert(unsigned(zero_extend(0xfffffffe7fffffff, 64)) == 18446744067267100671); + assert(unsigned(zero_extend(0xfffffffe80000000, 64)) == 18446744067267100672); + assert(unsigned(zero_extend(0xfffffffef89b3cde, 64)) == 18446744069290540254); + assert(unsigned(zero_extend(0xfffffffefffffffe, 64)) == 18446744069414584318); + assert(unsigned(zero_extend(0xfffffffeffffffff, 64)) == 18446744069414584319); assert(unsigned(zero_extend(0xffffffff, 64)) == 4294967295); - assert(unsigned(zero_extend(0xffffffff00000000, 64)) == int_of_string("18446744069414584320")); - assert(unsigned(zero_extend(0xffffffff00000001, 64)) == int_of_string("18446744069414584321")); - assert(unsigned(zero_extend(0xffffffff00007fff, 64)) == int_of_string("18446744069414617087")); - assert(unsigned(zero_extend(0xffffffff3ff01000, 64)) == int_of_string("18446744070487281664")); - assert(unsigned(zero_extend(0xffffffff5fffffff, 64)) == int_of_string("18446744071025197055")); - assert(unsigned(zero_extend(0xffffffff6dcba985, 64)) == int_of_string("18446744071256648069")); - assert(unsigned(zero_extend(0xffffffff6ffffffe, 64)) == int_of_string("18446744071293632510")); - assert(unsigned(zero_extend(0xffffffff6fffffff, 64)) == int_of_string("18446744071293632511")); - assert(unsigned(zero_extend(0xffffffff77665544, 64)) == int_of_string("18446744071417779524")); - assert(unsigned(zero_extend(0xffffffff7ffefffc, 64)) == int_of_string("18446744071562002428")); - assert(unsigned(zero_extend(0xffffffff7ffffffc, 64)) == int_of_string("18446744071562067964")); - assert(unsigned(zero_extend(0xffffffff7ffffffd, 64)) == int_of_string("18446744071562067965")); - assert(unsigned(zero_extend(0xffffffff7ffffffe, 64)) == int_of_string("18446744071562067966")); - assert(unsigned(zero_extend(0xffffffff7fffffff, 64)) == int_of_string("18446744071562067967")); - assert(unsigned(zero_extend(0xffffffff80000000, 64)) == int_of_string("18446744071562067968")); - assert(unsigned(zero_extend(0xffffffff80000001, 64)) == int_of_string("18446744071562067969")); - assert(unsigned(zero_extend(0xffffffff94837260, 64)) == int_of_string("18446744071906226784")); - assert(unsigned(zero_extend(0xffffffffdfffffff, 64)) == int_of_string("18446744073172680703")); - assert(unsigned(zero_extend(0xffffffffed9fff7f, 64)) == int_of_string("18446744073401270143")); - assert(unsigned(zero_extend(0xffffffffedafff8f, 64)) == int_of_string("18446744073402318735")); - assert(unsigned(zero_extend(0xfffffffff0000000, 64)) == int_of_string("18446744073441116160")); - assert(unsigned(zero_extend(0xfffffffff7ffffff, 64)) == int_of_string("18446744073575333887")); - assert(unsigned(zero_extend(0xfffffffff89b3cde, 64)) == int_of_string("18446744073585507550")); - assert(unsigned(zero_extend(0xfffffffffcefffff, 64)) == int_of_string("18446744073658171391")); - assert(unsigned(zero_extend(0xfffffffffcf0ffff, 64)) == int_of_string("18446744073658236927")); - assert(unsigned(zero_extend(0xfffffffffcf1ffff, 64)) == int_of_string("18446744073658302463")); - assert(unsigned(zero_extend(0xfffffffffcf84000, 64)) == int_of_string("18446744073658712064")); - assert(unsigned(zero_extend(0xfffffffffcf94000, 64)) == int_of_string("18446744073658777600")); - assert(unsigned(zero_extend(0xfffffffffcfa4000, 64)) == int_of_string("18446744073658843136")); - assert(unsigned(zero_extend(0xfffffffffd0affff, 64)) == int_of_string("18446744073659940863")); - assert(unsigned(zero_extend(0xfffffffffd0bffff, 64)) == int_of_string("18446744073660006399")); - assert(unsigned(zero_extend(0xfffffffffd0fc000, 64)) == int_of_string("18446744073660252160")); - assert(unsigned(zero_extend(0xfffffffffd10c000, 64)) == int_of_string("18446744073660317696")); - assert(unsigned(zero_extend(0xfffffffffd10ffff, 64)) == int_of_string("18446744073660334079")); - assert(unsigned(zero_extend(0xfffffffffd11ffff, 64)) == int_of_string("18446744073660399615")); - assert(unsigned(zero_extend(0xfffffffffd130000, 64)) == int_of_string("18446744073660465152")); - assert(unsigned(zero_extend(0xfffffffffd13ffff, 64)) == int_of_string("18446744073660530687")); - assert(unsigned(zero_extend(0xfffffffffd140000, 64)) == int_of_string("18446744073660530688")); - assert(unsigned(zero_extend(0xfffffffffd14ffff, 64)) == int_of_string("18446744073660596223")); - assert(unsigned(zero_extend(0xfffffffffd170000, 64)) == int_of_string("18446744073660727296")); - assert(unsigned(zero_extend(0xfffffffffd18c000, 64)) == int_of_string("18446744073660841984")); - assert(unsigned(zero_extend(0xfffffffffebffe6b, 64)) == int_of_string("18446744073688579691")); - assert(unsigned(zero_extend(0xfffffffffebffefb, 64)) == int_of_string("18446744073688579835")); - assert(unsigned(zero_extend(0xfffffffffebfff3b, 64)) == int_of_string("18446744073688579899")); - assert(unsigned(zero_extend(0xffffffffffefffff, 64)) == int_of_string("18446744073708503039")); + assert(unsigned(zero_extend(0xffffffff00000000, 64)) == 18446744069414584320); + assert(unsigned(zero_extend(0xffffffff00000001, 64)) == 18446744069414584321); + assert(unsigned(zero_extend(0xffffffff00007fff, 64)) == 18446744069414617087); + assert(unsigned(zero_extend(0xffffffff3ff01000, 64)) == 18446744070487281664); + assert(unsigned(zero_extend(0xffffffff5fffffff, 64)) == 18446744071025197055); + assert(unsigned(zero_extend(0xffffffff6dcba985, 64)) == 18446744071256648069); + assert(unsigned(zero_extend(0xffffffff6ffffffe, 64)) == 18446744071293632510); + assert(unsigned(zero_extend(0xffffffff6fffffff, 64)) == 18446744071293632511); + assert(unsigned(zero_extend(0xffffffff77665544, 64)) == 18446744071417779524); + assert(unsigned(zero_extend(0xffffffff7ffefffc, 64)) == 18446744071562002428); + assert(unsigned(zero_extend(0xffffffff7ffffffc, 64)) == 18446744071562067964); + assert(unsigned(zero_extend(0xffffffff7ffffffd, 64)) == 18446744071562067965); + assert(unsigned(zero_extend(0xffffffff7ffffffe, 64)) == 18446744071562067966); + assert(unsigned(zero_extend(0xffffffff7fffffff, 64)) == 18446744071562067967); + assert(unsigned(zero_extend(0xffffffff80000000, 64)) == 18446744071562067968); + assert(unsigned(zero_extend(0xffffffff80000001, 64)) == 18446744071562067969); + assert(unsigned(zero_extend(0xffffffff94837260, 64)) == 18446744071906226784); + assert(unsigned(zero_extend(0xffffffffdfffffff, 64)) == 18446744073172680703); + assert(unsigned(zero_extend(0xffffffffed9fff7f, 64)) == 18446744073401270143); + assert(unsigned(zero_extend(0xffffffffedafff8f, 64)) == 18446744073402318735); + assert(unsigned(zero_extend(0xfffffffff0000000, 64)) == 18446744073441116160); + assert(unsigned(zero_extend(0xfffffffff7ffffff, 64)) == 18446744073575333887); + assert(unsigned(zero_extend(0xfffffffff89b3cde, 64)) == 18446744073585507550); + assert(unsigned(zero_extend(0xfffffffffcefffff, 64)) == 18446744073658171391); + assert(unsigned(zero_extend(0xfffffffffcf0ffff, 64)) == 18446744073658236927); + assert(unsigned(zero_extend(0xfffffffffcf1ffff, 64)) == 18446744073658302463); + assert(unsigned(zero_extend(0xfffffffffcf84000, 64)) == 18446744073658712064); + assert(unsigned(zero_extend(0xfffffffffcf94000, 64)) == 18446744073658777600); + assert(unsigned(zero_extend(0xfffffffffcfa4000, 64)) == 18446744073658843136); + assert(unsigned(zero_extend(0xfffffffffd0affff, 64)) == 18446744073659940863); + assert(unsigned(zero_extend(0xfffffffffd0bffff, 64)) == 18446744073660006399); + assert(unsigned(zero_extend(0xfffffffffd0fc000, 64)) == 18446744073660252160); + assert(unsigned(zero_extend(0xfffffffffd10c000, 64)) == 18446744073660317696); + assert(unsigned(zero_extend(0xfffffffffd10ffff, 64)) == 18446744073660334079); + assert(unsigned(zero_extend(0xfffffffffd11ffff, 64)) == 18446744073660399615); + assert(unsigned(zero_extend(0xfffffffffd130000, 64)) == 18446744073660465152); + assert(unsigned(zero_extend(0xfffffffffd13ffff, 64)) == 18446744073660530687); + assert(unsigned(zero_extend(0xfffffffffd140000, 64)) == 18446744073660530688); + assert(unsigned(zero_extend(0xfffffffffd14ffff, 64)) == 18446744073660596223); + assert(unsigned(zero_extend(0xfffffffffd170000, 64)) == 18446744073660727296); + assert(unsigned(zero_extend(0xfffffffffd18c000, 64)) == 18446744073660841984); + assert(unsigned(zero_extend(0xfffffffffebffe6b, 64)) == 18446744073688579691); + assert(unsigned(zero_extend(0xfffffffffebffefb, 64)) == 18446744073688579835); + assert(unsigned(zero_extend(0xfffffffffebfff3b, 64)) == 18446744073688579899); + assert(unsigned(zero_extend(0xffffffffffefffff, 64)) == 18446744073708503039); assert(unsigned(zero_extend(0xfffffffffff, 64)) == 17592186044415); - assert(unsigned(zero_extend(0xfffffffffff70000, 64)) == int_of_string("18446744073708961792")); - assert(unsigned(zero_extend(0xfffffffffff80000, 64)) == int_of_string("18446744073709027328")); - assert(unsigned(zero_extend(0xfffffffffffc0000, 64)) == int_of_string("18446744073709289472")); - assert(unsigned(zero_extend(0xfffffffffffd0000, 64)) == int_of_string("18446744073709355008")); - assert(unsigned(zero_extend(0xfffffffffffdffff, 64)) == int_of_string("18446744073709420543")); - assert(unsigned(zero_extend(0xfffffffffffe0000, 64)) == int_of_string("18446744073709420544")); - assert(unsigned(zero_extend(0xfffffffffffe7ffe, 64)) == int_of_string("18446744073709453310")); - assert(unsigned(zero_extend(0xfffffffffffe7fff, 64)) == int_of_string("18446744073709453311")); - assert(unsigned(zero_extend(0xfffffffffffe8000, 64)) == int_of_string("18446744073709453312")); - assert(unsigned(zero_extend(0xfffffffffffe8001, 64)) == int_of_string("18446744073709453313")); - assert(unsigned(zero_extend(0xfffffffffffefffe, 64)) == int_of_string("18446744073709486078")); - assert(unsigned(zero_extend(0xfffffffffffeffff, 64)) == int_of_string("18446744073709486079")); - assert(unsigned(zero_extend(0xffffffffffff0000, 64)) == int_of_string("18446744073709486080")); - assert(unsigned(zero_extend(0xffffffffffff0001, 64)) == int_of_string("18446744073709486081")); - assert(unsigned(zero_extend(0xffffffffffff641f, 64)) == int_of_string("18446744073709511711")); - assert(unsigned(zero_extend(0xffffffffffff7ffc, 64)) == int_of_string("18446744073709518844")); - assert(unsigned(zero_extend(0xffffffffffff7ffd, 64)) == int_of_string("18446744073709518845")); - assert(unsigned(zero_extend(0xffffffffffff7ffe, 64)) == int_of_string("18446744073709518846")); - assert(unsigned(zero_extend(0xffffffffffff7fff, 64)) == int_of_string("18446744073709518847")); - assert(unsigned(zero_extend(0xffffffffffff8000, 64)) == int_of_string("18446744073709518848")); - assert(unsigned(zero_extend(0xffffffffffff8001, 64)) == int_of_string("18446744073709518849")); - assert(unsigned(zero_extend(0xffffffffffffbeff, 64)) == int_of_string("18446744073709534975")); - assert(unsigned(zero_extend(0xffffffffffffbf40, 64)) == int_of_string("18446744073709535040")); - assert(unsigned(zero_extend(0xffffffffffffbf41, 64)) == int_of_string("18446744073709535041")); - assert(unsigned(zero_extend(0xffffffffffffbfff, 64)) == int_of_string("18446744073709535231")); - assert(unsigned(zero_extend(0xffffffffffffc22c, 64)) == int_of_string("18446744073709535788")); - assert(unsigned(zero_extend(0xffffffffffffc24c, 64)) == int_of_string("18446744073709535820")); - assert(unsigned(zero_extend(0xffffffffffffd220, 64)) == int_of_string("18446744073709539872")); - assert(unsigned(zero_extend(0xffffffffffffd23c, 64)) == int_of_string("18446744073709539900")); - assert(unsigned(zero_extend(0xffffffffffffe220, 64)) == int_of_string("18446744073709543968")); - assert(unsigned(zero_extend(0xffffffffffffe23c, 64)) == int_of_string("18446744073709543996")); - assert(unsigned(zero_extend(0xffffffffffffefff, 64)) == int_of_string("18446744073709547519")); - assert(unsigned(zero_extend(0xfffffffffffffeef, 64)) == int_of_string("18446744073709551343")); - assert(unsigned(zero_extend(0xfffffffffffffeff, 64)) == int_of_string("18446744073709551359")); - assert(unsigned(zero_extend(0xffffffffffffff1f, 64)) == int_of_string("18446744073709551391")); - assert(unsigned(zero_extend(0xffffffffffffff2f, 64)) == int_of_string("18446744073709551407")); - assert(unsigned(zero_extend(0xffffffffffffff4f, 64)) == int_of_string("18446744073709551439")); - assert(unsigned(zero_extend(0xffffffffffffff6f, 64)) == int_of_string("18446744073709551471")); - assert(unsigned(zero_extend(0xffffffffffffff80, 64)) == int_of_string("18446744073709551488")); - assert(unsigned(zero_extend(0xffffffffffffff8f, 64)) == int_of_string("18446744073709551503")); - assert(unsigned(zero_extend(0xffffffffffffff9f, 64)) == int_of_string("18446744073709551519")); - assert(unsigned(zero_extend(0xffffffffffffffa0, 64)) == int_of_string("18446744073709551520")); - assert(unsigned(zero_extend(0xffffffffffffffaf, 64)) == int_of_string("18446744073709551535")); - assert(unsigned(zero_extend(0xffffffffffffffbf, 64)) == int_of_string("18446744073709551551")); - assert(unsigned(zero_extend(0xffffffffffffffc2, 64)) == int_of_string("18446744073709551554")); - assert(unsigned(zero_extend(0xffffffffffffffc4, 64)) == int_of_string("18446744073709551556")); - assert(unsigned(zero_extend(0xffffffffffffffc6, 64)) == int_of_string("18446744073709551558")); - assert(unsigned(zero_extend(0xffffffffffffffc8, 64)) == int_of_string("18446744073709551560")); - assert(unsigned(zero_extend(0xffffffffffffffca, 64)) == int_of_string("18446744073709551562")); - assert(unsigned(zero_extend(0xffffffffffffffcc, 64)) == int_of_string("18446744073709551564")); - assert(unsigned(zero_extend(0xffffffffffffffce, 64)) == int_of_string("18446744073709551566")); - assert(unsigned(zero_extend(0xffffffffffffffcf, 64)) == int_of_string("18446744073709551567")); - assert(unsigned(zero_extend(0xffffffffffffffd0, 64)) == int_of_string("18446744073709551568")); - assert(unsigned(zero_extend(0xffffffffffffffd2, 64)) == int_of_string("18446744073709551570")); - assert(unsigned(zero_extend(0xffffffffffffffd4, 64)) == int_of_string("18446744073709551572")); - assert(unsigned(zero_extend(0xffffffffffffffd6, 64)) == int_of_string("18446744073709551574")); - assert(unsigned(zero_extend(0xffffffffffffffd8, 64)) == int_of_string("18446744073709551576")); - assert(unsigned(zero_extend(0xffffffffffffffda, 64)) == int_of_string("18446744073709551578")); - assert(unsigned(zero_extend(0xffffffffffffffdb, 64)) == int_of_string("18446744073709551579")); - assert(unsigned(zero_extend(0xffffffffffffffdc, 64)) == int_of_string("18446744073709551580")); - assert(unsigned(zero_extend(0xffffffffffffffde, 64)) == int_of_string("18446744073709551582")); - assert(unsigned(zero_extend(0xffffffffffffffdf, 64)) == int_of_string("18446744073709551583")); - assert(unsigned(zero_extend(0xffffffffffffffe0, 64)) == int_of_string("18446744073709551584")); - assert(unsigned(zero_extend(0xffffffffffffffe2, 64)) == int_of_string("18446744073709551586")); - assert(unsigned(zero_extend(0xffffffffffffffe4, 64)) == int_of_string("18446744073709551588")); - assert(unsigned(zero_extend(0xffffffffffffffe6, 64)) == int_of_string("18446744073709551590")); - assert(unsigned(zero_extend(0xffffffffffffffe7, 64)) == int_of_string("18446744073709551591")); - assert(unsigned(zero_extend(0xffffffffffffffe8, 64)) == int_of_string("18446744073709551592")); - assert(unsigned(zero_extend(0xffffffffffffffea, 64)) == int_of_string("18446744073709551594")); - assert(unsigned(zero_extend(0xffffffffffffffec, 64)) == int_of_string("18446744073709551596")); - assert(unsigned(zero_extend(0xffffffffffffffee, 64)) == int_of_string("18446744073709551598")); - assert(unsigned(zero_extend(0xffffffffffffffef, 64)) == int_of_string("18446744073709551599")); + assert(unsigned(zero_extend(0xfffffffffff70000, 64)) == 18446744073708961792); + assert(unsigned(zero_extend(0xfffffffffff80000, 64)) == 18446744073709027328); + assert(unsigned(zero_extend(0xfffffffffffc0000, 64)) == 18446744073709289472); + assert(unsigned(zero_extend(0xfffffffffffd0000, 64)) == 18446744073709355008); + assert(unsigned(zero_extend(0xfffffffffffdffff, 64)) == 18446744073709420543); + assert(unsigned(zero_extend(0xfffffffffffe0000, 64)) == 18446744073709420544); + assert(unsigned(zero_extend(0xfffffffffffe7ffe, 64)) == 18446744073709453310); + assert(unsigned(zero_extend(0xfffffffffffe7fff, 64)) == 18446744073709453311); + assert(unsigned(zero_extend(0xfffffffffffe8000, 64)) == 18446744073709453312); + assert(unsigned(zero_extend(0xfffffffffffe8001, 64)) == 18446744073709453313); + assert(unsigned(zero_extend(0xfffffffffffefffe, 64)) == 18446744073709486078); + assert(unsigned(zero_extend(0xfffffffffffeffff, 64)) == 18446744073709486079); + assert(unsigned(zero_extend(0xffffffffffff0000, 64)) == 18446744073709486080); + assert(unsigned(zero_extend(0xffffffffffff0001, 64)) == 18446744073709486081); + assert(unsigned(zero_extend(0xffffffffffff641f, 64)) == 18446744073709511711); + assert(unsigned(zero_extend(0xffffffffffff7ffc, 64)) == 18446744073709518844); + assert(unsigned(zero_extend(0xffffffffffff7ffd, 64)) == 18446744073709518845); + assert(unsigned(zero_extend(0xffffffffffff7ffe, 64)) == 18446744073709518846); + assert(unsigned(zero_extend(0xffffffffffff7fff, 64)) == 18446744073709518847); + assert(unsigned(zero_extend(0xffffffffffff8000, 64)) == 18446744073709518848); + assert(unsigned(zero_extend(0xffffffffffff8001, 64)) == 18446744073709518849); + assert(unsigned(zero_extend(0xffffffffffffbeff, 64)) == 18446744073709534975); + assert(unsigned(zero_extend(0xffffffffffffbf40, 64)) == 18446744073709535040); + assert(unsigned(zero_extend(0xffffffffffffbf41, 64)) == 18446744073709535041); + assert(unsigned(zero_extend(0xffffffffffffbfff, 64)) == 18446744073709535231); + assert(unsigned(zero_extend(0xffffffffffffc22c, 64)) == 18446744073709535788); + assert(unsigned(zero_extend(0xffffffffffffc24c, 64)) == 18446744073709535820); + assert(unsigned(zero_extend(0xffffffffffffd220, 64)) == 18446744073709539872); + assert(unsigned(zero_extend(0xffffffffffffd23c, 64)) == 18446744073709539900); + assert(unsigned(zero_extend(0xffffffffffffe220, 64)) == 18446744073709543968); + assert(unsigned(zero_extend(0xffffffffffffe23c, 64)) == 18446744073709543996); + assert(unsigned(zero_extend(0xffffffffffffefff, 64)) == 18446744073709547519); + assert(unsigned(zero_extend(0xfffffffffffffeef, 64)) == 18446744073709551343); + assert(unsigned(zero_extend(0xfffffffffffffeff, 64)) == 18446744073709551359); + assert(unsigned(zero_extend(0xffffffffffffff1f, 64)) == 18446744073709551391); + assert(unsigned(zero_extend(0xffffffffffffff2f, 64)) == 18446744073709551407); + assert(unsigned(zero_extend(0xffffffffffffff4f, 64)) == 18446744073709551439); + assert(unsigned(zero_extend(0xffffffffffffff6f, 64)) == 18446744073709551471); + assert(unsigned(zero_extend(0xffffffffffffff80, 64)) == 18446744073709551488); + assert(unsigned(zero_extend(0xffffffffffffff8f, 64)) == 18446744073709551503); + assert(unsigned(zero_extend(0xffffffffffffff9f, 64)) == 18446744073709551519); + assert(unsigned(zero_extend(0xffffffffffffffa0, 64)) == 18446744073709551520); + assert(unsigned(zero_extend(0xffffffffffffffaf, 64)) == 18446744073709551535); + assert(unsigned(zero_extend(0xffffffffffffffbf, 64)) == 18446744073709551551); + assert(unsigned(zero_extend(0xffffffffffffffc2, 64)) == 18446744073709551554); + assert(unsigned(zero_extend(0xffffffffffffffc4, 64)) == 18446744073709551556); + assert(unsigned(zero_extend(0xffffffffffffffc6, 64)) == 18446744073709551558); + assert(unsigned(zero_extend(0xffffffffffffffc8, 64)) == 18446744073709551560); + assert(unsigned(zero_extend(0xffffffffffffffca, 64)) == 18446744073709551562); + assert(unsigned(zero_extend(0xffffffffffffffcc, 64)) == 18446744073709551564); + assert(unsigned(zero_extend(0xffffffffffffffce, 64)) == 18446744073709551566); + assert(unsigned(zero_extend(0xffffffffffffffcf, 64)) == 18446744073709551567); + assert(unsigned(zero_extend(0xffffffffffffffd0, 64)) == 18446744073709551568); + assert(unsigned(zero_extend(0xffffffffffffffd2, 64)) == 18446744073709551570); + assert(unsigned(zero_extend(0xffffffffffffffd4, 64)) == 18446744073709551572); + assert(unsigned(zero_extend(0xffffffffffffffd6, 64)) == 18446744073709551574); + assert(unsigned(zero_extend(0xffffffffffffffd8, 64)) == 18446744073709551576); + assert(unsigned(zero_extend(0xffffffffffffffda, 64)) == 18446744073709551578); + assert(unsigned(zero_extend(0xffffffffffffffdb, 64)) == 18446744073709551579); + assert(unsigned(zero_extend(0xffffffffffffffdc, 64)) == 18446744073709551580); + assert(unsigned(zero_extend(0xffffffffffffffde, 64)) == 18446744073709551582); + assert(unsigned(zero_extend(0xffffffffffffffdf, 64)) == 18446744073709551583); + assert(unsigned(zero_extend(0xffffffffffffffe0, 64)) == 18446744073709551584); + assert(unsigned(zero_extend(0xffffffffffffffe2, 64)) == 18446744073709551586); + assert(unsigned(zero_extend(0xffffffffffffffe4, 64)) == 18446744073709551588); + assert(unsigned(zero_extend(0xffffffffffffffe6, 64)) == 18446744073709551590); + assert(unsigned(zero_extend(0xffffffffffffffe7, 64)) == 18446744073709551591); + assert(unsigned(zero_extend(0xffffffffffffffe8, 64)) == 18446744073709551592); + assert(unsigned(zero_extend(0xffffffffffffffea, 64)) == 18446744073709551594); + assert(unsigned(zero_extend(0xffffffffffffffec, 64)) == 18446744073709551596); + assert(unsigned(zero_extend(0xffffffffffffffee, 64)) == 18446744073709551598); + assert(unsigned(zero_extend(0xffffffffffffffef, 64)) == 18446744073709551599); assert(unsigned(zero_extend(0xfffffffffffffff, 64)) == 1152921504606846975); - assert(unsigned(zero_extend(0xfffffffffffffff0, 64)) == int_of_string("18446744073709551600")); - assert(unsigned(zero_extend(0xfffffffffffffff1, 64)) == int_of_string("18446744073709551601")); - assert(unsigned(zero_extend(0xfffffffffffffff2, 64)) == int_of_string("18446744073709551602")); - assert(unsigned(zero_extend(0xfffffffffffffff4, 64)) == int_of_string("18446744073709551604")); - assert(unsigned(zero_extend(0xfffffffffffffff6, 64)) == int_of_string("18446744073709551606")); - assert(unsigned(zero_extend(0xfffffffffffffff7, 64)) == int_of_string("18446744073709551607")); - assert(unsigned(zero_extend(0xfffffffffffffff8, 64)) == int_of_string("18446744073709551608")); - assert(unsigned(zero_extend(0xfffffffffffffffa, 64)) == int_of_string("18446744073709551610")); - assert(unsigned(zero_extend(0xfffffffffffffffb, 64)) == int_of_string("18446744073709551611")); - assert(unsigned(zero_extend(0xfffffffffffffffc, 64)) == int_of_string("18446744073709551612")); - assert(unsigned(zero_extend(0xfffffffffffffffd, 64)) == int_of_string("18446744073709551613")); - assert(unsigned(zero_extend(0xfffffffffffffffe, 64)) == int_of_string("18446744073709551614")); - assert(unsigned(zero_extend(0xffffffffffffffff, 64)) == int_of_string("18446744073709551615")); + assert(unsigned(zero_extend(0xfffffffffffffff0, 64)) == 18446744073709551600); + assert(unsigned(zero_extend(0xfffffffffffffff1, 64)) == 18446744073709551601); + assert(unsigned(zero_extend(0xfffffffffffffff2, 64)) == 18446744073709551602); + assert(unsigned(zero_extend(0xfffffffffffffff4, 64)) == 18446744073709551604); + assert(unsigned(zero_extend(0xfffffffffffffff6, 64)) == 18446744073709551606); + assert(unsigned(zero_extend(0xfffffffffffffff7, 64)) == 18446744073709551607); + assert(unsigned(zero_extend(0xfffffffffffffff8, 64)) == 18446744073709551608); + assert(unsigned(zero_extend(0xfffffffffffffffa, 64)) == 18446744073709551610); + assert(unsigned(zero_extend(0xfffffffffffffffb, 64)) == 18446744073709551611); + assert(unsigned(zero_extend(0xfffffffffffffffc, 64)) == 18446744073709551612); + assert(unsigned(zero_extend(0xfffffffffffffffd, 64)) == 18446744073709551613); + assert(unsigned(zero_extend(0xfffffffffffffffe, 64)) == 18446744073709551614); + assert(unsigned(zero_extend(0xffffffffffffffff, 64)) == 18446744073709551615); assert(unsigned(zero_extend(0x0, 8)) == 0); assert(unsigned(zero_extend(0x20, 8)) == 32); assert(unsigned(zero_extend(0x28, 8)) == 40); diff --git a/test/builtins/zeros.sail b/test/builtins/zeros.sail index 79500469..c2fb75c4 100644 --- a/test/builtins/zeros.sail +++ b/test/builtins/zeros.sail @@ -4,6 +4,8 @@ $include <exception_basic.sail> $include <flow.sail> $include <vector_dec.sail> +overload zeros = {sail_zeros} + function main (() : unit) -> unit = { assert(zeros(1) == 1^0b0); assert(zeros(10) == 10^0x0); diff --git a/test/c/run_tests.py b/test/c/run_tests.py new file mode 100755 index 00000000..9c5c486c --- /dev/null +++ b/test/c/run_tests.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python + +import os +import re +import sys +import hashlib + +sail_dir = os.environ['SAIL_DIR'] +os.chdir(os.path.dirname(__file__)) +sys.path.insert(0, os.path.join(sail_dir, 'test')) + +from sailtest import * + +def test_c(name, c_opts, sail_opts, valgrind): + banner('Testing {} with C options: {} Sail options: {} valgrind: {}'.format(name, c_opts, sail_opts, valgrind)) + tests = {} + for filename in os.listdir('.'): + if re.match('.+\.sail', filename): + basename = os.path.splitext(os.path.basename(filename))[0] + tests[filename] = os.fork() + if tests[filename] == 0: + step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename)) + step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, sail_dir, sail_dir, basename)) + step('./{} 1> {}.result'.format(basename, basename)) + step('diff {}.result {}.expect'.format(basename, basename)) + if valgrind: + step("valgrind --leak-check=full --errors-for-leak-kinds=all --error-exitcode=1 ./{}".format(basename)) + print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) + sys.exit() + return collect_results(name, tests) + +xml = '<testsuites>\n' + +xml += test_c('unoptimized C', '', '', True) +xml += test_c('optimized C', '-O2', '-O', True) +xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False) + +xml += '</testsuites>\n' + +output = open('tests.xml', 'w') +output.write(xml) +output.close() diff --git a/test/sailtest.py b/test/sailtest.py new file mode 100644 index 00000000..f0036236 --- /dev/null +++ b/test/sailtest.py @@ -0,0 +1,51 @@ +import os +import re +import sys +import subprocess +import datetime + +class color: + NOTICE = '\033[94m' + PASS = '\033[92m' + WARNING = '\033[93m' + FAIL = '\033[91m' + END = '\033[0m' + + +def step(string): + p = subprocess.Popen(string, shell=True, stderr=subprocess.PIPE, stdout=subprocess.PIPE) + out, err = p.communicate() + status = p.wait() + if status != 0: + print("{}Failed{}: {}".format(color.FAIL, color.END, string)) + print('{}stdout{}:'.format(color.NOTICE, color.END)) + print(out) + print('{}stderr{}:'.format(color.NOTICE, color.END)) + print(err) + sys.exit(1) + +def banner(string): + print '=' * len(string) + print string + print '=' * len(string) + +def collect_results(name, tests): + passes = 0 + failures = 0 + xml = "" + + for test in tests: + _, status = os.waitpid(tests[test], 0) + if status != 0: + failures += 1 + xml += ' <testcase name="{}">\n <error message="fail">fail</error>\n </testcase>\n'.format(test) + else: + passes += 1 + xml += ' <testcase name="{}"/>\n'.format(test) + + print '{}{} passes and {} failures{}'.format(color.NOTICE, passes, failures, color.END) + + time = datetime.datetime.utcnow() + suite = ' <testsuite name="{}" tests="{}" failures="{}" timestamp="{}">\n{} </testsuite>\n' + xml = suite.format(name, passes + failures, failures, time, xml) + return xml |