diff options
| author | Thomas Bauereiss | 2018-05-11 12:04:10 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-11 12:04:10 +0100 |
| commit | ff18bac6654a73cedf32a45ee406fe3e74ae3efd (patch) | |
| tree | ed940ea575c93d741c84cd24cd3e029d0a590b81 /test | |
| parent | 823fe1d82e753add2d54ba010689a81af027ba6d (diff) | |
| parent | db3b6d21c18f4ac516c2554db6890274d2b8292c (diff) | |
Merge branch 'sail2' into cheri-mono
In order to use up-to-date sequential CHERI model for test suite
Diffstat (limited to 'test')
| -rwxr-xr-x | test/arm/run_tests.sh | 2 | ||||
| -rw-r--r-- | test/builtins/get_slice_int.sail | 36 | ||||
| -rwxr-xr-x | test/builtins/run_tests.sh | 48 | ||||
| -rw-r--r-- | test/builtins/set_slice_bits.sail | 2 | ||||
| -rw-r--r-- | test/builtins/signed.sail | 120 | ||||
| -rw-r--r-- | test/builtins/test_extras.lem | 22 | ||||
| -rw-r--r-- | test/builtins/unsigned6.sail | 392 | ||||
| -rw-r--r-- | test/isabelle/Aarch64_code.thy | 61 | ||||
| -rw-r--r-- | test/isabelle/Cheri_code.thy | 62 | ||||
| -rw-r--r-- | test/isabelle/Makefile | 27 | ||||
| -rw-r--r-- | test/isabelle/ROOT | 9 | ||||
| -rw-r--r-- | test/isabelle/elf_loader.ml | 126 | ||||
| -rw-r--r-- | test/isabelle/run_aarch64.ml | 93 | ||||
| -rw-r--r-- | test/isabelle/run_cheri.ml | 92 | ||||
| -rwxr-xr-x | test/isabelle/run_tests.sh | 90 | ||||
| -rw-r--r-- | test/typecheck/pass/simple_record_access.sail | 1 |
16 files changed, 916 insertions, 267 deletions
diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh index 15a45e7c..f758d634 100755 --- a/test/arm/run_tests.sh +++ b/test/arm/run_tests.sh @@ -73,7 +73,7 @@ then else red "compiling no_vector specification" "fail"; - for $i in `ls *.elf`; + for i in `ls *.elf`; do red "failed $i" "fail" done diff --git a/test/builtins/get_slice_int.sail b/test/builtins/get_slice_int.sail index 70894155..73c495fa 100644 --- a/test/builtins/get_slice_int.sail +++ b/test/builtins/get_slice_int.sail @@ -4,6 +4,12 @@ $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"); @@ -251,20 +257,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, 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, 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, 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"); @@ -465,4 +471,4 @@ function main (() : unit) -> unit = { assert(get_slice_int(64, 91820, 0) == 64^0x166ac, "get_slice_int(64, 91820, 0) == 64^0x166ac"); assert(get_slice_int(64, 91824, 0) == 64^0x166b0, "get_slice_int(64, 91824, 0) == 64^0x166b0"); assert(get_slice_int(64, 91828, 0) == 64^0x166b4, "get_slice_int(64, 91828, 0) == 64^0x166b4"); -}
\ No newline at end of file +} diff --git a/test/builtins/run_tests.sh b/test/builtins/run_tests.sh index b1d19639..1fe2d182 100755 --- a/test/builtins/run_tests.sh +++ b/test/builtins/run_tests.sh @@ -5,6 +5,7 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" cd $DIR SAILDIR="$DIR/../.." +LEMBUILDDIR="$DIR/_lembuild" RED='\033[0;31m' GREEN='\033[0;32m' @@ -81,7 +82,54 @@ do red "compiling $(basename $file) (OCaml)" "fail" fi; + mkdir -p "$LEMBUILDDIR" + + if "$SAILDIR/sail" -no_warn -lem -lem_mwords -lem_lib Test_extras -undefined_gen -o out "$file" 1> /dev/null 2> /dev/null; + then + mv out.lem out_types.lem "$LEMBUILDDIR" + if lem -ocaml -lib "$SAILDIR/src/lem_interp" \ + -outdir "$LEMBUILDDIR" \ + "$SAILDIR/src/gen_lib/sail_values.lem" \ + "$SAILDIR/src/gen_lib/sail_operators.lem" \ + "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \ + "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \ + "$SAILDIR/src/gen_lib/prompt.lem" \ + "$SAILDIR/src/gen_lib/state_monad.lem" \ + "$SAILDIR/src/gen_lib/state.lem" \ + "$SAILDIR/src/gen_lib/prompt_monad.lem" \ + "test_extras.lem" "$LEMBUILDDIR/out_types.lem" "$LEMBUILDDIR/out.lem" 1> /dev/null 2> /dev/null; + then + cd "$LEMBUILDDIR" + if ocamlfind ocamlc -linkpkg -package zarith -package lem \ + sail_values.ml sail_operators.ml \ + sail_instr_kinds.ml prompt_monad.ml prompt.ml \ + sail_operators_mwords.ml state_monad.ml state.ml \ + test_extras.ml out_types.ml out.ml ../test.ml \ + -o test 1> /dev/null 2> /dev/null + then + green "compiling $(basename $file) (Lem)" "ok" + if ./test 1> /dev/null 2> /dev/null + then + green "tested $(basename ${file%.sail}) (Lem)" "ok" + else + red "tested $(basename ${file%.sail}) (Lem)" "fail" + fi + else + red "compiling $(basename $file) (Sail->Lem->Ocaml->Bytecode)" "fail" + fi + cd "$DIR" + else + red "compiling $(basename $file) (Sail->Lem->Ocaml)" "fail" + fi + else + red "compiling $(basename $file) (Sail->Lem)" "fail" + fi; + rm -rf $DIR/_sbuild/; + rm -rf "$LEMBUILDDIR"; + rm -f Out_lemmas.thy; + rm -f out_types.lem; + rm -f out.lem; rm -f ${file%.sail}.c; rm -f a.out; rm -f out diff --git a/test/builtins/set_slice_bits.sail b/test/builtins/set_slice_bits.sail index 67b11cdf..07c01e5b 100644 --- a/test/builtins/set_slice_bits.sail +++ b/test/builtins/set_slice_bits.sail @@ -680,4 +680,4 @@ function main (() : unit) -> unit = { assert(set_slice_bits(64, 9, 64^0x0, 14, 9^0x0) == 64^0x0, "set_slice_bits(64, 9, 64^0x0, 14, 9^0x0) == 64^0x0"); assert(set_slice_bits(64, 9, 64^0x0, 32, 9^0x0) == 64^0x0, "set_slice_bits(64, 9, 64^0x0, 32, 9^0x0) == 64^0x0"); assert(set_slice_bits(64, 9, 64^0x80800000, 14, 9^0x0) == 64^0x80800000, "set_slice_bits(64, 9, 64^0x80800000, 14, 9^0x0) == 64^0x80800000"); -}
\ No newline at end of file +} diff --git a/test/builtins/signed.sail b/test/builtins/signed.sail index 7b9160f7..21524e2f 100644 --- a/test/builtins/signed.sail +++ b/test/builtins/signed.sail @@ -3,6 +3,12 @@ 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 + function main (() : unit) -> unit = { assert(signed(zero_extend(0x0, 32)) == 0); assert(signed(zero_extend(0x1, 32)) == 1); @@ -1352,8 +1358,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)) == 6510615555426900569); - assert(signed(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == 6510615555426900570); + assert(signed(zero_extend(0x5a5a5a5a5a5a5a59, 64)) == int_of_string("6510615555426900569")); + assert(signed(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == int_of_string("6510615555426900570")); assert(signed(zero_extend(0x5b, 64)) == 91); assert(signed(zero_extend(0x5c, 64)) == 92); assert(signed(zero_extend(0x5c000, 64)) == 376832); @@ -1398,10 +1404,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)) == 7988907161199463611); + assert(signed(zero_extend(0x6ede4cbc6ede4cbb, 64)) == int_of_string("7988907161199463611")); assert(signed(zero_extend(0x6f, 64)) == 111); - assert(signed(zero_extend(0x6ffffffffffffffe, 64)) == 8070450532247928830); - assert(signed(zero_extend(0x6fffffffffffffff, 64)) == 8070450532247928831); + assert(signed(zero_extend(0x6ffffffffffffffe, 64)) == int_of_string("8070450532247928830")); + assert(signed(zero_extend(0x6fffffffffffffff, 64)) == int_of_string("8070450532247928831")); assert(signed(zero_extend(0x7, 64)) == 7); assert(signed(zero_extend(0x70, 64)) == 112); assert(signed(zero_extend(0x71, 64)) == 113); @@ -1412,10 +1418,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)) == 8603376411415500098); - assert(signed(zero_extend(0x7766554477665542, 64)) == 8603657890687243586); + assert(signed(zero_extend(0x7765554377655542, 64)) == int_of_string("8603376411415500098")); + assert(signed(zero_extend(0x7766554477665542, 64)) == int_of_string("8603657890687243586")); assert(signed(zero_extend(0x78, 64)) == 120); - assert(signed(zero_extend(0x789abcdef0123456, 64)) == 8690466096661279830); + assert(signed(zero_extend(0x789abcdef0123456, 64)) == int_of_string("8690466096661279830")); assert(signed(zero_extend(0x79, 64)) == 121); assert(signed(zero_extend(0x7a, 64)) == 122); assert(signed(zero_extend(0x7b, 64)) == 123); @@ -1428,54 +1434,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)) == 9223231297218904061); - assert(signed(zero_extend(0x7fff7fff7fff7fff, 64)) == 9223231297218904063); + assert(signed(zero_extend(0x7fff7fff7fff7ffd, 64)) == int_of_string("9223231297218904061")); + assert(signed(zero_extend(0x7fff7fff7fff7fff, 64)) == int_of_string("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)) == 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(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(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)) == -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(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(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)) == -9223231297218904064); - assert(signed(zero_extend(0x8000800080008002, 64)) == -9223231297218904062); + assert(signed(zero_extend(0x8000800080008000, 64)) == int_of_string("-9223231297218904064")); + assert(signed(zero_extend(0x8000800080008002, 64)) == int_of_string("-9223231297218904062")); assert(signed(zero_extend(0x8001, 64)) == 32769); assert(signed(zero_extend(0x80010003, 64)) == 2147549187); assert(signed(zero_extend(0x8002, 64)) == 32770); @@ -1503,26 +1509,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)) == -8690466096661279831); + assert(signed(zero_extend(0x876543210fedcba9, 64)) == int_of_string("-8690466096661279831")); assert(signed(zero_extend(0x88, 64)) == 136); assert(signed(zero_extend(0x8899aabb, 64)) == 2291772091); - 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(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(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)) == -8070450532247928833); + assert(signed(zero_extend(0x8fffffffffffffff, 64)) == int_of_string("-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)) == -8070450532247928832); - assert(signed(zero_extend(0x9000000000000001, 64)) == -8070450532247928831); + assert(signed(zero_extend(0x9000000000000000, 64)) == int_of_string("-8070450532247928832")); + assert(signed(zero_extend(0x9000000000000001, 64)) == int_of_string("-8070450532247928831")); assert(signed(zero_extend(0x90000001, 64)) == 2415919105); - assert(signed(zero_extend(0x9121b3439121b344, 64)) == -7988907161199463612); + assert(signed(zero_extend(0x9121b3439121b344, 64)) == int_of_string("-7988907161199463612")); assert(signed(zero_extend(0x9200040, 64)) == 153092160); assert(signed(zero_extend(0x920005c, 64)) == 153092188); assert(signed(zero_extend(0x9200060, 64)) == 153092192); @@ -1540,7 +1546,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)) == -6510615555426900571); + assert(signed(zero_extend(0xa5a5a5a5a5a5a5a5, 64)) == int_of_string("-6510615555426900571")); assert(signed(zero_extend(0xa8, 64)) == 168); assert(signed(zero_extend(0xb, 64)) == 11); assert(signed(zero_extend(0xb0, 64)) == 176); @@ -1550,13 +1556,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)) == -2459565876494606884); + assert(signed(zero_extend(0xdddddddddddddddc, 64)) == int_of_string("-2459565876494606884")); assert(signed(zero_extend(0xe, 64)) == 14); assert(signed(zero_extend(0xe0, 64)) == 224); - assert(signed(zero_extend(0xedcba9876543210e, 64)) == -1311768467463790322); + assert(signed(zero_extend(0xedcba9876543210e, 64)) == int_of_string("-1311768467463790322")); assert(signed(zero_extend(0xf, 64)) == 15); assert(signed(zero_extend(0xf00, 64)) == 3840); - assert(signed(zero_extend(0xf000000000000000, 64)) == -1152921504606846976); + assert(signed(zero_extend(0xf000000000000000, 64)) == int_of_string("-1152921504606846976")); assert(signed(zero_extend(0xff, 64)) == 255); assert(signed(zero_extend(0xfffe, 64)) == 65534); assert(signed(zero_extend(0xffff, 64)) == 65535); @@ -1704,4 +1710,4 @@ function main (() : unit) -> unit = { assert(signed(zero_extend(0xfffffffffffffffd, 64)) == -3); assert(signed(zero_extend(0xfffffffffffffffe, 64)) == -2); assert(signed(zero_extend(0xffffffffffffffff, 64)) == -1); -}
\ No newline at end of file +} diff --git a/test/builtins/test_extras.lem b/test/builtins/test_extras.lem new file mode 100644 index 00000000..136f680e --- /dev/null +++ b/test/builtins/test_extras.lem @@ -0,0 +1,22 @@ +open import Pervasives_extra +open import Sail_instr_kinds +open import Sail_values +open import Sail_operators_mwords +open import Prompt_monad +open import State + +type ty0 +instance (Size ty0) let size = 0 end +declare isabelle target_rep type ty1 = `0` + +val undefined_int : forall 'rv 'e. unit -> monad 'rv integer 'e +let undefined_int () = return 0 + +val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e +let undefined_bitvector len = return (zeros(len)) + +val undefined_unit : forall 'rv 'e. unit -> monad 'rv unit 'e +let undefined_unit () = return () + +val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e +let internal_pick xs = return (List_extra.head xs) diff --git a/test/builtins/unsigned6.sail b/test/builtins/unsigned6.sail index 556b0db6..ec2635d6 100644 --- a/test/builtins/unsigned6.sail +++ b/test/builtins/unsigned6.sail @@ -3,6 +3,12 @@ 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 + function main (() : unit) -> unit = { assert(unsigned(zero_extend(0x2e015f0, 64)) == 48240112); assert(unsigned(zero_extend(0x2e015f8, 64)) == 48240120); @@ -2057,8 +2063,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)) == 6510615555426900569); - assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == 6510615555426900570); + assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a59, 64)) == int_of_string("6510615555426900569")); + assert(unsigned(zero_extend(0x5a5a5a5a5a5a5a5a, 64)) == int_of_string("6510615555426900570")); assert(unsigned(zero_extend(0x5b, 64)) == 91); assert(unsigned(zero_extend(0x5c, 64)) == 92); assert(unsigned(zero_extend(0x5c000, 64)) == 376832); @@ -2147,10 +2153,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)) == 7988907161199463611); + assert(unsigned(zero_extend(0x6ede4cbc6ede4cbb, 64)) == int_of_string("7988907161199463611")); assert(unsigned(zero_extend(0x6f, 64)) == 111); - assert(unsigned(zero_extend(0x6ffffffffffffffe, 64)) == 8070450532247928830); - assert(unsigned(zero_extend(0x6fffffffffffffff, 64)) == 8070450532247928831); + assert(unsigned(zero_extend(0x6ffffffffffffffe, 64)) == int_of_string("8070450532247928830")); + assert(unsigned(zero_extend(0x6fffffffffffffff, 64)) == int_of_string("8070450532247928831")); assert(unsigned(zero_extend(0x7, 64)) == 7); assert(unsigned(zero_extend(0x70, 64)) == 112); assert(unsigned(zero_extend(0x71, 64)) == 113); @@ -2161,10 +2167,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)) == 8603376411415500098); - assert(unsigned(zero_extend(0x7766554477665542, 64)) == 8603657890687243586); + assert(unsigned(zero_extend(0x7765554377655542, 64)) == int_of_string("8603376411415500098")); + assert(unsigned(zero_extend(0x7766554477665542, 64)) == int_of_string("8603657890687243586")); assert(unsigned(zero_extend(0x78, 64)) == 120); - assert(unsigned(zero_extend(0x789abcdef0123456, 64)) == 8690466096661279830); + assert(unsigned(zero_extend(0x789abcdef0123456, 64)) == int_of_string("8690466096661279830")); assert(unsigned(zero_extend(0x79, 64)) == 121); assert(unsigned(zero_extend(0x7a, 64)) == 122); assert(unsigned(zero_extend(0x7b, 64)) == 123); @@ -2177,54 +2183,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)) == 9223231297218904061); - assert(unsigned(zero_extend(0x7fff7fff7fff7fff, 64)) == 9223231297218904063); + assert(unsigned(zero_extend(0x7fff7fff7fff7ffd, 64)) == int_of_string("9223231297218904061")); + assert(unsigned(zero_extend(0x7fff7fff7fff7fff, 64)) == int_of_string("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)) == 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(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(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)) == 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(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(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)) == 9223512776490647552); - assert(unsigned(zero_extend(0x8000800080008002, 64)) == 9223512776490647554); + assert(unsigned(zero_extend(0x8000800080008000, 64)) == int_of_string("9223512776490647552")); + assert(unsigned(zero_extend(0x8000800080008002, 64)) == int_of_string("9223512776490647554")); assert(unsigned(zero_extend(0x8001, 64)) == 32769); assert(unsigned(zero_extend(0x80010003, 64)) == 2147549187); assert(unsigned(zero_extend(0x8002, 64)) == 32770); @@ -2252,26 +2258,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)) == 9756277977048271785); + assert(unsigned(zero_extend(0x876543210fedcba9, 64)) == int_of_string("9756277977048271785")); assert(unsigned(zero_extend(0x88, 64)) == 136); assert(unsigned(zero_extend(0x8899aabb, 64)) == 2291772091); - 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(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(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)) == 10376293541461622783); + assert(unsigned(zero_extend(0x8fffffffffffffff, 64)) == int_of_string("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)) == 10376293541461622784); - assert(unsigned(zero_extend(0x9000000000000001, 64)) == 10376293541461622785); + assert(unsigned(zero_extend(0x9000000000000000, 64)) == int_of_string("10376293541461622784")); + assert(unsigned(zero_extend(0x9000000000000001, 64)) == int_of_string("10376293541461622785")); assert(unsigned(zero_extend(0x90000001, 64)) == 2415919105); - assert(unsigned(zero_extend(0x9121b3439121b344, 64)) == 10457836912510088004); + assert(unsigned(zero_extend(0x9121b3439121b344, 64)) == int_of_string("10457836912510088004")); assert(unsigned(zero_extend(0x9200000, 64)) == 153092096); assert(unsigned(zero_extend(0x9200004, 64)) == 153092100); assert(unsigned(zero_extend(0x9200008, 64)) == 153092104); @@ -2355,7 +2361,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)) == 11936128518282651045); + assert(unsigned(zero_extend(0xa5a5a5a5a5a5a5a5, 64)) == int_of_string("11936128518282651045")); assert(unsigned(zero_extend(0xa8, 64)) == 168); assert(unsigned(zero_extend(0xb, 64)) == 11); assert(unsigned(zero_extend(0xb0, 64)) == 176); @@ -2365,160 +2371,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)) == 15987178197214944732); + assert(unsigned(zero_extend(0xdddddddddddddddc, 64)) == int_of_string("15987178197214944732")); assert(unsigned(zero_extend(0xe, 64)) == 14); assert(unsigned(zero_extend(0xe0, 64)) == 224); - assert(unsigned(zero_extend(0xedcba9876543210e, 64)) == 17134975606245761294); + assert(unsigned(zero_extend(0xedcba9876543210e, 64)) == int_of_string("17134975606245761294")); assert(unsigned(zero_extend(0xf, 64)) == 15); assert(unsigned(zero_extend(0xf00, 64)) == 3840); - assert(unsigned(zero_extend(0xf000000000000000, 64)) == 17293822569102704640); + assert(unsigned(zero_extend(0xf000000000000000, 64)) == int_of_string("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)) == 18446708893632421888); + assert(unsigned(zero_extend(0xffffe000ffffe000, 64)) == int_of_string("18446708893632421888")); assert(unsigned(zero_extend(0xfffffff, 64)) == 268435455); assert(unsigned(zero_extend(0xfffffffe, 64)) == 4294967294); - 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(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(0xffffffff, 64)) == 4294967295); - 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(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(0xfffffffffff, 64)) == 17592186044415); - 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(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(0xfffffffffffffff, 64)) == 1152921504606846975); - 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(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(0x0, 8)) == 0); assert(unsigned(zero_extend(0x20, 8)) == 32); assert(unsigned(zero_extend(0x28, 8)) == 40); diff --git a/test/isabelle/Aarch64_code.thy b/test/isabelle/Aarch64_code.thy new file mode 100644 index 00000000..05e5bb2e --- /dev/null +++ b/test/isabelle/Aarch64_code.thy @@ -0,0 +1,61 @@ +theory Aarch64_code + imports + Aarch64_lemmas + "HOL-Library.Code_Char" + "HOL-Library.Code_Target_Nat" + "HOL-Library.Code_Target_Int" + "HOL-Library.Code_Real_Approx_By_Float" +begin + +declare [[code abort: failwith]] + +termination shl_int by lexicographic_order +termination while sorry +termination whileM sorry +termination untilM sorry + +declare insert_code[code del] +declare union_coset_filter[code del] + +lemma [code]: "(set xs) \<union> (set ys) = set (xs @ ys)" + by auto + +lemma [code]: "insert x (set xs) = set (x # xs)" + by auto + +declare [[code drop: + "less :: real \<Rightarrow> real \<Rightarrow> bool" + "less_eq :: real \<Rightarrow> real \<Rightarrow> bool" + "floor :: real \<Rightarrow> int"]] + +code_printing constant "floor :: real \<Rightarrow> int" \<rightharpoonup> (OCaml) "(Int'_of'_integer (Big'_int.big'_int'_of'_int (Pervasives.int'_of'_float (Pervasives.floor _))))" + +code_identifier constant ASR \<rightharpoonup> (OCaml) "Aarch64.asr0" +code_identifier constant LSL \<rightharpoonup> (OCaml) "Aarch64.lsl0" +code_identifier constant LSR \<rightharpoonup> (OCaml) "Aarch64.lsr0" + +fun prerr_endline' :: "String.literal \<Rightarrow> unit" where "prerr_endline' _ = ()" +lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto + +fun putchar' :: "char \<Rightarrow> unit" where "putchar' _ = ()" +lemma [code]: "putchar c = putchar' (char_of_nat (nat c))" by auto + +code_identifier code_module List \<rightharpoonup> (OCaml) "List0" +code_printing constant String.implode \<rightharpoonup> (OCaml) "!(let l = _ in let res = Bytes.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> Bytes.set res i c; imp (i + 1) l in imp 0 l)" + +code_printing constant prerr_endline' \<rightharpoonup> (OCaml) "Pervasives.prerr'_endline" +code_printing constant putchar' \<rightharpoonup> (OCaml) "Pervasives.print'_char" + +fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exception) monadS" where + "write_char_mem addr c = + bindS (write_mem_eaS BC_bitU_list Write_plain (bits_of_int 64 addr) 1) (\<lambda>_. + bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\<lambda>_. + returnS ()))" + +definition "initial_state \<equiv> init_state initial_regstate (\<lambda>seed. (False, seed)) 0" + +code_printing constant elf_entry \<rightharpoonup> (OCaml) "(Int'_of'_integer (Elf'_loader.elf'_entry _))" +termination BigEndianReverse sorry +export_code main initial_state liftState get_regval set_regval bindS returnS iteriS iterS write_char_mem integer_of_int int_of_integer "op + :: int \<Rightarrow> int \<Rightarrow> int" prerr_results in OCaml module_name "Aarch64" file "aarch64_export.ml" + +end diff --git a/test/isabelle/Cheri_code.thy b/test/isabelle/Cheri_code.thy new file mode 100644 index 00000000..cfd01413 --- /dev/null +++ b/test/isabelle/Cheri_code.thy @@ -0,0 +1,62 @@ +theory Cheri_code + imports Cheri_lemmas "HOL-Library.Code_Char" "HOL-Library.Code_Target_Nat" "HOL-Library.Code_Target_Int" +begin + +declare [[code abort: failwith]] + +code_datatype + DADDIU DADDU DADDI DADD ADD ADDI ADDU ADDIU DSUBU DSUB SUB SUBU AND0 ANDI OR0 + ORI NOR XOR0 XORI LUI DSLL DSLL32 DSLLV DSRA DSRA32 DSRAV DSRL DSRL32 DSRLV SLL + SLLV SRA SRAV SRL SRLV SLT SLTI SLTU SLTIU MOVN MOVZ MFHI MFLO MTHI MTLO MUL + MULT MULTU DMULT DMULTU MADD MADDU MSUB MSUBU DIV DIVU DDIV DDIVU J JAL JR JALR + BEQ BCMPZ SYSCALL_THREAD_START ImplementationDefinedStopFetching SYSCALL BREAK + WAIT TRAPREG TRAPIMM Load Store LWL LWR SWL SWR LDL LDR SDL SDR CACHE PREF SYNC + MFC0 HCF MTC0 TLBWI TLBWR TLBR TLBP RDHWR ERET CGetPerm CGetType CGetBase + CGetLen CGetTag CGetSealed CGetOffset CGetPCC CGetPCCSetOffset CGetCause + CSetCause CReadHwr CWriteHwr CAndPerm CToPtr CSub CPtrCmp CIncOffset + CIncOffsetImmediate CSetOffset CSetBounds CSetBoundsImmediate CSetBoundsExact + CClearTag CMOVX ClearRegs CFromPtr CBuildCap CCopyType CCheckPerm CCheckType + CTestSubset CSeal CCSeal CUnseal CCall CReturn CBX CBZ CJALR CLoad CStore CSC + CLC C2Dump RI CGetAddr + +termination whileM sorry + +fun prerr_endline' :: "String.literal \<Rightarrow> unit" where "prerr_endline' _ = ()" +lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto + +fun putchar' :: "char \<Rightarrow> unit" where "putchar' _ = ()" +lemma [code]: "putchar c = putchar' (char_of_nat (nat c))" by auto + +code_identifier code_module List \<rightharpoonup> (OCaml) "List0" +code_printing constant String.implode \<rightharpoonup> (OCaml) "!(let l = _ in let res = Bytes.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> Bytes.set res i c; imp (i + 1) l in imp 0 l)" + +code_printing constant prerr_endline' \<rightharpoonup> (OCaml) "Pervasives.prerr'_endline" +code_printing constant putchar' \<rightharpoonup> (OCaml) "Pervasives.print'_char" + +declare insert_code[code del] +declare union_coset_filter[code del] + +lemma set_union_append[code]: "(set xs) \<union> (set ys) = set (xs @ ys)" + by auto + +lemma set_insert_Cons[code]: "insert x (set xs) = set (x # xs)" + by auto + +declare ast.case[code] + +fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exception) monadS" where + "write_char_mem addr c = + bindS (write_mem_eaS BC_bitU_list Write_plain (bits_of_int 64 addr) 1) (\<lambda>_. + bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\<lambda>_. + returnS ()))" + +definition "initial_state \<equiv> init_state initial_regstate (\<lambda>seed. (False, seed)) 0" + +code_printing constant elf_entry \<rightharpoonup> (OCaml) "(Arith.Int'_of'_integer (Elf'_loader.elf'_entry _))" +code_printing constant get_time_ns \<rightharpoonup> (OCaml) "(Arith.Int'_of'_integer (Big'_int.big'_int'_of'_int (Pervasives.int'_of'_float (1e9 *. Unix.gettimeofday _))))" + +export_code main initial_state liftState get_regval set_regval bindS returnS iteriS iterS + write_char_mem integer_of_int int_of_integer "op + :: int \<Rightarrow> int \<Rightarrow> int" prerr_results + in OCaml file "cheri_export.ml" + +end diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile new file mode 100644 index 00000000..43028fed --- /dev/null +++ b/test/isabelle/Makefile @@ -0,0 +1,27 @@ +CHERI_DIR = ../../cheri +AARCH64_DIR = ../../aarch64 +TGTS = run_cheri.native run_aarch64.native +SESSION_DIRS = -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . + +.PHONY: all clean + +all: $(TGTS) + +%.native: %.ml elf_loader.ml + ocamlbuild -use-ocamlfind -pkg lem -pkg linksem -pkg num -pkg unix $@ + +run_cheri.native: cheri_export.ml +run_aarch64.native: aarch64_export.ml + +cheri_export.ml: Cheri_code.thy + make -C $(CHERI_DIR) Cheri.thy + isabelle build -c $(SESSION_DIRS) Sail-CHERI-Code + +aarch64_export.ml: Aarch64_code.thy + make -C $(AARCH64_DIR) Aarch64.thy + isabelle build -c $(SESSION_DIRS) Sail-AArch64-Code + +clean: + -ocamlbuild -clean + -rm -f cheri_export.ml + -rm -f aarch64_export.ml diff --git a/test/isabelle/ROOT b/test/isabelle/ROOT new file mode 100644 index 00000000..97544a58 --- /dev/null +++ b/test/isabelle/ROOT @@ -0,0 +1,9 @@ +session "Sail-CHERI-Code" = "Sail-CHERI" + + options [document = false, quick_and_dirty] + theories + Cheri_code + +session "Sail-AArch64-Code" = "Sail-AArch64" + + options [document = false, quick_and_dirty] + theories + Aarch64_code diff --git a/test/isabelle/elf_loader.ml b/test/isabelle/elf_loader.ml new file mode 100644 index 00000000..6ec89ee6 --- /dev/null +++ b/test/isabelle/elf_loader.ml @@ -0,0 +1,126 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +(*module Big_int = Nat_big_num*) + +let opt_elf_threads = ref 1 +let opt_elf_entry = ref Nat_big_num.zero +let opt_elf_tohost = ref Nat_big_num.zero + +type word8 = int + +let escape_char c = + if int_of_char c <= 31 then '.' + else if int_of_char c >= 127 then '.' + else c + +let hex_line bs = + let hex_char i c = + (if i mod 2 == 0 && i <> 0 then " " else "") ^ Printf.sprintf "%02x" (int_of_char c) + in + String.concat "" (List.mapi hex_char bs) ^ " " ^ String.concat "" (List.map (fun c -> Printf.sprintf "%c" (escape_char c)) bs) + +let rec break n = function + | [] -> [] + | (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs) + +let print_segment seg = + let bs = seg.Elf_interpreted_segment.elf64_segment_body in + prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef"; + List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs)) + +let read name = + let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in + + prerr_endline "Elf read:"; + let (elf_file, elf_epi, symbol_map) = + begin match info with + | Error.Fail s -> failwith (Printf.sprintf "populate_and_obtain_global_symbol_init_info: %s" s) + | Error.Success ((elf_file: Elf_file.elf_file), + (elf_epi: Sail_interface.executable_process_image), + (symbol_map: Elf_file.global_symbol_init_info)) + -> + (* XXX disabled because it crashes if entry_point overflows an ocaml int :-( + prerr_endline (Sail_interface.string_of_executable_process_image elf_epi);*) + (elf_file, elf_epi, symbol_map) + end + in + + prerr_endline "\nElf segments:"; + let (segments, e_entry, e_machine) = + begin match elf_epi, elf_file with + | (Sail_interface.ELF_Class_32 _, _) -> failwith "cannot handle ELF_Class_32" + | (_, Elf_file.ELF_File_32 _) -> failwith "cannot handle ELF_File_32" + | (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 f1) -> + (* remove all the auto generated segments (they contain only 0s) *) + let segments = + Lem_list.mapMaybe + (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) + segments + in + (segments, e_entry, e_machine) + end + in + (segments, e_entry, symbol_map) + +(*let write_sail_lib paddr i byte = + Sail_lib.wram (Nat_big_num.add paddr (Nat_big_num.of_int i)) byte*) + +let write_file chan paddr i byte = + output_string chan (Nat_big_num.to_string (Nat_big_num.add paddr (Nat_big_num.of_int i)) ^ "\n"); + output_string chan (string_of_int byte ^ "\n") + +let load_elf name = + let segments, e_entry, symbol_map = read name in + opt_elf_entry := e_entry; + (if List.mem_assoc "tohost" symbol_map then + let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in + opt_elf_tohost := tohost_addr); + (*List.iter (load_segment ~writer:writer) segments*) + segments + +(* The sail model can access this by externing a unit -> Big_int.t function + as Elf_loader.elf_entry. *) +let elf_entry () = Big_int.big_int_of_string (Nat_big_num.to_string !opt_elf_entry) +(* Used by RISCV sail model test harness for exiting test *) +let elf_tohost () = Big_int.big_int_of_string (Nat_big_num.to_string !opt_elf_tohost) diff --git a/test/isabelle/run_aarch64.ml b/test/isabelle/run_aarch64.ml new file mode 100644 index 00000000..c6037866 --- /dev/null +++ b/test/isabelle/run_aarch64.ml @@ -0,0 +1,93 @@ +open Aarch64_export;; + + + +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Elf_loader;; + +let opt_file_arguments = ref ([] : string list) + +let options = Arg.align [] + +let usage_msg = "Sail OCaml RTS options:" + +let () = + Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg + +let (>>) = Aarch64.bindS +let liftS = Aarch64.liftState (Aarch64.get_regval, Aarch64.set_regval) + +let load_elf_segment seg = + let open Elf_interpreted_segment in + let open Aarch64_export in + let bs = seg.elf64_segment_body in + let paddr = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_paddr) in + let base = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_base) in + let offset = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_offset) in + let writer i byte = Aarch64.write_char_mem (Aarch64.plus_int (Aarch64.Int_of_integer paddr) i) byte in + prerr_endline "\nLoading Segment"; + prerr_endline ("Segment offset: " ^ Big_int.string_of_big_int offset); + prerr_endline ("Segment base address: " ^ Big_int.string_of_big_int base); + prerr_endline ("Segment physical address: " ^ Big_int.string_of_big_int paddr); + print_segment seg; + Aarch64.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs) + +let _ = + Random.self_init (); + let elf_segments = match !opt_file_arguments with + | f :: _ -> load_elf f + | _ -> [] + in + Aarch64.prerr_results + (Aarch64.initial_state |> + (Aarch64.iterS load_elf_segment elf_segments >> (fun _ -> + liftS (Aarch64.main ())))); diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml new file mode 100644 index 00000000..e6d752b7 --- /dev/null +++ b/test/isabelle/run_cheri.ml @@ -0,0 +1,92 @@ +open Cheri_export;; + + + +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Elf_loader;; + +let opt_file_arguments = ref ([] : string list) + +let options = Arg.align [] + +let usage_msg = "Sail OCaml RTS options:" + +let () = + Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg + +let (>>) = State_monad.bindS +let liftS = State.liftState (Cheri_types.get_regval, Cheri_types.set_regval) + +let load_elf_segment seg = + let open Elf_interpreted_segment in + let bs = seg.elf64_segment_body in + let paddr = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_paddr) in + let base = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_base) in + let offset = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_offset) in + let writer i byte = Cheri_code.write_char_mem (Arith.plus_int (Arith.Int_of_integer paddr) i) byte in + prerr_endline "\nLoading Segment"; + prerr_endline ("Segment offset: " ^ Big_int.string_of_big_int offset); + prerr_endline ("Segment base address: " ^ Big_int.string_of_big_int base); + prerr_endline ("Segment physical address: " ^ Big_int.string_of_big_int paddr); + print_segment seg; + State.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs) + +let _ = + Random.self_init (); + let elf_segments = match !opt_file_arguments with + | f :: _ -> load_elf f + | _ -> [] + in + (* State_monad.prerr_results *) + (Cheri_code.initial_state |> + (State.iterS load_elf_segment elf_segments >> (fun _ -> + liftS (Cheri.main ())))); diff --git a/test/isabelle/run_tests.sh b/test/isabelle/run_tests.sh new file mode 100755 index 00000000..7b3f7bc1 --- /dev/null +++ b/test/isabelle/run_tests.sh @@ -0,0 +1,90 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +cd $DIR +SAILDIR="$DIR/../.." +AARCH64_TEST_DIR="$DIR/../arm" + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +rm -f $DIR/tests.xml + +pass=0 +fail=0 +XML="" + +function green { + (( pass += 1 )) + printf "$1: ${GREEN}$2${NC}\n" + XML+=" <testcase name=\"$1\"/>\n" +} + +function yellow { + (( fail += 1 )) + printf "$1: ${YELLOW}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function red { + (( fail += 1 )) + printf "$1: ${RED}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function finish_suite { + printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n" + XML=" <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML </testsuite>\n" + printf "$XML" >> $DIR/tests.xml + XML="" + pass=0 + fail=0 +} + +SAILLIBDIR="$DIR/../../lib/" + +printf "<testsuites>\n" >> $DIR/tests.xml + +printf "Compiling AArch64 specification (Sail->Isabelle->OCaml)...\n" + +if make "run_aarch64.native" 1> /dev/null 2> /dev/null; +then + green "compiled no_vector specification" "ok"; + + for i in `ls ${AARCH64_TEST_DIR}/*.elf`; + do + $DIR/run_aarch64.native $i 2> /dev/null 1> ${i%.elf}.result + if diff ${i%.elf}.result ${i%.elf}.expect; + then + green "ran $(basename $i)" "ok" + else + red "failed $(basename $i)" "fail" + fi; + rm -f ${i%.elf}.result + done; +else + red "compiling no_vector specification" "fail"; + + for i in `ls ${AARCH64_TEST_DIR}/*.elf`; + do + red "failed $(basename $i)" "fail" + done +fi + +printf "Compiling CHERI specification (Sail->Isabelle->OCaml)...\n" + +if make "run_cheri.native" 1> /dev/null 2> /dev/null; +then + green "compiled CHERI-256 specification" "ok"; +else + red "compiling CHERI-256 specification" "fail"; +fi + +make clean 1> /dev/null 2> /dev/null + +finish_suite "Isabelle code generation tests" + +printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail index a6e34c8b..76cbbaed 100644 --- a/test/typecheck/pass/simple_record_access.sail +++ b/test/typecheck/pass/simple_record_access.sail @@ -1,4 +1,5 @@ $include <flow.sail> +$include <vector_inc.sail> enum signal = {LOW, HIGH} |