1 files changed, 43 insertions, 0 deletions
diff --git a/aarch64_small/mono-splices/DecodeBitMasks.sail b/aarch64_small/mono-splices/DecodeBitMasks.sail
new file mode 100644
index 00000000..fc1d63fa
--- /dev/null
+++ b/aarch64_small/mono-splices/DecodeBitMasks.sail
@@ -0,0 +1,43 @@
+val DecodeBitMasks2 : forall 'M 'S 'd, 'M >= 'd + 1 & 'S >= 0 & 'd >= 0. (int, int('S), nat, int('d), int('M)) -> (bits('M), bits('M)) effect {escape}
+
+function DecodeBitMasks2(esize as 'E, S, R, d, M) = {
+  assert(constraint('E in {2,4,8,16,32,64} & 'M >= 'E & 'E >= 'd + 1));
+  assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
+  welem : bits('E) = ZeroExtend(Ones(S + 1));
+  telem : bits('E) = ZeroExtend(Ones(d + 1));
+  wmask = Replicate(M,ROR(welem, R));
+  tmask = Replicate(M,telem);
+  (wmask, tmask);
+}
+
+function DecodeBitMasks(M : int('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
+  /* let M = (length((bit['M]) 0)) in { */
+  /* ARM: (bit['M]) tmask := 0; (* ARM: uninitialized *) */
+  /* ARM: (bit['M]) wmask := 0; (* ARM: uninitialized *) */
+  levels : bits(6) = Zeros(); /* ARM: uninitialized */
+
+  /* Compute log2 of element size */
+  /* 2^len must be in range [2, 'M] */
+  let len : range(0,6) = match HighestSetBit([immN]@(~(imms))) {
+    None() => { assert (false, "DecodeBitMasks: HighestSetBit returned None"); 0; },
+    Some(c) => c
+  };
+  if len < 1 then {ReservedValue(); exit()} else {
+  assert(M >= lsl(1, len));
+
+  /* Determine S, R and S - R parameters */
+  levels = ZeroExtend(Ones(len));
+
+  /* For logical immediates an all-ones value of S is reserved */
+  /* since it would generate a useless all-ones result (many times) */
+  if immediate & ((imms & levels) == levels) then
+    ReservedValue();
+
+  let S = UInt (imms & levels);
+  let R = UInt (immr & levels);
+  let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
+
+  let esize as int('E) = lsl(1, len);
+  let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
+  DecodeBitMasks2(esize, S, R, d, M);
+}}