summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBrian Campbell2019-06-20 12:22:04 +0100
committerBrian Campbell2019-06-20 12:22:26 +0100
commit055d5b61c63b61270cf74c4e2b5af5f66c91e387 (patch)
tree881d7976df1591c8d7f5a98836b7376cfa760559
parent56ad3c612c662ecedb4ee83845ec15815ae264c2 (diff)
Tweak two aarch64_small definitions to help monomorphisation
-rw-r--r--aarch64_small/armV8.sail6
-rw-r--r--aarch64_small/armV8_A64_lib.sail2
2 files changed, 5 insertions, 3 deletions
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index d8ee0bbe..5754b159 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -2142,10 +2142,12 @@ function clause execute ( Reverse((d,n,datasize as int('R),op)) ) = {
assert (vsize > 0); /* FIXME: CP adding assertion to make typecheck */
foreach (base from 0 to (datasize - 1) by (2 * vsize)) { /* ARM: while base < datasize do */
assert (base+vsize*2 - 1 < datasize); /* FIXME: CP adding assertion to make typecheck */
- let a = tmp[(base+(2*vsize) - 1)..(base+vsize)];
+/* let a = tmp[(base+(2*vsize) - 1)..(base+vsize)];
result[((base+vsize) - 1)..base] = a;
let b = tmp[(base+vsize - 1)..base];
- result[(base+(2*vsize) - 1)..(base+vsize)] = b;
+ result[(base+(2*vsize) - 1)..(base+vsize)] = b;*/
+ result[((base+vsize) - 1)..base] = tmp[(base+(2*vsize) - 1)..(base+vsize)];
+ result[(base+(2*vsize) - 1)..(base+vsize)] = tmp[(base+vsize - 1)..base];
/* ARM: base = base + (2 * vsize); */
};
};
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index 8c684fc7..8b32e09f 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -799,7 +799,7 @@ function ExtendReg (N, _reg, etype, shift) = {
let len = uMin(len, length(_val) - shift);
assert( len >= 1 & 'S + len < 'N);
- let a = (_val[(len - 1)..0]);
+/* let a = (_val[(len - 1)..0]);*/
/* Zeros() */
Extend((_val[(len - 1)..0]) @ (Zeros() : bits('S)), _unsigned)
}