P4C
The P4 Compiler
Loading...
Searching...
No Matches
execution_state.h
1#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_EXECUTION_STATE_H_
2#define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_EXECUTION_STATE_H_
3
4#include <cstdint>
5#include <functional>
6#include <initializer_list>
7#include <iostream>
8#include <map>
9#include <optional>
10#include <stack>
11#include <utility>
12#include <variant>
13#include <vector>
14
15#include "backends/p4tools/common/compiler/reachability.h"
16#include "backends/p4tools/common/core/abstract_execution_state.h"
17#include "backends/p4tools/common/lib/namespace_context.h"
18#include "backends/p4tools/common/lib/symbolic_env.h"
19#include "backends/p4tools/common/lib/trace_event.h"
20#include "ir/declaration.h"
21#include "ir/ir.h"
22#include "ir/node.h"
23#include "ir/solver.h"
24#include "lib/cstring.h"
25#include "lib/exceptions.h"
26#include "midend/coverage.h"
27
28#include "backends/p4tools/modules/testgen/lib/continuation.h"
29#include "backends/p4tools/modules/testgen/lib/test_object.h"
30
31namespace P4::P4Tools::P4Testgen {
32
35 friend class Test::SmallStepTest;
36
37 public:
38 class StackFrame {
39 public:
40 using ExceptionHandlers = std::map<Continuation::Exception, Continuation>;
41
42 private:
43 Continuation normalContinuation;
44 ExceptionHandlers exceptionHandlers;
45 const NamespaceContext *namespaces = nullptr;
46
47 public:
48 StackFrame(Continuation normalContinuation, const NamespaceContext *namespaces);
49
50 StackFrame(Continuation normalContinuation, ExceptionHandlers exceptionHandlers,
51 const NamespaceContext *namespaces);
52
53 StackFrame(const StackFrame &) = default;
54 StackFrame(StackFrame &&) noexcept = default;
55 StackFrame &operator=(const StackFrame &) = default;
56 StackFrame &operator=(StackFrame &&) = default;
57 ~StackFrame() = default;
58
60 [[nodiscard]] const Continuation &getContinuation() const;
61
63 [[nodiscard]] const ExceptionHandlers &getExceptionHandlers() const;
64
66 [[nodiscard]] const NamespaceContext *getNameSpaces() const;
67 };
68
71 ExecutionState &operator=(ExecutionState &&) = delete;
72 ~ExecutionState() override = default;
73
74 private:
76 std::vector<std::reference_wrapper<const TraceEvent>> trace;
77
79 P4::Coverage::CoverageSet visitedNodes;
80
85
92 // Invariant: if the @body is empty, then so is this, and this state is terminal.
93 std::stack<std::reference_wrapper<const StackFrame>> stack;
94
101 std::map<cstring, Continuation::PropertyValue> stateProperties;
102
103 // Test objects are classes of variables that influence the execution of test frameworks. They
104 // are collected during interpreter execution and consumed by the respective test framework. For
105 // example, when visiting a table, the interpreter will generate a table test object per table,
106 // which defines control plane match action entries. Once the interpreter has solved for the
107 // variables used by these test objects and concretized the values, they can be used to generate
108 // a test. Test objects are not constant because they may be manipulated by a target back end.
109 std::map<cstring, TestObjectMap> testObjects;
110
113 std::optional<IR::StateVariable> parserErrorLabel = std::nullopt;
114
119 int inputPacketCursor = 0;
120
123 std::vector<const IR::Expression *> pathConstraint;
124
126 std::vector<uint64_t> selectedBranches;
127
129 ReachabilityEngineState *reachabilityEngineState = nullptr;
130
133 uint16_t numAllocatedPacketVariables = 0;
134
139 [[nodiscard]] const IR::SymbolicVariable *createPacketVariable(const IR::Type *type);
140
141 /* =========================================================================================
142 * Accessors
143 * ========================================================================================= */
144 public:
146 [[nodiscard]] bool isTerminal() const;
147
149 [[nodiscard]] const std::vector<const IR::Expression *> &getPathConstraint() const;
150
152 [[nodiscard]] const std::vector<uint64_t> &getSelectedBranches() const;
153
155 void pushPathConstraint(const IR::Expression *e);
156
160 void pushBranchDecision(uint64_t);
161
164 [[nodiscard]] std::optional<const Continuation::Command> getNextCmd() const;
165
167 [[nodiscard]] const IR::Expression *get(const IR::StateVariable &var) const override;
168
170 void markVisited(const IR::Node *node);
171
173 [[nodiscard]] const P4::Coverage::CoverageSet &getVisited() const;
174
177 void set(const IR::StateVariable &var, const IR::Expression *value) override;
178
180 [[nodiscard]] const std::vector<std::reference_wrapper<const TraceEvent>> &getTrace() const;
181
183 [[nodiscard]] const Continuation::Body &getBody() const;
184
186 [[nodiscard]] const std::stack<std::reference_wrapper<const StackFrame>> &getStack() const;
187
189 void setProperty(cstring propertyName, Continuation::PropertyValue property);
190
192 [[nodiscard]] bool hasProperty(cstring propertyName) const;
193
196 template <class T>
197 [[nodiscard]] T getProperty(cstring propertyName) const {
198 auto iterator = stateProperties.find(propertyName);
199 if (iterator != stateProperties.end()) {
200 auto val = iterator->second;
201 try {
202 T resolvedVal = std::get<T>(val);
203 return resolvedVal;
204 } catch (std::bad_variant_access const &ex) {
205 BUG("Expected property value type does not correspond to value type stored in the "
206 "property map.");
207 }
208 }
209 BUG("Property %s not found in configuration map.", propertyName);
210 }
211
214 void addTestObject(cstring category, cstring objectLabel, const TestObject *object);
215
218 [[nodiscard]] const TestObject *getTestObject(cstring category, cstring objectLabel,
219 bool checked) const;
220
222 void deleteTestObject(cstring category, cstring objectLabel);
223
225 void deleteTestObjectCategory(cstring category);
226
231 template <class T>
232 [[nodiscard]] const T *getTestObject(cstring category, cstring objectLabel) const {
233 const auto *testObject = getTestObject(category, objectLabel, true);
234 return testObject->checkedTo<T>();
235 }
236
239 [[nodiscard]] TestObjectMap getTestObjectCategory(cstring category) const;
240
243
246
247 /* =========================================================================================
248 * Trace events.
249 * ========================================================================================= */
251 void add(const TraceEvent &event);
252
253 /* =========================================================================================
254 * Body operations
255 * ========================================================================================= */
257 void replaceTopBody(const Continuation::Command &cmd);
258
261 void replaceTopBody(const std::vector<Continuation::Command> *cmds);
262
265 void replaceTopBody(std::initializer_list<Continuation::Command> cmds);
266
270 //
271 // Needs to be implemented here because of limitations with templates.
272 template <class N>
273 void replaceTopBody(const std::vector<const N *> *nodes) {
274 BUG_CHECK(!nodes->empty(), "Replaced top of execution stack with empty list");
275 body.pop();
276 for (auto it = nodes->rbegin(); it != nodes->rend(); ++it) {
277 BUG_CHECK(*it, "Evaluation produced a null node.");
278 body.push(*it);
279 }
280 }
281
283 void popBody();
284
286 void replaceBody(const Continuation::Body &body);
287
288 /* =========================================================================================
289 * Continuation-stack operations
290 * ========================================================================================= */
292 void pushContinuation(const StackFrame &frame);
293
297 void pushCurrentContinuation(StackFrame::ExceptionHandlers handlers);
298
303 void pushCurrentContinuation(std::optional<const IR::Type *> parameterType_opt = std::nullopt,
304 StackFrame::ExceptionHandlers = {});
305
312 void popContinuation(std::optional<const IR::Node *> argument_opt = std::nullopt);
313
316
317 /* =========================================================================================
318 * Packet manipulation
319 * ========================================================================================= */
322 static const IR::SymbolicVariable *getInputPacketSizeVar();
323
326 [[nodiscard]] static int getMaxPacketLength();
327
329 [[nodiscard]] const IR::Expression *getInputPacket() const;
330
332 [[nodiscard]] int getInputPacketSize() const;
333
335 void appendToInputPacket(const IR::Expression *expr);
336
338 void prependToInputPacket(const IR::Expression *expr);
339
341 [[nodiscard]] int getInputPacketCursor() const;
342
344 [[nodiscard]] const IR::Expression *getPacketBuffer() const;
345
347 [[nodiscard]] int getPacketBufferSize() const;
348
353 const IR::Expression *slicePacketBuffer(int amount);
354
359 [[nodiscard]] const IR::Expression *peekPacketBuffer(int amount);
360
362 void appendToPacketBuffer(const IR::Expression *expr);
363
365 void prependToPacketBuffer(const IR::Expression *expr);
366
368 void resetPacketBuffer();
369
371 [[nodiscard]] const IR::Expression *getEmitBuffer() const;
372
374 void resetEmitBuffer();
375
377 void appendToEmitBuffer(const IR::Expression *expr);
378
380 void setParserErrorLabel(const IR::StateVariable &parserError);
381
383 [[nodiscard]] const IR::StateVariable &getCurrentParserErrorLabel() const;
384
385 /* =========================================================================================
386 * Constructors
387 * ========================================================================================= */
390 [[nodiscard]] ExecutionState &clone() const override;
391
394 [[nodiscard]] static ExecutionState &create(const IR::P4Program *program);
395
396 private:
398 explicit ExecutionState(Continuation::Body body);
399
400 // Execution state should always be allocated through explicit operators.
402 explicit ExecutionState(const IR::P4Program *program);
403 ExecutionState(const ExecutionState &) = default;
404
406 ExecutionState &operator=(const ExecutionState &) = default;
407};
408
409using ExecutionStateReference = std::reference_wrapper<ExecutionState>;
410
411} // namespace P4::P4Tools::P4Testgen
412
413#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_EXECUTION_STATE_H_ */
Definition node.h:95
Represents state of execution after having reached a program point.
Definition abstract_execution_state.h:12
Represents a stack of namespaces.
Definition namespace_context.h:14
A continuation body is a list of commands.
Definition continuation.h:129
void push(Command cmd)
Pushes the given command onto the command stack.
Definition continuation.cpp:43
void pop()
Definition continuation.cpp:45
Definition continuation.h:29
Exception
Enumerates the exceptions that can be thrown during symbolic execution.
Definition continuation.h:35
std::variant< cstring, uint64_t, int64_t, bool, const IR::Expression * > PropertyValue
Definition continuation.h:85
const NamespaceContext * getNameSpaces() const
Definition execution_state.cpp:63
const ExceptionHandlers & getExceptionHandlers() const
Definition execution_state.cpp:59
const Continuation & getContinuation() const
Definition execution_state.cpp:54
Represents state of execution after having reached a program point.
Definition execution_state.h:34
const IR::Expression * getInputPacket() const
Definition execution_state.cpp:376
static const IR::SymbolicVariable * getInputPacketSizeVar()
Definition execution_state.cpp:369
const std::vector< const IR::Expression * > & getPathConstraint() const
Definition execution_state.cpp:113
void replaceTopBody(const Continuation::Command &cmd)
Replaces the top element of @body with @cmd.
Definition execution_state.cpp:346
int getInputPacketSize() const
Definition execution_state.cpp:380
void pushContinuation(const StackFrame &frame)
Pushes a new frame onto the continuation stack.
Definition execution_state.cpp:289
const IR::Expression * getPacketBuffer() const
Definition execution_state.cpp:401
void setReachabilityEngineState(ReachabilityEngineState *newEngineState)
Update the reachability engine state.
Definition execution_state.cpp:271
void pushCurrentContinuation(StackFrame::ExceptionHandlers handlers)
Definition execution_state.cpp:291
void deleteTestObject(cstring category, cstring objectLabel)
Remove a test object from a category.
Definition execution_state.cpp:262
const IR::StateVariable & getCurrentParserErrorLabel() const
Definition execution_state.cpp:531
const IR::Expression * getEmitBuffer() const
Definition execution_state.cpp:512
void set(const IR::StateVariable &var, const IR::Expression *value) override
Definition execution_state.cpp:198
void replaceBody(const Continuation::Body &body)
Replaces @body with the given argument.
Definition execution_state.cpp:287
void popBody()
Pops the top element of @body.
Definition execution_state.cpp:285
const P4::Coverage::CoverageSet & getVisited() const
Definition execution_state.cpp:179
const IR::Expression * get(const IR::StateVariable &var) const override
Definition execution_state.cpp:124
bool hasProperty(cstring propertyName) const
Definition execution_state.cpp:231
ExecutionState(ExecutionState &&)=delete
No move semantics because of constant members. We always need to clone a state.
void markVisited(const IR::Node *node)
Checks whether the node has been visited in this state.
Definition execution_state.cpp:158
void appendToPacketBuffer(const IR::Expression *expr)
Append data to the packet buffer.
Definition execution_state.cpp:494
const TestObject * getTestObject(cstring category, cstring objectLabel, bool checked) const
Definition execution_state.cpp:240
void deleteTestObjectCategory(cstring category)
Remove a test category entirely.
Definition execution_state.cpp:269
T getProperty(cstring propertyName) const
Definition execution_state.h:197
const std::vector< std::reference_wrapper< const TraceEvent > > & getTrace() const
Definition execution_state.cpp:216
void prependToInputPacket(const IR::Expression *expr)
Prepend data to the input packet.
Definition execution_state.cpp:392
void pushPathConstraint(const IR::Expression *e)
Adds path constraint.
Definition execution_state.cpp:365
const IR::Expression * slicePacketBuffer(int amount)
Definition execution_state.cpp:443
std::optional< const Continuation::Command > getNextCmd() const
Definition execution_state.cpp:117
void handleException(Continuation::Exception e)
Invokes first handler for e found on the stack.
Definition execution_state.cpp:327
ExecutionState & clone() const override
Definition execution_state.cpp:101
void appendToEmitBuffer(const IR::Expression *expr)
Append data to the emit buffer.
Definition execution_state.cpp:520
TestObjectMap getTestObjectCategory(cstring category) const
Definition execution_state.cpp:254
void setProperty(cstring propertyName, Continuation::PropertyValue property)
Set the property with.
Definition execution_state.cpp:227
bool isTerminal() const
Determines whether this state represents the end of an execution.
Definition execution_state.cpp:107
void resetEmitBuffer()
Reset the emit buffer to zero.
Definition execution_state.cpp:516
const T * getTestObject(cstring category, cstring objectLabel) const
Definition execution_state.h:232
void popContinuation(std::optional< const IR::Node * > argument_opt=std::nullopt)
Definition execution_state.cpp:317
void addTestObject(cstring category, cstring objectLabel, const TestObject *object)
Definition execution_state.cpp:235
void setParserErrorLabel(const IR::StateVariable &parserError)
Set the parser error label to the.
Definition execution_state.cpp:527
void pushBranchDecision(uint64_t)
Definition execution_state.cpp:367
int getPacketBufferSize() const
Definition execution_state.cpp:405
const IR::Expression * peekPacketBuffer(int amount)
Definition execution_state.cpp:410
ReachabilityEngineState * getReachabilityEngineState() const
Get the current state of the reachability engine.
Definition execution_state.cpp:275
int getInputPacketCursor() const
Definition execution_state.cpp:399
const std::stack< std::reference_wrapper< const StackFrame > > & getStack() const
Definition execution_state.cpp:223
void replaceTopBody(const std::vector< const N * > *nodes)
Definition execution_state.h:273
void add(const TraceEvent &event)
Add a new trace event to the state.
Definition execution_state.cpp:283
const Continuation::Body & getBody() const
Definition execution_state.cpp:220
void resetPacketBuffer()
Reset the packet buffer to zero.
Definition execution_state.cpp:508
void prependToPacketBuffer(const IR::Expression *expr)
Prepend data to the packet buffer.
Definition execution_state.cpp:501
static int getMaxPacketLength()
Definition execution_state.cpp:374
const std::vector< uint64_t > & getSelectedBranches() const
Definition execution_state.cpp:109
void appendToInputPacket(const IR::Expression *expr)
Append data to the input packet.
Definition execution_state.cpp:385
static ExecutionState & create(const IR::P4Program *program)
Definition execution_state.cpp:97
Definition test_object.h:15
The main data for reachability engine.
Definition reachability.h:122
Definition modules/testgen/test/small-step/util.h:40
An event in a trace of the execution of a P4 program.
Definition trace_event.h:14
Definition cstring.h:85
std::set< const IR::Node *, SourceIdCmp > CoverageSet
Definition coverage.h:39