diff options
Diffstat (limited to 'test/typecheck')
22 files changed, 222 insertions, 5 deletions
diff --git a/test/typecheck/fail/scattered_union_rec.expect b/test/typecheck/fail/scattered_union_rec.expect new file mode 100644 index 00000000..cbc9f70a --- /dev/null +++ b/test/typecheck/fail/scattered_union_rec.expect @@ -0,0 +1,16 @@ +Type error: +[[96mscattered_union_rec.sail[0m]:6:24-25 +6[96m |[0munion clause U = Ctor : E + [91m |[0m [91m^[0m + [91m |[0m Undefined type E + [91m |[0m This error was caused by: + [91m |[0m [[96mscattered_union_rec.sail[0m]:6:0-25 + [91m |[0m 6[96m |[0munion clause U = Ctor : E + [91m |[0m [91m |[0m[91m^-----------------------^[0m + [91m |[0m [91m |[0m Types are not well-formed within this type definition. Note that recursive types are forbidden. + [91m |[0m This error was caused by: + [91m |[0m [[96mscattered_union_rec.sail[0m]:6:13-14 + [91m |[0m 6[96m |[0munion clause U = Ctor : E + [91m |[0m [91m |[0m [91m^[0m + [91m |[0m [91m |[0m As this is a scattered union clause, this could also be caused by using a type defined after the 'scattered union' declaration + [91m |[0m diff --git a/test/typecheck/fail/scattered_union_rec.sail b/test/typecheck/fail/scattered_union_rec.sail new file mode 100644 index 00000000..9f005f4e --- /dev/null +++ b/test/typecheck/fail/scattered_union_rec.sail @@ -0,0 +1,6 @@ + +scattered union U + +enum E = A | B | C + +union clause U = Ctor : E diff --git a/test/typecheck/fail/shadow_leak_check.expect b/test/typecheck/fail/shadow_leak_check.expect new file mode 100644 index 00000000..a92e0078 --- /dev/null +++ b/test/typecheck/fail/shadow_leak_check.expect @@ -0,0 +1,8 @@ +Type error: +[[96mshadow_leak_check.sail[0m]:17:5-18:6 +17[96m |[0m let 'x = some_other_int(); + [91m |[0m [91m^-------------------------[0m +18[96m |[0m x + [91m |[0m[91m-----^[0m + [91m |[0m Type variable 'x would leak into a scope where it is shadowed + [91m |[0m diff --git a/test/typecheck/fail/shadow_leak_check.sail b/test/typecheck/fail/shadow_leak_check.sail new file mode 100644 index 00000000..266a0469 --- /dev/null +++ b/test/typecheck/fail/shadow_leak_check.sail @@ -0,0 +1,24 @@ +default Order dec + +function some_int() -> int = { + 4 +} + +function some_other_int() -> int = { + 5 +} + +val test : forall 'n 'm, 'n == 'm. (int('n), int('m)) -> unit + +function main() -> unit = { + let 'x = some_int(); + + let 'y: int('x) = { + let 'x = some_other_int(); + x + }; + + _prove(constraint('x == 'y)); + + test(x, y) +} diff --git a/test/typecheck/fail/shadow_leak_infer.expect b/test/typecheck/fail/shadow_leak_infer.expect new file mode 100644 index 00000000..63aba5d7 --- /dev/null +++ b/test/typecheck/fail/shadow_leak_infer.expect @@ -0,0 +1,8 @@ +Type error: +[[96mshadow_leak_infer.sail[0m]:17:5-18:6 +17[96m |[0m let 'x = some_other_int(); + [91m |[0m [91m^-------------------------[0m +18[96m |[0m x + [91m |[0m[91m-----^[0m + [91m |[0m Type variable '_x would leak into a scope where it is shadowed + [91m |[0m diff --git a/test/typecheck/fail/shadow_leak_infer.sail b/test/typecheck/fail/shadow_leak_infer.sail new file mode 100644 index 00000000..cb122cf9 --- /dev/null +++ b/test/typecheck/fail/shadow_leak_infer.sail @@ -0,0 +1,24 @@ +default Order dec + +function some_int() -> int = { + 4 +} + +function some_other_int() -> int = { + 5 +} + +val test : forall 'n 'm, 'n == 'm. (int('n), int('m)) -> unit + +function main() -> unit = { + let 'x = some_int(); + + let 'y = { + let 'x = some_other_int(); + x + }; + + _prove(constraint('x == 'y)); + + test(x, y) +} diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect new file mode 100644 index 00000000..2b5b1852 --- /dev/null +++ b/test/typecheck/fail/struct_rec.expect @@ -0,0 +1,13 @@ +Type error: +[[96mstruct_rec.sail[0m]:3:10-11 +3[96m |[0m field : S + [91m |[0m [91m^[0m + [91m |[0m Undefined type S + [91m |[0m This error was caused by: + [91m |[0m [[96mstruct_rec.sail[0m]:2:0-4:1 + [91m |[0m 2[96m |[0mstruct S = { + [91m |[0m [91m |[0m[91m^-----------[0m + [91m |[0m 4[96m |[0m} + [91m |[0m [91m |[0m[91m^[0m + [91m |[0m [91m |[0m Types are not well-formed within this type definition. Note that recursive types are forbidden. + [91m |[0m diff --git a/test/typecheck/fail/struct_rec.sail b/test/typecheck/fail/struct_rec.sail new file mode 100644 index 00000000..01c29d6d --- /dev/null +++ b/test/typecheck/fail/struct_rec.sail @@ -0,0 +1,4 @@ + +struct S = { + field : S +} diff --git a/test/typecheck/fail/synonym_rec.expect b/test/typecheck/fail/synonym_rec.expect new file mode 100644 index 00000000..3d482f40 --- /dev/null +++ b/test/typecheck/fail/synonym_rec.expect @@ -0,0 +1,11 @@ +Type error: +[[96msynonym_rec.sail[0m]:2:9-10 +2[96m |[0mtype T = T + [91m |[0m [91m^[0m + [91m |[0m Undefined type T + [91m |[0m This error was caused by: + [91m |[0m [[96msynonym_rec.sail[0m]:2:0-10 + [91m |[0m 2[96m |[0mtype T = T + [91m |[0m [91m |[0m[91m^--------^[0m + [91m |[0m [91m |[0m Types are not well-formed within this type definition. Note that recursive types are forbidden. + [91m |[0m diff --git a/test/typecheck/fail/synonym_rec.sail b/test/typecheck/fail/synonym_rec.sail new file mode 100644 index 00000000..54906418 --- /dev/null +++ b/test/typecheck/fail/synonym_rec.sail @@ -0,0 +1,2 @@ + +type T = T diff --git a/test/typecheck/fail/union_rec.expect b/test/typecheck/fail/union_rec.expect new file mode 100644 index 00000000..7fd07169 --- /dev/null +++ b/test/typecheck/fail/union_rec.expect @@ -0,0 +1,13 @@ +Type error: +[[96munion_rec.sail[0m]:3:9-10 +3[96m |[0m Ctor : U + [91m |[0m [91m^[0m + [91m |[0m Undefined type U + [91m |[0m This error was caused by: + [91m |[0m [[96munion_rec.sail[0m]:2:0-4:1 + [91m |[0m 2[96m |[0munion U = { + [91m |[0m [91m |[0m[91m^----------[0m + [91m |[0m 4[96m |[0m} + [91m |[0m [91m |[0m[91m^[0m + [91m |[0m [91m |[0m Types are not well-formed within this type definition. Note that recursive types are forbidden. + [91m |[0m diff --git a/test/typecheck/fail/union_rec.sail b/test/typecheck/fail/union_rec.sail new file mode 100644 index 00000000..7ca7b8e9 --- /dev/null +++ b/test/typecheck/fail/union_rec.sail @@ -0,0 +1,4 @@ + +union U = { + Ctor : U +} diff --git a/test/typecheck/fail/union_recf.expect b/test/typecheck/fail/union_recf.expect new file mode 100644 index 00000000..ec610ae6 --- /dev/null +++ b/test/typecheck/fail/union_recf.expect @@ -0,0 +1,13 @@ +Type error: +[[96munion_recf.sail[0m]:3:9-10 +3[96m |[0m Ctor : U -> U + [91m |[0m [91m^[0m + [91m |[0m Undefined type U + [91m |[0m This error was caused by: + [91m |[0m [[96munion_recf.sail[0m]:2:0-4:1 + [91m |[0m 2[96m |[0munion U = { + [91m |[0m [91m |[0m[91m^----------[0m + [91m |[0m 4[96m |[0m} + [91m |[0m [91m |[0m[91m^[0m + [91m |[0m [91m |[0m Types are not well-formed within this type definition. Note that recursive types are forbidden. + [91m |[0m diff --git a/test/typecheck/fail/union_recf.sail b/test/typecheck/fail/union_recf.sail new file mode 100644 index 00000000..f64ca675 --- /dev/null +++ b/test/typecheck/fail/union_recf.sail @@ -0,0 +1,4 @@ + +union U = { + Ctor : U -> U +} diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect index 8c95193d..0b0dda29 100644 --- a/test/typecheck/pass/constrained_struct/v1.expect +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -3,4 +3,9 @@ Type error: 10[96m |[0mtype MyStruct64 = MyStruct(65) [91m |[0m [91m^------^[0m [91m |[0m Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct + [91m |[0m This error was caused by: + [91m |[0m [[96mconstrained_struct/v1.sail[0m]:10:0-30 + [91m |[0m 10[96m |[0mtype MyStruct64 = MyStruct(65) + [91m |[0m [91m |[0m[91m^----------------------------^[0m + [91m |[0m [91m |[0m Types are not well-formed within this type definition. Note that recursive types are forbidden. [91m |[0m diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index e2823692..8d061933 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('ex270#) + [91m |[0m [94m*[0m datasize('ex276#) [91m |[0m diff --git a/test/typecheck/pass/mapping_rreg.sail b/test/typecheck/pass/mapping_rreg.sail new file mode 100644 index 00000000..1f3e1212 --- /dev/null +++ b/test/typecheck/pass/mapping_rreg.sail @@ -0,0 +1,17 @@ +default Order dec + +$include <prelude.sail> + +register enabled : bits(1) + +union ast = { + I: bits(1) +} + +val encdec : ast <-> bits(2) effect {rreg} + +scattered mapping encdec + +mapping clause encdec = I(imm) if enabled == 0b0 <-> 0b0 @ imm if enabled == 0b0 + +end encdec diff --git a/test/typecheck/pass/new_bitfields.sail b/test/typecheck/pass/new_bitfields.sail new file mode 100644 index 00000000..fdb17576 --- /dev/null +++ b/test/typecheck/pass/new_bitfields.sail @@ -0,0 +1,16 @@ +default Order dec + +$include <prelude.sail> + +$option -new_bitfields + +bitfield B : bits(32) = { + Field: 7..0 +} + +register R : B + +function main() -> unit = { + R[Field] = 0xFF; + assert(R[Field] == 0xFF) +}
\ No newline at end of file diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect index 24439bed..90166904 100644 --- a/test/typecheck/pass/reg_32_64/v2.expect +++ b/test/typecheck/pass/reg_32_64/v2.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data [91m |[0m Coercion failed because: [91m |[0m Mismatched argument types in subtype check - [91m |[0m This error occured because of a previous error: + [91m |[0m This error was caused by: [91m |[0m [[96mreg_32_64/v2.sail[0m]:21:2-15 [91m |[0m 21[96m |[0m (*R)['d .. 0] = data [91m |[0m [91m |[0m [91m^-----------^[0m diff --git a/test/typecheck/pass/union_recf_ok.sail b/test/typecheck/pass/union_recf_ok.sail new file mode 100644 index 00000000..0f415601 --- /dev/null +++ b/test/typecheck/pass/union_recf_ok.sail @@ -0,0 +1,4 @@ + +union U = { + Ctor : int -> U +}
\ No newline at end of file diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index e5650646..adc30c42 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -87,6 +87,24 @@ do done done +for file in $DIR/fail/*.sail; +do + pushd $DIR/fail > /dev/null; + if $SAILDIR/sail -no_memo_z3 $(basename $file) 2> result + then + red "Expected failure, but $i $(basename $file) passed" "fail" + else + if diff ${file%.sail}.expect result; + then + green "failing $i $(basename $file)" "pass" + else + yellow "failing $i $(basename $file)" "unexpected error" + fi + fi; + rm -f result; + popd > /dev/null +done + finish_suite "Typechecking tests" printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh index ba436daf..1d174797 100755 --- a/test/typecheck/update_errors.sh +++ b/test/typecheck/update_errors.sh @@ -10,8 +10,15 @@ do shopt -s nullglob; for file in $DIR/pass/${i%.sail}/*.sail; do - pushd $DIR/pass > /dev/null; - $SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true; - popd > /dev/null + pushd $DIR/pass > /dev/null; + $SAILDIR/sail -no_memo_z3 ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true; + popd > /dev/null done done + +for file in $DIR/fail/*.sail; +do + pushd $DIR/fail > /dev/null; + $SAILDIR/sail -no_memo_z3 $(basename $file) 2> ${file%.sail}.expect || true; + popd > /dev/null +done |