Add llvm_ffi_setup command

[qsctr]

Add the llvm_ffi_setup command, which generates a LLVMSetup spec that can be used to verify a Cryptol foreign function implementation in LLVM against its reference Cryptol specification.

The code supports all Cryptol types that are supported by the Cryptol FFI, with the exception of Integer, Rational, and Z, since those use gmp which would be hard for SAW to handle without additional overrides. Support for Cryptol floating point types is implemented here, but remains unimplemented in SAW Core (#1237), so we can generate the spec for floating point types but llvm_verify won't be able to actually do the verification.

Two integration tests are included: test_ffi_verify extends the Cryptol FFI test suite's test-ffi module with Cryptol implementations for most foreign functions, and verifies them with llvm_ffi_setup and llvm_verify. test_ffi_verify_salsa is a more nontrivial test which verifies djb's Salsa20 reference implementation, as a Cryptol foreign function, against the spec from cryptol-specs, similar to @WeeknightMVP's example.

See the manual for more documentation.

Closes #1842.

TODO:

• Bit
• machine-size bitvectors
• any bitvector <= 64 bits
• flat arrays
• multidimensional arrays
• tuples
• records
• size polymorphism
• llvm_ffi_verify
• documentation

[qsctr]

@andreistefanescu doesn't want to add llvm_ffi_verify because it increases the number of built in commands implemented in Haskell, so I am removing it. I put the code on a branch llvm_ffi_verify in case it ever ends up being useful for something.

[andreistefanescu]

👍