From 41e6fe10e7d28193fa62711fcdad797b1f0103a0 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 13 May 2019 18:03:35 +0100
Subject: 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.
---
 test/typecheck/pass/constant_nexp.sail      | 13 +++++++++++++
 test/typecheck/pass/constant_nexp/v1.expect |  7 +++++++
 test/typecheck/pass/constant_nexp/v1.sail   | 13 +++++++++++++
 test/typecheck/pass/constant_nexp/v2.expect |  8 ++++++++
 test/typecheck/pass/constant_nexp/v2.sail   | 14 ++++++++++++++
 5 files changed, 55 insertions(+)
 create mode 100644 test/typecheck/pass/constant_nexp.sail
 create mode 100644 test/typecheck/pass/constant_nexp/v1.expect
 create mode 100644 test/typecheck/pass/constant_nexp/v1.sail
 create mode 100644 test/typecheck/pass/constant_nexp/v2.expect
 create mode 100644 test/typecheck/pass/constant_nexp/v2.sail

(limited to 'test/typecheck')

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:
+[constant_nexp/v1.sail]:11:2-26
+11 |  multi_param(2 + 3, n, 5);
+   |  ^----------------------^
+   | Could not resolve quantifiers for multi_param
+   | * is_constant(('m : Int))
+   | 
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:
+[constant_nexp/v2.sail]:12:10-38
+12 |  let _ = czeros(sizeof('n - 10) + 20);
+   |          ^--------------------------^
+   | Could not resolve quantifiers for czeros
+   | * is_constant(('fv47#n : Int))
+   | * (('n - 10) + 20) >= 0
+   | 
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
-- 
cgit v1.2.3