SymbolicExplorator

class tritondse.SymbolicExplorator(config: Config, loader: Loader = None, workspace: Workspace = None, executor_stop_at: int = None, seed_scheduler_class: Type[SeedScheduler] = None)

Symbolic Exploration. This class is in charge of iterating executions with the different seeds available in the workspace and generated along the way.

add_input_seed(seed: bytes | Seed) → None

Add the given bytes or Seed object as input for the exploration.

Parameters:

seed (Union[bytes, Seed]) – input seed to add in the pending inputs to process

property callback_manager: CallbackManager

CallbackManager global instance that will be transmitted to all SymbolicExecutor.

Return type:

CallbackManager

cbm: CallbackManager

CallbackManager to register callbacks

config: Config

Configuration file

coverage: GlobalCoverage

GlobalCoverage object holding information about the global coverage. (not really meant to be manipulated by the user)

current_executor: SymbolicExecutor | None

last symbolic executor executed

property execution_count: int

Get the number of execution performed.

Returns:

number of execution performed

Return type:

int

explore() → ExplorationStatus

Start the symbolic exploration. That function holds until the exploration is interrupted or finished.

Returns:

the status of the exploration

Return type:

ExplorationStatus

loader: Loader

Program being analyzed

post_exploration() → None

Perform all calls to post exploration functions

seeds_manager: SeedManager

Manager of seed, holding all seeds related data and various statistics

status: ExplorationStatus

status of the execution

step() → None

Perform a single exploration step. That means it execute a single SymbolicExecutor. Then it gives the hand back to the user.

stop_exploration() → None

Interrupt the exploration

terminate_exploration() → None

Terminate exploration with status terminated (normal shutdown)

property total_emulation_time: float

Represent total emulation time. This includes all callbacks execution but not the SMT solving time (performed at the end).

ts: float

Timestamp (object instantiation)

workspace: Workspace

workspace object

class tritondse.ExplorationStatus(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

Enum representing the current state of the exploration

IDLE = 2

NOT_RUNNING = 0

RUNNING = 1

STOPPED = 3

TERMINATED = 4

SeedManager

class tritondse.seed_manager.SeedManager(coverage: GlobalCoverage, workspace: Workspace, smt_queries_limit: int, callback_manager: CallbackManager = None, seed_scheduler_class: Type[SeedScheduler] = None)

Seed Manager. This class is in charge of providing the next seed to execute by prioritizing them. It also holds various sets of pending seeds, corpus, crashes etc. and manages them in the workspace.

It contains basically 2 types of seeds which are:

• pending seeds (kept in the seed scheduler). These are the seeds that might be selected to be run

• seed consumed (corpus, crash, hangs) which are seeds not meant to be re-executed as they cannot lead to new paths, all candidate paths are UNSAT etc.

Parameters:

• coverage (GlobalCoverage) – global coverage object. The instance will be updated by the seed manager

• workspace (Workspace) – workspace instance object.

• smt_queries_limit (int) – maximum number of queries for a given execution

• seed_scheduler_class (SeedScheduler) – seed scheduler class to use as scheduling strategy

add_new_seed(seed: Seed) → None

Add the given seed in the manager. The function uses its type to know where to add the seed.

Parameters:

seed (Seed) – seed to add

add_seed_queue(seed: Seed) → None

Add a seed to the appropriate internal queue depending on its status. If it is new it is added in pending seed, if OK, HANG or CRASH it the appropriate set. Note that the seed is not written in the workspace

Parameters:

seed (Seed) – Seed to add in an internal queue

archive_seed(seed: Seed, status: SeedStatus = None) → None

Send a seed in the corpus. As such, the seed is not meant to be used anymore (for finding new seeds).

Parameters:

• seed (Seed) – seed object

• status (SeedStatus) – optional status to assign the seed

drop_seed(seed: Seed) → None

Drop a seed that is not of interest anymore. The function thus switch its status to OK_DONE and move it in the corpus. (the seed is not removed from the corpus)

Parameters:

seed (Seed) – seed object to drop

is_new_seed(seed: Seed) → bool

Check if a seed is a new one (not into corpus, crash, hangs and fails)

Parameters:

seed (Seed) – The seed to test

Returns:

True if the seed is a new one

Warning

That function does not check that the seed is not in the pending seeds queue

pick_seed() → Seed | None

Get the next seed to be executed by querying it in the seed scheduler.

Returns:

Seed to execute from the pending seeds

Return type:

Seed

post_execution(execution: SymbolicExecutor, seed: Seed, solve_new_path: int = True) → float

Function called after each execution. It updates the global code coverage object, and tries to generate new paths through SMT in accordance with the seed scheduling strategy.

Parameters:

• execution (SymbolicExecutor) – The current execution

• seed (Seed) – The seed of the execution

• solve_new_path (bool) – Whether to solve constraint to find new paths

Returns:

Total SMT solving time

post_exploration() → None

Function called at the end of exploration. It performs some stats printing, but would also perform any clean up tasks. (not meant to be called by the user)

pp_meta_filename(covitem: int | Tuple[int, int] | str | Tuple[str, Tuple[int, int]], typ: SymExType) → str

pretty-print a covitem

seeds_available() → bool

Checks whether there is still pending seeds to process.

Returns:

True if seeds are still pending

property total_solving_time: float