LSR (alias of UBFM) in Data Processing Immediate. (#20)

### Description:
Add LSR instruction which is an alias of UBFM and is part of Bitfield
instructions of Data Processing - Immediate (DPI)

https://developer.arm.com/documentation/ddi0602/2023-12/Base-Instructions/LSR--immediate---Logical-Shift-Right--immediate---an-alias-of-UBFM-


### Testing:

`make all` including conformance testing.

#### Call out:
There is a specific rand function to add LSR immediate instructions.
However, the conformance test output shows mostly UBFX and UBFIZ and a
few LSR and LSL in the output. I think the specific function is not
being called.

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Arm/Decode/DPI.lean

@@ -55,7 +55,7 @@ deriving DecidableEq, Repr
 
 instance : ToString PC_rel_addressing_cls where toString a := toString (repr a)
 
-structure Bitfield_cls where 
+structure Bitfield_cls where
   sf     : BitVec 1                -- [31:31]
   opc    : BitVec 2                -- [30:29]
   _fixed : BitVec 6 := 0b100110#6  -- [28:23]
@@ -68,6 +68,9 @@ deriving DecidableEq, Repr
 
 instance : ToString Bitfield_cls where toString a := toString (repr a)
 
+def Bitfield_cls.toBitVec32 (x : Bitfield_cls) : BitVec 32 :=
+  x.sf ++ x.opc ++ x._fixed ++ x.N ++ x.immr ++ x.imms ++ x.Rn ++ x.Rd
+
 inductive DataProcImmInst where
   | Add_sub_imm :
     Add_sub_imm_cls → DataProcImmInst

Arm/Exec.lean

@@ -17,6 +17,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
     DPI.exec_pc_rel_addressing i s
   | DPI (DataProcImmInst.Logical_imm i) =>
     DPI.exec_logical_imm i s
+  | DPI (DataProcImmInst.Bitfield i) =>
+    DPI.exec_bitfield i s
 
   | BR (BranchInst.Compare_branch i) =>
     BR.exec_compare_branch i s

Arm/Insts/DPI/Add_sub_imm.lean

@@ -39,7 +39,7 @@ def exec_add_sub_imm (inst : Add_sub_imm_cls) (s : ArmState) : ArmState :=
 ----------------------------------------------------------------------
 
 /-- Generate random instructions of the DPI.Add_sub_imm class. -/
-def Add_sub_imm_cls.rand : IO (Option (BitVec 32)) := do
+def Add_sub_imm_cls.inst.rand : IO (Option (BitVec 32)) := do
   let (inst : Add_sub_imm_cls) :=
     { sf    := ← BitVec.rand 1,
       op    := ← BitVec.rand 1,
@@ -54,6 +54,8 @@ def Add_sub_imm_cls.rand : IO (Option (BitVec 32)) := do
       Rd    := ← BitVec.rand 5 (lo := 0) (hi := 30) }
   pure (some (inst.toBitVec32))
 
+def Add_sub_imm_cls.rand : List (IO (Option (BitVec 32))) :=
+  [ Add_sub_imm_cls.inst.rand ]
 ----------------------------------------------------------------------
 
 end DPI

Arm/Insts/DPI/Bitfield.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel, Nevine
+-/
+-- For now, support only UBFM (immediate) 32- and 64-bit versions
+-- (aliased as LSR and LSL (immediate) among other aliases)
+
+import Arm.Decode
+import Arm.Insts.Common
+
+namespace DPI
+
+open Std.BitVec
+
+@[simp]
+def exec_bitfield (inst: Bitfield_cls) (s : ArmState) : ArmState :=
+  if inst.opc != 0b10#2 then
+    write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
+  else
+    let immr5 := inst.immr >>> 5
+    let imms5 := inst.imms >>> 5
+    if (inst.sf == 1 && inst.N != 1) ||
+      (inst.sf == 0 && (inst.N != 0 || immr5 != 0 || imms5 != 0)) then
+      write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+    else
+      let datasize  := if inst.sf == 1#1 then 64 else 32
+      let wtmask    := decode_bit_masks inst.N inst.imms inst.immr false datasize
+      match wtmask with
+      | none => write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+      | some (wmask, tmask) =>
+        let src := read_gpr_zr datasize inst.Rn s
+        let bot := (BitVec.ror src inst.immr.toNat) &&& wmask
+        let result := bot &&& tmask
+        let s := write_gpr_zr datasize inst.Rd result s
+        let s := write_pc ((read_pc s) + 4#64) s
+        s
+
+
+----------------------------------------------------------------------
+
+/-- Generate random instructions of the DPI.Bitfield class. -/
+partial def Bitfield_cls.ubfm.rand : IO (Option (BitVec 32)) := do
+  -- Choose assignments based on sf that will not result in illegal instructions
+  let sf := ← BitVec.rand 1
+  let N := sf
+  let immr := sf ++ (← BitVec.rand 5)
+  let imms := sf ++ (← BitVec.rand 5)
+  let (inst : Bitfield_cls) :=
+    { sf    := sf,
+      opc   := ← pure 0b10#2,
+      N     := N,
+      immr  := immr,
+      imms  := imms,
+       -- TODO: Do we need to limit Rn and Rd to be up to 30 as in Add_sub_imm?
+      Rn    := ← BitVec.rand 5,
+      Rd    := ← BitVec.rand 5 }
+  pure (some (inst.toBitVec32))
+
+partial def Bitfield_cls.lsr.rand : IO (Option (BitVec 32)) := do
+  -- Specifically test the assignment that results in LSR
+  let sf := ← BitVec.rand 1
+  let N := sf
+  let immr := sf ++ (← BitVec.rand 5)
+  let imms := sf ++ 0b11111#5
+  let (inst : Bitfield_cls) :=
+    { sf    := sf,
+      opc   := ← pure 0b10#2,
+      N     := N,
+      immr  := immr,
+      imms  := imms,
+       -- TODO: Do we need to limit Rn and Rd to be up to 30 as in Add_sub_imm?
+      Rn    := ← BitVec.rand 5,
+      Rd    := ← BitVec.rand 5 }
+  pure (some (inst.toBitVec32))
+
+
+def Bitfield_cls.rand : List (IO (Option (BitVec 32))) :=
+  [ Bitfield_cls.lsr.rand,
+    Bitfield_cls.ubfm.rand ]
+----------------------------------------------------------------------
+
+end DPI

Arm/Insts/DPI/Insts.lean

@@ -6,9 +6,11 @@ Author(s): Shilpi Goel
 import Arm.Insts.DPI.Add_sub_imm
 import Arm.Insts.DPI.PC_rel_addressing
 import Arm.Insts.DPI.Logical_imm
+import Arm.Insts.DPI.Bitfield
 
 /-- List of functions to generate random instructions of the
 DPI class. -/
 def DPI.rand : List (IO (Option (BitVec 32))) :=
-  [ DPI.Add_sub_imm_cls.rand,
-    DPI.Logical_imm_cls.rand ]
+  DPI.Add_sub_imm_cls.rand ++
+  DPI.Logical_imm_cls.rand ++
+  DPI.Bitfield_cls.rand

Arm/Insts/DPI/Logical_imm.lean

@@ -61,7 +61,7 @@ def exec_logical_imm (inst : Logical_imm_cls) (s : ArmState) : ArmState :=
 ----------------------------------------------------------------------
 
 /-- Generate random instructions of the DPI.Logical_imm class. -/
-partial def Logical_imm_cls.rand : IO (Option (BitVec 32)) := do
+partial def Logical_imm_cls.inst.rand : IO (Option (BitVec 32)) := do
   let opc := ← BitVec.rand 2
   let op  := decode_op opc
   -- (FIXME) We want to avoid use of SP (i.e., register index
@@ -79,8 +79,11 @@ partial def Logical_imm_cls.rand : IO (Option (BitVec 32)) := do
     }
   let datasize := 32 <<< inst.sf.toNat
   if inst.sf = 0#1 ∧ inst.N = 1#1 ∨ invalid_bit_masks inst.N inst.imms true datasize then
-    Logical_imm_cls.rand
+    Logical_imm_cls.inst.rand
   else
     pure (some (inst.toBitVec32))
 
+def Logical_imm_cls.rand : List (IO (Option (BitVec 32))) :=
+  [ Logical_imm_cls.inst.rand ]
+
 end DPI

Arm/Insts/DPSFP/Crypto_four_reg.lean

@@ -16,6 +16,7 @@ namespace DPSFP
 
 open Std.BitVec
 
+@[simp]
 def exec_crypto_four_reg (inst : Crypto_four_reg_cls) (s : ArmState) : ArmState :=
   -- This function assumes IsFeatureImplemented(FEAT_SHA3) is true
   -- and that AArch64.CheckFPAdvSIMDEnabled() returns successfully