package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

dune-project

Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (19)

Authors

Maintainers

B

BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.11.0.tbz

sha256=4cf70a0367fef6f33ee3165f05255914513ea0539b94ddfef0bd46fc9b42fa8a

sha512=cd67a5b7617f661a7786bef0c828ee55307cef5260dfecbb700a618be795d81b1ac49fc1a18c4904fd2eb8a182dc862b0159093028651e78e7dc743f5babf9e3

doc/binsec.smtlib/Binsec_smtlib/Formula/index.html

Module `Binsec_smtlib.Formula`Source

include module type of struct include Formula end

type status =

| SAT
| UNSAT
| TIMEOUT
| UNKNOWN

val status_to_exit_code : status -> int

type bl_unop =

| BlNot

type bl_bnop =

| BlImply
| BlAnd
| BlOr
| BlXor

type bl_comp =

| BlEqual
| BlDistinct

type bv_unop =

| BvNot
| BvNeg
| BvRepeat of int
| BvZeroExtend of int
(*
result has size: `size_of(bv) + int` *
*)
| BvSignExtend of int
| BvRotateLeft of int
| BvRotateRight of int
| BvExtract of int Binsec_base.Interval.t

type bv_bnop =

| BvConcat
| BvAnd
| BvNand
| BvOr
| BvNor
| BvXor
| BvXnor
| BvCmp
| BvAdd
| BvSub
| BvMul
| BvUdiv
| BvSdiv
| BvUrem
| BvSrem
| BvSmod
| BvShl
| BvAshr
| BvLshr

type bv_comp =

| BvEqual
| BvDistinct
| BvUlt
| BvUle
| BvUgt
| BvUge
| BvSlt
| BvSle
| BvSgt
| BvSge

type ax_comp =

| AxEqual
| AxDistinct

type sort =

| BlSort
| BvSort of int
| AxSort of int * int

type bl_var = private {

bl_hash : int;
bl_name : string;

}

type bv_var = private {

bv_hash : int;
bv_name : string;
bv_size : int;

}

type ax_var = private {

ax_hash : int;
ax_name : string;
idx_size : int;
elt_size : int;

}

type var =

| BlVar of bl_var
| BvVar of bv_var
| AxVar of ax_var

type term_desc =

| BlTerm of bl_term
| BvTerm of bv_term
| AxTerm of ax_term

and term = private {

term_hash : int;
term_desc : term_desc;

}

and bl_term_desc =

| BlTrue
| BlFalse
| BlFun of bl_var * term list
| BlLet of def list * bl_term
| BlUnop of bl_unop * bl_term
| BlBnop of bl_bnop * bl_term * bl_term
| BlComp of bl_comp * bl_term * bl_term
| BvComp of bv_comp * bv_term * bv_term
| AxComp of ax_comp * ax_term * ax_term
| BlIte of bl_term * bl_term * bl_term

and bl_term = private {

bl_term_hash : int;
bl_term_desc : bl_term_desc;

}

and bv_term_desc =

| BvCst of Binsec_base.Bitvector.t
| BvFun of bv_var * term list
| BvLet of def list * bv_term
| BvUnop of bv_unop * bv_term
| BvBnop of bv_bnop * bv_term * bv_term
| BvIte of bl_term * bv_term * bv_term
| Select of int * ax_term * bv_term

and bv_term = private {

bv_term_hash : int;
bv_term_desc : bv_term_desc;
bv_term_size : int;

}

and ax_term_desc =

| AxFun of ax_var * term list
| AxLet of def list * ax_term
| AxIte of bl_term * ax_term * ax_term
| Store of int * ax_term * bv_term * bv_term

and ax_term = private {

ax_term_hash : int;
ax_term_desc : ax_term_desc;
idx_term_size : int;
elt_term_size : int;

}

and def_desc =

