From efb20df5f8efb40f2d90d9b0740e591a375953c6 Mon Sep 17 00:00:00 2001 From: Fabian Ruffy <5960321+fruffy@users.noreply.github.com> Date: Tue, 6 Feb 2024 16:07:54 +0100 Subject: [PATCH] [P4Testgen] Hotfixes and improvements to the P4Constraints parsers. (#4387) * Small hotfixes to prevent crashes. * Review comments and fixes. --- backends/p4tools/common/lib/variables.h | 13 +- .../modules/testgen/targets/bmv2/bmv2.cpp | 21 +-- .../modules/testgen/targets/bmv2/bmv2.h | 7 +- .../targets/bmv2/p4_asserts_parser.cpp | 99 +++++++---- .../testgen/targets/bmv2/p4_asserts_parser.h | 19 +- .../targets/bmv2/p4_refers_to_parser.cpp | 162 +++++++++++++----- .../targets/bmv2/p4_refers_to_parser.h | 35 +++- .../testgen/targets/bmv2/program_info.cpp | 6 +- .../small-step/p4_asserts_parser_test.cpp | 35 ++-- 9 files changed, 264 insertions(+), 133 deletions(-) diff --git a/backends/p4tools/common/lib/variables.h b/backends/p4tools/common/lib/variables.h index 93afa2caf84..254de3d9e43 100644 --- a/backends/p4tools/common/lib/variables.h +++ b/backends/p4tools/common/lib/variables.h @@ -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; + +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, @@ -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_ */ diff --git a/backends/p4tools/modules/testgen/targets/bmv2/bmv2.cpp b/backends/p4tools/modules/testgen/targets/bmv2/bmv2.cpp index dbc8c0a03c0..cbee30ea633 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/bmv2.cpp +++ b/backends/p4tools/modules/testgen/targets/bmv2/bmv2.cpp @@ -22,7 +22,7 @@ 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)), @@ -30,7 +30,7 @@ BMv2V1ModelCompilerResult::BMv2V1ModelCompilerResult(TestgenCompilerResult compi const P4::P4RuntimeAPI &BMv2V1ModelCompilerResult::getP4RuntimeApi() const { return p4runtimeApi; } -P4ConstraintsVector BMv2V1ModelCompilerResult::getP4ConstraintsRestrictions() const { +ConstraintsVector BMv2V1ModelCompilerResult::getP4ConstraintsRestrictions() const { return p4ConstraintsRestrictions; } @@ -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; } diff --git a/backends/p4tools/modules/testgen/targets/bmv2/bmv2.h b/backends/p4tools/modules/testgen/targets/bmv2/bmv2.h index 2db89d47391..478c6f60eba 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/bmv2.h +++ b/backends/p4tools/modules/testgen/targets/bmv2/bmv2.h @@ -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" @@ -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; diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp index eadbabbfc1e..c19b484efc5 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -28,7 +28,7 @@ static const std::vector NAMES{ "Mul", "Comment", "Unknown", "EndString", "End", }; -AssertsParser::AssertsParser(P4ConstraintsVector &output) : restrictionsVec(output) { +AssertsParser::AssertsParser(ConstraintsVector &output) : restrictionsVec(output) { setName("Restrictions"); } @@ -121,24 +121,18 @@ const IR::Expression *makeSingleExpr(std::vector 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 &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()) { type = bit; } else if (const auto *varbit = keyType->to()) { @@ -164,7 +158,7 @@ const IR::Expression *makeConstant(Token input, const IR::Vector 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 @@ -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 tokens, - const IR::Vector &keyElements) { +const IR::Expression *getIR(std::vector tokens, const IdenitifierTypeMap &typeMap) { std::vector exprVec; for (size_t idx = 0; idx < tokens.size(); idx++) { @@ -256,9 +249,9 @@ const IR::Expression *getIR(std::vector 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()) { auto *clone = constant->clone(); clone->type = rightL->type; @@ -266,18 +259,18 @@ const IR::Expression *getIR(std::vector tokens, } } 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)); } @@ -356,6 +349,11 @@ std::vector combineTokensToNumbers(std::vector input) { cstring numb = ""; std::vector 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()); @@ -468,8 +466,9 @@ std::vector removeComments(const std::vector &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 AssertsParser::genIRStructs( - cstring tableName, cstring restrictionString, const IR::Vector &keyElements) { +std::vector AssertsParser::genIRStructs(cstring tableName, + cstring restrictionString, + const IdenitifierTypeMap &typeMap) { Lexer lex(restrictionString); std::vector tmp; for (auto token = lex.next(); !token.isOneOf(Token::Kind::End, Token::Kind::Unknown); @@ -486,12 +485,12 @@ std::vector AssertsParser::genIRStructs( std::vector 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 { @@ -502,35 +501,65 @@ std::vector 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 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); } } @@ -538,7 +567,7 @@ const IR::Node *AssertsParser::postorder(IR::P4Table *node) { cloneTable->properties = cloneProperties; return cloneTable; } - return node; + return tableContext; } Token Lexer::atom(Token::Kind kind) noexcept { return {kind, mBeg++, 1}; } diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.h b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.h index 45a1b30b43a..8e37dcfed69 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.h +++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.h @@ -6,6 +6,7 @@ #include #include +#include "backends/p4tools/common/lib/variables.h" #include "ir/ir.h" #include "ir/node.h" #include "ir/vector.h" @@ -14,21 +15,25 @@ namespace P4Tools::P4Testgen::Bmv2 { -using P4ConstraintsVector = std::vector>; +/// 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; 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 genIRStructs( - cstring tableName, cstring restrictionString, - const IR::Vector &keyElements); - const IR::Node *postorder(IR::P4Table *node) override; + static std::vector 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 { diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp index b0d7c9a9b49..f56684ff184 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -1,57 +1,92 @@ #include "backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h" #include -#include -#include +#include #include #include "backends/p4tools/common/lib/variables.h" #include "ir/declaration.h" #include "ir/id.h" #include "ir/indexed_vector.h" +#include "ir/ir-generated.h" #include "ir/ir.h" +#include "ir/irutils.h" #include "ir/vector.h" #include "lib/exceptions.h" #include "lib/null.h" namespace P4Tools::P4Testgen::Bmv2 { -RefersToParser::RefersToParser(std::vector> &output) - : restrictionsVec(output) { - setName("RefersToParser"); -} +RefersToParser::RefersToParser() { setName("RefersToParser"); } -const IR::SymbolicVariable *RefersToParser::buildReferredKey(const IR::P4Control &ctrlContext, - const IR::Annotation &refersAnno) { - auto annotationList = refersAnno.body; - BUG_CHECK(annotationList.size() > 2, - "'@refers_to' annotation %1% does not have the correct format.", refersAnno); - auto srcTableRefStr = annotationList.at(0)->text; - // Build the referred key by assembling all remaining tokens. +const RefersToParser::RefersToBuiltinMap RefersToParser::REFERS_TO_BUILTIN_MAP = {{ + "multicast_group_table", + { + { + "multicast_group_id", + IR::SymbolicVariable(IR::getBitType(16), "refers_to_multicast_group_id"), + }, + { + "replica.port", + IR::SymbolicVariable(IR::getBitType(9), "refers_to_replica.port"), + }, + { + "replica.instance", + IR::SymbolicVariable(IR::getBitType(16), "refers_to_replica.instance"), + }, + }, +}}; + +cstring RefersToParser::assembleKeyReference(const IR::Vector &annotationList, + size_t offset) { // E.g., "hdr.eth.eth_type" is multiple tokens. - cstring referredKeyStr = ""; - for (uint64_t i = 2; i < annotationList.size(); i++) { - referredKeyStr += annotationList[i]->text; + std::stringstream keyReference; + for (; offset < annotationList.size(); offset++) { + keyReference << annotationList[offset]->text; } - const IR::IDeclaration *srcTableRef = nullptr; - for (const auto *decl : *ctrlContext.getDeclarations()) { - auto declName = decl->controlPlaneName(); - if (declName.endsWith(srcTableRefStr)) { - srcTableRef = decl; + return keyReference; +} + +const IR::SymbolicVariable *RefersToParser::lookUpBuiltinKey( + const IR::Annotation &refersAnno, const IR::Vector &annotationList) { + BUG_CHECK( + annotationList.size() > 3, + "'@refers_to' annotation %1% with \"builtin\" prefix does not have the correct format.", + refersAnno); + BUG_CHECK(annotationList.at(1)->text == ":" && annotationList.at(2)->text == ":", + "'@refers_to' annotation %1% does not have the correct format.", refersAnno); + cstring tableReference = ""; + size_t offset = 3; + for (; offset < annotationList.size(); offset++) { + auto token = annotationList[offset]->text; + if (token == ",") { + offset++; break; } + tableReference += token; } - BUG_CHECK(srcTableRef != nullptr, "Table %1% does not exist.", srcTableRefStr); - const auto *srcTable = srcTableRef->checkedTo(); - const auto *key = srcTable->getKey(); + cstring keyReference = assembleKeyReference(annotationList, offset); + + auto it = REFERS_TO_BUILTIN_MAP.find(tableReference); + BUG_CHECK(it != REFERS_TO_BUILTIN_MAP.end(), "Unknown table %1%", tableReference); + auto referredKey = it->second.find(keyReference); + BUG_CHECK(referredKey != it->second.end(), "Unknown key %1% in table %2%", keyReference, + tableReference); + return &referredKey->second; +} + +const IR::SymbolicVariable *RefersToParser::lookUpKeyInTable(const IR::P4Table &srcTable, + cstring keyReference) { + const auto *key = srcTable.getKey(); BUG_CHECK(key != nullptr, "Table %1% does not have any keys.", srcTable); for (const auto *keyElement : key->keyElements) { auto annotations = keyElement->annotations->annotations; const auto *nameAnnot = keyElement->getAnnotation("name"); // Some hidden tables do not have any key name annotations. BUG_CHECK(nameAnnot != nullptr, "Refers-to table key without a name annotation"); - if (referredKeyStr == nameAnnot->getName()) { - auto referredKeyName = srcTable->controlPlaneName() + "_key_" + referredKeyStr; + if (keyReference == nameAnnot->getName()) { + // TODO: Move this assembly into a library. + auto referredKeyName = srcTable.controlPlaneName() + "_key_" + keyReference; return ToolsVariables::getSymbolicVariable(keyElement->expression->type, referredKeyName); } @@ -59,38 +94,69 @@ const IR::SymbolicVariable *RefersToParser::buildReferredKey(const IR::P4Control BUG("Did not find a matching key in table %1%. ", srcTable); } -bool RefersToParser::preorder(const IR::P4Table *table) { - const auto *key = table->getKey(); +const IR::SymbolicVariable *RefersToParser::getReferencedKey(const IR::P4Control &ctrlContext, + const IR::Annotation &refersAnno) { + const auto &annotationList = refersAnno.body; + BUG_CHECK(annotationList.size() > 2, + "'@refers_to' annotation %1% does not have the correct format.", refersAnno); + + auto tableReference = annotationList.at(0)->text; + if (tableReference == "builtin") { + return lookUpBuiltinKey(refersAnno, annotationList); + } + BUG_CHECK(annotationList.at(1)->text == ",", + "'@refers_to' annotation %1% does not have the correct format.", refersAnno); + + // Try to find the table the control declarations. + // TODO: Currently this lookUp does not support aliasing and simply tries to find the first + // occurrence of a table where the suffix matches. + // Ideally, we would use originalName, but originalName currently is not preserved correctly. + const IR::IDeclaration *tableDeclaration = nullptr; + for (const auto *decl : *ctrlContext.getDeclarations()) { + auto declName = decl->controlPlaneName(); + if (declName.endsWith(tableReference)) { + tableDeclaration = decl; + break; + } + } + BUG_CHECK(tableDeclaration != nullptr, "Table %1% does not exist.", tableReference); + const auto *srcTable = tableDeclaration->checkedTo(); + + cstring keyReference = assembleKeyReference(annotationList, 2); + return lookUpKeyInTable(*srcTable, keyReference); +} + +bool RefersToParser::preorder(const IR::P4Table *tableContext) { + const auto *key = tableContext->getKey(); if (key == nullptr) { return false; } - const auto *ctrl = findOrigCtxt(); - CHECK_NULL(ctrl); + const auto *controlContext = findOrigCtxt(); + CHECK_NULL(controlContext); for (const auto *keyElement : key->keyElements) { auto annotations = keyElement->annotations->annotations; for (const auto *annotation : annotations) { - if (annotation->name.name == "refers_to") { + if (annotation->name.name == "refers_to" || annotation->name.name == "referenced_by") { const auto *nameAnnot = keyElement->getAnnotation("name"); - BUG_CHECK(nameAnnot != nullptr, "refers_to table key without a name annotation"); - const auto *referredKey = buildReferredKey(*ctrl, *annotation); - auto srcKeyName = table->controlPlaneName() + "_key_" + nameAnnot->getName(); + BUG_CHECK(nameAnnot != nullptr, "%1% table key without a name annotation", + annotation->name.name); + // TODO: Move this assembly into a library. + auto srcKeyName = tableContext->controlPlaneName() + "_key_" + nameAnnot->getName(); const auto *srcKey = ToolsVariables::getSymbolicVariable(keyElement->expression->type, srcKeyName); - auto *expr = new IR::Equ(srcKey, referredKey); - std::vector constraint; - constraint.push_back(expr); - restrictionsVec.push_back(constraint); + const auto *referredKey = getReferencedKey(*controlContext, *annotation); + restrictionsVector.push_back(new IR::Equ(srcKey, referredKey)); } } } - const auto *actionList = table->getActionList(); + const auto *actionList = tableContext->getActionList(); if (actionList == nullptr) { return false; } for (const auto *action : actionList->actionList) { - const auto *decl = ctrl->getDeclByName(action->getName().name); + const auto *decl = controlContext->getDeclByName(action->getName().name); if (decl == nullptr) { return false; } @@ -103,16 +169,16 @@ bool RefersToParser::preorder(const IR::P4Table *table) { const auto *parameter = params->parameters.at(idx); auto annotations = parameter->annotations->annotations; for (const auto *annotation : annotations) { - if (annotation->name.name == "refers_to") { - const auto *referredKey = buildReferredKey(*ctrl, *annotation); - auto srcParamName = table->controlPlaneName() + "_arg_" + + if (annotation->name.name == "refers_to" || + annotation->name.name == "referenced_by") { + const auto *referredKey = getReferencedKey(*controlContext, *annotation); + // TODO: Move this assembly into a library. + auto srcParamName = tableContext->controlPlaneName() + "_arg_" + actionCall->controlPlaneName() + std::to_string(idx); const auto *srcKey = ToolsVariables::getSymbolicVariable(parameter->type, srcParamName); - auto *expr = new IR::Equ(srcKey, referredKey); - std::vector constraint; - constraint.push_back(expr); - restrictionsVec.push_back(constraint); + auto *constraint = new IR::Equ(srcKey, referredKey); + restrictionsVector.push_back(constraint); } } } @@ -120,4 +186,6 @@ bool RefersToParser::preorder(const IR::P4Table *table) { return false; } +ConstraintsVector RefersToParser::getRestrictionsVector() const { return restrictionsVector; } + } // namespace P4Tools::P4Testgen::Bmv2 diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h index 9ad74528988..f7e0a4bc74e 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h +++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h @@ -1,27 +1,48 @@ #ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_ #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_ -#include - +#include "backends/p4tools/common/lib/variables.h" #include "ir/ir.h" #include "ir/visitor.h" namespace P4Tools::P4Testgen::Bmv2 { class RefersToParser : public Inspector { - std::vector> &restrictionsVec; + private: + /// A vector of restrictions imposed on the control-plane. + ConstraintsVector restrictionsVector; + + /// A lookup map for builtin table keys. + using RefersToBuiltinMap = std::map>; + static const RefersToBuiltinMap REFERS_TO_BUILTIN_MAP; + + /// Assemble the referenced key by concatenating all remaining tokens in the annotation. + /// TODO: We should use the annotation parser for this. + static cstring assembleKeyReference(const IR::Vector &annotationList, + size_t offset); - /// Build the referred table key by looking up the table referenced in the annotation @param + /// Lookup the key in the builtin map and return the corresponding symbolic variable. + static const IR::SymbolicVariable *lookUpBuiltinKey( + const IR::Annotation &refersAnno, const IR::Vector &annotationList); + + /// Lookup the key in the table and return the corresponding symbolic variable. + static const IR::SymbolicVariable *lookUpKeyInTable(const IR::P4Table &srcTable, + cstring keyReference); + + /// Get the referred table key by looking up the table referenced in the annotation @param /// refersAnno in the /// @param ctrlContext and retrieving the appropriate type. @returns a symbolic variable /// corresponding to the control plane entry variable. - const IR::SymbolicVariable *buildReferredKey(const IR::P4Control &ctrlContext, - const IR::Annotation &refersAnno); + static const IR::SymbolicVariable *getReferencedKey(const IR::P4Control &ctrlContext, + const IR::Annotation &refersAnno); bool preorder(const IR::P4Table *table) override; public: - explicit RefersToParser(std::vector> &output); + RefersToParser(); + + /// Returns the restrictions imposed on the control-plane. + [[nodiscard]] ConstraintsVector getRestrictionsVector() const; }; } // namespace P4Tools::P4Testgen::Bmv2 diff --git a/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp index fef177d9d9f..662525f386f 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp +++ b/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp @@ -75,10 +75,8 @@ Bmv2V1ModelProgramInfo::Bmv2V1ModelProgramInfo( new IR::Grt(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(), IR::getConstant(&PacketVars::PACKET_SIZE_VAR_TYPE, minPktSize)); - for (const auto &element : compilerResult.getP4ConstraintsRestrictions()) { - for (const auto *restriction : element) { - constraint = new IR::LAnd(constraint, restriction); - } + for (const auto &restriction : compilerResult.getP4ConstraintsRestrictions()) { + constraint = new IR::LAnd(constraint, restriction); } /// Finally, set the target constraints. diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/modules/testgen/targets/bmv2/test/small-step/p4_asserts_parser_test.cpp index 19f6d8860f3..27f7c33af07 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/modules/testgen/targets/bmv2/test/small-step/p4_asserts_parser_test.cpp @@ -6,7 +6,6 @@ #include #include -#include #include @@ -43,9 +42,9 @@ class P4TestOptions : public CompilerOptions { }; /// Vector containing pairs of restrictions and nodes to which these restrictions apply. using P4TestContext = P4CContextWithOptions; -using Restrictions = std::vector>; +using P4Tools::ConstraintsVector; -Restrictions loadExample(const char *curFile, bool flag) { +ConstraintsVector loadExample(const char *curFile, bool flag) { AutoCompileContext autoP4TestContext(new P4TestContext); auto &options = P4TestContext::get().options(); const char *argv = "./gtest-p4testgen"; @@ -75,25 +74,25 @@ Restrictions loadExample(const char *curFile, bool flag) { P4::TypeMap typeMap; P4Tools::MidEnd midEnd(options); program = program->apply(midEnd); - Restrictions result; if (flag) { + P4Tools::ConstraintsVector result; program->apply(P4Tools::P4Testgen::Bmv2::AssertsParser(result)); - } else { - program->apply(P4Tools::P4Testgen::Bmv2::RefersToParser(result)); + return result; } - return result; + P4Tools::P4Testgen::Bmv2::RefersToParser referstoParser; + program->apply(referstoParser); + return referstoParser.getRestrictionsVector(); } TEST_F(P4AssertsParserTest, RestrictionCount) { - Restrictions parsingResult = loadExample( + ConstraintsVector parsingResult = loadExample( "backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4", true); - ASSERT_EQ(parsingResult.size(), (unsigned long)1); - ASSERT_EQ(parsingResult[0].size(), (unsigned long)3); + ASSERT_EQ(parsingResult.size(), (unsigned long)3); } TEST_F(P4AssertsParserTest, Restrictions) { - Restrictions parsingResult = loadExample( + ConstraintsVector parsingResult = loadExample( "backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4", true); ASSERT_EQ(parsingResult.size(), (unsigned long)1); @@ -106,26 +105,26 @@ TEST_F(P4AssertsParserTest, Restrictions) { const auto *const2 = IR::getConstant(IR::Type_Bits::get(8), 64); const auto *operation = new IR::LAnd(new IR::Neq(expr1, const1), new IR::Neq(expr2, const2)); - ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); + ASSERT_TRUE(parsingResult[0]->equiv(*operation)); } { const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable( IR::Type_Bits::get(8), "ingress.ternary_table_key_h.h.a1"); const auto *const1 = IR::getConstant(IR::Type_Bits::get(8), 0); const auto *operation1 = new IR::Neq(expr1, const1); - ASSERT_TRUE(parsingResult[0][1]->equiv(*operation1)); + ASSERT_TRUE(parsingResult[1]->equiv(*operation1)); } { const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable( IR::Type_Bits::get(8), "ingress.ternary_table_key_h.h.a"); const auto *const2 = IR::getConstant(IR::Type_Bits::get(8), 255); const auto *operation2 = new IR::Neq(expr1, const2); - ASSERT_TRUE(parsingResult[0][2]->equiv(*operation2)); + ASSERT_TRUE(parsingResult[2]->equiv(*operation2)); } } TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { - Restrictions parsingResult = loadExample( + ConstraintsVector parsingResult = loadExample( "backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), (unsigned long)3); @@ -134,11 +133,11 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { const auto &expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), "ingress.table_2_key_h.h.b"); const auto *operation = new IR::Equ(expr1, expr2); - ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); + ASSERT_TRUE(parsingResult[0]->equiv(*operation)); } TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { - Restrictions parsingResult = loadExample( + ConstraintsVector parsingResult = loadExample( "backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), (unsigned long)3); @@ -147,7 +146,7 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { const auto *expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), "ingress.table_1_key_h.h.a"); auto *operation = new IR::Equ(expr1, expr2); - ASSERT_TRUE(parsingResult[1][0]->equiv(*operation)); + ASSERT_TRUE(parsingResult[1]->equiv(*operation)); } } // namespace Test