From 28dc04bd39e8a1573c322cd83d530295d8303206 Mon Sep 17 00:00:00 2001 From: Yan Peng <112029182+pennyannn@users.noreply.github.com> Date: Mon, 18 Mar 2024 14:46:39 -0700 Subject: [PATCH] Add shift related instructions (#25) ### Description: 1. Added [advanced SIMD scalar shift by immediate](https://developer.arm.com/documentation/ddi0602/2023-12/Index-by-Encoding/Data-Processing----Scalar-Floating-Point-and-Advanced-SIMD?lang=en) instructions: SHL, SSHR and USHR, SSRA and USRA, SRSHR and URSHR, SRSRA and URSRA) 2. Added [advanced SIMD (vector) shift by immediate ](https://developer.arm.com/documentation/ddi0602/2023-12/Index-by-Encoding/Data-Processing----Scalar-Floating-Point-and-Advanced-SIMD?lang=en) instructions: SHL, SSHR and USHR, SSRA and USRA, SRSHR and URSHR, SRSRA and URSRA) 3. Added [data processing two source](https://developer.arm.com/documentation/ddi0602/2023-12/Index-by-Encoding/Data-Processing----Register?lang=en) class for variable shifts (LSLV, LSRV, ARSV, RORV 32-, 64-bit) ### Testing: The `make all` succeeds and conformance testing runs successfully on Graviton2 and Graviton3. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --- Arm/BitVec.lean | 2 +- Arm/Decode.lean | 9 ++ Arm/Decode/DPR.lean | 52 ++++--- Arm/Decode/DPSFP.lean | 41 ++++++ Arm/Exec.lean | 10 ++ Arm/Insts/Common.lean | 77 ++++++++++ Arm/Insts/DPR/Data_processing_two_source.lean | 64 +++++++++ Arm/Insts/DPR/Insts.lean | 4 +- ...vanced_simd_scalar_shift_by_immediate.lean | 121 ++++++++++++++++ .../Advanced_simd_shift_by_immediate.lean | 132 ++++++++++++++++++ Arm/Insts/DPSFP/Insts.lean | 4 + 11 files changed, 498 insertions(+), 18 deletions(-) create mode 100644 Arm/Insts/DPR/Data_processing_two_source.lean create mode 100644 Arm/Insts/DPSFP/Advanced_simd_scalar_shift_by_immediate.lean create mode 100644 Arm/Insts/DPSFP/Advanced_simd_shift_by_immediate.lean diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean index b1a197d7..84ad9ec3 100644 --- a/Arm/BitVec.lean +++ b/Arm/BitVec.lean @@ -512,7 +512,7 @@ macro_rules | _ => $rhsElse:term) => do let mut result := rhsElse let x ← `(discr) - for p in ps, rhs in rhss do + for p in ps.reverse, rhs in rhss.reverse do let test ← genBVPatMatchTest x p let rhs ← declBVPatVars x p rhs result ← `(if $test then $rhs else $result) diff --git a/Arm/Decode.lean b/Arm/Decode.lean index 76534c8d..0e63bc02 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -78,6 +78,8 @@ def decode_data_proc_reg (i : BitVec 32) : Option ArmInst := DPR (Conditional_select {sf, op, S, Rm, cond, op2, Rn, Rd}) | [sf:1, 1, S:1, 11010110, opcode2:5, opcode:6, Rn:5, Rd:5] => DPR (Data_processing_one_source {sf, S, opcode2, opcode, Rn, Rd}) + | [sf:1, 0, S:1, 11010110, Rm:5, opcode:6, Rn:5, Rd:5] => + DPR (Data_processing_two_source {sf, S, Rm, opcode, Rn, Rd}) | [sf:1, opc:2, 01010, shift:2, N:1, Rm:5, imm6:6, Rn:5, Rd:5] => DPR (Logical_shifted_reg {sf, opc, shift, N, Rm, imm6, Rn, Rd}) | _ => none @@ -104,6 +106,13 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst := DPSFP (Advanced_simd_permute {Q, size, Rm, opcode, 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}) + -- Note: Advanced SIMD shift by immediate constraint immh != 0000 + -- An instruction will be matched against `Advanced_simd_modified_immediate` first, + -- if it doesn't match, then we know immh can't be 0b0000#4 + | [0, Q:1, U:1, 011110, immh:4, immb:3, opcode:5, 1, Rn:5, Rd:5] => + DPSFP (Advanced_simd_shift_by_immediate {Q, U, immh, immb, opcode, Rn, Rd}) + | [01, U:1, 111110, immh:4, immb:3, opcode:5, 1, Rn:5, Rd:5] => + DPSFP (Advanced_simd_scalar_shift_by_immediate {U, immh, immb, opcode, Rn, 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, 001110, op2:2, 0, Rm:5, 0, len:2, op:1, 00, Rn:5, Rd:5] => diff --git a/Arm/Decode/DPR.lean b/Arm/Decode/DPR.lean index 7a7b8cf4..d1b1e95b 100644 --- a/Arm/Decode/DPR.lean +++ b/Arm/Decode/DPR.lean @@ -64,6 +64,40 @@ instance : ToString Conditional_select_cls where toString a := toString (repr a) def Conditional_select_cls.toBitVec32 (x : Conditional_select_cls) : BitVec 32 := x.sf ++ x.op ++ x.S ++ x._fixed ++ x.Rm ++ x.cond ++ x.op2 ++ x.Rn ++ x.Rd +structure Data_processing_one_source_cls where + sf : BitVec 1 -- [31:31] + _fixed1 : BitVec 1 := 0b1#1 -- [30:30] + S : BitVec 1 -- [29:29] + _fixed2 : BitVec 8 := 0b11010110#8 -- [28:21] + opcode2 : BitVec 5 -- [20:16] + opcode : BitVec 6 -- [15:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Data_processing_one_source_cls where toString a := toString (repr a) + +def Data_processing_one_source_cls.toBitVec32 + (x : Data_processing_one_source_cls) : BitVec 32 := + x.sf ++ x._fixed1 ++ x.S ++ x._fixed2 ++ x.opcode2 ++ x.opcode ++ x.Rn ++ x.Rd + +structure Data_processing_two_source_cls where + sf : BitVec 1 -- [31:31] + _fixed1 : BitVec 1 := 0b0#1 -- [30:30] + S : BitVec 1 -- [29:29] + _fixed2 : BitVec 8 := 0b11010110#8 -- [28:21] + Rm : BitVec 5 -- [20:16] + opcode : BitVec 6 -- [15:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Data_processing_two_source_cls where toString a := toString (repr a) + +def Data_processing_two_source_cls.toBitVec32 + (x : Data_processing_two_source_cls) : BitVec 32 := + x.sf ++ x._fixed1 ++ x.S ++ x._fixed2 ++ x.Rm ++ x.opcode ++ x.Rn ++ x.Rd + structure Logical_shifted_reg_cls where sf : BitVec 1 -- [31:31] opc : BitVec 2 -- [30:29] @@ -81,22 +115,6 @@ instance : ToString Logical_shifted_reg_cls where toString a := toString (repr a def Logical_shifted_reg_cls.toBitVec32 (x : Logical_shifted_reg_cls) : BitVec 32 := x.sf ++ x.opc ++ x._fixed ++ x.shift ++ x.N ++ x.Rm ++ x.imm6 ++ x.Rn ++ x.Rd -structure Data_processing_one_source_cls where - sf : BitVec 1 -- [31:31] - _fixed1 : BitVec 1 := 0b1#1 -- [30:30] - S : BitVec 1 -- [29:29] - _fixed2 : BitVec 8 := 0b11010110#8 -- [28:21] - opcode2 : BitVec 5 -- [20:16] - opcode : BitVec 6 -- [15:10] - Rn : BitVec 5 -- [9:5] - Rd : BitVec 5 -- [4:0] -deriving DecidableEq, Repr - -instance : ToString Data_processing_one_source_cls where toString a := toString (repr a) - -def Data_processing_one_source_cls.toBitVec32 (x : Data_processing_one_source_cls) : BitVec 32 := - x.sf ++ x._fixed1 ++ x.S ++ x._fixed2 ++ x.opcode2 ++ x.opcode ++ x.Rn ++ x.Rd - inductive DataProcRegInst where | Add_sub_carry : Add_sub_carry_cls → DataProcRegInst @@ -106,6 +124,8 @@ inductive DataProcRegInst where Conditional_select_cls → DataProcRegInst | Data_processing_one_source: Data_processing_one_source_cls → DataProcRegInst + | Data_processing_two_source: + Data_processing_two_source_cls → DataProcRegInst | Logical_shifted_reg : Logical_shifted_reg_cls → DataProcRegInst deriving DecidableEq, Repr diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean index eceb57bb..a0e42d0a 100644 --- a/Arm/Decode/DPSFP.lean +++ b/Arm/Decode/DPSFP.lean @@ -187,6 +187,43 @@ instance : ToString Advanced_simd_modified_immediate_cls where toString a := toS 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_shift_by_immediate_cls where + _fixed1 : BitVec 1 := 0b0#1 -- [31:31] + Q : BitVec 1 -- [30:30] + U : BitVec 1 -- [29:29] + _fixed2 : BitVec 6 := 0b011110#6 -- [28:23] + immh : BitVec 4 -- [22:19] + immb : BitVec 3 -- [18:16] + opcode : BitVec 5 -- [15:11] + _fixed3 : BitVec 1 := 0b1#1 -- [10:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Advanced_simd_shift_by_immediate_cls where toString a := toString (repr a) + +def Advanced_simd_shift_by_immediate_cls.toBitVec32 + (x : Advanced_simd_shift_by_immediate_cls) : BitVec 32 := + x._fixed1 ++ x.Q ++ x.U ++ x._fixed2 ++ x.immh ++ x.immb ++ x.opcode ++ x._fixed3 ++ x.Rn ++ x.Rd + +structure Advanced_simd_scalar_shift_by_immediate_cls where + _fixed1 : BitVec 2 := 0b01#2 -- [31:30] + U : BitVec 1 -- [29:29] + _fixed2 : BitVec 6 := 0b111110#6 -- [28:23] + immh : BitVec 4 -- [22:19] + immb : BitVec 3 -- [18:16] + opcode : BitVec 5 -- [15:11] + _fixed3 : BitVec 1 := 0b1#1 -- [10:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Advanced_simd_scalar_shift_by_immediate_cls where toString a := toString (repr a) + +def Advanced_simd_scalar_shift_by_immediate_cls.toBitVec32 + (x : Advanced_simd_scalar_shift_by_immediate_cls) : BitVec 32 := + x._fixed1 ++ x.U ++ x._fixed2 ++ x.immh ++ x.immb ++ x.opcode ++ x._fixed3 ++ x.Rn ++ x.Rd + structure Advanced_simd_table_lookup_cls where _fixed1 : BitVec 1 := 0b0#1 -- [31:31] Q : BitVec 1 -- [30:30] @@ -283,6 +320,10 @@ inductive DataProcSFPInst where Advanced_simd_permute_cls → DataProcSFPInst | Advanced_simd_modified_immediate : Advanced_simd_modified_immediate_cls → DataProcSFPInst + | Advanced_simd_shift_by_immediate : + Advanced_simd_shift_by_immediate_cls → DataProcSFPInst + | Advanced_simd_scalar_shift_by_immediate : + Advanced_simd_scalar_shift_by_immediate_cls → DataProcSFPInst | Advanced_simd_scalar_copy : Advanced_simd_scalar_copy_cls → DataProcSFPInst | Advanced_simd_table_lookup : diff --git a/Arm/Exec.lean b/Arm/Exec.lean index 86b92c34..f7c7f675 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -37,6 +37,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := DPR.exec_conditional_select i s | DPR (DataProcRegInst.Data_processing_one_source i) => DPR.exec_data_processing_one_source i s + | DPR (DataProcRegInst.Data_processing_two_source i) => + DPR.exec_data_processing_two_source i s | DPR (DataProcRegInst.Logical_shifted_reg i) => DPR.exec_logical_shifted_reg i s @@ -58,6 +60,10 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := DPSFP.exec_advanced_simd_permute i s | DPSFP (DataProcSFPInst.Advanced_simd_modified_immediate i) => DPSFP.exec_advanced_simd_modified_immediate i s + | DPSFP (DataProcSFPInst.Advanced_simd_shift_by_immediate i) => + DPSFP.exec_advanced_simd_shift_by_immediate i s + | DPSFP (DataProcSFPInst.Advanced_simd_scalar_shift_by_immediate i) => + DPSFP.exec_advanced_simd_scalar_shift_by_immediate i s | DPSFP (DataProcSFPInst.Advanced_simd_scalar_copy i) => DPSFP.exec_advanced_simd_scalar_copy i s | DPSFP (DataProcSFPInst.Advanced_simd_table_lookup i) => @@ -84,6 +90,10 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := | LDST (LDSTInst.Advanced_simd_multiple_struct_post_indexed i) => LDST.exec_advanced_simd_multiple_struct_post_indexed i s + -- | _ => + -- write_err + -- (StateError.Unimplemented s!"Unsupported ArmInst {ai} encountered in exec_inst!") s + def stepi (s : ArmState) : ArmState := -- This function should be simulated away automatically because the diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index c78660b4..f349be99 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -368,4 +368,81 @@ def elem_set (vector : BitVec n) (e : Nat) (size : Nat) have h : hi - lo + 1 = size := by simp only [hi, lo]; omega BitVec.partInstall hi lo (h ▸ value) vector +---------------------------------------------------------------------- + +-- Field unsigned, round and accumulate are not used in left shifts +structure ShiftInfo where + esize : Nat + elements : Nat + shift : Nat + unsigned := true + round := false + accumulate := false + h : esize > 0 +deriving DecidableEq, Repr + +export ShiftInfo (esize elements shift unsigned round accumulate) + +@[state_simp_rules] +def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool) (h : n > 0) + : BitVec n := + -- assert shift > 0 + let fn := if unsigned then ushiftRight else sshiftRight + let rounded_bv := + if round then + let rounded := value + (1 <<< (shift - 1)) + BitVec.ofInt (n + 1) rounded + else + BitVec.ofInt (n + 1) value + have h₀ : n - 1 - 0 + 1 = n := by omega + h₀ ▸ extractLsb (n-1) 0 (fn rounded_bv shift) + +@[state_simp_rules] +def Int_with_unsigned (unsigned : Bool) (value : BitVec n) : Int := + if unsigned then value.toNat else value.toInt + +def shift_right_common_aux + (e : Nat) (info : ShiftInfo) (operand : BitVec datasize) + (operand2 : BitVec datasize) (result : BitVec datasize) : BitVec datasize := + if h : info.elements ≤ e then + result + else + let elem := Int_with_unsigned info.unsigned $ elem_get operand e info.esize info.h + let shift_elem := RShr info.unsigned elem info.shift info.round info.h + let acc_elem := elem_get operand2 e info.esize info.h + shift_elem + let result := elem_set result e info.esize acc_elem info.h + have _ : info.elements - (e + 1) < info.elements - e := by omega + shift_right_common_aux (e + 1) info operand operand2 result + termination_by (info.elements - e) + +@[state_simp_rules] +def shift_right_common + (info : ShiftInfo) (datasize : Nat) (Rn : BitVec 5) (Rd : BitVec 5) + (s : ArmState) : BitVec datasize := + let operand := read_sfp datasize Rn s + let operand2 := if info.accumulate then read_sfp datasize Rd s else BitVec.zero datasize + let result := BitVec.zero datasize + shift_right_common_aux 0 info operand operand2 result + +def shift_left_common_aux + (e : Nat) (info : ShiftInfo) (operand : BitVec datasize) + (result : BitVec datasize) : BitVec datasize := + if h : info.elements ≤ e then + result + else + let elem := elem_get operand e info.esize info.h + let shift_elem := elem <<< info.shift + let result := elem_set result e info.esize shift_elem info.h + have _ : info.elements - (e + 1) < info.elements - e := by omega + shift_left_common_aux (e + 1) info operand result + termination_by (info.elements - e) + +@[state_simp_rules] +def shift_left_common + (info : ShiftInfo) (datasize : Nat) (Rn : BitVec 5) (s : ArmState) + : BitVec datasize := + let operand := read_sfp datasize Rn s + let result := BitVec.zero datasize + shift_left_common_aux 0 info operand result + end Common diff --git a/Arm/Insts/DPR/Data_processing_two_source.lean b/Arm/Insts/DPR/Data_processing_two_source.lean new file mode 100644 index 00000000..5e3ccf3d --- /dev/null +++ b/Arm/Insts/DPR/Data_processing_two_source.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +-- LSLV, LSRV, ASRV, RORV (32-, 64-bit) + +import Arm.Decode +import Arm.Insts.Common + +---------------------------------------------------------------------- + +namespace DPR + +open BitVec + +@[state_simp_rules] +def exec_data_processing_shift + (inst : Data_processing_two_source_cls) (s : ArmState) : ArmState := + let datasize := 32 <<< inst.sf.toNat + let shift_type := decode_shift $ extractLsb 1 0 inst.opcode + let operand2 := read_gpr_zr datasize inst.Rm s + let amount := BitVec.ofInt 6 (operand2.toInt % datasize) + let operand := read_gpr_zr datasize inst.Rn s + let result := shift_reg operand shift_type amount + -- State Update + let s := write_gpr_zr datasize inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +@[state_simp_rules] +def exec_data_processing_two_source + (inst : Data_processing_two_source_cls) (s : ArmState) : ArmState := + match inst.S, inst.opcode with + | 0b0#1, 0b001000#6 -- LSLV 32-, 64-bit + | 0b0#1, 0b001001#6 -- LSRV 32-, 64-bit + | 0b0#1, 0b001010#6 -- ASRV 32-, 64-bit + | 0b0#1, 0b001011#6 -- RORV 32-, 64-bit + => exec_data_processing_shift inst s + | _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s + +---------------------------------------------------------------------- + +def Data_processing_two_source_cls.shift.rand + (opcode : BitVec 6) : IO (Option (BitVec 32)) := do + let (inst : Data_processing_two_source_cls) := + { sf := ← BitVec.rand 1, + S := 0b0#1, + Rm := ← BitVec.rand 5, + opcode := opcode, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +/-- Generate random instructions of Data_processing_two_source_cls class. -/ +def Data_processing_two_source_cls.rand : List (IO (Option (BitVec 32))) := + [ Data_processing_two_source_cls.shift.rand 0b001000#6, + Data_processing_two_source_cls.shift.rand 0b001001#6, + Data_processing_two_source_cls.shift.rand 0b001010#6, + Data_processing_two_source_cls.shift.rand 0b001011#6 + ] + +end DPR diff --git a/Arm/Insts/DPR/Insts.lean b/Arm/Insts/DPR/Insts.lean index cc10db8b..13e254b6 100644 --- a/Arm/Insts/DPR/Insts.lean +++ b/Arm/Insts/DPR/Insts.lean @@ -7,6 +7,7 @@ import Arm.Insts.DPR.Add_sub_carry import Arm.Insts.DPR.Add_sub_shifted_reg import Arm.Insts.DPR.Conditional_select import Arm.Insts.DPR.Data_processing_one_source +import Arm.Insts.DPR.Data_processing_two_source import Arm.Insts.DPR.Logical_shifted_reg /-- List of functions to generate random instructions of the @@ -16,4 +17,5 @@ def DPR.rand : List (IO (Option (BitVec 32))) := DPR.Add_sub_shifted_reg_cls.rand, DPR.Conditional_select_cls.rand, DPR.Data_processing_one_source_cls.rand, - DPR.Logical_shifted_reg_cls.rand] + DPR.Logical_shifted_reg_cls.rand] ++ + DPR.Data_processing_two_source_cls.rand diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_shift_by_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_shift_by_immediate.lean new file mode 100644 index 00000000..8f58067e --- /dev/null +++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_shift_by_immediate.lean @@ -0,0 +1,121 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +-- SHL, SSHR and USHR, SSRA and USRA, SRSHR and URSHR, SRSRA and URSRA (scalar) + +import Arm.Decode +import Arm.Insts.Common + +---------------------------------------------------------------------- + +namespace DPSFP + +open BitVec + +@[state_simp_rules] +def exec_shift_right_scalar + (inst : Advanced_simd_scalar_shift_by_immediate_cls) (s : ArmState) : ArmState := + if extractLsb 3 3 inst.immh != 0b1#1 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let esize := 8 <<< 3 + have h : esize > 0 := by decide + let datasize := esize + let (info : ShiftInfo) := + { esize := esize, + elements := 1, + shift := (esize * 2) - (inst.immh ++ inst.immb).toNat, + unsigned := inst.U == 0b1#1, + round := (extractLsb 2 2 inst.opcode) == 0b1#1, + accumulate := (extractLsb 1 1 inst.opcode) == 0b1#1, + h := h + } + let result := shift_right_common info datasize inst.Rn inst.Rd s + -- State Update + let s := write_sfp datasize inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +@[state_simp_rules] +def exec_shl_scalar + (inst : Advanced_simd_scalar_shift_by_immediate_cls) (s : ArmState) : ArmState := + if extractLsb 3 3 inst.immh != 0b1#1 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let esize := 8 <<< 3 + have h : esize > 0 := by decide + let datasize := esize + let (info : ShiftInfo) := + { esize := esize, + elements := 1, + shift := (inst.immh ++ inst.immb).toNat - esize, + h := h + } + let result := shift_left_common info datasize inst.Rn s + -- State Update + let s := write_sfp datasize inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +@[state_simp_rules] +def exec_advanced_simd_scalar_shift_by_immediate + (inst : Advanced_simd_scalar_shift_by_immediate_cls) (s : ArmState) : ArmState := + match inst.U, inst.opcode with + | 0b0#1, 0b01010#5 => exec_shl_scalar inst s -- SHL + | 0b0#1, 0b00000#5 -- SSHR + | 0b0#1, 0b00010#5 -- SSRA + | 0b0#1, 0b00100#5 -- SRSHR + | 0b0#1, 0b00110#5 -- SRSRA + | 0b1#1, 0b00000#5 -- USHR + | 0b1#1, 0b00010#5 -- USRA + | 0b1#1, 0b00100#5 -- URSHR + | 0b1#1, 0b00110#5 -- URSRA + => exec_shift_right_scalar inst s + | _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s + +---------------------------------------------------------------------- + +partial def Advanced_simd_scalar_shift_by_immediate_cls.shr_all.rand + (opcode : BitVec 5) : IO (Option (BitVec 32)) := do + let immh := ← BitVec.rand 4 + if extractLsb 3 3 immh != 0b1#1 then + Advanced_simd_scalar_shift_by_immediate_cls.shr_all.rand opcode + else + let (inst : Advanced_simd_scalar_shift_by_immediate_cls) := + { U := ← BitVec.rand 1, + immh := immh, + immb := ← BitVec.rand 3, + opcode := opcode, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +partial def Advanced_simd_scalar_shift_by_immediate_cls.shl.rand + : IO (Option (BitVec 32)) := do + let immh := ← BitVec.rand 4 + if extractLsb 3 3 immh != 0b1#1 then + Advanced_simd_scalar_shift_by_immediate_cls.shl.rand + else + let (inst : Advanced_simd_scalar_shift_by_immediate_cls) := + { U := 0b0#1, + immh := immh, + immb := ← BitVec.rand 3, + opcode := 0b01010#5, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +/-- Generate random instructions of Advanced_simd_scalar_shift_by_immediate_cls class. -/ +def Advanced_simd_scalar_shift_by_immediate_cls.rand : List (IO (Option (BitVec 32))) := +[ Advanced_simd_scalar_shift_by_immediate_cls.shl.rand, -- SHL + Advanced_simd_scalar_shift_by_immediate_cls.shr_all.rand 0b00000#5, -- SSHR, USHR + Advanced_simd_scalar_shift_by_immediate_cls.shr_all.rand 0b00010#5, -- SSRA, USRA + Advanced_simd_scalar_shift_by_immediate_cls.shr_all.rand 0b00100#5, -- SRSHR, URSHR + Advanced_simd_scalar_shift_by_immediate_cls.shr_all.rand 0b00110#5 -- SRSRA, URSRA + ] + +end DPSFP diff --git a/Arm/Insts/DPSFP/Advanced_simd_shift_by_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_shift_by_immediate.lean new file mode 100644 index 00000000..c067fded --- /dev/null +++ b/Arm/Insts/DPSFP/Advanced_simd_shift_by_immediate.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +-- SHL, SSHR and USHR, SSRA and USRA, SRSHR and URSHR, SRSRA and URSRA (vector) + +import Arm.Decode +import Arm.Insts.Common + +---------------------------------------------------------------------- + +namespace DPSFP + +open BitVec + +@[state_simp_rules] +def exec_shift_right_vector + (inst : Advanced_simd_shift_by_immediate_cls) (s : ArmState) : ArmState := + if (extractLsb 3 3 inst.immh) ++ inst.Q == 0b10#2 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let l := Option.get! $ highest_set_bit inst.immh + let esize := 8 <<< l + have h : esize > 0 := by + simp only [esize] + apply zero_lt_shift_left_pos (by decide) + let datasize := 64 <<< inst.Q.toNat + let (info : ShiftInfo) := + { esize := esize, + elements := datasize / esize, + shift := (2 * esize) - (inst.immh ++ inst.immb).toNat, + unsigned := inst.U == 0b1#1, + round := (extractLsb 2 2 inst.opcode) == 0b1#1, + accumulate := (extractLsb 1 1 inst.opcode) == 0b1#1, + h := h } + let result := shift_right_common info datasize inst.Rn inst.Rd s + -- State Update + let s := write_sfp datasize inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +@[state_simp_rules] +def exec_shl_vector + (inst : Advanced_simd_shift_by_immediate_cls) (s : ArmState) : ArmState := + if (extractLsb 3 3 inst.immh) ++ inst.Q == 0b10#2 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let l := Option.get! $ highest_set_bit inst.immh + let esize := 8 <<< l + have h : esize > 0 := by + simp only [esize] + apply zero_lt_shift_left_pos (by decide) + let datasize := 64 <<< inst.Q.toNat + let (info : ShiftInfo) := + { esize := esize, + elements := datasize / esize, + shift := (inst.immh ++ inst.immb).toNat - esize, + h := h } + let result := shift_left_common info datasize inst.Rn s + -- State Update + let s := write_sfp datasize inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +@[state_simp_rules] +def exec_advanced_simd_shift_by_immediate + (inst : Advanced_simd_shift_by_immediate_cls) (s : ArmState) : ArmState := + if inst.immh == 0b0000#4 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + match inst.U, inst.opcode with + | 0b0#1, 0b01010#5 => exec_shl_vector inst s -- SHL + | 0b0#1, 0b00000#5 -- SSHR + | 0b0#1, 0b00010#5 -- SSRA + | 0b0#1, 0b00100#5 -- SRSHR + | 0b0#1, 0b00110#5 -- SRSRA + | 0b1#1, 0b00000#5 -- USHR + | 0b1#1, 0b00010#5 -- USRA + | 0b1#1, 0b00100#5 -- URSHR + | 0b1#1, 0b00110#5 -- URSRA + => exec_shift_right_vector inst s + | _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s + +---------------------------------------------------------------------- + +partial def Advanced_simd_shift_by_immediate_cls.shr_all.rand + (opcode : BitVec 5) : IO (Option (BitVec 32)) := do + let Q := ← BitVec.rand 1 + let immh := ← BitVec.rand 4 + if immh == 0b0000#4 || (extractLsb 3 3 immh) ++ Q == 0b10#2 then + Advanced_simd_shift_by_immediate_cls.shr_all.rand opcode + else + let (inst : Advanced_simd_shift_by_immediate_cls) := + { Q := Q, + U := ← BitVec.rand 1, + immh := immh, + immb := ← BitVec.rand 3, + opcode := opcode, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +partial def Advanced_simd_shift_by_immediate_cls.shl.rand + : IO (Option (BitVec 32)) := do + let Q := ← BitVec.rand 1 + let immh := ← BitVec.rand 4 + if immh == 0b0000#4 || (extractLsb 3 3 immh) ++ Q == 0b10#2 then + Advanced_simd_shift_by_immediate_cls.shl.rand + else + let (inst : Advanced_simd_shift_by_immediate_cls) := + { Q := Q, + U := 0b0#1, + immh := immh, + immb := ← BitVec.rand 3, + opcode := 0b01010#5, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +/-- Generate random instructions of Advanced_simd_shift_by_immediate_cls class. -/ +def Advanced_simd_shift_by_immediate_cls.rand : List (IO (Option (BitVec 32))) := +[ Advanced_simd_shift_by_immediate_cls.shl.rand, -- SHL + Advanced_simd_shift_by_immediate_cls.shr_all.rand 0b00000#5, -- SSHR, USHR + Advanced_simd_shift_by_immediate_cls.shr_all.rand 0b00010#5, -- SSRA, USRA + Advanced_simd_shift_by_immediate_cls.shr_all.rand 0b00100#5, -- SRSHR, URSHR + Advanced_simd_shift_by_immediate_cls.shr_all.rand 0b00110#5 -- SRSRA, URSRA + ] + +end DPSFP diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean index 6bef855f..c9209500 100644 --- a/Arm/Insts/DPSFP/Insts.lean +++ b/Arm/Insts/DPSFP/Insts.lean @@ -8,6 +8,8 @@ import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc import Arm.Insts.DPSFP.Advanced_simd_extract import Arm.Insts.DPSFP.Advanced_simd_permute import Arm.Insts.DPSFP.Advanced_simd_modified_immediate +import Arm.Insts.DPSFP.Advanced_simd_shift_by_immediate +import Arm.Insts.DPSFP.Advanced_simd_scalar_shift_by_immediate import Arm.Insts.DPSFP.Advanced_simd_scalar_copy import Arm.Insts.DPSFP.Advanced_simd_table_lookup import Arm.Insts.DPSFP.Advanced_simd_three_same @@ -25,6 +27,8 @@ def DPSFP.rand : List (IO (Option (BitVec 32))) := DPSFP.Advanced_simd_extract_cls.rand ++ DPSFP.Advanced_simd_permute_cls.rand ++ DPSFP.Advanced_simd_modified_immediate_cls.rand ++ + DPSFP.Advanced_simd_shift_by_immediate_cls.rand ++ + DPSFP.Advanced_simd_scalar_shift_by_immediate_cls.rand ++ DPSFP.Advanced_simd_scalar_copy_cls.rand ++ DPSFP.Advanced_simd_table_lookup_cls.rand ++ DPSFP.Advanced_simd_three_same_cls.rand ++