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.
leanprover · Mar 18, 2024 · 28dc04b · 28dc04b
1 parent 49990d5
commit 28dc04b
Show file tree

Hide file tree

Showing 11 changed files with 498 additions and 18 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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