Sail tries to check for pattern match completeness and issues warnings
but this often gives false positives: see discussion at
https://github.com/rems-project/sail/issues/191 .  To suppress these
we add a wildcard case that raises an internal error.  There is
effectively no behaviour change as these would previously have
resulted in a match error at runtime and they should be unreachable
anyway.

At the same time we change the DOUBLE case in memory access paths to
allow for xlen > 64.

Following discussion on the PR I also changed internal_error to take a
file and line number as an argument to aid with debugging.

Fixes: https://github.com/riscv/sail-riscv/issues/194

Merged after code review. Thanks everybody for helping.

* test: Ignore generated XML output

* run_tests: Build RVFI emulators too

Can't run tests with them though as they're built for direct instruction
injection (RVFI-DII) via an instruction stream over a network socket,
not fetching instructions from memory, so this remains just a build
test.

* run_tests/run_fp_tests: Print summary and give meaningful exit code

* run_tests/run_fp_tests: Include tests and failures in top-level XML entity

* run_tests/run_fp_tests: Use failure not error for XML output

The former is the standard tag for normal test failures, the latter is
for catastrophic things like test harness errors.

* Run ISA tests in CI

pull-requests ideally come with an explanation how the correctness of
the PR was established.

These are intended to deal with much of the low-hanging fruit; plenty of
room for improvement exists.

The order used for wildcard is not deterministic and varies between
systems. Sorting ensures the diffs are easy to inspect going forwards.

Closes: #142

NB: Smstateen support is missing in the model so enabling the Zfinx
extension provides an architectural covert channel via FCSR if
privileged software is not aware of Zfinx's existence.

Co-authored-by: Jessica Clarke <jrtc27@jrtc27.com>

Co-authored-by: Ibrahim Abu Kharmeh <abukharmeh@gmail.com>

This reverts commit c5e62ea4.

* Adds Zfinx enable flag

* Hardwire misa.{f,d} and mstats.FS to 0

* Moving nan boxing functions to fdext_reg

* Swaps register names for floating point instructions

Adds new mapping to swap register names, and use it in all assembly clauses

* Disable Floating point loads, stores and moves

* Add X_or_F_s and X_or_F_d functions, and use them to access all registers for floating points

Changes register accessed for floating point instructions and modify nan boxing functions for zfinx

* Formatting

Remove couple of misplaced whitespace, unnecessary parens

* Fix inconsistent indentation in insts_dext file

* Fix spacing in fdext_regs

* Remove redundant comparasion with true/ false

* Constistant tuples spacing and removes couple of unnecessary parens.

* Consistent functions declaration & calls spacing and removes couple of unnecessary parens.

* Consistent spacing and removes couple of unnecessary comparasion with true/false

* Make spacing consistent

* Remove checks from execution stage

* Add checks to encdec stage

Trying to make the behavior of aesks1i easier to understand, and more
obviously correspond to the specification.

- Ensure that the aes_decode_rcon function only accepts valid values, plus
  add comments.

- Re-name operands to aesks1i rcon -> rnum to be in line with the specification

- Re-structure the Sail code for clarity based on jrtc27's suggestion.

Remove weird whitespace " );" -> ");" at end of expressions to be
consistent with the rest of the code base.

 On branch scalar-crypto-tidy
 Changes to be committed:
	modified:   model/riscv_insts_zkn.sail

Add spaces pre/post used of "==" operator to be consistent with the rest
of the code.

File is no longer needed, as per this discussion: https://github.com/riscv/sail-riscv/issues/119

Fixes rems-project/sail#152

* Use bool for floating point comparison result

Using bits_WU (bits(32)) or bits_LU (bits(64)) makes no sense, these are
just boolean values, and having fixed-width types is a pain for
suporting RV32D (since RV32D would need to truncate, but RV128D would
need to extend). Instead represent these as an actual bool to match what
the values really are. This could be done with bits(1) but the value is
logically a boolean (like the built-in integer comparison operators) not
a bit vector of length one so we convert to bool and back for a cleaner
interface.

* Support compiling RV32F with flen == 64

The code conflated flen and xlen; deconflating them and adding suitable
assertions (rather than silently retiring as a no-op that doesn't bump
instret) ensures that it can be compiled for RV32 with flen set to 64.
Whilst here, add the extensions and truncations that would be needed for
RV128F.

Note that there are already suitable guards on the decode clauses to
ensure these instructions are illegal on RV32.

* Support compiling RV32D

This copies various bits of XLEN generality from the F code.

* Support RV32D loads/stores

* Correctly initialise misa.D based on flen not xlen

* Makefile: Enable D extension for RV32

This now works so can be enabled.

* test: Enable RV32D tests

Merged scalar-crypto pull request #99  of 1.0.0-rc2 spec work from Ben Marshall. See https://github.com/riscv/sail-riscv/pull/99.

Fix crash when fcsr.frm is invalid

Fix incorrect SV48_Vaddr bitfield

tweak README for move to riscv organisation

Encourage use of `opam` and streamline by moving discussion of setting `SAIL_DIR` into a separate section about building using a custom Sail version.

Also tweak Makefile to remove new Coq generated files

This is required for implementing memory version support for CHERI.