package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

Dune Dependency

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

Authors

Maintainers

B

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

Sources

binsec-0.10.1.tbz

sha256=87d4048c9a90c8a14ee029e77d31032a15427f06416a31938cec8a68394234c4

sha512=6a023d2a5c87c56b0aac489874431d8dcccee1451a072a826190be3a7f75a961688bab95f193f494231744abc3bc9733ab5c809057d36a5e4d24c6c29c369144

doc/libterm/Libterm/Sexpr/Expr/index.html

Module `Sexpr.Expr`

include Binsec.Term.S with type a := string and type b := Memory.t

type nonrec size = Binsec.Term.size

type nonrec 'a interval = 'a Binsec.Term.interval = {

lo : 'a;
hi : 'a;

}

type nonrec endianness = Binsec.Term.endianness =

| LittleEndian
| BigEndian

type 'a op = 'a Binsec.Term.operator =

| Not : Binsec.Term.unary op
| Sext : size -> Binsec.Term.unary op
| Uext : size -> Binsec.Term.unary op
| Restrict : int interval -> Binsec.Term.unary op
| Plus : Binsec.Term.binary op
| Minus : _ op
| Mul : Binsec.Term.binary op
| Udiv : Binsec.Term.binary op
| Umod : Binsec.Term.binary op
| Sdiv : Binsec.Term.binary op
| Smod : Binsec.Term.binary op
| Or : Binsec.Term.binary op
| And : Binsec.Term.binary op
| Xor : Binsec.Term.binary op
| Concat : Binsec.Term.binary op
| Lsl : Binsec.Term.binary op
| Lsr : Binsec.Term.binary op
| Asr : Binsec.Term.binary op
| Rol : Binsec.Term.binary op
| Ror : Binsec.Term.binary op
| Eq : Binsec.Term.binary op
| Diff : Binsec.Term.binary op
| Ule : Binsec.Term.binary op
| Ult : Binsec.Term.binary op
| Uge : Binsec.Term.binary op
| Ugt : Binsec.Term.binary op
| Sle : Binsec.Term.binary op
| Slt : Binsec.Term.binary op
| Sge : Binsec.Term.binary op
| Sgt : Binsec.Term.binary op

type ('k, 'a, 'b) term = private ('k, 'a, 'b) Binsec.Term.t =

| Var : {
1. hash : int;
2. size : size;
3. name : string;
4. label : 'a;
} -> ([< `Var | `Loc | `Exp ], 'a, _) term
| Load : {
1. hash : int;
2. len : size;
3. dir : endianness;
4. mutable addr : ([ `Exp ], 'a, 'b) term;
5. label : 'b;
} -> ([< `Mem | `Loc | `Exp ], 'a, 'b) term
| Cst : Binsec.Bitvector.t -> ([< `Cst | `Exp ], _, _) term
| Unary : {
1. hash : int;
2. size : size;
3. f : Binsec.Term.unary Binsec.Term.operator;
4. mutable x : ([ `Exp ], 'a, 'b) term;
} -> ([< `Unary | `Exp ], 'a, 'b) term
| Binary : {
1. hash : int;
2. size : size;
3. f : Binsec.Term.binary Binsec.Term.operator;
4. mutable x : ([ `Exp ], 'a, 'b) term;
5. mutable y : ([ `Exp ], 'a, 'b) term;
} -> ([< `Binary | `Exp ], 'a, 'b) term
| Ite : {
1. hash : int;
2. size : size;
3. mutable c : ([ `Exp ], 'a, 'b) term;
4. mutable t : ([ `Exp ], 'a, 'b) term;
5. mutable e : ([ `Exp ], 'a, 'b) term;
} -> ([< `Ite | `Exp ], 'a, 'b) term

type t = ([ `Exp ], string, Memory.t) term

Smart constructors

val var : string -> size -> string -> t

var name bitsize label

val load : size -> endianness -> t -> Memory.t -> t

load nbytes endianness addr label

val constant : Binsec.Bitvector.t -> t

constant bv creates a constant expression from the bitvector bv.

val unary : Binsec.Term.unary op -> t -> t

unary f x creates a unary application of f on x.

val binary : Binsec.Term.binary op -> t -> t -> t

binary f x y creates a binary application of f on x and y.

val ite : t -> t -> t -> t

ite c t e creates an if-then-else expression c ? t : e.

val uminus : t -> t

val add : t -> t -> t

val sub : t -> t -> t

val mul : t -> t -> t

val smod : t -> t -> t

val umod : t -> t -> t

val udiv : t -> t -> t

val sdiv : t -> t -> t

val append : t -> t -> t

val equal : t -> t -> t

val diff : t -> t -> t

val ule : t -> t -> t

val uge : t -> t -> t

val ult : t -> t -> t

val ugt : t -> t -> t

val sle : t -> t -> t

val sge : t -> t -> t

val slt : t -> t -> t

val sgt : t -> t -> t

val logand : t -> t -> t

val logor : t -> t -> t

val lognot : t -> t

val logxor : t -> t -> t

val shift_left : t -> t -> t

val shift_right : t -> t -> t

val shift_right_signed : t -> t -> t

shift_(left|right) e q shifts expression e by quantity q, padding with zeroes

val rotate_left : t -> t -> t

val rotate_right : t -> t -> t

rotate_(left|right) e q rotates expression e by quantity q

val sext : size -> t -> t

sext sz e performs a signed extension of expression e to size sz

val uext : size -> t -> t

uext sz e performs an unsigned extension expression e to size sz

val restrict : lo:int -> hi:int -> t -> t

restrict lo hi e creates Dba.ExprUnary(Restrict(lo, hi), e) if hi >= lo && lo >=0 .

val bit_restrict : int -> t -> t

bit_restrict o e is restrict o o e

Specific constants

val zeros : int -> t

zeros n creates a constant expression of value 0 with length n

val ones : int -> t

ones n creates a constant expression of value 1 with length n. I.e.; it has (n - 1) zeros in binary.

val one : t

val zero : t

val addi : t -> int -> t

val addz : t -> Z.t -> t

Utils

*

val hash : t -> int

hash t returns the hash of t in constant time.

val is_equal : t -> t -> bool

val compare : t -> t -> int

val sizeof : t -> size

sizeof t returns the bit size of t in constant time.

val map : 
  (string -> int -> 'a -> t) ->
  (int -> Binsec.Machine.endianness -> t -> 'b -> t) ->
  (_, 'a, 'b) term ->
  t

val _unary : Binsec.Term.unary op -> t -> t

Raw constructors

_unary f x creates a unary application of f on x.

val _binary : Binsec.Term.binary op -> t -> t -> t

_binary f x y creates a binary application of f on x and y.

val _ite : t -> t -> t -> t

_ite c t e creates an if-then-else expression c ? t : e.