| BlDef of bl_var * decl list * bl_term
| BvDef of bv_var * decl list * bv_term
| AxDef of ax_var * decl list * ax_term

and def = private {

def_hash : int;
def_desc : def_desc;

}

and decl_desc =

| BlDecl of bl_var * sort list
| BvDecl of bv_var * sort list
| AxDecl of ax_var * sort list

and decl = private {

decl_hash : int;
decl_desc : decl_desc;

}

type entry_desc =

| Declare of decl
| Define of def
| Assert of bl_term
| Assume of bl_term
| Comment of string
| Custom of custom_desc

and custom_desc = ..

An user defined entry.

Custom entry support is experimental and very limited. For now, it will work only for formula creation (no transformation) and printing (and by extension, call to external SMT solver).

type custom_handler = {

hash : custom_desc -> int option;
pp : Format.formatter -> custom_desc -> bool;

}

val register_custom : custom_handler -> unit

register_custom { hash; pp } registers a hash and a pretty printer functions for custom entries.

The hash function should return Some h for the custom entries the handler supports, None otherwise. The pretty printer should print the entry without the surrounding parenthesis and return true for the custom entries the handler supports, false otherwise.

Handlers will be scanned in the reverse order of the call to the register_custom function. Using a custom entry without any registered handler will raise Invalid_custom.

exception Invalid_custom

An exception raised by a function that can not handle a custom entry, either because no hander has been registered for this entry or because the function does not support entry extension.

type entry = private {

entry_hash : int;
entry_desc : entry_desc;

}

type formula = private {

entries : entry Binsec_base.Sequence.t;

}

val empty : formula

val length : formula -> int

val append : formula -> formula -> formula

val push_front : entry -> formula -> formula

val push_back : entry -> formula -> formula

val peek_front : formula -> entry option

val peek_back : formula -> entry option

val pop_front : formula -> formula option

val pop_back : formula -> formula option

val map_forward : (entry -> entry) -> formula -> formula

val map_backward : (entry -> entry) -> formula -> formula

val iter_forward : (entry -> unit) -> formula -> unit

val iter_backward : (entry -> unit) -> formula -> unit

val fold_forward : (entry -> 'a -> 'a) -> formula -> 'a -> 'a

val fold_backward : (entry -> 'a -> 'a) -> formula -> 'a -> 'a

val push_front_declare : decl -> formula -> formula

val push_front_define : def -> formula -> formula

val push_front_assert : bl_term -> formula -> formula

val push_front_assume : bl_term -> formula -> formula

val push_front_comment : string -> formula -> formula

val push_back_declare : decl -> formula -> formula

val push_back_define : def -> formula -> formula

val push_back_assert : bl_term -> formula -> formula

val push_back_assume : bl_term -> formula -> formula

val push_back_comment : string -> formula -> formula

module Printing : sig ... end

Basic printing of formulas

val equal_bl_term : bl_term -> bl_term -> bool

val equal_bv_term : bv_term -> bv_term -> bool

val equal_ax_term : ax_term -> ax_term -> bool

val bl_sort : sort

val bv_sort : int -> sort

val ax_sort : int -> int -> sort

val bl_var : string -> bl_var

val bv_var : string -> int -> bv_var

val ax_var : string -> int -> int -> ax_var

val term : term_desc -> term

val bl_term : bl_term_desc -> bl_term

val bv_term : bv_term_desc -> bv_term

val ax_term : ax_term_desc -> ax_term

val def : def_desc -> def

val decl : decl_desc -> decl

val entry : entry_desc -> entry

val mk_bl_term : bl_term -> term

val mk_bv_term : bv_term -> term

val mk_ax_term : ax_term -> term

val mk_bl_true : bl_term

val mk_bl_false : bl_term

val mk_bl_var : bl_var -> bl_term

val mk_bl_fun : bl_var -> term list -> bl_term

val mk_bl_let : def list -> bl_term -> bl_term

