Update LDST (#15)

### Description:

This PR updates LDST, specifically:

1. LDP/STP instructions include pre-indexed, post-indexed and signed
offset with GPR and SIMD/FP at all sizes
2. LDR/STR immediate instructions include post-indexed and unsigned
offset with GPR and SIMD/FP at all sizes
3. LDRB/STRB are newly added
4. In addition, a test file Tests/LDSTTest.lean is introduced to test
the LDST instructions.

Note:

1. Proofs sha512_block_armv8_test_3_sym and
sha512_block_armv8_new_program are sorry'ed.

### Testing:

The `make all` succeeds and conformance testing has been done
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.

---------

Arm/Decode.lean

@@ -112,6 +112,10 @@ def decode_ldst_inst (i : BitVec 32) : Option ArmInst :=
     LDST (Reg_unsigned_imm {size, V, opc, imm12, Rn, Rt})
   | [opc:2, 101, V:1, 011, L:1, imm7:7, Rt2:5, Rn:5, Rt:5] =>
     LDST (Reg_pair_pre_indexed {opc, V, L, imm7, Rt2, Rn, Rt})
+  | [opc:2, 101, V:1, 001, L:1, imm7:7, Rt2:5, Rn:5, Rt:5] =>
+    LDST (Reg_pair_post_indexed {opc, V, L, imm7, Rt2, Rn, Rt})
+  | [opc:2, 101, V:1, 010, L:1, imm7:7, Rt2:5, Rn:5, Rt:5] =>
+    LDST (Reg_pair_signed_offset {opc, V, L, imm7, Rt2, Rn, Rt})
   | [0, Q:1, 0011000, L:1, 000000, opcode:4, size:2, Rn:5, Rt:5] =>
     LDST (Advanced_simd_multiple_struct {Q, L, opcode, size, Rn, Rt})
   | [0, Q:1, 0011001, L:1, 0, Rm:5, opcode:4, size:2, Rn:5, Rt:5] =>

Arm/Decode/LDST.lean

@@ -1,7 +1,7 @@
 /-
 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
+Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
 
@@ -55,6 +55,34 @@ deriving DecidableEq, Repr
 
 instance : ToString Reg_pair_pre_indexed_cls where toString a := toString (repr a)
 
+structure Reg_pair_post_indexed_cls where
+  opc     : BitVec 2            -- [31:30]
+  _fixed1 : BitVec 3 := 0b101#3 -- [29:27]
+  V       : BitVec 1            -- [26:26]
+  _fixed2 : BitVec 3 := 0b001#3 -- [25:23]
+  L       : BitVec 1            -- [22:22]
+  imm7    : BitVec 7            -- [21:15]
+  Rt2     : BitVec 5            -- [14:10]
+  Rn      : BitVec 5            --   [9:5]
+  Rt      : BitVec 5            --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Reg_pair_post_indexed_cls where toString a := toString (repr a)
+
+structure Reg_pair_signed_offset_cls where
+  opc     : BitVec 2            -- [31:30]
+  _fixed1 : BitVec 3 := 0b101#3 -- [29:27]
+  V       : BitVec 1            -- [26:26]
+  _fixed2 : BitVec 3 := 0b010#3 -- [25:23]
+  L       : BitVec 1            -- [22:22]
+  imm7    : BitVec 7            -- [21:15]
+  Rt2     : BitVec 5            -- [14:10]
+  Rn      : BitVec 5            --   [9:5]
+  Rt      : BitVec 5            --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Reg_pair_signed_offset_cls where toString a := toString (repr a)
+
 structure Advanced_simd_multiple_struct_cls where
   _fixed1 : BitVec 1 := 0b0#1       -- [31:31]
   Q       : BitVec 1                -- [30:30]
@@ -70,16 +98,16 @@ deriving DecidableEq, Repr
 instance : ToString Advanced_simd_multiple_struct_cls where toString a := toString (repr a)
 
 structure Advanced_simd_multiple_struct_post_indexed_cls where
-  _fixed1 : BitVec 1 := 0b0#1     -- [31:31]
-  Q       : BitVec 1              -- [30:30]
-  _fixed2 : BitVec 7 := 0011001#7 -- [29:23]
-  L       : BitVec 1              -- [22:22]
-  _fixed3 : BitVec 1 := 0b0#1     -- [21:21]
-  Rm      : BitVec 5              -- [20:16]
-  opcode  : BitVec 4              -- [15:12]
-  size    : BitVec 2              -- [11:10]
-  Rn      : BitVec 5              --   [9:5]
-  Rt      : BitVec 5              --   [4:0]
+  _fixed1 : BitVec 1 := 0b0#1       -- [31:31]
+  Q       : BitVec 1                -- [30:30]
+  _fixed2 : BitVec 7 := 0b0011001#7 -- [29:23]
+  L       : BitVec 1                -- [22:22]
+  _fixed3 : BitVec 1 := 0b0#1       -- [21:21]
+  Rm      : BitVec 5                -- [20:16]
+  opcode  : BitVec 4                -- [15:12]
+  size    : BitVec 2                -- [11:10]
+  Rn      : BitVec 5                --   [9:5]
+  Rt      : BitVec 5                --   [4:0]
 deriving DecidableEq, Repr
 
 instance : ToString Advanced_simd_multiple_struct_post_indexed_cls where toString a := toString (repr a)
@@ -91,6 +119,10 @@ inductive LDSTInst where
     Reg_unsigned_imm_cls → LDSTInst
   | Reg_pair_pre_indexed :
     Reg_pair_pre_indexed_cls → LDSTInst
+  | Reg_pair_post_indexed :
+    Reg_pair_post_indexed_cls → LDSTInst
+  | Reg_pair_signed_offset :
+    Reg_pair_signed_offset_cls → LDSTInst
   | Advanced_simd_multiple_struct :
     Advanced_simd_multiple_struct_cls → LDSTInst
   | Advanced_simd_multiple_struct_post_indexed :

Arm/Exec.lean

@@ -52,9 +52,13 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
   | LDST (LDSTInst.Reg_imm_post_indexed i) =>
     LDST.exec_reg_imm_post_indexed i s
   | LDST (LDSTInst.Reg_unsigned_imm i) =>
-    LDST.exec_reg_unsigned_imm i s
+    LDST.exec_reg_imm_unsigned_offset i s
   | LDST (LDSTInst.Reg_pair_pre_indexed i) =>
     LDST.exec_reg_pair_pre_indexed i s
+  | LDST (LDSTInst.Reg_pair_post_indexed i) =>
+    LDST.exec_reg_pair_post_indexed i s
+  | LDST (LDSTInst.Reg_pair_signed_offset i) =>
+    LDST.exec_reg_pair_signed_offset i s
   | LDST (LDSTInst.Advanced_simd_multiple_struct i) =>
     LDST.exec_advanced_simd_multiple_struct i s
   | LDST (LDSTInst.Advanced_simd_multiple_struct_post_indexed i) =>

Arm/Insts/Common.lean

@@ -202,4 +202,16 @@ def Vpart (n : BitVec 5) (part : Nat) (width : Nat) (s : ArmState) (H : width >
     -- assert width IN {32,64};
     h2 ▸ extractLsb (width*2-1) width $ read_sfp 128 n s
 
+----------------------------------------------------------------------
+
+@[simp]
+def ldst_read (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (s : ArmState)
+  : BitVec width :=
+  if SIMD? then read_sfp width idx s else read_gpr width idx s
+
+@[simp]
+def ldst_write (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (val : BitVec width) (s : ArmState)
+  : ArmState :=
+  if SIMD? then write_sfp width idx val s else write_gpr width idx val s
+
 end Common

Arm/Insts/LDST/Reg_imm.lean

@@ -1,9 +1,10 @@
 /-
 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
+Author(s): Shilpi Goel, Yan Peng
 -/
--- LDR/STR (immediate, SIMD&FP)
+-- LDR/STR (immediate, post-indexed and unsigned offset, GPR and SIMD&FP)
+-- LDRB/STRB (immediate, post-indexed and unsigned offset, GPR)
 
 import Arm.Decode
 import Arm.Insts.Common
@@ -14,11 +15,25 @@ namespace LDST
 
 open Std.BitVec
 
+structure Reg_imm_cls where
+  size      : BitVec 2
+  opc       : BitVec 2
+  Rn        : BitVec 5
+  Rt        : BitVec 5
+  SIMD?     : Bool
+  wback     : Bool
+  postindex : Bool
+  imm       : BitVec 12 ⊕ (BitVec 9)
+deriving DecidableEq, Repr
+
+instance : ToString Reg_imm_cls where toString a := toString (repr a)
+
 @[simp]
 def reg_imm_operation (inst_str : String) (op : BitVec 1)
-  (wback : Bool) (postindex : Bool) (datasize : Nat)
-  (Rn : BitVec 5) (Rt : BitVec 5) (offset : BitVec 64)
-  (s : ArmState)  (H : 8 ∣ datasize) : ArmState :=
+  (wback : Bool) (postindex : Bool) (SIMD? : Bool)
+  (datasize : Nat) (regsize : Option Nat) (Rn : BitVec 5)
+  (Rt : BitVec 5) (offset : BitVec 64) (s : ArmState)
+  (H : 8 ∣ datasize) : ArmState :=
   let address := read_gpr 64 Rn s
   if Rn == 31#5 && not (CheckSPAlignment s) then
       write_err (StateError.Fault s!"[Inst: {inst_str}] SP {address} is not aligned!") s
@@ -32,64 +47,97 @@ def reg_imm_operation (inst_str : String) (op : BitVec 1)
     let s :=
       match op with
       | 0#1 => -- STORE
-        let data := read_sfp datasize Rt s
+        let data := ldst_read SIMD? datasize Rt s
         write_mem_bytes (datasize / 8) address (h.symm ▸ data) s
       | _ => -- LOAD
         let data := read_mem_bytes (datasize / 8) address s
-        write_sfp datasize Rt (h.symm ▸ data) s
+        if SIMD? then write_sfp datasize Rt (h.symm ▸ data) s
+        else write_gpr regsize.get! Rt (zeroExtend regsize.get! data) s
     if wback then
       let address := if postindex then address + offset else address
       write_gpr 64 Rn address s
     else
       s
 
 @[simp]
-def exec_reg_unsigned_imm
-  (inst : Reg_unsigned_imm_cls) (s : ArmState) : ArmState :=
-  -- Decoding for all variants for post-indexed encoding:
-  let wback := false
-  let postindex := false
-  have h_scale : (1 - 1 + 1 + 2) = 3 := by decide
-  let scale := (extractLsb 1 1 inst.opc) ++ inst.size
-  let scale := (h_scale ▸ scale)
-  -- (FIXME) Why can't I use scale > 4#3 here?
-  if Std.BitVec.ult 4#3 scale then
-    write_err (StateError.Illegal "Illegal instruction {inst} encountered!") s
+def reg_imm_constrain_unpredictable (wback : Bool) (SIMD? : Bool) (Rn : BitVec 5)
+  (Rt : BitVec 5) : Bool :=
+  if SIMD? then false else wback && Rn == Rt && Rn != 31#5
+
+@[simp]
+def supported_reg_imm (size : BitVec 2) (opc : BitVec 2) (SIMD? : Bool) : Bool :=
+  match size, opc, SIMD? with
+  | 0b00#2, 0b00#2, false => true -- STRB, 32-bit, GPR
+  | 0b00#2, 0b01#2, false => true -- LDRB, 32-bit, GPR
+  | 0b10#2, 0b00#2, false => true -- STR, 32-bit, GPR
+  | 0b10#2, 0b01#2, false => true -- LDR, 32-bit, GPR
+  | 0b11#2, 0b00#2, false => true -- STR, 64-bit, GPR
+  | 0b11#2, 0b01#2, false => true -- LDR, 64-bit, GPR
+  | _, 0b00#2, true => true      -- STR, 8-bit, 16-bit, 32-bit, 64-bit, SIMD&FP
+  | _, 0b01#2, true => true      -- LDR, 8-bit, 16-bit, 32-bit, 64-bit, SIMD&FP
+  | 0b00#2, 0b10#2, true => true -- STR, 128-bit, SIMD&FP
+  | 0b00#2, 0b11#2, true => true -- LDR, 128-bit, SIMD&FP
+  | _, _, _ => false -- other instructions that are not supported or illegal
+
+@[simp]
+def exec_reg_imm_common
+  (inst : Reg_imm_cls) (inst_str : String) (s : ArmState) : ArmState :=
+  let scale :=
+    if inst.SIMD? then ((extractLsb 1 1 inst.opc) ++ inst.size).toNat
+    else inst.size.toNat
+  -- Only allow supported LDST Reg immediate instructions
+  if not $ supported_reg_imm inst.size inst.opc inst.SIMD? then
+    write_err (StateError.Illegal "Unsupported or Illegal instruction {inst_str} encountered!") s
+  -- UNDEFINED case in LDR/STR SIMD/FP instructions
+  -- FIXME: prove that this branch condition is trivially false
+  else if inst.SIMD? && scale > 4 then
+    write_err (StateError.Illegal "Illegal instruction {inst_str} encountered!") s
+  -- constrain unpredictable when GPR
+  else if reg_imm_constrain_unpredictable inst.wback inst.SIMD? inst.Rn inst.Rt then
+    write_err (StateError.Illegal "Illegal instruction {inst_str} encountered!") s
   else
-    let offset := (Std.BitVec.zeroExtend 64 inst.imm12) <<< scale.toNat
-    let datasize := 8 <<< scale.toNat
+    let offset := match inst.imm with
+      | Sum.inl imm12 => (Std.BitVec.zeroExtend 64 imm12) <<< scale
+      | Sum.inr imm9 => signExtend 64 imm9
+    let datasize := 8 <<< scale
+    let regsize :=
+      if inst.SIMD? then none
+      else if inst.size == 0b11#2 then some 64 else some 32
     have H : 8 ∣ datasize := by
       simp_all! only [Nat.shiftLeft_eq, dvd_mul_right]
     -- State Updates
-    let s' := reg_imm_operation s!"{inst}"
-              (extractLsb 0 0 inst.opc) wback postindex datasize
-              inst.Rn inst.Rt offset
-              s (H)
+    let s' := reg_imm_operation inst_str
+              (extractLsb 0 0 inst.opc) inst.wback inst.postindex
+              inst.SIMD? datasize regsize inst.Rn inst.Rt offset s (H)
     let s' := write_pc ((read_pc s) + 4#64) s'
     s'
 
+@[simp]
+def exec_reg_imm_unsigned_offset
+  (inst : Reg_unsigned_imm_cls) (s : ArmState) : ArmState :=
+  let (extracted_inst : Reg_imm_cls) :=
+    { size      := inst.size,
+      opc       := inst.opc,
+      Rn        := inst.Rn,
+      Rt        := inst.Rt,
+      SIMD?     := inst.V == 1#1,
+      wback     := false,
+      postindex := false,
+      imm       := Sum.inl inst.imm12 }
+  exec_reg_imm_common extracted_inst s!"{inst}" s
+
 @[simp]
 def exec_reg_imm_post_indexed
   (inst : Reg_imm_post_indexed_cls) (s : ArmState) : ArmState :=
-  -- Decoding for all variants for post-indexed encoding:
-  open Std.BitVec in
-  let wback := true
-  let postindex := true
-  let scale := (extractLsb 1 1 inst.opc) ++ inst.size
-  -- (FIXME) Why can't I use scale > 4#3 here?
-  if Std.BitVec.ult 4#3 scale then
-    write_err (StateError.Illegal "Illegal instruction {inst} encountered!") s
-  else
-    let datasize := 8 <<< scale.toNat
-    let offset := signExtend 64 inst.imm9
-    have H : 8 ∣ datasize := by
-      simp_all! only [Nat.shiftLeft_eq, dvd_mul_right]
-    -- State Updates
-    let s' := reg_imm_operation s!"{inst}"
-              (extractLsb 0 0 inst.opc) wback postindex datasize
-              inst.Rn inst.Rt offset
-              s (H)
-    let s' := write_pc ((read_pc s) + 4#64) s'
-    s'
+  let (extracted_inst : Reg_imm_cls) :=
+    { size      := inst.size,
+      opc       := inst.opc,
+      Rn        := inst.Rn,
+      Rt        := inst.Rt,
+      SIMD?     := inst.V == 1#1,
+      wback     := true,
+      postindex := true,
+      imm       := Sum.inr inst.imm9 }
+  exec_reg_imm_common extracted_inst s!"{inst}" s
 
 end LDST