From 061c7da3c0629d5fc6cc4a9a91bf4b251b61863d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 18 Jun 2019 16:57:44 +0100
Subject: Monomorphisation improvements for aarch64_small - additional rewrites
 (signed extend of subrange@zeros, subrange assignment,   variants with casts)
 - drop # from new top-level type variables (e.g., n_times_8) so that the  
 rewriter knows that they're safe to include in casts - add casts in
 else-branches when only one possible value for a size is left - add casts
 when assertions force a size to be a particular value - don't use types to
 detect set constraints in analysis because we won't   know which part of the
 assertion should be replaced - also use non-top-level type variables when
 simplifying sizes in analysis   (useful when it can from pattern matching on
 an ast) - cope with repeated int('n) in a pattern match (!)

---
 test/mono/castreq.sail     | 17 ++++++++++++++++-
 test/mono/pass/repeatedint |  1 +
 test/mono/repeatedint.sail | 22 ++++++++++++++++++++++
 3 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 test/mono/pass/repeatedint
 create mode 100644 test/mono/repeatedint.sail

(limited to 'test')

diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index bb1bc952..e8fbabb0 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -33,6 +33,14 @@ function foo(n, x) =
     64 => let z = y@y@y@y in let dfsf = 4 in z
   }
 
+val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
+
+function foo_if(n, x) =
+  let y : bits(16) = extzv(x) in
+  if n == 32
+  then y@y
+  else /* 64 */ let z = y@y@y@y in let dfsf = 4 in z
+
 val use : bits(16) -> unit effect pure
 
 function use(x) = ()
@@ -45,6 +53,13 @@ function bar(x) =
    16 => use(x)
   }
 
+val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure
+
+function bar_if(x) =
+  if 'n == 8
+  then use(x@x)
+  else /* 16 */ use(x)
+
 val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef}
 
 function ret(n, x) =
@@ -116,4 +131,4 @@ function run () = {
     assert(foo2(64,0x12) == 0x0012001200120012);
     assert(foo3(4,0x12) == 0x00120012);
     assert(foo3(8,0x12) == 0x0012001200120012);
-}
\ No newline at end of file
+}
diff --git a/test/mono/pass/repeatedint b/test/mono/pass/repeatedint
new file mode 100644
index 00000000..ff26c84d
--- /dev/null
+++ b/test/mono/pass/repeatedint
@@ -0,0 +1 @@
+repeatedint.sail -auto_mono
diff --git a/test/mono/repeatedint.sail b/test/mono/repeatedint.sail
new file mode 100644
index 00000000..2d01e814
--- /dev/null
+++ b/test/mono/repeatedint.sail
@@ -0,0 +1,22 @@
+/* Silly, but it did appear in a model, and we didn't handle it... */
+
+default Order dec
+$include <prelude.sail>
+
+union ast = {
+  SomeInstr : {'size, 'size in {8,16}. (int('size), int('size))}
+}
+
+val test : ast -> bits(32)
+
+function test(SomeInstr(s as int('size),r)) = {
+  x : bits('size) = sail_zero_extend(0x80, s);
+  sail_sign_extend(x,32)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test(SomeInstr(8,8)) == 0xffffff80);
+  assert(test(SomeInstr(16,16)) == 0x00000080);
+}
-- 
cgit v1.2.3