P4C
The P4 Compiler
Loading...
Searching...
No Matches
p4tools/modules/testgen/targets/bmv2/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 "ir/ir.h"
5#include "ir/solver.h"
6
7#include "backends/p4tools/modules/testgen/core/program_info.h"
8#include "backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h"
9#include "backends/p4tools/modules/testgen/core/target.h"
10#include "backends/p4tools/modules/testgen/lib/execution_state.h"
11#include "backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.h"
12#include "backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.h"
13#include "backends/p4tools/modules/testgen/targets/bmv2/program_info.h"
14#include "backends/p4tools/modules/testgen/targets/bmv2/test_backend.h"
15
17
19 public:
21 static void make();
22
23 protected:
25 const CompilerResult &compilerResult,
26 const IR::Declaration_Instance *mainDecl) const override;
27
29 const TestBackendConfiguration &testBackendConfiguration,
30 SymbolicExecutor &symbex) const override;
31
33 const ProgramInfo &programInfo) const override;
34
36 const ProgramInfo &programInfo) const override;
37
38 private:
40
41 [[nodiscard]] MidEnd mkMidEnd(const CompilerOptions &options) const override;
42
43 CompilerResultOrError runCompilerImpl(const CompilerOptions &options,
44 const IR::P4Program *program) const override;
45};
46
47} // namespace P4::P4Tools::P4Testgen::Bmv2
48
49#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:24
Definition frontends/common/options.h:30
Definition common/compiler/compiler_result.h:14
Definition p4tools/common/compiler/midend.h:24
Definition targets/bmv2/test_backend.h:22
Definition targets/bmv2/cmd_stepper.h:19
Definition targets/bmv2/expr_stepper.h:17
Definition targets/bmv2/program_info.h:15
Definition p4tools/modules/testgen/targets/bmv2/target.h:18
Bmv2TestBackend * getTestBackendImpl(const ProgramInfo &programInfo, const TestBackendConfiguration &testBackendConfiguration, SymbolicExecutor &symbex) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:155
Bmv2V1ModelExprStepper * getExprStepperImpl(ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:167
Bmv2V1ModelCmdStepper * getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:162
const Bmv2V1ModelProgramInfo * produceProgramInfoImpl(const CompilerResult &compilerResult, const IR::Declaration_Instance *mainDecl) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:122
static void make()
Registers this target.
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:36
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
Definition symbolic_executor.h:21
Definition p4tools/modules/testgen/core/target.h:19
Inja.
Definition targets/bmv2/cmd_stepper.cpp:33
std::optional< std::reference_wrapper< const CompilerResult > > CompilerResultOrError
Definition common/compiler/compiler_result.h:31
Definition test_backend_configuration.h:16