diff options
| author | Alasdair Armstrong | 2019-05-13 18:03:35 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-14 15:13:29 +0100 |
| commit | 41e6fe10e7d28193fa62711fcdad797b1f0103a0 (patch) | |
| tree | 0113597f0c1b5ba909028f576a6a51c8dbead6ac /test/typecheck | |
| parent | 7257b23239a3f8d6a45f973b9d953b31772abe06 (diff) | |
Add feature that allows functions to require type variables are constant
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
Diffstat (limited to 'test/typecheck')
| -rw-r--r-- | test/typecheck/pass/constant_nexp.sail | 13 | ||||
| -rw-r--r-- | test/typecheck/pass/constant_nexp/v1.expect | 7 | ||||
| -rw-r--r-- | test/typecheck/pass/constant_nexp/v1.sail | 13 | ||||
| -rw-r--r-- | test/typecheck/pass/constant_nexp/v2.expect | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/constant_nexp/v2.sail | 14 |
5 files changed, 55 insertions, 0 deletions
diff --git a/test/typecheck/pass/constant_nexp.sail b/test/typecheck/pass/constant_nexp.sail new file mode 100644 index 00000000..d8213d42 --- /dev/null +++ b/test/typecheck/pass/constant_nexp.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val czeros = "zeros" : forall (constant 'n : Int), 'n >= 0. int('n) -> bits('n) + +val multi_param : forall (constant 'n 'm : Int) ('o : Int). (int('n), int('m), int('o)) -> unit + +function test forall 'n, 'n >= 0. (n: int('n)) -> unit = { + let _ = czeros(64); + multi_param(2 + 3, 5, n); + () +}
\ No newline at end of file diff --git a/test/typecheck/pass/constant_nexp/v1.expect b/test/typecheck/pass/constant_nexp/v1.expect new file mode 100644 index 00000000..71ed455b --- /dev/null +++ b/test/typecheck/pass/constant_nexp/v1.expect @@ -0,0 +1,7 @@ +Type error: +[[96mconstant_nexp/v1.sail[0m]:11:2-26 +11[96m |[0m multi_param(2 + 3, n, 5); + [91m |[0m [91m^----------------------^[0m + [91m |[0m Could not resolve quantifiers for multi_param + [91m |[0m [94m*[0m is_constant(('m : Int)) + [91m |[0m diff --git a/test/typecheck/pass/constant_nexp/v1.sail b/test/typecheck/pass/constant_nexp/v1.sail new file mode 100644 index 00000000..eca83a44 --- /dev/null +++ b/test/typecheck/pass/constant_nexp/v1.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val czeros = "zeros" : forall (constant 'n : Int), 'n >= 0. int('n) -> bits('n) + +val multi_param : forall (constant 'n 'm : Int) ('o : Int). (int('n), int('m), int('o)) -> unit + +function test forall 'n, 'n >= 0. (n: int('n)) -> unit = { + let _ = czeros(64); + multi_param(2 + 3, n, 5); + () +}
\ No newline at end of file diff --git a/test/typecheck/pass/constant_nexp/v2.expect b/test/typecheck/pass/constant_nexp/v2.expect new file mode 100644 index 00000000..3c4dcc16 --- /dev/null +++ b/test/typecheck/pass/constant_nexp/v2.expect @@ -0,0 +1,8 @@ +Type error: +[[96mconstant_nexp/v2.sail[0m]:12:10-38 +12[96m |[0m let _ = czeros(sizeof('n - 10) + 20); + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Could not resolve quantifiers for czeros + [91m |[0m [94m*[0m is_constant(('fv47#n : Int)) + [91m |[0m [94m*[0m (('n - 10) + 20) >= 0 + [91m |[0m diff --git a/test/typecheck/pass/constant_nexp/v2.sail b/test/typecheck/pass/constant_nexp/v2.sail new file mode 100644 index 00000000..b3799eed --- /dev/null +++ b/test/typecheck/pass/constant_nexp/v2.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +val czeros = "zeros" : forall (constant 'n : Int), 'n >= 0. int('n) -> bits('n) + +val multi_param : forall (constant 'n 'm : Int) ('o : Int). (int('n), int('m), int('o)) -> unit + +function test forall 'n, 'n >= 0. (n: int('n)) -> unit = { + let _ = czeros(64); + multi_param(2 + 3, 5, n); + let _ = czeros(sizeof('n - 10) + 20); + () +}
\ No newline at end of file |