Adding MADD (32- and 64-bit) (alias MUL) to instructions (leanprover#67)

### Description: Adding support for MADD (32- and 64-bit) instructions. MUL is an alias. ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? _**HAVE NOT RUN CONFORMANCE**_ ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Co-authored-by: Nathan Wetzler <wetznath@amazon.com>
pennyannn · Aug 8, 2024 · 7b2229d · 7b2229d
1 parent 345fd27
commit 7b2229d
Show file tree

Hide file tree

Showing 5 changed files with 122 additions and 1 deletion.
diff --git a/Arm/Decode.lean b/Arm/Decode.lean
@@ -85,6 +85,8 @@ def decode_data_proc_reg (i : BitVec 32) : Option ArmInst :=
     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})
+  | [sf:1, op54:2, 11011, op31:3, Rm:5, o0:1, Ra:5, Rn:5, Rd:5] =>
+    DPR (Data_processing_three_source {sf, op54, op31, Rm, o0, Ra, Rn, Rd})
   | _ => none
 
 def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst :=

diff --git a/Arm/Decode/DPR.lean b/Arm/Decode/DPR.lean
@@ -115,6 +115,23 @@ 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_three_source_cls where
+  sf     : BitVec 1                 -- [31:31]
+  op54   : BitVec 2                 -- [30:29]
+  _fixed : BitVec 5 := 0b11011#5    -- [28:24]
+  op31   : BitVec 3                 -- [23:21]
+  Rm     : BitVec 5                 -- [20:16]
+  o0     : BitVec 1                 -- [15:15]
+  Ra     : BitVec 5                 -- [14:10]
+  Rn     : BitVec 5                 --   [9:5]
+  Rd     : BitVec 5                 --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Data_processing_three_source_cls where toString a := toString (repr a)
+
+def Data_processing_three_source_cls.toBitVec32 (x : Data_processing_three_source_cls) : BitVec 32 :=
+  x.sf ++ x.op54 ++ x._fixed ++ x.op31 ++ x.Rm ++ x.o0 ++ x.Ra ++ x.Rn ++ x.Rd
+
 inductive DataProcRegInst where
   | Add_sub_carry :
     Add_sub_carry_cls → DataProcRegInst
@@ -128,6 +145,8 @@ inductive DataProcRegInst where
     Data_processing_two_source_cls → DataProcRegInst
   | Logical_shifted_reg :
     Logical_shifted_reg_cls → DataProcRegInst
+  | Data_processing_three_source :
+    Data_processing_three_source_cls → DataProcRegInst
 deriving DecidableEq, Repr
 
 instance : ToString DataProcRegInst where toString a := toString (repr a)

diff --git a/Arm/Exec.lean b/Arm/Exec.lean
@@ -44,6 +44,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
     DPR.exec_data_processing_two_source i s
   | DPR (DataProcRegInst.Logical_shifted_reg i) =>
     DPR.exec_logical_shifted_reg i s
+  | DPR (DataProcRegInst.Data_processing_three_source i) =>
+    DPR.exec_data_processing_three_source i s
 
   | DPSFP (DataProcSFPInst.Advanced_simd_copy i) =>
     DPSFP.exec_advanced_simd_copy i s

