summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/vector_dec.sail2
-rw-r--r--src/gen_lib/sail_operators.lem12
-rw-r--r--src/gen_lib/sail_operators_bitlists.lem17
-rw-r--r--src/gen_lib/sail_operators_mwords.lem17
-rw-r--r--test/builtins/get_slice_int.sail36
-rwxr-xr-xtest/builtins/run_tests.sh48
-rw-r--r--test/builtins/set_slice_bits.sail2
-rw-r--r--test/builtins/signed.sail120
-rw-r--r--test/builtins/test_extras.lem22
-rw-r--r--test/builtins/unsigned6.sail392
-rw-r--r--test/typecheck/pass/simple_record_access.sail1
11 files changed, 403 insertions, 266 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 1307bb56..17603e03 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -68,11 +68,13 @@ val vector_update = {
val add_bits = {
ocaml: "add_vec",
+ lem: "add_vec",
c: "add_bits"
} : forall 'n. (bits('n), bits('n)) -> bits('n)
val add_bits_int = {
ocaml: "add_vec_int",
+ lem: "add_vec_int",
c: "add_bits_int"
} : forall 'n. (bits('n), int) -> bits('n)
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..78aab65e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -223,3 +223,15 @@ let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedInteger
val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
+
+val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int_bv len n lo =
+ let hi = lo + len - 1 in
+ let bs = bools_of_int (hi + 1) n in
+ of_bools (subrange_list false bs hi lo)
+
+val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+let set_slice_int_bv len n lo v =
+ let hi = lo + len - 1 in
+ let bs = bits_of_int (hi + 1) n in
+ maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index b0a29b5e..fed293b4 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -35,6 +35,9 @@ let zero_extend bits len = extz_bits len bits
val sign_extend : list bitU -> integer -> list bitU
let sign_extend bits len = exts_bits len bits
+val zeros : integer -> list bitU
+let zeros len = repeat [B0] len
+
val vector_truncate : list bitU -> integer -> list bitU
let vector_truncate bs len = extz_bv len bs
@@ -289,6 +292,20 @@ let duplicate_oracle b n =
val reverse_endianness : list bitU -> list bitU
let reverse_endianness v = reverse_endianness_list v
+val get_slice_int : integer -> integer -> integer -> list bitU
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+ subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+ update_subrange_vec_dec out (n + slice_len - 1) n v
+
val eq_vec : list bitU -> list bitU -> bool
val neq_vec : list bitU -> list bitU -> bool
val ult_vec : list bitU -> list bitU -> bool
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8bcc0319..077dfb02 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -76,6 +76,9 @@ let zero_extend w _ = Machine_word.zeroExtend w
val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let sign_extend w _ = Machine_word.signExtend w
+val zeros : forall 'a. Size 'a => integer -> mword 'a
+let zeros _ = Machine_word.wordFromNatural 0
+
val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let vector_truncate w _ = Machine_word.zeroExtend w
@@ -310,6 +313,20 @@ let duplicate b n = maybe_failwith (duplicate_maybe b n)
val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let slice v lo len =
+ subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+ update_subrange_vec_dec out (n + slice_len - 1) n v
+
val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
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/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}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:45:07 +0000