sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Smtlib
type smt_typ =
| Bitvec of int
| Bool
| String
| Real
| Datatype of string * (string * (string * smt_typ) list) list
| Tuple of smt_typ list
| Array of smt_typ * smt_typ
val smt_typ_compare : smt_typ -> smt_typ -> int
val smt_typ_equal : smt_typ -> smt_typ -> bool
val mk_enum : string -> string list -> smt_typ
val mk_record : string -> (string * smt_typ) list -> smt_typ
val mk_variant : string -> (string * smt_typ) list -> smt_typ
type smt_exp =
| Bool_lit of bool
| Bitvec_lit of Sail2_values.bitU list
| Real_lit of string
| String_lit of string
| Var of string
| Shared of string
| Read_res of string
| Enum of string
| Fn of string * smt_exp list
| Ctor of string * smt_exp list
| Ite of smt_exp * smt_exp * smt_exp
| SignExtend of int * smt_exp
| Extract of int * int * smt_exp
| Tester of string * smt_exp
| Syntactic of smt_exp * smt_exp list
| Struct of string * (string * smt_exp) list
| Field of string * smt_exp
| Forall of (string * smt_typ) list * smt_exp
val fold_smt_exp : ( smt_exp -> smt_exp ) -> smt_exp -> smt_exp
val smt_conj : smt_exp list -> smt_exp
val smt_disj : smt_exp list -> smt_exp
val extract : int -> int -> smt_exp -> smt_exp
val bvnot : smt_exp -> smt_exp
val bvand : smt_exp -> smt_exp -> smt_exp
val bvor : smt_exp -> smt_exp -> smt_exp
val bvneg : smt_exp -> smt_exp
val bvadd : smt_exp -> smt_exp -> smt_exp
val bvmul : smt_exp -> smt_exp -> smt_exp
val bvudiv : smt_exp -> smt_exp -> smt_exp
val bvurem : smt_exp -> smt_exp -> smt_exp
val bvshl : smt_exp -> smt_exp -> smt_exp
val bvlshr : smt_exp -> smt_exp -> smt_exp
val bvult : smt_exp -> smt_exp -> smt_exp
val bvzero : int -> smt_exp
val bvones : int -> smt_exp
val simp_equal : smt_exp -> smt_exp -> bool option
val simp_and : smt_exp list -> smt_exp
val simp_or : smt_exp list -> smt_exp
val all_bitvec_lit : smt_exp list -> bool
val merge_bitvec_lit : smt_exp list -> Sail2_values.bitU list
val simp_fn : smt_exp -> smt_exp
val simp_ite : smt_exp -> smt_exp
val simp_smt_exp : ( string, smt_exp ) Hashtbl.t -> ( string, string ) Hashtbl.t -> smt_exp -> smt_exp
type read_info = {
name : string;
node : int;
active : smt_exp;
kind : smt_exp;
addr_type : smt_typ;
addr : smt_exp;
ret_type : smt_typ;
doc : string;
}
type write_info = {
name : string;
node : int;
active : smt_exp;
kind : smt_exp;
addr_type : smt_typ;
addr : smt_exp;
data_type : smt_typ;
data : smt_exp;
doc : string;
}
type barrier_info = {
name : string;
node : int;
active : smt_exp;
kind : smt_exp;
doc : string;
}
type branch_info = {
name : string;
node : int;
active : smt_exp;
addr_type : smt_typ;
addr : smt_exp;
doc : string;
}
type cache_op_info = {
name : string;
node : int;
active : smt_exp;
kind : smt_exp;
addr_type : smt_typ;
addr : smt_exp;
doc : string;
}
type smt_def =
| Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
| Declare_fun of string * smt_typ list * smt_typ
| Declare_const of string * smt_typ
| Define_const of string * smt_typ * smt_exp
| Preserve_const of string * smt_typ * smt_exp
| Write_mem of write_info
| Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
| Read_mem of read_info
| Barrier of barrier_info
| Branch_announce of branch_info
| Cache_maintenance of cache_op_info
| Excl_res of string * int * smt_exp
| Declare_datatypes of string * (string * (string * smt_typ) list) list
| Declare_tuple of int
| Assert of smt_exp
val smt_def_map_exp : ( smt_exp -> smt_exp ) -> smt_def -> smt_def
val smt_def_iter_exp : ( smt_exp -> unit ) -> smt_def -> unit
val declare_datatypes : smt_typ -> smt_def
val suffix_variables_exp : string -> smt_exp -> smt_exp
val suffix_variables_read_info : string -> read_info -> read_info
val suffix_variables_write_info : string -> write_info -> write_info
val suffix_variables_barrier_info : string -> barrier_info -> barrier_info
val suffix_variables_branch_info : string -> branch_info -> branch_info
val suffix_variables_cache_op_info : string -> cache_op_info -> cache_op_info
val suffix_variables_def : string -> smt_def -> smt_def
val pp_sfun : string -> PPrint.document list -> PPrint.document
val pp_smt_typ : smt_typ -> PPrint.document
val pp_str_smt_typ : (string * smt_typ) -> PPrint.document
val pp_smt_exp : smt_exp -> PPrint.document
val pp_smt_def : smt_def -> PPrint.document
val string_of_smt_def : smt_def -> string
val output_smt_defs : out_channel -> smt_def list -> unit
type sexpr =
| List of sexpr list
| Atom of string
val string_of_sexpr : sexpr -> string
val parse_sexps : string -> sexpr list
val value_of_sexpr : sexpr -> Jib.ctyp -> Value.value
val find_arg : Ast.id -> Jib.ctyp -> (Ast.id * string option) list -> sexpr list -> Ast.id * Value.value
val build_counterexample : Ast.id list -> Jib.ctyp list -> (Ast.id * string option) list -> sexpr list -> (Ast.id * Value.value) list
val run : Interpreter.frame -> Value.value option
val check_counterexample : Type_check.tannot Ast_defs.ast -> Type_check.Env.t -> string -> Ast.id -> Ast.id list -> Jib.ctyp list -> (Ast.id * string option) list -> unit