diff --git a/Arm/Insts/DPR/Data_processing_three_source.lean b/Arm/Insts/DPR/Data_processing_three_source.lean
@@ -0,0 +1,96 @@
+/-
+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): Nathan Wetzler
+-/
+-- MADD, MSUB (32-, 64-bit); SMADDL, SMSUBL, SMULH, UMADDL, UMSUBL, UMULH
+
+import Arm.Decode
+import Arm.Insts.Common
+
+----------------------------------------------------------------------
+
+namespace DPR
+
+open BitVec
+
+@[state_simp_rules]
+def exec_data_processing_madd
+  (inst : Data_processing_three_source_cls) (s : ArmState) : ArmState :=
+  let destsize := 32 <<< inst.sf.toNat
+  let operand1 := read_gpr_zr destsize inst.Rn s
+  let operand2 := read_gpr_zr destsize inst.Rm s
+  let operand3 := read_gpr_zr destsize inst.Ra s
+  -- let result := BitVec.add operand3 (BitVec.mul operand1 operand2)
+  let result := operand3 + (operand1 * operand2)
+  -- State Update
+  let s := write_gpr_zr destsize inst.Rd result s
+  let s := write_pc ((read_pc s) + 4#64) s
+  s
+
+@[state_simp_rules]
+def exec_data_processing_three_source
+  (inst : Data_processing_three_source_cls) (s : ArmState) : ArmState :=
+  let (illegal, unimplemented) :=
+    match inst.sf, inst.op54, inst.op31, inst.o0 with
+    | _, 0b00#2, 0b010#3, 0b1#1
+    | _, 0b00#2, 0b011#3, _
+    | _, 0b00#2, 0b100#3, _
+    | _, 0b00#2, 0b110#3, 0b1#1
+    | _, 0b00#2, 0b111#3, _
+    | _, 0b01#2, _, _
+    | _, 0b10#2, _, _
+    | _, 0b11#2, _, _
+      => (true, false) -- Unallocated
+    | 0b0#1, 0b00#2, 0b000#3, 0b0#1 => (false, false) -- MADD (32-bit)
+    | 0b0#1, 0b00#2, 0b000#3, 0b1#1 => (false, true)  -- MSUB (32-bit)
+    | 0b0#1, 0b00#2, 0b001#3, 0b0#1
+    | 0b0#1, 0b00#2, 0b001#3, 0b1#1
+    | 0b0#1, 0b00#2, 0b010#3, 0b0#1
+    | 0b0#1, 0b00#2, 0b101#3, 0b0#1
+    | 0b0#1, 0b00#2, 0b101#3, 0b1#1
+    | 0b0#1, 0b00#2, 0b110#3, 0b0#1
+      => (true, false) -- Unallocated
+    | 0b1#1, 0b00#2, 0b000#3, 0b0#1 => (false, false) -- MADD (64-bit)
+    | 0b1#1, 0b00#2, 0b000#3, 0b1#1 => (false, true)  -- MSUB (64-bit)
+    | 0b1#1, 0b00#2, 0b001#3, 0b0#1 => (false, true)  -- SMADDL
+    | 0b1#1, 0b00#2, 0b001#3, 0b1#1 => (false, true)  -- SMSUBL
+    | 0b1#1, 0b00#2, 0b010#3, 0b0#1 => (false, true)  -- SMULH
+    | 0b1#1, 0b00#2, 0b101#3, 0b0#1 => (false, true)  -- UMADDL
+    | 0b1#1, 0b00#2, 0b101#3, 0b1#1 => (false, true)  -- UMSUBL
+    | 0b1#1, 0b00#2, 0b110#3, 0b0#1 => (false, true)  -- UMULH
+    | _, _, _, _ => (true, false)
+  if illegal then
+    write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  else if unimplemented then
+    write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
+  else
+    match inst.sf, inst.op54, inst.op31, inst.o0 with
+    | 0b0#1, 0b00#2, 0b000#3, 0b0#1 => exec_data_processing_madd inst s -- MADD (32-bit)
+    | 0b1#1, 0b00#2, 0b000#3, 0b0#1 => exec_data_processing_madd inst s -- MADD (64-bit)
+    | _, _, _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
+
+----------------------------------------------------------------------
+
+def Data_processing_three_source_cls.shift.rand
+  (sf : BitVec 1) (op54 : BitVec 2) (op31 : BitVec 3) (o0 : BitVec 1)
+  : IO (Option (BitVec 32)) := do
+  let (inst : Data_processing_three_source_cls) :=
+    { sf := sf,
+      op54 := op54,
+      op31 := op31,
+      Rm := ← BitVec.rand 5,
+      o0 := o0,
+      Ra := ← BitVec.rand 5,
+      Rn := ← BitVec.rand 5,
+      Rd := ← BitVec.rand 5
+    }
+  pure (some inst.toBitVec32)
+
+/-- Generate random instructions of Data_processing_three_source_cls class. -/
+def Data_processing_three_source_cls.rand : List (IO (Option (BitVec 32))) :=
+  [ Data_processing_three_source_cls.shift.rand 0b0#1 0b00#2 0b000#3 0b0#1, -- MADD (32-bit)
+    Data_processing_three_source_cls.shift.rand 0b1#1 0b00#2 0b000#3 0b0#1, -- MADD (64-bit)
+  ]
+
+end DPR
diff --git a/Arm/Insts/DPR/Insts.lean b/Arm/Insts/DPR/Insts.lean
@@ -9,6 +9,7 @@ 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
+import Arm.Insts.DPR.Data_processing_three_source
 
 /-- List of functions to generate random instructions of the
 DPR class. -/
@@ -18,4 +19,5 @@ def DPR.rand : List (IO (Option (BitVec 32))) :=
    DPR.Conditional_select_cls.rand,
    DPR.Data_processing_one_source_cls.rand,
    DPR.Logical_shifted_reg_cls.rand] ++
-  DPR.Data_processing_two_source_cls.rand
+  DPR.Data_processing_two_source_cls.rand ++
+  DPR.Data_processing_three_source_cls.rand