Merge remote-tracking branch 'origin/sail2' into separate_bv

20 files changed, 63 insertions, 24 deletions

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:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | 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)))
+   | 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)))
    | 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 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 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex205#)
+   | * datasize('ex269#)
    | 
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:
 [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('ex167#)) is not a subtype of (int('ex162#), int('ex163#))
+   | (int(33), int('ex231#)) is not a subtype of (int('ex226#), int('ex227#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex162# bound here
+   |    | 'ex226# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex163# bound here
+   |    | 'ex227# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex167# bound here
+   |    | 'ex231# bound here
    | 
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:
 [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('ex167#)) is not a subtype of (int('ex162#), int('ex163#))
+   | (int(31), int('ex231#)) is not a subtype of (int('ex226#), int('ex227#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex162# bound here
+   |    | 'ex226# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex163# bound here
+   |    | 'ex227# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex167# bound here
+   |    | 'ex231# bound here
    | 
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 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex206# & ('ex206# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex270# & 'ex270# < 64))
    | 
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:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex124# & ('ex124# + 1) <= 3)
+   |    * (0 <= 'ex187# & 'ex187# < 3)
    | * plain_vector_access
    |    No valid casts resulted in unification
    | 
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:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex124# & ('ex124# + 1) <= 4)
+   |    * (0 <= 'ex187# & 'ex187# < 4)
    | * plain_vector_access
    |    No valid casts resulted in unification
    | 
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:
   | 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
   |    No valid casts resulted in unification
   | 
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:
   | 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
   |    No valid casts resulted in unification
   | 
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:
   | 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
   |    No valid casts resulted in unification
   | 
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:
   | 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
   |    No valid casts resulted in unification
   | 
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:
    | 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
    |    No valid casts resulted in unification
    | 
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:
+[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 <prelude.sail>
+
+let THIRTY_TWO : atom(32) = 32
+
+val f : bits(32) -> bits(THIRTY_TWO)