Fix merge conflicts

Arm/Decode.lean

@@ -76,6 +76,8 @@ def decode_data_proc_reg (i : BitVec 32) : Option ArmInst :=
     DPR (Add_sub_shifted_reg {sf, op, S, shift, Rm, imm6, Rn, Rd})
   | [sf:1, op:1, S:1, 11010100, Rm:5, cond:4, op2:2, Rn:5, Rd:5] =>
     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, 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
@@ -460,6 +462,20 @@ example : decode_raw_inst 0x9eaf00b9 =
               Rd := 0x19#5 })) := by
             rfl
 
+-- rev x0, x25
+example : decode_raw_inst 0xdac00f20 =
+          (ArmInst.DPR
+            (DataProcRegInst.Data_processing_one_source
+            { sf := 0x1#1,
+              _fixed1 := 0x1#1,
+              S := 0x0#1,
+              _fixed2 := 0xd6#8,
+              opcode2 := 0x00#5,
+              opcode := 0x03#6,
+              Rn := 0x19#5,
+              Rd := 0x00#5 })) := by
+          rfl
+
 -- Unimplemented
 example : decode_raw_inst 0x00000000#32 = none := by rfl
 

Arm/Decode/DPR.lean

@@ -67,7 +67,7 @@ def Conditional_select_cls.toBitVec32 (x : Conditional_select_cls) : BitVec 32 :
 structure Logical_shifted_reg_cls where
   sf     : BitVec 1                 -- [31:31]
   opc    : BitVec 2                 -- [30:29]
-  _fixed : BitVec 5 := 0b01010      -- [28:24]
+  _fixed : BitVec 5 := 0b01010#5    -- [28:24]
   shift  : BitVec 2                 -- [23:22]
   N      : BitVec 1                 -- [21:21]
   Rm     : BitVec 5                 -- [20:16]
@@ -81,13 +81,31 @@ 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
   | Add_sub_shifted_reg :
     Add_sub_shifted_reg_cls → DataProcRegInst
   | Conditional_select :
     Conditional_select_cls → DataProcRegInst
+  | Data_processing_one_source:
+    Data_processing_one_source_cls → DataProcRegInst
   | Logical_shifted_reg :
     Logical_shifted_reg_cls → DataProcRegInst
 deriving DecidableEq, Repr

Arm/Exec.lean

@@ -35,6 +35,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
     DPR.exec_add_sub_shifted_reg i s
   | DPR (DataProcRegInst.Conditional_select i) =>
     DPR.exec_conditional_select i s
+  | DPR (DataProcRegInst.Data_processing_one_source i) =>
+    DPR.exec_data_processing_one_source i s
   | DPR (DataProcRegInst.Logical_shifted_reg i) =>
     DPR.exec_logical_shifted_reg i s
 

Arm/Insts/Common.lean

@@ -256,4 +256,69 @@ inductive FPConvOp where
   | FPConvOp_CVT_FtoI_JS : FPConvOp
 deriving DecidableEq, Repr
 
+----------------------------------------------------------------------
+
+/-- Reverse the order of `esize`-bit elements in `x`.-/
+def rev_elems (n esize : Nat) (x : BitVec n) (h₀ : esize ∣ n) (h₁ : 0 < esize) : BitVec n :=
+  if h0 : n <= esize then
+    x
+  else
+    let element := BitVec.zeroExtend esize x
+    let rest_x := BitVec.zeroExtend (n - esize) (x >>> esize)
+    have h1 : esize <= n := by 
+      simp at h0; exact Nat.le_of_lt h0; done
+    have h2 : esize ∣ (n - esize) := by
+      refine Nat.dvd_sub ?H h₀ ?h₂
+      · exact h1
+      · simp only [Nat.dvd_refl]
+      done
+    have ?term_lemma : n - esize < n := by exact Nat.sub_lt_self h₁ h1
+    let rest_ans := rev_elems (n - esize) esize rest_x h2 h₁
+    have h3 : (esize + (n - esize)) = n := by
+      simp_all only [ge_iff_le, Nat.add_sub_cancel', h1]
+    h3 ▸ (element ++ rest_ans)
+   termination_by n
+
+example : rev_elems 4 4 0xA#4 (by decide) (by decide) = 0xA#4 := rfl
+example : rev_elems 8 4 0xAB#8 (by decide) (by decide) = 0xBA#8 := rfl
+example : rev_elems 8 4 (rev_elems 8 4 0xAB#8 (by decide) (by decide))
+          (by decide) (by decide) = 0xAB#8 := by native_decide 
+
+theorem rev_elems_base :
+  rev_elems esize esize x h₀ h₁ = x := by
+  unfold rev_elems; simp; done
+
+/-- Divide a bv of width `datasize` into containers, each of size
+`container_size`, and within a container, reverse the order of `esize`-bit
+elements. -/
+def rev_vector (datasize container_size esize : Nat) (x : BitVec datasize)
+  (h₀ : 0 < esize) (h₁ : esize <= container_size) (h₂ : container_size <= datasize)
+  (h₃ : esize ∣ container_size) (h₄ : container_size ∣ datasize) :
+  BitVec datasize :=
+  if h0 : datasize = container_size then
+    h0 ▸ (rev_elems container_size esize (h0 ▸ x) h₃ h₀)
+  else
+    let container := BitVec.zeroExtend container_size x
+    let new_container := rev_elems container_size esize container h₃ h₀
+    let new_datasize := datasize - container_size
+    let rest_x := BitVec.zeroExtend new_datasize (x >>> container_size)
+    have h₄' : container_size ∣ new_datasize := by
+      have h : container_size ∣ container_size := Nat.dvd_refl _
+      exact Nat.dvd_sub h₂ h₄ h
+    have h₂' : container_size <= new_datasize := by 
+      refine Nat.le_of_dvd ?h h₄'
+      omega
+    have h1 : 0 < container_size := by exact Nat.lt_of_lt_of_le h₀ h₁
+    have ?term_lemma : new_datasize < datasize := by exact Nat.sub_lt_self h1 h₂
+    let rest_ans := rev_vector new_datasize container_size esize rest_x h₀ h₁ h₂' h₃ h₄'
+    have h2 : new_datasize + container_size = datasize := by
+        rw [Nat.sub_add_cancel h₂]
+    h2 ▸ (rest_ans ++ new_container)
+  termination_by datasize
+
+example : rev_vector 32 16 8 0xaabbccdd#32 (by decide)
+          (by decide) (by decide) (by decide) (by decide) =
+          0xbbaaddcc#32 := by
+          native_decide
+
 end Common

Arm/Insts/DPI/Bitfield.lean

@@ -11,7 +11,7 @@ import Arm.Insts.Common
 
 namespace DPI
 
-open Std.BitVec
+open BitVec
 
 @[simp]
 def exec_bitfield (inst: Bitfield_cls) (s : ArmState) : ArmState :=
@@ -52,11 +52,18 @@ partial def Bitfield_cls.ubfm.rand : IO (Option (BitVec 32)) := do
       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?
+       -- 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))
 
+-- (FIXME) We have a separate function to test LSR specifically
+-- because we want to make sure it is hit during conformance testing,
+-- which may not be the case when `Bitfield_cls.ubfm.rand` is used to
+-- generate a small number of test cases.  Once we have conformance
+-- testing running in CI, the volume of tests we'd be running will
+-- eliminate the need to have alias-specific instruction generators.
 partial def Bitfield_cls.lsr.rand : IO (Option (BitVec 32)) := do
   -- Specifically test the assignment that results in LSR
   let sf := ← BitVec.rand 1
@@ -69,7 +76,8 @@ partial def Bitfield_cls.lsr.rand : IO (Option (BitVec 32)) := do
       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?
+       -- 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))
@@ -78,6 +86,7 @@ partial def Bitfield_cls.lsr.rand : IO (Option (BitVec 32)) := do
 def Bitfield_cls.rand : List (IO (Option (BitVec 32))) :=
   [ Bitfield_cls.lsr.rand,
     Bitfield_cls.ubfm.rand ]
+
 ----------------------------------------------------------------------
 
 end DPI

Arm/Insts/DPR/Data_processing_one_source.lean

@@ -0,0 +1,124 @@
+/-
+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
+-/
+-- REV, REV16, REV32
+
+import Arm.Decode
+import Arm.Insts.Common
+
+----------------------------------------------------------------------
+
+namespace DPR
+
+open BitVec
+
+private theorem shiftLeft_ge (x : Nat) (y : Nat) : x ≤ x <<< y := by
+  have h₀ : 0 < 2 ^ y := by
+    simp only [Nat.zero_lt_two, Nat.pow_pos]
+  have h₁ : x ≤ x * 2 ^ y := by
+    apply Nat.le_mul_of_pos_right
+    simp only [h₀]
+  simp only [Nat.mul_one] at h₁
+  simp only [Nat.shiftLeft_eq]
+  exact h₁
+
+private theorem container_size_le_datasize (opc : Nat) (sf : Nat)
+  (h₀ : opc ≥ 0) (h₁ : opc < 4) (h₃ : ¬(opc = 3 ∧ sf = 0)) :
+  8 <<< opc ≤ 32 <<< sf := by
+  have H1 : 8 = 2 ^ 3 := by decide
+  have H2 : 32 = 2 ^ 5 := by decide
+  have H3 : 3 + opc ≤ 5 + sf := by omega
+  simp only [Nat.shiftLeft_eq, H1, H2, ← Nat.pow_add]
+  refine Nat.pow_le_pow_right ?ha H3
+  decide
+
+private theorem container_size_dvd_datasize (opc : Nat) (sf : Nat)
+  (h₀ : opc ≥ 0) (h₁ : opc < 4) (h₃ : ¬(opc = 3 ∧ sf = 0)):
+  (8 <<< opc ∣ 32 <<< sf) := by
+  have H1 : 8 = 2 ^ 3 := by decide
+  have H2 : 32 = 2 ^ 5 := by decide
+  have H3 : 3 + opc ≤ 5 + sf := by omega
+  simp only [Nat.shiftLeft_eq, H1, H2, ← Nat.pow_add]
+  apply Nat.pow_dvd_pow_iff_le_right'.mpr H3
+
+private theorem opc_and_sf_constraint (x : BitVec 2) (y : BitVec 1)
+  (h : ¬(x == 0b11#2 && y == 0b0#1) ) :
+  ¬(x.toNat = 3 ∧ y.toNat = 0) := by
+  revert h
+  simp only [BitVec.toNat_eq_nat]
+  have h₁ : 3 < 2 ^ 2 := by decide
+  simp [h₁]
+
+@[simp]
+def exec_data_processing_rev
+  (inst : Data_processing_one_source_cls) (s : ArmState) : ArmState :=
+  have H₀: 1 - 0 + 1 = 2 := by decide
+  let opc := H₀ ▸ extractLsb 1 0 inst.opcode
+  if H₁ : opc == 0b11#2 && inst.sf == 0b0#1 then
+    write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  else
+    let datasize := 32 <<< inst.sf.toNat
+    let container_size := 8 <<< opc.toNat
+    let operand := read_gpr_zr datasize inst.Rn s
+    let esize := 8
+    have opc_h₁ : opc.toNat ≥ 0 := by simp only [ge_iff_le, Nat.zero_le]
+    have opc_h₂ : opc.toNat < 4 := by      
+      refine BitVec.isLt (extractLsb 1 0 inst.opcode)
+    have opc_sf_h : ¬(opc.toNat = 3 ∧ inst.sf.toNat = 0) := by
+      apply opc_and_sf_constraint (extractLsb 1 0 inst.opcode) inst.sf H₁
+    have h₀ : 0 < esize := by native_decide
+    have h₁ : esize ≤ container_size := by apply shiftLeft_ge
+    have h₂ : container_size ≤ datasize := by
+      apply container_size_le_datasize opc.toNat inst.sf.toNat opc_h₁ opc_h₂ opc_sf_h
+    have h₃ : esize ∣ container_size := by
+      simp only [esize, container_size]
+      generalize BitVec.toNat (extractLsb 1 0 inst.opcode) = x
+      simp only [Nat.shiftLeft_eq]
+      generalize 2 ^ x = n
+      simp only [Nat.dvd_mul_right]
+    have h₄ : container_size ∣ datasize := by
+      apply container_size_dvd_datasize opc.toNat inst.sf.toNat opc_h₁ opc_h₂ opc_sf_h
+    let result := rev_vector datasize container_size esize operand h₀ h₁ h₂ h₃ h₄
+    -- State Updates
+    let s := write_gpr_zr datasize inst.Rd result s
+    let s := write_pc ((read_pc s) + 4#64) s
+    s
+
+@[simp]
+def exec_data_processing_one_source
+  (inst : Data_processing_one_source_cls) (s : ArmState) : ArmState :=
+  match inst.sf, inst.S, inst.opcode2, inst.opcode with
+  | 0#1, 0#1, 0b00000#5, 0b000001#6 -- REV16 - 32-bit
+  | 0#1, 0#1, 0b00000#5, 0b000010#6 -- REV - 32-bit
+  | 1#1, 0#1, 0b00000#5, 0b000001#6 -- REV16 - 64-bit
+  | 1#1, 0#1, 0b00000#5, 0b000010#6 -- REV32
+  | 1#1, 0#1, 0b00000#5, 0b000011#6 -- REV - 64-bit
+    => exec_data_processing_rev inst s
+  | _, _, _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
+
+----------------------------------------------------------------------
+
+partial def Data_processing_one_source_cls.rev_all.rand : IO (Option (BitVec 32)) := do
+  let opc := ← BitVec.rand 2
+  let sf := ← BitVec.rand 1
+  -- When opc == 0b00#2, inst is instruction RBIT, RBIT is not modeled currently
+  if opc == 0b00#2 || opc == 0b11#2 && sf == 0b0#1 then
+    Data_processing_one_source_cls.rev_all.rand
+  else
+    let (inst : Data_processing_one_source_cls) :=
+      { sf := sf,
+        S := 0b0#1,
+        opcode2 := 0b00000#5,
+        opcode := 0b0000#4 ++ opc,
+        Rn := ← BitVec.rand 5,
+        Rd := ← BitVec.rand 5
+      }
+    pure (some (inst.toBitVec32))
+
+/-- Generate random instructions of Data_processing_one_source_cls class. -/
+def Data_processing_one_source_cls.rand : IO (Option (BitVec 32)) :=
+  Data_processing_one_source_cls.rev_all.rand
+
+end DPR

Arm/Insts/DPR/Insts.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 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.Logical_shifted_reg
 
 /-- List of functions to generate random instructions of the
@@ -14,4 +15,5 @@ def DPR.rand : List (IO (Option (BitVec 32))) :=
   [DPR.Add_sub_carry_cls.rand,
    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]