diff options
Diffstat (limited to 'test')
37 files changed, 378 insertions, 42 deletions
diff --git a/test/c/cfold_reg.expect b/test/c/cfold_reg.expect new file mode 100644 index 00000000..27ba77dd --- /dev/null +++ b/test/c/cfold_reg.expect @@ -0,0 +1 @@ +true diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail new file mode 100644 index 00000000..a5090e91 --- /dev/null +++ b/test/c/cfold_reg.sail @@ -0,0 +1,30 @@ +default Order dec + +$include <prelude.sail> + +val "eq_string" : (string, string) -> bool + +overload operator == = {eq_string} + +register R : bool + +val "print_endline" : string -> unit + +function IMPDEF(str : string) -> bool = { + if str == "A" then { + return(R) + } else if str == "B" then { + true + } else { + false + } +} + +function main(() : unit) -> unit = { + R = true; + if IMPDEF("A") then { + print_endline("true") + } else { + print_endline("false") + } +}
\ No newline at end of file diff --git a/test/c/cheri128_hsb.expect b/test/c/cheri128_hsb.expect new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/test/c/cheri128_hsb.expect diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail new file mode 100644 index 00000000..a06a2ad2 --- /dev/null +++ b/test/c/cheri128_hsb.sail @@ -0,0 +1,62 @@ +default Order dec + +$include <flow.sail> +$include <arith.sail> +$include <option.sail> +$include <vector_dec.sail> +$include <exception_basic.sail> + +val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) + +val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} + +overload operator + = {add_range} +overload operator - = {sub_range} + +infix 1 >> +infix 1 << + +val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef} +val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef} + +val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) +val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) + +overload operator >> = {shift_bits_right, shiftr} +overload operator << = {shift_bits_left, shiftl} + +val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))} + +function HighestSetBit x = { + foreach (i from ('N - 1) to 0 by 1 in dec) + if [x[i]] == 0b1 then return (true, i); + return (false, 0) +} + +/* hw rounds up E to multiple of 4 */ +function roundUp(e) : range(0, 45) -> range(0, 48) = + let 'r = modulus(e, 4) in + if (r == 0) + then e + else (e - r + 4) + +function computeE (rlength) : bits(65) -> range(0, 48) = + let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in + if nonzero then + /* above will always return <= 45 because 19 bits of zero are shifted in from right */ + {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) } + else + 0 + +val main : unit -> unit effect {escape} + +function main() = { + let _ = computeE(0xFFFF_FFFF_FFFF_FFFF @ 0b1); + () +}
\ No newline at end of file diff --git a/test/c/cheri_capstruct_order.expect b/test/c/cheri_capstruct_order.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/cheri_capstruct_order.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/cheri_capstruct_order.sail b/test/c/cheri_capstruct_order.sail new file mode 100644 index 00000000..6eb774dd --- /dev/null +++ b/test/c/cheri_capstruct_order.sail @@ -0,0 +1,32 @@ +default Order dec + +val SignalException : unit -> unit effect {rreg} + +val SignalExceptionBadAddr : unit -> unit effect {rreg} + +function SignalExceptionBadAddr() = { + SignalException(); +} + +struct CapStruct = { + base : bool, +} + +type CapReg = CapStruct + +function getCapBase(c) : CapStruct -> bool = c.base + +register KCC : CapReg + +function SignalException () = { + base = getCapBase(KCC); + (); +} + +val "print_endline" : string -> unit + +val main : unit -> unit + +function main() = { + print_endline("ok") +}
\ No newline at end of file diff --git a/test/c/config_register.expect b/test/c/config_register.expect new file mode 100644 index 00000000..8d164b5c --- /dev/null +++ b/test/c/config_register.expect @@ -0,0 +1 @@ +R = 0x00000000 diff --git a/test/c/config_register.sail b/test/c/config_register.sail new file mode 100644 index 00000000..f4831ca5 --- /dev/null +++ b/test/c/config_register.sail @@ -0,0 +1,16 @@ +default Order dec + +$include <prelude.sail> + +function zeros forall 'n. (() : unit) -> bits('n) = { + sail_zeros('n) +} + +register configuration R : bits(32) = zeros() + +register S : bits(32) + +function main(() : unit) -> unit = { + R = zeros(); + print_bits("R = ", R) +}
\ No newline at end of file diff --git a/test/c/non_unique.expect b/test/c/non_unique.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/non_unique.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/non_unique.sail b/test/c/non_unique.sail new file mode 100644 index 00000000..eda7720d --- /dev/null +++ b/test/c/non_unique.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +function f(_: int) -> unit = () +function g(_: bits(1)) -> unit = () + +function main(() : unit) -> unit = { + let y : int = { + let x : int = 3; + x + }; + { + let x : bits(1) = 0b0; + g(x) + }; + print_endline("ok"); +}
\ No newline at end of file diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 6cd75981..268763ad 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -63,6 +63,7 @@ xml = '<testsuites>\n' xml += test_c('unoptimized C', '', '', True) xml += test_c('optimized C', '-O2', '-O', True) xml += test_c('constant folding', '', '-Oconstant_fold', True) +xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True) xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False) xml += test_interpreter('interpreter') diff --git a/test/c/small_slice.expect b/test/c/small_slice.expect new file mode 100644 index 00000000..64d39581 --- /dev/null +++ b/test/c/small_slice.expect @@ -0,0 +1,2 @@ +v1 = 0x1234 +v2 = 0x34 diff --git a/test/c/small_slice.sail b/test/c/small_slice.sail new file mode 100644 index 00000000..80878a80 --- /dev/null +++ b/test/c/small_slice.sail @@ -0,0 +1,16 @@ +default Order dec + +$include <prelude.sail> + +function get_16((): unit) -> range(0, 16) = 16 +function get_8((): unit) -> range(0, 16) = 8 + +function main((): unit) -> unit = { + let x = get_16(); + let y = get_8(); + let addr = 0x1234_ABCD; + let v1 = slice(addr, 16, x); + let v2 = slice(addr, 16, y); + print_bits("v1 = ", v1); + print_bits("v2 = ", v2); +}
\ No newline at end of file diff --git a/test/c/string_of_bits.expect b/test/c/string_of_bits.expect new file mode 100644 index 00000000..e373cf38 --- /dev/null +++ b/test/c/string_of_bits.expect @@ -0,0 +1,6 @@ +HelloWorld0b11110000111 0xFF +HelloWorld0b11110000111 0xFF +HelloWorld0b11110000111 0xFF +HelloWorld0b11110000111 0xFF +HelloWorld0b11110000111 0xFF +HelloWorld0b11110000111 0xFF diff --git a/test/c/string_of_bits.sail b/test/c/string_of_bits.sail new file mode 100644 index 00000000..fcaeb3e1 --- /dev/null +++ b/test/c/string_of_bits.sail @@ -0,0 +1,25 @@ +default Order dec + +$include <prelude.sail> + +val "concat_str" : (string, string) -> string + +infixl 1 ++ + +overload operator ++ = {concat_str} + +val "print_endline" : string -> unit + +val BitStr = "string_of_bits" : forall 'n. bits('n) -> string + +val DecStr = "decimal_string_of_bits" : forall 'n. bits('n) -> string + +function main(() : unit) -> unit = { + foreach (i from 0 to 5) { + let x = "Hello"; + let y = "World"; + let z = 0b1111_0000_111; + let w = 0xFF; + print_endline(x ++ y ++ BitStr(z) ++ " " ++ BitStr(w)) + } +}
\ No newline at end of file diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail index 1e1f391c..d0a14586 100644 --- a/test/ocaml/reg_ref/rr.sail +++ b/test/ocaml/reg_ref/rr.sail @@ -52,7 +52,7 @@ val slice_slice : forall 'n 'm 'o 'p, 0 <= 'p <= 'm <= 'o & 'o - 'p < 'n. function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start]) /* We can update a bitvector from another bitvector or a slice */ -val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n. +val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (register(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit effect {wreg, rreg} function _set_slice (v, stop, start, update) = { @@ -61,7 +61,7 @@ function _set_slice (v, stop, start, update) = { (*v) = v2; } -val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o <= 'n. +val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o < 'n. (register(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit effect {wreg, rreg} function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update) diff --git a/test/typecheck/pass/constrained_struct.sail b/test/typecheck/pass/constrained_struct.sail new file mode 100644 index 00000000..64b2287f --- /dev/null +++ b/test/typecheck/pass/constrained_struct.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +struct MyStruct 'n, 'n in {32, 64} = { + field: bits('n) +} + +type MyStruct32 = MyStruct(32) +type MyStruct64 = MyStruct(64) + +let x : MyStruct64 = struct { field = 0xFFFF_FFFF_FFFF_FFFF } diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect new file mode 100644 index 00000000..5173ef0b --- /dev/null +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -0,0 +1,5 @@ +Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 10, character 26 + +type MyStruct64 = [41mMyStruct[0m(65) + +Could not prove (65 = 32 | 65 = 64) for type constructor MyStruct diff --git a/test/typecheck/pass/constrained_struct/v1.sail b/test/typecheck/pass/constrained_struct/v1.sail new file mode 100644 index 00000000..62fc1c01 --- /dev/null +++ b/test/typecheck/pass/constrained_struct/v1.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +struct MyStruct 'n, 'n in {32, 64} = { + field: bits('n) +} + +type MyStruct32 = MyStruct(32) +type MyStruct64 = MyStruct(65) + +let x : MyStruct64 = struct { field = 0b1 @ 0xFFFF_FFFF_FFFF_FFFF } diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail index dd761b83..95be790c 100644 --- a/test/typecheck/pass/inline_typ.sail +++ b/test/typecheck/pass/inline_typ.sail @@ -1,2 +1,2 @@ -function test (x : atom('n), y : atom('m)) -> forall 'n 'm. atom('m + 'n) = undefined
\ No newline at end of file +function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = undefined
\ No newline at end of file diff --git a/test/typecheck/pass/lexp_vec.sail b/test/typecheck/pass/lexp_vec.sail new file mode 100644 index 00000000..605c3855 --- /dev/null +++ b/test/typecheck/pass/lexp_vec.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +register V : vector(1, dec, vector(32, dec, bit)) + +val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit) + +function main() : unit -> unit = { + V[0] = zeros() +} diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail index a12e81da..f171eb9b 100644 --- a/test/typecheck/pass/nat_set.sail +++ b/test/typecheck/pass/nat_set.sail @@ -1,4 +1,4 @@ -function test x : atom('n) -> forall 'n. bool = true +function test forall 'n, 'n in {1, 3}. x : atom('n) -> bool = true let x = test(1) diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail index de4458ed..24e50259 100644 --- a/test/typecheck/pass/option_either.sail +++ b/test/typecheck/pass/option_either.sail @@ -2,11 +2,11 @@ default Order inc union option ('a : Type) = {None : unit, Some : 'a} -function none () -> forall ('a : Type). option('a) = None() +function none forall ('a : Type). () -> option('a) = None() -function some x : 'a -> forall ('a : Type). option('a) = Some(x) +function some forall ('a : Type). x : 'a -> option('a) = Some(x) -function test x : option('a) -> forall ('a : Type). range(0, 1) = match x { +function test forall ('a : Type). x : option('a) -> range(0, 1) = match x { None() => 0, Some(y) => 1 } diff --git a/test/typecheck/pass/or_pattern.sail b/test/typecheck/pass/or_pattern.sail deleted file mode 100644 index a6e11ecd..00000000 --- a/test/typecheck/pass/or_pattern.sail +++ /dev/null @@ -1,16 +0,0 @@ -default Order dec - -$include <prelude.sail> - -let x : int = 5 - -val main : unit -> unit - -function main() = { - match x { - 3 | 4 => (), - (1 | 2) | 3 => (), - 1 | (2 | 3) => (), - _ => () - } -}
\ No newline at end of file diff --git a/test/typecheck/pass/or_pattern/v1.expect b/test/typecheck/pass/or_pattern/v1.expect deleted file mode 100644 index edf07f03..00000000 --- a/test/typecheck/pass/or_pattern/v1.expect +++ /dev/null @@ -1,5 +0,0 @@ -Type error at file "or_pattern/v1.sail", line 11, character 5 to line 11, character 5 - - [41my[0m | z => (), - -Bindings are not allowed in this context diff --git a/test/typecheck/pass/or_pattern/v1.sail b/test/typecheck/pass/or_pattern/v1.sail deleted file mode 100644 index 21bc87e8..00000000 --- a/test/typecheck/pass/or_pattern/v1.sail +++ /dev/null @@ -1,14 +0,0 @@ -default Order dec - -$include <prelude.sail> - -let x : int = 5 - -val main : unit -> unit - -function main() = { - match x { - y | z => (), - _ => () - } -}
\ No newline at end of file diff --git a/test/typecheck/pass/reg_ref.sail b/test/typecheck/pass/reg_ref.sail new file mode 100644 index 00000000..a81f6abf --- /dev/null +++ b/test/typecheck/pass/reg_ref.sail @@ -0,0 +1,13 @@ +register reg : range(0, 10) + +val modify : register(range(0,10)) -> unit effect {wreg} + +function modify (r) = { + (*r) = 9; + (*r) = 10; + (*r) = 8 +} + +val test : unit -> unit effect {wreg} + +function test () = modify(ref reg) diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail new file mode 100644 index 00000000..21911b15 --- /dev/null +++ b/test/typecheck/pass/vec_length.sail @@ -0,0 +1,9 @@ +default Order dec +$include <vector_dec.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[3]; + let z = [x with 5 = y]; + () +} diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect new file mode 100644 index 00000000..68a4ca70 --- /dev/null +++ b/test/typecheck/pass/vec_length/v1.expect @@ -0,0 +1,13 @@ +Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15 + + let y = [41mx[10][0m; + +No overloadings for vector_access, tried: + bitvector_access: + Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) + plain_vector_access: + Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) diff --git a/test/typecheck/pass/vec_length/v1.sail b/test/typecheck/pass/vec_length/v1.sail new file mode 100644 index 00000000..735da89c --- /dev/null +++ b/test/typecheck/pass/vec_length/v1.sail @@ -0,0 +1,8 @@ +default Order dec +$include <vector_dec.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[10]; + () +}
\ No newline at end of file diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect new file mode 100644 index 00000000..7ce8fd99 --- /dev/null +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -0,0 +1,13 @@ +Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15 + + let y = [41mx[10][0m; + +No overloadings for vector_access, tried: + bitvector_access: + Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) + plain_vector_access: + Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) diff --git a/test/typecheck/pass/vec_length/v1_inc.sail b/test/typecheck/pass/vec_length/v1_inc.sail new file mode 100644 index 00000000..b72738d1 --- /dev/null +++ b/test/typecheck/pass/vec_length/v1_inc.sail @@ -0,0 +1,8 @@ +default Order inc +$include <vector_inc.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[10]; + () +} diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect new file mode 100644 index 00000000..d123cabd --- /dev/null +++ b/test/typecheck/pass/vec_length/v2.expect @@ -0,0 +1,13 @@ +Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25 + + let z = [41m[x with 10 = y][0m; + +No overloadings for vector_update, tried: + bitvector_update: + Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) + plain_vector_update: + Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) diff --git a/test/typecheck/pass/vec_length/v2.sail b/test/typecheck/pass/vec_length/v2.sail new file mode 100644 index 00000000..4df62e81 --- /dev/null +++ b/test/typecheck/pass/vec_length/v2.sail @@ -0,0 +1,9 @@ +default Order dec +$include <vector_dec.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[3]; + let z = [x with 10 = y]; + () +} diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect new file mode 100644 index 00000000..e7d2b52f --- /dev/null +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -0,0 +1,13 @@ +Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25 + + let z = [41m[x with 10 = y][0m; + +No overloadings for vector_update, tried: + bitvector_update: + Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) + plain_vector_update: + Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8) + + Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) diff --git a/test/typecheck/pass/vec_length/v2_inc.sail b/test/typecheck/pass/vec_length/v2_inc.sail new file mode 100644 index 00000000..3f75fee1 --- /dev/null +++ b/test/typecheck/pass/vec_length/v2_inc.sail @@ -0,0 +1,9 @@ +default Order inc +$include <vector_inc.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[3]; + let z = [x with 10 = y]; + () +} diff --git a/test/typecheck/pass/vec_length_inc.sail b/test/typecheck/pass/vec_length_inc.sail new file mode 100644 index 00000000..a8dd707f --- /dev/null +++ b/test/typecheck/pass/vec_length_inc.sail @@ -0,0 +1,9 @@ +default Order inc +$include <vector_inc.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[3]; + let z = [x with 5 = y]; + () +} |