SymbolicExecutor

class tritondse.SymbolicExecutor(config: ~tritondse.config.Config, seed: ~tritondse.seed.Seed = <tritondse.seed.Seed object>, workspace: ~tritondse.workspace.Workspace = None, uid=0, callbacks=None)

Single Program Execution Class. That module, is in charge of performing the process loading from the given program.

Parameters:

• config (Config) – configuration file to use

• seed (Seed) – input file to inject either in stdin or argv (optional)

• workspace (Optional[Workspace]) – Workspace to use. If None it will be instantiated

• uid (int) – Unique ID. Given by SymbolicExplorator to identify uniquely executions

• callbacks (CallbackManager) – callbacks to bind on this execution before running (instanciated if empty !)

abort() → NoReturn

Abort the current execution. It works by raising an exception which is caught by the emulation function that takes care of returning appropriately afterward.

Raises:

AbortExecutionException – to abort execution from anywhere

property callback_manager: CallbackManager

Get the callback manager associated with the execution.

Return type:

CallbackManager

cbm: CallbackManager

callback manager

config: Config

Configuration file used

coverage: CoverageSingleRun

Coverage of the execution

current_pc

current program counter

emulate()

emulation_deinit()

emulation_init() → bool

end_time: int

end time of the process

enqueue_seed(seed: Seed) → None

Add a seed to the queue of seed to be executed in later iterations. This function is meant to be used by user callbacks.

Parameters:

seed (Seed) – Seed to be added

property execution_time: int

Time taken for the execution in seconds

Warning

Only relevant at the end of the execution

Returns:

execution time (in s)

property exitcode: int

Exit code value of the process. The value is simply the concrete value of the register marked as return_register (rax, on x86, r0 on ARM..)

inject_symbolic_argv_memory(addr: int, index: int, value: bytes) → None

Inject the ith item of argv in memory. To be used only with composite seeds and only if seed have a symbolic argv

Parameters:

• addr – address where to inject the argv[ith]

• index – ith argv item

• value – value of the item

inject_symbolic_file_memory(addr: int, name: str, value: bytes, offset: int = 0) → None

Inject a symbolic file (or part of it) in memory.

Parameters:

• addr – address where to inject the file bytes

• name – name of the file in the composite seed

• value – bytes content of the file

• offset – offset within the file (for partial file injection)

inject_symbolic_file_register(reg: str | Register, name: str, value: int, offset: int = 0) → None

Inject a symbolic file (or part of it) into a register. The value has to be an integer. The caller has add constraints to the associated symbolic expression so when a model is obtained the resulting value fits in a byte.

Parameters:

• reg – register identifier

• name – name of the file in the composite seed

• value – integer value

• offset – offset within the file

inject_symbolic_raw_input(addr: int, data: bytes, offset: int = 0) → None

Inject the input in memory. This injection method should be used for RAW seed type.

Parameters:

• addr – address where to inject input.

• data – content of the seed

• offset – offset within the content of the seed.

inject_symbolic_variable_memory(addr: int, name: str, value: bytes, offset: int = 0) → None

Inject a symbolic variable in memory.

Parameters:

• addr – address where to inject the variable

• name – name of the variable in the composite seed

• value – value of the variable

• offset – offset within the variable (for partial variable injection)

Returns:

inject_symbolic_variable_register(reg: str | Register, name: str, value: int) → None

Inject a symbolic variable (or part of it) in a register. The value has to be an integer.

Parameters:

• reg – register identifier

• name – name of the variable

• value – integer value

is_seed_injected() → bool

Get whether the seed has been injected.

Returns:

True if the seed has already been inserted

load(loader: Loader) → None

Use the given loader to initialize the ProcessState. It overrides the current ProcessState if any.

Parameters:

loader – Loader describing how to load

Returns:

None

load_process(pstate: ProcessState) → None

Load the given process state. Do nothing but setting the internal ProcessState.

Parameters:

pstate – ProcessState to set

loader: Type[Loader] | None

Loader used to run the code

static mem_usage_str() → str

Debug function to track memory consumption of an execution (not implemented on Windows).

mk_new_seed_from_model(model: Model) → Seed

Creates a new seed from the given SMT model.

Parameters:

model – SMT model

Returns:

new seed object

property pending_seeds: List[Seed]

List of pending seeds gathered during execution.

Warning

Only relevant at the end of execution

Returns:

list of new seeds generated

Return type:

List[Seed]

previous_pc: int

previous program counter executed

pstate: ProcessState | None

ProcessState

run(stop_at: int = None) → None

Execute the program.

If the tritondse.Config.execution_timeout is not set the execution might hang forever if the program does.

Parameters:

stop_at – Address where to stop (if necessary)

Returns:

None

seed: Seed

The current seed used for the execution

skip_instruction() → NoReturn

Skip the current instruction before it gets executed. It is only relevant to call it from pre-inst or pre-addr callbacks.

Raises:

SkipInstructionException – to skip the current instruction

start_time: int

start time of the process

step() → bool

Perform a single instruction step. Returns whether the emulation can continue or we have to stop.

stop_exploration() → NoReturn

Function to call to stop the whole exploration of the program. It raises an exception which is caught by SymbolicExplorator.

Raises:

StopExplorationException – to stop the exploration

symbolic_seed

symbolic seed (same structure than Seed but with symbols)

trace_offset: int

counter of instructions executed

uid: int

Unique identifier meant to unique accross Exploration instances

workspace: Workspace

workspace object