From b083b30563f7a7801192b5b763a6487f7bcb91b4 Mon Sep 17 00:00:00 2001 From: Yan Peng <112029182+pennyannn@users.noreply.github.com> Date: Fri, 1 Mar 2024 14:24:15 -0800 Subject: [PATCH] Add data processing (1 source) class for REV (#21) ### Description: This PR adds support for REV, REV16 and REV32 from the [Data processing (1 source) ](https://developer.arm.com/documentation/ddi0602/2023-12/Index-by-Encoding/Data-Processing----Register?lang=en#dp_1src) class. ### Testing: The `make all` succeeds and conformance testing runs 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 | 16 ++ Arm/Decode/DPR.lean | 20 ++- Arm/Exec.lean | 2 + Arm/Insts/Common.lean | 65 ++++++++ Arm/Insts/DPR/Data_processing_one_source.lean | 143 ++++++++++++++++++ Arm/Insts/DPR/Insts.lean | 2 + .../DPSFP/Advanced_simd_two_reg_misc.lean | 63 -------- Tests/SHA512ProgramTest.lean | 2 +- 8 files changed, 248 insertions(+), 65 deletions(-) create mode 100644 Arm/Insts/DPR/Data_processing_one_source.lean diff --git a/Arm/Decode.lean b/Arm/Decode.lean index 9e2cf372..c0bf2d22 100644 --- a/Arm/Decode.lean +++ b/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 diff --git a/Arm/Decode/DPR.lean b/Arm/Decode/DPR.lean index 4a82dcb9..411f6c3e 100644 --- a/Arm/Decode/DPR.lean +++ b/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,6 +81,22 @@ 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 @@ -88,6 +104,8 @@ inductive DataProcRegInst where 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 diff --git a/Arm/Exec.lean b/Arm/Exec.lean index 631345fe..cf4cd455 100644 --- a/Arm/Exec.lean +++ b/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 diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 2eae3049..9386de7d 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -258,4 +258,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 := Std.BitVec.zeroExtend esize x + let rest_x := Std.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 [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, add_tsub_cancel_of_le, h1] + h3 ▸ (element ++ rest_ans) + termination_by rev_elems n esize x h₀ h₁ => 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 := Std.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 := Std.BitVec.zeroExtend new_datasize (x >>> container_size) + have h₄' : container_size ∣ new_datasize := by + have h : container_size ∣ container_size := by simp + exact Nat.dvd_sub h₂ h₄ h + have h₂' : container_size <= new_datasize := by + refine Nat.le_of_dvd ?h h₄' + simp_all!; exact Ne.lt_of_le' h0 h₂ + 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 rev_vector datasize container_size esize x _ _ _ _ _ => 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 diff --git a/Arm/Insts/DPR/Data_processing_one_source.lean b/Arm/Insts/DPR/Data_processing_one_source.lean new file mode 100644 index 00000000..9edf7dd4 --- /dev/null +++ b/Arm/Insts/DPR/Data_processing_one_source.lean @@ -0,0 +1,143 @@ +/- +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 Std.BitVec + +private theorem shiftLeft_ge (x : Nat) (y : Nat) : x ≤ x <<< y := by + have h₀ : 0 < 2 ^ y := by + simp only [zero_lt_two, 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, ← 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, ← pow_add] + apply Nat.pow_dvd_pow_iff_le_right'.mpr H3 + +-- TODO: this theorem could be removed once it gets into Std.BitVec +private theorem toNat_eq_nat (x : BitVec n) (y : Nat) + : (x.toNat = y) ↔ (y < 2^n ∧ (x = y#n)) := by + apply Iff.intro + · intro eq + have lt := x.isLt + simp only [eq] at lt + simp [←eq, lt, x.isLt] + · intro eq + simp only [eq] + unfold Std.BitVec.ofNat + unfold Fin.ofNat' + unfold Std.BitVec.toNat + simp only [] + apply Nat.mod_eq_of_lt + simp only [eq] + +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 [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, zero_le] + have opc_h₂ : opc.toNat < 4 := by + simp only [] + refine Std.BitVec.isLt (extractLsb 1 0 inst.opcode) + have opc_sf_h : ¬(opc.toNat = 3 ∧ inst.sf.toNat = 0) := by + simp only [] + 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 [] + generalize Std.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 diff --git a/Arm/Insts/DPR/Insts.lean b/Arm/Insts/DPR/Insts.lean index 7dd42747..cc10db8b 100644 --- a/Arm/Insts/DPR/Insts.lean +++ b/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] diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean index dac34303..6cd62690 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean @@ -16,69 +16,6 @@ namespace DPSFP open Std.BitVec -/-- 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 := Std.BitVec.zeroExtend esize x - let rest_x := Std.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 [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, add_tsub_cancel_of_le, h1] - h3 ▸ (element ++ rest_ans) - termination_by rev_elems n esize x h₀ h₁ => 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 := Std.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 := Std.BitVec.zeroExtend new_datasize (x >>> container_size) - have h₄' : container_size ∣ new_datasize := by - have h : container_size ∣ container_size := by simp - exact Nat.dvd_sub h₂ h₄ h - have h₂' : container_size <= new_datasize := by - refine Nat.le_of_dvd ?h h₄' - simp_all!; exact Ne.lt_of_le' h0 h₂ - 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 rev_vector datasize container_size esize x _ _ _ _ _ => datasize - -example : rev_vector 32 16 8 0xaabbccdd#32 (by decide) - (by decide) (by decide) (by decide) (by decide) = - 0xbbaaddcc#32 := by - native_decide - theorem Nat_lt_of_2_pow_dvd (x y : Nat) (h : x < y) : 2^x ∣ 2^y := by rw [Nat.pow_dvd_pow_iff_le_right] exact Nat.le_of_lt h diff --git a/Tests/SHA512ProgramTest.lean b/Tests/SHA512ProgramTest.lean index 0cb26e35..b952e915 100644 --- a/Tests/SHA512ProgramTest.lean +++ b/Tests/SHA512ProgramTest.lean @@ -626,7 +626,7 @@ example : final_sha512_hash = -- the specification function. def spec_input_message : List (List (BitVec 64)) := let block_revbytes := - List.map (fun elem => DPSFP.rev_elems 64 8 elem (by decide) (by decide)) message_block + List.map (fun elem => rev_elems 64 8 elem (by decide) (by decide)) message_block [block_revbytes] -- The specification function computes the same hash value as our