RVWMO support via Sail concurrency interface

Sail has for a while now had a flexible way of passing additional information to either operational or axiomatic concurrency models by instantiating outcomes (effects) with model-specific types. The set of possible outcomes is defined in the Sail library, and a subset of these can be instantiated by any model.

This PR refactors the base memory access functions to correctly instantiate these outcomes, which enables our concurrency tooling (most relevantly to this PR: https://github.com/rems-project/isla) to work correctly with the RISC-V model. Previously I had been maintaining this on my own fork, but it really should be upstreamed!

Outside of the memory read and write primitives being changed, there are several small changes required for the concurrency model. We need to announce when each instruction has ended, when branches occur, and tell the concurrency model what instruction is being executed after each ifetch. This for dependency analysis (deriving addr, data, and ctrl). The riscv_analysis.sail file that was previously being used for this is no longer required, so it is removed as part of this PR. There are also a few additional entry points to the model other than main used by the symbolic execution tooling to execute a single instruction, with and without any prior initialisation.

This PR was tested on the tests in https://github.com/litmus-tests/litmus-tests-riscv, but I do need to re-run them so we should hold off on merging until that has been done.

riscv / sail-riscv

RVWMO support via Sail concurrency interface #458

Test Results