Skip to content

Commit

Permalink
[P4Testgen] Hotfixes and improvements to the P4Constraints parsers. (#…
Browse files Browse the repository at this point in the history 
…4387)

* Small hotfixes to prevent crashes.

* Review comments and fixes.
  • Loading branch information
@fruffy
fruffy committed Feb 6, 2024
1 parent c5c38a7 commit efb20df
Show file tree
Hide file tree
Showing 9 changed files with 264 additions and 133 deletions.
13 changes: 11 additions & 2 deletions backends/p4tools/common/lib/variables.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,14 @@
/// Variables internal to P4Tools. These variables do not exist in the P4
/// program itself, but are generated and added to the environment by the P4Tools tooling. These
/// variables are also used for SMT solvers as symbolic variables.
namespace P4Tools::ToolsVariables {
namespace P4Tools {

/// A list of constraints. These constraints may take the form of "x == 8w1","x != y", where "x" and
/// "y" are symbolic variables. They are expressed in P4C IR form and may be consumed by SMT or
/// similar solvers.
using ConstraintsVector = std::vector<const IR::Expression *>;

namespace ToolsVariables {

/// To represent header validity, we pretend that every header has a field that reflects the
/// header's validity state. This is the name of that field. This is not a valid P4 identifier,
Expand Down Expand Up @@ -41,6 +48,8 @@ IR::StateVariable getHeaderValidity(const IR::Expression *headerRef);
/// and IR::Member can be converted into a state variable.
IR::StateVariable convertReference(const IR::Expression *ref);

} // namespace P4Tools::ToolsVariables
} // namespace ToolsVariables

} // namespace P4Tools

#endif /* BACKENDS_P4TOOLS_COMMON_LIB_VARIABLES_H_ */
21 changes: 11 additions & 10 deletions backends/p4tools/modules/testgen/targets/bmv2/bmv2.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,15 +22,15 @@ namespace P4Tools::P4Testgen::Bmv2 {
BMv2V1ModelCompilerResult::BMv2V1ModelCompilerResult(TestgenCompilerResult compilerResult,
P4::P4RuntimeAPI p4runtimeApi,
DirectExternMap directExternMap,
P4ConstraintsVector p4ConstraintsRestrictions)
ConstraintsVector p4ConstraintsRestrictions)
: TestgenCompilerResult(std::move(compilerResult)),
p4runtimeApi(p4runtimeApi),
directExternMap(std::move(directExternMap)),
p4ConstraintsRestrictions(std::move(p4ConstraintsRestrictions)) {}

const P4::P4RuntimeAPI &BMv2V1ModelCompilerResult::getP4RuntimeApi() const { return p4runtimeApi; }

