let initialization_callback = Some f registers the function f to be called to initialize the initial state.

It can be used to set the initial value of some Dba variables or declare new field in the path structure.

The function f is called before any instruction in the script. It will be called once and it is the only safe place to call Path.register_key.

let declaration_callback = Some f registers the handler f to perform new top level script commands (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 an Some state for the script commands it supports, None otherwise.

let instruction_callback = Some f registers the handler f to translate the new script instructions (Ast.Instr.t) to one or several micro-instruction (Ir), including new 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 an non empty instruction list for the script instructions it supports, [] otherwise.

let process_callback = Some f registers the funcion f to instrument the intermediate representation (Ir).

It can be used to automatically insert new micro-instructions, including new 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 Ir.GRAPH interface. It can add new micro-instructions with the functions insert_before and insert_list_before.

The function should only modify the newly disassembled part of the graph (is_new_vertex, iter_new_vertex). Inserting new instructions in an already visited part will result in an error.

The function should not insert instructions before an Instruction label. To instrument the Instruction labels, use the insert_before or insert_list_before function on the successor of the node.

let builtin_callback = Some f registers the function f in charge to resolve the handler of a given builtin.

The resolver f should return Some h for the builtins it supports, None 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 current program counter (Virtual_address);
• the per-path data (Path), including registered ones;
• the current instruction depth of the path (int);
• the current symbolic state (State).

It should return Ok state to continue the exploration along this path. Error status cuts the path and logs the given status. The special value Error Halt terminates the whole exploration.

The handler h is called each time the path reaches the given builtin.

let builtin_printer = Some f registers the custom printer f to format the new builtins in debug outputs.

The printer f should return true for the builtins it handles, false otherwise.

let at_exit_callback = Some f 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 result.