package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
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) Stdlib.Hashtbl.t -> (string, string) Stdlib.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 : Stdlib.out_channel -> smt_def list -> unit
type sexpr =
  1. | List of sexpr list
  2. | Atom of string
val string_of_sexpr : sexpr -> string
val lparen : Str.split_result list -> unit Parser_combinators.parse_result
val rparen : Str.split_result list -> unit Parser_combinators.parse_result
val atom : Str.split_result list -> string Parser_combinators.parse_result
val sexp : Str.split_result list -> sexpr Parser_combinators.parse_result
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 -> Type_check.Env.t -> string -> Ast.id -> Ast.id list -> Jib.ctyp list -> (Ast.id * string option) list -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct