From 2e271d91c58a2d4db4adbb4c47d34bcbe1a6992e Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 23 Nov 2018 22:05:24 +0000
Subject: Introduce intermediate bitvector representation in C

Bitvectors that aren't fixed size, but can still be shown to fit
within 64-bits, now have a specialised representation. Still need to
introduce more optimized functions, as right now we mostly have to
convert them into large bitvectors to pass them into most
functions. Nevertheless, this doubles the performance of the TLBLookup
function in ARMv8.
---
 test/c/run_tests.py       |  1 +
 test/c/small_slice.expect |  2 ++
 test/c/small_slice.sail   | 16 ++++++++++++++++
 3 files changed, 19 insertions(+)
 create mode 100644 test/c/small_slice.expect
 create mode 100644 test/c/small_slice.sail

(limited to 'test/c')

diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 6cd75981..268763ad 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -63,6 +63,7 @@ xml = '<testsuites>\n'
 xml += test_c('unoptimized C', '', '', True)
 xml += test_c('optimized C', '-O2', '-O', True)
 xml += test_c('constant folding', '', '-Oconstant_fold', True)
+xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True)
 xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False)
 
 xml += test_interpreter('interpreter')
diff --git a/test/c/small_slice.expect b/test/c/small_slice.expect
new file mode 100644
index 00000000..64d39581
--- /dev/null
+++ b/test/c/small_slice.expect
@@ -0,0 +1,2 @@
+v1 = 0x1234
+v2 = 0x34
diff --git a/test/c/small_slice.sail b/test/c/small_slice.sail
new file mode 100644
index 00000000..80878a80
--- /dev/null
+++ b/test/c/small_slice.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+function get_16((): unit) -> range(0, 16) = 16
+function get_8((): unit) -> range(0, 16) = 8
+
+function main((): unit) -> unit = {
+  let x = get_16();
+  let y = get_8();
+  let addr = 0x1234_ABCD;
+  let v1 = slice(addr, 16, x);
+  let v2 = slice(addr, 16, y);
+  print_bits("v1 = ", v1);
+  print_bits("v2 = ", v2);
+}
\ No newline at end of file
-- 
cgit v1.2.3