From 1ac7d1b3ddb0cc1aeff4964559dbf92e0addf057 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 5 Jan 2021 14:36:21 +0000
Subject: Fix some cases when monomorphising vectors containing variable-length
 bitvectors

---
 test/c/run_tests.py |  2 +-
 test/c/split.expect |  1 +
 test/c/split.sail   | 30 ++++++++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 test/c/split.expect
 create mode 100644 test/c/split.sail

(limited to 'test')

diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 28a4d28d..a88de411 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -115,7 +115,7 @@ def test_lem(name):
 
 xml = '<testsuites>\n'
 
-xml += test_c2('unoptimized C', '', '', True)
+#xml += test_c2('unoptimized C', '', '', True)
 xml += test_c('unoptimized C', '', '', True)
 xml += test_c('optimized C', '-O2', '-O', True)
 xml += test_c('constant folding', '', '-Oconstant_fold', True)
diff --git a/test/c/split.expect b/test/c/split.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/split.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/split.sail b/test/c/split.sail
new file mode 100644
index 00000000..8c994e80
--- /dev/null
+++ b/test/c/split.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+$include <generic_equality.sail>
+$include <string.sail>
+
+val split : forall 'n 'm, 'n * 'm == 64 & 'n in {1, 2, 4, 8}. (int('n), int('m), bits(64)) -> vector('n, dec, bits('m)) effect {undef}
+
+function split(n, m, bv) = {
+    var result: vector('n, dec, bits('m)) = undefined;
+
+    foreach (i from 0 to (n - 1)) {
+        result[i] = sail_shiftright(bv, i * m)[m - 1 .. 0]
+    };
+
+    result
+}
+
+val main : unit -> unit effect {escape, undef}
+
+function main() = {
+    assert(split(8,  8, 0xAAAABBBBCCCCDDDD) == [0xAA, 0xAA, 0xBB, 0xBB, 0xCC, 0xCC, 0xDD, 0xDD]);
+    assert(split(4, 16, 0xAAAABBBBCCCCDDDD) == [0xAAAA, 0xBBBB, 0xCCCC, 0xDDDD]);
+    assert(split(2, 32, 0xAAAABBBBCCCCDDDD) == [0xAAAABBBB, 0xCCCCDDDD]);
+    assert(split(1, 64, 0xAAAABBBBCCCCDDDD) == [0xAAAABBBBCCCCDDDD]);
+
+    assert(split(4, 16, 0xAAAABBBBCCCCDDDD) != [0xDDDD, 0xCCCC, 0xBBBB, 0xAAAA]);
+
+    print_endline("ok");
+}
-- 
cgit v1.2.3