feat: introduce CosimM to store platform features in a cache #98

bollu · 2024-08-19T21:02:14Z

Closes #97 .

Description:

We implement a CosimM monad that tests platform features via platform_features.sh once. These are then used during instruction generation time. e.g. the presence/absence of SHA-512 instructions.

At least locally, I observe a modest decrease in wall clock time:

before

real 131.23
user 79.43
sys 67.27

after

real 126.06
user 75.35
sys 60.94

License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Arm/Insts/DPSFP/Crypto_four_reg.lean

Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean

Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean

Arm/Cosim.lean

Arm/Insts/Common.lean

bollu · 2024-08-20T03:35:49Z

@shigoel fixed parens.

### Description: `x18` is not used either as a source or destination register. Moreover, it is not expected to be preserved after a cosim test. This is expected to clear up the bogus mismatches we see on Arm-based Apple machines. Another relevant PR: #98 ### Testing: `make all` succeeds on my M3. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Siddharth <[email protected]>

bollu · 2024-08-25T15:38:10Z

@shigoel merged to synchronize with latest upstream/master. I feel this can be merged, and we can improve CosimM iteratively to save more data.

shigoel

Nice! Thanks, @bollu!

Arm/Insts/CosimM.lean

bollu added 2 commits August 19, 2024 15:41

chore: add CosimM

2400c5d

chore: cache SHA states as well

fc93bde