Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding MOV related instructions #16

Merged
merged 5 commits into from
Feb 22, 2024
Merged

Adding MOV related instructions #16

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d091e5a
Add Advanced_simd_modified_immediate (MOVI) instruction
pennyannn Feb 14, 2024
3bf520e
Add advanced simd scalar copy (DUP element scalar class)
pennyannn Feb 16, 2024
a3ada79
Add advanced simd copy
pennyannn Feb 16, 2024
f39fe84
Merge branch 'main' into yppe/mov
shigoel Feb 22, 2024
1225eac
Prove away a 'sorry'
shigoel Feb 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions Arm/Decode.lean
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading