leanprover · shigoel · Mar 8, 2024 · Feb 29, 2024
@@ -106,6 +106,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst :=
     DPSFP (Advanced_simd_modified_immediate {Q, op, a, b, c, cmode, o2, d, e, f, g, h, 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] =>
+    DPSFP (Advanced_simd_table_lookup {Q, op2, Rm, len, op, Rn, Rd})
   | [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:5, 1, Rn:5, Rd:5] =>
     DPSFP (Advanced_simd_three_same {Q, U, size, Rm, opcode, Rn, Rd})
   | [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:4, 00, Rn:5, Rd:5] =>

@@ -184,6 +184,26 @@ 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_table_lookup_cls where
+  _fixed1 : BitVec 1 := 0b0#1      -- [31:31]
+  Q       : BitVec 1               -- [30:30]
+  _fixed2 : BitVec 6 := 0b001110#6 -- [29:24]
+  op2     : BitVec 2               -- [23:22]
+  _fixed3 : BitVec 1 := 0b0#1      -- [21:21]
+  Rm      : BitVec 5               -- [20:16]
+  _fixed4 : BitVec 1 := 0b0#1      -- [15:15]
+  len     : BitVec 2               -- [14:13]
+  op      : BitVec 1               -- [12:12]
+  _fixed5 : BitVec 2 := 0b00#2     -- [11:10]
+  Rn      : BitVec 5               --   [9:5]
+  Rd      : BitVec 5               --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Advanced_simd_table_lookup_cls where toString a := toString (repr a)
+
+def Advanced_simd_table_lookup_cls.toBitVec32 (x : Advanced_simd_table_lookup_cls) : BitVec 32 :=
+  x._fixed1 ++ x.Q ++ x._fixed2 ++ x.op2 ++ x._fixed3 ++ x.Rm ++ x._fixed4 ++ x.len ++ x.op ++ x._fixed5 ++ x.Rn ++ x.Rd
+
 structure Advanced_simd_three_same_cls where
   _fixed1 : BitVec 1 := 0b0#1      -- [31:31]
   Q       : BitVec 1               -- [30:30]
@@ -262,6 +282,8 @@ inductive DataProcSFPInst where
     Advanced_simd_modified_immediate_cls → DataProcSFPInst
   | Advanced_simd_scalar_copy :
     Advanced_simd_scalar_copy_cls → DataProcSFPInst
+  | Advanced_simd_table_lookup :
+    Advanced_simd_table_lookup_cls → DataProcSFPInst
   | Advanced_simd_three_same :
     Advanced_simd_three_same_cls → DataProcSFPInst
   | Advanced_simd_three_different :

@@ -58,6 +58,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
     DPSFP.exec_advanced_simd_modified_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) =>
+    DPSFP.exec_advanced_simd_table_lookup i s
   | DPSFP (DataProcSFPInst.Advanced_simd_three_same i) =>
     DPSFP.exec_advanced_simd_three_same i s
   | DPSFP (DataProcSFPInst.Advanced_simd_three_different i) =>

@@ -127,7 +127,7 @@ def exec_advanced_simd_copy
   | [_Q:1, 0, _imm5:5, 0111] => exec_smov_umov inst s false
   | [1, 0, _imm5:5, 0011] => exec_ins_general inst s
   | [1, 1, _imm5:5, _imm4:4] => exec_ins_element inst s
-  | _ => write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  | _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
 
 ----------------------------------------------------------------------
 

