Merge

8 files changed, 149 insertions, 0 deletions

diff --git a/test/typecheck/fail/set_spsr1.sail b/test/typecheck/fail/set_spsr1.sail
new file mode 100644
index 00000000..27c343b2
--- /dev/null
+++ b/test/typecheck/fail/set_spsr1.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[30..0] := r
+}
diff --git a/test/typecheck/fail/set_spsr2.sail b/test/typecheck/fail/set_spsr2.sail
new file mode 100644
index 00000000..00493444
--- /dev/null
+++ b/test/typecheck/fail/set_spsr2.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[0..31] := r
+}
diff --git a/test/typecheck/fail/set_spsr3.sail b/test/typecheck/fail/set_spsr3.sail
new file mode 100644
index 00000000..c3a6208e
--- /dev/null
+++ b/test/typecheck/fail/set_spsr3.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[32..1] := r
+}
diff --git a/test/typecheck/fail/set_spsr4.sail b/test/typecheck/fail/set_spsr4.sail
new file mode 100644
index 00000000..65596b59
--- /dev/null
+++ b/test/typecheck/fail/set_spsr4.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[31] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[31..0] := r
+}
diff --git a/test/typecheck/fail/set_spsr5.sail b/test/typecheck/fail/set_spsr5.sail
new file mode 100644
index 00000000..d8a6588c
--- /dev/null
+++ b/test/typecheck/fail/set_spsr5.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[16]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[31..0] := r
+}
diff --git a/test/typecheck/pass/set_spsr.sail b/test/typecheck/pass/set_spsr.sail
new file mode 100644
index 00000000..b30343a2
--- /dev/null
+++ b/test/typecheck/pass/set_spsr.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[31..0] := r
+}
diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail
new file mode 100644
index 00000000..41479888
--- /dev/null
+++ b/test/typecheck/pass/simple_scattered.sail
@@ -0,0 +1,20 @@
+
+default Order dec
+
+scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize.
+
+val forall Num 'datasize, Num 'destsize, Num 'regsize.
+  ast<'datasize,'destsize,'regsize> -> unit effect pure execute
+
+scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute
+
+union ast member (bit[8], bit['regsize]) test
+
+function clause execute (test (x, y)) =
+{
+  return ()
+}
+
+end ast
+
+end execute
diff --git a/test/typecheck/pass/simple_scattered2.sail b/test/typecheck/pass/simple_scattered2.sail
new file mode 100644
index 00000000..8cd26e95
--- /dev/null
+++ b/test/typecheck/pass/simple_scattered2.sail
@@ -0,0 +1,27 @@
+
+default Order dec
+
+scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize.
+
+val forall Num 'datasize, Num 'destsize, Num 'regsize.
+  ast<'datasize,'destsize,'regsize> -> unit effect pure execute
+
+scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute
+
+union ast member (bit[8], bit['regsize]) test
+
+function clause execute (test (x, y)) =
+{
+  return ()
+}
+
+union ast member int test2
+
+function clause execute (test2(x)) =
+{
+  return ()
+}
+
+end ast
+
+end execute