final_state.h

/*
 * SPDX-FileCopyrightText: 2022 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_
 
#include <functional>
#include <optional>
#include <vector>
 
#include "backends/p4tools/common/lib/model.h"
#include "backends/p4tools/common/lib/trace_event.h"
#include "ir/solver.h"
#include "midend/coverage.h"
 
#include "backends/p4tools/modules/testgen/lib/concolic.h"
#include "backends/p4tools/modules/testgen/lib/execution_state.h"
 
namespace P4::P4Tools::P4Testgen {

class FinalState {
 private:
    std::reference_wrapper<AbstractSolver> solver;

    std::reference_wrapper<const ExecutionState> state;

    std::reference_wrapper<const Model> finalModel;

    std::vector<std::reference_wrapper<const TraceEvent>> trace;

    static void calculatePayload(const ExecutionState &executionState, Model &evaluatedModel);

    static Model &processModel(const ExecutionState &finalState, Model &model,
                               bool postProcess = true);
 
 public:
    FinalState(AbstractSolver &solver, const ExecutionState &finalState);

    FinalState(AbstractSolver &solver, const ExecutionState &finalState, const Model &finalModel);

    [[nodiscard]] std::optional<std::reference_wrapper<const FinalState>> computeConcolicState(
        const ConcolicVariableMap &resolvedConcolicVariables) const;

    [[nodiscard]] const Model &getFinalModel() const;

    [[nodiscard]] AbstractSolver &getSolver() const;

    [[nodiscard]] const ExecutionState *getExecutionState() const;

    [[nodiscard]] const std::vector<std::reference_wrapper<const TraceEvent>> *getTraces() const;

    [[nodiscard]] const P4::Coverage::CoverageSet &getVisited() const;
};
 
}  // namespace P4::P4Tools::P4Testgen
 
#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_ */