whitesymex.state module

class whitesymex.state.State(instructions: list[Instruction], labels: dict[int, int], stdin: Optional[deque[Value]], bitlength: int)

Bases: object

Represents the execution state.

ip

An integer representing instruction pointer/program counter.

stack

A deque for the execution stack.

callstack

A deque that stores return addresses as stack.

heap

A dictionary to store/retrieve values by indexes.

labels

A dictionary that maps labels to ip values.

instructions

A list that contains program instructions.

input

A deque to represent stdin. As long as this deque is not empty, inputs will be read from it. However, if it is empty, symbolic variables will be read automaticaly.

stdin

A list that contains inputs read so far.

stdout

A list that represents stdout.

var_to_type

A dictionary that maps variables to VarType values.

solver

A whitesymex.solver.Solver instance to store and solve path constraints.

operations

A dictionary that maps whitesymex.ops.Op values to respective methods.

clone() → whitesymex.state.State

Returns a copy of the state.

Properties are shallow copied except for instructions and labels which are not copied but shared between the clones.

concretize(buffer: list[Union[int, z3.ExprRef]] = None) → bytes

Converts given symbolic buffer to concrete bytes.

If the buffer is None, it concretizes stdin instead.

Parameters

buffer – A list that contains either bytes or symbolic variables.

Returns

Concretized buffer as bytes object.

classmethod create_entry_state(instructions: list[Instruction], stdin: list[Value] = None, bitlength: int = 24) → State

Returns an entry state for the Whitespace program.

Parameters

• instructions – A list of instructions.

• stdin – A list of ints or symbolic variables.

• bitlength – Length of symbolic bitvectors. If this value is None, unbounded symbolic integers are used instead of bitvectors.

property instruction: Optional[Instruction]

Current instruction pointed by ip.

If the ip points to a location that is out of program’s space, None is returned.

is_satisfiable() → bool

Returns whether the path constraints are satisfiable or not.

step() → list[State]

Single-steps the current state.

If the instruction is conditional and the condition is a symbolic expression, the state clones itself and single-steps both paths.

Returns

A list that contains the successor states.

class whitesymex.state.VarType(value)

Bases: enum.Enum

An enumeration.

CHAR = 1

NUMBER = 2