package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

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

Authors

  1. A
    Adel Djoudi
  2. B
    Benoit Boero
  3. B
    Benjamin Farinier
  4. C
    Chakib Foulani
  5. D
    Dorian Lesbre
  6. F
    Frédéric Recoules
  7. G
    Guillaume Girol
  8. J
    Josselin Feist
  9. L
    Lesly-Ann Daniel
  10. M
    Mahmudul Faisal Al Ameen
  11. M
    Manh-Dung Nguyen
  12. M
    Mathéo Vergnolle
  13. M
    Matthieu Lemerre
  14. N
    Nicolas Bellec
  15. O
    Olivier Nicole
  16. R
    Richard Bonichon
  17. R
    Robin David
  18. S
    Sébastien Bardin
  19. S
    Soline Ducousso
  20. T
    Ta Thanh Dinh
  21. Y
    Yaëlle Vinçont
  22. Y
    Yanis Sellami

Maintainers

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

Sources

binsec-0.11.1.tbz
sha256=bb48234a4b60a872015a88282df4873f01dcc984753d49ad2583d49c1ae7d705
sha512=e8aa47a736b83bfd47d5b5e96d0988859b4873ad4a112fee7cd21d02bc72ecec61b7de610a959e38d2f2f5eef8082a2c100c201e5eae5ae3a880c747dce6ae63

doc/binsec.base/Binsec_base/Bitvector/index.html

Module Binsec_base.BitvectorSource

Sourcemodule type Common = sig ... end

Bitvector representation

Sourcetype t
include Common with type t := t and type boolean = bool
Sourceval create : Z.t -> int -> t
Sourceval create_from_tuple : (Z.t * int) -> t
Sourceval value_of : t -> Z.t
Sourceval signed_of : t -> Z.t
Sourceval size_of : t -> int
Sourceval ucompare : t -> t -> int

ucompare t t' returns the comparison of the unsigned values of t and t'.

