P4C
The P4 Compiler
Loading...
Searching...
No Matches
targets/bmv2/expr_stepper.h
1#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_EXPR_STEPPER_H_
2#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_EXPR_STEPPER_H_
3
4#include <cstdint>
5#include <string>
6
7#include "ir/ir.h"
8#include "ir/solver.h"
9
10#include "backends/p4tools/modules/testgen/core/program_info.h"
11#include "backends/p4tools/modules/testgen/core/small_step/expr_stepper.h"
12#include "backends/p4tools/modules/testgen/core/small_step/small_step.h"
13#include "backends/p4tools/modules/testgen/lib/execution_state.h"
14
16
18 protected:
19 std::string getClassName() override;
20
21 private:
22 // Helper function that checks whether the given structure filed has a 'field_list' annotation
23 // and the recirculate index matches. @returns true if that is the case.
24 static bool isPartOfFieldList(const IR::StructField *field, uint64_t recirculateIndex);
25
30 void resetPreservingFieldList(ExecutionState &nextState, const IR::PathExpression *ref,
31 uint64_t recirculateIndex) const;
32
34 void processClone(const ExecutionState &state, SmallStepEvaluator::Result &result);
35
38 void processRecirculate(const ExecutionState &state, SmallStepEvaluator::Result &result);
39
40 // using MethodImpl = std::function<void(const ExternInfo &, Bmv2V1ModelExprStepper &stepper)>;
41 // Provides implementations of BMv2 externs.
43 ASSERT_ASSUME_EXECUTE;
44 static const ExternMethodImpls<Bmv2V1ModelExprStepper> BMV2_EXTERN_METHOD_IMPLS;
45
46 public:
49
50 void evalExternMethodCall(const ExternInfo &externInfo) override;
51
52 bool preorder(const IR::P4Table * /*table*/) override;
53};
54} // namespace P4::P4Tools::P4Testgen::Bmv2
55
56#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_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
Result result
The output of the evaluation.
Definition abstract_stepper.h:55
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/bmv2/expr_stepper.h:17
std::string getClassName() override
Definition targets/bmv2/expr_stepper.cpp:45
void evalExternMethodCall(const ExternInfo &externInfo) override
Definition targets/bmv2/expr_stepper.cpp:1632
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
Inja.
Definition targets/bmv2/cmd_stepper.cpp:33