P4C
The P4 Compiler
Loading...
Searching...
No Matches
targets/ebpf/cmd_stepper.h
1#ifndef TESTGEN_TARGETS_EBPF_CMD_STEPPER_H_
2#define TESTGEN_TARGETS_EBPF_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/ebpf/program_info.h"
16
17namespace P4::P4Tools::P4Testgen::EBPF {
18
19class EBPFCmdStepper : public CmdStepper {
20 protected:
21 std::string getClassName() override { return "EBPFCmdStepper"; }
22
23 const EBPFProgramInfo &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::EBPF
40
41#endif /* TESTGEN_TARGETS_EBPF_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
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
Definition targets/ebpf/cmd_stepper.h:19
void initializeTargetEnvironment(ExecutionState &nextState) const override
Definition targets/ebpf/cmd_stepper.cpp:37
std::string getClassName() override
Definition targets/ebpf/cmd_stepper.h:21
std::optional< const Constraint * > startParserImpl(const IR::P4Parser *parser, ExecutionState &nextState) const override
Definition targets/ebpf/cmd_stepper.cpp:62
std::map< Continuation::Exception, Continuation > getExceptionHandlers(const IR::P4Parser *parser, Continuation::Body normalContinuation, const ExecutionState &nextState) const override
Definition targets/ebpf/cmd_stepper.cpp:67
Definition targets/ebpf/program_info.h:15
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