It is equivalent of Z.compare (value_of t) (value_of t').

The bitvector t and t' should be of the same size.

Sourceval scompare : t -> t -> int

scompare t t' returns the comparison of the signed values of t and t'.

It is equivalent of Z.compare (signed_of t) (signed_of t').

The bitvector t and t' should be of the same size.

Sourceval zero : t
Sourceval one : t
Sourceval zeros : int -> t
Sourceval ones : int -> t
Sourceval fill : ?lo:int -> ?hi:int -> int -> t

fill lo hi n returns a bitvector of size n where bits from lo to hi are set to one. By default, lo is equal to zero and hi is equal to n. Raise Invalid_argument if lo or hi have incoherent values.

Sourceval is_zero : t -> bool
Sourceval is_one : t -> bool

is_zero t (resp. is_one t) checks if t is equal to zero (resp. one)

Sourceval is_zeros : t -> bool
Sourceval is_ones : t -> bool
Sourceval is_fill : t -> bool

is_zeros t (resp. is_ones t) checks if it exists n such that t is equal to zeros n (resp. ones n)

Sourceval max_ubv : int -> t
Sourceval max_sbv : int -> t
Sourceval min_sbv : int -> t

max_ubv n (resp. max_sbv n) returns a bitvector of size n containing the biggest possible unsigned (resp. signed) value for its size

Sourceval is_max_ubv : t -> bool
Sourceval is_max_sbv : t -> bool
Sourceval is_min_sbv : t -> bool

is_max_ubv t (resp. is_max_sbv t) returns true if t is a bitvector containing the biggest possible unsigned (resp. signed) value for its size, or returns false otherwise

include Sigs.COMPARISON with type t := t and type boolean = bool with type boolean = bool
Sourcetype boolean = bool
Sourceval diff : t -> t -> boolean
Sourceval ule : t -> t -> boolean
Sourceval uge : t -> t -> boolean
Sourceval ult : t -> t -> boolean
Sourceval ugt : t -> t -> boolean
Sourceval sle : t -> t -> boolean
Sourceval sge : t -> t -> boolean
Sourceval slt : t -> t -> boolean
Sourceval sgt : t -> t -> boolean
include Sigs.ARITHMETIC with type t := t
Sourceval add : t -> t -> t
Sourceval sub : t -> t -> t
Sourceval mul : t -> t -> t
Sourceval neg : t -> t
Sourceval udiv : t -> t -> t
Sourceval umod : t -> t -> t
Sourceval urem : t -> t -> t
Sourceval sdiv : t -> t -> t
Sourceval smod : t -> t -> t
Sourceval srem : t -> t -> t
Sourceval pow : t -> t -> t
Sourceval succ : t -> t
Sourceval pred : t -> t
Sourceval add_int : t -> int -> t
Sourceval umax : t -> t -> t
Sourceval umin : t -> t -> t
Sourceval smax : t -> t -> t
Sourceval smin : t -> t -> t
Sourceval is_neg : t -> bool
Sourceval is_pos : t -> bool

is_neg t (resp. is_pos t) returns true if the signed interpretation of t is strictly negative (resp. strictly positive)

include Sigs.BITWISE with type t := t
include Sigs.EXTENDED_LOGICAL with type t := t
include Sigs.LOGICAL with type t := t
Sourceval logand : t -> t -> t
Sourceval logor : t -> t -> t
Sourceval lognot : t -> t
Sourceval logxor : t -> t -> t
include Sigs.SHIFT_ROT with type t := t and type index := int
Sourceval shift_left : t -> int -> t
Sourceval shift_right : t -> int -> t
Sourceval shift_right_signed : t -> int -> t
Sourceval rotate_left : t -> int -> t
Sourceval rotate_right : t -> int -> t
Sourceval reduce : t -> int -> t
Sourceval extend : t -> int -> t
Sourceval extend_signed : t -> int -> t
Sourceval extend_unsafe : t -> int -> t
Sourceval num_bits : t -> int
Sourceval get_bit : t -> int -> bool
Sourceval set_bit : t -> int -> t
Sourceval clear_bit : t -> int -> t
Sourceval flip_bit : t -> int -> t
Sourceval append : t -> t -> t
Sourceval concat : t list -> t

concat bv1, bv2, ..., bvn is bv1 @ bv2 @ ... @ bvn

Sourceval extract : hi:int -> lo:int -> t -> t

Creation functions

Sourceval rand : int -> t

rand sz creates a bitvector of size sz with random value

Sourceval of_bool : bool -> t
Sourceval to_bool : t -> bool
Sourceval of_char : char -> t
Sourceval to_char : t -> char
Sourceval of_int32 : int32 -> t

of_int32 n creates a bitvector of size 32 and value n

Sourceval to_int32 : t -> int32
Sourceval of_int64 : int64 -> t

of_int64 n creates a bitvector of size 64 and value n

Sourceval to_int64 : t -> int64
Sourceval of_int : size:int -> int -> t
Sourceval to_int : t -> int
Sourceval to_uint : t -> int
Sourceval of_bits : string -> t

of_bits s cast an ascii string s to its bitvector representation.

Sourceval of_string : string -> t

of_string s converts a string s whose format respects (+-)?0xb0-9+ i.e., hex and bin strings

Otherwise raises Invalid_argument

Sourceval to_string : t -> string

to_string s converts a bitvector to hexadecimal notation (if size is a multiple of 4) or to binary (otherwise).

Sourceval of_hexstring : string -> t

of_hexstring is an alias for of_string

Sourceval to_bitstring : t -> string

to_bitstring bv returns the binary string representation of bv, i.e., the string "0b"[01]+ with the same value and size as bv.

Sourceval to_hexstring : t -> string

to_hexstring bv returns the hex string representation of bv, i.e., the string "0x"[0-9a-f]+ with the same value and size as bv.

Sourceval to_asciistring : t -> string

to_asciistring bv returns the ascii string representation of bv.

Printing functions

Sourceval pp : Format.formatter -> t -> unit

pp ppf bv prints the decimal value of bv into ppf

Sourceval pp_hex : Format.formatter -> t -> unit

pp_hex ppf bv prints the hexadecimal value of bv into ppf

Sourceval pp_hex_or_bin : Format.formatter -> t -> unit

pp_hex ppf bv prints the hexadecimal value of bv into ppf if possible, else prints the binary value of bv.

Sourceval print : t -> string

print bv behaves like pp Format.str_formatter bv; Format.flush_str_formatter ()

include Collection.S with type t := t
include Sigs.HASHABLE with type t := t
include Sigs.COMPARABLE with type t := t
Sourceval compare : t -> t -> int
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourcemodule Map : sig ... end
Sourcemodule Set : sig ... end
Sourcemodule Htbl : sig ... end