@@ -0,0 +1,93 @@
+/-
+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
+-/
+-- TBL and TBX (Single, Two, Three, Four register table)
+
+import Arm.Decode
+import Arm.Insts.Common
+
+----------------------------------------------------------------------
+
+namespace DPSFP
+
+open Std.BitVec
+
+@[simp]
+def create_table (i : Nat) (regs : Nat) (Rn : BitVec 5) (table : BitVec (128 * regs))
+  (s : ArmState) : BitVec (128 * regs) :=
+  if h₀ : regs <= i then
+    table
+  else
+    let val := read_sfp 128 Rn s
+    have h₁ : 128 = 128 * i + 127 - 128 * i + 1 := by omega
+    let table := BitVec.partInstall (128 * i + 127) (128 * i) (h₁ ▸ val) table
+    let Rn := (Rn + 1) % 32
+    have h₂ : regs - (i + 1) < regs - i := by omega
+    create_table (i + 1) regs Rn table s
+  termination_by create_table i regs Rn table s => (regs - i)
+
+@[simp]
+def tblx_aux (i : Nat) (elements : Nat) (indices : BitVec datasize)
+  (regs : Nat) (table : BitVec (128 * regs)) (result: BitVec datasize)
+  : BitVec datasize :=
+  if h₀ : elements <= i then
+    result
+  else
+    have h₁ : 8 > 0 := by decide
+    let index := (elem_get indices i 8 h₁).toNat
+    let result := 
+      if index < 16 * regs then
+        let val := elem_get table index 8 h₁
+        elem_set result i 8 val h₁
+      else
+        result
+    have h₂ : elements - (i + 1) < elements - i := by omega
+    tblx_aux (i + 1) elements indices regs table result
+  termination_by tblx_aux i elements indices regs table result => (elements - i)
+
+@[simp]
+def exec_tblx (inst : Advanced_simd_table_lookup_cls) (s : ArmState) : ArmState :=
+  let datasize := 64 <<< inst.Q.toNat
+  let elements := datasize / 8
+  let regs := inst.len.toNat + 1
+  let is_tbl := (inst.op == 0b0#1)
+  let indices := read_sfp datasize inst.Rm s
+  let table := Std.BitVec.zero (128 * regs)
+  let table := create_table 0 regs inst.Rn table s
+  let result := if is_tbl
+                then Std.BitVec.zero datasize
+                else read_sfp datasize inst.Rd s
+  let result := tblx_aux 0 elements indices regs table result
+  -- State Updates
+  let s := write_sfp datasize inst.Rd result s
+  let s := write_pc ((read_pc s) + 4#64) s
+  s
+
+@[simp]
+def exec_advanced_simd_table_lookup
+  (inst : Advanced_simd_table_lookup_cls) (s : ArmState) : ArmState :=
+  if inst.op2 == 0b00#2 then
+    exec_tblx inst s
+  else write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
+
+----------------------------------------------------------------------
+
+def Advanced_simd_table_lookup_cls.tbl.rand : IO (Option (BitVec 32)) := do
+  let (inst : Advanced_simd_table_lookup_cls) :=
+    { Q := ← BitVec.rand 1,
+      op2 := 0b00#2,
+      Rm := ← BitVec.rand 5,
+      len := ← BitVec.rand 2,
+      op := ← BitVec.rand 1,
+      Rn := ← BitVec.rand 5,
+      Rd := ← BitVec.rand 5
+    }
+  pure (some (inst.toBitVec32))
+
+/-- Generate random instructions of Advanced_simd_table_lookup class. -/
+def Advanced_simd_table_lookup_cls.rand : List (IO (Option (BitVec 32))) :=
+  [ Advanced_simd_table_lookup_cls.tbl.rand ]
+
+end DPSFP
@@ -9,6 +9,7 @@ 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_scalar_copy
+import Arm.Insts.DPSFP.Advanced_simd_table_lookup
 import Arm.Insts.DPSFP.Advanced_simd_three_same
 import Arm.Insts.DPSFP.Advanced_simd_three_different
 import Arm.Insts.DPSFP.Crypto_aes
@@ -25,6 +26,7 @@ def DPSFP.rand : List (IO (Option (BitVec 32))) :=
   DPSFP.Advanced_simd_permute_cls.rand ++
   DPSFP.Advanced_simd_modified_immediate_cls.rand ++
   DPSFP.Advanced_simd_scalar_copy_cls.rand ++
+  DPSFP.Advanced_simd_table_lookup_cls.rand ++
   DPSFP.Advanced_simd_three_same_cls.rand ++
   DPSFP.Advanced_simd_three_different_cls.rand ++
   DPSFP.Advanced_simd_two_reg_misc_cls.rand ++