A wide move: imm16 at bit 5, the halfword selector at bits 21-22.
645def aarch64WideWord =
646 (lambda unrestricted base3 : Nat .
647 (lambda unrestricted destination : (family AArch64Register) .
648 (lambda unrestricted value : Nat .
649 (lambda unrestricted shift : (family AArch64HalfwordShift) .
650 (aarch64EncodeBounded
651 value
652 aarch64Immediate16Limit
653 (aarch64ByteWord
654 (naturalAdd (aarch64LowFive destination) (aarch64FromBitFiveByte0 value))
655 (aarch64FromBitFiveByte1 value)
656 (naturalAdd
657 (naturalAdd 128 (aarch64FromBitFiveByte2 value))
658 (naturalMultiply (aarch64HalfwordShiftCode shift) aarch64ThirtyTwo))
659 base3))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.