P4C
The P4 Compiler
Loading...
Searching...
No Matches
targets/ebpf/expr_stepper.h
1#ifndef TESTGEN_TARGETS_EBPF_EXPR_STEPPER_H_
2#define TESTGEN_TARGETS_EBPF_EXPR_STEPPER_H_
3
4#include <string>
5
6#include "ir/ir.h"
7#include "ir/solver.h"
8
9#include "backends/p4tools/modules/testgen/core/program_info.h"
10#include "backends/p4tools/modules/testgen/core/small_step/expr_stepper.h"
11#include "backends/p4tools/modules/testgen/lib/execution_state.h"
12
13namespace P4::P4Tools::P4Testgen::EBPF {
14
16 private:
18 static const ExternMethodImpls<EBPFExprStepper> EBPF_EXTERN_METHOD_IMPLS;
19
20 protected:
21 std::string getClassName() override { return "EBPFExprStepper"; }
22
23 public:
25
26 void evalExternMethodCall(const ExternInfo &externInfo) override;
27
28 bool preorder(const IR::P4Table * /*table*/) override;
29
31 static const IR::MethodCallStatement *produceEmitCall(const IR::Member *fieldLabel);
32};
33} // namespace P4::P4Tools::P4Testgen::EBPF
34
35#endif /* TESTGEN_TARGETS_EBPF_EXPR_STEPPER_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:24
ExecutionState & state
The state being evaluated.
Definition abstract_stepper.h:49
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/ebpf/expr_stepper.h:15
std::string getClassName() override
Definition targets/ebpf/expr_stepper.h:21
void evalExternMethodCall(const ExternInfo &externInfo) override
Definition targets/ebpf/expr_stepper.cpp:181
static const IR::MethodCallStatement * produceEmitCall(const IR::Member *fieldLabel)
Represents state of execution after having reached a program point.
Definition execution_state.h:34
Encapsulates a set of extern method implementations.
Definition core/small_step/expr_stepper.h:27
Implements small-step operational semantics for expressions.
Definition core/small_step/expr_stepper.h:20
Definition extern_info.h:14
Stores target-specific information about a P4 program.
Definition core/program_info.h:21