Skip to content

Commit

Permalink
[P4Testgen] Clean up the implementation of the BMv2 clone externs. (#…
Browse files Browse the repository at this point in the history
…3976)

* Clean up the implementation of the BMv2 clone implementation. Use explicit info objects to maintain state.

* A different clone id is not needed. Instead, we should fix PI.

* Update the session ID maximum.

* Merge fixes.
  • Loading branch information
fruffy authored May 2, 2023
1 parent 06f520f commit 7be200d
Show file tree
Hide file tree
Showing 30 changed files with 742 additions and 546 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
#include <optional>
#include <ostream>
#include <string>
#include <utility>
#include <vector>

#include <boost/multiprecision/cpp_int.hpp>
Expand Down
15 changes: 13 additions & 2 deletions backends/p4tools/modules/testgen/lib/execution_state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include <algorithm>
#include <cstddef>
#include <initializer_list>
#include <list>
#include <map>
#include <stack>
#include <string>
Expand All @@ -25,6 +26,7 @@
#include "ir/irutils.h"
#include "lib/log.h"
#include "lib/null.h"
#include "lib/ordered_map.h"
#include "lib/source_file.h"

#include "backends/p4tools/modules/testgen/lib/continuation.h"
Expand Down Expand Up @@ -193,15 +195,24 @@ const TestObject *ExecutionState::getTestObject(cstring category, cstring object
return nullptr;
}

