Module `Exec.Start`Source

Parameters

module SF : Types.STATE_FACTORY

module W : Types.WORKLIST

Signature

Sourcetype time = {

mutable sec : float;

}

Sourcemodule Exploration_stats : Types.EXPLORATION_STATISTICS

Sourcemodule Query_stats : Types.QUERY_STATISTICS

Sourcemodule Screen : sig ... end

Sourcemodule State : sig ... end

Sourcetype label = [ `Label ] Fiber.t

Sourceand fiber = [ `All ] Fiber.t

Sourceand thunk = {

id : int;
depth : int;
scope : label;
fiber : fiber;
state : State.t;

}

Sourceand 'a mode =

| Default : unit mode
| Linear : State.t mode
| Merge : thunk mode

Sourcetype section =

| RX of {
1. base : Binsec.Virtual_address.t;
2. content : Binsec.Loader_buf.t;
}
| RWX

Sourcetype t = {

mutable code : section Binsec.Imap.t;
(*
set of executable sections
*)
rocache : label Binsec.Virtual_address.Htbl.t;
(*
instruction cache for RX sections
*)
cache : label OMap.t Binsec.Virtual_address.Htbl.t;
(*
instruction cache for RWX sections
*)
mutable worklist : thunk W.t;
(*
worklist of pending path
*)
mutable tid : int;
(*
the next unique task identifier
*)
tasks : unit Libsse.Types.I.Htbl.t;
(*
set of tasks to perform
*)

}

Sourceval env : t

Sourceval choose : unit -> thunk

Sourceval add : thunk -> unit

Sourceval halt : unit -> unit

Sourceval print : Binsec.Virtual_address.t -> State.t -> Types.Output.t -> unit

Sourceval disasm : Binsec.Virtual_address.t -> Binsec.Lreader.t -> [ `Label ] Fiber.t

Sourceexception Continue of label

Source

val exec : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  fiber ->
  'a

Source

val assume : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  [ `Assume ] Fiber.t ->
  'a

Source

val check : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  [ `Assert ] Fiber.t ->
  'a

Source

val ite : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  [ `Branch ] Fiber.t ->
  'a

Source

val dynamic_jump : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  [ `Jump ] Fiber.t ->
  'a

Source

val goto : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  Binsec.Virtual_address.t ->
  (bool * fiber) list ->
  fiber ->
  'a

Source

val transient_instruction : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  Binsec.Virtual_address.t ->
  'a

Sourceval yield : 'a. 'a mode -> max_depth:int -> 'a

Source

val probe : 
  'a. 'a mode ->
  int ->
  int ->
  max_depth:int ->
  State.t ->
  label ->
  [ `Probe ] Fiber.t ->
  'a

Sourceval initialize_state : unit -> [ `All ] Fiber.t * State.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/binsec.sse/Libsse/Exec/Start/index.html

Module `Exec.Start`Source

Parameters

Signature

package binsec

Install

Dune Dependency

Authors

Maintainers

Sources

doc/binsec.sse/Libsse/Exec/Start/index.html

Module Exec.StartSource

Parameters

Signature

Module `Exec.Start`Source