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)

---
 lib/mono_rewrites.sail  |  2 +-
 src/monomorphise.ml     |  7 ++++++-
 test/mono/pass/rewrites |  1 +
 test/mono/rewrites.sail | 26 ++++++++++++++++++++++++++
 4 files changed, 34 insertions(+), 2 deletions(-)
 create mode 100644 test/mono/pass/rewrites
 create mode 100644 test/mono/rewrites.sail

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 3efc028a..b24bb152 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -165,7 +165,7 @@ val place_subrange_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
 function place_subrange_signed(m,xs,i,j,shift) = {
-  place_slice_signed(m, xs, i, i-j+1, shift)
+  place_slice_signed(m, xs, j, i-j+1, shift)
 }
 
 /* This has different names in the aarch64 prelude (UInt) and the other
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index f4d0aa56..9bb47774 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -2910,6 +2910,11 @@ let rec rewrite_app env typ (id,args) =
     is_id env (Id "zero_extend") id || is_id env (Id "sail_zero_extend") id ||
     is_id env (Id "mips_zero_extend") id || is_id env (Id "EXTZ") id
   in
+  let is_sign_extend =
+    is_id env (Id "SignExtend") id ||
+    is_id env (Id "sign_extend") id || is_id env (Id "sail_sign_extend") id ||
+    is_id env (Id "mips_sign_extend") id || is_id env (Id "EXTS") id
+  in
   let is_truncate = is_id env (Id "truncate") id in
   let mk_exp e = E_aux (e, (Unknown, empty_tannot)) in
   let rec is_zeros_exp e = match unaux_exp e with
@@ -3244,7 +3249,7 @@ let rec rewrite_app env typ (id,args) =
 
     | _ -> E_app (id,args)
 
-  else if is_id env (Id "SignExtend") id || is_id env (Id "sign_extend") id then
+  else if is_sign_extend then
     let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in
     match List.filter (fun arg -> not (is_number (typ_of arg))) args with
     | [E_aux (E_app (slice1, [vector1; start1; length1]),_)]
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