package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module W : Types.WORKLIST

Signature

type time = {
  1. mutable sec : float;
}
module Screen : sig ... end
module State : sig ... end
type label = [ `Label ] Fiber.t
and fiber = [ `All ] Fiber.t
and thunk = {
  1. id : int;
  2. depth : int;
  3. scope : label;
  4. fiber : fiber;
  5. state : State.t;
}
and 'a mode =
  1. | Default : unit mode
  2. | Linear : State.t mode
  3. | Merge : thunk mode
type section =
  1. | RX of {
    1. base : Binsec.Virtual_address.t;
    2. content : Binsec.Loader_buf.t;
    }
  2. | RWX
type t = {
  1. mutable code : section Binsec.Imap.t;
    (*

    set of executable sections

    *)
  2. rocache : label Binsec.Virtual_address.Htbl.t;
    (*

    instruction cache for RX sections

    *)
  3. cache : label OMap.t Binsec.Virtual_address.Htbl.t;
    (*

    instruction cache for RWX sections

    *)
  4. mutable worklist : thunk W.t;
    (*

    worklist of pending path

    *)
  5. mutable tid : int;
    (*

    the next unique task identifier

    *)
  6. tasks : unit Libsse.Types.I.Htbl.t;
    (*

    set of tasks to perform

    *)
}
val env : t
val choose : unit -> thunk
val add : thunk -> unit
val halt : unit -> unit
val disasm : Binsec.Virtual_address.t -> Binsec.Lreader.t -> [ `Label ] Fiber.t
exception Continue of label
val exec : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> fiber -> 'a
val assume : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Assume ] Fiber.t -> 'a
val check : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Assert ] Fiber.t -> 'a
val ite : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Branch ] Fiber.t -> 'a
val dynamic_jump : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Jump ] Fiber.t -> 'a
val goto : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> Binsec.Virtual_address.t -> fiber list -> fiber -> 'a
val transient_instruction : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> Binsec.Virtual_address.t -> 'a
val yield : 'a. 'a mode -> max_depth:int -> 'a
val probe : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Probe ] Fiber.t -> 'a
val initialize_state : unit -> [ `All ] Fiber.t * State.t