P4C
The P4 Compiler
Loading...
Searching...
No Matches
core/small_step/cmd_stepper.h
1#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_CMD_STEPPER_H_
2#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_CMD_STEPPER_H_
3
4#include <map>
5#include <optional>
6#include <vector>
7
8#include "ir/ir.h"
9#include "ir/solver.h"
10#include "lib/cstring.h"
11
12#include "backends/p4tools/modules/testgen/core/program_info.h"
13#include "backends/p4tools/modules/testgen/core/small_step/abstract_stepper.h"
14#include "backends/p4tools/modules/testgen/lib/continuation.h"
15#include "backends/p4tools/modules/testgen/lib/execution_state.h"
16
17namespace P4::P4Tools::P4Testgen {
18
21 public:
23
24 bool preorder(const IR::AssignmentStatement *assign) override;
25 bool preorder(const IR::P4Parser *p4parser) override;
26 bool preorder(const IR::P4Control *p4control) override;
27 bool preorder(const IR::EmptyStatement *empty) override;
28 bool preorder(const IR::IfStatement *ifStatement) override;
29 bool preorder(const IR::MethodCallStatement *methodCallStatement) override;
30 bool preorder(const IR::P4Program *program) override;
31 bool preorder(const IR::ParserState *parserState) override;
32 bool preorder(const IR::BlockStatement *block) override;
33 bool preorder(const IR::ExitStatement *e) override;
34 bool preorder(const IR::SwitchStatement *switchStatement) override;
35
36 protected:
40 const Constraint *startParser(const IR::P4Parser *parser, ExecutionState &state);
41
44 virtual std::optional<const Constraint *> startParserImpl(const IR::P4Parser *parser,
45 ExecutionState &state) const = 0;
46
50
55 virtual std::map<Continuation::Exception, Continuation> getExceptionHandlers(
56 const IR::P4Parser *parser, Continuation::Body normalContinuation,
57 const ExecutionState &state) const = 0;
58};
59
60} // namespace P4::P4Tools::P4Testgen
61
62#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_CMD_STEPPER_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:24
Definition abstract_stepper.h:28
ExecutionState & state
The state being evaluated.
Definition abstract_stepper.h:49
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
Implements small-step operational semantics for commands.
Definition core/small_step/cmd_stepper.h:20
virtual void initializeTargetEnvironment(ExecutionState &state) const =0
virtual std::map< Continuation::Exception, Continuation > getExceptionHandlers(const IR::P4Parser *parser, Continuation::Body normalContinuation, const ExecutionState &state) const =0
virtual std::optional< const Constraint * > startParserImpl(const IR::P4Parser *parser, ExecutionState &state) const =0
const Constraint * startParser(const IR::P4Parser *parser, ExecutionState &state)
Definition core/small_step/cmd_stepper.cpp:441
A continuation body is a list of commands.
Definition continuation.h:129
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
IR::Expression Constraint
Represents a constraint that can be shipped to and asserted within a solver.
Definition solver.h:17