From fc93bde5dd13228bcd519dec33e1efc68b93037e Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 19 Aug 2024 15:55:20 -0500 Subject: [PATCH] chore: cache SHA states as well --- Arm/Insts/Common.lean | 9 +++------ Arm/Insts/CosimM.lean | 18 +++++++++++++----- Arm/Insts/DPR/Data_processing_one_source.lean | 4 ++-- .../DPR/Data_processing_three_source.lean | 2 +- Arm/Insts/DPR/Data_processing_two_source.lean | 2 +- Arm/Insts/DPSFP/Crypto_four_reg.lean | 6 +----- Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean | 6 +----- Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean | 8 ++------ 8 files changed, 24 insertions(+), 31 deletions(-) diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 4579a9bd..61505720 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -7,6 +7,7 @@ Author(s): Shilpi Goel, Yan Peng, Nathan Wetzler import LeanSAT import Arm.BitVec import Arm.State +import Arm.Insts.CosimM section Common @@ -27,12 +28,8 @@ the latest version is available at https://github.com/ARM-software/abi-aa/releases -/ partial def GPRIndex.rand (lo := 0) (hi := 31) : - IO (BitVec 5) := do - let darwin_check ← - IO.Process.output - { cmd := "Arm/Insts/Cosim/platform_check.sh", - args := #["-d"] } - if darwin_check.exitCode == 1 then + Cosim.CosimM (BitVec 5) := do + if ← Cosim.darwin? then go lo hi else -- On non-Darwin machines, fall through to `BitVec.rand`. diff --git a/Arm/Insts/CosimM.lean b/Arm/Insts/CosimM.lean index 1cb53892..086df82e 100644 --- a/Arm/Insts/CosimM.lean +++ b/Arm/Insts/CosimM.lean @@ -16,6 +16,8 @@ namespace Cosim structure Context where private mk :: aarch64? : Bool darwin? : Bool + sha3? : Bool + sha512? : Bool /-- Monad for cosimulation to run in. This acts as a cache for platform information. @@ -24,23 +26,29 @@ abbrev CosimM := ReaderT Context IO /-- Run `platform_check.sh` to gather platform details -/ -private def getPlatformCheckExitCode (arg : String) : IO UInt32 := do +private def getPlatformCheckExitCode (args : Array String) : IO UInt32 := do let machine_check ← IO.Process.output { cmd := "Arm/Insts/Cosim/platform_check.sh", - args := #[arg] + args := args } return machine_check.exitCode /-- Make a new Context by reading platform information. -/ def Context.new : IO Context := do - let darwin? := (← getPlatformCheckExitCode "-d") == 1 - let aarch64? := (← getPlatformCheckExitCode "-m") == 1 - return { darwin? := darwin?, aarch64? := aarch64? } + let darwin? := (← getPlatformCheckExitCode #["-d"]) == 1 + let aarch64? := (← getPlatformCheckExitCode #["-m"]) == 1 + let sha3? := (← getPlatformCheckExitCode #["-f", "sha3"]) == 1 + let sha512? := (← getPlatformCheckExitCode #["-f", "sha512"]) == 1 + return { darwin?, aarch64?, sha3?, sha512? } def aarch64? : CosimM Bool := do return (← read).aarch64? def darwin? : CosimM Bool := do return (← read).aarch64? +def sha3? : CosimM Bool := do return (← read).sha3? + +def sha512? : CosimM Bool := do return (← read).sha512? + def CosimM.run (m : CosimM α) : IO α := do ReaderT.run m (← Context.new) end Cosim diff --git a/Arm/Insts/DPR/Data_processing_one_source.lean b/Arm/Insts/DPR/Data_processing_one_source.lean index 7d55cdd5..037027b4 100644 --- a/Arm/Insts/DPR/Data_processing_one_source.lean +++ b/Arm/Insts/DPR/Data_processing_one_source.lean @@ -100,7 +100,7 @@ def exec_data_processing_one_source ---------------------------------------------------------------------- -partial def Data_processing_one_source_cls.rev_all.rand : IO (Option (BitVec 32)) := do +partial def Data_processing_one_source_cls.rev_all.rand : Cosim.CosimM (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 @@ -118,7 +118,7 @@ partial def Data_processing_one_source_cls.rev_all.rand : IO (Option (BitVec 32) 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)) := +def Data_processing_one_source_cls.rand : Cosim.CosimM (Option (BitVec 32)) := Data_processing_one_source_cls.rev_all.rand end DPR diff --git a/Arm/Insts/DPR/Data_processing_three_source.lean b/Arm/Insts/DPR/Data_processing_three_source.lean index 6542981a..9b1e489e 100644 --- a/Arm/Insts/DPR/Data_processing_three_source.lean +++ b/Arm/Insts/DPR/Data_processing_three_source.lean @@ -75,7 +75,7 @@ def exec_data_processing_three_source def Data_processing_three_source_cls.shift.rand (sf : BitVec 1) (op54 : BitVec 2) (op31 : BitVec 3) (o0 : BitVec 1) - : IO (Option (BitVec 32)) := do + : Cosim.CosimM (Option (BitVec 32)) := do let (inst : Data_processing_three_source_cls) := { sf := sf, op54 := op54, diff --git a/Arm/Insts/DPR/Data_processing_two_source.lean b/Arm/Insts/DPR/Data_processing_two_source.lean index 6e161252..807fccca 100644 --- a/Arm/Insts/DPR/Data_processing_two_source.lean +++ b/Arm/Insts/DPR/Data_processing_two_source.lean @@ -43,7 +43,7 @@ def exec_data_processing_two_source ---------------------------------------------------------------------- def Data_processing_two_source_cls.shift.rand - (opcode : BitVec 6) : IO (Option (BitVec 32)) := do + (opcode : BitVec 6) : Cosim.CosimM (Option (BitVec 32)) := do let (inst : Data_processing_two_source_cls) := { sf := ← BitVec.rand 1, S := 0b0#1, diff --git a/Arm/Insts/DPSFP/Crypto_four_reg.lean b/Arm/Insts/DPSFP/Crypto_four_reg.lean index d901f367..34aa426d 100644 --- a/Arm/Insts/DPSFP/Crypto_four_reg.lean +++ b/Arm/Insts/DPSFP/Crypto_four_reg.lean @@ -36,11 +36,7 @@ def exec_crypto_four_reg (inst : Crypto_four_reg_cls) (s : ArmState) : ArmState ---------------------------------------------------------------------- def Crypto_four_reg_cls.eor3.rand : Cosim.CosimM (Option (BitVec 32)) := do - let feat_check ← - IO.Process.output - { cmd := "Arm/Insts/Cosim/platform_check.sh", - args := #["-f", "sha3"] } - if feat_check.exitCode = 1 then + if (← Cosim.sha3?) then -- SHA3 feature supported. let (inst : Crypto_four_reg_cls) := { Op0 := ← pure 0b00#2, diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean index 41ce98ee..59b6e85d 100644 --- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean @@ -96,11 +96,7 @@ def exec_crypto_three_reg_sha512 ---------------------------------------------------------------------- def Crypto_three_reg_sha512_cls.sha512.rand : Cosim.CosimM (Option (BitVec 32)) := do - let feat_check ← - IO.Process.output - { cmd := "Arm/Insts/Cosim/platform_check.sh", - args := #["-f", "sha512"] } - if feat_check.exitCode == 1 then + if (← Cosim.sha512?) then -- SHA512 feature supported. let (inst : Crypto_three_reg_sha512_cls) := { Rm := ← BitVec.rand 5, diff --git a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean index 1529b61c..ec9bfc33 100644 --- a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean @@ -51,12 +51,8 @@ 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 := "Arm/Insts/Cosim/platform_check.sh", - args := #["-f", "sha512"] } - if feat_check.exitCode = 1 then +def Crypto_two_reg_sha512_cls.sha512su0.rand : Cosim.CosimM (Option (BitVec 32)) := do + if (← Cosim.sha512?) then -- SHA512 feature supported. let (inst : Crypto_two_reg_sha512_cls) := { opcode := ← pure 0b00#2,