Run ARM built-in tests for Lem backend (via OCaml)

1 files changed, 63 insertions, 57 deletions

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
+}