search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Pass arguments in RISC-V argument registers (instead of using hardcoded heap addresses) #957

Closed samuelgruetter closed 2 years ago

samuelgruetter commented 2 years ago

This PR updates the bedrock2 submodule to a newer version, where the code emitted by the compiler accepts arguments in the RISC-V argument registers a0, a1, ... a7, and also uses these registers for return values, and preserves callee-saved registers, all as specified by the RISC-V Calling Conventions.

This should make it possible for gcc-emitted riscv code to call bedrock2-compiler-emitted riscv code (I have yet not tested it, I only proved it, so I don't know if it works :wink:).

For anyone who has some time to review this PR, I'd be particularly interested in feedback on Theorem sha256_end2end_correct in Sha256ToCava.v, because that's the toplevel theorem we're trying to sell. Does it make sense to you? Do you think factoring some pre- or postconditions into a definition like preconditions_hold or machine_valid or similar (but maybe with a better name) would make it more digestible?

samuelgruetter commented 2 years ago

I seems that the build failure is caused by Sha256Properties.v running out of memory. It's surprising though that it worked before, I'd expect that my one change should not have any impact, and also, locally, it did not: Before my changes: (a96dfaad03cb1340ddc25720b72743f7d092a88f, Fri Oct 22, Relax precondition on SHA256 spec and hotfix for HMAC (#955)), TIMED=1 make printed

Sha256Properties.vo (real: 1119.16, user: 1110.65, sys: 3.53, mem: 10215044 ko)

and after my changes, it printed

Sha256Properties.vo (real: 1058.05, user: 1051.58, sys: 2.81, mem: 8889496 ko)

i.e. less time and memory, but of course that's just one measurement...

@blaxill do you have any plans in the pipeline to optimize Sha256Properties.v, or should I start fiddling with it and try eg if splitting into several files or sub-proofs helps?

blaxill commented 2 years ago

I seems that the build failure is caused by Sha256Properties.v running out of memory.

Yes it seems we are dangerously close to the CI limits. Unfortunately the CI machines are quite limited in resources and cannot be expanded AFAIK.

@blaxill do you have any plans in the pipeline to optimize Sha256Properties.v, or should I start fiddling with it and try eg if splitting into several files or sub-proofs helps?

I'm currently supposed to be on paternity leave :) so I'll let you or someone else tackle it. I had a look before and I struggled to find a way to improve it in an small-effort incremental manner.