Struct SymbolicProgramState<TInstruction>

Namespace

Echo.DataFlow.Emulation

Assembly

Echo.DataFlow.dll

Represents an immutable snapshot of a program state that is fully symbolic.

public readonly struct SymbolicProgramState<TInstruction> where TInstruction : notnull

Type Parameters

TInstruction

The type of instructions.

Inherited Members

ValueType.Equals(object)

ValueType.GetHashCode()

object.Equals(object, object)

object.GetType()

object.ReferenceEquals(object, object)

Constructors

SymbolicProgramState(long)

Creates a new empty program state, initialized at the provided program counter.

public SymbolicProgramState(long programCounter)

Parameters

programCounter long

The initial program counter.

SymbolicProgramState(long, ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>)

Creates a new empty program state, initialized at the provided program counter.

public SymbolicProgramState(long programCounter, ImmutableDictionary<IVariable, SymbolicValue<TInstruction>> variables)

Parameters

programCounter long

The initial program counter.

variables ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>

The initial state of the variables.

SymbolicProgramState(long, ImmutableStack<SymbolicValue<TInstruction>>)

Creates a new empty program state, initialized at the provided program counter.

public SymbolicProgramState(long programCounter, ImmutableStack<SymbolicValue<TInstruction>> stack)

Parameters

programCounter long

The initial program counter.

stack ImmutableStack<SymbolicValue<TInstruction>>

The initial stack state.

SymbolicProgramState(long, ImmutableStack<SymbolicValue<TInstruction>>, ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>)

Creates a new empty program state, initialized at the provided program counter.

public SymbolicProgramState(long programCounter, ImmutableStack<SymbolicValue<TInstruction>> stack, ImmutableDictionary<IVariable, SymbolicValue<TInstruction>> variables)

Parameters

programCounter long

The initial program counter.

stack ImmutableStack<SymbolicValue<TInstruction>>

The initial stack state.

variables ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>

The initial state of the variables.

Properties

Empty

Gets an empty program state.

public static SymbolicProgramState<TInstruction> Empty { get; }

Property Value

SymbolicProgramState<TInstruction>

ProgramCounter

Gets the current value of the program counter that points to the instruction to be executed next.

public long ProgramCounter { get; }

Property Value

long

Stack

Gets the current stack state of the program.

public ImmutableStack<SymbolicValue<TInstruction>> Stack { get; }

Property Value

ImmutableStack<SymbolicValue<TInstruction>>

Variables

Gets the current variable state of the program.

public ImmutableDictionary<IVariable, SymbolicValue<TInstruction>> Variables { get; }

Property Value

ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>

Methods

MergeStates(in SymbolicProgramState<TInstruction>, out SymbolicProgramState<TInstruction>)

Merges two program states together, combining all data sources.

public bool MergeStates(in SymbolicProgramState<TInstruction> otherState, out SymbolicProgramState<TInstruction> newState)

Parameters

otherState SymbolicProgramState<TInstruction>

The other program state to merge with.

newState SymbolicProgramState<TInstruction>

The newly created state.

Returns

bool

true if the state has changed, false otherwise.

Exceptions

ArgumentException

Occurs when the program counters do not match.

StackImbalanceException

Occurs when the stack heights do not match.

Pop(out SymbolicValue<TInstruction>)

Copies the current state and pops the top value from the stack.

public SymbolicProgramState<TInstruction> Pop(out SymbolicValue<TInstruction> value)

Parameters

value SymbolicValue<TInstruction>

The popped value.

Returns

SymbolicProgramState<TInstruction>

The new program state.

Exceptions

StackImbalanceException

Occurs when the stack is empty.

Push(SymbolicValue<TInstruction>)

Copies the current state and pushes a new value onto the stack.

public SymbolicProgramState<TInstruction> Push(SymbolicValue<TInstruction> value)

Parameters

value SymbolicValue<TInstruction>

The new value.

Returns

SymbolicProgramState<TInstruction>

The new program state.

ToString()

public override string ToString()

Returns

string

WithProgramCounter(long)

Copies the current state and moves the program counter of the copy to the provided address.

public SymbolicProgramState<TInstruction> WithProgramCounter(long programCounter)

Parameters

programCounter long

The new program counter.

Returns

SymbolicProgramState<TInstruction>

The new program state.

WithStack(ImmutableStack<SymbolicValue<TInstruction>>)

Copies the current state and replaces the stack state with a new one.

public SymbolicProgramState<TInstruction> WithStack(ImmutableStack<SymbolicValue<TInstruction>> stack)

Parameters

stack ImmutableStack<SymbolicValue<TInstruction>>

The new stack state.

Returns

SymbolicProgramState<TInstruction>

The new program state.

WithVariables(ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>)

Copies the current state and replaces the variables state with a new one.

public SymbolicProgramState<TInstruction> WithVariables(ImmutableDictionary<IVariable, SymbolicValue<TInstruction>> variables)

Parameters

variables ImmutableDictionary<IVariable, SymbolicValue<TInstruction>>

The new variables state.

Returns

SymbolicProgramState<TInstruction>

The new program state.