diff options
Diffstat (limited to 'test')
30 files changed, 1014 insertions, 598 deletions
diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh index d4e01079..f758d634 100755 --- a/test/arm/run_tests.sh +++ b/test/arm/run_tests.sh @@ -51,7 +51,7 @@ cd $SAILDIR/aarch64 printf "Compiling specification...\n" -if $SAILDIR/sail -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; +if $SAILDIR/sail -no_lexp_bounds_check -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; then green "compiled no_vector specification" "ok"; mv aarch64_test $DIR/; @@ -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 @@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n" cd $SAILDIR/aarch64 -if $SAILDIR/sail -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; +if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; then green "loaded no_vector specification" "ok"; 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/coq/run_tests.sh b/test/coq/run_tests.sh new file mode 100755 index 00000000..efca8275 --- /dev/null +++ b/test/coq/run_tests.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAILDIR="$DIR/../.." +TESTSDIR="$DIR/../typecheck/pass" + +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 +} + +printf "<testsuites>\n" >> $DIR/tests.xml + +cd $DIR + +for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`; +do + if $SAILDIR/sail -coq -o out $TESTSDIR/$i &>/dev/null; + then + if coqc -R ~/bbv bbv -R ../../../sail-private/coq-duopods/precise/lib Sail out_types.v out.v &>/dev/null; + then + green "tested $i expecting pass" "pass" + else + yellow "tested $i expecting pass" "failed to typecheck generated Coq" + fi + else + red "tested $i expecting pass" "failed to generate Coq" + fi +done + +finish_suite "Coq tests" + +printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/coq/skip b/test/coq/skip new file mode 100644 index 00000000..922cbbe1 --- /dev/null +++ b/test/coq/skip @@ -0,0 +1,12 @@ +XXXXX tests with undefined functions +bind_typ_var.sail +bitwise_not.* +bv_simple_index_bit.sail +ex_cast.sail +exint.sail +exist1.sail +exist2.sail +exist_subrange.sail +exist_tlb.sail +XXXXX tests with full generic equality +decode_patterns.sail
\ No newline at end of file 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/ocaml/bitfield/bitfield.sail b/test/ocaml/bitfield/bitfield.sail index 2a53ab3c..342b3d08 100644 --- a/test/ocaml/bitfield/bitfield.sail +++ b/test/ocaml/bitfield/bitfield.sail @@ -11,13 +11,6 @@ bitfield cr : bits(8) = { register CR : cr -bitfield dr : vector(4, inc, bit) = { - DR0 : 2 .. 3, - LT : 2 -} - -register DR : dr - val main : unit -> unit effect {rreg, wreg} function main () = { diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail index fab04306..74d2b8e5 100644 --- a/test/ocaml/lsl/lsl.sail +++ b/test/ocaml/lsl/lsl.sail @@ -1,6 +1,3 @@ -val zeros : forall ('n : Int), 'n >= 0. atom('n) -> bits('n) - -function zeros n = replicate_bits(0b0, 'n) val lslc : forall ('n : Int) ('shift : Int), 'n >= 1. (bits('n), atom('shift)) -> (bits('n), bit) effect {escape} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 5b046104..c2c5133f 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -1,21 +1,6 @@ default Order dec -type bits ('n : Int) = vector('n, dec, bit) - -infix 4 == - -val int : int <-> string -overload int = string_of_int - -val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool - -val eq_int = "eq_int" : (int, int) -> bool - -val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool +$include <prelude.sail> union option ('a : Type) = {None : unit, Some : 'a} @@ -37,286 +22,8 @@ val eq_anything = { val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) -overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything} - -val vector_subrange_dec = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) - -val vector_subrange_inc = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. - (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit) - -/* -val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int). - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) -*/ - -overload vector_subrange = {vector_subrange_dec, vector_subrange_inc} - -val vector_access_dec = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. - (vector('n, dec, 'a), atom('m)) -> 'a - -/* -val vector_access_B = "access" : forall ('n : Int) ('a : Type). - (vector('n, dec, 'a), int) -> 'a -*/ - -overload vector_access = {vector_access_dec} - -val vector_update = "update" : forall 'n ('a : Type). - (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) - -val vector_update_subrange_dec = "update_subrange" : forall 'n 'm 'o. - (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) - -val vector_update_subrange_inc = "update_subrange" : forall 'n 'm 'o. - (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) - -overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} - -val vcons : forall ('n : Int) ('a : Type). - ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) - -val append = "append" : forall ('n : Int) ('m : Int) ('a : Type). - (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) - -val not_bool = "not" : bool -> bool - -val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) +overload operator == = {eq_string, eq_real, eq_anything} overload ~ = {not_bool, not_vec} -val neq_atom : forall 'n 'm. (atom('n), atom('m)) -> bool - -function neq_atom (x, y) = not_bool(eq_atom(x, y)) - -val neq_int : (int, int) -> bool - -function neq_int (x, y) = not_bool(eq_int(x, y)) - -val neq_vec : forall 'n. (bits('n), bits('n)) -> bool - -function neq_vec (x, y) = not_bool(eq_vec(x, y)) - -val neq_anything : forall ('a : Type). ('a, 'a) -> bool - -function neq_anything (x, y) = not_bool(x == y) - -overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} - -val and_bool = "and_bool" : (bool, bool) -> bool - -val builtin_and_vec = "and_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n) - -function and_vec (xs, ys) = builtin_and_vec(xs, ys) - -overload operator & = {and_bool, and_vec} - -val or_bool = "or_bool" : (bool, bool) -> bool - -val builtin_or_vec = "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n) - -function or_vec (xs, ys) = builtin_or_vec(xs, ys) - -overload operator | = {or_bool, or_vec} - -val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) - -val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) - -val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) - -val __SetSlice_bits = "set_slice" : forall 'n 'm. - (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) - -val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int - -val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int - -val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) - -val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) - -function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) - -val __raw_SetSlice_bits : forall 'n 'w. - (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) - -val __raw_GetSlice_bits : forall 'n 'w. - (atom('n), atom('w), bits('n), int) -> bits('w) - -val __ShiftLeft : forall 'm. (bits('m), int) -> bits('m) - -val __SignExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) - -val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) - -val cast cast_unit_vec : bit -> bits(1) - -function cast_unit_vec bitone = 0b1 -and cast_unit_vec bitzero = 0b0 - val print = "print_endline" : string -> unit - -val string_of_int = "string_of_int" : int -> string - -val putchar = "putchar" : forall ('a : Type). 'a -> unit - -val concat_str = "concat_str" : (string, string) -> string - -val DecStr : int -> string - -val HexStr : int -> string - -val BitStr = "string_of_bits" : forall 'n. bits('n) -> string - -val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val int_power : (int, int) -> int - -val real_power = "real_power" : (real, int) -> real - -overload operator ^ = {xor_vec, int_power, real_power} - -val add_range = "add_int" : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val add_int = "add_int" : (int, int) -> int - -val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) - -val add_real = "add_real" : (real, real) -> real - -overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} - -val sub_range = "sub_int" : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val sub_int = "sub_int" : (int, int) -> int - -val sub_nat = "sub_int" : (nat, nat) -> nat - -val sub_vec : forall 'n. (bits('n), bits('n)) -> bits('n) - -val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) - -val sub_real = "sub_real" : (real, real) -> real - -val negate_range = "negate" : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) - -val negate_int = "negate" : int -> int - -val negate_real = "negate_real" : real -> real - -overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} - -overload negate = {negate_range, negate_int, negate_real} - -val mult_range = "mult" : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) - -val mult_int = "mult" : (int, int) -> int - -val mult_real = "mult_real" : (real, real) -> real - -overload operator * = {mult_range, mult_int, mult_real} - -val Sqrt = "sqrt_real" : real -> real - -val gteq_int = "gteq" : (int, int) -> bool - -val gteq_real = "gteq_real" : (real, real) -> bool - -overload operator >= = {gteq_atom, gteq_int, gteq_real} - -val lteq_int = "lteq" : (int, int) -> bool - -val lteq_real = "lteq_real" : (real, real) -> bool - -overload operator <= = {lteq_atom, lteq_int, lteq_real} - -val gt_int = "gt" : (int, int) -> bool - -val gt_real = "gt_real" : (real, real) -> bool - -overload operator > = {gt_atom, gt_int, gt_real} - -val lt_int = "lt" : (int, int) -> bool - -val lt_real = "lt_real" : (real, real) -> bool - -overload operator < = {lt_atom, lt_int, lt_real} - -val RoundDown = "round_down" : real -> int - -val RoundUp = "round_up" : real -> int - -val abs = "abs_num" : real -> real - -val quotient_nat = "quotient" : (nat, nat) -> nat - -val quotient_real = "quotient_real" : (real, real) -> real - -val quotient = "quotient" : (int, int) -> int - -infixl 7 / - -overload operator / = {quotient_nat, quotient, quotient_real} - -val modulus = "modulus" : (int, int) -> int - -infixl 7 % - -overload operator % = {modulus} - -val Real = "to_real" : int -> real - -val shl_int = "shl_int" : (int, int) -> int - -val shr_int = "shr_int" : (int, int) -> int - -val min_nat = "min_int" : (nat, nat) -> nat - -val min_int = "min_int" : (int, int) -> int - -val max_nat = "max_int" : (nat, nat) -> nat - -val max_int = "max_int" : (int, int) -> int - -overload min = {min_nat, min_int} - -overload max = {max_nat, max_int} - -val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) - -val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} - -function ex_nat 'n = n - -val cast ex_int : int -> {'n, true. atom('n)} - -function ex_int 'n = n - -val ex_range : forall 'n 'm. - range('n, 'm) -> {'o, 'n <= 'o & 'o <= 'm. atom('o)} - -val coerce_int_nat : int -> nat effect {escape} - -function coerce_int_nat 'x = { - assert(constraint('x >= 0)); - x -} - -val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. - (bits('m), int, atom('n)) -> bits('n) - -val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) - -val "print_int" : (string, int) -> unit - -val "print_bits" : forall 'n. (string, bits('n)) -> unit diff --git a/test/ocaml/string_of_struct/sos.sail b/test/ocaml/string_of_struct/sos.sail index 69a17e6c..ecef0e36 100644 --- a/test/ocaml/string_of_struct/sos.sail +++ b/test/ocaml/string_of_struct/sos.sail @@ -2,11 +2,6 @@ struct would cause the ocaml backend to generate a bad string_of function for the struct */ -union option ('a : Type) = { - None : unit, - Some : 'a -} - struct test = { test1 : int, test2 : option(int) diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail index d13b527c..6790140e 100644 --- a/test/ocaml/types/types.sail +++ b/test/ocaml/types/types.sail @@ -24,8 +24,6 @@ struct TestStruct = { register SREG : TestStruct -union option ('a : Type) = {None : unit, Some : 'a} - register OREG : option(byte) val main : unit -> unit effect {rreg, wreg} diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail index 5afd421d..ac44d9ae 100644 --- a/test/ocaml/vec_32_64/vec_32_64.sail +++ b/test/ocaml/vec_32_64/vec_32_64.sail @@ -8,11 +8,6 @@ function get_size () = 32 val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit -val zeros : forall 'n. atom('n) -> vector('n, dec, bit) - -function zeros n = - if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1) - val main : unit -> unit function main () = { diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail index d93143f0..2021bf67 100644 --- a/test/typecheck/pass/arm_FPEXC1.sail +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -1,12 +1,12 @@ default Order dec -val vector_access = {ocaml: "access", lem: "access_vec_dec"}: forall ('n : Int). +val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int). (vector('n, dec, bit), int) -> bit -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) -val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. +val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit) register _FPEXC32_EL2 : vector(32, dec, bit) diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail index 4e030a60..d2549e01 100644 --- a/test/typecheck/pass/atomcase.sail +++ b/test/typecheck/pass/atomcase.sail @@ -2,7 +2,7 @@ default Order dec infix 4 == -val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int). +val eq_atom = {ocaml: "eq_atom", lem: "eq", coq: "Z.eqb"}: forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> bool overload operator == = {eq_atom} diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail index 991cd828..261e3b44 100644 --- a/test/typecheck/pass/deinfix_plus.sail +++ b/test/typecheck/pass/deinfix_plus.sail @@ -1,6 +1,6 @@ default Order inc -val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). +val bv_add = {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) overload operator + = {bv_add} diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 47343e02..96b1ecf1 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -8,14 +8,14 @@ register x : nat register y : nat -val eq_int = {lem: "eq"} : (int, int) -> bool -val eq_vec = {lem: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool +val eq_int = {lem: "eq", coq: "Z.eqb"} : (int, int) -> bool +val eq_vec = {lem: "eq_vec", coq: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool overload operator == = {eq_int, eq_vec} -val "and_bool" : (bool, bool) -> bool +val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc", coq: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit) type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)} diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail index 6763922a..dc625084 100644 --- a/test/typecheck/pass/nzcv.sail +++ b/test/typecheck/pass/nzcv.sail @@ -10,6 +10,6 @@ function test nzcv = { Z = 0b0; C = 0b0; V = 0b0; - (N, Z, C, V) = nzcv; + (N @ Z @ C @ V) = nzcv; () } 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} diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail index c148e6da..84b4f7b4 100644 --- a/test/typecheck/pass/while_PM.sail +++ b/test/typecheck/pass/while_PM.sail @@ -22,10 +22,12 @@ val vector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n. register GPR00 : vector(64, dec, bit) +/* FIXME: Currently this doesn't work in lem function test b : bit -> unit = { - i : int = 0; + i : range(0, 64) = 0; while i < 64 do { GPR00[i] = b; - i = i + 1 + i = i + 1; } } +*/
\ No newline at end of file |