P4C
The P4 Compiler
Loading...
Searching...
No Matches
targets/bmv2/cmd_stepper.h
1#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_CMD_STEPPER_H_
2#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_CMD_STEPPER_H_
3
4#include <map>
5#include <optional>
6#include <string>
7
8#include "ir/ir.h"
9#include "ir/solver.h"
10
11#include "backends/p4tools/modules/testgen/core/program_info.h"
12#include "backends/p4tools/modules/testgen/core/small_step/cmd_stepper.h"
13#include "backends/p4tools/modules/testgen/lib/continuation.h"
14#include "backends/p4tools/modules/testgen/lib/execution_state.h"
15#include "backends/p4tools/modules/testgen/targets/bmv2/program_info.h"
16
18
20 protected:
21 std::string getClassName() override { return "Bmv2V1ModelCmdStepper"; }
22
23 const Bmv2V1ModelProgramInfo &getProgramInfo() const override;
24
25 void initializeTargetEnvironment(ExecutionState &nextState) const override;
26
27 std::optional<const Constraint *> startParserImpl(const IR::P4Parser *parser,
28 ExecutionState &nextState) const override;
29
30 std::map<Continuation::Exception, Continuation> getExceptionHandlers(
31 const IR::P4Parser *parser, Continuation::Body normalContinuation,
32 const ExecutionState &nextState) const override;
33
34 public:
37};
38
39} // namespace P4::P4Tools::P4Testgen::Bmv2
40
41#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_CMD_STEPPER_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:24
const ProgramInfo & programInfo
Target-specific information about the P4 program being evaluated.
Definition abstract_stepper.h:46
AbstractSolver & solver
The solver backing the state being executed.
Definition abstract_stepper.h:52
Definition targets/bmv2/cmd_stepper.h:19
void initializeTargetEnvironment(ExecutionState &nextState) const override
Definition targets/bmv2/cmd_stepper.cpp:43
std::map< Continuation::Exception, Continuation > getExceptionHandlers(const IR::P4Parser *parser, Continuation::Body normalContinuation, const ExecutionState &nextState) const override
Definition targets/bmv2/cmd_stepper.cpp:114
std::optional< const Constraint * > startParserImpl(const IR::P4Parser *parser, ExecutionState &nextState) const override
Definition targets/bmv2/cmd_stepper.cpp:104
std::string getClassName() override
Definition targets/bmv2/cmd_stepper.h:21
Definition targets/bmv2/program_info.h:15
Implements small-step operational semantics for commands.
Definition core/small_step/cmd_stepper.h:20
A continuation body is a list of commands.
Definition continuation.h:129
Represents state of execution after having reached a program point.
Definition execution_state.h:34
Stores target-specific information about a P4 program.
Definition core/program_info.h:21
Inja.
Definition targets/bmv2/cmd_stepper.cpp:33