[Updated]

Me, @CaelmBleidd and @denis-fokin came to this architecture:

After the refactoring the engine will consist of these main classes:

• [PathSelector]
• [Traverser]
• [SVM] stands for Symbolic Virtual Machine
• [SymbolicAnalyzer] (maybe there is a better name for this)
• [Engine]

All of them, except of [SVM], work with the objects of type ExecutionState.

ExecutionState

ExecutionState is a base entity of analysis step.
Internally, it is a sealed class with possible successors:

• SymbolicExecutionState is an intermediate state suitable for further analysis. It has a SymbolicState field and some other info, e.g. ExecutionStack. Maybe IntermidiateExecutionState is a better name for this.
• TerminalExecutionState is a terminal state from which we might (or might not) execute concretely and construct UtExecution. This state represents the final state of the program execution, that is a throw or return from the outer method.
• ConcreteExecutionState is a state which is not suitable for further symbolic analysis and it is also not a terminal state. Such states are only suitable for a concrete execution and may appear from Assumptions constraints.
• Any other kind of state in future

PathSelector

[PathSelector] is responsible for choosing the ExecutionState for analysis. Basically, it has very simple API:

• Add new state
• Poll the next state

We can use different algorithms for selecting and prioritizing states depending on what we want to do (e.g. cover all the branches, find deep NPEs, reach to the end as fast as possible, etc.)

Traverser

[Traverser] is responsible for producing new ExecutionStates from a SymbolicExecutionState. It traverses the top-level stmt, resolves it and produces the following states. They might be of any type.

Traverser is bound to a specific method processing and cannot be reused between different methods. Internally, [Traverser] uses
another class [SVM] (stands for Symbolic Virtual Machine) to handle the SymbolicState updating.

SVM

[SVM] is responsible for working with SymbolicState which consists of Memory and PathConstraint. It has a predefined API for updating SymbolicState, including createObject, createField, etc.

SymbolicAnalyzer

[SymbolicAnalyzer] is responsible only for symbolic analysis of our method. It handles one iteration of processing loop and deals with [PathSelector] and [Traverser]. [SymbolicAnalyzer] is an iterator-like object, and it has these methods:

• hasNext(): Boolean -- checks if there are more ExecutionStates
• pollState(): ExecutionState -- takes the state from the [PathSelector], passes it to the [Traverser] and pushes the new states to the [PathSelector]. The state obtained from the queue returned as a result. Very similar to Cold Flow. Maybe it's better to divide this into two methods.

Engine

The [Engine] class manages the control flow of our engine:

• pushes the initial state to [SymbolicAnalyzer]
• while (!symbolicAnalyzer.hasNext()) loop
• processes states:
  • resolves SymbolicState to the models, executes them concretely
  • does whatever he wants in other scenarios (e.g. in ModelSynthesis scenario just adds checks if the ExecutionState satisfies postcondition)

Decomposition of the previous Engine into the [SymbolicAnalyzer] and [Engine] allows:

• using different strategies for working with the states at the final phase
• testing these classes independently

Sequence Diagram

of one iteration of while (!symbolicAnalyzer.hasNext()) loop

sequenceDiagram
    participant Engine
    participant SymbolicAnalyzer
    participant PathSelector
    participant Traverser
    participant SVM

    note right of Engine: one iteration of the inner<br>while (symbolicAnalyzer.hasNext()) loop

    Engine->>+SymbolicAnalyzer: poll state

    SymbolicAnalyzer->>+PathSelector: poll state
    PathSelector-->>-SymbolicAnalyzer: [ExecutionState]

    opt If the state type is [SymbolicExecutionState]
        SymbolicAnalyzer->>+Traverser: traverse [SymbolicExecutionState]
        note left of Traverser: Here we traverse top-level stmt and<br> create new ExecutionStates<br>with the help of SVM
        loop For each possible branch
            Traverser->>+SVM: Previous SymbolicState + updates
            note left of SVM: The actual work with SymbolicMemory<br> and PathConstraints happens here
            SVM-->>-Traverser: new SymbolicState
            note left of Traverser: ExecutionState with updated<br> SymbolicState is created
        end

        Traverser-->>-SymbolicAnalyzer: new [ExecutionState]s
        note left of Traverser: these states can be of any type:<br> symbolic, terminal, concrete
        
        loop For each new state produced from the polled state
            SymbolicAnalyzer->>+PathSelector: add new [ExecutionState]
            PathSelector-->>-SymbolicAnalyzer: ok 
        end
    end

    SymbolicAnalyzer-->>-Engine: the polled [Execution state]

    note right of Engine: Switch on state type
    alt is SymbolicExecutionState
        note right of Engine: ignores this state, because we already added all<br> successors in SymbolicAnalyser 
    else is TerminalState
        Engine->>Engine: process [TerminalExecutionState]
        note right of Engine: usually here we construct models from symbolic variables,<br>call concrete executor and return UtExecution,<br>but this behavior can be overriden
    else is ConcreteExecutionState
        Engine->>Engine: process [ConcreteExecutionState]
        note right of Engine: usually here we do the same as above, except constructing<br> models for stateAfter and result, but it can be overriden
    end

Feedback and suggestions are appreciated.