symbolic_executor.h

/*
 * SPDX-FileCopyrightText: 2023 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_SYMBOLIC_EXECUTOR_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_SYMBOLIC_EXECUTOR_H_
 
#include <functional>
#include <iosfwd>
#include <vector>
 
#include "ir/solver.h"
#include "midend/coverage.h"
 
#include "backends/p4tools/modules/testgen/core/program_info.h"
#include "backends/p4tools/modules/testgen/core/small_step/small_step.h"
#include "backends/p4tools/modules/testgen/lib/execution_state.h"
#include "backends/p4tools/modules/testgen/lib/final_state.h"
 
namespace P4::P4Tools::P4Testgen {

class SymbolicExecutor {
 public:
    virtual ~SymbolicExecutor() = default;
 
    SymbolicExecutor(const SymbolicExecutor &) = default;
 
    SymbolicExecutor(SymbolicExecutor &&) = delete;
 
    SymbolicExecutor &operator=(const SymbolicExecutor &) = delete;
 
    SymbolicExecutor &operator=(SymbolicExecutor &&) = delete;

    using Callback = std::function<bool(const FinalState &)>;
 
    using Branch = SmallStepEvaluator::Branch;
 
    using StepResult = SmallStepEvaluator::Result;

    virtual void run(const Callback &callBack);
 
    virtual void runImpl(const Callback &callBack, ExecutionStateReference executionState) = 0;
 
    explicit SymbolicExecutor(AbstractSolver &solver, const ProgramInfo &programInfo);

    void printCurrentTraceAndBranches(std::ostream &out, const ExecutionState &executionState);

    const P4::Coverage::CoverageSet &getVisitedNodes();

    [[nodiscard]] bool updateVisitedNodes(const P4::Coverage::CoverageSet &newNodes);
 
 protected:
    const ProgramInfo &programInfo;

    AbstractSolver &solver;

    const P4::Coverage::CoverageSet &coverableNodes;

    P4::Coverage::CoverageSet visitedNodes;

    bool handleTerminalState(const Callback &callback, const ExecutionState &terminalState);

    StepResult step(ExecutionState &state);

    static bool evaluateBranch(const SymbolicExecutor::Branch &branch, AbstractSolver &solver);

    //  Remove the branch from the container.
    static SymbolicExecutor::Branch popRandomBranch(
        std::vector<SymbolicExecutor::Branch> &candidateBranches);
 
 private:
    SmallStepEvaluator evaluator;
};
 
}  // namespace P4::P4Tools::P4Testgen
 
#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_SYMBOLIC_EXECUTOR_H_ */