Skip to content

Commit

Permalink
Incorporate Yan's suggestions
Browse files Browse the repository at this point in the history
  • Loading branch information
shigoel committed Aug 19, 2024
1 parent 77c330c commit a72ae69
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 2 deletions.
4 changes: 4 additions & 0 deletions Arm/Insts/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,10 @@ as source operands does not violate the Apple ABI.
For details, see
https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms#Respect-the-purpose-of-specific-CPU-registers
Also see "Procedure Call Standard for the Arm 64-bit Architecture";
the latest version is available at
https://github.com/ARM-software/abi-aa/releases
-/
partial def GPRIndex.rand (lo := 0) (hi := 31) :
IO (BitVec 5) := do
Expand Down
4 changes: 2 additions & 2 deletions Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
Original file line number Diff line number Diff line change
Expand Up @@ -105,11 +105,11 @@ partial def Conversion_between_FP_and_Int_cls.fmov_general.rand : IO (Option (Bi
Rn := ← BitVec.rand 5,
Rd := ← (if (lsb opcode 0) = 1#1 then
-- FPConvOp.FPConvOp_MOV_ItoF
-- GPR used as a source operand.
-- Destination operand is a SIMD&FP register.
BitVec.rand 5
else
-- FPConvOp.FPConvOp_MOV_FtoI
-- GPR used as a destination operand.
-- Destination operand is a GPR register.
GPRIndex.rand) }
pure (inst.toBitVec32)

Expand Down

0 comments on commit a72ae69

Please sign in to comment.