Seed Scheduling

Seed scheduling algorithm, are classes basically providing the next seed input to execute. They can be given to the tritondse.seed_manager.SeedManager constructor. The scheduling of seeds might be different depending on the need. All strategies should satisfy the interface defined by tritondse.seed_manager.SeedManager.

class tritondse.seed_scheduler.SeedScheduler

Abstract class for all seed selection strategies. This class provides the base methods that all subclasses should implement to be compliant with the interface.

add(seed: Seed) → None

Add a new seed in the scheduler

Parameters:

seed (Seed) – Seed to add in the scheduler

can_solve_models() → bool

Function called by the seed manager to know if it can start negating branches to discover new paths. Some seed scheduler might want to run concretely all inputs first before starting negating branches.

Returns:

true if the SeedManager can negate branches

has_seed_remaining() → bool

Returns true if there are still seeds to be processed in the scheduler

Returns:

true if there are seeds to process

pick() → Seed | None

Return the next seed to execute.

Returns:

seed to execute

Return type:

Seed

post_execution() → None

Called at the end of each execution after the generation of new seeds through SMT. Last thing called before starting the next iteration.

post_exploration(workspace: Workspace) → None

Called at the end of the exploration to perform some clean-up or anything else.

update_worklist(coverage: GlobalCoverage) → None

Call after every execution. That function might help the scheduler with some of its internal states. For instance the scheduler keep some seeds meant to cover an address which is now covered, it can just drop these seeds.

Parameters:

coverage (GlobalCoverage) – global coverage of the exploration

Existing strategies

class tritondse.seed_scheduler.FreshSeedPrioritizerWorklist(manager: SeedManager)

Bases: SeedScheduler

Strategy that first execute all seeds without negating branches in order to get the most updated coverage and which then re-run all relevant seeds to negate their branches.

This worklist works as follows:

• return first fresh seeds first to get them executed (to improve coverage)

• keep the seed in the worklist up until it gets dropped or thoroughly processed

• if no fresh seed is available, iterates seed that will generate coverage

__len__() → int

Number of pending seeds to execute

add(seed: Seed) → None

Add a seed to the worklist

Parameters:

seed (Seed) – seed to add to the scheduler

can_solve_models() → bool

Returns True if there are no “fresh” seeds to execute.

Returns:

True if all fresh seeds have been executed.

has_seed_remaining() → bool

Returns true if there are still seeds in the worklist

pick() → Seed | None

Return the next seed to execute

post_execution() → None

Solely used to show intermediate statistics

post_exploration(workspace: Workspace) → None

At the end of the execution, print the worklist to know its state before exit.

update_worklist(coverage: GlobalCoverage) → None

Update the coverage state of the worklist with the global one

class tritondse.seed_scheduler.WorklistAddressToSet(manager: SeedManager)

Bases: SeedScheduler

This worklist classifies seeds by addresses. We map a seed X to an address Y, if the seed X has been generated to reach the address Y. When the method pick() is called, seeds covering a new address ‘Y’ are selected first. Otherwise, anyone is taken.

__len__() → int

Number of pending seeds to execute

add(seed: Seed) → None

Add a seed to the worklist

can_solve_models() → bool

Always true. This strategy always allows solving branches. As a consequence it might try to solve a branch already covered in a seed not run yet. But this enables iterating a seed only once.

Returns:

True

has_seed_remaining() → bool

Returns true if there are still seeds in the worklist

pick() → Seed | None

Return the next seed to execute

Returns:

next seed to execute (first one covering new addresses, otherwise any other)

Return type:

Seed

post_execution() → None

Called at the end of each execution after the generation of new seeds through SMT. Last thing called before starting the next iteration.

post_exploration(workspace: Workspace) → None

Called at the end of the exploration to perform some clean-up or anything else.

update_worklist(coverage: GlobalCoverage) → None

Update the coverage state of the woklist with the global one

class tritondse.seed_scheduler.WorklistRand(manager: SeedManager)

Bases: SeedScheduler

Trivial strategy that returns any Seed without any classification. It uses a Set for insertion and pop (which is random) for picking seeds.

__len__() → int

Number of pending seeds to execute

add(seed: Seed) → None

Add a seed to the worklist

Parameters:

seed (Seed) – Seed to add to this rand scheduler

can_solve_models() → bool

Always true

has_seed_remaining() → bool

Returns true if there are still seeds in the worklist

pick() → Seed | None

Return the next seed to execute. The method pop() removes a random element from the set and returns the removed element. Unlike, a stack a random element is popped off the set.

Returns:

next seed to execute

Return type:

Seed

post_execution() → None

Called at the end of each execution after the generation of new seeds through SMT. Last thing called before starting the next iteration.

post_exploration(workspace: Workspace) → None

Called at the end of the exploration to perform some clean-up or anything else.

update_worklist(coverage: GlobalCoverage) → None

Update the coverage state of the worklist with the global one