From 37c5fb51e9986917a791de73435e182549e21fca Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 4 Jun 2019 17:36:22 +0100 Subject: Make sure aarch64_small can generate Jib for SMT Add a test case for this --- test/aarch64_small/run_tests.sh | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test') diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh index dc2bdde4..424252de 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 smt 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 "\n" >> $DIR/tests.xml -- cgit v1.2.3 From 0cb7d12f606bbfb311108d8dfc114b7829a82c29 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 5 Jun 2019 22:58:41 +0100 Subject: Add some regression tests --- test/c/toplevel_tyvar.expect | 1 + test/c/toplevel_tyvar.sail | 14 ++++++++++++++ test/typecheck/pass/type_pow_zero.sail | 12 ++++++++++++ 3 files changed, 27 insertions(+) create mode 100644 test/c/toplevel_tyvar.expect create mode 100644 test/c/toplevel_tyvar.sail create mode 100644 test/typecheck/pass/type_pow_zero.sail (limited to 'test') 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 + +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/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 + +/* 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)) +} -- cgit v1.2.3 From 1ad5bb9ea7b4462c0ec07b0f6021f6f228834eb5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 6 Jun 2019 15:31:00 +0100 Subject: Add arith_shiftr to C and OCaml libraries --- test/builtins/shift.sail | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 test/builtins/shift.sail (limited to 'test') 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 + +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); +} -- cgit v1.2.3 From ee830e823cbcf773fa6ac0d0606d7b4eff38ac4e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 6 Jun 2019 18:20:11 +0100 Subject: Fix aarch64_small test --- test/aarch64_small/run_tests.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh index 424252de..416ad9f1 100755 --- a/test/aarch64_small/run_tests.sh +++ b/test/aarch64_small/run_tests.sh @@ -52,7 +52,7 @@ else red "failed to build lem" "fail" fi -if make -B -C ../../aarch64_small smt SAIL="$SAILDIR/sail" +if make -B -C ../../aarch64_small armV8.smt_model SAIL="$SAILDIR/sail" then green "compiled aarch64_small for SMT generation" "ok" else -- cgit v1.2.3 From 3eadd260f7382f98eb7dcbd706a3ed3e910167eb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 10 Jun 2019 17:53:58 +0100 Subject: Add well-formedness check for type schemes in valspecs. Fixes #47. Also adjust the nexp substitution so that the error message points to a useful location, and replace the empty environment with the initial environment in a few functions that do type checking to ensure that the prover is set up (which may be needed for the wf check). --- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v2.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 ++-- test/typecheck/pass/if_infer/v2.expect | 4 ++-- test/typecheck/pass/wf_specs.sail | 11 +++++++++++ test/typecheck/pass/wf_specs/wf_specs.expect | 6 ++++++ test/typecheck/pass/wf_specs/wf_specs.sail | 10 ++++++++++ 10 files changed, 42 insertions(+), 15 deletions(-) create mode 100644 test/typecheck/pass/wf_specs.sail create mode 100644 test/typecheck/pass/wf_specs/wf_specs.expect create mode 100644 test/typecheck/pass/wf_specs/wf_specs.sail (limited to 'test') diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index acadd4e2..89ab2910 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:13:4-30 13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex172# : Int), true. vector(('M * 'ex172#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 7bb8a4ab..56b89364 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex196#) +  | * datasize('ex248#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 4b9bd7cc..346b7b75 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | 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))  | Coercion failed because: -  | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#)) +  | (int(33), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex153# bound here +  |  | 'ex205# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex154# bound here +  |  | 'ex206# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex158# bound here +  |  | 'ex210# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 52eb2f13..7f18c94e 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | 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))  | Coercion failed because: -  | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#)) +  | (int(31), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex153# bound here +  |  | 'ex205# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex154# bound here +  |  | 'ex206# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex158# bound here +  |  | 'ex210# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 0e43cd52..585cf2c6 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex249# & ('ex249# + 1) <= 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 011ecbdf..50bd530d 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex115# & ('ex115# + 1) <= 3) +  | * (0 <= 'ex166# & ('ex166# + 1) <= 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex118# & ('ex118# + 1) <= 3) +  | * (0 <= 'ex169# & ('ex169# + 1) <= 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 9a34f688..27b05208 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex115# & ('ex115# + 1) <= 4) +  | * (0 <= 'ex166# & ('ex166# + 1) <= 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex118# & ('ex118# + 1) <= 4) +  | * (0 <= 'ex169# & ('ex169# + 1) <= 4)  | 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 + +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: +[wf_specs/wf_specs.sail]:10:25-35 +10 |val f : bits(32) -> bits(THIRTY_TWO) +  | ^--------^ +  | Undefined synonym THIRTY_TWO +  | 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 + +let THIRTY_TWO : atom(32) = 32 + +val f : bits(32) -> bits(THIRTY_TWO) -- cgit v1.2.3 From 2dd28164e40241a2117142fbb197c967740f196d Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 17 Jun 2019 14:25:01 +0100 Subject: Implement a count_leading_zeros builtin for ocaml and c. This may be a slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends. --- test/builtins/clz.sail | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test/builtins/clz.sail (limited to 'test') 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 + +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 -- cgit v1.2.3 From 65a8bd3e771f5c062c96dbc940b024ec513aeeca Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 18 Jun 2019 14:39:21 +0100 Subject: Implement count_leading_zeros in Lem --- test/builtins/count_leading_zeros.sail | 11 +++++++++++ test/builtins/run_tests.py | 1 + 2 files changed, 12 insertions(+) create mode 100644 test/builtins/count_leading_zeros.sail (limited to 'test') 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 + +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') -- cgit v1.2.3 From 790da51af29e5a17f4bf0c8d95c9bbccb9747b41 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 18 Jun 2019 20:41:21 +0100 Subject: Update test cases --- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v1.expect | 2 +- test/typecheck/pass/exist_synonym/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v3.expect | 2 +- test/typecheck/pass/exist_synonym/v4.expect | 2 +- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 10 +++++----- test/typecheck/pass/existential_ast3/v2.expect | 10 +++++----- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 ++-- test/typecheck/pass/if_infer/v2.expect | 4 ++-- test/typecheck/pass/vec_length/v1.expect | 4 ++-- test/typecheck/pass/vec_length/v1_inc.expect | 4 ++-- test/typecheck/pass/vec_length/v2.expect | 4 ++-- test/typecheck/pass/vec_length/v2_inc.expect | 4 ++-- test/typecheck/pass/vec_length/v3.expect | 4 ++-- 16 files changed, 31 insertions(+), 31 deletions(-) (limited to 'test') diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 89ab2910..151eb1da 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:13:4-30 13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex172# : Int), true. vector(('M * 'ex172#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex174# : Int), true. vector(('M * 'ex174#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | 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:  | ^  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4  | Coercion failed because: -  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) +  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)  | 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:  | ^  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4  | Coercion failed because: -  | Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) +  | Could not prove constraints (0 <= 'n & 'n < 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)  | 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: [exist_synonym/v3.sail]:9:38-47 9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit  | ^-------^ -  | 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) +  | 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)  | 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: [exist_synonym/v4.sail]:9:35-44 9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit  | ^-------^ -  | 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) +  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 56b89364..b6d21c9d 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex248#) +  | * datasize('ex250#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 346b7b75..f926c07e 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -2,19 +2,19 @@ Type error: [existential_ast3/v1.sail]:17:48-65 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  | ^---------------^ -  | 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)) +  | 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))  | Coercion failed because: -  | (int(33), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#)) +  | (int(33), int('ex212#)) is not a subtype of (int('ex207#), int('ex208#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex205# bound here +  |  | 'ex207# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex206# bound here +  |  | 'ex208# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex210# bound here +  |  | 'ex212# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 7f18c94e..f348260d 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -2,19 +2,19 @@ Type error: [existential_ast3/v2.sail]:17:48-65 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  | ^---------------^ -  | 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)) +  | 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))  | Coercion failed because: -  | (int(31), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#)) +  | (int(31), int('ex212#)) is not a subtype of (int('ex207#), int('ex208#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex205# bound here +  |  | 'ex207# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex206# bound here +  |  | 'ex208# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex210# bound here +  |  | 'ex212# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 585cf2c6..9f1f6286 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex249# & ('ex249# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex251# & 'ex251# < 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 50bd530d..3df876b5 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex166# & ('ex166# + 1) <= 3) +  | * (0 <= 'ex168# & 'ex168# < 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex169# & ('ex169# + 1) <= 3) +  | * (0 <= 'ex171# & 'ex171# < 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 27b05208..630a9f2d 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex166# & ('ex166# + 1) <= 4) +  | * (0 <= 'ex168# & 'ex168# < 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex169# & ('ex169# + 1) <= 4) +  | * (0 <= 'ex171# & 'ex171# < 4)  | diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index ce61cf2a..f4cf71c1 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index 3d40cdb0..55f072f2 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index c77ecaa7..349000fb 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_update, tried:  | * bitvector_update  | Could not resolve quantifiers for bitvector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_update  | Could not resolve quantifiers for plain_vector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index cff65f62..1f900286 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_update, tried:  | * bitvector_update  | Could not resolve quantifiers for bitvector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_update  | Could not resolve quantifiers for plain_vector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect index e3afecee..91bb4c99 100644 --- a/test/typecheck/pass/vec_length/v3.expect +++ b/test/typecheck/pass/vec_length/v3.expect @@ -7,8 +7,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | -- cgit v1.2.3 From 2aff0f546d8ee88678a722ed6d98df2617a687c6 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 18 Jun 2019 20:57:16 +0100 Subject: Fix two SMT test cases --- test/smt/assembly_mapping.sat.sail | 4 ++-- test/smt/encdec.sat.sail | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'test') 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) -- cgit v1.2.3 From 061c7da3c0629d5fc6cc4a9a91bf4b251b61863d Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 18 Jun 2019 16:57:44 +0100 Subject: Monomorphisation improvements for aarch64_small - additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!) --- test/mono/castreq.sail | 17 ++++++++++++++++- test/mono/pass/repeatedint | 1 + test/mono/repeatedint.sail | 22 ++++++++++++++++++++++ 3 files changed, 39 insertions(+), 1 deletion(-) create mode 100644 test/mono/pass/repeatedint create mode 100644 test/mono/repeatedint.sail (limited to 'test') diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail index bb1bc952..e8fbabb0 100644 --- a/test/mono/castreq.sail +++ b/test/mono/castreq.sail @@ -33,6 +33,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 +53,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) = @@ -116,4 +131,4 @@ function run () = { 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 + +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); +} -- cgit v1.2.3 From 414b8f4e103bd6112001fe140cfb3b32c97e8bb5 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 19 Jun 2019 17:04:31 +0100 Subject: Make C emulator exit with failure for uncaught exception. Make special case for 'exception.sail' test that deliberately exits with uncaught exception. --- test/c/run_tests.py | 6 +++--- test/sailtest.py | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'test') 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/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) -- cgit v1.2.3 From 56ad3c612c662ecedb4ee83845ec15815ae264c2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 20 Jun 2019 12:17:23 +0100 Subject: Handle more uses of mutable variables during monomorphisation cast insertion In particular, bitvector subrange updates work with this version. --- test/mono/castreq.sail | 45 ++++++++++++++++++++++++++++++++++++++------- test/mono/run_tests.sh | 2 +- 2 files changed, 39 insertions(+), 8 deletions(-) (limited to 'test') diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail index e8fbabb0..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)) */ @@ -69,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 { @@ -82,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 */ @@ -123,10 +150,14 @@ 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); 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" -- cgit v1.2.3 From 7a5f75524c59bf885d7c31ed1ae8a7cfe725d5dc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 21 Jun 2019 10:57:15 +0100 Subject: Coq: be more careful when dealing with wildcard argument patterns If they're merged with a type variable then we still need to name the argument so that it can be used in other types. --- test/coq/pass/wildcardmerge.sail | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test/coq/pass/wildcardmerge.sail (limited to 'test') 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 + +/* 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(_,_) = () -- cgit v1.2.3 From e8697cb036720cdf75687f0c442c49dd48913bcb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 21 Jun 2019 14:44:29 +0100 Subject: Coq: add missing property derivation casts for effectful expressions These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere. --- test/coq/pass/returnwithfact.sail | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test/coq/pass/returnwithfact.sail (limited to 'test') 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 + +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) -- cgit v1.2.3 From e3041e8206b886e547923a1280e6267d898b9871 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 25 Jun 2019 14:16:17 +0100 Subject: SMT: Add another case to append --- test/smt/zeros_ones.unsat.sail | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/smt/zeros_ones.unsat.sail (limited to 'test') 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 + +$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 + } +} -- cgit v1.2.3 From d9e8b93142c3d4cfd75c123800b714b0393c5a6e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 27 Jun 2019 19:31:01 +0100 Subject: SMT: Add a reverse endianness function and fix some bugs --- test/smt/revrev_endianness.sail | 25 +++++++++++++++++++++++++ test/smt/revrev_endianness2.sail | 20 ++++++++++++++++++++ 2 files changed, 45 insertions(+) create mode 100644 test/smt/revrev_endianness.sail create mode 100644 test/smt/revrev_endianness2.sail (limited to 'test') 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 + +$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 + +$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 + } +} -- cgit v1.2.3