val mk_bl_unop : bl_unop -> bl_term -> bl_term

val mk_bl_bnop : bl_bnop -> bl_term -> bl_term -> bl_term

val mk_bl_comp : bl_comp -> bl_term -> bl_term -> bl_term

val mk_bv_comp : bv_comp -> bv_term -> bv_term -> bl_term

val mk_ax_comp : ax_comp -> ax_term -> ax_term -> bl_term

val mk_bl_ite : bl_term -> bl_term -> bl_term -> bl_term

val mk_bv_cst : Binsec_base.Bitvector.t -> bv_term

val mk_bv_var : bv_var -> bv_term

val mk_bv_fun : bv_var -> term list -> bv_term

val mk_bv_let : def list -> bv_term -> bv_term

val mk_bv_unop : bv_unop -> bv_term -> bv_term

val mk_bv_bnop : bv_bnop -> bv_term -> bv_term -> bv_term

val mk_bv_ite : bl_term -> bv_term -> bv_term -> bv_term

val mk_select : int -> ax_term -> bv_term -> bv_term

val mk_ax_var : ax_var -> ax_term

val mk_ax_fun : ax_var -> term list -> ax_term

val mk_ax_let : def list -> ax_term -> ax_term

val mk_ax_ite : bl_term -> ax_term -> ax_term -> ax_term

val mk_store : int -> ax_term -> bv_term -> bv_term -> ax_term

val mk_bl_def : bl_var -> decl list -> bl_term -> def

val mk_bv_def : bv_var -> decl list -> bv_term -> def

val mk_ax_def : ax_var -> decl list -> ax_term -> def

val mk_bl_decl : bl_var -> sort list -> decl

val mk_bv_decl : bv_var -> sort list -> decl

val mk_ax_decl : ax_var -> sort list -> decl

val mk_declare : decl -> entry

val mk_define : def -> entry

val mk_assert : bl_term -> entry

val mk_assume : bl_term -> entry

val mk_comment : string -> entry

val mk_bl_not : bl_term -> bl_term

val mk_bv_not : bv_term -> bv_term

val mk_bv_neg : bv_term -> bv_term

val mk_bv_repeat : int -> bv_term -> bv_term

val mk_bv_zero_extend : int -> bv_term -> bv_term

val mk_bv_sign_extend : int -> bv_term -> bv_term

val mk_bv_rotate_left : int -> bv_term -> bv_term

val mk_bv_rotate_right : int -> bv_term -> bv_term

val mk_bv_extract : int Binsec_base.Interval.t -> bv_term -> bv_term

val mk_bl_imply : bl_term -> bl_term -> bl_term

val mk_bl_and : bl_term -> bl_term -> bl_term

val mk_bl_or : bl_term -> bl_term -> bl_term

val mk_bl_xor : bl_term -> bl_term -> bl_term

val mk_bv_concat : bv_term -> bv_term -> bv_term

val mk_bv_and : bv_term -> bv_term -> bv_term

val mk_bv_nand : bv_term -> bv_term -> bv_term

val mk_bv_or : bv_term -> bv_term -> bv_term

val mk_bv_nor : bv_term -> bv_term -> bv_term

val mk_bv_xor : bv_term -> bv_term -> bv_term

val mk_bv_xnor : bv_term -> bv_term -> bv_term

val mk_bv_cmp : bv_term -> bv_term -> bv_term

val mk_bv_add : bv_term -> bv_term -> bv_term

val mk_bv_sub : bv_term -> bv_term -> bv_term

val mk_bv_mul : bv_term -> bv_term -> bv_term

val mk_bv_udiv : bv_term -> bv_term -> bv_term

val mk_bv_sdiv : bv_term -> bv_term -> bv_term

val mk_bv_urem : bv_term -> bv_term -> bv_term

val mk_bv_srem : bv_term -> bv_term -> bv_term

val mk_bv_smod : bv_term -> bv_term -> bv_term

