diff options
Diffstat (limited to 'test')
25 files changed, 2334 insertions, 31 deletions
diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh index f758d634..30f955b0 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 -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; +if $SAILDIR/sail -no_lexp_bounds_check -o aarch64_test -ocaml no_vector.sail 1> /dev/null 2> /dev/null; then green "compiled no_vector specification" "ok"; mv aarch64_test $DIR/; @@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n" cd $SAILDIR/aarch64 -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; +if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail no_vector.sail 1> /dev/null 2> /dev/null; then green "loaded no_vector specification" "ok"; diff --git a/test/builtins/test_extras.lem b/test/builtins/test_extras.lem index 136f680e..ae3ed1ba 100644 --- a/test/builtins/test_extras.lem +++ b/test/builtins/test_extras.lem @@ -17,6 +17,3 @@ 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/c/cheri_capreg.expect b/test/c/cheri_capreg.expect new file mode 100644 index 00000000..6e46a0e8 --- /dev/null +++ b/test/c/cheri_capreg.expect @@ -0,0 +1,10 @@ +default_cap = 0b10000000000000000000000000000000011111111111111110000111111111110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 +null_cap = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 +C03 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +C02 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +C01 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +DDC = 0b10000000000000000000000000000000011111111111111110000111111111110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 +C03 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 +C02 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 +C01 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 +DDC = 0b10000000000000000000000000000000011111111111111110000111111111110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111 diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail new file mode 100644 index 00000000..e8890a4a --- /dev/null +++ b/test/c/cheri_capreg.sail @@ -0,0 +1,254 @@ +default Order dec + +/* this is here because if we don't have it before including vector_dec + we get infinite loops caused by interaction with bool/bit casts */ +val eq_bit2 = "eq_bit" : (bit, bit) -> bool +overload operator == = {eq_bit2} + +$include <vector_dec.sail> + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +/* sneaky deref with no effect necessary for bitfield writes */ +val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a + +val zeros_0 = "zeros" : forall 'n. int('n) -> bits('n) + +val zeros : forall 'n. unit -> bits('n) +function zeros() = zeros_0('n) + +val ones : forall 'n, 'n >= 0 . unit -> bits('n) +function ones() = replicate_bits (0b1,'n) + +val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +val int_power = {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int + +overload operator ^ = {xor_vec, int_power} + +val cast bool_to_bits : bool -> bits(1) +function bool_to_bits x = if x then 0b1 else 0b0 + +val cast bit_to_bool : bit -> bool +function bit_to_bool b = match b { + bitone => true, + bitzero => false +} + +val to_bits : forall 'l, 'l >= 0 .(atom('l), int) -> bits('l) +function to_bits (l, n) = get_slice_int(l, n, 0) + +/* 256 bit cap + tag */ +type CapReg = bits(257) + +struct CapStruct = { + tag : bool , + padding : bits(8) , + otype : bits(24), + uperms : bits(16), + perm_reserved11_14 : bits(4) , + access_system_regs : bool , + permit_unseal : bool , + permit_ccall : bool , + permit_seal : bool , + permit_store_local_cap : bool , + permit_store_cap : bool , + permit_load_cap : bool , + permit_store : bool , + permit_load : bool , + permit_execute : bool , + global : bool , + sealed : bool , + address : bits(64), + base : bits(64), + length : bits(64), +} + +let null_cap : CapStruct = struct { + tag = false, + padding = zeros(), + otype = zeros(), + uperms = zeros(), + perm_reserved11_14 = zeros(), + access_system_regs = false, + permit_unseal = false, + permit_ccall = false, + permit_seal = false, + permit_store_local_cap = false, + permit_store_cap = false, + permit_load_cap = false, + permit_store = false, + permit_load = false, + permit_execute = false, + global = false, + sealed = false, + address = zeros(), + base = zeros(), + length = 0xffffffffffffffff +} + +let default_cap : CapStruct = struct { + tag = true, + padding = zeros(), + otype = zeros(), + uperms = ones(), + perm_reserved11_14 = zeros(), + access_system_regs = true, + permit_unseal = true, + permit_ccall = true, + permit_seal = true, + permit_store_local_cap = true, + permit_store_cap = true, + permit_load_cap = true, + permit_store = true, + permit_load = true, + permit_execute = true, + global = true, + sealed = false, + address = zeros(), + base = zeros(), + length = 0xffffffffffffffff +} + +let null_cap : CapStruct = struct { + tag = false, + padding = zeros(), + otype = zeros(), + uperms = zeros(), + perm_reserved11_14 = zeros(), + access_system_regs = false, + permit_unseal = false, + permit_ccall = false, + permit_seal = false, + permit_store_local_cap = false, + permit_store_cap = false, + permit_load_cap = false, + permit_store = false, + permit_load = false, + permit_execute = false, + global = false, + sealed = false, + address = zeros(), + base = zeros(), + length = 0xffffffffffffffff +} + +let 'cap_size = 32 + +function capRegToCapStruct(capReg) : CapReg -> CapStruct = + struct { + tag = capReg[256], + padding = capReg[255..248], + otype = capReg[247..224], + uperms = capReg[223..208], + perm_reserved11_14 = capReg[207..204], + access_system_regs = capReg[203], + permit_unseal = capReg[202], + permit_ccall = capReg[201], + permit_seal = capReg[200], + permit_store_local_cap = capReg[199], + permit_store_cap = capReg[198], + permit_load_cap = capReg[197], + permit_store = capReg[196], + permit_load = capReg[195], + permit_execute = capReg[194], + global = capReg[193], + sealed = capReg[192], + address = capReg[191..128], + base = capReg[127..64], + length = capReg[63..0] + } + +function getCapPerms(cap) : CapStruct -> bits(31) = + ( + cap.uperms + @ cap.perm_reserved11_14 + @ cap.access_system_regs + @ cap.permit_unseal + @ cap.permit_ccall + @ cap.permit_seal + @ cap.permit_store_local_cap + @ cap.permit_store_cap + @ cap.permit_load_cap + @ cap.permit_store + @ cap.permit_load + @ cap.permit_execute + @ cap.global + ) + + +/* Function to convert capabilities to in-memory format. */ +function capStructToMemBits256(cap) : CapStruct -> bits(256) = + ( + cap.padding + @ cap.otype + @ getCapPerms(cap) + @ cap.sealed + @ cap.address + @ cap.base + @ cap.length + ) + + +/* When saving/restoring capabilities xor them with bits of null_cap -- + this ensures that canonical null_cap is always all-zeros in memory + even though it may have bits set logically (e.g. length or exponent) */ + +let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) + +function capStructToMemBits(cap) : CapStruct -> bits(256)= + capStructToMemBits256(cap) ^ null_cap_bits + +function memBitsToCapBits(tag, b) : (bool, bits(256)) -> bits(257) = + tag @ (b ^ null_cap_bits) + +function capStructToCapReg(cap) : CapStruct -> CapReg = cap.tag @ capStructToMemBits256(cap) + +register DDC : CapReg +register C01 : CapReg +register C02 : CapReg +register C03 : CapReg + +let CapRegs : vector(4, dec, register(CapReg)) = + [ + ref C03, + ref C02, + ref C01, + ref DDC + ] + +val readCapReg : bits(2) -> CapStruct effect {rreg} +function readCapReg(n) = + if (n == 0b00) then + default_cap + else + let i = unsigned(n) in + capRegToCapStruct(reg_deref(CapRegs[i])) + +function writeCapReg(n, cap) : (bits(2), CapStruct) -> unit = + if (n == 0b00) then + () + else + let i = unsigned(n) in + (*CapRegs[i]) = capStructToCapReg(cap) + +val "print_bits" : forall 'n. (string, bits('n)) -> unit + +val main : unit -> unit effect {rreg, wreg} + +function main() = { + print_bits("default_cap = ", capStructToCapReg(default_cap)); + print_bits("null_cap = ", capStructToCapReg(null_cap)); + DDC = capStructToCapReg(default_cap); + print_bits("C03 = ", C03); + print_bits("C02 = ", C02); + print_bits("C01 = ", C01); + print_bits("DDC = ", DDC); + foreach(i from 1 to 3) { + let idx = to_bits(2, i); + writeCapReg(idx, null_cap) + }; + print_bits("C03 = ", C03); + print_bits("C02 = ", C02); + print_bits("C01 = ", C01); + print_bits("DDC = ", DDC); +}
\ No newline at end of file diff --git a/test/c/eq_struct.expect b/test/c/eq_struct.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/eq_struct.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail new file mode 100644 index 00000000..b4258569 --- /dev/null +++ b/test/c/eq_struct.sail @@ -0,0 +1,38 @@ +default Order dec + +$include <flow.sail> +$include <exception_basic.sail> + +val eq = "eq_anything" : forall ('a : Type). ('a, 'a) -> bool + +overload operator == = {eq} + +val neq : forall ('a : Type). ('a, 'a) -> bool + +overload operator != = {neq} + +overload ~ = {not_bool} + +function neq(x, y) = ~(eq(x, y)) + +struct S = { + field1: int, + field2: vector(8, dec, bit) +} + +val "print" : string -> unit + +val main : unit -> unit effect {escape} + +function main() = { + let s : S = struct { + field1 = 4, + field2 = 0xFF + }; + assert(s == s, "1"); + assert(~(s == { s with field2 = 0xAB }), "2"); + assert(s != { s with field1 = 5}, "3"); + assert(s == { s with field2 = 0xFF }); + assert({ s with field1 = 0} == {s with field1 = 0}); + print("ok\n") +}
\ No newline at end of file diff --git a/test/c/foreach_none.expect b/test/c/foreach_none.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/foreach_none.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/foreach_none.sail b/test/c/foreach_none.sail new file mode 100644 index 00000000..bc960b85 --- /dev/null +++ b/test/c/foreach_none.sail @@ -0,0 +1,11 @@ + +val "print" : string -> unit + +val main : unit -> unit + +function main() = { + foreach (i from 0 to -1 by 1 in inc) { + print("unreachable\n"); + }; + print("ok\n") +}
\ No newline at end of file diff --git a/test/c/gvectorlit.expect b/test/c/gvectorlit.expect index d3a1e9ab..9328600c 100644 --- a/test/c/gvectorlit.expect +++ b/test/c/gvectorlit.expect @@ -1,2 +1,2 @@ -x[0] = 0xAB -x[1] = 0xCD +x[0] = 0xCD +x[1] = 0xAB diff --git a/test/c/large_bitvector.expect b/test/c/large_bitvector.expect new file mode 100644 index 00000000..f67ec84a --- /dev/null +++ b/test/c/large_bitvector.expect @@ -0,0 +1,12 @@ +x = 0x1FFFF0000FFFFFFFF +length(x) = 68 +y = 0x1FFFF0000FFFFFFFF1FFFF0000FFFFFFFF1FFFF0000FFFFFFFF +length(y) = 204 +z = 0x1FFFF0000FFFFFFFF1FFFF0000FFFFFFFF1CAFE0000FFFFFFFF +length(z) = 204 +q = 0xFF0000FFFFFFFF1FFFF0000FFFFFFFF1CAFE0000FFFFFFFF +w = -24519554509435141245919758063389544641259977658452672513 +length(q) = 192 +0x8000 +0b1 @ zeros(64 * 3 - 1) = 0x800000000000000000000000000000000000000000000000 +q = 0x800000000000000000000000000000000000000000000000 diff --git a/test/c/large_bitvector.sail b/test/c/large_bitvector.sail new file mode 100644 index 00000000..78189d7d --- /dev/null +++ b/test/c/large_bitvector.sail @@ -0,0 +1,30 @@ +default Order dec + +$include <arith.sail> +$include <vector_dec.sail> + +val "zeros" : forall 'n. int('n) -> bits('n) + +val main : unit -> unit + +function main() = { + let x = [0x1FFFF0000FFFF0000 with 15 .. 0 = 0xFFFF]; + print_bits("x = ", x); + print_int("length(x) = ", length(x)); + let y = replicate_bits(x, 3); + print_bits("y = ", y); + print_int("length(y) = ", length(y)); + let z = [y with 63 .. (63 - 15) = 0xCAFE]; + print_bits("z = ", z); + print_int("length(z) = ", length(z)); + q = slice(z, 0, 64 * 3); + print_bits("q = ", q); + w = signed(q); + print_int("w = ", w); + print_int("length(q) = ", length(q)); + print_bits("", [0xFFFF with 14 .. 0 = zeros(15)]); + print_bits("0b1 @ zeros(64 * 3 - 1) = ", 0b1 @ zeros(64 * 3 - 1)); + q[64 * 3 - 2 .. 0] = zeros(64 * 3 - 1); + print_bits("q = ", q); + () +} diff --git a/test/cheri/cheribsd-cheri-sim-mdroot-smoketest-kernel.bz2 b/test/cheri/cheribsd-cheri-sim-mdroot-smoketest-kernel.bz2 Binary files differnew file mode 100644 index 00000000..61954cd3 --- /dev/null +++ b/test/cheri/cheribsd-cheri-sim-mdroot-smoketest-kernel.bz2 diff --git a/test/cheri/freebsd-beri-sim-mdroot-smoketest_bootonly-kernel.bz2 b/test/cheri/freebsd-beri-sim-mdroot-smoketest_bootonly-kernel.bz2 Binary files differnew file mode 100644 index 00000000..33794547 --- /dev/null +++ b/test/cheri/freebsd-beri-sim-mdroot-smoketest_bootonly-kernel.bz2 diff --git a/test/cheri/run_tests.sh b/test/cheri/run_tests.sh index 4e1550f4..337974d7 100755 --- a/test/cheri/run_tests.sh +++ b/test/cheri/run_tests.sh @@ -65,6 +65,17 @@ else red "Building MIPS_C specification" "fail" fi +printf "Booting FreeBSD-MIPS...\n" + +bunzip2 -fk freebsd-beri-sim-mdroot-smoketest_bootonly-kernel.bz2 +time $SAILDIR/mips/mips_c --cyclelimit 85000000 --binary 0x100000,freebsd-beri-sim-mdroot-smoketest_bootonly-kernel --binary 0x7f010000,sim.dtb --image simboot_128m.sailbin > freebsd_out.txt +if grep -q 'Done booting' freebsd_out.txt; +then + green "Booting FreeBSD MIPS" "ok" +else + red "Booting FreeBSD MIPS" "fail" +fi + printf "Building CHERI 256 specification...\n" if make -C $SAILDIR/cheri cheri ; diff --git a/test/cheri/sim.dtb b/test/cheri/sim.dtb Binary files differnew file mode 100644 index 00000000..2561f997 --- /dev/null +++ b/test/cheri/sim.dtb diff --git a/test/cheri/simboot_128m.sailbin b/test/cheri/simboot_128m.sailbin new file mode 100644 index 00000000..bd6f5c28 --- /dev/null +++ b/test/cheri/simboot_128m.sailbin @@ -0,0 +1,1794 @@ +1073741824 +60 +1073741825 +30 +1073741826 +0 +1073741827 +0 +1073741828 +103 +1073741829 +222 +1073741830 +0 +1073741831 +0 +1073741832 +0 +1073741833 +30 +1073741834 +244 +1073741835 +56 +1073741836 +103 +1073741837 +222 +1073741838 +135 +1073741839 +240 +1073741840 +0 +1073741841 +30 +1073741842 +244 +1073741843 +56 +1073741844 +103 +1073741845 +222 +1073741846 +252 +1073741847 +0 +1073741848 +60 +1073741849 +29 +1073741850 +0 +1073741851 +0 +1073741852 +103 +1073741853 +189 +1073741854 +0 +1073741855 +0 +1073741856 +0 +1073741857 +29 +1073741858 +236 +1073741859 +56 +1073741860 +103 +1073741861 +189 +1073741862 +135 +1073741863 +240 +1073741864 +0 +1073741865 +29 +1073741866 +236 +1073741867 +56 +1073741868 +103 +1073741869 +189 +1073741870 +252 +1073741871 +0 +1073741872 +103 +1073741873 +189 +1073741874 +255 +1073741875 +224 +1073741876 +64 +1073741877 +1 +1073741878 +96 +1073741879 +0 +1073741880 +52 +1073741881 +33 +1073741882 +0 +1073741883 +224 +1073741884 +64 +1073741885 +129 +1073741886 +96 +1073741887 +0 +1073741888 +64 +1073741889 +12 +1073741890 +128 +1073741891 +0 +1073741892 +53 +1073741893 +140 +1073741894 +0 +1073741895 +7 +1073741896 +57 +1073741897 +140 +1073741898 +0 +1073741899 +5 +1073741900 +64 +1073741901 +140 +1073741902 +128 +1073741903 +0 +1073741904 +60 +1073741905 +12 +1073741906 +144 +1073741907 +0 +1073741908 +101 +1073741909 +140 +1073741910 +0 +1073741911 +0 +1073741912 +0 +1073741913 +12 +1073741914 +100 +1073741915 +56 +1073741916 +101 +1073741917 +140 +1073741918 +64 +1073741919 +0 +1073741920 +0 +1073741921 +12 +1073741922 +100 +1073741923 +56 +1073741924 +101 +1073741925 +140 +1073741926 +0 +1073741927 +124 +1073741928 +52 +1073741929 +13 +1073741930 +152 +1073741931 +0 +1073741932 +0 +1073741933 +13 +1073741934 +108 +1073741935 +60 +1073741936 +1 +1073741937 +141 +1073741938 +96 +1073741939 +37 +1073741940 +1 +1073741941 +128 +1073741942 +0 +1073741943 +8 +1073741944 +0 +1073741945 +0 +1073741946 +0 +1073741947 +0 +1073741948 +64 +1073741949 +12 +1073741950 +120 +1073741951 +0 +1073741952 +49 +1073741953 +140 +1073741954 +255 +1073741955 +0 +1073741956 +57 +1073741957 +173 +1073741958 +137 +1073741959 +0 +1073741960 +17 +1073741961 +141 +1073741962 +0 +1073741963 +11 +1073741964 +36 +1073741965 +2 +1073741966 +0 +1073741967 +0 +1073741968 +64 +1073741969 +44 +1073741970 +120 +1073741971 +6 +1073741972 +49 +1073741973 +130 +1073741974 +255 +1073741975 +255 +1073741976 +64 +1073741977 +44 +1073741978 +120 +1073741979 +7 +1073741980 +0 +1073741981 +12 +1073741982 +28 +1073741983 +2 +1073741984 +32 +1073741985 +99 +1073741986 +0 +1073741987 +1 +1073741988 +49 +1073741989 +140 +1073741990 +255 +1073741991 +255 +1073741992 +112 +1073741993 +67 +1073741994 +16 +1073741995 +2 +1073741996 +0 +1073741997 +76 +1073741998 +16 +1073741999 +32 +1073742000 +20 +1073742001 +64 +1073742002 +0 +1073742003 +55 +1073742004 +0 +1073742005 +0 +1073742006 +0 +1073742007 +0 +1073742008 +36 +1073742009 +1 +1073742010 +0 +1073742011 +0 +1073742012 +36 +1073742013 +2 +1073742014 +0 +1073742015 +0 +1073742016 +36 +1073742017 +3 +1073742018 +0 +1073742019 +0 +1073742020 +36 +1073742021 +8 +1073742022 +0 +1073742023 +0 +1073742024 +36 +1073742025 +9 +1073742026 +0 +1073742027 +0 +1073742028 +36 +1073742029 +10 +1073742030 +0 +1073742031 +0 +1073742032 +36 +1073742033 +11 +1073742034 +0 +1073742035 +0 +1073742036 +36 +1073742037 +12 +1073742038 +0 +1073742039 +0 +1073742040 +36 +1073742041 +13 +1073742042 +0 +1073742043 +0 +1073742044 +36 +1073742045 +14 +1073742046 +0 +1073742047 +0 +1073742048 +36 +1073742049 +15 +1073742050 +0 +1073742051 +0 +1073742052 +36 +1073742053 +16 +1073742054 +0 +1073742055 +0 +1073742056 +36 +1073742057 +17 +1073742058 +0 +1073742059 +0 +1073742060 +36 +1073742061 +18 +1073742062 +0 +1073742063 +0 +1073742064 +36 +1073742065 +19 +1073742066 +0 +1073742067 +0 +1073742068 +36 +1073742069 +20 +1073742070 +0 +1073742071 +0 +1073742072 +36 +1073742073 +21 +1073742074 +0 +1073742075 +0 +1073742076 +36 +1073742077 +22 +1073742078 +0 +1073742079 +0 +1073742080 +36 +1073742081 +23 +1073742082 +0 +1073742083 +0 +1073742084 +36 +1073742085 +24 +1073742086 +0 +1073742087 +0 +1073742088 +36 +1073742089 +25 +1073742090 +0 +1073742091 +0 +1073742092 +36 +1073742093 +26 +1073742094 +0 +1073742095 +0 +1073742096 +36 +1073742097 +27 +1073742098 +0 +1073742099 +0 +1073742100 +36 +1073742101 +28 +1073742102 +0 +1073742103 +0 +1073742104 +0 +1073742105 +32 +1073742106 +0 +1073742107 +17 +1073742108 +0 +1073742109 +32 +1073742110 +0 +1073742111 +19 +1073742112 +36 +1073742113 +4 +1073742114 +0 +1073742115 +0 +1073742116 +60 +1073742117 +5 +1073742118 +144 +1073742119 +0 +1073742120 +100 +1073742121 +165 +1073742122 +0 +1073742123 +0 +1073742124 +0 +1073742125 +5 +1073742126 +44 +1073742127 +56 +1073742128 +100 +1073742129 +165 +1073742130 +64 +1073742131 +0 +1073742132 +0 +1073742133 +5 +1073742134 +44 +1073742135 +56 +1073742136 +100 +1073742137 +165 +1073742138 +3 +1073742139 +112 +1073742140 +60 +1073742141 +6 +1073742142 +144 +1073742143 +0 +1073742144 +100 +1073742145 +198 +1073742146 +0 +1073742147 +0 +1073742148 +0 +1073742149 +6 +1073742150 +52 +1073742151 +56 +1073742152 +100 +1073742153 +198 +1073742154 +64 +1073742155 +0 +1073742156 +0 +1073742157 +6 +1073742158 +52 +1073742159 +56 +1073742160 +100 +1073742161 +198 +1073742162 +3 +1073742163 +120 +1073742164 +60 +1073742165 +7 +1073742166 +0 +1073742167 +0 +1073742168 +100 +1073742169 +231 +1073742170 +0 +1073742171 +0 +1073742172 +0 +1073742173 +7 +1073742174 +60 +1073742175 +56 +1073742176 +100 +1073742177 +231 +1073742178 +7 +1073742179 +240 +1073742180 +0 +1073742181 +7 +1073742182 +60 +1073742183 +56 +1073742184 +100 +1073742185 +231 +1073742186 +252 +1073742187 +0 +1073742188 +60 +1073742189 +1 +1073742190 +0 +1073742191 +0 +1073742192 +100 +1073742193 +33 +1073742194 +0 +1073742195 +0 +1073742196 +0 +1073742197 +1 +1073742198 +12 +1073742199 +56 +1073742200 +100 +1073742201 +33 +1073742202 +128 +1073742203 +16 +1073742204 +0 +1073742205 +1 +1073742206 +12 +1073742207 +56 +1073742208 +100 +1073742209 +33 +1073742210 +0 +1073742211 +0 +1073742212 +220 +1073742213 +33 +1073742214 +0 +1073742215 +24 +1073742216 +0 +1073742217 +32 +1073742218 +0 +1073742219 +8 +1073742220 +0 +1073742221 +0 +1073742222 +0 +1073742223 +0 +1073742224 +0 +1073742225 +2 +1073742226 +97 +1073742227 +64 +1073742228 +60 +1073742229 +13 +1073742230 +0 +1073742231 +0 +1073742232 +101 +1073742233 +173 +1073742234 +0 +1073742235 +0 +1073742236 +0 +1073742237 +13 +1073742238 +108 +1073742239 +56 +1073742240 +101 +1073742241 +173 +1073742242 +128 +1073742243 +16 +1073742244 +0 +1073742245 +13 +1073742246 +108 +1073742247 +56 +1073742248 +101 +1073742249 +173 +1073742250 +0 +1073742251 +0 +1073742252 +1 +1073742253 +172 +1073742254 +96 +1073742255 +46 +1073742256 +36 +1073742257 +13 +1073742258 +0 +1073742259 +1 +1073742260 +253 +1073742261 +141 +1073742262 +0 +1073742263 +0 +1073742264 +253 +1073742265 +128 +1073742266 +0 +1073742267 +8 +1073742268 +253 +1073742269 +128 +1073742270 +0 +1073742271 +16 +1073742272 +253 +1073742273 +128 +1073742274 +0 +1073742275 +24 +1073742276 +0 +1073742277 +0 +1073742278 +0 +1073742279 +15 +1073742280 +0 +1073742281 +0 +1073742282 +0 +1073742283 +0 +1073742284 +0 +1073742285 +0 +1073742286 +0 +1073742287 +0 +1073742288 +0 +1073742289 +0 +1073742290 +0 +1073742291 +0 +1073742292 +0 +1073742293 +0 +1073742294 +0 +1073742295 +0 +1073742296 +0 +1073742297 +0 +1073742298 +0 +1073742299 +0 +1073742300 +0 +1073742301 +0 +1073742302 +0 +1073742303 +0 +1073742304 +0 +1073742305 +0 +1073742306 +0 +1073742307 +0 +1073742308 +0 +1073742309 +0 +1073742310 +0 +1073742311 +0 +1073742312 +0 +1073742313 +0 +1073742314 +0 +1073742315 +0 +1073742316 +0 +1073742317 +0 +1073742318 +0 +1073742319 +0 +1073742320 +0 +1073742321 +0 +1073742322 +0 +1073742323 +0 +1073742324 +0 +1073742325 +0 +1073742326 +0 +1073742327 +0 +1073742328 +0 +1073742329 +0 +1073742330 +0 +1073742331 +0 +1073742332 +0 +1073742333 +0 +1073742334 +0 +1073742335 +0 +1073742336 +0 +1073742337 +0 +1073742338 +0 +1073742339 +0 +1073742340 +0 +1073742341 +0 +1073742342 +0 +1073742343 +0 +1073742344 +0 +1073742345 +0 +1073742346 +0 +1073742347 +0 +1073742348 +0 +1073742349 +0 +1073742350 +0 +1073742351 +0 +1073742352 +0 +1073742353 +0 +1073742354 +0 +1073742355 +0 +1073742356 +0 +1073742357 +0 +1073742358 +0 +1073742359 +0 +1073742360 +0 +1073742361 +0 +1073742362 +0 +1073742363 +0 +1073742364 +0 +1073742365 +0 +1073742366 +0 +1073742367 +0 +1073742368 +0 +1073742369 +0 +1073742370 +0 +1073742371 +0 +1073742372 +0 +1073742373 +0 +1073742374 +0 +1073742375 +0 +1073742376 +0 +1073742377 +0 +1073742378 +0 +1073742379 +0 +1073742380 +0 +1073742381 +0 +1073742382 +0 +1073742383 +0 +1073742384 +0 +1073742385 +0 +1073742386 +0 +1073742387 +0 +1073742388 +0 +1073742389 +0 +1073742390 +0 +1073742391 +0 +1073742392 +0 +1073742393 +0 +1073742394 +0 +1073742395 +0 +1073742396 +0 +1073742397 +0 +1073742398 +0 +1073742399 +0 +1073742400 +0 +1073742401 +0 +1073742402 +0 +1073742403 +0 +1073742404 +0 +1073742405 +0 +1073742406 +0 +1073742407 +0 +1073742408 +0 +1073742409 +0 +1073742410 +0 +1073742411 +0 +1073742412 +0 +1073742413 +0 +1073742414 +0 +1073742415 +0 +1073742416 +0 +1073742417 +0 +1073742418 +0 +1073742419 +0 +1073742420 +0 +1073742421 +0 +1073742422 +0 +1073742423 +0 +1073742424 +0 +1073742425 +0 +1073742426 +0 +1073742427 +0 +1073742428 +0 +1073742429 +0 +1073742430 +0 +1073742431 +0 +1073742432 +0 +1073742433 +0 +1073742434 +0 +1073742435 +0 +1073742436 +0 +1073742437 +0 +1073742438 +0 +1073742439 +0 +1073742440 +0 +1073742441 +0 +1073742442 +0 +1073742443 +0 +1073742444 +0 +1073742445 +0 +1073742446 +0 +1073742447 +0 +1073742448 +0 +1073742449 +0 +1073742450 +0 +1073742451 +0 +1073742452 +0 +1073742453 +0 +1073742454 +0 +1073742455 +0 +1073742456 +0 +1073742457 +0 +1073742458 +0 +1073742459 +0 +1073742460 +0 +1073742461 +0 +1073742462 +0 +1073742463 +0 +1073742464 +0 +1073742465 +0 +1073742466 +0 +1073742467 +0 +1073742468 +0 +1073742469 +0 +1073742470 +0 +1073742471 +0 +1073742472 +0 +1073742473 +0 +1073742474 +0 +1073742475 +0 +1073742476 +0 +1073742477 +0 +1073742478 +0 +1073742479 +0 +1073742480 +0 +1073742481 +0 +1073742482 +0 +1073742483 +0 +1073742484 +0 +1073742485 +0 +1073742486 +0 +1073742487 +0 +1073742488 +0 +1073742489 +0 +1073742490 +0 +1073742491 +0 +1073742492 +0 +1073742493 +0 +1073742494 +0 +1073742495 +0 +1073742496 +0 +1073742497 +0 +1073742498 +0 +1073742499 +0 +1073742500 +0 +1073742501 +0 +1073742502 +0 +1073742503 +0 +1073742504 +0 +1073742505 +0 +1073742506 +0 +1073742507 +0 +1073742508 +0 +1073742509 +0 +1073742510 +0 +1073742511 +0 +1073742512 +0 +1073742513 +0 +1073742514 +0 +1073742515 +0 +1073742516 +0 +1073742517 +0 +1073742518 +0 +1073742519 +0 +1073742520 +0 +1073742521 +0 +1073742522 +0 +1073742523 +0 +1073742524 +0 +1073742525 +0 +1073742526 +0 +1073742527 +0 +1073742528 +0 +1073742529 +0 +1073742530 +0 +1073742531 +0 +1073742532 +0 +1073742533 +0 +1073742534 +0 +1073742535 +0 +1073742536 +0 +1073742537 +0 +1073742538 +0 +1073742539 +0 +1073742540 +0 +1073742541 +0 +1073742542 +0 +1073742543 +0 +1073742544 +0 +1073742545 +0 +1073742546 +0 +1073742547 +0 +1073742548 +0 +1073742549 +0 +1073742550 +0 +1073742551 +0 +1073742552 +0 +1073742553 +0 +1073742554 +0 +1073742555 +0 +1073742556 +0 +1073742557 +0 +1073742558 +0 +1073742559 +0 +1073742560 +0 +1073742561 +0 +1073742562 +0 +1073742563 +0 +1073742564 +0 +1073742565 +0 +1073742566 +0 +1073742567 +0 +1073742568 +0 +1073742569 +0 +1073742570 +0 +1073742571 +0 +1073742572 +0 +1073742573 +0 +1073742574 +0 +1073742575 +0 +1073742576 +0 +1073742577 +0 +1073742578 +0 +1073742579 +0 +1073742580 +0 +1073742581 +0 +1073742582 +0 +1073742583 +0 +1073742584 +0 +1073742585 +0 +1073742586 +0 +1073742587 +0 +1073742588 +0 +1073742589 +0 +1073742590 +0 +1073742591 +0 +1073742592 +0 +1073742593 +0 +1073742594 +0 +1073742595 +0 +1073742596 +0 +1073742597 +0 +1073742598 +0 +1073742599 +0 +1073742600 +0 +1073742601 +0 +1073742602 +0 +1073742603 +0 +1073742604 +0 +1073742605 +0 +1073742606 +0 +1073742607 +0 +1073742608 +0 +1073742609 +0 +1073742610 +0 +1073742611 +0 +1073742612 +0 +1073742613 +0 +1073742614 +0 +1073742615 +0 +1073742616 +0 +1073742617 +0 +1073742618 +0 +1073742619 +0 +1073742620 +0 +1073742621 +0 +1073742622 +0 +1073742623 +0 +1073742624 +0 +1073742625 +0 +1073742626 +0 +1073742627 +0 +1073742628 +0 +1073742629 +0 +1073742630 +0 +1073742631 +0 +1073742632 +0 +1073742633 +0 +1073742634 +0 +1073742635 +0 +1073742636 +0 +1073742637 +0 +1073742638 +0 +1073742639 +0 +1073742640 +0 +1073742641 +0 +1073742642 +0 +1073742643 +0 +1073742644 +0 +1073742645 +0 +1073742646 +0 +1073742647 +0 +1073742648 +0 +1073742649 +0 +1073742650 +0 +1073742651 +0 +1073742652 +0 +1073742653 +0 +1073742654 +0 +1073742655 +0 +1073742656 +0 +1073742657 +0 +1073742658 +0 +1073742659 +0 +1073742660 +0 +1073742661 +0 +1073742662 +0 +1073742663 +0 +1073742664 +0 +1073742665 +0 +1073742666 +0 +1073742667 +0 +1073742668 +0 +1073742669 +0 +1073742670 +0 +1073742671 +0 +1073742672 +0 +1073742673 +0 +1073742674 +0 +1073742675 +0 +1073742676 +0 +1073742677 +0 +1073742678 +0 +1073742679 +0 +1073742680 +221 +1073742681 +142 +1073742682 +0 +1073742683 +0 +1073742684 +17 +1073742685 +174 +1073742686 +255 +1073742687 +154 +1073742688 +0 +1073742689 +0 +1073742690 +0 +1073742691 +0 +1073742692 +0 +1073742693 +0 +1073742694 +0 +1073742695 +15 +1073742696 +1 +1073742697 +192 +1073742698 +0 +1073742699 +8 +1073742700 +221 +1073742701 +132 +1073742702 +0 +1073742703 +8 +1073742704 +0 +1073742705 +0 +1073742706 +0 +1073742707 +0 +1073742708 +0 +1073742709 +0 +1073742710 +0 +1073742711 +0 +1073742712 +0 +1073742713 +0 +1073742714 +0 +1073742715 +0 +1073742716 +0 +1073742717 +0 +1073742718 +0 +1073742719 +0 +elf_entry +10376293542535364608 diff --git a/test/coq/pass/allpats.sail b/test/coq/pass/allpats.sail new file mode 100644 index 00000000..c6e111e9 --- /dev/null +++ b/test/coq/pass/allpats.sail @@ -0,0 +1,100 @@ +/* Not really *all* of the patterns, but enough to exercise the exhaustiveness + checker for Coq output */ + +default Order dec +$include <prelude.sail> + +enum anenum = {Athing, Bthing, Cthing} + +union aunion = {Dthing: unit, Ething: anenum, Fthing: (anenum,int)} + +struct arecord = {elone: anenum, eltwo: aunion} + +val f : (anenum, aunion, arecord, vector(5,dec,int), bits(4),list(anenum)) -> unit + +function f(a,b,c,d,e,g) = { + match a { + Athing => (), + Bthing => (), + Cthing => () + }; + match a { + Athing => (), + _ => () + }; + match a { + Athing => (), + Bthing => () + }; + match b { + Dthing(()) => (), + Ething(Athing) => (), + Ething(Bthing) => (), + Ething(Cthing) => (), + Fthing(Athing,_) => (), + Fthing(Bthing,_) => (), + Fthing(Cthing,_) => () + }; + match b { + Dthing(()) => (), + Ething(Athing) => (), + Ething(Bthing) => (), + Ething(Cthing) => (), + Fthing(Athing,_) => (), + Fthing(Cthing,_) => () + }; + match b { + Dthing(()) => (), + Ething(Athing) => (), + Ething(Bthing) => (), + Ething(Cthing) => (), + Fthing(Athing,_) => (), + Fthing(_ as x,_) => () + }; + /* Um, no syntax for record patterns? */ + /* Vector patterns must be bits? */ + match e { + [_,_,_,bitzero] => (), + [_,_,_,_] => () + }; + match e { + [_,_,_,bitzero] => () + }; + match e { + [_,bitzero] @ (_ : bits(2)) => (), + _ => () + }; + match e { + [_,bitzero] @ (_ : bits(2)) => () + }; + match (a,b) { + (Athing,Ething(Bthing)) => (), + (_,Fthing(_,_)) => (), + (_,Dthing(())) => (), + (Bthing,_) => (), + (Cthing,_) => () + }; + match (a,b) { + (Athing,Ething(Bthing)) => (), + (Athing,Ething(_)) => (), + (_,Fthing(_,_)) => (), + (_,Dthing(())) => (), + (Bthing,_) => (), + (Cthing,_) => () + }; + match g { + [| |] => (), + [| Athing, Bthing |] => (), + _::_::_ => () + }; + match g { + [| |] => (), + [| Athing, _, Bthing |] => (), + _::_::_::_ => () + }; + match g { + [| |] => (), + [| Athing, _, Bthing |] => (), + _::_ => () + } +}
\ No newline at end of file diff --git a/test/coq/pass/atom.sail b/test/coq/pass/atom.sail new file mode 100644 index 00000000..c9c27b5d --- /dev/null +++ b/test/coq/pass/atom.sail @@ -0,0 +1,21 @@ +default Order dec +$include <flow.sail> +$include <arith.sail> + +val f : forall 'n, 'n >= 0. atom(8 * 'n) -> int + +function f(x) = x+1 + +val g : forall 'n, 'n > 0. atom('n) -> atom(2*'n) +val h : forall 'n, 'n > 1. atom('n) -> int + +function h(x) = x + +val test : unit -> bool + +function test() = { + /* Using f with Coq would need us to provide/infer witnesses for 'n + f(0) == 1 & f(8) == 9 + */ + h(g(1)) == 2 +}
\ No newline at end of file diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index 2be5e535..5a723a06 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -5,7 +5,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" SAILDIR="$DIR/../.." TYPECHECKTESTSDIR="$DIR/../typecheck/pass" EXTRATESTSDIR="$DIR/pass" -BBVDIR="$DIR/../../../bbv" +BBVDIR="$DIR/../../../bbv/theories" RED='\033[0;31m' GREEN='\033[0;32m' diff --git a/test/hol/test_raw_addScript.sml b/test/hol/test_raw_addScript.sml index 1eb90ef8..20465eb2 100644 --- a/test/hol/test_raw_addScript.sml +++ b/test/hol/test_raw_addScript.sml @@ -783,7 +783,7 @@ val () = computeLib.extend_compset [ ] ] cs; -val empty_state = ``init_state initial_regstate bool_oracle seed``; +val empty_state = ``init_state initial_regstate``; val init_registers_result = ``init_registers vinitPC s`` @@ -927,7 +927,7 @@ install_code_result val test_raw_add_thm = Q.store_thm("test_raw_add_thm", `PrePost - (λs. s = init_state initial_regstate bool_oracle seed) + (λs. s = init_state initial_regstate) (install_and_run test_raw_add_insts 40) (λ_ s. test_raw_add_post s)`, rw[PrePost_def] @@ -1378,7 +1378,7 @@ computeLib.CBV_CONV cs ``decode (EL 1 test_raw_add_insts)`` val th1 = EVAL ``THE (decode (EL 1 test_raw_add_insts))`` -val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate) o1 seed)`` +val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate))`` val th2 = ``execute ^(rhs(concl th1)) ^s1`` |> SIMP_CONV(srw_ss())[execute_def] diff --git a/test/isabelle/Aarch64_code.thy b/test/isabelle/Aarch64_code.thy index 05e5bb2e..8a0e1795 100644 --- a/test/isabelle/Aarch64_code.thy +++ b/test/isabelle/Aarch64_code.thy @@ -52,7 +52,7 @@ fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exc 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" +definition "initial_state \<equiv> init_state initial_regstate" code_printing constant elf_entry \<rightharpoonup> (OCaml) "(Int'_of'_integer (Elf'_loader.elf'_entry _))" termination BigEndianReverse sorry diff --git a/test/isabelle/Cheri_code.thy b/test/isabelle/Cheri_code.thy index cfd01413..c0e8f9a7 100644 --- a/test/isabelle/Cheri_code.thy +++ b/test/isabelle/Cheri_code.thy @@ -5,32 +5,55 @@ begin declare [[code abort: failwith]] code_datatype - DADDIU DADDU DADDI DADD ADD ADDI ADDU ADDIU DSUBU DSUB SUB SUBU AND0 ANDI OR0 + 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 + BEQ BCMPZ SYSCALL BREAK WAIT TRAPREG TRAPIMM Load Store LWL LWR SWL SWR LDL LDR + SDL SDR CACHE 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 + +(* Fake termination proofs of loops for code generation *) +lemma whileM_dom: "whileM_dom (vars, cond, body)" sorry +termination whileM using whileM_dom by auto +lemma whileS_dom: "whileS_dom (vars, cond, body, s)" sorry +termination whileS using whileS_dom by auto + +lemma liftS_whileM: "\<lbrakk>whileM vars cond body\<rbrakk>\<^sub>S = whileS vars (liftS \<circ> cond) (liftS \<circ> body)" + by (intro ext liftState_whileM[OF whileS_dom whileM_dom]) + +(* Pre-lift main loop to state monad to gain some performance *) +fun mainS :: "unit \<Rightarrow> (regstate, unit, exception) monadS" where + "mainS () = \<lbrakk>main ()\<rbrakk>\<^sub>S" + +schematic_goal liftS_main[symmetric, code]: "?m = mainS" + by (intro ext) + (simp add: main_def liftState_simp liftS_whileM comp_def del: whileM.simps whileS.simps + cong: bindS_cong if_cong) + +fun print_endline' :: "String.literal \<Rightarrow> unit" where "print_endline' _ = ()" +lemma [code]: "print_endline s = print_endline' (String.implode s)" by auto fun prerr_endline' :: "String.literal \<Rightarrow> unit" where "prerr_endline' _ = ()" lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto +fun prerr_string' :: "String.literal \<Rightarrow> unit" where "prerr_string' _ = ()" +lemma [code]: "prerr_string s = prerr_string' (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 print_endline' \<rightharpoonup> (OCaml) "Pervasives.print'_endline" code_printing constant prerr_endline' \<rightharpoonup> (OCaml) "Pervasives.prerr'_endline" +code_printing constant prerr_string' \<rightharpoonup> (OCaml) "Pervasives.prerr'_string" code_printing constant putchar' \<rightharpoonup> (OCaml) "Pervasives.print'_char" declare insert_code[code del] @@ -50,12 +73,12 @@ fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exc 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" +definition "initial_state \<equiv> init_state initial_regstate\<lparr>memstate := (\<lambda>_. Some [B0, B0, B0, B0, B0, B0, B0, B0])\<rparr>" 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 +export_code mainS 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" diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml index f51ef4dd..c50d525d 100644 --- a/test/isabelle/run_cheri.ml +++ b/test/isabelle/run_cheri.ml @@ -63,8 +63,8 @@ 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_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval) +let (>>) = Sail2_state_monad.bindS +(*let liftS = Sail2_state_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval)*) let load_elf_segment seg = let open Elf_interpreted_segment in @@ -78,7 +78,7 @@ let load_elf_segment seg = 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) + Sail2_state.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs) let _ = Random.self_init (); @@ -88,5 +88,5 @@ let _ = in (* State_monad.prerr_results *) (Cheri_code.initial_state |> - (State.iterS load_elf_segment elf_segments >> (fun _ -> - liftS (Cheri.main ())))); + (Sail2_state.iterS load_elf_segment elf_segments >> (fun _ -> + (Cheri_code.mainS ())))); diff --git a/test/riscv/tests/rv64ua-p-lrsc.elf b/test/riscv/tests/rv64ua-p-lrsc.elf Binary files differnew file mode 100755 index 00000000..0fb5b44e --- /dev/null +++ b/test/riscv/tests/rv64ua-p-lrsc.elf diff --git a/test/riscv/tests/rv64ua-v-lrsc.elf b/test/riscv/tests/rv64ua-v-lrsc.elf Binary files differnew file mode 100755 index 00000000..3f49c87c --- /dev/null +++ b/test/riscv/tests/rv64ua-v-lrsc.elf |