small_step.h

/*
 * SPDX-FileCopyrightText: 2022 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_SMALL_STEP_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_SMALL_STEP_H_
 
#include <cstdint>
#include <functional>
#include <optional>
#include <utility>
#include <vector>
 
#include "backends/p4tools/common/compiler/reachability.h"
#include "ir/node.h"
#include "ir/solver.h"
#include "midend/coverage.h"
 
#include "backends/p4tools/modules/testgen/core/program_info.h"
#include "backends/p4tools/modules/testgen/lib/execution_state.h"
 
namespace P4::P4Tools::P4Testgen {

class SmallStepEvaluator {
    friend class CommandVisitor;
 
 public:
    struct Branch {
        const Constraint *constraint;
 
        ExecutionStateReference nextState;
 
        P4::Coverage::CoverageSet potentialNodes;

        explicit Branch(ExecutionState &nextState);

        Branch(std::optional<const Constraint *> c, const ExecutionState &prevState,
               ExecutionState &nextState);

        Branch(std::optional<const Constraint *> c, const ExecutionState &prevState,
               ExecutionState &nextState, P4::Coverage::CoverageSet potentialNodes);
    };
 
    using Result = std::vector<Branch> *;

    static constexpr uint64_t MAX_GUARD_VIOLATIONS = 100;
 
 private:
    const ProgramInfo &programInfo;

    AbstractSolver &solver;

    uint64_t violatedGuardConditions = 0;

    ReachabilityEngine *reachabilityEngine = nullptr;
 
    using REngineType = std::pair<ReachabilityResult, std::vector<SmallStepEvaluator::Branch> *>;
 
    static void renginePostprocessing(ReachabilityResult &result,
                                      std::vector<SmallStepEvaluator::Branch> *branches);
 
    REngineType renginePreprocessing(SmallStepEvaluator &stepper, const ExecutionState &nextState,
                                     const IR::Node *node);
 
 public:
    Result step(ExecutionState &state);
 
    SmallStepEvaluator(AbstractSolver &solver, const ProgramInfo &programInfo);
};
 
}  // namespace P4::P4Tools::P4Testgen
 
#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_SMALL_STEP_H_ */