std::map<cstring, const TestObject *> ExecutionState::getTestObjectCategory(
cstring category) const {
TestObjectMap ExecutionState::getTestObjectCategory(cstring category) const {
auto it = testObjects.find(category);
if (it != testObjects.end()) {
return it->second;
}
return {};
}

void ExecutionState::deleteTestObject(cstring category, cstring objectLabel) {
auto it = testObjects.find(category);
if (it != testObjects.end()) {
return;
}
it->second.erase(objectLabel);
}

void ExecutionState::deleteTestObjectCategory(cstring category) { testObjects.erase(category); }

void ExecutionState::setReachabilityEngineState(ReachabilityEngineState *newEngineState) {
reachabilityEngineState = newEngineState;
}
Expand Down
20 changes: 14 additions & 6 deletions backends/p4tools/modules/testgen/lib/execution_state.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@
#include "midend/coverage.h"

#include "backends/p4tools/modules/testgen/lib/continuation.h"
#include "backends/p4tools/modules/testgen/lib/test_spec.h"
#include "backends/p4tools/modules/testgen/lib/test_object.h"

namespace P4Tools::P4Testgen {

Expand Down Expand Up @@ -103,7 +103,7 @@ class ExecutionState {
// which defines control plane match action entries. Once the interpreter has solved for the
// variables used by these test objects and concretized the values, they can be used to generate
// a test. Test objects are not constant because they may be manipulated by a target back end.
std::map<cstring, std::map<cstring, const TestObject *>> testObjects;
std::map<cstring, TestObjectMap> testObjects;

/// The parserErrorLabel is set by the parser to indicate the variable corresponding to the
/// parser error that is set by various built-in functions such as verify or extract.
Expand Down Expand Up @@ -217,29 +217,37 @@ class ExecutionState {
[[nodiscard]] const TestObject *getTestObject(cstring category, cstring objectLabel,
bool checked) const;

/// Remove a test object from a category.
void deleteTestObject(cstring category, cstring objectLabel);

/// Remove a test category entirely.
void deleteTestObjectCategory(cstring category);

/// @returns the uninterpreted test object using the provided category and object label. If
/// @param checked is enabled, a BUG is thrown if the object label does not exist.
/// Also casts the test object to the specified type. If the type does not match, a BUG is
/// thrown.
template <class T>
[[nodiscard]] T *getTestObject(cstring category, cstring objectLabel, bool checked) const {
const auto *testObject = getTestObject(category, objectLabel, checked);
[[nodiscard]] const T *getTestObject(cstring category, cstring objectLabel) const {
const auto *testObject = getTestObject(category, objectLabel, true);
return testObject->checkedTo<T>();
}

/// @returns the map of uninterpreted test objects for a specific test category. For example,
/// all the table entries saved under "tableconfigs".
[[nodiscard]] std::map<cstring, const TestObject *> getTestObjectCategory(
cstring category) const;
[[nodiscard]] TestObjectMap getTestObjectCategory(cstring category) const;

/// Get the current state of the reachability engine.
[[nodiscard]] ReachabilityEngineState *getReachabilityEngineState() const;

/// Update the reachability engine state.
void setReachabilityEngineState(ReachabilityEngineState *newEngineState);

/* =========================================================================================
* Trace events.
* ========================================================================================= */
public:
/// Add a new trace event to the state.
void add(const TraceEvent &event);

/* =========================================================================================
Expand Down
37 changes: 37 additions & 0 deletions backends/p4tools/modules/testgen/lib/test_object.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_OBJECT_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_OBJECT_H_
#include <map>

#include "backends/p4tools/common/lib/model.h"
#include "lib/castable.h"
#include "lib/cstring.h"

namespace P4Tools::P4Testgen {

/* =========================================================================================
* Abstract Test Object Class
* ========================================================================================= */

class TestObject : public ICastable {
public:
TestObject() = default;
~TestObject() override = default;
TestObject(const TestObject &) = default;
TestObject(TestObject &&) = default;
TestObject &operator=(const TestObject &) = default;
TestObject &operator=(TestObject &&) = default;

/// @returns the string name of this particular test object.
[[nodiscard]] virtual cstring getObjectName() const = 0;

/// @returns a version of the test object where all expressions are resolved and symbolic
/// variables are substituted according to the mapping present in the @param model.
[[nodiscard]] virtual const TestObject *evaluate(const Model &model) const = 0;
};

/// A map of test objects.
using TestObjectMap = ordered_map<cstring, const TestObject *>;

} // namespace P4Tools::P4Testgen

#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_OBJECT_H_ */
12 changes: 6 additions & 6 deletions backends/p4tools/modules/testgen/lib/test_spec.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#include "backends/p4tools/modules/testgen/lib/test_spec.h"

#include <list>
#include <map>
#include <optional>
#include <utility>
Expand All @@ -11,6 +12,7 @@
#include "backends/p4tools/common/lib/trace_event.h"
#include "ir/irutils.h"
#include "lib/exceptions.h"
#include "lib/ordered_map.h"

namespace P4Tools::P4Testgen {

Expand Down Expand Up @@ -216,14 +218,12 @@ TableConfig::TableConfig(const IR::P4Table *table, std::vector<TableRule> rules)
: table(table), rules(std::move(rules)) {}

TableConfig::TableConfig(const IR::P4Table *table, std::vector<TableRule> rules,
std::map<cstring, const TestObject *> tableProperties)
TestObjectMap tableProperties)
: table(table), rules(std::move(rules)), tableProperties(std::move(tableProperties)) {}

const std::vector<TableRule> *TableConfig::getRules() const { return &rules; }

const std::map<cstring, const TestObject *> *TableConfig::getProperties() const {
return &tableProperties;
}
const TestObjectMap *TableConfig::getProperties() const { return &tableProperties; }

const TestObject *TableConfig::getProperty(cstring propertyName, bool checked) const {
auto it = tableProperties.find(propertyName);
Expand All @@ -246,7 +246,7 @@ const TableConfig *TableConfig::evaluate(const Model &model) const {
const auto *evaluatedRule = rule.evaluate(model);
evaluatedRules.emplace_back(*evaluatedRule);
}
std::map<cstring, const TestObject *> evaluatedProperties;
TestObjectMap evaluatedProperties;
for (const auto &propertyTuple : tableProperties) {
auto name = propertyTuple.first;
const auto *property = propertyTuple.second;
Expand Down Expand Up @@ -298,7 +298,7 @@ const TestObject *TestSpec::getTestObject(cstring category, cstring objectLabel,
return nullptr;
}

std::map<cstring, const TestObject *> TestSpec::getTestObjectCategory(cstring category) const {
TestObjectMap TestSpec::getTestObjectCategory(cstring category) const {
auto it = testObjects.find(category);
if (it != testObjects.end()) {
return it->second;
Expand Down
Loading

0 comments on commit 7be200d

Please sign in to comment.