Move Lem shl_int, shr_int implementations from aarch64_extras to sail lib

(note that they're already declared in lib/arith.sail)

3 files changed, 17 insertions, 6 deletions

diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index 58f1b9c7..c9ea84e2 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -60,12 +60,6 @@ let exts_slice v i j = ext_slice true v i j
 val extz_slice : list bitU -> integer -> integer -> list bitU
 let extz_slice v i j = ext_slice false v i j*)
 
-val shr_int : ii -> ii -> ii
-let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
-
-val shl_int : integer -> integer -> integer
-let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
-
 let hexchar_to_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
   else if c = #'1' then Just ([false;false;false;true ])
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index a89456b9..cb2c3379 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -45,6 +45,12 @@ let negate_real r = realNegate r
 let abs_real r = realAbs r
 let power_real b e = realPowInteger b e*)
 
+val shr_int : ii -> ii -> ii
+let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
+
+val shl_int : integer -> integer -> integer
+let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+
 let inline or_bool l r = (l || r)
 let inline and_bool l r = (l && r)
 let inline xor_bool l r = xor l r
diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index 7fb2b822..99447d42 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -1,4 +1,5 @@
 $include <smt.sail>
+$include <arith.sail>
 $include <flow.sail>
 $include <vector_dec.sail>
 
@@ -23,6 +24,13 @@ function launder(x) = {
   x
 }
 
+/* A function that constant propagation won't touch */
+val launder_int : int -> int effect {escape}
+function launder_int(x) = {
+  assert(true);
+  x
+}
+
 val test : bool -> unit effect {escape}
 
 function test(b) = {
@@ -30,10 +38,13 @@ function test(b) = {
     let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
     let x' : bits('n) = launder(x);
     let y : bits('n) = match 'n { 8 => 0x35, 16 => 0x5637 };
+    let z : bits(8) = slice(x,5,3) @ slice(x,0,5);
+    assert(slice(x,0,8) == z, "slice, concat, == by propagation");
     assert(x != y, "!= by propagation");
     assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice");
     assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice");
     assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal");
+    assert(shl_int(5,2) == shl_int(launder_int(5),2), "shl_int");
 }
 
 val run : unit -> unit effect {escape}