Skip to content

Commit

Permalink
Use GPRIndex.rand in some more places (leanprover#109)
Browse files Browse the repository at this point in the history
### Description:

Use `GPRIndex.rand` for a few instructions that I overlooked in leanprover#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.
  • Loading branch information
shigoel authored Aug 21, 2024
1 parent 14e22ea commit d7607dc
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions Arm/Insts/DPSFP/Advanced_simd_copy.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)

Expand All @@ -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)

Expand Down

0 comments on commit d7607dc

Please sign in to comment.