P4C
The P4 Compiler
Loading...
Searching...
No Matches
p4tools/modules/testgen/targets/bmv2/target.h
1/*
2 * SPDX-FileCopyrightText: 2022 The P4 Language Consortium
3 *
4 * SPDX-License-Identifier: Apache-2.0
5 */
6
7#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_
8#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_
9
10#include "ir/ir.h"
11#include "ir/solver.h"
12
13#include "backends/p4tools/modules/testgen/core/program_info.h"
14#include "backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h"
15#include "backends/p4tools/modules/testgen/core/target.h"
16#include "backends/p4tools/modules/testgen/lib/execution_state.h"
17#include "backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.h"
18#include "backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.h"
19#include "backends/p4tools/modules/testgen/targets/bmv2/program_info.h"
20#include "backends/p4tools/modules/testgen/targets/bmv2/test_backend.h"
21
23
24class Bmv2V1ModelTestgenTarget : public TestgenTarget {
25 public:
27 static void make();
28
29 protected:
31 const CompilerResult &compilerResult,
32 const IR::Declaration_Instance *mainDecl) const override;
33
35 const TestBackendConfiguration &testBackendConfiguration,
36 SymbolicExecutor &symbex) const override;
37
39 const ProgramInfo &programInfo) const override;
40
42 const ProgramInfo &programInfo) const override;
43
44 private:
45 Bmv2V1ModelTestgenTarget();
46
47 [[nodiscard]] MidEnd mkMidEnd(const CompilerOptions &options) const override;
48
49 CompilerResultOrError runCompilerImpl(const CompilerOptions &options,
50 const IR::P4Program *program) const override;
51};
52
53} // namespace P4::P4Tools::P4Testgen::Bmv2
54
55#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_TARGET_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:30
Definition frontends/common/options.h:31
Definition common/compiler/compiler_result.h:20
Definition p4tools/common/compiler/midend.h:30
Definition targets/bmv2/test_backend.h:28
Definition targets/bmv2/cmd_stepper.h:25
Definition targets/bmv2/expr_stepper.h:23
Definition targets/bmv2/program_info.h:21
Bmv2TestBackend * getTestBackendImpl(const ProgramInfo &programInfo, const TestBackendConfiguration &testBackendConfiguration, SymbolicExecutor &symbex) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:171
Bmv2V1ModelExprStepper * getExprStepperImpl(ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:183
Bmv2V1ModelCmdStepper * getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:178
const Bmv2V1ModelProgramInfo * produceProgramInfoImpl(const CompilerResult &compilerResult, const IR::Declaration_Instance *mainDecl) const override
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:127
static void make()
Registers this target.
Definition p4tools/modules/testgen/targets/bmv2/target.cpp:41
Represents state of execution after having reached a program point.
Definition execution_state.h:40
Stores target-specific information about a P4 program.
Definition core/program_info.h:27
Definition symbolic_executor.h:27
Inja.
Definition targets/bmv2/cmd_stepper.cpp:37
std::optional< std::reference_wrapper< const CompilerResult > > CompilerResultOrError
Definition common/compiler/compiler_result.h:37
Definition phv/solver/action_constraint_solver.cpp:33
Definition test_backend_configuration.h:22