diff options
Diffstat (limited to 'test')
40 files changed, 294 insertions, 42 deletions
diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh index dc2bdde4..416ad9f1 100755 --- a/test/aarch64_small/run_tests.sh +++ b/test/aarch64_small/run_tests.sh @@ -52,6 +52,13 @@ else red "failed to build lem" "fail" fi +if make -B -C ../../aarch64_small armV8.smt_model SAIL="$SAILDIR/sail" +then + green "compiled aarch64_small for SMT generation" "ok" +else + red "failed to build aarch64_small for SMT generation" "fail" +fi + finish_suite "aarch64_small tests" printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/builtins/clz.sail b/test/builtins/clz.sail new file mode 100644 index 00000000..5cf20068 --- /dev/null +++ b/test/builtins/clz.sail @@ -0,0 +1,9 @@ +default Order dec +$include <vector_dec.sail> + +function main () : unit -> unit = { + assert(count_leading_zeros(0x0) == 4); + assert(count_leading_zeros(0x1) == 3); + assert(count_leading_zeros(0x4) == 1); + assert(count_leading_zeros(0xf) == 0); +}
\ No newline at end of file diff --git a/test/builtins/count_leading_zeros.sail b/test/builtins/count_leading_zeros.sail new file mode 100644 index 00000000..6d6d0901 --- /dev/null +++ b/test/builtins/count_leading_zeros.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <vector_dec.sail> + +val main : unit -> unit effect {escape} + +function main () = { + foreach (i from 0 to 32 by 1 in inc) { + assert(count_leading_zeros(sail_shiftright(0xDEADBEEF, i)) == i); + } +} diff --git a/test/builtins/run_tests.py b/test/builtins/run_tests.py index ba13d5b9..a677ccfe 100755 --- a/test/builtins/run_tests.py +++ b/test/builtins/run_tests.py @@ -68,6 +68,7 @@ def test_lem_builtins(name): step('mkdir -p _lbuild_{}'.format(basename)) step('mv {}.lem _lbuild_{}'.format(basename, basename)) step('mv {}_types.lem _lbuild_{}'.format(basename, basename)) + step('cp $SAIL_DIR/src/lem_interp/sail2_instr_kinds.lem _lbuild_{}'.format(basename)) step('cp myocamlbuild.ml _lbuild_{}'.format(basename)) os.chdir('_lbuild_{}'.format(basename)) step('ln -s $SAIL_DIR/src/gen_lib/ gen_lib') diff --git a/test/builtins/shift.sail b/test/builtins/shift.sail new file mode 100644 index 00000000..1972c3a4 --- /dev/null +++ b/test/builtins/shift.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <vector_dec.sail> + +val main : unit -> unit effect {escape} + +function main () = { + assert(sail_shiftright(0xDEADBEEF, 16) == 0x0000DEAD); + assert(sail_shiftright(0xDEADBEEF, 4) == 0x0DEADBEE); + assert(sail_arith_shiftright(0xDEADBEEF, 16) == 0xFFFFDEAD); + assert(sail_arith_shiftright(0xDEADBEEF, 4) == 0xFDEADBEE); + assert(sail_shiftleft(0xDEADBEEF, 16) == 0xBEEF0000); + assert(sail_shiftleft(0xDEADBEEF, 4) == 0xEADBEEF0); +} diff --git a/test/c/run_tests.py b/test/c/run_tests.py index f5347831..64c3ae42 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -22,10 +22,10 @@ def test_c(name, c_opts, sail_opts, valgrind): if tests[filename] == 0: step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename)) step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, sail_dir, sail_dir, basename)) - step('./{} 1> {}.result'.format(basename, basename)) + step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.result {}.expect'.format(basename, basename)) if valgrind: - step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=1 ./{}".format(basename)) + step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -57,7 +57,7 @@ def test_ocaml(name): tests[filename] = os.fork() if tests[filename] == 0: step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(basename, basename, filename)) - step('./{} 1> {}.oresult'.format(basename, basename)) + step('./{} 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.oresult {}.expect'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() diff --git a/test/c/toplevel_tyvar.expect b/test/c/toplevel_tyvar.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/toplevel_tyvar.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/toplevel_tyvar.sail b/test/c/toplevel_tyvar.sail new file mode 100644 index 00000000..af2f4d1e --- /dev/null +++ b/test/c/toplevel_tyvar.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +let 'var = 32 + +function main() -> unit = { + let x: bits('var) = 0xFFFF_FFFF; + let y: bits(32) = 0xFFFF_FFFF; + assert(x == y); + print_endline("ok") +} diff --git a/test/coq/pass/returnwithfact.sail b/test/coq/pass/returnwithfact.sail new file mode 100644 index 00000000..14179c17 --- /dev/null +++ b/test/coq/pass/returnwithfact.sail @@ -0,0 +1,19 @@ +default Order dec +$include <prelude.sail> + +val f : int -> range(2,6) effect {escape} + +val g1 : (bool,int) -> range(0,8) effect {escape} + +function g1(b,x) = { + if b then + return f(x) + else { + return f(x+1); + 5 + } +} + +val g2 : int -> range(0,8) effect {escape} + +function g2(x) = f(x) diff --git a/test/coq/pass/wildcardmerge.sail b/test/coq/pass/wildcardmerge.sail new file mode 100644 index 00000000..ca83b47d --- /dev/null +++ b/test/coq/pass/wildcardmerge.sail @@ -0,0 +1,10 @@ +default Order dec +$include <prelude.sail> + +/* Checks that when merging the type variable with the integer argument, + that we name the integer so that we can write the type of the + second argument. */ + +val f : forall 'n, 'n >= 0. (int('n), bits('n)) -> unit + +function f(_,_) = () diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail index bb1bc952..ce7080c4 100644 --- a/test/mono/castreq.sail +++ b/test/mono/castreq.sail @@ -21,6 +21,13 @@ val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect p val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) overload length = {bitvector_length} overload __size = {length} +val add_bits = {ocaml: "add_vec", lem: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +overload operator + = {add_bits} +val vector_update_subrange = { + ocaml: "update_subrange", + lem: "update_subrange_vec_dec" +} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + /* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */ @@ -33,6 +40,14 @@ function foo(n, x) = 64 => let z = y@y@y@y in let dfsf = 4 in z } +val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure + +function foo_if(n, x) = + let y : bits(16) = extzv(x) in + if n == 32 + then y@y + else /* 64 */ let z = y@y@y@y in let dfsf = 4 in z + val use : bits(16) -> unit effect pure function use(x) = () @@ -45,6 +60,13 @@ function bar(x) = 16 => use(x) } +val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure + +function bar_if(x) = + if 'n == 8 + then use(x@x) + else /* 16 */ use(x) + val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef} function ret(n, x) = @@ -54,11 +76,9 @@ function ret(n, x) = 64 => let z = y@y@y@y in { dfsf = 4; return z; undefined } } -/* TODO: Assignments need more plumbing - -val assign : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect {undef} +val assign : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef} -function assign(x) = { +function assign(n, x) = { let y : bits(16) = extzv(x); r : bits('n) = undefined; match 'n { @@ -67,7 +87,29 @@ function assign(x) = { }; r } -*/ + +val assign2 : forall 'm, 'm in {8,16}. bits('m) -> bits(32) + +function assign2(x) = { + y : bits('m) = x; + r : bits(32) = 0x00000000; + match 'm { + 8 => { y = y + 0x01; r = extzv(y) }, + 16 => r = extzv(y) + }; + r +} + +val assign3 : forall 'm, 'm in {8,16}. bits('m) -> bits('m) + +function assign3(x) = { + y : bits('m) = x; + match 'm { + 8 => y = y + 0x01, + 16 => y[7..0] = 0x89 + }; + y +} /* Adding casts for top-level pattern matches */ @@ -108,12 +150,16 @@ function run () = { assert((ret(0x34) : bits(64)) == 0x0034003400340034); assert((ret(0x3456) : bits(32)) == 0x34563456); assert((ret(0x3456) : bits(64)) == 0x3456345634563456); -/* assert((assign(0x12) : bits(32)) == 0x00120012); + assert((assign(0x12) : bits(32)) == 0x00120012); assert((assign(0x1234) : bits(32)) == 0x12341234); assert((assign(0x12) : bits(64)) == 0x0012001200120012); - assert((assign(0x1234) : bits(64)) == 0x1234123412341234);*/ + assert((assign(0x1234) : bits(64)) == 0x1234123412341234); + assert(assign2(0x12) == 0x00000013); + assert(assign2(0x1234) == 0x00001234); + assert(assign3(0x12) == 0x13); + assert(assign3(0x1234) == 0x1289); assert(foo2(32,0x12) == 0x00120012); assert(foo2(64,0x12) == 0x0012001200120012); assert(foo3(4,0x12) == 0x00120012); assert(foo3(8,0x12) == 0x0012001200120012); -}
\ No newline at end of file +} diff --git a/test/mono/pass/repeatedint b/test/mono/pass/repeatedint new file mode 100644 index 00000000..ff26c84d --- /dev/null +++ b/test/mono/pass/repeatedint @@ -0,0 +1 @@ +repeatedint.sail -auto_mono diff --git a/test/mono/repeatedint.sail b/test/mono/repeatedint.sail new file mode 100644 index 00000000..2d01e814 --- /dev/null +++ b/test/mono/repeatedint.sail @@ -0,0 +1,22 @@ +/* Silly, but it did appear in a model, and we didn't handle it... */ + +default Order dec +$include <prelude.sail> + +union ast = { + SomeInstr : {'size, 'size in {8,16}. (int('size), int('size))} +} + +val test : ast -> bits(32) + +function test(SomeInstr(s as int('size),r)) = { + x : bits('size) = sail_zero_extend(0x80, s); + sail_sign_extend(x,32) +} + +val run : unit -> unit effect {escape} + +function run () = { + assert(test(SomeInstr(8,8)) == 0xffffff80); + assert(test(SomeInstr(16,16)) == 0x00000080); +} diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh index 08926aaa..d2023229 100755 --- a/test/mono/run_tests.sh +++ b/test/mono/run_tests.sh @@ -2,7 +2,7 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" -SAILDIR="$DIR/../.." +SAILDIR=${SAIL_DIR:-"$DIR/../.."} TESTSDIR="$DIR" OUTPUTDIR="$DIR/test-output" diff --git a/test/sailtest.py b/test/sailtest.py index 6910d522..36568469 100644 --- a/test/sailtest.py +++ b/test/sailtest.py @@ -30,11 +30,11 @@ def chunks(filenames, cores): ys.append(list(chunk)) return ys -def step(string): +def step(string, expected_status=0): p = subprocess.Popen(string, shell=True, stderr=subprocess.PIPE, stdout=subprocess.PIPE) out, err = p.communicate() status = p.wait() - if status != 0: + if status != expected_status: print("{}Failed{}: {}".format(color.FAIL, color.END, string)) print('{}stdout{}:'.format(color.NOTICE, color.END)) print(out) diff --git a/test/smt/assembly_mapping.sat.sail b/test/smt/assembly_mapping.sat.sail index a7b0bec5..4aff3605 100644 --- a/test/smt/assembly_mapping.sat.sail +++ b/test/smt/assembly_mapping.sat.sail @@ -49,10 +49,10 @@ mapping utype_mnemonic : uop <-> string = { RISCV_AUIPC <-> "auipc" } -val assembly : ast <-> string - scattered union ast +val assembly : ast <-> string + union clause ast = UTYPE : (bits(20), regbits, uop) mapping clause assembly = UTYPE(imm, rd, op) diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail index d34f3629..0777c904 100644 --- a/test/smt/encdec.sat.sail +++ b/test/smt/encdec.sat.sail @@ -49,10 +49,10 @@ mapping utype_mnemonic : uop <-> string = { RISCV_AUIPC <-> "auipc" } -val assembly : ast <-> string - scattered union ast +val assembly : ast <-> string + union clause ast = UTYPE : (bits(20), regbits, uop) mapping clause assembly = UTYPE(imm, rd, op) diff --git a/test/smt/revrev_endianness.sail b/test/smt/revrev_endianness.sail new file mode 100644 index 00000000..f792871f --- /dev/null +++ b/test/smt/revrev_endianness.sail @@ -0,0 +1,25 @@ +default Order dec + +$include <reverse_endianness.sail> + +$property +function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = { + if length(xs) == 8 then { + let ys: bits(8) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 16 then { + let ys: bits(16) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 32 then { + let ys: bits(32) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 64 then { + let ys: bits(64) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 128 then { + let ys: bits(128) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else { + true + } +} diff --git a/test/smt/revrev_endianness2.sail b/test/smt/revrev_endianness2.sail new file mode 100644 index 00000000..33ba93a2 --- /dev/null +++ b/test/smt/revrev_endianness2.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <reverse_endianness.sail> + +$property +function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = { + if length(xs) == 8 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 16 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 32 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 64 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 128 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else { + true + } +} diff --git a/test/smt/zeros_ones.unsat.sail b/test/smt/zeros_ones.unsat.sail new file mode 100644 index 00000000..0ebfba42 --- /dev/null +++ b/test/smt/zeros_ones.unsat.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +$property +function prop(x: range(0, 64)) -> bool = { + let bv: bits(64) = sail_zeros(64 - x) @ sail_ones(x); + if x == 32 then { + bv == 0x0000_0000_FFFF_FFFF + } else { + true + } +} diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 7d4891f9..f17fbc79 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [[96mReplicate/v2.sail[0m]:13:4-30 13[96m |[0m replicate_bits(x, 'N / 'M) [91m |[0m [91m^------------------------^[0m - [91m |[0m Tried performing type coercion from {('ex128# : Int), true. bitvector(('M * 'ex128#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) + [91m |[0m Tried performing type coercion from {('ex193# : Int), true. bitvector(('M * 'ex193#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) [91m |[0m Coercion failed because: [91m |[0m Mismatched argument types in subtype check [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index cc8b874f..940ba4d5 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -4,5 +4,5 @@ Type error: [91m |[0m [91m^[0m [91m |[0m Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4 [91m |[0m Coercion failed because: - [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) + [91m |[0m Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index c01d8359..b52572e5 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -4,5 +4,5 @@ Type error: [91m |[0m [91m^[0m [91m |[0m Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4 [91m |[0m Coercion failed because: - [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) + [91m |[0m Could not prove constraints (0 <= 'n & 'n < 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index d63918b4..11563de1 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -2,5 +2,5 @@ Type error: [[96mexist_synonym/v3.sail[0m]:9:38-47 9[96m |[0mval test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit [91m |[0m [91m^-------^[0m - [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) + [91m |[0m Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index 8157c64f..30e51117 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -2,5 +2,5 @@ Type error: [[96mexist_synonym/v4.sail[0m]:9:35-44 9[96m |[0mval test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit [91m |[0m [91m^-------^[0m - [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) + [91m |[0m Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) [91m |[0m diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 78711c2b..f051c61c 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26[96m |[0m Some(Ctor1(a, x, c)) [91m |[0m [91m^------------^[0m [91m |[0m Could not resolve quantifiers for Ctor1 - [91m |[0m [94m*[0m datasize('ex205#) + [91m |[0m [94m*[0m datasize('ex269#) [91m |[0m diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 40657d0c..36577bf6 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -2,19 +2,19 @@ Type error: [[96mexistential_ast3/v1.sail[0m]:17:48-65 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [91m^---------------^[0m - [91m |[0m Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a)) + [91m |[0m Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (33, unsigned(a)) [91m |[0m Coercion failed because: - [91m |[0m (int(33), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#)) + [91m |[0m (int(33), int('ex231#)) is not a subtype of (int('ex226#), int('ex227#)) [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex162# bound here + [91m |[0m [93m |[0m 'ex226# bound here [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex163# bound here + [91m |[0m [93m |[0m 'ex227# bound here [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex167# bound here + [91m |[0m [93m |[0m 'ex231# bound here [91m |[0m diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 8954736e..cc1ff08e 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -2,19 +2,19 @@ Type error: [[96mexistential_ast3/v2.sail[0m]:17:48-65 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [91m^---------------^[0m - [91m |[0m Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a)) + [91m |[0m Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (31, unsigned(a)) [91m |[0m Coercion failed because: - [91m |[0m (int(31), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#)) + [91m |[0m (int(31), int('ex231#)) is not a subtype of (int('ex226#), int('ex227#)) [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex162# bound here + [91m |[0m [93m |[0m 'ex226# bound here [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex163# bound here + [91m |[0m [93m |[0m 'ex227# bound here [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex167# bound here + [91m |[0m [93m |[0m 'ex231# bound here [91m |[0m diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index d0fcdc06..36a342b3 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25[96m |[0m Some(Ctor(64, unsigned(0b0 @ b @ a))) [91m |[0m [91m^-----------------------------^[0m [91m |[0m Could not resolve quantifiers for Ctor - [91m |[0m [94m*[0m (datasize(64) & (0 <= 'ex206# & ('ex206# + 1) <= 64)) + [91m |[0m [94m*[0m (datasize(64) & (0 <= 'ex270# & 'ex270# < 64)) [91m |[0m diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index e236d4b6..01403d0a 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 'ex124# & ('ex124# + 1) <= 3) + [91m |[0m [94m*[0m (0 <= 'ex187# & 'ex187# < 3) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index fa7fb9ff..ea492ea7 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 'ex124# & ('ex124# + 1) <= 4) + [91m |[0m [94m*[0m (0 <= 'ex187# & 'ex187# < 4) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/type_pow_zero.sail b/test/typecheck/pass/type_pow_zero.sail new file mode 100644 index 00000000..cc7b5736 --- /dev/null +++ b/test/typecheck/pass/type_pow_zero.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <flow.sail> + +/* Run this test with CVC4, as we want to test that 1 - 1 gets +simplified, and 2 ^ 0 evaluates directly to 1. CVC4 doesn't deal with +power unlike z3, so by using it we ensure we check this. */ +$option -smt_solver cvc4 + +function test() -> unit = { + _prove(constraint(2 ^ (1 - 1) == 1)) +} diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index 36bd848e..7f4e734b 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m (0 <= 10 & 10 < 8) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index efbfcc54..f4e10cfa 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m (0 <= 10 & 10 < 8) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index 9ce8f9a2..af54ddf8 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_update, tried: [91m |[0m [94m*[0m bitvector_update [91m |[0m Could not resolve quantifiers for bitvector_update - [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m (0 <= 10 & 10 < 8) [91m |[0m [94m*[0m plain_vector_update [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index dba312ea..b50bf1ef 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_update, tried: [91m |[0m [94m*[0m bitvector_update [91m |[0m Could not resolve quantifiers for bitvector_update - [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m (0 <= 10 & 10 < 8) [91m |[0m [94m*[0m plain_vector_update [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect index 88e6fa50..7536498d 100644 --- a/test/typecheck/pass/vec_length/v3.expect +++ b/test/typecheck/pass/vec_length/v3.expect @@ -7,7 +7,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m (0 <= 10 & 10 < 8) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/wf_specs.sail b/test/typecheck/pass/wf_specs.sail new file mode 100644 index 00000000..2bacf7e0 --- /dev/null +++ b/test/typecheck/pass/wf_specs.sail @@ -0,0 +1,11 @@ +/* Example from https://github.com/rems-project/sail/issues/47 where a variable + name is mistakenly used at the type level, which wasn't caught before due to + the lack of a well-formedness check on specs. This is the corrected version. + */ + +default Order dec +$include <prelude.sail> + +let 'THIRTY_TWO : atom(32) = 32 + +val f : bits(32) -> bits('THIRTY_TWO) diff --git a/test/typecheck/pass/wf_specs/wf_specs.expect b/test/typecheck/pass/wf_specs/wf_specs.expect new file mode 100644 index 00000000..88844e18 --- /dev/null +++ b/test/typecheck/pass/wf_specs/wf_specs.expect @@ -0,0 +1,6 @@ +Type error: +[[96mwf_specs/wf_specs.sail[0m]:10:25-35 +10[96m |[0mval f : bits(32) -> bits(THIRTY_TWO) + [91m |[0m [91m^--------^[0m + [91m |[0m Undefined synonym THIRTY_TWO + [91m |[0m diff --git a/test/typecheck/pass/wf_specs/wf_specs.sail b/test/typecheck/pass/wf_specs/wf_specs.sail new file mode 100644 index 00000000..bb108ee3 --- /dev/null +++ b/test/typecheck/pass/wf_specs/wf_specs.sail @@ -0,0 +1,10 @@ +/* Example from https://github.com/rems-project/sail/issues/47 where a variable + name is mistakenly used at the type level, which wasn't caught before due to + the lack of a well-formedness check on specs. */ + +default Order dec +$include <prelude.sail> + +let THIRTY_TWO : atom(32) = 32 + +val f : bits(32) -> bits(THIRTY_TWO) |