Skip to content

Commit

Permalink
Adding MOV related instructions (#16)
Browse files Browse the repository at this point in the history 
### Description:

This PR adds supports for:
1. Advanced SIMD Modified Immediate instructions including `MOVI, MVNI,
ORR, BIC (Immediate, vector) and FMOV (vector, immediate,
single/double-precision)`
2. Advanced SIMD Scalar Copy instructions including `DUP (element,
scalar)`
3. Advanced SIMD Copy instructions including `DUP (element vector,
general), INS (element, general), SMOV (32-, 64-bit) and UMOV (32-,
64-bit)`
4. Refactors proofs involving `hi - lo + 1 = esize` and `esize > 0`.

### Testing:

The `make all` succeeds and conformance testing succeeds on both
Graviton2 and Graviton3 machines

### 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
@pennyannn
pennyannn authored Feb 22, 2024
1 parent 7b3bc81 commit 9fc7c4b
Show file tree
Hide file tree
Showing 10 changed files with 620 additions and 29 deletions.
42 changes: 42 additions & 0 deletions Arm/Decode.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,10 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst :=
DPSFP (Advanced_simd_copy {Q, op, imm5, imm4, Rn, Rd})
| [0, Q:1, 101110, op2:2, 0, Rm:5, 0, imm4:4, 0, Rn:5, Rd:5] =>
DPSFP (Advanced_simd_extract {Q, op2, Rm, imm4, Rn, Rd})
| [0, Q:1, op:1, 0111100000, a:1, b:1, c:1, cmode:4, o2:1, 1, d:1, e:1, f:1, g:1, h:1, Rd:5] =>
DPSFP (Advanced_simd_modified_immediate {Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd})
| [01, op:1, 11110000, imm5:5, 0, imm4:4, 1, Rn:5, Rd:5] =>
DPSFP (Advanced_simd_scalar_copy {op, imm5, imm4, Rn, Rd})
| [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:5, 1, Rn:5, Rd:5] =>
DPSFP (Advanced_simd_three_same {Q, U, size, Rm, opcode, Rn, Rd})
| [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:4, 00, Rn:5, Rd:5] =>
Expand Down Expand Up @@ -399,6 +403,44 @@ example : decode_raw_inst 0xcb0fdf69 =
Rd := 0x09#5 })) := by
rfl

-- orr v5.8h, #0x77, lsl #8
example : decode_raw_inst 0x4f03b6e5 =
(ArmInst.DPSFP
(DataProcSFPInst.Advanced_simd_modified_immediate
{ _fixed1 := 0x0#1,
Q := 0x1#1,
op := 0x0#1,
_fixed2 := 0x1e0#10,
a := 0x0#1,
b := 0x1#1,
c := 0x1#1,
cmode := 0xb#4,
o2 := 0x0#1,
_fixed3 := 0x1#1,
d := 0x1#1,
e := 0x0#1,
f := 0x1#1,
g := 0x1#1,
h := 0x1#1,
Rd := 0x05#5 })) := by
rfl

-- mov v10.h[0] v17.h[6]
example : decode_raw_inst 0x6e026e2a =
(ArmInst.DPSFP
(DataProcSFPInst.Advanced_simd_copy
{ _fixed1 := 0x0#1,
Q := 0x1#1,
op := 0x1#1,
_fixed2 := 0x70#8,
imm5 := 0x02#5,
_fixed3 := 0x0#1,
imm4 := 0xd#4,
_fixed4 := 0x1#1,
Rn := 0x11#5,
Rd := 0x0a#5 })) := by
rfl

-- Unimplemented
example : decode_raw_inst 0x00000000#32 = none := by rfl

Expand Down
68 changes: 58 additions & 10 deletions Arm/Decode/DPSFP.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,20 +88,40 @@ def Advanced_simd_two_reg_misc_cls.toBitVec32 (x : Advanced_simd_two_reg_misc_cl
x._fixed1 ++ x.Q ++ x.U ++ x._fixed2 ++ x.size ++ x._fixed3 ++ x.opcode ++ x._fixed4 ++ x.Rn ++ x.Rd

structure Advanced_simd_copy_cls where
_fixed1 : BitVec 1 := 0b0#1 -- [31:31]
Q : BitVec 1 -- [30:30]
op : BitVec 1 -- [29:29]
_fixed2 : BitVec 7 := 01110000#7 -- [28:21]
imm5 : BitVec 5 -- [20:16]
_fixed3 : BitVec 1 := 0b0#1 -- [15:15]
imm4 : BitVec 4 -- [14:11]
_fixed4 : BitVec 1 := 0b1#1 -- [10:10]
Rn : BitVec 5 -- [9:5]
Rd : BitVec 5 -- [4:0]
_fixed1 : BitVec 1 := 0b0#1 -- [31:31]
Q : BitVec 1 -- [30:30]
op : BitVec 1 -- [29:29]
_fixed2 : BitVec 8 := 0b01110000#8 -- [28:21]
imm5 : BitVec 5 -- [20:16]
_fixed3 : BitVec 1 := 0b0#1 -- [15:15]
imm4 : BitVec 4 -- [14:11]
_fixed4 : BitVec 1 := 0b1#1 -- [10:10]
Rn : BitVec 5 -- [9:5]
Rd : BitVec 5 -- [4:0]
deriving DecidableEq, Repr

instance : ToString Advanced_simd_copy_cls where toString a := toString (repr a)

def Advanced_simd_copy_cls.toBitVec32 (x : Advanced_simd_copy_cls) : BitVec 32 :=
x._fixed1 ++ x.Q ++ x.op ++ x._fixed2 ++ x.imm5 ++ x._fixed3 ++ x.imm4 ++ x._fixed4 ++ x.Rn ++ x.Rd

structure Advanced_simd_scalar_copy_cls where
_fixed1 : BitVec 2 := 0b01#2 -- [31:30]
op : BitVec 1 -- [29:29]
_fixed2 : BitVec 8 := 0b11110000#8 -- [28:21]
imm5 : BitVec 5 -- [20:16]
_fixed3 : BitVec 1 := 0b0#1 -- [15:15]
imm4 : BitVec 4 -- [14:11]
_fixed4 : BitVec 1 := 0b1#1 -- [10:10]
Rn : BitVec 5 -- [9:5]
Rd : BitVec 5 -- [4:0]
deriving DecidableEq, Repr

instance : ToString Advanced_simd_scalar_copy_cls where toString a := toString (repr a)

def Advanced_simd_scalar_copy_cls.toBitVec32 (x : Advanced_simd_scalar_copy_cls) : BitVec 32 :=
x._fixed1 ++ x.op ++ x._fixed2 ++ x.imm5 ++ x._fixed3 ++ x.imm4 ++ x._fixed4 ++ x.Rn ++ x.Rd

structure Advanced_simd_extract_cls where
_fixed1 : BitVec 1 := 0b0#1 -- [31:31]
Q : BitVec 1 -- [30:30]
Expand All @@ -121,6 +141,30 @@ instance : ToString Advanced_simd_extract_cls where toString a := toString (repr
def Advanced_simd_extract_cls.toBitVec32 (x : Advanced_simd_extract_cls) : BitVec 32 :=
x._fixed1 ++ x.Q ++ x._fixed2 ++ x.op2 ++ x._fixed3 ++ x.Rm ++ x._fixed4 ++ x.imm4 ++ x._fixed5 ++ x.Rn ++ x.Rd

structure Advanced_simd_modified_immediate_cls where
_fixed1 : BitVec 1 := 0b0#1 -- [31:31]
Q : BitVec 1 -- [30:30]
op : BitVec 1 -- [29:29]
_fixed2 : BitVec 10 := 0b0111100000#10 -- [28:19]
a : BitVec 1 -- [18:18]
b : BitVec 1 -- [17:17]
c : BitVec 1 -- [16:16]
cmode : BitVec 4 -- [15:12]
o2 : BitVec 1 -- [11:11]
_fixed3 : BitVec 1 := 0b1#1 -- [10:10]
d : BitVec 1 -- [9:9]
e : BitVec 1 -- [8:8]
f : BitVec 1 -- [7:7]
g : BitVec 1 -- [6:6]
h : BitVec 1 -- [5:5]
Rd : BitVec 5 -- [4:0]
deriving DecidableEq, Repr

instance : ToString Advanced_simd_modified_immediate_cls where toString a := toString (repr a)

def Advanced_simd_modified_immediate_cls.toBitVec32 (x : Advanced_simd_modified_immediate_cls) : BitVec 32 :=
x._fixed1 ++ x.Q ++ x.op ++ x._fixed2 ++ x.a ++ x.b ++ x.c ++ x.cmode ++ x.o2 ++ x._fixed3 ++ x.d ++ x.e ++ x.f ++ x.g ++ x.h ++ x.Rd

structure Advanced_simd_three_same_cls where
_fixed1 : BitVec 1 := 0b0#1 -- [31:31]
Q : BitVec 1 -- [30:30]
Expand Down Expand Up @@ -174,6 +218,10 @@ inductive DataProcSFPInst where
Advanced_simd_copy_cls → DataProcSFPInst
| Advanced_simd_extract :
Advanced_simd_extract_cls → DataProcSFPInst
| Advanced_simd_modified_immediate :
Advanced_simd_modified_immediate_cls → DataProcSFPInst
| Advanced_simd_scalar_copy :
Advanced_simd_scalar_copy_cls → DataProcSFPInst
| Advanced_simd_three_same :
Advanced_simd_three_same_cls → DataProcSFPInst
| Advanced_simd_three_different :
Expand Down
6 changes: 6 additions & 0 deletions Arm/Exec.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
| DPR (DataProcRegInst.Logical_shifted_reg i) =>
DPR.exec_logical_shifted_reg i s

| DPSFP (DataProcSFPInst.Advanced_simd_copy i) =>
DPSFP.exec_advanced_simd_copy i s
| DPSFP (DataProcSFPInst.Crypto_two_reg_sha512 i) =>
DPSFP.exec_crypto_two_reg_sha512 i s
| DPSFP (DataProcSFPInst.Crypto_three_reg_sha512 i) =>
Expand All @@ -46,6 +48,10 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
DPSFP.exec_advanced_simd_two_reg_misc i s
| DPSFP (DataProcSFPInst.Advanced_simd_extract i) =>
DPSFP.exec_advanced_simd_extract i s
| DPSFP (DataProcSFPInst.Advanced_simd_modified_immediate i) =>
DPSFP.exec_advanced_simd_modified_immediate i s
| DPSFP (DataProcSFPInst.Advanced_simd_scalar_copy i) =>
DPSFP.exec_advanced_simd_scalar_copy i s
| DPSFP (DataProcSFPInst.Advanced_simd_three_same i) =>
DPSFP.exec_advanced_simd_three_same i s
| DPSFP (DataProcSFPInst.Advanced_simd_three_different i) =>
Expand Down
19 changes: 19 additions & 0 deletions Arm/Insts/Common.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,14 @@ def highest_set_bit (bv : BitVec n) : Option Nat := Id.run do
break
return acc

def lowest_set_bit (bv : BitVec n) : Nat := Id.run do
let mut acc := n
for i in List.range n do
if extractLsb i i bv == 1
then acc := i
break
return acc

def invalid_bit_masks (immN : BitVec 1) (imms : BitVec 6) (immediate : Bool)
(M : Nat) : Bool :=
let len := highest_set_bit $ immN ++ ~~~imms
Expand Down Expand Up @@ -214,4 +222,15 @@ def ldst_write (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (val : BitVec width
: ArmState :=
if SIMD? then write_sfp width idx val s else write_gpr width idx val s

----------------------------------------------------------------------

theorem hi_lo_diff_equal_esize (esize : Nat) (lo : Nat) (hi : Nat)
(h₀ : esize > 0) (h₁ : hi = lo + esize - 1):
hi - lo + 1 = esize := by omega

theorem esize_gt_zero (size : Nat):
8 <<< size > 0 := by
simp_all only [ Nat.shiftLeft_eq, gt_iff_lt, Nat.zero_lt_succ
, mul_pos_iff_of_pos_left, zero_lt_two, pow_pos]

end Common
Loading

0 comments on commit 9fc7c4b

Please sign in to comment.