Module `Binsec_sse.Types`

type trilean = Binsec_kernel.Basic_types.Ternary.t =

| False
| True
| Unknown

type status = Metrics.status =

| Halt
| Cut
| Merged
| Stashed
| Unsatisfiable_assumption
| Assertion_failure
| Max_depth
| Enumeration_limit
| Unresolved_formula
| Non_executable_code
| Error of string

The reason a path execution ends (via Signal).

type 'path continuation =

| Continue of ([ `All ], 'path) fiber
(*
Reroutes the execution to the given low-level instructions.
*)
| Call of 'path -> 'path continuation * 'path continuation
(*
Call the given OCaml function. Then, when the function yields Return, evaluates the given continuation.
*)
| Tail_call of 'path -> 'path continuation
(*
Call the given OCaml function without altering the callstack.
*)
| Return
(*
Returns from a Call.
*)
| Return_to of ([ `All ], 'path) fiber
(*
Return from a Call but reroutes the execution to the given low-level instruction instead of the Call continuation.
*)
| Signal of status
(*
Ends the path execution.
If the status is Stashed, the excecution can be resumed with the function ENGINE.resume or a Merge request.
*)
| Fork of 'path continuation * 'path continuation
(*
Request for a path fork. The parent path will evaluate the first continuation while the child path will evaluate the second one.
*)
| Merge of 'path list * 'path continuation
(*
Request for a path merging. The symbolic engine will try to merge the current path with the given ones.
All the listed paths must have been paused with Signal Stashed.
The merge result will evaluate the given continuation. If a path can not be merged, it will evaluate the given continuation too.
*)

The return of a Ir.builtin Call.

and (_, 'path) fiber =

| Step : {
1. addr : Binsec_kernel.Virtual_address.t;
2. n : int;
3. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Step | `All ], 'path) fiber
| Assign : {
1. var : Binsec_kernel.Dba.Var.t;
2. rval : Binsec_kernel.Dba.Expr.t;
3. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Assign | `All ], 'path) fiber
| Clobber : {
1. var : Binsec_kernel.Dba.Var.t;
2. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Clobber | `All ], 'path) fiber
| Load : {
1. var : Binsec_kernel.Dba.Var.t;
2. base : string option;
3. dir : Binsec_kernel.Machine.endianness;
4. addr : Binsec_kernel.Dba.Expr.t;
5. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Load | `All ], 'path) fiber
| Store : {
1. base : string option;
2. dir : Binsec_kernel.Machine.endianness;
3. addr : Binsec_kernel.Dba.Expr.t;
4. rval : Binsec_kernel.Dba.Expr.t;
5. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Store | `All ], 'path) fiber
| Symbolize : {
1. var : Binsec_kernel.Dba.Var.t;
2. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Symbolize | `All ], 'path) fiber
| Apply : {
1. f : 'path -> unit;
2. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Apply | `All ], 'path) fiber
| Assume : {
1. test : Binsec_kernel.Dba.Expr.t;
2. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Assume | `All ], 'path) fiber
| Assert : {
1. test : Binsec_kernel.Dba.Expr.t;
2. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Assert | `All ], 'path) fiber
| Branch : {
1. test : Binsec_kernel.Dba.Expr.t;
2. mutable taken : ([ `All ], 'path) fiber;
3. mutable fallthrough : ([ `All ], 'path) fiber;
} -> ([< `Branch | `All ], 'path) fiber
| Goto : Binsec_kernel.Virtual_address.t -> ([< `Goto | `All ], 'path) fiber
| Jump : Binsec_kernel.Dba.Expr.t -> ([< `Jump | `All ], 'path) fiber
| Call : {
1. f : 'path -> 'path continuation;
2. mutable succ : ([ `All ], 'path) fiber;
} -> ([< `Call | `All ], 'path) fiber
| Tail_call : ('path -> 'path continuation) -> ([< `Tail_call | `All ], 'path) fiber

module type STATE = Binsec_sse.Symbolic.State.S

module type PATH = Binsec_sse.Symbolic.Path.S

type stage = Binsec_sse_loader.Disassembly.stage =

| Early
| Late

type 'a hook = {

scope : Binsec_kernel.Virtual_address.t Binsec_kernel.Interval.t option;
stage : stage;
callback : 'a;

}

A hook declaration as used by the extensions.

The hooks are evaluated in the following phase order: Fetch_hook, Decode_hook, Disasm_hook and Rewrite_hook.

Within the same phase, Early stage hooks are evaluated before Late stage hooks.

Within the same stage, hooks are evaluated in the order of insertion.

A hook is only active under a given scope (i.e range of addresses or None for always).

type 'a primitive =

| Unknown
| Apply of 'a -> unit
| Call of 'a -> 'a continuation

Return value of the Builtin_resolver callback.

type 'path extension =

| Initialization_callback of 'path -> unit
(*
Registers the function f to be called during initialization of the first path.
It can be used to set the initial value of some Dba variables in the state or initialize some fields in the path structure.
The function f is called only once and before any instruction in the script.
*)
| Fetch_hook of (Binsec_kernel.Virtual_address.t -> Binsec_sse.Ir.Graph.t option) hook
(*
Registers the hook h to be called each time a new virtual address in the scope is discovered.
Given the virtual address, the callback can return a new instruction graph (Ir.Graph.t) to hook this address.
If the graph ends with the Ir.EndOfHook builtin, the disassembly continues to proceed with the following hooks. Otherwise, the hook acts as a replacement and skips the subsequent ones.
The hooks of the same stage are evaluated in the same order they are inserted.
*)
| Decode_hook of (Binsec_kernel.Virtual_address.t -> int Binsec_kernel.Reader.t -> Binsec_sse.Ir.Graph.t option) hook
(*
Registers the hook h to be called each time a new virtual address in the scope is about to be decoded (after all fetch hooks).
Given the virtual address and the byte opcode (Reader.t), the callback can return a new instruction graph (Ir.Graph.t) to hook this address.
If the graph ends with the Ir.EndOfHook builtin, the disassembly continues to proceed with the following hooks. Otherwise, the hook acts as a replacement and skips the subsequent ones.
The hooks of the same stage are evaluated in the same order they are inserted.
*)
| Disasm_hook of (Binsec_kernel.Instruction.t -> Binsec_sse.Ir.Graph.t option) hook
(*
Registers the hook h to be called each time a new virtual address in the scope has been decoded (after all decode hooks).
Given the decoded instruction (Instruction.t), the callback can return a new instruction graph (Ir.Graph.t) to hook this address.
If the graph ends with the Ir.EndOfHook builtin, the disassembly continues to proceed with the following hooks. Otherwise, the hook acts as a replacement and skips the subsequent ones.
The hooks of the same stage are evaluated in the same order they are inserted.
*)
| Rewrite_hook of (Binsec_sse.Ir.Graph.t -> unit) hook
(*
Registers the hook h to be called each time a new virtual address in the scope is about to yield a instruction graph (Ir.Graph.t) (after all disasm hooks).
Given the instruction graph, the callback can modify it in place using the Ir.Graph interface (e.g. Ir.Graph.insert_before, Ir.Graph.insert_list_before, Ir.Graph.replace_node or Ir.Graph.append_node).
The hooks of the same stage are evaluated in the same order they are inserted.
*)
| Instrumentation_routine of Revision.t -> unit
(*
Registers the funcion f to instrument the intermediate representation (Ir).
It can be used to automatically insert new micro-instructions, including custom Ir.builtins at strategic points (e.g. memory access, branch conditions, etc.).
The function f is called each time the engine discover new assembly instructions. The function f can explore the new micro-instructions by using the Revision interface. It can add new micro-instructions with the functions Revision.insert_before and Revision.insert_list_before.
The function should only modify the newly disassembled part of the graph (Revision.is_new_vertex, Revision.iter_new_vertex). Inserting instructions in a previously visited part will raise Invalid_argument.
The function should not insert instructions before an Ir.opcode.Instruction label. To instrument the Ir.opcode.Instruction labels, use the Revision.insert_before or Revision.insert_list_before function on the successor of the node.
*)
| Grammar_extension of (unit, Binsec_script.obj, unit, unit, Binsec_script.obj Dyp.dyplexbuf) Dyp.dyp_action list
(*
A list of dypgen grammar rules (Dyp.dyp_action).
*)
| Instruction_resolver of Binsec_sse.Script.Ast.Instr.t -> Script.env -> Ir.fallthrough list
(*
Registers the handler f to translate custom script instructions (Script.Ast.Instr.t) to one or several micro-instruction (Ir.fallthrough), including custom Ir.builtins.
The handler f can use the parser environment (Script.env) to parse and resolve script expressions with Script.eval_loc and Script.eval_expr.
The handler f should return a non empty instruction list for the script instructions it supports, [] otherwise.
*)
| Instruction_printer of Format.formatter -> Binsec_sse.Script.Ast.Instr.t -> bool
(*
Registers the custom printer f to format the new script instruction (Script.Ast.Instr.t) in debug outputs.
The printer f should return true for the instructions it handles, false otherwise.
*)
| Command_handler of Binsec_sse.Script.Ast.t -> Script.env -> 'path -> bool
(*
Registers the handler f to perform custom top level script commands (Script.Ast.t).
The handler f can use the parser environment (Script.env) to parse and resolve script expressions with Script.eval_loc and Script.eval_expr.
The handler f should return true when the command has been treated, false otherwise.
*)
| Command_printer of Format.formatter -> Binsec_sse.Script.Ast.t -> bool
(*
Registers the custom printer f to format the new top level script commands (Script.Ast.t) in debug outputs.
The printer f should return true for the instructions it handles, false otherwise.
*)
| Builtin_resolver of Ir.builtin -> 'path primitive
(*
Registers the function f in charge to resolve the handler of a given Ir.builtin.
The resolver f should return Call h or Apply h for the builtins it supports, Unknown otherwise. It is called once per builtin occurrence in the intermediate representation (Ir).
It is an error to not handle a builtin added by the plugin.
The handler h has access to the path interface (PATH).
It should return Return to resume the exploration along this path. Signal status cuts the path and logs the given status.
The handler h is called each time the path reaches the given Ir.builtin.
*)
| Builtin_may_read of Ir.builtin -> Binsec_kernel.Dba_types.Var.Set.t option option
(*
Registers the knowledge provider f for custom Ir.builtins.
It must return Some k for the builtin it handles, None otherwise.
- k = Some set is the (overapproximated) set of all variables the builtin may access. It is an error to access a variable not listed here and may result in undefined value.
- k = None means any variable may be accessed.
*)
| Builtin_may_write of Ir.builtin -> Binsec_kernel.Dba_types.Var.Set.t option option
(*
Registers the knowledge provider f for custom Ir.builtins.
It must return Some k for the builtin it handles, None otherwise.
- k = Some set is the (overapproximated) set of all variables the builtin may modify. It is an error to modify a variable not listed here and may result in undefined value.
- k = None means any variable may be modified.
*)
| Builtin_must_write of Ir.builtin -> Binsec_kernel.Dba_types.Var.Set.t option
(*
Registers the knowledge provider f for custom Ir.builtins.
It must return Some set for the builtin it handles, None otherwise. set is the (underapproximated) set of the variables a builtin must overwrite. Previous values of these variables are deemed no longer reachable.
*)
| Builtin_printer of Format.formatter -> Ir.builtin -> bool
(*
Registers the custom printer f to format the custom Ir.builtins in debug outputs.
The printer f should return true when the Ir.builtin is treated, false otherwise.
*)
| Fork_callback of 'path -> 'path -> unit
(*
Registers the function f to be called when a path execution is about to fork.
It can be used to maintain invariants between the parent (first parameter) and the child (second parameter) paths.
*)
| Signal_callback of 'path -> status -> unit
(*
Registers the function f to be called when a path receives a signal. The status gives information about why the execution is interrupted.
*)
| Exit_callback of unit -> unit
(*
Registers the function f to be called when the exploration is about to terminate.
It can be used to output some global wise statistics or results.
*)

type ('value, 'model, 'state, 'path, 'a) field_id = ..

An identifier used to declare new field in the PATH structure via the PLUGIN interface.

A PATH.key to a value of type 'a can be queried with the function ENGINE.lookup if the related field is present in one PLUGIN.fields list. The type 'a can be anything, including a function, and may depend on the type parameters 'value, 'model, 'state and 'path.

For instance, the field PATH.models could have been added as follows.

type ('value, 'model, 'state, 'path, 'a) field_id +=
  | Models : ('value, 'model, 'state, 'path, 'model list) field_id

let fields _ =
  [
    Field
    {
      id = Models;
      default = [];
      copy = None;
      merge = Some (fun x y -> Some (List.append x y));
    };
  ]

and field =

| Field : {
1. id : ('value, 'model, 'state, 'path, 'a) field_id;
2. default : 'a;
3. copy : ('a -> 'a) option;
4. merge : ('a -> 'a -> 'a option) option;
} -> field

A field declaration used to declare new field in the PATH structure via the PLUGIN.fields list.

The declaration contain an identifier id (field_id), the default value, an optional copy function and an optional merge function.

The copy function is called each time a path is forked to create a new local copy of the field value (by default Fun.id).

The merge function is called each time two paths are about to merge. It returns Some when the field values are mergeable, and None otherwise (by default, it returns Some if both values are physically equal).

module type ENGINE = sig ... end

module type PLUGIN = sig ... end

module type EXTENSIONS = sig ... end

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/binsec.sse/Binsec_sse/Types/index.html

Module `Binsec_sse.Types`

package binsec

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/binsec.sse/Binsec_sse/Types/index.html

Module Binsec_sse.Types

dune-project
Dependency

Module `Binsec_sse.Types`