From 1edd0e73a7d19904639341fd360fff5fa3ff4fec Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 5 Nov 2019 18:04:51 +0000 Subject: Make sure we correctly forbid recursive datatypes that we don't want to support Ensure we give a nice error message that explains that recursive types are forbidden ``` Type error: [struct_rec.sail]:3:10-11 3 | field : S | ^ | Undefined type S | This error was caused by: | [struct_rec.sail]:2:0-4:1 | 2 |struct S = { | |^----------- | 4 |} | |^ | | Recursive types are not allowed ``` The theorem prover backends create a special register_value union that can be recursive, so we make sure to special case that. --- test/typecheck/fail/struct_rec.expect | 13 +++++++++++++ test/typecheck/fail/struct_rec.sail | 4 ++++ test/typecheck/fail/synonym_rec.expect | 11 +++++++++++ test/typecheck/fail/synonym_rec.sail | 2 ++ test/typecheck/fail/union_rec.expect | 13 +++++++++++++ test/typecheck/fail/union_rec.sail | 4 ++++ test/typecheck/fail/union_recf.expect | 13 +++++++++++++ test/typecheck/fail/union_recf.sail | 4 ++++ test/typecheck/pass/constrained_struct/v1.expect | 5 +++++ test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/reg_32_64/v2.expect | 2 +- test/typecheck/pass/union_recf_ok.sail | 4 ++++ test/typecheck/run_tests.sh | 18 ++++++++++++++++++ test/typecheck/update_errors.sh | 13 ++++++++++--- 14 files changed, 103 insertions(+), 5 deletions(-) create mode 100644 test/typecheck/fail/struct_rec.expect create mode 100644 test/typecheck/fail/struct_rec.sail create mode 100644 test/typecheck/fail/synonym_rec.expect create mode 100644 test/typecheck/fail/synonym_rec.sail create mode 100644 test/typecheck/fail/union_rec.expect create mode 100644 test/typecheck/fail/union_rec.sail create mode 100644 test/typecheck/fail/union_recf.expect create mode 100644 test/typecheck/fail/union_recf.sail create mode 100644 test/typecheck/pass/union_recf_ok.sail (limited to 'test') diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect new file mode 100644 index 00000000..6daa067d --- /dev/null +++ b/test/typecheck/fail/struct_rec.expect @@ -0,0 +1,13 @@ +Type error: +[struct_rec.sail]:3:10-11 +3 | field : S +  | ^ +  | Undefined type S +  | This error was caused by: +  | [struct_rec.sail]:2:0-4:1 +  | 2 |struct S = { +  |  |^----------- +  | 4 |} +  |  |^ +  |  | Recursive types are not allowed +  | 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..5d205606 --- /dev/null +++ b/test/typecheck/fail/synonym_rec.expect @@ -0,0 +1,11 @@ +Type error: +[synonym_rec.sail]:2:9-10 +2 |type T = T +  | ^ +  | Undefined type T +  | This error was caused by: +  | [synonym_rec.sail]:2:0-10 +  | 2 |type T = T +  |  |^--------^ +  |  | Recursive types are not allowed +  | 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..2d50cea6 --- /dev/null +++ b/test/typecheck/fail/union_rec.expect @@ -0,0 +1,13 @@ +Type error: +[union_rec.sail]:3:9-10 +3 | Ctor : U +  | ^ +  | Undefined type U +  | This error was caused by: +  | [union_rec.sail]:2:0-4:1 +  | 2 |union U = { +  |  |^---------- +  | 4 |} +  |  |^ +  |  | Recursive types are not allowed +  | 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..b07910ba --- /dev/null +++ b/test/typecheck/fail/union_recf.expect @@ -0,0 +1,13 @@ +Type error: +[union_recf.sail]:3:9-10 +3 | Ctor : U -> U +  | ^ +  | Undefined type U +  | This error was caused by: +  | [union_recf.sail]:2:0-4:1 +  | 2 |union U = { +  |  |^---------- +  | 4 |} +  |  |^ +  |  | Recursive types are not allowed +  | 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..bf498a36 100644 --- a/test/typecheck/pass/constrained_struct/v1.expect +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -3,4 +3,9 @@ Type error: 10 |type MyStruct64 = MyStruct(65)  | ^------^  | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct +  | This error was caused by: +  | [constrained_struct/v1.sail]:10:0-30 +  | 10 |type MyStruct64 = MyStruct(65) +  |  |^----------------------------^ +  |  | Recursive types are not allowed  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index ca83adb9..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 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex273#) +  | * datasize('ex276#)  | 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:  | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data  | Coercion failed because:  | Mismatched argument types in subtype check -  | This error occured because of a previous error: +  | This error was caused by:  | [reg_32_64/v2.sail]:21:2-15  | 21 | (*R)['d .. 0] = data  |  | ^-----------^ 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 "\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 -- cgit v1.2.3