Address review

leanprover · Mar 18, 2024 · 057fc94 · 057fc94
1 parent 9ddffd7
commit 057fc94
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 19 deletions.
diff --git a/Arm/Decode.lean b/Arm/Decode.lean
@@ -107,6 +107,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst :=
   | [0, Q:1, op:1, 0111100000, a:1, b:1, c:1, cmode:4, o2:1, 1, d:1, e:1, f:1, g:1, h:1, Rd:5] =>
     DPSFP (Advanced_simd_modified_immediate {Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd})
   -- Note: Advanced SIMD shift by immediate constraint immh != 0000
+  -- An instruction will be matched against `Advanced_simd_modified_immediate` first,
+  -- if it doesn't match, then we know immh can't be 0b0000#4
   | [0, Q:1, U:1, 011110, immh:4, immb:3, opcode:5, 1, Rn:5, Rd:5] =>
     DPSFP (Advanced_simd_shift_by_immediate {Q, U, immh, immb, opcode, Rn, Rd})
   | [01, U:1, 111110, immh:4, immb:3, opcode:5, 1, Rn:5, Rd:5] =>

diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
@@ -370,7 +370,7 @@ def elem_set (vector : BitVec n) (e : Nat) (size : Nat)
 
 ----------------------------------------------------------------------
 
--- Field unsigned, round and accumulate are optional for left shifts
+-- Field unsigned, round and accumulate are not used in left shifts
 structure ShiftInfo where
   esize : Nat
   elements : Nat

diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_shift_by_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_shift_by_immediate.lean
@@ -63,15 +63,16 @@ def exec_shl_scalar
 def exec_advanced_simd_scalar_shift_by_immediate
   (inst : Advanced_simd_scalar_shift_by_immediate_cls) (s : ArmState) : ArmState :=
   match inst.U, inst.opcode with
-  | 0b0#1, 0b01010#5 => exec_shl_scalar inst s
-  | 0b0#1, 0b00000#5
-  | 0b0#1, 0b00010#5
-  | 0b0#1, 0b00100#5
-  | 0b0#1, 0b00110#5
-  | 0b1#1, 0b00000#5
-  | 0b1#1, 0b00010#5
-  | 0b1#1, 0b00100#5
-  | 0b1#1, 0b00110#5 => exec_shift_right_scalar inst s
+  | 0b0#1, 0b01010#5 => exec_shl_scalar inst s    -- SHL
+  | 0b0#1, 0b00000#5                              -- SSHR
+  | 0b0#1, 0b00010#5                              -- SSRA
+  | 0b0#1, 0b00100#5                              -- SRSHR
+  | 0b0#1, 0b00110#5                              -- SRSRA
+  | 0b1#1, 0b00000#5                              -- USHR
+  | 0b1#1, 0b00010#5                              -- USRA
+  | 0b1#1, 0b00100#5                              -- URSHR
+  | 0b1#1, 0b00110#5                              -- URSRA
+    => exec_shift_right_scalar inst s
   | _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
 
 ----------------------------------------------------------------------

diff --git a/Arm/Insts/DPSFP/Advanced_simd_shift_by_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_shift_by_immediate.lean
@@ -70,15 +70,16 @@ def exec_advanced_simd_shift_by_immediate
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
     match inst.U, inst.opcode with
-    | 0b0#1, 0b01010#5 => exec_shl_vector inst s
-    | 0b0#1, 0b00000#5
-    | 0b0#1, 0b00010#5
-    | 0b0#1, 0b00100#5
-    | 0b0#1, 0b00110#5
-    | 0b1#1, 0b00000#5
-    | 0b1#1, 0b00010#5
-    | 0b1#1, 0b00100#5
-    | 0b1#1, 0b00110#5 => exec_shift_right_vector inst s
+    | 0b0#1, 0b01010#5 => exec_shl_vector inst s    -- SHL
+    | 0b0#1, 0b00000#5                              -- SSHR
+    | 0b0#1, 0b00010#5                              -- SSRA
+    | 0b0#1, 0b00100#5                              -- SRSHR
+    | 0b0#1, 0b00110#5                              -- SRSRA
+    | 0b1#1, 0b00000#5                              -- USHR
+    | 0b1#1, 0b00010#5                              -- USRA
+    | 0b1#1, 0b00100#5                              -- URSHR
+    | 0b1#1, 0b00110#5                              -- URSRA
+      => exec_shift_right_vector inst s
     | _, _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
 
 ----------------------------------------------------------------------