From 1f421b865a87a161a82550443a0cf39aa2642d9c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 15 Apr 2019 12:08:28 +0100
Subject: Basic loop termination measures for Coq Currently only supports pure
 termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
---
 test/coq/pass/while_MM_terminating.sail | 18 ++++++++++++++++++
 test/coq/pass/while_MP_terminating.sail | 13 +++++++++++++
 test/coq/pass/while_PM_terminating.sail | 15 +++++++++++++++
 test/coq/pass/while_PP_terminating.sail | 13 +++++++++++++
 test/coq/skip                           |  9 +++++++++
 5 files changed, 68 insertions(+)
 create mode 100644 test/coq/pass/while_MM_terminating.sail
 create mode 100644 test/coq/pass/while_MP_terminating.sail
 create mode 100644 test/coq/pass/while_PM_terminating.sail
 create mode 100644 test/coq/pass/while_PP_terminating.sail

(limited to 'test')

diff --git a/test/coq/pass/while_MM_terminating.sail b/test/coq/pass/while_MM_terminating.sail
new file mode 100644
index 00000000..e3bca7f5
--- /dev/null
+++ b/test/coq/pass/while_MM_terminating.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register COUNT : int
+
+register INT : bool
+
+function test () -> unit = {
+  COUNT = 0;
+  while not_bool(INT) do {
+    COUNT = COUNT + 1;
+    if COUNT > 5 then
+      INT = true
+  }
+}
+
+termination_measure test while (5 - COUNT)
diff --git a/test/coq/pass/while_MP_terminating.sail b/test/coq/pass/while_MP_terminating.sail
new file mode 100644
index 00000000..d9b71ad9
--- /dev/null
+++ b/test/coq/pass/while_MP_terminating.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+register INT : bool
+
+function test () -> int = {
+  count : int = 0;
+  while not_bool(INT) & count < 5 do count = count + 1;
+  return(count)
+}
+
+termination_measure test while 5 - count
diff --git a/test/coq/pass/while_PM_terminating.sail b/test/coq/pass/while_PM_terminating.sail
new file mode 100644
index 00000000..5129e997
--- /dev/null
+++ b/test/coq/pass/while_PM_terminating.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register GPR00 : int
+
+function test b : int -> unit = {
+  i : int = 0;
+  while i < 64 do {
+    GPR00 = b + i;
+    i = i + 1;
+  }
+}
+
+termination_measure test while 64 - i
diff --git a/test/coq/pass/while_PP_terminating.sail b/test/coq/pass/while_PP_terminating.sail
new file mode 100644
index 00000000..00a4450b
--- /dev/null
+++ b/test/coq/pass/while_PP_terminating.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+function test n : int -> int = {
+  i : int = 1;
+  j : int = 1;
+  while i < n do {
+    j = i * j;
+    i = i + 1
+  };
+  j
+}
diff --git a/test/coq/skip b/test/coq/skip
index 49744fce..a4be9719 100644
--- a/test/coq/skip
+++ b/test/coq/skip
@@ -42,3 +42,12 @@ reg_mod.sail
 reg_ref.sail
 XXXXX Dodgy division/modulo stuff
 Replicate.sail
+XXXXX Non-terminating loops - I've written terminating versions of these
+while_MM.sail
+while_MP.sail
+while_PM.sail
+while_PP.sail
+XXXXX Not yet - haven't decided whether to support register reads in measures
+while_MM_terminating.sail
+XXXXX Not yet - haven't arranged for lifting pure loops into the monad (or proving termination outright) yet
+while_PP_terminating.sail
-- 
cgit v1.2.3


From 4529e0acc377bed4d1bab4230f4023e4bee3ae85 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 15 Apr 2019 14:35:02 +0100
Subject: Fix: Allow zero-length vector literals

---
 test/c/zero_length_bv.expect            |  1 +
 test/c/zero_length_bv.sail              | 14 ++++++++++++++
 test/typecheck/pass/zero_length_bv.sail | 14 ++++++++++++++
 3 files changed, 29 insertions(+)
 create mode 100644 test/c/zero_length_bv.expect
 create mode 100644 test/c/zero_length_bv.sail
 create mode 100644 test/typecheck/pass/zero_length_bv.sail

(limited to 'test')

diff --git a/test/c/zero_length_bv.expect b/test/c/zero_length_bv.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/zero_length_bv.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/zero_length_bv.sail b/test/c/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/c/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let x: bits(0) = [];
+  if x == sail_zeros(0) then {
+    print_endline("ok")
+  };
+  let x: vector(0, dec, string) = [];
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/zero_length_bv.sail b/test/typecheck/pass/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/typecheck/pass/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let x: bits(0) = [];
+  if x == sail_zeros(0) then {
+    print_endline("ok")
+  };
+  let x: vector(0, dec, string) = [];
+  ()
+}
\ No newline at end of file
-- 
cgit v1.2.3