Compile Sail builtins to SMT bitvector expressions
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.
val current_location : Parse_ast.l check_writerThe SMT generation monad contains the location of the expression or definition we are generating SMT for
val return : 'a -> 'a check_writerval bind : 'a check_writer -> ('a -> 'b check_writer) -> 'b check_writerval fmap : ('a -> 'b) -> 'a check_writer -> 'b check_writerval let* : 'a check_writer -> ('a -> 'b check_writer) -> 'b check_writerval let+ : 'a check_writer -> ('a -> 'b) -> 'b check_writerval mapM : ('a -> 'b check_writer) -> 'a list -> 'b list check_writerval run : 'a check_writer -> Parse_ast.l -> 'a * checksval signed_size :
?checked:bool ->
into:int ->
from:int ->
Smt_exp.smt_exp ->
Smt_exp.smt_exp check_writerConvert 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.
val unsigned_size :
?max_value:int ->
?checked:bool ->
into:int ->
from:int ->
Smt_exp.smt_exp ->
Smt_exp.smt_exp check_writerSimilar to signed_size, except it assumes the bitvector is representing an unsigned value.
val bvint : int -> Libsail.Ast_util.Big_int.num -> Smt_exp.smt_expbvint 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.
module type CONFIG = sig ... endmodule type PRIMOP_GEN = sig ... endSome Sail primitives we can't directly convert to pure SMT bitvectors, 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 generate the required implementations for these primitives.
module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) : sig ... end