summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorBrian Campbell2018-02-02 16:18:20 +0000
committerBrian Campbell2018-02-02 16:18:20 +0000
commit3ebce8457eb25f3ddceda77530c81580003296de (patch)
treece0d20db97111a144671d8367e06a9ac620b685e /lib
parentb0584ce1fea8c5df5e8e84269d9ec4bee5e5b90d (diff)
Add arithmetic shift right for aarch64 mono
Diffstat (limited to 'lib')
-rw-r--r--lib/mono_rewrites.sail3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 650fdf53..1af9b17f 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -16,6 +16,9 @@ val shiftright = "shiftr" : forall 'n ('ord : Order).
overload operator >> = {shiftright}
+val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
+ (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
function extzv(v) = extz_vec(sizeof('m),v)