val mk_bv_shl : bv_term -> bv_term -> bv_term

val mk_bv_ashr : bv_term -> bv_term -> bv_term

val mk_bv_lshr : bv_term -> bv_term -> bv_term

val mk_bl_equal : bl_term -> bl_term -> bl_term

val mk_bl_distinct : bl_term -> bl_term -> bl_term

val mk_bv_equal : bv_term -> bv_term -> bl_term

val mk_bv_distinct : bv_term -> bv_term -> bl_term

val mk_ax_equal : ax_term -> ax_term -> bl_term

val mk_ax_distinct : ax_term -> ax_term -> bl_term

val mk_bv_ult : bv_term -> bv_term -> bl_term

val mk_bv_ule : bv_term -> bv_term -> bl_term

val mk_bv_ugt : bv_term -> bv_term -> bl_term

val mk_bv_uge : bv_term -> bv_term -> bl_term

val mk_bv_slt : bv_term -> bv_term -> bl_term

val mk_bv_sle : bv_term -> bv_term -> bl_term

val mk_bv_sgt : bv_term -> bv_term -> bl_term

val mk_bv_sge : bv_term -> bv_term -> bl_term

val mk_bv_zero : bv_term

val mk_bv_one : bv_term

val mk_bv_zeros : int -> bv_term

val mk_bv_ones : int -> bv_term

val mk_bv_fill : int -> bv_term

val mk_bv_add_int : bv_term -> int -> bv_term

val mk_bv_sub_int : bv_term -> int -> bv_term

module VarSet : sig ... end

module BlVarSet : sig ... end

module BvVarSet : sig ... end

module AxVarSet : sig ... end

module BlVarHashtbl : sig ... end

module BvVarHashtbl : sig ... end

module AxVarHashtbl : sig ... end

module BlTermHashtbl : sig ... end

module BvTermHashtbl : sig ... end

module AxTermHashtbl : sig ... end

This module aim at generating well formatted smtlib2 formulas, taking in account some solvers differences (e.g: boolector not supporting function have arrays in parameters). All the strings generated by this module are smtlib 2 compliant.

val pp_status : Format.formatter -> Formula.status -> unit

pretty print the smt_result with a given color

val print_status : Formula.status -> string

returns
the string associated with a smt_result

val print_bv_unop : Formula.bv_unop -> string

returns
the string of an unary bitvector expression

val print_bv_bnop : Formula.bv_bnop -> string

returns
the string of a binary bitvector expression

val print_bv_comp : Formula.bv_comp -> string

returns
the string of a binary bitvector expression

val print_bv_term : Formula.bv_term -> string

returns
the string of a bitvector expression.

val print_ax_term : Formula.ax_term -> string

see print_bv_term

val print_bl_term : Formula.bl_term -> string

see print_bv_term

val print_varset : Formula.VarSet.t -> string

returns
the string formatting every input variable on a new line

val pp_varset : Format.formatter -> Formula.VarSet.t -> unit

val print_header : theory:string -> unit -> string

returns
the preformatted header

val pp_header : theory:string -> Format.formatter -> unit -> unit

val pp_as_comment : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a ->
  unit

val pp_bl_term : Format.formatter -> Formula.bl_term -> unit

val pp_bv_term : Format.formatter -> Formula.bv_term -> unit

val pp_ax_term : Format.formatter -> Formula.ax_term -> unit

val pp_term : Format.formatter -> Formula.term -> unit

val pp_entry : Format.formatter -> Formula.entry -> unit

val pp_formula : Format.formatter -> Formula.formula -> unit

module To_smtlib : sig ... end

Translation functions from BINSEC inner representation to SMT-LIB terms

module Transformation : sig ... end

module Model : sig ... end

Internal model representation

module Solver : sig ... end

Interface with SMT solvers

module Utils : sig ... end

Utility functions for formula creation

module Logger : sig ... end