From d7607dc7fd16aaada9d4e173e1d87b0e1afd1d25 Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Wed, 21 Aug 2024 13:48:03 -0700 Subject: [PATCH] Use GPRIndex.rand in some more places (#109) ### Description: Use `GPRIndex.rand` for a few instructions that I overlooked in #103 ### Testing: `make all` succeeds on my M3. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --- Arm/Insts/DPSFP/Advanced_simd_copy.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean index be8f3cdb..407b83ef 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean @@ -167,7 +167,8 @@ partial def Advanced_simd_copy_cls.dup_general.rand : IO (Option (BitVec 32)) := op := 0b0#1, imm5 := imm5, imm4 := 0b0001#4, - Rn := ← BitVec.rand 5, + -- GPR Rn is a source operand for this instruction. + Rn := ← GPRIndex.rand, Rd := ← BitVec.rand 5 } pure (inst.toBitVec32) @@ -199,7 +200,8 @@ partial def Advanced_simd_copy_cls.ins_general.rand : IO (Option (BitVec 32)) := op := 0b0#1, imm5 := imm5, imm4 := 0b0011#4, - Rn := ← BitVec.rand 5, + -- GPR Rn is a source operand for this instruction. + Rn := ← GPRIndex.rand, Rd := ← BitVec.rand 5 } pure (inst.toBitVec32) @@ -219,7 +221,8 @@ partial def Advanced_simd_copy_cls.smov.rand : IO (Option (BitVec 32)) := do imm5 := imm5, imm4 := 0b0101#4, Rn := ← BitVec.rand 5, - Rd := ← BitVec.rand 5 + -- GPR Rd is the destination operand for this instruction. + Rd := ← GPRIndex.rand } pure (inst.toBitVec32) @@ -238,7 +241,8 @@ partial def Advanced_simd_copy_cls.umov.rand : IO (Option (BitVec 32)) := do imm5 := imm5, imm4 := 0b0111#4, Rn := ← BitVec.rand 5, - Rd := ← BitVec.rand 5 + -- GPR Rd is the destination operand for this instruction. + Rd := ← GPRIndex.rand } pure (inst.toBitVec32)