P4C
The P4 Compiler
Loading...
Searching...
No Matches
targets/bmv2/expr_stepper.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_EXPR_STEPPER_H_
8#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_EXPR_STEPPER_H_
9
10#include <cstdint>
11#include <string>
12
13#include "ir/ir.h"
14#include "ir/solver.h"
15
16#include "backends/p4tools/modules/testgen/core/program_info.h"
17#include "backends/p4tools/modules/testgen/core/small_step/expr_stepper.h"
18#include "backends/p4tools/modules/testgen/core/small_step/small_step.h"
19#include "backends/p4tools/modules/testgen/lib/execution_state.h"
20
22
23class Bmv2V1ModelExprStepper : public ExprStepper {
24 protected:
25 std::string getClassName() override;
26
27 private:
28 // Helper function that checks whether the given structure filed has a 'field_list' annotation
29 // and the recirculate index matches. @returns true if that is the case.
30 static bool isPartOfFieldList(const IR::StructField *field, uint64_t recirculateIndex);
31
36 void resetPreservingFieldList(ExecutionState &nextState, const IR::PathExpression *ref,
37 uint64_t recirculateIndex) const;
38
40 void processClone(const ExecutionState &state, SmallStepEvaluator::Result &result);
41
44 void processRecirculate(const ExecutionState &state, SmallStepEvaluator::Result &result);
45
46 // using MethodImpl = std::function<void(const ExternInfo &, Bmv2V1ModelExprStepper &stepper)>;
47 // Provides implementations of BMv2 externs.
49 ASSERT_ASSUME_EXECUTE;
50 static const ExternMethodImpls<Bmv2V1ModelExprStepper> BMV2_EXTERN_METHOD_IMPLS;
51
52 public:
53 Bmv2V1ModelExprStepper(ExecutionState &state, AbstractSolver &solver,
55
56 void evalExternMethodCall(const ExternInfo &externInfo) override;
57
58 bool preorder(const IR::P4Table * /*table*/) override;
59};
60} // namespace P4::P4Tools::P4Testgen::Bmv2
61
62#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_EXPR_STEPPER_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:30
ExecutionState & state
The state being evaluated.
Definition abstract_stepper.h:55
Result result
The output of the evaluation.
Definition abstract_stepper.h:61
const ProgramInfo & programInfo
Target-specific information about the P4 program being evaluated.
Definition abstract_stepper.h:52
std::string getClassName() override
Definition targets/bmv2/expr_stepper.cpp:49
void evalExternMethodCall(const ExternInfo &externInfo) override
Definition targets/bmv2/expr_stepper.cpp:1629
Represents state of execution after having reached a program point.
Definition execution_state.h:40
Encapsulates a set of extern method implementations.
Definition core/small_step/expr_stepper.h:33
Definition extern_info.h:20
Stores target-specific information about a P4 program.
Definition core/program_info.h:27
Inja.
Definition targets/bmv2/cmd_stepper.cpp:37
Definition phv/solver/action_constraint_solver.cpp:33