package sail

  1. Overview
  2. Docs
type smt_typ =
  1. | Bitvec of int
  2. | Bool
  3. | String
  4. | Real
  5. | Datatype of string * (string * (string * smt_typ) list) list
  6. | Tuple of smt_typ list
  7. | 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 =
  1. | Bool_lit of bool
  2. | Bitvec_lit of Sail2_values.bitU list
  3. | Real_lit of string
  4. | String_lit of string
  5. | Var of string
  6. | Shared of string
  7. | Read_res of string
  8. | Enum of string
  9. | Fn of string * smt_exp list
  10. | Ctor of string * smt_exp list
  11. | Ite of smt_exp * smt_exp * smt_exp
  12. | SignExtend of int * smt_exp
  13. | Extract of int * int * smt_exp
  14. | Tester of string * smt_exp
  15. | Syntactic of smt_exp * smt_exp list
  16. | Struct of string * (string * smt_exp) list
  17. | Field of string * smt_exp
  18. | 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 = {
  1. name : string;
  2. node : int;
  3. active : smt_exp;
  4. kind : smt_exp;
  5. addr_type : smt_typ;
  6. addr : smt_exp;
  7. ret_type : smt_typ;
  8. doc : string;
}
type write_info = {
  1. name : string;
  2. node : int;
  3. active : smt_exp;
  4. kind : smt_exp;
  5. addr_type : smt_typ;
  6. addr : smt_exp;
  7. data_type : smt_typ;
  8. data : smt_exp;
  9. doc : string;
}
type barrier_info = {
  1. name : string;
  2. node : int;
  3. active : smt_exp;
  4. kind : smt_exp;
  5. doc : string;
}
type branch_info = {
  1. name : string;
  2. node : int;
  3. active : smt_exp;
  4. addr_type : smt_typ;
  5. addr : smt_exp;
  6. doc : string;
}
type cache_op_info = {
  1. name : string;
  2. node : int;
  3. active : smt_exp;
  4. kind : smt_exp;
  5. addr_type : smt_typ;
  6. addr : smt_exp;
  7. doc : string;
}
type smt_def =
  1. | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
  2. | Declare_fun of string * smt_typ list * smt_typ
  3. | Declare_const of string * smt_typ
  4. | Define_const of string * smt_typ * smt_exp
  5. | Preserve_const of string * smt_typ * smt_exp
  6. | Write_mem of write_info
  7. | Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
  8. | Read_mem of read_info
  9. | Barrier of barrier_info
  10. | Branch_announce of branch_info
  11. | Cache_maintenance of cache_op_info
  12. | Excl_res of string * int * smt_exp
  13. | Declare_datatypes of string * (string * (string * smt_typ) list) list
  14. | Declare_tuple of int
  15. | 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 =
  1. | List of sexpr list
  2. | 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