chore: cache SHA states as well

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`.

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

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

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,

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,

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,

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,

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,