symbolic_executor.h

#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_ */