From 0a293f2e7ca72e1dc422f0035d271d7dc39cfcb2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 26 Dec 2018 00:41:43 +0000 Subject: More error messages improvments --- test/typecheck/pass/bool_constraint/v1.expect | 21 ++++++++++++++++++++- test/typecheck/pass/bool_constraint/v2.expect | 1 + test/typecheck/pass/bool_constraint/v3.expect | 1 + test/typecheck/pass/bool_constraint/v4.expect | 1 + test/typecheck/pass/constrained_struct/v1.expect | 1 + test/typecheck/pass/constraint_ctor/v1.expect | 1 + test/typecheck/pass/constraint_ctor/v2.expect | 1 + test/typecheck/pass/constraint_ctor/v3.expect | 1 + test/typecheck/pass/constraint_ctor/v4.expect | 1 + test/typecheck/pass/constraint_ctor/v5.expect | 1 + test/typecheck/pass/exist_synonym/v1.expect | 1 + test/typecheck/pass/exist_synonym/v2.expect | 1 + test/typecheck/pass/exist_synonym/v3.expect | 4 +++- test/typecheck/pass/exist_synonym/v4.expect | 4 +++- test/typecheck/pass/function_namespace/v1.expect | 1 + test/typecheck/pass/global_type_var/v1.expect | 1 + test/typecheck/pass/global_type_var/v2.expect | 1 + test/typecheck/pass/global_type_var/v3.expect | 1 + test/typecheck/pass/if_infer/v1.expect | 1 + test/typecheck/pass/if_infer/v2.expect | 1 + test/typecheck/pass/if_infer/v3.expect | 1 + test/typecheck/pass/not_pattern/v1.expect | 1 + test/typecheck/pass/vec_length/v1.expect | 1 + test/typecheck/pass/vec_length/v1_inc.expect | 1 + test/typecheck/pass/vec_length/v2.expect | 1 + test/typecheck/pass/vec_length/v2_inc.expect | 1 + test/typecheck/pass/vec_length/v3.expect | 14 ++++++++++++++ test/typecheck/pass/vec_length/v3.sail | 14 ++++++++++++++ 28 files changed, 77 insertions(+), 3 deletions(-) create mode 100644 test/typecheck/pass/vec_length/v3.expect create mode 100644 test/typecheck/pass/vec_length/v3.sail (limited to 'test') diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect index 34fdea2b..b1597759 100644 --- a/test/typecheck/pass/bool_constraint/v1.expect +++ b/test/typecheck/pass/bool_constraint/v1.expect @@ -1 +1,20 @@ -Fatal error: exception Failure("No location") +Type error: +[bool_constraint/v1.sail]:12:19-20 +12 | if b then n else 4 +  | ^ +  | Tried performing type coercion from int(4) to {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} on 4 +  | Coercion failed because: +  | int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} +  | [bool_constraint/v1.sail]:11:0-13:1 +  | 11 |function foo(b, n) = { +  |  |^--------------------- +  | 13 |} +  |  |^ +  |  | 'b bound here +  | [bool_constraint/v1.sail]:11:0-13:1 +  | 11 |function foo(b, n) = { +  |  |^--------------------- +  | 13 |} +  |  |^ +  |  | 'n bound here +  | diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect index 989226fb..c7a355e1 100644 --- a/test/typecheck/pass/bool_constraint/v2.expect +++ b/test/typecheck/pass/bool_constraint/v2.expect @@ -1,3 +1,4 @@ +Type error: [bool_constraint/v2.sail]:38:4-32 38 | _prove(constraint('n <= 14))  | ^--------------------------^ diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect index 51692dd7..63791a70 100644 --- a/test/typecheck/pass/bool_constraint/v3.expect +++ b/test/typecheck/pass/bool_constraint/v3.expect @@ -1,3 +1,4 @@ +Type error: [bool_constraint/v3.sail]:46:4-32 46 | _prove(constraint('n <= 14))  | ^--------------------------^ diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect index df65fc8a..420909bf 100644 --- a/test/typecheck/pass/bool_constraint/v4.expect +++ b/test/typecheck/pass/bool_constraint/v4.expect @@ -1,3 +1,4 @@ +Type error: [bool_constraint/v4.sail]:46:4-32 46 | _prove(constraint('n <= 13))  | ^--------------------------^ diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect index f3771c9d..8c95193d 100644 --- a/test/typecheck/pass/constrained_struct/v1.expect +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -1,3 +1,4 @@ +Type error: [constrained_struct/v1.sail]:10:18-26 10 |type MyStruct64 = MyStruct(65)  | ^------^ diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect index b2c62a8c..cf3b9399 100644 --- a/test/typecheck/pass/constraint_ctor/v1.expect +++ b/test/typecheck/pass/constraint_ctor/v1.expect @@ -1,3 +1,4 @@ +Type error: [constraint_ctor/v1.sail]:10:2-29 10 | _prove(constraint('x >= 4));  | ^-------------------------^ diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect index a6774adc..0e56f0a4 100644 --- a/test/typecheck/pass/constraint_ctor/v2.expect +++ b/test/typecheck/pass/constraint_ctor/v2.expect @@ -1,3 +1,4 @@ +Type error: [constraint_ctor/v2.sail]:18:2-30 18 | _prove(constraint('x >= 24));  | ^--------------------------^ diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect index bd93a7e1..37d1dff2 100644 --- a/test/typecheck/pass/constraint_ctor/v3.expect +++ b/test/typecheck/pass/constraint_ctor/v3.expect @@ -1,3 +1,4 @@ +Type error: [constraint_ctor/v3.sail]:18:2-30 18 | _prove(constraint('x >= 23));  | ^--------------------------^ diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect index 942db0a4..64893e4d 100644 --- a/test/typecheck/pass/constraint_ctor/v4.expect +++ b/test/typecheck/pass/constraint_ctor/v4.expect @@ -1,3 +1,4 @@ +Type error: [constraint_ctor/v4.sail]:17:33-36 17 |function bar(Bar(x as int('x)) : Bar(23)) -> unit = {  | ^-^ diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect index 93fb2a43..fc2ef615 100644 --- a/test/typecheck/pass/constraint_ctor/v5.expect +++ b/test/typecheck/pass/constraint_ctor/v5.expect @@ -1,3 +1,4 @@ +Type error: [constraint_ctor/v5.sail]:27:2-29 27 | _prove(constraint('x >= 4));  | ^-------------------------^ diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index 651dda4c..cc8b874f 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -1,3 +1,4 @@ +Type error: [exist_synonym/v1.sail]:6:41-42 6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4  | ^ diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index d5617688..c01d8359 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -1,3 +1,4 @@ +Type error: [exist_synonym/v2.sail]:6:40-41 6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4  | ^ diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index 34fdea2b..c237ae2d 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1 +1,3 @@ -Fatal error: exception Failure("No location") +Type error: +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) + diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index 34fdea2b..1cbc3df8 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1 +1,3 @@ -Fatal error: exception Failure("No location") +Type error: +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) + diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect index 15ab6962..2bb734aa 100644 --- a/test/typecheck/pass/function_namespace/v1.expect +++ b/test/typecheck/pass/function_namespace/v1.expect @@ -1,3 +1,4 @@ +Type error: [function_namespace/v1.sail]:9:6-10 9 | let test = true;  | ^--^ diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index 22a3756d..ac4428c6 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/test/typecheck/pass/global_type_var/v1.expect @@ -1,3 +1,4 @@ +Type error: [global_type_var/v1.sail]:23:13-15 23 |let _ = test(32)  | ^^ diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index 360a6e48..93eb628b 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/test/typecheck/pass/global_type_var/v2.expect @@ -1,3 +1,4 @@ +Type error: [global_type_var/v2.sail]:23:13-15 23 |let _ = test(64)  | ^^ diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect index 8e687370..6def5172 100644 --- a/test/typecheck/pass/global_type_var/v3.expect +++ b/test/typecheck/pass/global_type_var/v3.expect @@ -1,3 +1,4 @@ +Type error: [global_type_var/v3.sail]:15:23-27 15 | let y : atom(64) = size in  | ^--^ diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index e9db69f5..c8217478 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -1,3 +1,4 @@ +Type error: [if_infer/v1.sail]:10:10-37 10 | let _ = 0b100[if R then 0 else f()];  | ^-------------------------^ diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 06800859..f0c2fab3 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -1,3 +1,4 @@ +Type error: [if_infer/v2.sail]:10:10-38 10 | let _ = 0b1001[if R then 0 else f()];  | ^--------------------------^ diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect index b701032d..7e0e74bb 100644 --- a/test/typecheck/pass/if_infer/v3.expect +++ b/test/typecheck/pass/if_infer/v3.expect @@ -1,3 +1,4 @@ +Type error: [if_infer/v3.sail]:10:10-38 10 | let _ = 0b1001[if R then 0 else f()];  | ^--------------------------^ diff --git a/test/typecheck/pass/not_pattern/v1.expect b/test/typecheck/pass/not_pattern/v1.expect index 2b766c43..aeefb901 100644 --- a/test/typecheck/pass/not_pattern/v1.expect +++ b/test/typecheck/pass/not_pattern/v1.expect @@ -1,3 +1,4 @@ +Type error: [not_pattern/v1.sail]:12:6-7 12 | ~(y) => (),  | ^ diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index 096b09a7..ce61cf2a 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -1,3 +1,4 @@ +Type error: [vec_length/v1.sail]:6:10-15 6 | let y = x[10];  | ^---^ diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index c42b12ad..3d40cdb0 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -1,3 +1,4 @@ +Type error: [vec_length/v1_inc.sail]:6:10-15 6 | let y = x[10];  | ^---^ diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index 7b0e6634..c77ecaa7 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -1,3 +1,4 @@ +Type error: [vec_length/v2.sail]:7:10-25 7 | 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 index f7ef04e4..cff65f62 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -1,3 +1,4 @@ +Type error: [vec_length/v2_inc.sail]:7:10-25 7 | let z = [x with 10 = y];  | ^-------------^ diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect new file mode 100644 index 00000000..e3afecee --- /dev/null +++ b/test/typecheck/pass/vec_length/v3.expect @@ -0,0 +1,14 @@ +Type error: +[vec_length/v3.sail]:6:10-12:3 +6  | let y = x[ +  | ^- +12 | ]; +  |--^ +  | No overloading for vector_access, tried: +  | * bitvector_access +  | Could not resolve quantifiers for bitvector_access +  | * (0 <= 10 & (10 + 1) <= 8) +  | * plain_vector_access +  | Could not resolve quantifiers for plain_vector_access +  | * (0 <= 10 & (10 + 1) <= 8) +  | diff --git a/test/typecheck/pass/vec_length/v3.sail b/test/typecheck/pass/vec_length/v3.sail new file mode 100644 index 00000000..8736278e --- /dev/null +++ b/test/typecheck/pass/vec_length/v3.sail @@ -0,0 +1,14 @@ +default Order dec +$include + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[ + + + + + 10 + ]; + () +} -- cgit v1.2.3