P4ConstraintsVector BMv2V1ModelCompilerResult::getP4ConstraintsRestrictions() const {
ConstraintsVector BMv2V1ModelCompilerResult::getP4ConstraintsRestrictions() const {
return p4ConstraintsRestrictions;
}

Expand Down Expand Up @@ -79,17 +79,18 @@ CompilerResultOrError Bmv2V1ModelCompilerTarget::runCompilerImpl(
return std::nullopt;
}

// Vector containing pairs of restrictions and nodes to which these restrictions apply.
P4ConstraintsVector p4ConstraintsRestrictions;
// Defines all "entry_restriction" and then converts restrictions from string to IR
// expressions, and stores them in p4ConstraintsRestrictions to move targetConstraints further.
program->apply(AssertsParser(p4ConstraintsRestrictions));
// Parses any @refers_to annotations and converts them into a vector of restrictions.
auto refersToParser = RefersToParser();
program->apply(refersToParser);
if (::errorCount() > 0) {
return std::nullopt;
}
// Defines all "refers_to" and then converts restrictions from string to IR expressions,
// and stores them in p4ConstraintsRestrictions to move targetConstraints further.
program->apply(RefersToParser(p4ConstraintsRestrictions));
ConstraintsVector p4ConstraintsRestrictions = refersToParser.getRestrictionsVector();

// Defines all "entry_restriction" and then converts restrictions from string to IR
// expressions, and stores them in p4ConstraintsRestrictions to move targetConstraints
// further.
program->apply(AssertsParser(p4ConstraintsRestrictions));
if (::errorCount() > 0) {
return std::nullopt;
}
Expand Down
7 changes: 4 additions & 3 deletions backends/p4tools/modules/testgen/targets/bmv2/bmv2.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

#include "backends/p4tools/common/compiler/compiler_target.h"
#include "backends/p4tools/common/compiler/midend.h"
#include "backends/p4tools/common/lib/variables.h"
#include "frontends/common/options.h"

#include "backends/p4tools/modules/testgen/core/compiler_target.h"
Expand All @@ -22,20 +23,20 @@ class BMv2V1ModelCompilerResult : public TestgenCompilerResult {

// Vector containing vectors of P4Constraints restrictions and nodes to which these restrictions
// apply.
P4ConstraintsVector p4ConstraintsRestrictions;
ConstraintsVector p4ConstraintsRestrictions;

public:
explicit BMv2V1ModelCompilerResult(TestgenCompilerResult compilerResult,
P4::P4RuntimeAPI p4runtimeApi,
DirectExternMap directExternMap,
P4ConstraintsVector p4ConstraintsRestrictions);
ConstraintsVector p4ConstraintsRestrictions);

/// @returns the P4RuntimeAPI inferred from this particular BMv2 V1Model P4 program.
[[nodiscard]] const P4::P4RuntimeAPI &getP4RuntimeApi() const;

/// @returns the vector of pairs of P4Constraints restrictions and nodes to which these
// apply.
[[nodiscard]] P4ConstraintsVector getP4ConstraintsRestrictions() const;
[[nodiscard]] ConstraintsVector getP4ConstraintsRestrictions() const;

/// @returns the map of direct extern declarations which are attached to a table.
[[nodiscard]] const DirectExternMap &getDirectExternMap() const;
Expand Down
99 changes: 64 additions & 35 deletions backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ static const std::vector<std::string> NAMES{
"Mul", "Comment", "Unknown", "EndString", "End",
};

AssertsParser::AssertsParser(P4ConstraintsVector &output) : restrictionsVec(output) {
AssertsParser::AssertsParser(ConstraintsVector &output) : restrictionsVec(output) {
setName("Restrictions");
}

Expand Down Expand Up @@ -121,24 +121,18 @@ const IR::Expression *makeSingleExpr(std::vector<const IR::Expression *> input)
}

/// Determines the token type according to the table key and generates a symbolic variable for it.
const IR::Expression *makeConstant(Token input, const IR::Vector<IR::KeyElement> &keyElements,
const IR::Expression *makeConstant(Token input, const IdenitifierTypeMap &typeMap,
const IR::Type *leftType) {
const IR::Type_Base *type = nullptr;
const IR::Expression *result = nullptr;
auto inputStr = input.lexeme();
if (input.is(Token::Kind::Text)) {
for (const auto *key : keyElements) {
cstring keyName;
if (const auto *annotation = key->getAnnotation(IR::Annotation::nameAnnotation)) {
keyName = annotation->getName();
}
BUG_CHECK(keyName.size() > 0, "Key does not have a name annotation.");
auto annoSize = keyName.size();
for (const auto &[identifier, keyType] : typeMap) {
auto annoSize = identifier.size();
auto tokenLength = inputStr.length();
if (inputStr.compare(tokenLength - annoSize, annoSize, keyName) != 0) {
if (inputStr.compare(tokenLength - annoSize, annoSize, identifier) != 0) {
continue;
}
const auto *keyType = key->expression->type;
if (const auto *bit = keyType->to<IR::Type_Bits>()) {
type = bit;
} else if (const auto *varbit = keyType->to<IR::Extracted_Varbits>()) {
Expand All @@ -164,7 +158,7 @@ const IR::Expression *makeConstant(Token input, const IR::Vector<IR::KeyElement>
BUG_CHECK(result != nullptr,
"Could not match restriction key label %s was not found in key list.",
std::string(inputStr));
return nullptr;
return result;
}

/// Determines the right side of the expression starting from the original position and returns a
Expand Down Expand Up @@ -243,8 +237,7 @@ const IR::Expression *pickBinaryExpr(const Token &token, const IR::Expression *l
/// For example, at the input we have a vector of tokens:
/// [key1(Text), ->(Implication), key2(Text), &&(Conjunction), key3(Text)] The result will be an
/// IR::Expression equal to !IR::Expression || (IR::Expression && IR::Expression)
const IR::Expression *getIR(std::vector<Token> tokens,
const IR::Vector<IR::KeyElement> &keyElements) {
const IR::Expression *getIR(std::vector<Token> tokens, const IdenitifierTypeMap &typeMap) {
std::vector<const IR::Expression *> exprVec;

for (size_t idx = 0; idx < tokens.size(); idx++) {
Expand All @@ -256,28 +249,28 @@ const IR::Expression *getIR(std::vector<Token> tokens,
Token::Kind::Shl, Token::Kind::Mul, Token::Kind::NotEqual)) {
const IR::Expression *leftL = nullptr;
const IR::Expression *rightL = nullptr;
leftL = makeConstant(tokens[idx - 1], keyElements, nullptr);
leftL = makeConstant(tokens[idx - 1], typeMap, nullptr);
if (tokens[idx + 1].isOneOf(Token::Kind::Text, Token::Kind::Number)) {
rightL = makeConstant(tokens[idx + 1], keyElements, leftL->type);
rightL = makeConstant(tokens[idx + 1], typeMap, leftL->type);
if (const auto *constant = leftL->to<IR::Constant>()) {
auto *clone = constant->clone();
clone->type = rightL->type;
leftL = clone;
}
} else {
auto rightPart = findRightPart(tokens, idx);
rightL = getIR(rightPart.first, keyElements);
rightL = getIR(rightPart.first, typeMap);
idx = rightPart.second;
}

if (idx - 2 > 0 && tokens[idx - 2].is(Token::Kind::LNot)) {
if (idx >= 2 && tokens[idx - 2].is(Token::Kind::LNot)) {
leftL = new IR::LNot(leftL);
}
exprVec.push_back(pickBinaryExpr(token, leftL, rightL));
} else if (token.is(Token::Kind::LNot)) {
if (!tokens[idx + 1].isOneOf(Token::Kind::Text, Token::Kind::Number)) {
auto rightPart = findRightPart(tokens, idx);
const IR::Expression *exprLNot = getIR(rightPart.first, keyElements);
const IR::Expression *exprLNot = getIR(rightPart.first, typeMap);
idx = rightPart.second;
exprVec.push_back(new IR::LNot(exprLNot));
}
Expand Down Expand Up @@ -356,6 +349,11 @@ std::vector<Token> combineTokensToNumbers(std::vector<Token> input) {
cstring numb = "";
std::vector<Token> result;
for (uint64_t i = 0; i < input.size(); i++) {
if (input[i].is(Token::Kind::Minus)) {
numb += "-";
i++;
}

if (input[i].is(Token::Kind::Text)) {
auto str = std::string(input[i].lexeme());

Expand Down Expand Up @@ -468,8 +466,9 @@ std::vector<Token> removeComments(const std::vector<Token> &input) {
/// A function that calls the beginning of the transformation of restrictions from a string into an
/// IR::Expression. Internally calls all other necessary functions, for example combineTokensToNames
/// and the like, to eventually get an IR expression that meets the string constraint
std::vector<const IR::Expression *> AssertsParser::genIRStructs(
cstring tableName, cstring restrictionString, const IR::Vector<IR::KeyElement> &keyElements) {
std::vector<const IR::Expression *> AssertsParser::genIRStructs(cstring tableName,
cstring restrictionString,
const IdenitifierTypeMap &typeMap) {
Lexer lex(restrictionString);
std::vector<Token> tmp;
for (auto token = lex.next(); !token.isOneOf(Token::Kind::End, Token::Kind::Unknown);
Expand All @@ -486,12 +485,12 @@ std::vector<const IR::Expression *> AssertsParser::genIRStructs(
std::vector<Token> tokens;
for (uint64_t i = 0; i < tmp.size(); i++) {
if (tmp[i].is(Token::Kind::Semicolon)) {
const auto *expr = getIR(tokens, keyElements);
const auto *expr = getIR(tokens, typeMap);
result.push_back(expr);
tokens.clear();
} else if (i == tmp.size() - 1) {
tokens.push_back(tmp[i]);
const auto *expr = getIR(tokens, keyElements);
const auto *expr = getIR(tokens, typeMap);
result.push_back(expr);
tokens.clear();
} else {
Expand All @@ -502,43 +501,73 @@ std::vector<const IR::Expression *> AssertsParser::genIRStructs(
return result;
}

const IR::Node *AssertsParser::postorder(IR::P4Table *node) {
const auto *annotation = node->getAnnotation("entry_restriction");
const auto *key = node->getKey();
const IR::Node *AssertsParser::postorder(IR::P4Action *actionContext) {
const auto *annotation = actionContext->getAnnotation("action_restriction");
if (annotation == nullptr) {
return actionContext;
}

IdenitifierTypeMap typeMap;
for (const auto *arg : actionContext->parameters->parameters) {
typeMap[arg->controlPlaneName()] = arg->type;
}

for (const auto *restrStr : annotation->body) {
auto restrictions =
genIRStructs(actionContext->controlPlaneName(), restrStr->text, typeMap);
// Using Z3Solver, we check the feasibility of restrictions, if they are not
// feasible, we delete keys and entries from the table to execute
// default_action
restrictionsVec.insert(restrictionsVec.begin(), restrictions.begin(), restrictions.end());
}
return actionContext;
}

const IR::Node *AssertsParser::postorder(IR::P4Table *tableContext) {
const auto *annotation = tableContext->getAnnotation("entry_restriction");
const auto *key = tableContext->getKey();
if (annotation == nullptr || key == nullptr) {
return node;
return tableContext;
}

IdenitifierTypeMap typeMap;
for (const auto *keyElement : tableContext->getKey()->keyElements) {
const auto *nameAnnot = keyElement->getAnnotation("name");
BUG_CHECK(nameAnnot != nullptr, "%1% table key without a name annotation",
annotation->name.name);
typeMap[nameAnnot->getName()] = keyElement->expression->type;
}

Z3Solver solver;
for (const auto *restrStr : annotation->body) {
auto restrictions =
genIRStructs(node->controlPlaneName(), restrStr->text, key->keyElements);
auto restrictions = genIRStructs(tableContext->controlPlaneName(), restrStr->text, typeMap);
// Using Z3Solver, we check the feasibility of restrictions, if they are not
// feasible, we delete keys and entries from the table to execute
// default_action
solver.push();
if (solver.checkSat(restrictions) == true) {
restrictionsVec.push_back(restrictions);
restrictionsVec.insert(restrictionsVec.begin(), restrictions.begin(),
restrictions.end());
continue;
}
::warning(
"Restriction %1% is not feasible. Not generating entries for table %2% and instead "
"using default action.",
restrStr, node);
restrStr, tableContext);
solver.pop();
auto *cloneTable = node->clone();
auto *cloneProperties = node->properties->clone();
auto *cloneTable = tableContext->clone();
auto *cloneProperties = tableContext->properties->clone();
IR::IndexedVector<IR::Property> properties;
for (const auto *property : cloneProperties->properties) {
if (property->name.name != "key" || property->name.name != "entries") {
if (property->name.name != "key" && property->name.name != "entries") {
properties.push_back(property);
}
}
cloneProperties->properties = properties;
cloneTable->properties = cloneProperties;
return cloneTable;
}
return node;
return tableContext;
}

Token Lexer::atom(Token::Kind kind) noexcept { return {kind, mBeg++, 1}; }
Expand Down
19 changes: 12 additions & 7 deletions backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
#include <string_view>
#include <vector>

#include "backends/p4tools/common/lib/variables.h"
#include "ir/ir.h"
#include "ir/node.h"
#include "ir/vector.h"
Expand All @@ -14,21 +15,25 @@

namespace P4Tools::P4Testgen::Bmv2 {

using P4ConstraintsVector = std::vector<std::vector<const IR::Expression *>>;
/// Maps control plane identifiers to their corresponding IR type.
/// Once we have resolved the tokens in the annotation, we can then lookup the corresponding type.
using IdenitifierTypeMap = std::map<cstring, const IR::Type *>;

class AssertsParser : public Transform {
P4ConstraintsVector &restrictionsVec;
/// A vector of restrictions imposed on the control-plane.
ConstraintsVector &restrictionsVec;

public:
explicit AssertsParser(P4ConstraintsVector &output);
explicit AssertsParser(ConstraintsVector &output);
/// A function that calls the beginning of the transformation of restrictions from a string into
/// an IR::Expression. Internally calls all other necessary functions, for example
/// combineTokensToNames and the like, to eventually get an IR expression that meets the string
/// constraint
static std::vector<const IR::Expression *> genIRStructs(
cstring tableName, cstring restrictionString,
const IR::Vector<IR::KeyElement> &keyElements);
const IR::Node *postorder(IR::P4Table *node) override;
static std::vector<const IR::Expression *> genIRStructs(cstring tableName,
cstring restrictionString,
const IdenitifierTypeMap &typeMap);
const IR::Node *postorder(IR::P4Action *actionContext) override;
const IR::Node *postorder(IR::P4Table *tableContext) override;
};

class Token {
Expand Down
Loading

0 comments on commit efb20df

Please sign in to comment.