Lean emulator

[Ptival]

Opening this pull request for discussion about what it would take to integrate these changes upstream.

This PR contains:

• a frontend to start an emulator based on Lean extracted from SAIL RISC-V,
• a CI job that builds said emulator, and tests it on some ELF files.

There are, however, a couple of things that ought to be discussed:

1. In order to parse ELF files, this adds a dependency to ELFSage. Well, almost, the project is purposefully kept compatible with an old version of Lean (see here), so we forked and modernized it. This is a new dependency. I have found it fairly easy to maintain, but I wanted to be upfront about it.
2. Our "main" is not the cleanest, I might do a tiny bit of refactoring, but please let us know whether it would require significant changes to merge.
3. I have extended the Lean workflow to test the extracted emulator. Unfortunately, we have to re-extract the Lean code with a smaller set of modules to get less prohibitive compilation times, and then also extract the ELF files. There might be nicer ways of achieving this without all the redundancy here, but I'm neither an expert at CMake or CI, so I'm open to ideas.

Putting this as a draft request for now.

[github-actions]

Test Results

2 325 tests   - 1   2 325 ✅  - 1   31m 0s ⏱️ +9s
    1 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit d556774. ± Comparison against base commit 664e5c1.

This pull request removes 1 test.

unit_tests ‑ unit_tests

[pmundkur]

This is really great!

[Timmmm]

I agree this is great! I don't see any issue with merging it except potentially that not many of us really know Lean. Would you be willing to maintain it. Also what are you using it for, just out of curiosity?

(And on the other hand, learning Lean has been on my todo list for ages so maybe this is a good excuse to finally get around to it!)

[jprider63]

I agree this is great! I don't see any issue with merging it except potentially that not many of us really know Lean. Would you be willing to maintain it. Also what are you using it for, just out of curiosity?

(And on the other hand, learning Lean has been on my todo list for ages so maybe this is a good excuse to finally get around to it!)

There's a group of us at Galois and Cambridge who have been working on Sail's Lean backend so we can help if things break.

[Ptival]

Alright, I have made a lot of changes, and it's back to being reviewable:

• I have moved the whole logic of building and running the Lean emulator in CMake. Now the CI only calls the appropriate CMake target, much nicer.
• In order to support printing out the logging of the emulator run, I needed to pass -D PRINT_EFFECTS to sail. But there was no way to do so from the current CMake setup, so I added an option PRINT_EFFECTS that, when set, adds -D PRINT_EFFECTS to sail invocations.
• I wanted to use the status code of the emulator run as the status code of the process, so that a failing emulator run would be a failing run for CI. Unfortunately, the original loop did not return the result. If this is okay with everyone, I'm suggesting a change where loop returns the exit code of the code being looped. I have updated one use that doesn't care about it to throw it away, and I'm demonstrating in the emulator main function its use.
• As part of having loop return a status code, I reorganized its control flow to have a clearer single exit point, rather than the current state where the handling of the exit state happens mid-loop.

EDIT: The CI is currently failing because of this limitation:
rems-project/sail#1624

[pmundkur]

This needs a pre-commit fix for CI.

Does the Lean emulator need an unusual amount of CPU/memory resources to build? It's been building for quite a while on my desktop.

[pmundkur]

This file needs to pass pre-commit checks. See

sail-riscv/CONTRIBUTING.md

Line 33 in c4d3140

We recommend installing pre-commit hooks that ensure certain basic coding

[Ptival]

I will look at the pre-commit fix.

As for the resources, I have been building it on a powerful laptop so I'm not sure.
Anecdotally, on our Github CI, the Lean emulator build seems to take ~8 minutes.