From 19573d9ce8448f8296195fe1990a6d88593b57f1 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 7 Sep 2020 11:40:37 +0100
Subject: Fix typo a mono_rewrites definition - add tests for a couple of
 related rewrites - accept same range of constants for sign extension in the
 rewrite as for   the zero extension version (to make the test simpler)

---
 test/mono/pass/rewrites |  1 +
 test/mono/rewrites.sail | 26 ++++++++++++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 test/mono/pass/rewrites
 create mode 100644 test/mono/rewrites.sail

(limited to 'test')

diff --git a/test/mono/pass/rewrites b/test/mono/pass/rewrites
new file mode 100644
index 00000000..10272fed
--- /dev/null
+++ b/test/mono/pass/rewrites
@@ -0,0 +1 @@
+rewrites.sail -mono_rewrites
diff --git a/test/mono/rewrites.sail b/test/mono/rewrites.sail
new file mode 100644
index 00000000..b08af90f
--- /dev/null
+++ b/test/mono/rewrites.sail
@@ -0,0 +1,26 @@
+// Tests for -mono_rewrites
+
+default Order dec
+$include <prelude.sail>
+$include <mono_rewrites.sail>
+
+// The preconditions for this rewrite require a non-constant size somewhere, so
+// pull the example out into a separate function.
+val sign_ext_fun : forall 'z 'n, 'z >= 0 & 'n >= 4 + 'z. (bits(12), int('z), int('n)) -> bits('n)
+function sign_ext_fun(y, z, n) = {
+  sail_sign_extend(y[7..4] @ sail_zeros(z), n)
+}
+
+val run : unit -> unit effect {escape}
+
+function run() = {
+    let x : bits(12) = 0x123;
+    let y : bits(12) = 0x987;
+    let 'i = 7;
+    let 'j = 4;
+    let 'z = 8;
+    assert(sail_zero_extend(x[7..4] @ sail_zeros(8), 32) == 0x00000200);
+    assert(sign_ext_fun(x, z, 32) == 0x00000200);
+    assert(sail_zero_extend(y[7..4] @ sail_zeros(8), 32) == 0x00000800);
+    assert(sign_ext_fun(y, z, 32) == 0xfffff800);
+}
-- 
cgit v1.2.3