The main limitiation when converting Sail into pure SMT bitvectors is that Sail has arbitrary precision types, as well as types like real and string that are not very SMT friendly. We can add dynamic assertions that effectivly check at runtime that we never exceed some upper bound on bitvector size, and log if we ever use features like strings or real numbers.

We generate primitives in a monad that accumulates any required dynamic checks, and contains the location information for any error messages.

The SMT generation monad contains the location of the expression or definition we are generating SMT for

Get the Jib context during SMT generation

Convert a SMT bitvector expression of size from into a SMT bitvector expression of size into with the same signed value. When into < from inserts a dynamic check that the original value is representable at the new length.

Similar to signed_size, except it assumes the bitvector is representing an unsigned value.

bvint sz n Create a (two's complement) SMT bitvector representing a the number n in a bitvector of length sz. Raises an error if this is not possible.

Some Sail primitives we can't directly convert to pure SMT definitions, either because they don't exist in SMTLIB (like count_leading_zeros), or they involve input/output. In these cases we provide a module so the backend can provide callbacks to generate the required implementations for these primitives.

We have various options for handling undefined bits for SMT generation, either we can treat them all as zero (which is consistent with the default emulator behavior), or generated undefined bits, or have the builtin generator skip these functions.