From 7b3bc81e47ab1113a09c55fa77cd6c3ac0f360b6 Mon Sep 17 00:00:00 2001 From: Nevine Ebeid <66388554+nebeid@users.noreply.github.com> Date: Wed, 21 Feb 2024 23:32:17 -0500 Subject: [PATCH] EOR3, part of Crypto four registers. (#17) ### Description: Add EOR3 instruction which is part of the Cryptographic four-register group of DPSFP https://developer.arm.com/documentation/ddi0602/2023-12/SIMD-FP-Instructions/EOR3--Three-way-Exclusive-OR-?lang=en Also place the shabang line at the top of the shell script `platform_check.sh`. Otherwise, aarch64 is not detected. ### Testing: `make all` including conformance testing. ### 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 | 2 + Arm/Decode/DPSFP.lean | 18 +++++++ Arm/Exec.lean | 2 + Arm/Insts/Cosim/platform_check.sh | 4 +- Arm/Insts/DPSFP/Crypto_four_reg.lean | 57 ++++++++++++++++++++ Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean | 10 ++-- Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean | 4 +- Arm/Insts/DPSFP/Insts.lean | 6 ++- 8 files changed, 92 insertions(+), 11 deletions(-) create mode 100644 Arm/Insts/DPSFP/Crypto_four_reg.lean diff --git a/Arm/Decode.lean b/Arm/Decode.lean index a438c360..6db16fa2 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -90,6 +90,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst := DPSFP (Crypto_three_reg_sha512 {Rm, O, opcode, Rn, Rd}) | [11001110110000001000, opcode:2, Rn:5, Rd:5] => DPSFP (Crypto_two_reg_sha512 {opcode, Rn, Rd}) + | [110011100, Op0:2, Rm:5, 0, Ra:5, Rn:5, Rd:5] => + DPSFP (Crypto_four_reg {Op0, Rm, Ra, Rn, Rd}) | [0, Q:1, U:1, 01110, size:2, 10000, opcode:5, 10, Rn:5, Rd:5] => DPSFP (Advanced_simd_two_reg_misc {Q, U, size, opcode, Rn, Rd}) | [0, Q:1, op:1, 01110000, imm5:5, 0, imm4:4, 1, Rn:5, Rd:5] => diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean index 5b12859c..7adcd735 100644 --- a/Arm/Decode/DPSFP.lean +++ b/Arm/Decode/DPSFP.lean @@ -53,6 +53,22 @@ instance : ToString Crypto_two_reg_sha512_cls where toString a := toString (repr def Crypto_two_reg_sha512_cls.toBitVec32 (x : Crypto_two_reg_sha512_cls) : BitVec 32 := x._fixed ++ x.opcode ++ x.Rn ++ x.Rd +structure Crypto_four_reg_cls where + _fixed1 : BitVec 9 := 0b110011100#9 -- [31:23] + Op0 : BitVec 2 -- [22:21] + Rm : BitVec 5 -- [20:16] + _fixed2 : BitVec 1 := 0b0#1 -- [15:15] + Ra : BitVec 5 -- [14:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Crypto_four_reg_cls where +toString a := toString (repr a) + +def Crypto_four_reg_cls.toBitVec32 (x : Crypto_four_reg_cls) : BitVec 32 := + x._fixed1 ++ x.Op0 ++ x.Rm ++ x._fixed2 ++ x.Ra ++ x.Rn ++ x.Rd + structure Advanced_simd_two_reg_misc_cls where _fixed1 : BitVec 1 := 0b0#1 -- [31:31] Q : BitVec 1 -- [30:30] @@ -150,6 +166,8 @@ inductive DataProcSFPInst where Crypto_two_reg_sha512_cls → DataProcSFPInst | Crypto_three_reg_sha512 : Crypto_three_reg_sha512_cls → DataProcSFPInst + | Crypto_four_reg : + Crypto_four_reg_cls → DataProcSFPInst | Advanced_simd_two_reg_misc : Advanced_simd_two_reg_misc_cls → DataProcSFPInst | Advanced_simd_copy : diff --git a/Arm/Exec.lean b/Arm/Exec.lean index bea31af6..90731b1e 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -40,6 +40,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := DPSFP.exec_crypto_two_reg_sha512 i s | DPSFP (DataProcSFPInst.Crypto_three_reg_sha512 i) => DPSFP.exec_crypto_three_reg_sha512 i s + | DPSFP (DataProcSFPInst.Crypto_four_reg i) => + DPSFP.exec_crypto_four_reg i s | DPSFP (DataProcSFPInst.Advanced_simd_two_reg_misc i) => DPSFP.exec_advanced_simd_two_reg_misc i s | DPSFP (DataProcSFPInst.Advanced_simd_extract i) => diff --git a/Arm/Insts/Cosim/platform_check.sh b/Arm/Insts/Cosim/platform_check.sh index d56a2707..a622dbc3 100755 --- a/Arm/Insts/Cosim/platform_check.sh +++ b/Arm/Insts/Cosim/platform_check.sh @@ -1,9 +1,9 @@ +#!/bin/bash + # 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 -#!/bin/bash - machine_check () { machine=$(uname -m) if [[ $machine == *aarch64* ]]; then diff --git a/Arm/Insts/DPSFP/Crypto_four_reg.lean b/Arm/Insts/DPSFP/Crypto_four_reg.lean new file mode 100644 index 00000000..6eb02107 --- /dev/null +++ b/Arm/Insts/DPSFP/Crypto_four_reg.lean @@ -0,0 +1,57 @@ +/- +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): Shilpi Goel, Nevine Ebeid +-/ +-- EOR3 + +import Arm.Decode +import Arm.Memory +import Arm.Insts.Common +import Arm.BitVec + +---------------------------------------------------------------------- + +namespace DPSFP + +open Std.BitVec + +def exec_crypto_four_reg (inst : Crypto_four_reg_cls) (s : ArmState) : ArmState := + -- This function assumes IsFeatureImplemented(FEAT_SHA3) is true + -- and that AArch64.CheckFPAdvSIMDEnabled() returns successfully + if inst.Op0 != 0b00#2 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let datasize := 128 + let opdm := read_sfp datasize inst.Rm s + let opdn := read_sfp datasize inst.Rn s + let opda := read_sfp datasize inst.Ra s + let result := opdm ^^^ opdn ^^^ opda + let s := write_sfp datasize inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +---------------------------------------------------------------------- + +def Crypto_four_reg_cls.eor3.rand : IO (Option (BitVec 32)) := do + let feat_check ← + IO.Process.output + { cmd := "Arm/Insts/Cosim/platform_check.sh", + args := #["-f", "sha3"] } + if feat_check.exitCode == 0 then + let (inst : Crypto_four_reg_cls) := + { Op0 := ← pure 0b00#2, + Rm := ← BitVec.rand 5, + Rn := ← BitVec.rand 5, + Ra := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 } + pure (some inst.toBitVec32) + else + pure none + +/-- Generate random instructions of Crypto_four_reg_cls class. -/ +def Crypto_four_reg_cls.rand : List (IO (Option (BitVec 32))) := + [Crypto_four_reg_cls.eor3.rand] + + +end DPSFP diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean index 333ddcc6..cfcf0d18 100644 --- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean @@ -70,7 +70,7 @@ def sha512su1 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) result @[simp] -def exec_crypto_three_reg_sha512 +def exec_crypto_three_reg_sha512 (inst : Crypto_three_reg_sha512_cls) (s : ArmState) : ArmState := open Std.BitVec in let x := read_sfp 128 inst.Rn s @@ -81,10 +81,10 @@ def exec_crypto_three_reg_sha512 | 0b0#1, 0b00#2 => some (sha512h x y w) | 0b0#1, 0b01#2 => some (sha512h2 x y w) | 0b0#1, 0b10#2 => some (sha512su1 x y w) - | _, _ => none + | _, _ => none -- State Updates if result.isNone then - write_err + write_err (StateError.Unimplemented s!"Unsupported instruction {inst} encountered!") s else @@ -97,7 +97,7 @@ def exec_crypto_three_reg_sha512 def Crypto_three_reg_sha512_cls.sha512.rand : IO (Option (BitVec 32)) := do let feat_check ← IO.Process.output - { cmd := "../Cosim/platform_check.sh", + { cmd := "Arm/Insts/Cosim/platform_check.sh", args := #["-f", "sha512"] } if feat_check.exitCode == 0 then let (inst : Crypto_three_reg_sha512_cls) := @@ -111,7 +111,7 @@ def Crypto_three_reg_sha512_cls.sha512.rand : IO (Option (BitVec 32)) := do pure none /-- Generate random instructions of Crypto_three_reg_sha512_cls class. -/ -def Crypto_three_reg_sha512_cls.rand : List (IO (Option (BitVec 32))) := +def Crypto_three_reg_sha512_cls.rand : List (IO (Option (BitVec 32))) := [Crypto_three_reg_sha512_cls.sha512.rand] diff --git a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean index 9574fdcc..18726c68 100644 --- a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean @@ -53,7 +53,7 @@ def exec_crypto_two_reg_sha512 def Crypto_two_reg_sha512_cls.sha512su0.rand : IO (Option (BitVec 32)) := do let feat_check ← IO.Process.output - { cmd := "../Cosim/platform_check.sh", + { cmd := "Arm/Insts/Cosim/platform_check.sh", args := #["-f", "sha512"] } if feat_check.exitCode == 0 then let (inst : Crypto_two_reg_sha512_cls) := @@ -65,7 +65,7 @@ def Crypto_two_reg_sha512_cls.sha512su0.rand : IO (Option (BitVec 32)) := do pure none /-- Generate random instructions of Crypto_two_reg_sha512_cls class. -/ -def Crypto_two_reg_sha512_cls.rand : List (IO (Option (BitVec 32))) := +def Crypto_two_reg_sha512_cls.rand : List (IO (Option (BitVec 32))) := [Crypto_two_reg_sha512_cls.sha512su0.rand] end DPSFP diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean index 0009361a..d2d51f20 100644 --- a/Arm/Insts/DPSFP/Insts.lean +++ b/Arm/Insts/DPSFP/Insts.lean @@ -10,7 +10,8 @@ import Arm.Insts.DPSFP.Advanced_simd_three_different import Arm.Insts.DPSFP.Crypto_aes import Arm.Insts.DPSFP.Crypto_two_reg_sha512 import Arm.Insts.DPSFP.Crypto_three_reg_sha512 - +import Arm.Insts.DPSFP.Crypto_four_reg + /-- List of functions to generate random instructions of the DPSFP class. -/ def DPSFP.rand : List (IO (Option (BitVec 32))) := @@ -19,4 +20,5 @@ def DPSFP.rand : List (IO (Option (BitVec 32))) := DPSFP.Advanced_simd_three_different_cls.rand ++ DPSFP.Advanced_simd_two_reg_misc_cls.rand ++ DPSFP.Crypto_three_reg_sha512_cls.rand ++ - DPSFP.Crypto_two_reg_sha512_cls.rand + DPSFP.Crypto_two_reg_sha512_cls.rand ++ + DPSFP.Crypto_four_reg_cls.rand