P4C
The P4 Compiler
 
Loading...
Searching...
No Matches
target.h
1#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_
2#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_
3
4#include <cstdint>
5#include <filesystem>
6#include <optional>
7
8#include "backends/p4tools/common/lib/arch_spec.h"
9#include "ir/ir.h"
10#include "ir/solver.h"
11
12#include "backends/p4tools/modules/testgen/core/program_info.h"
13#include "backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h"
14#include "backends/p4tools/modules/testgen/core/target.h"
15#include "backends/p4tools/modules/testgen/lib/execution_state.h"
16#include "backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.h"
17#include "backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.h"
18#include "backends/p4tools/modules/testgen/targets/bmv2/program_info.h"
19#include "backends/p4tools/modules/testgen/targets/bmv2/test_backend.h"
20
22
24 public:
26 static void make();
27
28 protected:
30 const CompilerResult &compilerResult,
31 const IR::Declaration_Instance *mainDecl) const override;
32
34 const TestBackendConfiguration &testBackendConfiguration,
35 SymbolicExecutor &symbex) const override;
36
37 Bmv2V1ModelCmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
38 const ProgramInfo &programInfo) const override;
39
40 Bmv2V1ModelExprStepper *getExprStepperImpl(ExecutionState &state, AbstractSolver &solver,
41 const ProgramInfo &programInfo) const override;
42
43 private:
45};
46
47} // namespace P4Tools::P4Testgen::Bmv2
48
49#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_ */
Definition compiler_target.h:21
Definition test_backend.h:22
const Bmv2V1ModelProgramInfo * produceProgramInfoImpl(const CompilerResult &compilerResult, const IR::Declaration_Instance *mainDecl) const override
Definition target.cpp:40
Bmv2V1ModelCmdStepper * getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const override
Definition target.cpp:80
static void make()
Registers this target.
Definition target.cpp:33
Bmv2V1ModelExprStepper * getExprStepperImpl(ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const override
Definition target.cpp:85
Bmv2TestBackend * getTestBackendImpl(const ProgramInfo &programInfo, const TestBackendConfiguration &testBackendConfiguration, SymbolicExecutor &symbex) const override
Definition target.cpp:73
Represents state of execution after having reached a program point.
Definition execution_state.h:34
Stores target-specific information about a P4 program.
Definition program_info.h:22
Definition symbolic_executor.h:21
Definition target.h:22
Inja.
Definition bmv2.cpp:25
Definition test_backend_configuration.h:16