whitesymex.strategies.strategy module

class whitesymex.strategies.strategy.Strategy(path_group: PathGroup, find: Callable[[State], bool], avoid: Callable[[State], bool], loop_limit: Optional[int], num_find: int = 1)

Bases: object

Strategy to select and step states during symbolic execution.

This class is supposed to be subclassed for each strategy.

path_group

A PathGroup instance to run the strategy.

find

A filter function to decide if a state should be marked as found.

avoid

A filter function to decide if a state should be avoided.

loop_limit

A maximum number of iterations for loops with a symbolic expression as a condition.

loop_counts

A dict mapping ip values of conditionals to hit counts.

num_find

Number of states to be found.

run()

Runs the symbolic execution with the strategy.

Returns if num_find states are found. Otherwise, runs until no active states left.

select_states() → list[State]

Selects states to be executed in the next iteration.

This function is supposed to be implemented in subclasses.

Returns

A list of states to be executed.

step(state: State) → Optional[list[State]]

Steps the given state.

The state is stepped until one of the followings happen:

• The state exits.

• The state throws an error.

• The state gets marked as found.

• The state gets marked as avoided.

• The state returns multiple successor states.

• The state hits the loop limit.

Parameters

state – A state to be stepped.

Returns

A list of successor states is returned. If the state is classified such as errored, found, avoided, or hits the loop limit, None is returned.

whitesymex.strategies.strategy.is_symbolic_conditional(state: State) → bool

Checks whether a state is on a symbolic conditional instruction.

A symbolic conditional is a conditional instruction that contains symbolic expressions in its condition.

Parameters

state – A state to be checked.

Returns

True if the current instruction is a symbolic conditional. Otherwise, returns False.