From 57d5b6793b6f589df4ccd2b9e86a61b4e1276549 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 12 Oct 2022 13:10:46 +0300 Subject: [PATCH 01/25] Initial commit [no-jira] --- backends/p4tools/testgen/CMakeLists.txt | 2 + .../testgen/targets/bmv2/CMakeLists.txt | 2 + .../targets/bmv2/p4_asserts_parser.cpp | 624 ++++++++++++++++++ .../testgen/targets/bmv2/p4_asserts_parser.h | 113 ++++ .../targets/bmv2/p4_refers_to_parser.cpp | 152 +++++ .../targets/bmv2/p4_refers_to_parser.h | 35 + .../testgen/targets/bmv2/program_info.cpp | 12 +- .../testgen/targets/bmv2/program_info.h | 9 +- .../test/p4-programs/bmv2_restrictions.p4 | 94 +++ .../test/p4-programs/bmv2_restrictions_2.p4 | 104 +++ .../small-step/p4_asserts_parser_test.cpp | 137 ++++ 11 files changed, 1280 insertions(+), 4 deletions(-) mode change 100644 => 100755 backends/p4tools/testgen/CMakeLists.txt mode change 100644 => 100755 backends/p4tools/testgen/targets/bmv2/CMakeLists.txt create mode 100755 backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp create mode 100755 backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h create mode 100755 backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp create mode 100755 backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h mode change 100644 => 100755 backends/p4tools/testgen/targets/bmv2/program_info.cpp mode change 100644 => 100755 backends/p4tools/testgen/targets/bmv2/program_info.h create mode 100755 backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 create mode 100755 backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 create mode 100755 backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp diff --git a/backends/p4tools/testgen/CMakeLists.txt b/backends/p4tools/testgen/CMakeLists.txt old mode 100644 new mode 100755 index abe8e8c0fc1..7c49bff9fe8 --- a/backends/p4tools/testgen/CMakeLists.txt +++ b/backends/p4tools/testgen/CMakeLists.txt @@ -48,6 +48,7 @@ set( # # XXX These should be in a library. ${P4C_SOURCE_DIR}/test/gtest/helpers.cpp ${P4C_SOURCE_DIR}/test/gtest/gtestp4c.cpp + test/gtest_utils.cpp test/lib/format_int.cpp test/lib/taint.cpp @@ -55,6 +56,7 @@ set( test/small-step/unary.cpp test/small-step/util.cpp test/small-step/value.cpp + test/small-step/p4_asserts_parser_test.cpp test/transformations/saturation_arithm.cpp test/z3-solver/asrt_model.cpp test/z3-solver/expressions.cpp diff --git a/backends/p4tools/testgen/targets/bmv2/CMakeLists.txt b/backends/p4tools/testgen/targets/bmv2/CMakeLists.txt old mode 100644 new mode 100755 index 4cf619813cd..6a83974406a --- a/backends/p4tools/testgen/targets/bmv2/CMakeLists.txt +++ b/backends/p4tools/testgen/targets/bmv2/CMakeLists.txt @@ -20,6 +20,8 @@ set( ${CMAKE_CURRENT_SOURCE_DIR}/program_info.cpp ${CMAKE_CURRENT_SOURCE_DIR}/table_stepper.cpp ${CMAKE_CURRENT_SOURCE_DIR}/target.cpp + ${CMAKE_CURRENT_SOURCE_DIR}/p4_asserts_parser.cpp + ${CMAKE_CURRENT_SOURCE_DIR}/p4_refers_to_parser.cpp ${CMAKE_CURRENT_SOURCE_DIR}/test_backend.cpp ${CMAKE_CURRENT_SOURCE_DIR}/test_spec.cpp PARENT_SCOPE diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp new file mode 100755 index 00000000000..5d07568227a --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -0,0 +1,624 @@ +#include "backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h" + +#include +#include + +#include "lib/error.h" + +#include "backends/p4tools/common/core/z3_solver.h" +#include "backends/p4tools/common/lib/ir.h" + +namespace P4Tools { + +namespace AssertsParser { + +AssertsParser::AssertsParser(std::vector>& output) + : restrictionsVec(output) { + setName("Restrictions"); +} + +bool is_space(char c) noexcept { + switch (c) { + case ' ': + case '\t': + case '\r': + return true; + default: + return false; + } +} + +std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { + static const char* const names[]{ + "Text", "True", "False", "LineStatementClose", + "Id", "Number", "Minus", "Plus", + "Dot", "FieldAcces", "MetadataAccess", "LeftParen", + "RightParen", "Equal", "NotEqual", "GreaterThan", + "GreaterEqual", "LessThan", "LessEqual", "LNot", + "Colon", "Semicolon", "Conjunction", "Disjunction", + "Implication", "Slash", "Percent", "Shr", + "Shl", "Mul", "Comment", "Unknown", + "EndString", "End", + }; + return os << names[static_cast(kind)]; +} + +const IR::Expression* makeExpr(std::vector input) { + const IR::Expression* expr = nullptr; + for (int i = 0; i < input.size(); i++) { + if (auto lOr = input[i]->to()) { + if (expr == nullptr) { + if (lOr->right->toString() == "(tmp") { + std::vector tmp; + int idx = i; + i++; + if (i + 1 == input.size()) { + expr = new IR::LOr(input[idx - 1], input[i]); + break; + } + while (i < input.size()) { + tmp.push_back(input[i]); + i++; + } + expr = new IR::LOr(input[idx - 1], makeExpr(tmp)); + break; + } + expr = new IR::LOr(input[i - 1], input[i + 1]); + continue; + } else if (lOr->right->toString() == "(tmp") { + if (i + 1 != input.size()) { + std::vector tmp; + i++; + if (i + 1 == input.size()) { + expr = new IR::LOr(input[i - 2], input[i]); + } + while (i < input.size()) { + tmp.push_back(input[i]); + i++; + } + expr = new IR::LOr(expr, makeExpr(tmp)); + } + + } else { + if (i + 1 != input.size()) { + expr = new IR::LOr(expr, input[i + 1]); + } + } + } + if (input[i]->is()) { + if (expr == nullptr) { + expr = new IR::LAnd(input[i - 1], input[i + 1]); + continue; + } else { + if (i + 1 != input.size()) expr = new IR::LAnd(expr, input[i + 1]); + } + } + } + + return expr; +} +const IR::Expression* getIR(std::vector tokens, IR::Vector keyElements) { + const IR::Expression* expr = nullptr; + std::vector exprVec; + const IR::Type_Base* type = nullptr; + + for (int i = 0; i < tokens.size(); i++) { + if (tokens[i].kind() == Token::Kind::Minus || tokens[i].kind() == Token::Kind::Plus || + tokens[i].kind() == Token::Kind::Equal || tokens[i].kind() == Token::Kind::NotEqual || + tokens[i].kind() == Token::Kind::GreaterThan || + tokens[i].kind() == Token::Kind::GreaterEqual || + tokens[i].kind() == Token::Kind::LessThan || + tokens[i].kind() == Token::Kind::LessEqual || tokens[i].kind() == Token::Kind::Slash || + tokens[i].kind() == Token::Kind::Percent || tokens[i].kind() == Token::Kind::Shr || + tokens[i].kind() == Token::Kind::Shl || tokens[i].kind() == Token::Kind::Mul || + tokens[i].kind() == Token::Kind::NotEqual) { + const IR::Expression* leftL = nullptr; + const IR::Expression* rightL = nullptr; + if (i != 0) { + i--; + i--; + } + if (i <= 0 || tokens[i].kind() == Token::Kind::Conjunction || + tokens[i].kind() == Token::Kind::Disjunction || + tokens[i].kind() == Token::Kind::LeftParen || + tokens[i].kind() == Token::Kind::Implication) { + i++; + + if (tokens[i].kind() == Token::Kind::Text) { + std::string str = static_cast(tokens[i].lexeme()); + for (auto key : keyElements) { + cstring annotationName = ""; + for (auto annotation : key->annotations->annotations) { + if (annotation->name.name == "name") { + if (annotation->body.size() > 0) + annotationName = annotation->body[0]->text; + } + } + if (str.find(key->expression->toString()) != std::string::npos || + (annotationName.size() > 0 && + str.find(annotationName) != std::string::npos)) { + if (auto bit = key->expression->type->to()) { + type = bit; + } else if (auto varbit = + key->expression->type->to()) { + type = varbit; + } else if (key->expression->type->to()) { + type = IR::Type_Bits::get(32); + } else { + type = IR::Type_Bits::get(1); + } + leftL = IRUtils::getZombieConst(type, 0, str); + break; + } + } + if (!leftL) { + type = IR::Type_Bits::get(8); + leftL = IRUtils::getZombieConst(type, 0, str); + } + + } else if (tokens[i].kind() == Token::Kind::Number) { + if (!type) { + type = IR::Type_Bits::get(8); + } + std::string str = static_cast(tokens[i].lexeme()); + leftL = IRUtils::getConstant(type, static_cast(str)); + } + } else { + leftL = exprVec[exprVec.size() - 1]; + exprVec.pop_back(); + i++; + } + i++; + i++; + i++; + if (i == tokens.size() || tokens[i].kind() == Token::Kind::Conjunction || + tokens[i].kind() == Token::Kind::Disjunction || + tokens[i].kind() == Token::Kind::RightParen || + tokens[i].kind() == Token::Kind::Implication) { + i--; + if (tokens[i].kind() == Token::Kind::Text) { + std::string str = static_cast(tokens[i].lexeme()); + for (auto key : keyElements) { + cstring annotationName = ""; + for (auto annotation : key->annotations->annotations) { + if (annotation->name.name == "name") { + if (annotation->body.size() > 0) + annotationName = annotation->body[0]->text; + } + } + if (str.find(key->expression->toString()) != std::string::npos || + (annotationName.size() > 0 && + str.find(annotationName) != std::string::npos)) { + if (auto bit = key->expression->type->to()) { + type = bit; + } else if (auto varbit = + key->expression->type->to()) { + type = varbit; + } else if (key->expression->type->to()) { + type = IR::Type_Bits::get(32); + } else { + type = IR::Type_Bits::get(1); + } + if (auto constant = leftL->to()) { + auto clone = constant->clone(); + clone->type = type; + leftL = clone; + } + rightL = IRUtils::getZombieConst(type, 0, str); + break; + } + } + if (!rightL) { + type = IR::Type_Bits::get(8); + rightL = IRUtils::getZombieConst(type, 0, str); + } + } else if (tokens[i].kind() == Token::Kind::Number) { + if (!type) { + type = IR::Type_Bits::get(8); + } + std::string str = static_cast(tokens[i].lexeme()); + rightL = IRUtils::getConstant(type, static_cast(str)); + } + } else { + i--; + int idx = i; + int endIdx = 0; + bool flag = true; + while (flag) { + i++; + if (i == tokens.size() || tokens[i].kind() == Token::Kind::Conjunction || + tokens[i].kind() == Token::Kind::Disjunction || + tokens[i].kind() == Token::Kind::RightParen) { + endIdx = i; + flag = false; + i = idx; + } + } + + std::vector rightTokens; + for (int j = idx; j < endIdx + 1; j++) { + rightTokens.push_back(tokens[j]); + } + + rightL = getIR(rightTokens, keyElements); + } + i--; + if (tokens[i].kind() == Token::Kind::Minus) expr = new IR::Sub(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Plus) expr = new IR::Add(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Equal) expr = new IR::Equ(leftL, rightL); + if (tokens[i].kind() == Token::Kind::NotEqual) expr = new IR::Neq(leftL, rightL); + if (tokens[i].kind() == Token::Kind::GreaterThan) expr = new IR::Grt(leftL, rightL); + if (tokens[i].kind() == Token::Kind::GreaterEqual) expr = new IR::Geq(leftL, rightL); + if (tokens[i].kind() == Token::Kind::LessThan) expr = new IR::Lss(leftL, rightL); + if (tokens[i].kind() == Token::Kind::LessEqual) expr = new IR::Leq(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Slash) expr = new IR::Div(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Percent) expr = new IR::Mod(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Shr) expr = new IR::Shr(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Shl) expr = new IR::Shl(leftL, rightL); + if (tokens[i].kind() == Token::Kind::Mul) expr = new IR::Mul(leftL, rightL); + if (tokens[i].kind() == Token::Kind::NotEqual) expr = new IR::Neq(leftL, rightL); + exprVec.push_back(expr); + + } else if (tokens[i].kind() == Token::Kind::LNot) { + auto flag = true; + int idx = i; + cstring str = ""; + auto first = true; + while (flag) { + i++; + if (tokens[i].kind() == Token::Kind::LeftParen) { + first = false; + continue; + } else if (first) { + break; + } + if (tokens[i].kind() != Token::Kind::RightParen) { + str += static_cast(tokens[i].lexeme()); + } else { + flag = false; + } + } + i = idx; + if (str.size() == 0) { + str = "tmp"; + } + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID(str))); + exprVec.push_back(new IR::LNot(expr1)); + } else if (tokens[i].kind() == Token::Kind::Implication) { + auto tmp = exprVec[exprVec.size() - 1]; + exprVec.pop_back(); + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + exprVec.push_back(new IR::LNot(expr1)); + exprVec.push_back(tmp); + const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("(tmp"))); + exprVec.push_back(new IR::LOr(expr1, expr2)); + } else if (tokens[i].kind() == Token::Kind::Disjunction) { + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + exprVec.push_back(new IR::LOr(expr1, expr2)); + } else if (tokens[i].kind() == Token::Kind::Conjunction) { + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + exprVec.push_back(new IR::LAnd(expr1, expr2)); + } + } + std::vector tmp; + for (int i = 0; i < exprVec.size(); i++) { + if (auto lNot = exprVec[i]->to()) { + i++; + auto lNotStr = lNot->expr->toString(); + + auto binary = exprVec[i]->checkedTo()->clone(); + if (auto subBin = binary->left->to()) { + cstring str = subBin->getStringOp(); + str.replace(" ", ""); + + if (lNotStr.find(str)) { + binary->left = new IR::LNot(binary->left); + tmp.push_back(binary); + continue; + } + } + + tmp.push_back(new IR::LNot(exprVec[i])); + continue; + } else { + tmp.push_back(exprVec[i]); + } + } + if (tmp.size() == 1) { + return expr; + } + + expr = makeExpr(tmp); + + return expr; +} + +std::vector AssertsParser::genIRStructs(cstring str) { + Lexer lex(str); + std::vector tmp; + std::vector result; + Token prevToken = Token(Token::Kind::Unknown, " ", 1); + cstring txt = ""; + cstring numb = ""; + for (auto token = lex.next(); !token.is_one_of(Token::Kind::End, Token::Kind::Unknown); + token = lex.next()) { + if (prevToken.kind() == Token::Kind::Text && token.kind() == Token::Kind::Number) { + txt += static_cast(token.lexeme()); + continue; + } + if (token.kind() == Token::Kind::Text) { + auto strtmp = static_cast(token.lexeme()); + if (strtmp == "." && prevToken.kind() == Token::Kind::Number) { + ::error( + "Syntax error, unexpected INTEGER. P4 does not support floating point values. " + "Exiting"); + } + txt += strtmp; + if (prevToken.kind() == Token::Kind::Number) { + txt = static_cast(prevToken.lexeme()) + txt; + tmp.pop_back(); + } + } else { + if (txt.size() > 0) { + tmp.push_back(Token(Token::Kind::Text, txt, txt.size())); + txt = ""; + } + tmp.push_back(token); + } + + prevToken = token; + } + std::vector tokens; + prevToken = Token(Token::Kind::Unknown, " ", 1); + for (int i = 0; i < tmp.size(); i++) { + if (tmp[i].kind() == Token::Kind::Text) { + auto str = static_cast(tmp[i].lexeme()); + + if (str.rfind("0x", 0) == 0 || str.rfind("0X", 0) == 0) { + cstring cstr = str; + tokens.push_back(Token(Token::Kind::Number, cstr, cstr.size())); + continue; + } + auto substr = str.substr(0, str.find("::mask")); + if (substr != str) { + cstring cstr = tableName + "_mask_" + substr; + tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + continue; + } + substr = str.substr(0, str.find("::prefix_length")); + if (substr != str) { + cstring cstr = tableName + "_lpm_prefix_" + substr; + tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + continue; + } + + substr = str.substr(0, str.find("::priority")); + if (substr != str) { + cstring cstr = tableName + "_priority"; + tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + continue; + } + + if (str == "true") { + tokens.push_back(Token(Token::Kind::Number, "1", 1)); + continue; + } + + if (str == "false") { + tokens.push_back(Token(Token::Kind::Number, "0", 1)); + continue; + } + + if (str.find("isValid") != std::string::npos) { + i++; + cstring cString = str + static_cast(tmp[i].lexeme()); + if (tmp[i + 1].kind() == Token::Kind::Text) { + cString += static_cast(tmp[i + 1].lexeme()); + i++; + } + cString += static_cast(tmp[i + 1].lexeme()); + i++; + cString = tableName + "_key_" + cString; + tokens.push_back(Token(Token::Kind::Text, cString, cString.size())); + continue; + } + + cstring cstr = tableName + "_key_" + str; + tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + continue; + } + if (tmp[i].kind() == Token::Kind::Number) { + numb += static_cast(tmp[i].lexeme()); + if (i + 1 == tmp.size()) { + tokens.push_back(Token(Token::Kind::Number, numb, numb.size())); + numb = ""; + continue; + } + } else { + if (numb.size() > 0) { + tokens.push_back(Token(Token::Kind::Number, numb, numb.size())); + numb = ""; + } + tokens.push_back(tmp[i]); + } + } + tmp.clear(); + bool flag = true; + for (int i = 0; i < tokens.size(); i++) { + if (tokens[i].kind() == Token::Kind::Comment) { + flag = false; + continue; + } + if (tokens[i].kind() == Token::Kind::EndString) { + flag = true; + continue; + } + if (flag) { + tmp.push_back(tokens[i]); + } + } + tokens.clear(); + + for (int i = 0; i < tmp.size(); i++) { + if (tmp[i].kind() == Token::Kind::Semicolon) { + auto expr = getIR(tokens, keyElements); + result.push_back(expr); + tokens.clear(); + } else if (i == tmp.size() - 1) { + tokens.push_back(tmp[i]); + auto expr = getIR(tokens, keyElements); + result.push_back(expr); + tokens.clear(); + } else { + tokens.push_back(tmp[i]); + } + } + + return result; +} + +const IR::Node* AssertsParser::postorder(IR::P4Table* node) { + tableName = node->controlPlaneName(); + if (node->getKey()) { + keyElements = node->getKey()->keyElements; + for (auto annotation : node->annotations->annotations) { + if (annotation->name.name == "entry_restriction") { + for (auto restrStr : annotation->body) { + auto restrictions = genIRStructs(restrStr->text); + Z3Solver solver; + if (solver.checkSat(restrictions) == true) { + restrictionsVec.push_back(restrictions); + } else { + auto cloneTable = node->clone(); + auto cloneProperties = node->properties->clone(); + IR::IndexedVector properties; + for (auto property : cloneProperties->properties) { + if (property->name.name != "key" || property->name.name != "entries") + properties.push_back(property); + } + cloneProperties->properties = properties; + cloneTable->properties = cloneProperties; + return cloneTable; + } + } + } + } + } + return node; +} + +Token Lexer::atom(Token::Kind kind) noexcept { return Token(kind, m_beg++, 1); } + +Token Lexer::next() noexcept { + while (is_space(peek())) get(); + + switch (peek()) { + case '\0': + return Token(Token::Kind::End, m_beg, 1); + case '\n': + get(); + return Token(Token::Kind::EndString, m_beg, 1); + default: + return atom(Token::Kind::Text); + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': + return atom(Token::Kind::Number); + case '(': + return atom(Token::Kind::LeftParen); + case ')': + return atom(Token::Kind::RightParen); + case '=': + get(); + if (get() == '=') { + get(); + return Token(Token::Kind::Equal, "==", 2); + } + prev(); + return atom(Token::Kind::Unknown); + case '!': + get(); + if (get() == '=') { + get(); + return Token(Token::Kind::NotEqual, "!=", 2); + } + prev(); + return atom(Token::Kind::LNot); + case '-': + get(); + if (get() == '>') { + get(); + return Token(Token::Kind::Implication, "->", 2); + } + prev(); + return atom(Token::Kind::Minus); + case '<': + get(); + if (get() == '=') { + get(); + return Token(Token::Kind::LessEqual, "<=", 2); + } + prev(); + if (get() == '<') { + return Token(Token::Kind::Shl, "<<", 2); + } + prev(); + return atom(Token::Kind::LessThan); + case '>': + get(); + if (get() == '=') { + get(); + return Token(Token::Kind::GreaterEqual, ">=", 2); + } + prev(); + if (get() == '>') { + return Token(Token::Kind::Shr, ">>", 2); + } + prev(); + return atom(Token::Kind::GreaterThan); + case ';': + return atom(Token::Kind::Semicolon); + case '&': + get(); + if (get() == '&') { + get(); + return Token(Token::Kind::Conjunction, "&&", 2); + } + prev(); + return atom(Token::Kind::Text); + case '|': + get(); + if (get() == '|') { + get(); + return Token(Token::Kind::Disjunction, "||", 2); + } + prev(); + return atom(Token::Kind::Text); + case '+': + return atom(Token::Kind::Plus); + case '/': + get(); + if (get() == '/') { + get(); + return Token(Token::Kind::Comment, "//", 2); + } + prev(); + return atom(Token::Kind::Slash); + case '%': + return atom(Token::Kind::Percent); + case '*': + return atom(Token::Kind::Mul); + } +} +} // namespace AssertsParser + +} // namespace P4Tools diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h new file mode 100755 index 00000000000..67b8ed13fb1 --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h @@ -0,0 +1,113 @@ +#ifndef TESTGEN_TARGETS_BMV2_P4_ASSERTS_PARSER_H_ +#define TESTGEN_TARGETS_BMV2_P4_ASSERTS_PARSER_H_ + +#include +#include +#include +#include +#include +#include + +#include "ir/ir.h" + +namespace P4Tools { +namespace AssertsParser { + +class AssertsParser : public Transform { + std::vector>& restrictionsVec; + IR::Vector keyElements; + cstring tableName; + + public: + explicit AssertsParser(std::vector>& output); + std::vector genIRStructs(cstring str); + const IR::Node* postorder(IR::P4Table* node) override; +}; + +class Token { + public: + enum class Kind { + Text, + True, + False, + LineStatementClose, // \n + Id, // this, this.foo + Number, // 1, 2, -1, 5.2, -5.3 + Minus, // - + Plus, // + + Dot, // . + FieldAcces, // :: (after key) + MetadataAccess, // :: (otherwise) + LeftParen, // ( + RightParen, // ) + Equal, // == + NotEqual, // != + GreaterThan, // > + GreaterEqual, // >= + LessThan, // < + LessEqual, // <= + LNot, // ! + Colon, // : + Semicolon, // ; + Conjunction, // && + Disjunction, // || + Implication, // -> + Slash, // / + Percent, // % + Shr, // >> + Shl, // << + Mul, // * + Comment, // // + Unknown, + EndString, + End, + }; + + Kind m_kind{}; + std::string_view m_lexeme{}; + explicit Token(Kind kind) noexcept : m_kind{kind} {} + + Token(Kind kind, const char* beg, std::size_t len) noexcept + : m_kind{kind}, m_lexeme(beg, len) {} + + Token(Kind kind, const char* beg, const char* end) noexcept + : m_kind{kind}, m_lexeme(beg, std::distance(beg, end)) {} + + Kind kind() const noexcept { return m_kind; } + + void kind(Kind kind) noexcept { m_kind = kind; } + + bool is(Kind kind) const noexcept { return m_kind == kind; } + + bool is_not(Kind kind) const noexcept { return m_kind != kind; } + + bool is_one_of(Kind k1, Kind k2) const noexcept { return is(k1) || is(k2); } + + template + bool is_one_of(Kind k1, Kind k2, Ts... ks) const noexcept { + return is(k1) || is_one_of(k2, ks...); + } + + std::string_view lexeme() const noexcept { return m_lexeme; } + + void lexeme(std::string_view lexeme) noexcept { m_lexeme = std::move(lexeme); } +}; + +class Lexer { + public: + explicit Lexer(const char* beg) noexcept : m_beg{beg} {} + + Token next() noexcept; + const char* m_beg = nullptr; + + private: + Token atom(Token::Kind) noexcept; + + char peek() const noexcept { return *m_beg; } + char prev() noexcept { return *m_beg--; } + char get() noexcept { return *m_beg++; } +}; +} // namespace AssertsParser +} // namespace P4Tools + +#endif /* TESTGEN_TARGETS_BMV2_P4_ASSERTS_PARSER_H_ */ diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp new file mode 100755 index 00000000000..4e8a5419723 --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -0,0 +1,152 @@ +#include "backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h" + +#include + +#include "backends/p4tools/common/lib/ir.h" + +namespace P4Tools { + +namespace RefersToParser { + +RefersToParser::RefersToParser(std::vector>& output) + : restrictionsVec(output) { + setName("RefersToParser"); +} + +void RefersToParser::createConstraint(bool table, cstring currentName, cstring currentKeyName, + cstring destKeyName, cstring destTableName, + const IR::Type* type) { + cstring tmp = ""; + if (table) + tmp = currentName + "_key_" + currentKeyName; + else + tmp = currentName + currentKeyName; + auto left = IRUtils::getZombieConst(type, 0, tmp); + std::string str = static_cast(currentName); + std::vector elems; + std::stringstream ss(str); + std::string item; + while (std::getline(ss, item, '.')) { + elems.push_back(item); + } + str = ""; + for (auto i = 0; i < elems.size() - 1; i++) { + str += elems[i] + "."; + } + tmp = str + destTableName + "_key_" + destKeyName; + auto right = IRUtils::getZombieConst(type, 0, tmp); + auto expr = new IR::Equ(left, right); + std::vector constraint; + constraint.push_back(expr); + restrictionsVec.push_back(constraint); +} +const IR::Node* RefersToParser::postorder(IR::Annotation* annotation) { + const IR::P4Action* prevAction = nullptr; + if (annotation->name.name == "refers_to") { + if (auto action = findOrigCtxt()) { + if (prevAction != action) { + actionVector.push_back(action); + prevAction = action; + } + } else if (auto keys = findOrigCtxt()) { + auto table = findOrigCtxt(); + CHECK_NULL(table); + auto key = findOrigCtxt(); + CHECK_NULL(key); + auto it = find(keys->keyElements.begin(), keys->keyElements.end(), key); + if (it != keys->keyElements.end()) { + int id = it - keys->keyElements.begin(); + createRefersToConstraint(key->annotations->annotations, key->expression->type, + table->controlPlaneName(), id, false, + key->expression->toString()); + } + } + } + return annotation; +} + +const IR::P4Action* RefersToParser::findAction(const IR::ActionListElement* input) { + for (auto element : actionVector) { + if (input->getName().name == element->name.name) { + return element; + } + } + return nullptr; +} + +// Builds a variable name from the body of the "refers_to" annotation. +// The build starts at index 2 because 0 is the table name and 1 is ",". +cstring buildName(IR::Vector input) { + cstring result = ""; + for (auto i = 2; i < input.size(); i++) { + result += input[i]->text; + } + return result; +} + +void RefersToParser::createRefersToConstraint(IR::Vector annotations, + const IR::Type* inputType, cstring controlPlaneName, + int id, bool isParameter, cstring inputName) { + cstring destTableName = ""; + cstring destKeyName = ""; + cstring currentKeyName = inputName; + const IR::Type* type = nullptr; + for (auto annotation : annotations) { + if (annotation->name.name == "refers_to") { + destTableName = annotation->body[0]->text; + destKeyName = buildName(annotation->body); + } + if (!isParameter) { + if (annotation->name.name == "name") { + if (annotation->body.size() > 0) currentKeyName = annotation->body[0]->text; + } + } + + if (destTableName.size() > 0 && destKeyName.size() > 0) { + if (auto bit = inputType->to()) { + type = bit; + } else if (auto varbit = inputType->to()) { + type = varbit; + } else if (inputType->to()) { + type = IR::Type_Bits::get(32); + } else { + type = IR::Type_Bits::get(1); + } + if (isParameter) { + currentKeyName = "_param_" + inputName + std::to_string(id); + createConstraint(false, controlPlaneName, currentKeyName, destKeyName, + destTableName, type); + } else { + createConstraint(true, controlPlaneName, currentKeyName, destKeyName, destTableName, + type); + } + } + destTableName = ""; + destKeyName = ""; + } +} + +const IR::Node* RefersToParser::postorder(IR::ActionListElement* action) { + auto findedAction = findAction(action); + if (!findedAction) { + return action; + } + if (auto table = findOrigCtxt()) { + if (findedAction->parameters) { + int id = 0; + for (auto parameter : findedAction->parameters->parameters) { + if (parameter->annotations) { + createRefersToConstraint(parameter->annotations->annotations, parameter->type, + table->controlPlaneName(), id, true, + findedAction->controlPlaneName()); + } + id++; + } + } + } + + return action; +} +} // namespace RefersToParser + +} // namespace P4Tools diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h new file mode 100755 index 00000000000..39c3d31e6c6 --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h @@ -0,0 +1,35 @@ +#ifndef TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_ +#define TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_ + +#include +#include +#include +#include +#include +#include + +#include "ir/ir.h" + +namespace P4Tools { +namespace RefersToParser { + +class RefersToParser : public Transform { + std::vector>& restrictionsVec; + std::vector actionVector; + const IR::P4Action* findAction(const IR::ActionListElement* input); + void createRefersToConstraint(IR::Vector annotations, const IR::Type* inputType, + cstring controlPlaneName, int id, bool isParameter, + cstring inputName); + + public: + explicit RefersToParser(std::vector>& output); + const IR::Node* postorder(IR::ActionListElement* action) override; + const IR::Node* postorder(IR::Annotation* annotation) override; + void createConstraint(bool table, cstring currentName, cstring currentKeyName, + cstring destKeyName, cstring destTableName, const IR::Type* type); +}; + +} // namespace RefersToParser +} // namespace P4Tools + +#endif /* TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_ */ diff --git a/backends/p4tools/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/testgen/targets/bmv2/program_info.cpp old mode 100644 new mode 100755 index d0275d6272b..69896c1a99b --- a/backends/p4tools/testgen/targets/bmv2/program_info.cpp +++ b/backends/p4tools/testgen/targets/bmv2/program_info.cpp @@ -14,6 +14,8 @@ #include "backends/p4tools/testgen/core/target.h" #include "backends/p4tools/testgen/lib/concolic.h" #include "backends/p4tools/testgen/targets/bmv2/concolic.h" +#include "backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h" +#include "backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h" namespace P4Tools { @@ -52,9 +54,17 @@ BMv2_V1ModelProgramInfo::BMv2_V1ModelProgramInfo( } // Sending a too short packet in BMV2 produces nonsense, so we require the packet size to be // larger than 32 bits - targetConstraints = + const IR::Operation_Binary* constraint = new IR::Grt(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(), IRUtils::getConstant(ExecutionState::getPacketSizeVarType(), 32)); + program->apply(AssertsParser::AssertsParser(restrictionsVec)); + program->apply(RefersToParser::RefersToParser(restrictionsVec)); + for (auto element : restrictionsVec) { + for (auto restriction : element) { + constraint = new IR::LAnd(constraint, restriction); + } + } + targetConstraints = constraint; } const ordered_map* diff --git a/backends/p4tools/testgen/targets/bmv2/program_info.h b/backends/p4tools/testgen/targets/bmv2/program_info.h old mode 100644 new mode 100755 index b918a942bf1..1810dddf723 --- a/backends/p4tools/testgen/targets/bmv2/program_info.h +++ b/backends/p4tools/testgen/targets/bmv2/program_info.h @@ -1,5 +1,5 @@ -#ifndef BACKENDS_P4TOOLS_TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ -#define BACKENDS_P4TOOLS_TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ +#ifndef TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ +#define TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ #include @@ -31,6 +31,9 @@ class BMv2_V1ModelProgramInfo : public ProgramInfo { /// The bit width of standard_metadata.parser_error. static const IR::Type_Bits parserErrBits; + /// Vector containing pairs of restrictions and nodes to which these restrictions apply. + std::vector> restrictionsVec; + /// This function contains an imperative specification of the inter-pipe interaction in the /// target. std::vector processDeclaration(const IR::Type_Declaration* typeDecl, @@ -72,4 +75,4 @@ class BMv2_V1ModelProgramInfo : public ProgramInfo { } // namespace P4Tools -#endif /* BACKENDS_P4TOOLS_TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ */ +#endif /* TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ */ diff --git a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 new file mode 100755 index 00000000000..888c380c989 --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 @@ -0,0 +1,94 @@ +#include + +header ethernet_t { + bit<48> dst_addr; + bit<48> src_addr; + bit<16> eth_type; +} + +header H { + bit<8> a; + bit<8> a1; + bit<8> b; +} + +struct Headers { + ethernet_t eth_hdr; + H h; +} + +struct Meta { } + +parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) { + state start { + pkt.extract(h.eth_hdr); + transition parse_h; + } + state parse_h { + pkt.extract(h.h); + transition accept; + } +} + +control vrfy(inout Headers h, inout Meta meta) { + apply { } +} + + +control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { + + action MyAction1() { + h.h.b = 1; + } + + action MyAction2() { + h.h.b = 2; + } + + action MyAction3() { + h.h.b = 3; + } + @entry_restriction(" + h.h.a1::mask != 0 && h.h.a1::prefix_length != 64; + h.h.a1 != 0; + h.h.a != 0xFF; + ") + table ternary_table { + key = { + h.h.isValid() : exact @name("valid"); + h.h.a : exact; + h.h.a1 : ternary; + } + + actions = { + NoAction; + MyAction1; + MyAction2; + MyAction3; + } + + size = 1024; + default_action = NoAction(); + } + + apply { + ternary_table.apply(); + } +} + +control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) { + apply { } +} + +control update(inout Headers h, inout Meta m) { + apply { } +} + +control deparser(packet_out pkt, in Headers h) { + apply { + pkt.emit(h); + } +} + + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; \ No newline at end of file diff --git a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 new file mode 100755 index 00000000000..af3628ee24b --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 @@ -0,0 +1,104 @@ +#include + +header ethernet_t { + bit<48> dst_addr; + bit<48> src_addr; + bit<16> eth_type; +} + +header H { + bit<8> a; + bit<8> a1; + bit<8> b; +} + +struct Headers { + ethernet_t eth_hdr; + H h; +} + +struct Meta { } + +parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) { + state start { + pkt.extract(h.eth_hdr); + transition parse_h; + } + state parse_h { + pkt.extract(h.h); + transition accept; + } +} + +control vrfy(inout Headers h, inout Meta meta) { + apply { } +} + + +control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { + + action MyAction1(@refers_to(table_1 , h.h.a) bit<8> input ) { + h.h.b = 1; + } + + action MyAction2() { + h.h.b = 2; + } + + action MyAction3() { + h.h.b = 3; + } + table table_1 { + key = { + h.h.a : exact @refers_to(table_2 , h.h.a); + } + + actions = { + NoAction; + MyAction1; + MyAction2; + MyAction3; + } + + size = 1024; + default_action = NoAction(); + } + + table table_2 { + key = { + h.h.a : exact; + } + + actions = { + NoAction; + MyAction1; + MyAction2; + MyAction3; + } + + size = 1024; + default_action = NoAction(); + } + + apply { + table_2.apply(); + table_1.apply(); + } +} + +control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) { + apply { } +} + +control update(inout Headers h, inout Meta m) { + apply { } +} + +control deparser(packet_out pkt, in Headers h) { + apply { + pkt.emit(h); + } +} + + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; \ No newline at end of file diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp new file mode 100755 index 00000000000..c7eee911d8d --- /dev/null +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -0,0 +1,137 @@ +#include "backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h" + +#include + +#include +#include +#include +#include + +#include + +#include "backends/p4test/version.h" +#include "frontends/common/parseInput.h" +#include "frontends/p4/frontend.h" +#include "gtest/gtest-message.h" +#include "gtest/gtest-test-part.h" +#include "gtest/gtest.h" +#include "ir/ir.h" +#include "ir/node.h" +#include "lib/log.h" +#include "test/gtest/env.h" + +#include "backends/p4tools/common/compiler/midend.h" +#include "backends/p4tools/common/lib/ir.h" +#include "backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h" +#include "backends/p4tools/testgen/test/gtest_utils.h" +#include "backends/p4tools/testgen/test/small-step/util.h" + +namespace Test { +class P4AssertsParserTest : public P4ToolsTest {}; +class P4TestOptions : public CompilerOptions { + public: + virtual ~P4TestOptions() = default; + P4TestOptions() = default; + P4TestOptions(const P4TestOptions&) = default; + P4TestOptions(P4TestOptions&&) = delete; + P4TestOptions& operator=(const P4TestOptions&) = default; + P4TestOptions& operator=(P4TestOptions&&) = delete; +}; +/// Vector containing pairs of restrictions and nodes to which these restrictions apply. +using P4TestContext = P4CContextWithOptions; +using Restrictions = std::vector>; + +Restrictions loadExample(const char* curFile, bool flag) { + AutoCompileContext autoP4TestContext(new P4TestContext); + auto& options = P4TestContext::get().options(); + const char* argv = "./gtest-p4testgen"; + options.process(1, (char* const*)&argv); + options.langVersion = CompilerOptions::FrontendVersion::P4_16; + std::string includeDir = std::string(buildPath) + std::string("p4include"); + auto* originalEnv = getenv("P4C_16_INCLUDE_PATH"); + setenv("P4C_16_INCLUDE_PATH", includeDir.c_str(), 1); + options.compilerVersion = P4TEST_VERSION_STRING; + const IR::P4Program* program = nullptr; + options.file = sourcePath; + options.file += curFile; + if (access(options.file, 0) != 0) { + // Subpath for bf-p4c-compilers. + options.file = sourcePath; + options.file += curFile; + } + program = P4::parseP4File(options); + if (originalEnv == nullptr) { + unsetenv("P4C_16_INCLUDE_PATH"); + } else { + setenv("P4C_16_INCLUDE_PATH", originalEnv, 1); + } + P4::FrontEnd frontend; + program = frontend.run(options, program); + CHECK_NULL(program); + P4::ReferenceMap refMap; + P4::TypeMap typeMap; + P4Tools::MidEnd midEnd(options); + program = program->apply(midEnd); + Restrictions result; + if (flag) + program->apply(P4Tools::AssertsParser::AssertsParser(result)); + else + program->apply(P4Tools::RefersToParser::RefersToParser(result)); + return result; +} + +TEST_F(P4AssertsParserTest, RestrictionCount) { + Restrictions parsingResult = loadExample( + "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4", true); + ASSERT_EQ(parsingResult.size(), 1); + ASSERT_EQ(parsingResult[0].size(), 3); +} + +TEST_F(P4AssertsParserTest, Restrictions) { + Restrictions parsingResult = loadExample( + "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4", true); + ASSERT_EQ(parsingResult.size(), 1); + auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_mask_h.h.a1"); + auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_lpm_prefix_h.h.a1"); + auto const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); + auto const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 64); + auto operation = new IR::LAnd(new IR::Neq(expr1, const1), new IR::Neq(expr2,const2)); + expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_key_h.h.a1"); + auto operation1 = new IR::Neq(expr1,const1 ); + expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_key_h.h.a"); + const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 255); + auto operation2 = new IR::Neq(expr1,const2 ); + ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); + ASSERT_TRUE(parsingResult[0][1]->equiv(*operation1)); + ASSERT_TRUE(parsingResult[0][2]->equiv(*operation2)); +} + +TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { + Restrictions parsingResult = loadExample( + "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); + ASSERT_EQ(parsingResult.size(), 2); + auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.table_1_key_h.h.a"); + auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.table_2_key_h.h.a"); + auto operation = new IR::Equ(expr1, expr2); + ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); +} + +TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { + Restrictions parsingResult = loadExample( + "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); + ASSERT_EQ(parsingResult.size(), 2); + auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.table_1_param_ingress.MyAction10"); + auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.table_1_key_h.h.a"); + auto operation = new IR::Equ(expr1, expr2); + ASSERT_TRUE(parsingResult[1][0]->equiv(*operation)); +} + +} // namespace Test \ No newline at end of file From 1042558d112358a03340a8b4be747dad507e1537 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 12 Oct 2022 13:14:39 +0300 Subject: [PATCH 02/25] Fix [no-jira] --- .../testgen/test/small-step/p4_asserts_parser_test.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp index c7eee911d8d..c3adf5dc46a 100755 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -126,7 +126,7 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), 2); - auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_param_ingress.MyAction10"); auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); @@ -134,4 +134,4 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { ASSERT_TRUE(parsingResult[1][0]->equiv(*operation)); } -} // namespace Test \ No newline at end of file +} // namespace Test From 8648a3683af836161c73b8e1e598788bfbdff674 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 12 Oct 2022 14:24:15 +0300 Subject: [PATCH 03/25] Fix format [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 3 +-- .../small-step/p4_asserts_parser_test.cpp | 26 +++++++++---------- 2 files changed, 14 insertions(+), 15 deletions(-) mode change 100755 => 100644 backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp mode change 100755 => 100644 backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp old mode 100755 new mode 100644 index 5d07568227a..43c273a6cd8 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -3,10 +3,9 @@ #include #include -#include "lib/error.h" - #include "backends/p4tools/common/core/z3_solver.h" #include "backends/p4tools/common/lib/ir.h" +#include "lib/error.h" namespace P4Tools { diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp old mode 100755 new mode 100644 index c3adf5dc46a..a5082beaff2 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -10,6 +10,8 @@ #include #include "backends/p4test/version.h" +#include "backends/p4tools/common/compiler/midend.h" +#include "backends/p4tools/common/lib/ir.h" #include "frontends/common/parseInput.h" #include "frontends/p4/frontend.h" #include "gtest/gtest-message.h" @@ -20,8 +22,6 @@ #include "lib/log.h" #include "test/gtest/env.h" -#include "backends/p4tools/common/compiler/midend.h" -#include "backends/p4tools/common/lib/ir.h" #include "backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h" #include "backends/p4tools/testgen/test/gtest_utils.h" #include "backends/p4tools/testgen/test/small-step/util.h" @@ -97,14 +97,14 @@ TEST_F(P4AssertsParserTest, Restrictions) { "ingress.ternary_table_lpm_prefix_h.h.a1"); auto const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); auto const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 64); - auto operation = new IR::LAnd(new IR::Neq(expr1, const1), new IR::Neq(expr2,const2)); + auto operation = new IR::LAnd(new IR::Neq(expr1, const1), new IR::Neq(expr2, const2)); expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_key_h.h.a1"); - auto operation1 = new IR::Neq(expr1,const1 ); + "ingress.ternary_table_key_h.h.a1"); + auto operation1 = new IR::Neq(expr1, const1); expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_key_h.h.a"); + "ingress.ternary_table_key_h.h.a"); const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 255); - auto operation2 = new IR::Neq(expr1,const2 ); + auto operation2 = new IR::Neq(expr1, const2); ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); ASSERT_TRUE(parsingResult[0][1]->equiv(*operation1)); ASSERT_TRUE(parsingResult[0][2]->equiv(*operation2)); @@ -114,10 +114,10 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), 2); - auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.table_1_key_h.h.a"); - auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.table_2_key_h.h.a"); + auto expr1 = + P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); + auto expr2 = + P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.a"); auto operation = new IR::Equ(expr1, expr2); ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); } @@ -128,8 +128,8 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { ASSERT_EQ(parsingResult.size(), 2); auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_param_ingress.MyAction10"); - auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.table_1_key_h.h.a"); + auto expr2 = + P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); auto operation = new IR::Equ(expr1, expr2); ASSERT_TRUE(parsingResult[1][0]->equiv(*operation)); } From 9f25917d459d6b712e9fbabf6cd691b2a925c6e5 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Fri, 14 Oct 2022 12:01:25 +0300 Subject: [PATCH 04/25] Fix types [no-jira] --- .../testgen/targets/bmv2/p4_asserts_parser.cpp | 14 +++++++------- .../testgen/targets/bmv2/p4_refers_to_parser.cpp | 4 ++-- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 43c273a6cd8..650ffb2bd8c 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -44,12 +44,12 @@ std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { const IR::Expression* makeExpr(std::vector input) { const IR::Expression* expr = nullptr; - for (int i = 0; i < input.size(); i++) { + for (long unsigned int i = 0; i < input.size(); i++) { if (auto lOr = input[i]->to()) { if (expr == nullptr) { if (lOr->right->toString() == "(tmp") { std::vector tmp; - int idx = i; + long unsigned int idx = i; i++; if (i + 1 == input.size()) { expr = new IR::LOr(input[idx - 1], input[i]); @@ -101,7 +101,7 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector exprVec; const IR::Type_Base* type = nullptr; - for (int i = 0; i < tokens.size(); i++) { + for (long unsigned int i = 0; i < tokens.size(); i++) { if (tokens[i].kind() == Token::Kind::Minus || tokens[i].kind() == Token::Kind::Plus || tokens[i].kind() == Token::Kind::Equal || tokens[i].kind() == Token::Kind::NotEqual || tokens[i].kind() == Token::Kind::GreaterThan || @@ -302,7 +302,7 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector tmp; - for (int i = 0; i < exprVec.size(); i++) { + for (long unsigned int i = 0; i < exprVec.size(); i++) { if (auto lNot = exprVec[i]->to()) { i++; auto lNotStr = lNot->expr->toString(); @@ -371,7 +371,7 @@ std::vector AssertsParser::genIRStructs(cstring str) { } std::vector tokens; prevToken = Token(Token::Kind::Unknown, " ", 1); - for (int i = 0; i < tmp.size(); i++) { + for (long unsigned int i = 0; i < tmp.size(); i++) { if (tmp[i].kind() == Token::Kind::Text) { auto str = static_cast(tmp[i].lexeme()); @@ -445,7 +445,7 @@ std::vector AssertsParser::genIRStructs(cstring str) { } tmp.clear(); bool flag = true; - for (int i = 0; i < tokens.size(); i++) { + for (long unsigned int i = 0; i < tokens.size(); i++) { if (tokens[i].kind() == Token::Kind::Comment) { flag = false; continue; @@ -460,7 +460,7 @@ std::vector AssertsParser::genIRStructs(cstring str) { } tokens.clear(); - for (int i = 0; i < tmp.size(); i++) { + for (long unsigned int i = 0; i < tmp.size(); i++) { if (tmp[i].kind() == Token::Kind::Semicolon) { auto expr = getIR(tokens, keyElements); result.push_back(expr); diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp index 4e8a5419723..80c369be089 100755 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -30,7 +30,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c elems.push_back(item); } str = ""; - for (auto i = 0; i < elems.size() - 1; i++) { + for (long unsigned int i = 0; i < elems.size() - 1; i++) { str += elems[i] + "."; } tmp = str + destTableName + "_key_" + destKeyName; @@ -78,7 +78,7 @@ const IR::P4Action* RefersToParser::findAction(const IR::ActionListElement* inpu // The build starts at index 2 because 0 is the table name and 1 is ",". cstring buildName(IR::Vector input) { cstring result = ""; - for (auto i = 2; i < input.size(); i++) { + for (long unsigned int i = 2; i < input.size(); i++) { result += input[i]->text; } return result; From f57bf7c7c596d9b24bf6a5a4586a6df14db96e7e Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Fri, 14 Oct 2022 14:07:30 +0300 Subject: [PATCH 05/25] Fix types [no-jira] --- .../testgen/test/small-step/p4_asserts_parser_test.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp index a5082beaff2..4e78b1a40f5 100644 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -83,14 +83,14 @@ Restrictions loadExample(const char* curFile, bool flag) { TEST_F(P4AssertsParserTest, RestrictionCount) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4", true); - ASSERT_EQ(parsingResult.size(), 1); - ASSERT_EQ(parsingResult[0].size(), 3); + ASSERT_EQ(parsingResult.size(), (unsigned long)1); + ASSERT_EQ(parsingResult[0].size(), (unsigned long)3); } TEST_F(P4AssertsParserTest, Restrictions) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4", true); - ASSERT_EQ(parsingResult.size(), 1); + ASSERT_EQ(parsingResult.size(), (unsigned long)1); auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.ternary_table_mask_h.h.a1"); auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, @@ -113,7 +113,7 @@ TEST_F(P4AssertsParserTest, Restrictions) { TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); - ASSERT_EQ(parsingResult.size(), 2); + ASSERT_EQ(parsingResult.size(), (unsigned long)2); auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); auto expr2 = @@ -125,7 +125,7 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); - ASSERT_EQ(parsingResult.size(), 2); + ASSERT_EQ(parsingResult.size(), (unsigned long)2); auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_param_ingress.MyAction10"); auto expr2 = From c3e85f1db5a80fc62b436e1ccc382165262844b6 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Fri, 14 Oct 2022 16:33:58 +0300 Subject: [PATCH 06/25] Fix types [no-jira] --- backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 650ffb2bd8c..03ef13b5847 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -101,7 +101,7 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector exprVec; const IR::Type_Base* type = nullptr; - for (long unsigned int i = 0; i < tokens.size(); i++) { + for (int i = 0; i < (int)tokens.size(); i++) { if (tokens[i].kind() == Token::Kind::Minus || tokens[i].kind() == Token::Kind::Plus || tokens[i].kind() == Token::Kind::Equal || tokens[i].kind() == Token::Kind::NotEqual || tokens[i].kind() == Token::Kind::GreaterThan || @@ -170,7 +170,7 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector tokens, IR::Vector Date: Wed, 19 Oct 2022 15:46:04 +0300 Subject: [PATCH 07/25] Add new comments and rework [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 498 ++++++++++-------- .../testgen/targets/bmv2/p4_asserts_parser.h | 28 +- .../targets/bmv2/p4_refers_to_parser.cpp | 9 +- .../targets/bmv2/p4_refers_to_parser.h | 7 + .../testgen/targets/bmv2/program_info.cpp | 10 +- .../testgen/targets/bmv2/program_info.h | 9 +- 6 files changed, 315 insertions(+), 246 deletions(-) mode change 100755 => 100644 backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h mode change 100755 => 100644 backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp mode change 100755 => 100644 backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h mode change 100755 => 100644 backends/p4tools/testgen/targets/bmv2/program_info.cpp diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 03ef13b5847..ff015522bdb 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -16,6 +16,36 @@ AssertsParser::AssertsParser(std::vector>& ou setName("Restrictions"); } +/// The function to get kind from token +Token::Kind Token::kind() const noexcept { return m_kind; } +/// The function to replace the token kind with another kind +void Token::kind(Token::Kind kind) noexcept { m_kind = kind; } +/// Kind comparison function. Allows you to compare token kind with the specified kind and return +/// bool values, replacement for == +bool Token::is(Token::Kind kind) const noexcept { return m_kind == kind; } +/// Kind comparison function. Allows you to compare token kind with the specified kind and return +/// bool values, replacement for != +bool Token::is_not(Token::Kind kind) const noexcept { return m_kind != kind; } +/// Functions for multiple comparison kind +bool Token::is_one_of(Token::Kind k1, Token::Kind k2) const noexcept { return is(k1) || is(k2); } +template +bool Token::is_one_of(Token::Kind k1, Token::Kind k2, Ts... ks) const noexcept { + return is(k1) || is_one_of(k2, ks...); +} +/// The function to get lexeme from token +std::string_view Token::lexeme() const noexcept { return m_lexeme; } +/// The function to replace the token lexeme with another lexeme +void Token::lexeme(std::string_view lexeme) noexcept { m_lexeme = std::move(lexeme); } + +/// Function to get the current character +char Lexer::peek() const noexcept { return *m_beg; } +/// The function advances the iterator one index back and returns the character corresponding to the +/// position of the iterator +char Lexer::prev() noexcept { return *m_beg--; } +/// The function advances the iterator one index forward and returns the character corresponding to +/// the position of the iterator +char Lexer::get() noexcept { return *m_beg++; } + bool is_space(char c) noexcept { switch (c) { case ' ': @@ -42,126 +72,121 @@ std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { return os << names[static_cast(kind)]; } -const IR::Expression* makeExpr(std::vector input) { +/// The function combines IR expressions separated by the "or" ,"and" operators +/// and also by the implication which is indicated by "(tmp" ,inside the algorithm, +/// for the convenience of determining the order of expressions. At the output, we get one +/// expression. For example, at the input we have a vector of expressions: [IR::Expression, IR::LOr +/// with name "(tmp", IR::Expression, IR::LAnd, IR::Expression] The result will be an IR::Expression +/// equal to !IR::Expression || (IR::Expression && IR::Expression) +const IR::Expression* makeSingleExpr(std::vector input) { const IR::Expression* expr = nullptr; for (long unsigned int i = 0; i < input.size(); i++) { if (auto lOr = input[i]->to()) { - if (expr == nullptr) { - if (lOr->right->toString() == "(tmp") { - std::vector tmp; - long unsigned int idx = i; - i++; - if (i + 1 == input.size()) { - expr = new IR::LOr(input[idx - 1], input[i]); - break; - } - while (i < input.size()) { - tmp.push_back(input[i]); - i++; - } - expr = new IR::LOr(input[idx - 1], makeExpr(tmp)); + if (lOr->right->toString() == "(tmp") { + if (i + 1 == input.size()) break; + std::vector tmp; + long unsigned int idx = i; + i++; + if (i + 1 == input.size()) { + expr = new IR::LOr(input[idx - 1], input[i]); break; } - expr = new IR::LOr(input[i - 1], input[i + 1]); - continue; - } else if (lOr->right->toString() == "(tmp") { - if (i + 1 != input.size()) { - std::vector tmp; + while (i < input.size()) { + tmp.push_back(input[i]); i++; - if (i + 1 == input.size()) { - expr = new IR::LOr(input[i - 2], input[i]); - } - while (i < input.size()) { - tmp.push_back(input[i]); - i++; - } - expr = new IR::LOr(expr, makeExpr(tmp)); } - + if (expr == nullptr) + expr = new IR::LOr(input[idx - 1], makeSingleExpr(tmp)); + else + expr = new IR::LOr(expr, makeSingleExpr(tmp)); + break; } else { - if (i + 1 != input.size()) { + if (i + 1 == input.size()) break; + if (expr == nullptr) + expr = new IR::LOr(input[i - 1], input[i + 1]); + else expr = new IR::LOr(expr, input[i + 1]); - } } } if (input[i]->is()) { - if (expr == nullptr) { + if (i + 1 == input.size()) break; + if (expr == nullptr) expr = new IR::LAnd(input[i - 1], input[i + 1]); - continue; - } else { - if (i + 1 != input.size()) expr = new IR::LAnd(expr, input[i + 1]); - } + else + expr = new IR::LAnd(expr, input[i + 1]); } } return expr; } + +/// Determines the token type according to the table key and generates a zombie constant for it. +const IR::Expression* makeConstant(Token input, IR::Vector keyElements) { + const IR::Type_Base* type = nullptr; + const IR::Expression* result = nullptr; + std::string str = static_cast(input.lexeme()); + if (input.is(Token::Kind::Text)) { + for (auto key : keyElements) { + cstring annotationName = ""; + for (auto annotation : key->annotations->annotations) { + if (annotation->name.name == "name") { + if (annotation->body.size() > 0) annotationName = annotation->body[0]->text; + } + } + if (str.find(key->expression->toString()) != std::string::npos || + (annotationName.size() > 0 && str.find(annotationName) != std::string::npos)) { + if (auto bit = key->expression->type->to()) { + type = bit; + } else if (auto varbit = key->expression->type->to()) { + type = varbit; + } else if (key->expression->type->to()) { + type = IR::Type_Bits::get(32); + } else { + type = IR::Type_Bits::get(1); + } + result = IRUtils::getZombieConst(type, 0, str); + break; + } + } + if (!result) { + type = IR::Type_Bits::get(8); + result = IRUtils::getZombieConst(type, 0, str); + } + + } else if (input.is(Token::Kind::Number)) { + if (!type) { + type = IR::Type_Bits::get(8); + } + result = IRUtils::getConstant(type, static_cast(str)); + } + + return result; +} + +/// Converts a vector of tokens into a single IR:Expression +/// 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, IR::Vector keyElements) { const IR::Expression* expr = nullptr; std::vector exprVec; - const IR::Type_Base* type = nullptr; for (int i = 0; i < (int)tokens.size(); i++) { - if (tokens[i].kind() == Token::Kind::Minus || tokens[i].kind() == Token::Kind::Plus || - tokens[i].kind() == Token::Kind::Equal || tokens[i].kind() == Token::Kind::NotEqual || - tokens[i].kind() == Token::Kind::GreaterThan || - tokens[i].kind() == Token::Kind::GreaterEqual || - tokens[i].kind() == Token::Kind::LessThan || - tokens[i].kind() == Token::Kind::LessEqual || tokens[i].kind() == Token::Kind::Slash || - tokens[i].kind() == Token::Kind::Percent || tokens[i].kind() == Token::Kind::Shr || - tokens[i].kind() == Token::Kind::Shl || tokens[i].kind() == Token::Kind::Mul || - tokens[i].kind() == Token::Kind::NotEqual) { + if (tokens[i].is_one_of( + Token::Kind::Minus, Token::Kind::Plus, Token::Kind::Equal, Token::Kind::NotEqual, + Token::Kind::GreaterThan, Token::Kind::GreaterEqual, Token::Kind::LessThan, + Token::Kind::LessEqual, Token::Kind::Slash, Token::Kind::Percent, Token::Kind::Shr, + Token::Kind::Shl, Token::Kind::Mul, Token::Kind::NotEqual)) { const IR::Expression* leftL = nullptr; const IR::Expression* rightL = nullptr; if (i != 0) { i--; i--; } - if (i <= 0 || tokens[i].kind() == Token::Kind::Conjunction || - tokens[i].kind() == Token::Kind::Disjunction || - tokens[i].kind() == Token::Kind::LeftParen || - tokens[i].kind() == Token::Kind::Implication) { + if (i <= 0 || tokens[i].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, + Token::Kind::LeftParen, Token::Kind::Implication)) { i++; - - if (tokens[i].kind() == Token::Kind::Text) { - std::string str = static_cast(tokens[i].lexeme()); - for (auto key : keyElements) { - cstring annotationName = ""; - for (auto annotation : key->annotations->annotations) { - if (annotation->name.name == "name") { - if (annotation->body.size() > 0) - annotationName = annotation->body[0]->text; - } - } - if (str.find(key->expression->toString()) != std::string::npos || - (annotationName.size() > 0 && - str.find(annotationName) != std::string::npos)) { - if (auto bit = key->expression->type->to()) { - type = bit; - } else if (auto varbit = - key->expression->type->to()) { - type = varbit; - } else if (key->expression->type->to()) { - type = IR::Type_Bits::get(32); - } else { - type = IR::Type_Bits::get(1); - } - leftL = IRUtils::getZombieConst(type, 0, str); - break; - } - } - if (!leftL) { - type = IR::Type_Bits::get(8); - leftL = IRUtils::getZombieConst(type, 0, str); - } - - } else if (tokens[i].kind() == Token::Kind::Number) { - if (!type) { - type = IR::Type_Bits::get(8); - } - std::string str = static_cast(tokens[i].lexeme()); - leftL = IRUtils::getConstant(type, static_cast(str)); - } + leftL = makeConstant(tokens[i], keyElements); } else { leftL = exprVec[exprVec.size() - 1]; exprVec.pop_back(); @@ -170,53 +195,15 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector(tokens[i].lexeme()); - for (auto key : keyElements) { - cstring annotationName = ""; - for (auto annotation : key->annotations->annotations) { - if (annotation->name.name == "name") { - if (annotation->body.size() > 0) - annotationName = annotation->body[0]->text; - } - } - if (str.find(key->expression->toString()) != std::string::npos || - (annotationName.size() > 0 && - str.find(annotationName) != std::string::npos)) { - if (auto bit = key->expression->type->to()) { - type = bit; - } else if (auto varbit = - key->expression->type->to()) { - type = varbit; - } else if (key->expression->type->to()) { - type = IR::Type_Bits::get(32); - } else { - type = IR::Type_Bits::get(1); - } - if (auto constant = leftL->to()) { - auto clone = constant->clone(); - clone->type = type; - leftL = clone; - } - rightL = IRUtils::getZombieConst(type, 0, str); - break; - } - } - if (!rightL) { - type = IR::Type_Bits::get(8); - rightL = IRUtils::getZombieConst(type, 0, str); - } - } else if (tokens[i].kind() == Token::Kind::Number) { - if (!type) { - type = IR::Type_Bits::get(8); - } - std::string str = static_cast(tokens[i].lexeme()); - rightL = IRUtils::getConstant(type, static_cast(str)); + rightL = makeConstant(tokens[i], keyElements); + if (auto constant = leftL->to()) { + auto clone = constant->clone(); + clone->type = rightL->type; + leftL = clone; } } else { i--; @@ -225,15 +212,14 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector rightTokens; for (int j = idx; j < endIdx + 1; j++) { rightTokens.push_back(tokens[j]); @@ -242,36 +228,36 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector(tokens[i].lexeme()); } else { flag = false; @@ -283,7 +269,7 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector tokens, IR::Vector tokens, IR::Vector AssertsParser::genIRStructs(cstring str) { - Lexer lex(str); - std::vector tmp; - std::vector result; +/// Combines successive tokens into variable names. +/// Returns a vector with tokens combined into names. +/// For example, at the input we have a vector of tokens: +/// [a(Text),c(Text),b(text), +(Plus), 1(Number),2(number)] +/// The result will be [acb(Text), +(Plus), 1(Number),2(number)] +std::vector combineTokensToNames(std::vector input) { + std::vector result; Token prevToken = Token(Token::Kind::Unknown, " ", 1); cstring txt = ""; - cstring numb = ""; - for (auto token = lex.next(); !token.is_one_of(Token::Kind::End, Token::Kind::Unknown); - token = lex.next()) { - if (prevToken.kind() == Token::Kind::Text && token.kind() == Token::Kind::Number) { - txt += static_cast(token.lexeme()); + for (long unsigned int i = 0; i < input.size(); i++) { + if (prevToken.is(Token::Kind::Text) && input[i].is(Token::Kind::Number)) { + txt += static_cast(input[i].lexeme()); continue; } - if (token.kind() == Token::Kind::Text) { - auto strtmp = static_cast(token.lexeme()); - if (strtmp == "." && prevToken.kind() == Token::Kind::Number) { + if (input[i].is(Token::Kind::Text)) { + auto strtmp = static_cast(input[i].lexeme()); + if (strtmp == "." && prevToken.is(Token::Kind::Number)) { ::error( "Syntax error, unexpected INTEGER. P4 does not support floating point values. " "Exiting"); } txt += strtmp; - if (prevToken.kind() == Token::Kind::Number) { + if (prevToken.is(Token::Kind::Number)) { txt = static_cast(prevToken.lexeme()) + txt; - tmp.pop_back(); + result.pop_back(); } } else { if (txt.size() > 0) { - tmp.push_back(Token(Token::Kind::Text, txt, txt.size())); + result.push_back(Token(Token::Kind::Text, txt, txt.size())); txt = ""; } - tmp.push_back(token); + result.push_back(input[i]); } - prevToken = token; + prevToken = input[i]; } - std::vector tokens; - prevToken = Token(Token::Kind::Unknown, " ", 1); - for (long unsigned int i = 0; i < tmp.size(); i++) { - if (tmp[i].kind() == Token::Kind::Text) { - auto str = static_cast(tmp[i].lexeme()); + return result; +} + +/// Combines successive tokens into numbers. For converting boolean or Hex, Octal values ​​to +/// numbers we must first use combineTokensToNames. Returns a vector with tokens combined into +/// numbers. For example, at the input we have a vector of tokens: [a(Text),c(Text),b(text), +/// +(Plus), 1(Number),2(number)] The result will be [a(Text),c(Text),b(text), +(Plus), 12(number)] +/// Other examples : +/// [acb(text), ||(Disjunction), true(text)] -> [acb(text), ||(Disjunction), 1(number)] - This +/// example is possible only after executing combineTokensToNames, since to convert bool values, +/// they must first be collected from text tokens in the combineTokensToNames function +/// [2(Number), 5(number), 5(number), ==(Equal), 0xff(Text)] -> [255(number), ==(Equal), +/// 0xff(Number)] - This example is possible only after executing combineTokensToNames +std::vector combineTokensToNumbers(std::vector input) { + cstring numb = ""; + std::vector result; + for (long unsigned int i = 0; i < input.size(); i++) { + if (input[i].is(Token::Kind::Text)) { + auto str = static_cast(input[i].lexeme()); if (str.rfind("0x", 0) == 0 || str.rfind("0X", 0) == 0) { cstring cstr = str; - tokens.push_back(Token(Token::Kind::Number, cstr, cstr.size())); + result.push_back(Token(Token::Kind::Number, cstr, cstr.size())); + continue; + } + + if (str == "true") { + result.push_back(Token(Token::Kind::Number, "1", 1)); + continue; + } + + if (str == "false") { + result.push_back(Token(Token::Kind::Number, "0", 1)); + continue; + } + } + if (input[i].is(Token::Kind::Number)) { + numb += static_cast(input[i].lexeme()); + if (i + 1 == input.size()) { + result.push_back(Token(Token::Kind::Number, numb, numb.size())); + numb = ""; continue; } + } else { + if (numb.size() > 0) { + result.push_back(Token(Token::Kind::Number, numb, numb.size())); + numb = ""; + } + result.push_back(input[i]); + } + } + return result; +} +/// Convert access tokens or keys into table keys. For converting access tokens or keys ​​to +/// table keys we must first use combineTokensToNames. Returns a vector with tokens converted into +/// table keys. +/// For example, at the input we have a vector of tokens: +/// [key::mask(Text), ==(Equal) , 0(Number)] The result will be [tableName_mask_key(Text), ==(Equal) +/// , 0(Number)] Other examples : [key::prefix_length(Text), ==(Equal) , 0(Number)] -> +/// [tableName_lpm_prefix_key(Text), ==(Equal) , 0(Number)] [key::priority(Text), ==(Equal) , +/// 0(Number)] -> [tableName_priority_key(Text), ==(Equal) , 0(Number)] [Name01(Text), ==(Equal) , +/// 0(Number)] -> [tableName_key_Name01(Text), ==(Equal) , 0(Number)] +std::vector combineTokensToTableKeys(std::vector input, cstring tableName) { + std::vector result; + for (long unsigned int i = 0; i < input.size(); i++) { + if (input[i].is(Token::Kind::Text)) { + auto str = static_cast(input[i].lexeme()); + auto substr = str.substr(0, str.find("::mask")); if (substr != str) { cstring cstr = tableName + "_mask_" + substr; - tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); continue; } substr = str.substr(0, str.find("::prefix_length")); if (substr != str) { cstring cstr = tableName + "_lpm_prefix_" + substr; - tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); continue; } substr = str.substr(0, str.find("::priority")); if (substr != str) { cstring cstr = tableName + "_priority"; - tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); - continue; - } - - if (str == "true") { - tokens.push_back(Token(Token::Kind::Number, "1", 1)); - continue; - } - - if (str == "false") { - tokens.push_back(Token(Token::Kind::Number, "0", 1)); + result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); continue; } if (str.find("isValid") != std::string::npos) { i++; - cstring cString = str + static_cast(tmp[i].lexeme()); - if (tmp[i + 1].kind() == Token::Kind::Text) { - cString += static_cast(tmp[i + 1].lexeme()); + cstring cString = str + static_cast(input[i].lexeme()); + if (input[i + 1].is(Token::Kind::Text)) { + cString += static_cast(input[i + 1].lexeme()); i++; } - cString += static_cast(tmp[i + 1].lexeme()); + cString += static_cast(input[i + 1].lexeme()); i++; cString = tableName + "_key_" + cString; - tokens.push_back(Token(Token::Kind::Text, cString, cString.size())); + result.push_back(Token(Token::Kind::Text, cString, cString.size())); continue; } cstring cstr = tableName + "_key_" + str; - tokens.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); continue; - } - if (tmp[i].kind() == Token::Kind::Number) { - numb += static_cast(tmp[i].lexeme()); - if (i + 1 == tmp.size()) { - tokens.push_back(Token(Token::Kind::Number, numb, numb.size())); - numb = ""; - continue; - } } else { - if (numb.size() > 0) { - tokens.push_back(Token(Token::Kind::Number, numb, numb.size())); - numb = ""; - } - tokens.push_back(tmp[i]); + result.push_back(input[i]); } } - tmp.clear(); + return result; +} + +/// Removes comment lines from the input array. +/// For example, at the input we have a vector of tokens: +/// [//(Comment), CommentText(Text) , (EndString) , 28(Number), .....] -> [28(Number), .....] +std::vector removeComments(std::vector input) { + std::vector result; bool flag = true; - for (long unsigned int i = 0; i < tokens.size(); i++) { - if (tokens[i].kind() == Token::Kind::Comment) { + for (long unsigned int i = 0; i < input.size(); i++) { + if (input[i].is(Token::Kind::Comment)) { flag = false; continue; } - if (tokens[i].kind() == Token::Kind::EndString) { + if (input[i].is(Token::Kind::EndString)) { flag = true; continue; } if (flag) { - tmp.push_back(tokens[i]); + result.push_back(input[i]); } } - tokens.clear(); + return result; +} + +/// 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 str) { + Lexer lex(str); + std::vector tmp; + for (auto token = lex.next(); !token.is_one_of(Token::Kind::End, Token::Kind::Unknown); + token = lex.next()) { + tmp.push_back(token); + } + std::vector result; + + tmp = combineTokensToNames(tmp); + tmp = combineTokensToNumbers(tmp); + tmp = combineTokensToTableKeys(tmp, tableName); + tmp = removeComments(tmp); + std::vector tokens; for (long unsigned int i = 0; i < tmp.size(); i++) { - if (tmp[i].kind() == Token::Kind::Semicolon) { + if (tmp[i].is(Token::Kind::Semicolon)) { auto expr = getIR(tokens, keyElements); result.push_back(expr); tokens.clear(); @@ -486,6 +533,9 @@ const IR::Node* AssertsParser::postorder(IR::P4Table* node) { if (annotation->name.name == "entry_restriction") { for (auto restrStr : annotation->body) { auto restrictions = genIRStructs(restrStr->text); + /// 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 Z3Solver solver; if (solver.checkSat(restrictions) == true) { restrictionsVec.push_back(restrictions); diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h old mode 100755 new mode 100644 index 67b8ed13fb1..ef74fb80e56 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h @@ -20,6 +20,10 @@ class AssertsParser : public Transform { public: explicit AssertsParser(std::vector>& 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 std::vector genIRStructs(cstring str); const IR::Node* postorder(IR::P4Table* node) override; }; @@ -73,24 +77,22 @@ class Token { Token(Kind kind, const char* beg, const char* end) noexcept : m_kind{kind}, m_lexeme(beg, std::distance(beg, end)) {} - Kind kind() const noexcept { return m_kind; } + Kind kind() const noexcept; - void kind(Kind kind) noexcept { m_kind = kind; } + void kind(Kind kind) noexcept; - bool is(Kind kind) const noexcept { return m_kind == kind; } + bool is(Kind kind) const noexcept; - bool is_not(Kind kind) const noexcept { return m_kind != kind; } + bool is_not(Kind kind) const noexcept; - bool is_one_of(Kind k1, Kind k2) const noexcept { return is(k1) || is(k2); } + bool is_one_of(Kind k1, Kind k2) const noexcept; template - bool is_one_of(Kind k1, Kind k2, Ts... ks) const noexcept { - return is(k1) || is_one_of(k2, ks...); - } + bool is_one_of(Kind k1, Kind k2, Ts... ks) const noexcept; - std::string_view lexeme() const noexcept { return m_lexeme; } + std::string_view lexeme() const noexcept; - void lexeme(std::string_view lexeme) noexcept { m_lexeme = std::move(lexeme); } + void lexeme(std::string_view lexeme) noexcept; }; class Lexer { @@ -103,9 +105,9 @@ class Lexer { private: Token atom(Token::Kind) noexcept; - char peek() const noexcept { return *m_beg; } - char prev() noexcept { return *m_beg--; } - char get() noexcept { return *m_beg++; } + char peek() const noexcept; + char prev() noexcept; + char get() noexcept; }; } // namespace AssertsParser } // namespace P4Tools diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp old mode 100755 new mode 100644 index 80c369be089..5036c8390a4 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -13,6 +13,8 @@ RefersToParser::RefersToParser(std::vector>& setName("RefersToParser"); } +/// Builds names for the zombie constant and then creates a zombie constant and builds the refers_to +/// constraints based on them void RefersToParser::createConstraint(bool table, cstring currentName, cstring currentKeyName, cstring destKeyName, cstring destTableName, const IR::Type* type) { @@ -40,6 +42,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c constraint.push_back(expr); restrictionsVec.push_back(constraint); } + const IR::Node* RefersToParser::postorder(IR::Annotation* annotation) { const IR::P4Action* prevAction = nullptr; if (annotation->name.name == "refers_to") { @@ -64,7 +67,8 @@ const IR::Node* RefersToParser::postorder(IR::Annotation* annotation) { } return annotation; } - +// Finds a P4Action in the actionVector according +/// to the specified input argument which is an ActionListElement const IR::P4Action* RefersToParser::findAction(const IR::ActionListElement* input) { for (auto element : actionVector) { if (input->getName().name == element->name.name) { @@ -84,6 +88,9 @@ cstring buildName(IR::Vector input) { return result; } +/// An intermediate function that determines the type for future variables and partially +/// collects their names for them, after which it calls the createConstraint function, +/// which completes the construction of the constraint void RefersToParser::createRefersToConstraint(IR::Vector annotations, const IR::Type* inputType, cstring controlPlaneName, int id, bool isParameter, cstring inputName) { diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h old mode 100755 new mode 100644 index 39c3d31e6c6..30c3c4b88bc --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h @@ -16,7 +16,12 @@ namespace RefersToParser { class RefersToParser : public Transform { std::vector>& restrictionsVec; std::vector actionVector; + /// Finds a P4Action in the actionVector according + /// to the specified input argument which is an ActionListElement const IR::P4Action* findAction(const IR::ActionListElement* input); + /// An intermediate function that determines the type for future variables and partially + /// collects their names for them, after which it calls the createConstraint function, + /// which completes the construction of the constraint void createRefersToConstraint(IR::Vector annotations, const IR::Type* inputType, cstring controlPlaneName, int id, bool isParameter, cstring inputName); @@ -25,6 +30,8 @@ class RefersToParser : public Transform { explicit RefersToParser(std::vector>& output); const IR::Node* postorder(IR::ActionListElement* action) override; const IR::Node* postorder(IR::Annotation* annotation) override; + /// Builds names for the zombie constant and then creates a zombie constant and builds the + /// refers_to constraints based on them void createConstraint(bool table, cstring currentName, cstring currentKeyName, cstring destKeyName, cstring destTableName, const IR::Type* type); }; diff --git a/backends/p4tools/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/testgen/targets/bmv2/program_info.cpp old mode 100755 new mode 100644 index 69896c1a99b..20fb5b479fe --- a/backends/p4tools/testgen/targets/bmv2/program_info.cpp +++ b/backends/p4tools/testgen/targets/bmv2/program_info.cpp @@ -52,12 +52,18 @@ BMv2_V1ModelProgramInfo::BMv2_V1ModelProgramInfo( pipelineSequence.insert(pipelineSequence.end(), subResult.begin(), subResult.end()); ++pipeIdx; } - // Sending a too short packet in BMV2 produces nonsense, so we require the packet size to be - // larger than 32 bits + /// Sending a too short packet in BMV2 produces nonsense, so we require the packet size to be + /// larger than 32 bits const IR::Operation_Binary* constraint = new IR::Grt(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(), IRUtils::getConstant(ExecutionState::getPacketSizeVarType(), 32)); + /// Vector containing pairs of restrictions and nodes to which these restrictions apply. + std::vector> restrictionsVec; + /// Defines all "entry_restriction" and then converts restrictions from string to IR + /// expressions, and stores them in restrictionsVec to move targetConstraints further. program->apply(AssertsParser::AssertsParser(restrictionsVec)); + /// Defines all "refers_to" and then converts restrictions from string to IR expressions, + /// and stores them in restrictionsVec to move targetConstraints further. program->apply(RefersToParser::RefersToParser(restrictionsVec)); for (auto element : restrictionsVec) { for (auto restriction : element) { diff --git a/backends/p4tools/testgen/targets/bmv2/program_info.h b/backends/p4tools/testgen/targets/bmv2/program_info.h index 1810dddf723..b918a942bf1 100755 --- a/backends/p4tools/testgen/targets/bmv2/program_info.h +++ b/backends/p4tools/testgen/targets/bmv2/program_info.h @@ -1,5 +1,5 @@ -#ifndef TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ -#define TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ +#ifndef BACKENDS_P4TOOLS_TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ +#define BACKENDS_P4TOOLS_TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ #include @@ -31,9 +31,6 @@ class BMv2_V1ModelProgramInfo : public ProgramInfo { /// The bit width of standard_metadata.parser_error. static const IR::Type_Bits parserErrBits; - /// Vector containing pairs of restrictions and nodes to which these restrictions apply. - std::vector> restrictionsVec; - /// This function contains an imperative specification of the inter-pipe interaction in the /// target. std::vector processDeclaration(const IR::Type_Declaration* typeDecl, @@ -75,4 +72,4 @@ class BMv2_V1ModelProgramInfo : public ProgramInfo { } // namespace P4Tools -#endif /* TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ */ +#endif /* BACKENDS_P4TOOLS_TESTGEN_TARGETS_BMV2_PROGRAM_INFO_H_ */ From f8c72b5427e49d622ad5cec7277cf38ddf914b2f Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 19 Oct 2022 16:06:34 +0300 Subject: [PATCH 08/25] Fix [no-jira] --- .../testgen/test/small-step/p4_asserts_parser_test.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp index 4e78b1a40f5..8290193e378 100644 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -20,12 +20,15 @@ #include "ir/ir.h" #include "ir/node.h" #include "lib/log.h" -#include "test/gtest/env.h" #include "backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h" #include "backends/p4tools/testgen/test/gtest_utils.h" #include "backends/p4tools/testgen/test/small-step/util.h" +/// Variables are declared in "test/gtest/env.h" which is already included in reachablity.cpp +extern const char* sourcePath; +extern const char* buildPath; + namespace Test { class P4AssertsParserTest : public P4ToolsTest {}; class P4TestOptions : public CompilerOptions { From 6be3eca3a807642b97fb02de93b82af32821042b Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 19 Oct 2022 21:25:17 +0300 Subject: [PATCH 09/25] Rework refers_to parser [no-jira] --- .../testgen/targets/bmv2/p4_refers_to_parser.cpp | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp index 5036c8390a4..dd212d8d061 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -94,22 +94,12 @@ cstring buildName(IR::Vector input) { void RefersToParser::createRefersToConstraint(IR::Vector annotations, const IR::Type* inputType, cstring controlPlaneName, int id, bool isParameter, cstring inputName) { - cstring destTableName = ""; - cstring destKeyName = ""; cstring currentKeyName = inputName; const IR::Type* type = nullptr; for (auto annotation : annotations) { if (annotation->name.name == "refers_to") { - destTableName = annotation->body[0]->text; - destKeyName = buildName(annotation->body); - } - if (!isParameter) { - if (annotation->name.name == "name") { - if (annotation->body.size() > 0) currentKeyName = annotation->body[0]->text; - } - } - - if (destTableName.size() > 0 && destKeyName.size() > 0) { + cstring destTableName = annotation->body[0]->text; + cstring destKeyName = buildName(annotation->body); if (auto bit = inputType->to()) { type = bit; } else if (auto varbit = inputType->to()) { @@ -128,8 +118,6 @@ void RefersToParser::createRefersToConstraint(IR::Vector annotat type); } } - destTableName = ""; - destKeyName = ""; } } From 0d93e8f2c9682cc8b0554f73aa69148b72883a57 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Tue, 25 Oct 2022 14:50:17 +0300 Subject: [PATCH 10/25] Parser rework [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 432 +++++++++--------- .../testgen/targets/bmv2/p4_asserts_parser.h | 7 +- 2 files changed, 227 insertions(+), 212 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index ff015522bdb..3cf482b5000 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -35,7 +35,7 @@ bool Token::is_one_of(Token::Kind k1, Token::Kind k2, Ts... ks) const noexcept { /// The function to get lexeme from token std::string_view Token::lexeme() const noexcept { return m_lexeme; } /// The function to replace the token lexeme with another lexeme -void Token::lexeme(std::string_view lexeme) noexcept { m_lexeme = std::move(lexeme); } +void Token::lexeme(std::string_view lexeme) noexcept { m_lexeme = lexeme; } /// Function to get the current character char Lexer::peek() const noexcept { return *m_beg; } @@ -46,7 +46,7 @@ char Lexer::prev() noexcept { return *m_beg--; } /// the position of the iterator char Lexer::get() noexcept { return *m_beg++; } -bool is_space(char c) noexcept { +bool isSpace(char c) noexcept { switch (c) { case ' ': case '\t': @@ -58,18 +58,16 @@ bool is_space(char c) noexcept { } std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { - static const char* const names[]{ - "Text", "True", "False", "LineStatementClose", - "Id", "Number", "Minus", "Plus", - "Dot", "FieldAcces", "MetadataAccess", "LeftParen", - "RightParen", "Equal", "NotEqual", "GreaterThan", - "GreaterEqual", "LessThan", "LessEqual", "LNot", - "Colon", "Semicolon", "Conjunction", "Disjunction", - "Implication", "Slash", "Percent", "Shr", - "Shl", "Mul", "Comment", "Unknown", - "EndString", "End", + static const char* const NAMES[]{ + "Priority", "Text", "True", "False", "LineStatementClose", + "Id", "Number", "Minus", "Plus", "Dot", + "FieldAcces", "MetadataAccess", "LeftParen", "RightParen", "Equal", + "NotEqual", "GreaterThan", "GreaterEqual", "LessThan", "LessEqual", + "LNot", "Colon", "Semicolon", "Conjunction", "Disjunction", + "Implication", "Slash", "Percent", "Shr", "Shl", + "Mul", "Comment", "Unknown", "EndString", "End", }; - return os << names[static_cast(kind)]; + return os << NAMES[static_cast(kind)]; } /// The function combines IR expressions separated by the "or" ,"and" operators @@ -80,12 +78,14 @@ std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { /// equal to !IR::Expression || (IR::Expression && IR::Expression) const IR::Expression* makeSingleExpr(std::vector input) { const IR::Expression* expr = nullptr; - for (long unsigned int i = 0; i < input.size(); i++) { - if (auto lOr = input[i]->to()) { + for (uint64_t i = 0; i < input.size(); i++) { + if (const auto* lOr = input[i]->to()) { if (lOr->right->toString() == "(tmp") { - if (i + 1 == input.size()) break; + if (i + 1 == input.size()) { + break; + } std::vector tmp; - long unsigned int idx = i; + uint64_t idx = i; i++; if (i + 1 == input.size()) { expr = new IR::LOr(input[idx - 1], input[i]); @@ -95,25 +95,33 @@ const IR::Expression* makeSingleExpr(std::vector input) { tmp.push_back(input[i]); i++; } - if (expr == nullptr) + if (expr == nullptr) { expr = new IR::LOr(input[idx - 1], makeSingleExpr(tmp)); - else + } else { expr = new IR::LOr(expr, makeSingleExpr(tmp)); + } break; - } else { - if (i + 1 == input.size()) break; - if (expr == nullptr) + } + { + if (i + 1 == input.size()) { + break; + } + if (expr == nullptr) { expr = new IR::LOr(input[i - 1], input[i + 1]); - else + } else { expr = new IR::LOr(expr, input[i + 1]); + } } } if (input[i]->is()) { - if (i + 1 == input.size()) break; - if (expr == nullptr) + if (i + 1 == input.size()) { + break; + } + if (expr == nullptr) { expr = new IR::LAnd(input[i - 1], input[i + 1]); - else + } else { expr = new IR::LAnd(expr, input[i + 1]); + } } } @@ -121,130 +129,134 @@ const IR::Expression* makeSingleExpr(std::vector input) { } /// Determines the token type according to the table key and generates a zombie constant for it. -const IR::Expression* makeConstant(Token input, IR::Vector keyElements) { +const IR::Expression* makeConstant(Token input, const IR::Vector& keyElements, + const IR::Type* leftType) { const IR::Type_Base* type = nullptr; const IR::Expression* result = nullptr; - std::string str = static_cast(input.lexeme()); + auto inputStr = input.lexeme(); if (input.is(Token::Kind::Text)) { - for (auto key : keyElements) { - cstring annotationName = ""; - for (auto annotation : key->annotations->annotations) { - if (annotation->name.name == "name") { - if (annotation->body.size() > 0) annotationName = annotation->body[0]->text; + for (const auto* key : keyElements) { + cstring annotationName; + if (const auto* annotation = key->getAnnotation("name")) { + if (!annotation->body.empty()) { + annotationName = annotation->body[0]->text; } } - if (str.find(key->expression->toString()) != std::string::npos || - (annotationName.size() > 0 && str.find(annotationName) != std::string::npos)) { - if (auto bit = key->expression->type->to()) { - type = bit; - } else if (auto varbit = key->expression->type->to()) { - type = varbit; - } else if (key->expression->type->to()) { - type = IR::Type_Bits::get(32); - } else { - type = IR::Type_Bits::get(1); - } - result = IRUtils::getZombieConst(type, 0, str); - break; + BUG_CHECK(annotationName != "", "Key does not have a name annotation."); + auto annoSize = annotationName.size(); + auto tokenLength = inputStr.length(); + if (inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { + continue; } + const auto* keyType = key->expression->type; + if (const auto* bit = keyType->to()) { + type = bit; + } else if (const auto* varbit = keyType->to()) { + type = varbit; + } else if (keyType->is()) { + type = IR::Type_Bits::get(1); + } else { + BUG("Unexpected key type %s.", type->node_type_name()); + } + return IRUtils::getZombieConst(type, 0, std::string(inputStr)); } - if (!result) { - type = IR::Type_Bits::get(8); - result = IRUtils::getZombieConst(type, 0, str); - } - - } else if (input.is(Token::Kind::Number)) { - if (!type) { - type = IR::Type_Bits::get(8); - } - result = IRUtils::getConstant(type, static_cast(str)); } - - return result; + if (input.is(Token::Kind::Number)) { + if (leftType == nullptr) + return IRUtils::getConstant(IR::Type_Bits::get(32), static_cast(inputStr)); + else + return IRUtils::getConstant(leftType, static_cast(inputStr)); + } + // TODO: Is this the right solution for priorities? + if (input.is(Token::Kind::Priority)) { + return IRUtils::getZombieConst(IR::Type_Bits::get(32), 0, std::string(inputStr)); + } + BUG_CHECK(result != nullptr, + "Could not match restriction key label %s was not found in key list.", + std::string(inputStr)); + return nullptr; } /// Converts a vector of tokens into a single IR:Expression /// 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, IR::Vector keyElements) { +const IR::Expression* getIR(std::vector tokens, + const IR::Vector& keyElements) { const IR::Expression* expr = nullptr; std::vector exprVec; - for (int i = 0; i < (int)tokens.size(); i++) { - if (tokens[i].is_one_of( + for (int i = 0; i < static_cast(tokens.size()); i++) { + auto token = tokens.at(i); + if (token.is_one_of( Token::Kind::Minus, Token::Kind::Plus, Token::Kind::Equal, Token::Kind::NotEqual, Token::Kind::GreaterThan, Token::Kind::GreaterEqual, Token::Kind::LessThan, Token::Kind::LessEqual, Token::Kind::Slash, Token::Kind::Percent, Token::Kind::Shr, Token::Kind::Shl, Token::Kind::Mul, Token::Kind::NotEqual)) { const IR::Expression* leftL = nullptr; const IR::Expression* rightL = nullptr; - if (i != 0) { - i--; - i--; - } - if (i <= 0 || tokens[i].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, - Token::Kind::LeftParen, Token::Kind::Implication)) { - i++; - leftL = makeConstant(tokens[i], keyElements); - } else { - leftL = exprVec[exprVec.size() - 1]; - exprVec.pop_back(); - i++; - } - i++; - i++; - i++; - if (i == (int)tokens.size() || - tokens[i].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, - Token::Kind::RightParen, Token::Kind::Implication)) { - i--; - rightL = makeConstant(tokens[i], keyElements); - if (auto constant = leftL->to()) { - auto clone = constant->clone(); + leftL = makeConstant(tokens[i - 1], keyElements, nullptr); + if (tokens[i + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { + rightL = makeConstant(tokens[i + 1], keyElements, leftL->type); + if (const auto* constant = leftL->to()) { + auto* clone = constant->clone(); clone->type = rightL->type; leftL = clone; } } else { - i--; - int idx = i; + int idx = i + 1; int endIdx = 0; bool flag = true; while (flag) { - i++; - if (i == (int)tokens.size() || - tokens[i].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, - Token::Kind::RightParen)) { - endIdx = i; + if (idx == (int)tokens.size() || + tokens[idx].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, + Token::Kind::RightParen)) { + endIdx = idx; flag = false; - i = idx; } + idx++; } + std::vector rightTokens; - for (int j = idx; j < endIdx + 1; j++) { + for (int j = i + 1; j < endIdx; j++) { rightTokens.push_back(tokens[j]); } rightL = getIR(rightTokens, keyElements); + i = idx; } - i--; + if (tokens[i].is(Token::Kind::Minus)) expr = new IR::Sub(leftL, rightL); + if (tokens[i].is(Token::Kind::Plus)) expr = new IR::Add(leftL, rightL); + if (tokens[i].is(Token::Kind::Equal)) expr = new IR::Equ(leftL, rightL); + if (tokens[i].is(Token::Kind::NotEqual)) expr = new IR::Neq(leftL, rightL); + if (tokens[i].is(Token::Kind::GreaterThan)) expr = new IR::Grt(leftL, rightL); + if (tokens[i].is(Token::Kind::GreaterEqual)) expr = new IR::Geq(leftL, rightL); + if (tokens[i].is(Token::Kind::LessThan)) expr = new IR::Lss(leftL, rightL); + if (tokens[i].is(Token::Kind::LessEqual)) expr = new IR::Leq(leftL, rightL); + if (tokens[i].is(Token::Kind::Slash)) expr = new IR::Div(leftL, rightL); + if (tokens[i].is(Token::Kind::Percent)) expr = new IR::Mod(leftL, rightL); + if (tokens[i].is(Token::Kind::Shr)) expr = new IR::Shr(leftL, rightL); + if (tokens[i].is(Token::Kind::Shl)) expr = new IR::Shl(leftL, rightL); + if (tokens[i].is(Token::Kind::Mul)) expr = new IR::Mul(leftL, rightL); + if (tokens[i].is(Token::Kind::NotEqual)) expr = new IR::Neq(leftL, rightL); + exprVec.push_back(expr); - } else if (tokens[i].is(Token::Kind::LNot)) { + } else if (token.is(Token::Kind::LNot)) { auto flag = true; int idx = i; cstring str = ""; @@ -254,11 +266,12 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector(tokens[i].lexeme()); + str += std::string(tokens[i].lexeme()); } else { flag = false; } @@ -288,17 +301,17 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector tmp; - for (long unsigned int i = 0; i < exprVec.size(); i++) { - if (auto lNot = exprVec[i]->to()) { + for (uint64_t i = 0; i < exprVec.size(); i++) { + if (const auto* lNot = exprVec[i]->to()) { i++; auto lNotStr = lNot->expr->toString(); - auto binary = exprVec[i]->checkedTo()->clone(); - if (auto subBin = binary->left->to()) { + auto* binary = exprVec[i]->checkedTo()->clone(); + if (const auto* subBin = binary->left->to()) { cstring str = subBin->getStringOp(); str.replace(" ", ""); - if (lNotStr.find(str)) { + if (lNotStr.find(str) != nullptr) { binary->left = new IR::LNot(binary->left); tmp.push_back(binary); continue; @@ -307,9 +320,8 @@ const IR::Expression* getIR(std::vector tokens, IR::Vector tokens, IR::Vector combineTokensToNames(std::vector input) { +std::vector combineTokensToNames(const std::vector& inputVector) { std::vector result; Token prevToken = Token(Token::Kind::Unknown, " ", 1); cstring txt = ""; - for (long unsigned int i = 0; i < input.size(); i++) { - if (prevToken.is(Token::Kind::Text) && input[i].is(Token::Kind::Number)) { - txt += static_cast(input[i].lexeme()); + for (const auto& input : inputVector) { + if (prevToken.is(Token::Kind::Text) && input.is(Token::Kind::Number)) { + txt += std::string(input.lexeme()); continue; } - if (input[i].is(Token::Kind::Text)) { - auto strtmp = static_cast(input[i].lexeme()); + if (input.is(Token::Kind::Text)) { + auto strtmp = std::string(input.lexeme()); if (strtmp == "." && prevToken.is(Token::Kind::Number)) { ::error( "Syntax error, unexpected INTEGER. P4 does not support floating point values. " @@ -342,18 +354,18 @@ std::vector combineTokensToNames(std::vector input) { } txt += strtmp; if (prevToken.is(Token::Kind::Number)) { - txt = static_cast(prevToken.lexeme()) + txt; + txt = std::string(prevToken.lexeme()) + txt; result.pop_back(); } } else { if (txt.size() > 0) { - result.push_back(Token(Token::Kind::Text, txt, txt.size())); + result.emplace_back(Token::Kind::Text, txt, txt.size()); txt = ""; } - result.push_back(input[i]); + result.push_back(input); } - prevToken = input[i]; + prevToken = input; } return result; } @@ -371,36 +383,36 @@ std::vector combineTokensToNames(std::vector input) { std::vector combineTokensToNumbers(std::vector input) { cstring numb = ""; std::vector result; - for (long unsigned int i = 0; i < input.size(); i++) { + for (uint64_t i = 0; i < input.size(); i++) { if (input[i].is(Token::Kind::Text)) { - auto str = static_cast(input[i].lexeme()); + auto str = std::string(input[i].lexeme()); if (str.rfind("0x", 0) == 0 || str.rfind("0X", 0) == 0) { cstring cstr = str; - result.push_back(Token(Token::Kind::Number, cstr, cstr.size())); + result.emplace_back(Token::Kind::Number, cstr, cstr.size()); continue; } if (str == "true") { - result.push_back(Token(Token::Kind::Number, "1", 1)); + result.emplace_back(Token::Kind::Number, "1", 1); continue; } if (str == "false") { - result.push_back(Token(Token::Kind::Number, "0", 1)); + result.emplace_back(Token::Kind::Number, "0", 1); continue; } } if (input[i].is(Token::Kind::Number)) { - numb += static_cast(input[i].lexeme()); + numb += std::string(input[i].lexeme()); if (i + 1 == input.size()) { - result.push_back(Token(Token::Kind::Number, numb, numb.size())); + result.emplace_back(Token::Kind::Number, numb, numb.size()); numb = ""; continue; } } else { if (numb.size() > 0) { - result.push_back(Token(Token::Kind::Number, numb, numb.size())); + result.emplace_back(Token::Kind::Number, numb, numb.size()); numb = ""; } result.push_back(input[i]); @@ -419,50 +431,49 @@ std::vector combineTokensToNumbers(std::vector input) { /// 0(Number)] -> [tableName_key_Name01(Text), ==(Equal) , 0(Number)] std::vector combineTokensToTableKeys(std::vector input, cstring tableName) { std::vector result; - for (long unsigned int i = 0; i < input.size(); i++) { - if (input[i].is(Token::Kind::Text)) { - auto str = static_cast(input[i].lexeme()); + for (uint64_t i = 0; i < input.size(); i++) { + if (!input[i].is(Token::Kind::Text)) { + result.push_back(input[i]); + continue; + } + auto str = std::string(input[i].lexeme()); - auto substr = str.substr(0, str.find("::mask")); - if (substr != str) { - cstring cstr = tableName + "_mask_" + substr; - result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); - continue; - } - substr = str.substr(0, str.find("::prefix_length")); - if (substr != str) { - cstring cstr = tableName + "_lpm_prefix_" + substr; - result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); - continue; - } + auto substr = str.substr(0, str.find("::mask")); + if (substr != str) { + cstring cstr = tableName + "_mask_" + substr; + result.emplace_back(Token::Kind::Text, cstr, cstr.size()); + continue; + } + substr = str.substr(0, str.find("::prefix_length")); + if (substr != str) { + cstring cstr = tableName + "_lpm_prefix_" + substr; + result.emplace_back(Token::Kind::Text, cstr, cstr.size()); + continue; + } - substr = str.substr(0, str.find("::priority")); - if (substr != str) { - cstring cstr = tableName + "_priority"; - result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); - continue; - } + substr = str.substr(0, str.find("::priority")); + if (substr != str) { + cstring cstr = tableName + "_priority"; + result.emplace_back(Token::Kind::Priority, cstr, cstr.size()); + continue; + } - if (str.find("isValid") != std::string::npos) { - i++; - cstring cString = str + static_cast(input[i].lexeme()); - if (input[i + 1].is(Token::Kind::Text)) { - cString += static_cast(input[i + 1].lexeme()); - i++; - } - cString += static_cast(input[i + 1].lexeme()); + if (str.find("isValid") != std::string::npos) { + i++; + cstring cString = str + std::string(input[i].lexeme()); + if (input[i + 1].is(Token::Kind::Text)) { + cString += std::string(input[i + 1].lexeme()); i++; - cString = tableName + "_key_" + cString; - result.push_back(Token(Token::Kind::Text, cString, cString.size())); - continue; } - - cstring cstr = tableName + "_key_" + str; - result.push_back(Token(Token::Kind::Text, cstr, cstr.size())); + cString += std::string(input[i + 1].lexeme()); + i++; + cString = tableName + "_key_" + cString; + result.emplace_back(Token::Kind::Text, cString, cString.size()); continue; - } else { - result.push_back(input[i]); } + + cstring cstr = tableName + "_key_" + str; + result.emplace_back(Token::Kind::Text, cstr, cstr.size()); } return result; } @@ -470,20 +481,20 @@ std::vector combineTokensToTableKeys(std::vector input, cstring ta /// Removes comment lines from the input array. /// For example, at the input we have a vector of tokens: /// [//(Comment), CommentText(Text) , (EndString) , 28(Number), .....] -> [28(Number), .....] -std::vector removeComments(std::vector input) { +std::vector removeComments(const std::vector& input) { std::vector result; bool flag = true; - for (long unsigned int i = 0; i < input.size(); i++) { - if (input[i].is(Token::Kind::Comment)) { + for (const auto& i : input) { + if (i.is(Token::Kind::Comment)) { flag = false; continue; } - if (input[i].is(Token::Kind::EndString)) { + if (i.is(Token::Kind::EndString)) { flag = true; continue; } if (flag) { - result.push_back(input[i]); + result.push_back(i); } } return result; @@ -492,8 +503,9 @@ std::vector removeComments(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 str) { - Lexer lex(str); +std::vector AssertsParser::genIRStructs( + cstring tableName, cstring restrictionString, const IR::Vector& keyElements) { + Lexer lex(restrictionString); std::vector tmp; for (auto token = lex.next(); !token.is_one_of(Token::Kind::End, Token::Kind::Unknown); token = lex.next()) { @@ -507,14 +519,14 @@ std::vector AssertsParser::genIRStructs(cstring str) { tmp = combineTokensToTableKeys(tmp, tableName); tmp = removeComments(tmp); std::vector tokens; - for (long unsigned int i = 0; i < tmp.size(); i++) { + for (uint64_t i = 0; i < tmp.size(); i++) { if (tmp[i].is(Token::Kind::Semicolon)) { - auto expr = getIR(tokens, keyElements); + const auto* expr = getIR(tokens, keyElements); result.push_back(expr); tokens.clear(); } else if (i == tmp.size() - 1) { tokens.push_back(tmp[i]); - auto expr = getIR(tokens, keyElements); + const auto* expr = getIR(tokens, keyElements); result.push_back(expr); tokens.clear(); } else { @@ -526,49 +538,51 @@ std::vector AssertsParser::genIRStructs(cstring str) { } const IR::Node* AssertsParser::postorder(IR::P4Table* node) { - tableName = node->controlPlaneName(); - if (node->getKey()) { - keyElements = node->getKey()->keyElements; - for (auto annotation : node->annotations->annotations) { - if (annotation->name.name == "entry_restriction") { - for (auto restrStr : annotation->body) { - auto restrictions = genIRStructs(restrStr->text); - /// 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 - Z3Solver solver; - if (solver.checkSat(restrictions) == true) { - restrictionsVec.push_back(restrictions); - } else { - auto cloneTable = node->clone(); - auto cloneProperties = node->properties->clone(); - IR::IndexedVector properties; - for (auto property : cloneProperties->properties) { - if (property->name.name != "key" || property->name.name != "entries") - properties.push_back(property); - } - cloneProperties->properties = properties; - cloneTable->properties = cloneProperties; - return cloneTable; - } - } + const auto* annotation = node->getAnnotation("entry_restriction"); + const auto* key = node->getKey(); + if (annotation == nullptr || key == nullptr) { + return node; + } + + for (const auto* restrStr : annotation->body) { + auto restrictions = + genIRStructs(node->controlPlaneName(), restrStr->text, key->keyElements); + /// 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 + Z3Solver solver; + if (solver.checkSat(restrictions) == true) { + restrictionsVec.push_back(restrictions); + continue; + } + auto* cloneTable = node->clone(); + auto* cloneProperties = node->properties->clone(); + IR::IndexedVector properties; + for (const auto* property : cloneProperties->properties) { + if (property->name.name != "key" || property->name.name != "entries") { + properties.push_back(property); } } + cloneProperties->properties = properties; + cloneTable->properties = cloneProperties; + return cloneTable; } return node; } -Token Lexer::atom(Token::Kind kind) noexcept { return Token(kind, m_beg++, 1); } +Token Lexer::atom(Token::Kind kind) noexcept { return {kind, m_beg++, 1}; } Token Lexer::next() noexcept { - while (is_space(peek())) get(); + while (isSpace(peek())) { + get(); + } switch (peek()) { case '\0': - return Token(Token::Kind::End, m_beg, 1); + return {Token::Kind::End, m_beg, 1}; case '\n': get(); - return Token(Token::Kind::EndString, m_beg, 1); + return {Token::Kind::EndString, m_beg, 1}; default: return atom(Token::Kind::Text); case '0': @@ -590,7 +604,7 @@ Token Lexer::next() noexcept { get(); if (get() == '=') { get(); - return Token(Token::Kind::Equal, "==", 2); + return {Token::Kind::Equal, "==", 2}; } prev(); return atom(Token::Kind::Unknown); @@ -598,7 +612,7 @@ Token Lexer::next() noexcept { get(); if (get() == '=') { get(); - return Token(Token::Kind::NotEqual, "!=", 2); + return {Token::Kind::NotEqual, "!=", 2}; } prev(); return atom(Token::Kind::LNot); @@ -606,7 +620,7 @@ Token Lexer::next() noexcept { get(); if (get() == '>') { get(); - return Token(Token::Kind::Implication, "->", 2); + return {Token::Kind::Implication, "->", 2}; } prev(); return atom(Token::Kind::Minus); @@ -614,11 +628,11 @@ Token Lexer::next() noexcept { get(); if (get() == '=') { get(); - return Token(Token::Kind::LessEqual, "<=", 2); + return {Token::Kind::LessEqual, "<=", 2}; } prev(); if (get() == '<') { - return Token(Token::Kind::Shl, "<<", 2); + return {Token::Kind::Shl, "<<", 2}; } prev(); return atom(Token::Kind::LessThan); @@ -626,11 +640,11 @@ Token Lexer::next() noexcept { get(); if (get() == '=') { get(); - return Token(Token::Kind::GreaterEqual, ">=", 2); + return {Token::Kind::GreaterEqual, ">=", 2}; } prev(); if (get() == '>') { - return Token(Token::Kind::Shr, ">>", 2); + return {Token::Kind::Shr, ">>", 2}; } prev(); return atom(Token::Kind::GreaterThan); @@ -640,7 +654,7 @@ Token Lexer::next() noexcept { get(); if (get() == '&') { get(); - return Token(Token::Kind::Conjunction, "&&", 2); + return {Token::Kind::Conjunction, "&&", 2}; } prev(); return atom(Token::Kind::Text); @@ -648,7 +662,7 @@ Token Lexer::next() noexcept { get(); if (get() == '|') { get(); - return Token(Token::Kind::Disjunction, "||", 2); + return {Token::Kind::Disjunction, "||", 2}; } prev(); return atom(Token::Kind::Text); @@ -658,7 +672,7 @@ Token Lexer::next() noexcept { get(); if (get() == '/') { get(); - return Token(Token::Kind::Comment, "//", 2); + return {Token::Kind::Comment, "//", 2}; } prev(); return atom(Token::Kind::Slash); diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h index ef74fb80e56..416e33fe3ae 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h @@ -15,8 +15,6 @@ namespace AssertsParser { class AssertsParser : public Transform { std::vector>& restrictionsVec; - IR::Vector keyElements; - cstring tableName; public: explicit AssertsParser(std::vector>& output); @@ -24,13 +22,16 @@ class AssertsParser : public Transform { /// 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 genIRStructs(cstring str); + static std::vector genIRStructs( + cstring tableName, cstring restrictionString, + const IR::Vector& keyElements); const IR::Node* postorder(IR::P4Table* node) override; }; class Token { public: enum class Kind { + Priority, Text, True, False, From fadae11daf1620e28bc2a6e803fc1dc1c0fe0e26 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Tue, 25 Oct 2022 17:12:04 +0300 Subject: [PATCH 11/25] Fix [no-jira] --- backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 3cf482b5000..22e9c3199c3 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -136,16 +136,16 @@ const IR::Expression* makeConstant(Token input, const IR::Vector auto inputStr = input.lexeme(); if (input.is(Token::Kind::Text)) { for (const auto* key : keyElements) { - cstring annotationName; + cstring annotationName = ""; if (const auto* annotation = key->getAnnotation("name")) { if (!annotation->body.empty()) { annotationName = annotation->body[0]->text; } } - BUG_CHECK(annotationName != "", "Key does not have a name annotation."); auto annoSize = annotationName.size(); auto tokenLength = inputStr.length(); - if (inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { + if (!inputStr.find(key->expression->toString()) || + inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { continue; } const auto* keyType = key->expression->type; From 7308f64e6c3fab4d459b37be95efaba46ca5d180 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 26 Oct 2022 10:00:54 +0300 Subject: [PATCH 12/25] Fix [no-jira] --- backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp | 6 +++--- backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake | 6 ++++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 22e9c3199c3..b691fdc1169 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -136,16 +136,16 @@ const IR::Expression* makeConstant(Token input, const IR::Vector auto inputStr = input.lexeme(); if (input.is(Token::Kind::Text)) { for (const auto* key : keyElements) { - cstring annotationName = ""; + cstring annotationName; if (const auto* annotation = key->getAnnotation("name")) { if (!annotation->body.empty()) { annotationName = annotation->body[0]->text; } } + BUG_CHECK(annotationName.size() > 0, "Key does not have a name annotation."); auto annoSize = annotationName.size(); auto tokenLength = inputStr.length(); - if (!inputStr.find(key->expression->toString()) || - inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { + if (inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { continue; } const auto* keyType = key->expression->type; diff --git a/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake b/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake index 9d615653c38..cb98559fa4d 100755 --- a/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake +++ b/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake @@ -111,6 +111,12 @@ p4tools_add_xfail_reason( bmv2_assert.p4 ) +p4tools_add_xfail_reason( + "testgen-p4c-bmv2" + "Key does not have a name annotation." + bmv2_restrictions.p4 +) + p4tools_add_xfail_reason( "testgen-p4c-bmv2" "simple_switch died with return code -6" From 77e2758a932a88922dad26d303b28c2b0fdcb7a2 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 26 Oct 2022 10:02:22 +0300 Subject: [PATCH 13/25] Fix Xfails [no-jira] --- .../p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake | 6 ++++++ .../testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake b/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake index ae460b374ec..d4ae5444717 100644 --- a/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake +++ b/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake @@ -15,3 +15,9 @@ p4tools_add_xfail_reason( # Assert/Assume error: assert/assume(false). bmv2_assert.p4 ) + +p4tools_add_xfail_reason( + "testgen-p4c-bmv2-ptf" + "Key does not have a name annotation." + bmv2_restrictions.p4 +) diff --git a/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake b/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake index bef0c2780e2..1c57e548023 100644 --- a/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake +++ b/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake @@ -70,6 +70,12 @@ p4tools_add_xfail_reason( bmv2_assert.p4 ) +p4tools_add_xfail_reason( + "testgen-p4c-bmv2-protobuf" + "Key does not have a name annotation." + bmv2_restrictions.p4 +) + p4tools_add_xfail_reason( "testgen-p4c-bmv2-protobuf" "Computations are not supported in update_checksum" From 550c55d857f094b566cbc40dc0336d99ab841459 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 26 Oct 2022 11:36:06 +0300 Subject: [PATCH 14/25] Fix processing of LNot [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 79 +++++++------------ 1 file changed, 30 insertions(+), 49 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index b691fdc1169..414593091a2 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -226,6 +226,10 @@ const IR::Expression* getIR(std::vector tokens, i = idx; } + if (i - 2 > 0 && tokens[i - 2].is(Token::Kind::LNot)) { + leftL = new IR::LNot(leftL); + } + if (tokens[i].is(Token::Kind::Minus)) expr = new IR::Sub(leftL, rightL); if (tokens[i].is(Token::Kind::Plus)) expr = new IR::Add(leftL, rightL); @@ -257,37 +261,35 @@ const IR::Expression* getIR(std::vector tokens, exprVec.push_back(expr); } else if (token.is(Token::Kind::LNot)) { - auto flag = true; - int idx = i; - cstring str = ""; - auto first = true; - while (flag) { - i++; - if (tokens[i].is(Token::Kind::LeftParen)) { - first = false; - continue; - } - if (first) { - break; + if (!tokens[i + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { + const IR::Expression* exprLNot = nullptr; + int idx = i + 1; + int endIdx = 0; + bool flag = true; + while (flag) { + if (idx == (int)tokens.size() || + tokens[idx].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, + Token::Kind::RightParen)) { + endIdx = idx; + flag = false; + } + idx++; } - if (tokens[i].is_not(Token::Kind::RightParen)) { - str += std::string(tokens[i].lexeme()); - } else { - flag = false; + + std::vector lNotTokens; + for (int j = i + 1; j < endIdx; j++) { + lNotTokens.push_back(tokens[j]); } + + exprLNot = getIR(lNotTokens, keyElements); + i = idx; + exprVec.push_back(new IR::LNot(exprLNot)); } - i = idx; - if (str.size() == 0) { - str = "tmp"; - } - const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID(str))); - exprVec.push_back(new IR::LNot(expr1)); } else if (tokens[i].is(Token::Kind::Implication)) { auto tmp = exprVec[exprVec.size() - 1]; exprVec.pop_back(); const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); - exprVec.push_back(new IR::LNot(expr1)); - exprVec.push_back(tmp); + exprVec.push_back(new IR::LNot(tmp)); const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("(tmp"))); exprVec.push_back(new IR::LOr(expr1, expr2)); } else if (tokens[i].is(Token::Kind::Disjunction)) { @@ -300,34 +302,12 @@ const IR::Expression* getIR(std::vector tokens, exprVec.push_back(new IR::LAnd(expr1, expr2)); } } - std::vector tmp; - for (uint64_t i = 0; i < exprVec.size(); i++) { - if (const auto* lNot = exprVec[i]->to()) { - i++; - auto lNotStr = lNot->expr->toString(); - - auto* binary = exprVec[i]->checkedTo()->clone(); - if (const auto* subBin = binary->left->to()) { - cstring str = subBin->getStringOp(); - str.replace(" ", ""); - if (lNotStr.find(str) != nullptr) { - binary->left = new IR::LNot(binary->left); - tmp.push_back(binary); - continue; - } - } - - tmp.push_back(new IR::LNot(exprVec[i])); - continue; - } - tmp.push_back(exprVec[i]); - } - if (tmp.size() == 1) { - return expr; + if (exprVec.size() == 1) { + return exprVec[0]; } - expr = makeSingleExpr(tmp); + expr = makeSingleExpr(exprVec); return expr; } @@ -615,6 +595,7 @@ Token Lexer::next() noexcept { return {Token::Kind::NotEqual, "!=", 2}; } prev(); + prev(); return atom(Token::Kind::LNot); case '-': get(); From 8f952a5b8a7face9ae15bff26d7a58f9cff10c13 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 26 Oct 2022 14:47:57 +0300 Subject: [PATCH 15/25] Moving code into a function [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 71 ++++++++----------- 1 file changed, 30 insertions(+), 41 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 414593091a2..a0c9c69bd68 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -177,6 +177,30 @@ const IR::Expression* makeConstant(Token input, const IR::Vector return nullptr; } +/// Determines the right side of the expression starting from the original position and returns a +/// slice of tokens related to the right side and the index of the end of the right side. +/// Returning the end index is necessary so that after moving from the end of the right side +std::pair, int> findRightPart(std::vector tokens, int index) { + int idx = index + 1; + int endIdx = 0; + bool flag = true; + while (flag) { + if (idx == (int)tokens.size() || + tokens[idx].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, + Token::Kind::RightParen)) { + endIdx = idx; + flag = false; + } + idx++; + } + + std::vector rightTokens; + for (int j = index + 1; j < endIdx; j++) { + rightTokens.push_back(tokens[j]); + } + return std::make_pair(rightTokens, idx); +} + /// Converts a vector of tokens into a single IR:Expression /// For example, at the input we have a vector of tokens: /// [key1(Text), ->(Implication), key2(Text), &&(Conjunction), key3(Text)] The result will be an @@ -204,26 +228,9 @@ const IR::Expression* getIR(std::vector tokens, leftL = clone; } } else { - int idx = i + 1; - int endIdx = 0; - bool flag = true; - while (flag) { - if (idx == (int)tokens.size() || - tokens[idx].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, - Token::Kind::RightParen)) { - endIdx = idx; - flag = false; - } - idx++; - } - - std::vector rightTokens; - for (int j = i + 1; j < endIdx; j++) { - rightTokens.push_back(tokens[j]); - } - - rightL = getIR(rightTokens, keyElements); - i = idx; + auto rightPart = findRightPart(tokens, i); + rightL = getIR(rightPart.first, keyElements); + i = rightPart.second; } if (i - 2 > 0 && tokens[i - 2].is(Token::Kind::LNot)) { @@ -262,27 +269,9 @@ const IR::Expression* getIR(std::vector tokens, } else if (token.is(Token::Kind::LNot)) { if (!tokens[i + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { - const IR::Expression* exprLNot = nullptr; - int idx = i + 1; - int endIdx = 0; - bool flag = true; - while (flag) { - if (idx == (int)tokens.size() || - tokens[idx].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, - Token::Kind::RightParen)) { - endIdx = idx; - flag = false; - } - idx++; - } - - std::vector lNotTokens; - for (int j = i + 1; j < endIdx; j++) { - lNotTokens.push_back(tokens[j]); - } - - exprLNot = getIR(lNotTokens, keyElements); - i = idx; + auto rightPart = findRightPart(tokens, i); + const IR::Expression* exprLNot = getIR(rightPart.first, keyElements); + i = rightPart.second; exprVec.push_back(new IR::LNot(exprLNot)); } } else if (tokens[i].is(Token::Kind::Implication)) { From cbc7f487f78e34a02313a79105f77ee93ebd5869 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 26 Oct 2022 17:09:30 +0300 Subject: [PATCH 16/25] Fix [no-jira] --- backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index a0c9c69bd68..31c52e75e77 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -140,9 +140,15 @@ const IR::Expression* makeConstant(Token input, const IR::Vector if (const auto* annotation = key->getAnnotation("name")) { if (!annotation->body.empty()) { annotationName = annotation->body[0]->text; + } else if (!annotation->expr.empty()) { + annotationName = annotation->expr[0]->toString(); } } BUG_CHECK(annotationName.size() > 0, "Key does not have a name annotation."); + cstring separator = "\""; + if (annotationName.startsWith(separator) && annotationName.endsWith(separator)) { + annotationName = annotationName.substr(1, annotationName.size() - 2); + } auto annoSize = annotationName.size(); auto tokenLength = inputStr.length(); if (inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { From 73d7a9a2d347a4d3fda93aa066445687c1f3ec81 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 26 Oct 2022 17:10:42 +0300 Subject: [PATCH 17/25] Fix Xfails [no-jira] --- .../p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake | 6 ------ .../testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake | 6 ------ backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake | 6 ------ 3 files changed, 18 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake b/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake index d4ae5444717..ae460b374ec 100644 --- a/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake +++ b/backends/p4tools/testgen/targets/bmv2/test/BMV2PTFXfail.cmake @@ -15,9 +15,3 @@ p4tools_add_xfail_reason( # Assert/Assume error: assert/assume(false). bmv2_assert.p4 ) - -p4tools_add_xfail_reason( - "testgen-p4c-bmv2-ptf" - "Key does not have a name annotation." - bmv2_restrictions.p4 -) diff --git a/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake b/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake index 1c57e548023..bef0c2780e2 100644 --- a/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake +++ b/backends/p4tools/testgen/targets/bmv2/test/BMV2ProtobufXfail.cmake @@ -70,12 +70,6 @@ p4tools_add_xfail_reason( bmv2_assert.p4 ) -p4tools_add_xfail_reason( - "testgen-p4c-bmv2-protobuf" - "Key does not have a name annotation." - bmv2_restrictions.p4 -) - p4tools_add_xfail_reason( "testgen-p4c-bmv2-protobuf" "Computations are not supported in update_checksum" diff --git a/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake b/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake index cb98559fa4d..9d615653c38 100755 --- a/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake +++ b/backends/p4tools/testgen/targets/bmv2/test/BMV2Xfail.cmake @@ -111,12 +111,6 @@ p4tools_add_xfail_reason( bmv2_assert.p4 ) -p4tools_add_xfail_reason( - "testgen-p4c-bmv2" - "Key does not have a name annotation." - bmv2_restrictions.p4 -) - p4tools_add_xfail_reason( "testgen-p4c-bmv2" "simple_switch died with return code -6" From 31e50b73e1162954c775a729ff0b011c26b7b68a Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Fri, 28 Oct 2022 11:44:05 +0300 Subject: [PATCH 18/25] Add patch [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 211 ++++++++++-------- .../targets/bmv2/p4_refers_to_parser.cpp | 52 ++--- .../targets/bmv2/p4_refers_to_parser.h | 12 +- .../test/p4-programs/bmv2_restrictions.p4 | 94 -------- .../test/p4-programs/bmv2_restrictions_2.p4 | 6 +- .../small-step/p4_asserts_parser_test.cpp | 57 +++-- 6 files changed, 190 insertions(+), 242 deletions(-) delete mode 100755 backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 31c52e75e77..e0f358ca062 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -11,6 +11,16 @@ namespace P4Tools { namespace AssertsParser { +static std::vector NAMES{ + "Priority", "Text", "True", "False", "LineStatementClose", + "Id", "Number", "Minus", "Plus", "Dot", + "FieldAcces", "MetadataAccess", "LeftParen", "RightParen", "Equal", + "NotEqual", "GreaterThan", "GreaterEqual", "LessThan", "LessEqual", + "LNot", "Colon", "Semicolon", "Conjunction", "Disjunction", + "Implication", "Slash", "Percent", "Shr", "Shl", + "Mul", "Comment", "Unknown", "EndString", "End", +}; + AssertsParser::AssertsParser(std::vector>& output) : restrictionsVec(output) { setName("Restrictions"); @@ -18,30 +28,39 @@ AssertsParser::AssertsParser(std::vector>& ou /// The function to get kind from token Token::Kind Token::kind() const noexcept { return m_kind; } + /// The function to replace the token kind with another kind void Token::kind(Token::Kind kind) noexcept { m_kind = kind; } + /// Kind comparison function. Allows you to compare token kind with the specified kind and return /// bool values, replacement for == bool Token::is(Token::Kind kind) const noexcept { return m_kind == kind; } + /// Kind comparison function. Allows you to compare token kind with the specified kind and return /// bool values, replacement for != bool Token::is_not(Token::Kind kind) const noexcept { return m_kind != kind; } + /// Functions for multiple comparison kind bool Token::is_one_of(Token::Kind k1, Token::Kind k2) const noexcept { return is(k1) || is(k2); } + template bool Token::is_one_of(Token::Kind k1, Token::Kind k2, Ts... ks) const noexcept { return is(k1) || is_one_of(k2, ks...); } + /// The function to get lexeme from token std::string_view Token::lexeme() const noexcept { return m_lexeme; } + /// The function to replace the token lexeme with another lexeme void Token::lexeme(std::string_view lexeme) noexcept { m_lexeme = lexeme; } /// Function to get the current character char Lexer::peek() const noexcept { return *m_beg; } + /// The function advances the iterator one index back and returns the character corresponding to the /// position of the iterator char Lexer::prev() noexcept { return *m_beg--; } + /// The function advances the iterator one index forward and returns the character corresponding to /// the position of the iterator char Lexer::get() noexcept { return *m_beg++; } @@ -58,16 +77,7 @@ bool isSpace(char c) noexcept { } std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { - static const char* const NAMES[]{ - "Priority", "Text", "True", "False", "LineStatementClose", - "Id", "Number", "Minus", "Plus", "Dot", - "FieldAcces", "MetadataAccess", "LeftParen", "RightParen", "Equal", - "NotEqual", "GreaterThan", "GreaterEqual", "LessThan", "LessEqual", - "LNot", "Colon", "Semicolon", "Conjunction", "Disjunction", - "Implication", "Slash", "Percent", "Shr", "Shl", - "Mul", "Comment", "Unknown", "EndString", "End", - }; - return os << NAMES[static_cast(kind)]; + return os << NAMES.at(static_cast(kind)); } /// The function combines IR expressions separated by the "or" ,"and" operators @@ -78,49 +88,49 @@ std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { /// equal to !IR::Expression || (IR::Expression && IR::Expression) const IR::Expression* makeSingleExpr(std::vector input) { const IR::Expression* expr = nullptr; - for (uint64_t i = 0; i < input.size(); i++) { - if (const auto* lOr = input[i]->to()) { + for (uint64_t idx = 0; idx < input.size(); idx++) { + if (const auto* lOr = input[idx]->to()) { if (lOr->right->toString() == "(tmp") { - if (i + 1 == input.size()) { + if (idx + 1 == input.size()) { break; } std::vector tmp; - uint64_t idx = i; - i++; - if (i + 1 == input.size()) { - expr = new IR::LOr(input[idx - 1], input[i]); + uint64_t jdx = idx; + idx++; + if (idx + 1 == input.size()) { + expr = new IR::LOr(input[jdx - 1], input[idx]); break; } - while (i < input.size()) { - tmp.push_back(input[i]); - i++; + while (idx < input.size()) { + tmp.push_back(input[idx]); + idx++; } if (expr == nullptr) { - expr = new IR::LOr(input[idx - 1], makeSingleExpr(tmp)); + expr = new IR::LOr(input[jdx - 1], makeSingleExpr(tmp)); } else { expr = new IR::LOr(expr, makeSingleExpr(tmp)); } break; } { - if (i + 1 == input.size()) { + if (idx + 1 == input.size()) { break; } if (expr == nullptr) { - expr = new IR::LOr(input[i - 1], input[i + 1]); + expr = new IR::LOr(input[idx - 1], input[idx + 1]); } else { - expr = new IR::LOr(expr, input[i + 1]); + expr = new IR::LOr(expr, input[idx + 1]); } } } - if (input[i]->is()) { - if (i + 1 == input.size()) { + if (input[idx]->is()) { + if (idx + 1 == input.size()) { break; } if (expr == nullptr) { - expr = new IR::LAnd(input[i - 1], input[i + 1]); + expr = new IR::LAnd(input[idx - 1], input[idx + 1]); } else { - expr = new IR::LAnd(expr, input[i + 1]); + expr = new IR::LAnd(expr, input[idx + 1]); } } } @@ -162,16 +172,16 @@ const IR::Expression* makeConstant(Token input, const IR::Vector } else if (keyType->is()) { type = IR::Type_Bits::get(1); } else { - BUG("Unexpected key type %s.", type->node_type_name()); + BUG("Unexpected key type %s.", keyType->node_type_name()); } return IRUtils::getZombieConst(type, 0, std::string(inputStr)); } } if (input.is(Token::Kind::Number)) { - if (leftType == nullptr) + if (leftType == nullptr) { return IRUtils::getConstant(IR::Type_Bits::get(32), static_cast(inputStr)); - else - return IRUtils::getConstant(leftType, static_cast(inputStr)); + } + return IRUtils::getConstant(leftType, static_cast(inputStr)); } // TODO: Is this the right solution for priorities? if (input.is(Token::Kind::Priority)) { @@ -186,12 +196,12 @@ const IR::Expression* makeConstant(Token input, const IR::Vector /// Determines the right side of the expression starting from the original position and returns a /// slice of tokens related to the right side and the index of the end of the right side. /// Returning the end index is necessary so that after moving from the end of the right side -std::pair, int> findRightPart(std::vector tokens, int index) { - int idx = index + 1; +std::pair, size_t> findRightPart(std::vector tokens, size_t index) { + size_t idx = index + 1; int endIdx = 0; bool flag = true; while (flag) { - if (idx == (int)tokens.size() || + if (idx == tokens.size() || tokens[idx].is_one_of(Token::Kind::Conjunction, Token::Kind::Disjunction, Token::Kind::RightParen)) { endIdx = idx; @@ -207,17 +217,64 @@ std::pair, int> findRightPart(std::vector tokens, int return std::make_pair(rightTokens, idx); } +/// Chose a binary expression that correlates to the token kind. +const IR::Expression* pickBinaryExpr(const Token& token, const IR::Expression* leftL, + const IR::Expression* rightL) { + if (token.is(Token::Kind::Minus)) { + return new IR::Sub(leftL, rightL); + } + if (token.is(Token::Kind::Plus)) { + return new IR::Add(leftL, rightL); + } + if (token.is(Token::Kind::Equal)) { + return new IR::Equ(leftL, rightL); + } + if (token.is(Token::Kind::NotEqual)) { + return new IR::Neq(leftL, rightL); + } + if (token.is(Token::Kind::GreaterThan)) { + return new IR::Grt(leftL, rightL); + } + if (token.is(Token::Kind::GreaterEqual)) { + return new IR::Geq(leftL, rightL); + } + if (token.is(Token::Kind::LessThan)) { + return new IR::Lss(leftL, rightL); + } + if (token.is(Token::Kind::LessEqual)) { + return new IR::Leq(leftL, rightL); + } + if (token.is(Token::Kind::Slash)) { + return new IR::Div(leftL, rightL); + } + if (token.is(Token::Kind::Percent)) { + return new IR::Mod(leftL, rightL); + } + if (token.is(Token::Kind::Shr)) { + return new IR::Shr(leftL, rightL); + } + if (token.is(Token::Kind::Shl)) { + return new IR::Shl(leftL, rightL); + } + if (token.is(Token::Kind::Mul)) { + return new IR::Mul(leftL, rightL); + } + if (token.is(Token::Kind::NotEqual)) { + return new IR::Neq(leftL, rightL); + } + BUG("Unsupported binary expression."); +} + /// Converts a vector of tokens into a single IR:Expression /// 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* expr = nullptr; std::vector exprVec; - for (int i = 0; i < static_cast(tokens.size()); i++) { - auto token = tokens.at(i); + for (size_t idx = 0; idx < tokens.size(); idx++) { + auto token = tokens.at(idx); if (token.is_one_of( Token::Kind::Minus, Token::Kind::Plus, Token::Kind::Equal, Token::Kind::NotEqual, Token::Kind::GreaterThan, Token::Kind::GreaterEqual, Token::Kind::LessThan, @@ -225,75 +282,45 @@ 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[i - 1], keyElements, nullptr); - if (tokens[i + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { - rightL = makeConstant(tokens[i + 1], keyElements, leftL->type); + leftL = makeConstant(tokens[idx - 1], keyElements, nullptr); + if (tokens[idx + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { + rightL = makeConstant(tokens[idx + 1], keyElements, leftL->type); if (const auto* constant = leftL->to()) { auto* clone = constant->clone(); clone->type = rightL->type; leftL = clone; } } else { - auto rightPart = findRightPart(tokens, i); + auto rightPart = findRightPart(tokens, idx); rightL = getIR(rightPart.first, keyElements); - i = rightPart.second; + idx = rightPart.second; } - if (i - 2 > 0 && tokens[i - 2].is(Token::Kind::LNot)) { + if (idx - 2 > 0 && tokens[idx - 2].is(Token::Kind::LNot)) { leftL = new IR::LNot(leftL); } - - if (tokens[i].is(Token::Kind::Minus)) expr = new IR::Sub(leftL, rightL); - - if (tokens[i].is(Token::Kind::Plus)) expr = new IR::Add(leftL, rightL); - - if (tokens[i].is(Token::Kind::Equal)) expr = new IR::Equ(leftL, rightL); - - if (tokens[i].is(Token::Kind::NotEqual)) expr = new IR::Neq(leftL, rightL); - - if (tokens[i].is(Token::Kind::GreaterThan)) expr = new IR::Grt(leftL, rightL); - - if (tokens[i].is(Token::Kind::GreaterEqual)) expr = new IR::Geq(leftL, rightL); - - if (tokens[i].is(Token::Kind::LessThan)) expr = new IR::Lss(leftL, rightL); - - if (tokens[i].is(Token::Kind::LessEqual)) expr = new IR::Leq(leftL, rightL); - - if (tokens[i].is(Token::Kind::Slash)) expr = new IR::Div(leftL, rightL); - - if (tokens[i].is(Token::Kind::Percent)) expr = new IR::Mod(leftL, rightL); - - if (tokens[i].is(Token::Kind::Shr)) expr = new IR::Shr(leftL, rightL); - - if (tokens[i].is(Token::Kind::Shl)) expr = new IR::Shl(leftL, rightL); - - if (tokens[i].is(Token::Kind::Mul)) expr = new IR::Mul(leftL, rightL); - - if (tokens[i].is(Token::Kind::NotEqual)) expr = new IR::Neq(leftL, rightL); - - exprVec.push_back(expr); - + exprVec.push_back(pickBinaryExpr(token, leftL, rightL)); } else if (token.is(Token::Kind::LNot)) { - if (!tokens[i + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { - auto rightPart = findRightPart(tokens, i); + if (!tokens[idx + 1].is_one_of(Token::Kind::Text, Token::Kind::Number)) { + auto rightPart = findRightPart(tokens, idx); const IR::Expression* exprLNot = getIR(rightPart.first, keyElements); - i = rightPart.second; + idx = rightPart.second; exprVec.push_back(new IR::LNot(exprLNot)); } - } else if (tokens[i].is(Token::Kind::Implication)) { - auto tmp = exprVec[exprVec.size() - 1]; + } else if (token.is(Token::Kind::Implication)) { + const auto* tmp = exprVec[exprVec.size() - 1]; exprVec.pop_back(); - const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path("tmp")); exprVec.push_back(new IR::LNot(tmp)); - const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("(tmp"))); + const IR::Expression* expr2 = new IR::PathExpression(new IR::Path("(tmp")); exprVec.push_back(new IR::LOr(expr1, expr2)); - } else if (tokens[i].is(Token::Kind::Disjunction)) { - const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); - const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + } else if (token.is(Token::Kind::Disjunction)) { + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path("tmp")); + const IR::Expression* expr2 = new IR::PathExpression(new IR::Path("tmp")); exprVec.push_back(new IR::LOr(expr1, expr2)); - } else if (tokens[i].is(Token::Kind::Conjunction)) { - const IR::Expression* expr1 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); - const IR::Expression* expr2 = new IR::PathExpression(new IR::Path(IR::ID("tmp"))); + } else if (token.is(Token::Kind::Conjunction)) { + const IR::Expression* expr1 = new IR::PathExpression(new IR::Path("tmp")); + const IR::Expression* expr2 = new IR::PathExpression(new IR::Path("tmp")); exprVec.push_back(new IR::LAnd(expr1, expr2)); } } @@ -302,9 +329,7 @@ const IR::Expression* getIR(std::vector tokens, return exprVec[0]; } - expr = makeSingleExpr(exprVec); - - return expr; + return makeSingleExpr(exprVec); } /// Combines successive tokens into variable names. /// Returns a vector with tokens combined into names. @@ -345,7 +370,7 @@ std::vector combineTokensToNames(const std::vector& inputVector) { return result; } -/// Combines successive tokens into numbers. For converting boolean or Hex, Octal values ​​to +/// Combines successive tokens into numbers. For converting boolean or Hex, Octal values to /// numbers we must first use combineTokensToNames. Returns a vector with tokens combined into /// numbers. For example, at the input we have a vector of tokens: [a(Text),c(Text),b(text), /// +(Plus), 1(Number),2(number)] The result will be [a(Text),c(Text),b(text), +(Plus), 12(number)] @@ -395,7 +420,7 @@ std::vector combineTokensToNumbers(std::vector input) { } return result; } -/// Convert access tokens or keys into table keys. For converting access tokens or keys ​​to +/// Convert access tokens or keys into table keys. For converting access tokens or keys to /// table keys we must first use combineTokensToNames. Returns a vector with tokens converted into /// table keys. /// For example, at the input we have a vector of tokens: diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp index dd212d8d061..aee3f97ccc1 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -19,12 +19,13 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c cstring destKeyName, cstring destTableName, const IR::Type* type) { cstring tmp = ""; - if (table) + if (table) { tmp = currentName + "_key_" + currentKeyName; - else + } else { tmp = currentName + currentKeyName; + } auto left = IRUtils::getZombieConst(type, 0, tmp); - std::string str = static_cast(currentName); + std::string str = currentName.c_str(); std::vector elems; std::stringstream ss(str); std::string item; @@ -32,12 +33,12 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c elems.push_back(item); } str = ""; - for (long unsigned int i = 0; i < elems.size() - 1; i++) { + for (uint64_t i = 0; i < elems.size() - 1; i++) { str += elems[i] + "."; } tmp = str + destTableName + "_key_" + destKeyName; auto right = IRUtils::getZombieConst(type, 0, tmp); - auto expr = new IR::Equ(left, right); + auto* expr = new IR::Equ(left, right); std::vector constraint; constraint.push_back(expr); restrictionsVec.push_back(constraint); @@ -46,15 +47,15 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c const IR::Node* RefersToParser::postorder(IR::Annotation* annotation) { const IR::P4Action* prevAction = nullptr; if (annotation->name.name == "refers_to") { - if (auto action = findOrigCtxt()) { + if (const auto* action = findOrigCtxt()) { if (prevAction != action) { actionVector.push_back(action); prevAction = action; } - } else if (auto keys = findOrigCtxt()) { - auto table = findOrigCtxt(); + } else if (const auto* keys = findOrigCtxt()) { + const auto* table = findOrigCtxt(); CHECK_NULL(table); - auto key = findOrigCtxt(); + const auto* key = findOrigCtxt(); CHECK_NULL(key); auto it = find(keys->keyElements.begin(), keys->keyElements.end(), key); if (it != keys->keyElements.end()) { @@ -67,10 +68,11 @@ const IR::Node* RefersToParser::postorder(IR::Annotation* annotation) { } return annotation; } + // Finds a P4Action in the actionVector according /// to the specified input argument which is an ActionListElement const IR::P4Action* RefersToParser::findAction(const IR::ActionListElement* input) { - for (auto element : actionVector) { + for (const auto* element : actionVector) { if (input->getName().name == element->name.name) { return element; } @@ -82,7 +84,7 @@ const IR::P4Action* RefersToParser::findAction(const IR::ActionListElement* inpu // The build starts at index 2 because 0 is the table name and 1 is ",". cstring buildName(IR::Vector input) { cstring result = ""; - for (long unsigned int i = 2; i < input.size(); i++) { + for (uint64_t i = 2; i < input.size(); i++) { result += input[i]->text; } return result; @@ -91,23 +93,23 @@ cstring buildName(IR::Vector input) { /// An intermediate function that determines the type for future variables and partially /// collects their names for them, after which it calls the createConstraint function, /// which completes the construction of the constraint -void RefersToParser::createRefersToConstraint(IR::Vector annotations, +void RefersToParser::createRefersToConstraint(const IR::Vector& annotations, const IR::Type* inputType, cstring controlPlaneName, int id, bool isParameter, cstring inputName) { cstring currentKeyName = inputName; const IR::Type* type = nullptr; - for (auto annotation : annotations) { + for (const auto* annotation : annotations) { if (annotation->name.name == "refers_to") { cstring destTableName = annotation->body[0]->text; cstring destKeyName = buildName(annotation->body); - if (auto bit = inputType->to()) { + if (const auto* bit = inputType->to()) { type = bit; - } else if (auto varbit = inputType->to()) { + } else if (const auto* varbit = inputType->to()) { type = varbit; - } else if (inputType->to()) { - type = IR::Type_Bits::get(32); - } else { + } else if (inputType->is()) { type = IR::Type_Bits::get(1); + } else { + BUG("Unexpected key type %s.", inputType->node_type_name()); } if (isParameter) { currentKeyName = "_param_" + inputName + std::to_string(id); @@ -122,18 +124,18 @@ void RefersToParser::createRefersToConstraint(IR::Vector annotat } const IR::Node* RefersToParser::postorder(IR::ActionListElement* action) { - auto findedAction = findAction(action); - if (!findedAction) { + const auto* actionCall = findAction(action); + if (actionCall == nullptr) { return action; } - if (auto table = findOrigCtxt()) { - if (findedAction->parameters) { + if (const auto* table = findOrigCtxt()) { + if (actionCall->parameters != nullptr) { int id = 0; - for (auto parameter : findedAction->parameters->parameters) { - if (parameter->annotations) { + for (const auto* parameter : actionCall->parameters->parameters) { + if (parameter->annotations != nullptr) { createRefersToConstraint(parameter->annotations->annotations, parameter->type, table->controlPlaneName(), id, true, - findedAction->controlPlaneName()); + actionCall->controlPlaneName()); } id++; } diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h index 30c3c4b88bc..f852eb19c43 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h @@ -15,21 +15,27 @@ namespace RefersToParser { class RefersToParser : public Transform { std::vector>& restrictionsVec; + std::vector actionVector; + /// Finds a P4Action in the actionVector according /// to the specified input argument which is an ActionListElement const IR::P4Action* findAction(const IR::ActionListElement* input); + /// An intermediate function that determines the type for future variables and partially /// collects their names for them, after which it calls the createConstraint function, /// which completes the construction of the constraint - void createRefersToConstraint(IR::Vector annotations, const IR::Type* inputType, - cstring controlPlaneName, int id, bool isParameter, - cstring inputName); + void createRefersToConstraint(const IR::Vector& annotations, + const IR::Type* inputType, cstring controlPlaneName, int id, + bool isParameter, cstring inputName); public: explicit RefersToParser(std::vector>& output); + const IR::Node* postorder(IR::ActionListElement* action) override; + const IR::Node* postorder(IR::Annotation* annotation) override; + /// Builds names for the zombie constant and then creates a zombie constant and builds the /// refers_to constraints based on them void createConstraint(bool table, cstring currentName, cstring currentKeyName, diff --git a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 deleted file mode 100755 index 888c380c989..00000000000 --- a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4 +++ /dev/null @@ -1,94 +0,0 @@ -#include - -header ethernet_t { - bit<48> dst_addr; - bit<48> src_addr; - bit<16> eth_type; -} - -header H { - bit<8> a; - bit<8> a1; - bit<8> b; -} - -struct Headers { - ethernet_t eth_hdr; - H h; -} - -struct Meta { } - -parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) { - state start { - pkt.extract(h.eth_hdr); - transition parse_h; - } - state parse_h { - pkt.extract(h.h); - transition accept; - } -} - -control vrfy(inout Headers h, inout Meta meta) { - apply { } -} - - -control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { - - action MyAction1() { - h.h.b = 1; - } - - action MyAction2() { - h.h.b = 2; - } - - action MyAction3() { - h.h.b = 3; - } - @entry_restriction(" - h.h.a1::mask != 0 && h.h.a1::prefix_length != 64; - h.h.a1 != 0; - h.h.a != 0xFF; - ") - table ternary_table { - key = { - h.h.isValid() : exact @name("valid"); - h.h.a : exact; - h.h.a1 : ternary; - } - - actions = { - NoAction; - MyAction1; - MyAction2; - MyAction3; - } - - size = 1024; - default_action = NoAction(); - } - - apply { - ternary_table.apply(); - } -} - -control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) { - apply { } -} - -control update(inout Headers h, inout Meta m) { - apply { } -} - -control deparser(packet_out pkt, in Headers h) { - apply { - pkt.emit(h); - } -} - - -V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; \ No newline at end of file diff --git a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 index af3628ee24b..e4283a67bb5 100755 --- a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 +++ b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 @@ -37,8 +37,8 @@ control vrfy(inout Headers h, inout Meta meta) { control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { - action MyAction1(@refers_to(table_1 , h.h.a) bit<8> input ) { - h.h.b = 1; + action MyAction1(@refers_to(table_1 , h.h.a) bit<8> input_val) { + h.h.b = input_val; } action MyAction2() { @@ -101,4 +101,4 @@ control deparser(packet_out pkt, in Headers h) { } -V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; \ No newline at end of file +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp index 8290193e378..fbfef03c733 100644 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -76,52 +76,61 @@ Restrictions loadExample(const char* curFile, bool flag) { P4Tools::MidEnd midEnd(options); program = program->apply(midEnd); Restrictions result; - if (flag) + if (flag) { program->apply(P4Tools::AssertsParser::AssertsParser(result)); - else + } else { program->apply(P4Tools::RefersToParser::RefersToParser(result)); + } return result; } TEST_F(P4AssertsParserTest, RestrictionCount) { Restrictions parsingResult = loadExample( - "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4", true); + "backends/p4tools/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); } TEST_F(P4AssertsParserTest, Restrictions) { Restrictions parsingResult = loadExample( - "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions.p4", true); + "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4", true); ASSERT_EQ(parsingResult.size(), (unsigned long)1); - auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_mask_h.h.a1"); - auto expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_lpm_prefix_h.h.a1"); - auto const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); - auto const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 64); - auto operation = new IR::LAnd(new IR::Neq(expr1, const1), new IR::Neq(expr2, const2)); - expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_key_h.h.a1"); - auto operation1 = new IR::Neq(expr1, const1); - expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_key_h.h.a"); - const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 255); - auto operation2 = new IR::Neq(expr1, const2); - ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); - ASSERT_TRUE(parsingResult[0][1]->equiv(*operation1)); - ASSERT_TRUE(parsingResult[0][2]->equiv(*operation2)); + { + const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_mask_h.h.a1"); + const auto& expr2 = P4Tools::IRUtils::getZombieConst( + IR::Type_Bits::get(8), 0, "ingress.ternary_table_lpm_prefix_h.h.a1"); + const auto* const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); + const auto* const2 = P4Tools::IRUtils::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)); + } + { + const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_key_h.h.a1"); + const auto* const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); + const auto* operation1 = new IR::Neq(expr1, const1); + ASSERT_TRUE(parsingResult[0][1]->equiv(*operation1)); + } + { + const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_key_h.h.a"); + const auto* const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 255); + const auto* operation2 = new IR::Neq(expr1, const2); + ASSERT_TRUE(parsingResult[0][2]->equiv(*operation2)); + } } TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), (unsigned long)2); - auto expr1 = + const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); - auto expr2 = + const auto& expr2 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.a"); - auto operation = new IR::Equ(expr1, expr2); + const auto* operation = new IR::Equ(expr1, expr2); ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); } From bd63d1a599e82684854b8da8cbfea28646ec3ab4 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Fri, 28 Oct 2022 14:02:21 +0300 Subject: [PATCH 19/25] Fix [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 21 +++++++------------ 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index e0f358ca062..b28797db58a 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -431,12 +431,12 @@ std::vector combineTokensToNumbers(std::vector input) { /// 0(Number)] -> [tableName_key_Name01(Text), ==(Equal) , 0(Number)] std::vector combineTokensToTableKeys(std::vector input, cstring tableName) { std::vector result; - for (uint64_t i = 0; i < input.size(); i++) { - if (!input[i].is(Token::Kind::Text)) { - result.push_back(input[i]); + for (uint64_t idx = 0; idx < input.size(); idx++) { + if (!input[idx].is(Token::Kind::Text)) { + result.push_back(input[idx]); continue; } - auto str = std::string(input[i].lexeme()); + auto str = std::string(input[idx].lexeme()); auto substr = str.substr(0, str.find("::mask")); if (substr != str) { @@ -459,16 +459,9 @@ std::vector combineTokensToTableKeys(std::vector input, cstring ta } if (str.find("isValid") != std::string::npos) { - i++; - cstring cString = str + std::string(input[i].lexeme()); - if (input[i + 1].is(Token::Kind::Text)) { - cString += std::string(input[i + 1].lexeme()); - i++; - } - cString += std::string(input[i + 1].lexeme()); - i++; - cString = tableName + "_key_" + cString; - result.emplace_back(Token::Kind::Text, cString, cString.size()); + cstring cstr = tableName + "_key_" + str; + result.emplace_back(Token::Kind::Text, cstr, cstr.size()); + idx += 2; continue; } From 0694a91ec44c2db45e8276fa1c7b0b5f5f10b64f Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Fri, 28 Oct 2022 15:25:08 +0300 Subject: [PATCH 20/25] Add new p4 program [no-jira] --- .../test/p4-programs/bmv2_restrictions_1.p4 | 94 +++++++++++++++++++ 1 file changed, 94 insertions(+) create mode 100644 backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4 diff --git a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4 b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4 new file mode 100644 index 00000000000..ee8ef2d6786 --- /dev/null +++ b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4 @@ -0,0 +1,94 @@ +#include + +header ethernet_t { + bit<48> dst_addr; + bit<48> src_addr; + bit<16> eth_type; +} + +header H { + bit<8> a; + bit<8> a1; + bit<8> b; +} + +struct Headers { + ethernet_t eth_hdr; + H h; +} + +struct Meta { } + +parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) { + state start { + pkt.extract(h.eth_hdr); + transition parse_h; + } + state parse_h { + pkt.extract(h.h); + transition accept; + } +} + +control vrfy(inout Headers h, inout Meta meta) { + apply { } +} + + +control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { + + action MyAction1() { + h.h.b = 1; + } + + action MyAction2() { + h.h.b = 2; + } + + action MyAction3() { + h.h.b = 3; + } + @entry_restriction(" + h.h.a1::mask != 0 && h.h.a1::prefix_length != 64; + h.h.a1 != 0; + h.h.a != 0xFF; + ") + table ternary_table { + key = { + h.h.isValid() : exact @name("valid"); + h.h.a : exact; + h.h.a1 : ternary; + } + + actions = { + NoAction; + MyAction1; + MyAction2; + MyAction3; + } + + size = 1024; + default_action = NoAction(); + } + + apply { + ternary_table.apply(); + } +} + +control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) { + apply { } +} + +control update(inout Headers h, inout Meta m) { + apply { } +} + +control deparser(packet_out pkt, in Headers h) { + apply { + pkt.emit(h); + } +} + + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; From 8152926a74a5e2c1af3f14784c37a5d94081acf2 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Mon, 31 Oct 2022 10:09:56 +0200 Subject: [PATCH 21/25] Add patch and fix makeSingleExpr function [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 68 +++++-------------- 1 file changed, 18 insertions(+), 50 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index b28797db58a..f1b8d67c6c4 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -89,38 +89,14 @@ std::ostream& operator<<(std::ostream& os, const Token::Kind& kind) { const IR::Expression* makeSingleExpr(std::vector input) { const IR::Expression* expr = nullptr; for (uint64_t idx = 0; idx < input.size(); idx++) { - if (const auto* lOr = input[idx]->to()) { - if (lOr->right->toString() == "(tmp") { - if (idx + 1 == input.size()) { - break; - } - std::vector tmp; - uint64_t jdx = idx; - idx++; - if (idx + 1 == input.size()) { - expr = new IR::LOr(input[jdx - 1], input[idx]); - break; - } - while (idx < input.size()) { - tmp.push_back(input[idx]); - idx++; - } - if (expr == nullptr) { - expr = new IR::LOr(input[jdx - 1], makeSingleExpr(tmp)); - } else { - expr = new IR::LOr(expr, makeSingleExpr(tmp)); - } + if (input[idx]->is()) { + if (idx + 1 == input.size()) { break; } - { - if (idx + 1 == input.size()) { - break; - } - if (expr == nullptr) { - expr = new IR::LOr(input[idx - 1], input[idx + 1]); - } else { - expr = new IR::LOr(expr, input[idx + 1]); - } + if (expr == nullptr) { + expr = new IR::LOr(input[idx - 1], input[idx + 1]); + } else { + expr = new IR::LOr(expr, input[idx + 1]); } } if (input[idx]->is()) { @@ -146,22 +122,16 @@ const IR::Expression* makeConstant(Token input, const IR::Vector auto inputStr = input.lexeme(); if (input.is(Token::Kind::Text)) { for (const auto* key : keyElements) { - cstring annotationName; - if (const auto* annotation = key->getAnnotation("name")) { + cstring keyName; + if (const auto* annotation = key->getAnnotation(IR::Annotation::nameAnnotation)) { if (!annotation->body.empty()) { - annotationName = annotation->body[0]->text; - } else if (!annotation->expr.empty()) { - annotationName = annotation->expr[0]->toString(); + keyName = annotation->getName(); } } - BUG_CHECK(annotationName.size() > 0, "Key does not have a name annotation."); - cstring separator = "\""; - if (annotationName.startsWith(separator) && annotationName.endsWith(separator)) { - annotationName = annotationName.substr(1, annotationName.size() - 2); - } - auto annoSize = annotationName.size(); + BUG_CHECK(keyName.size() > 0, "Key does not have a name annotation."); + auto annoSize = keyName.size(); auto tokenLength = inputStr.length(); - if (inputStr.find(annotationName, tokenLength - annoSize) == std::string::npos) { + if (inputStr.find(keyName, tokenLength - annoSize) == std::string::npos) { continue; } const auto* keyType = key->expression->type; @@ -307,14 +277,12 @@ const IR::Expression* getIR(std::vector tokens, idx = rightPart.second; exprVec.push_back(new IR::LNot(exprLNot)); } - } else if (token.is(Token::Kind::Implication)) { - const auto* tmp = exprVec[exprVec.size() - 1]; - exprVec.pop_back(); - const IR::Expression* expr1 = new IR::PathExpression(new IR::Path("tmp")); - exprVec.push_back(new IR::LNot(tmp)); - const IR::Expression* expr2 = new IR::PathExpression(new IR::Path("(tmp")); - exprVec.push_back(new IR::LOr(expr1, expr2)); - } else if (token.is(Token::Kind::Disjunction)) { + } else if (token.is_one_of(Token::Kind::Disjunction, Token::Kind::Implication)) { + if (token.is(Token::Kind::Implication)) { + const auto* tmp = exprVec[exprVec.size() - 1]; + exprVec.pop_back(); + exprVec.push_back(new IR::LNot(tmp)); + } const IR::Expression* expr1 = new IR::PathExpression(new IR::Path("tmp")); const IR::Expression* expr2 = new IR::PathExpression(new IR::Path("tmp")); exprVec.push_back(new IR::LOr(expr1, expr2)); From 843418d1b8e70b5943f459d41fa3d2d9de209262 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Mon, 31 Oct 2022 13:47:08 +0200 Subject: [PATCH 22/25] Fix [no-jira] --- backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index f1b8d67c6c4..ddc5fc1d30d 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -124,9 +124,7 @@ const IR::Expression* makeConstant(Token input, const IR::Vector for (const auto* key : keyElements) { cstring keyName; if (const auto* annotation = key->getAnnotation(IR::Annotation::nameAnnotation)) { - if (!annotation->body.empty()) { - keyName = annotation->getName(); - } + keyName = annotation->getName(); } BUG_CHECK(keyName.size() > 0, "Key does not have a name annotation."); auto annoSize = keyName.size(); From d19496a276b9f358d0fa73bbba55bda949a495f0 Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Tue, 1 Nov 2022 17:01:14 +0200 Subject: [PATCH 23/25] Fix [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 12 ++++--- .../targets/bmv2/p4_refers_to_parser.cpp | 8 +++-- .../testgen/targets/bmv2/program_info.cpp | 2 +- .../small-step/p4_asserts_parser_test.cpp | 35 ++++++++++--------- 4 files changed, 31 insertions(+), 26 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index ddc5fc1d30d..42720b472bc 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -4,7 +4,9 @@ #include #include "backends/p4tools/common/core/z3_solver.h" -#include "backends/p4tools/common/lib/ir.h" +#include "backends/p4tools/common/lib/util.h" +#include "ir/ir.h" +#include "ir/irutils.h" #include "lib/error.h" namespace P4Tools { @@ -142,18 +144,18 @@ const IR::Expression* makeConstant(Token input, const IR::Vector } else { BUG("Unexpected key type %s.", keyType->node_type_name()); } - return IRUtils::getZombieConst(type, 0, std::string(inputStr)); + return Utils::getZombieConst(type, 0, std::string(inputStr)); } } if (input.is(Token::Kind::Number)) { if (leftType == nullptr) { - return IRUtils::getConstant(IR::Type_Bits::get(32), static_cast(inputStr)); + return IR::getConstant(IR::Type_Bits::get(32), static_cast(inputStr)); } - return IRUtils::getConstant(leftType, static_cast(inputStr)); + return IR::getConstant(leftType, static_cast(inputStr)); } // TODO: Is this the right solution for priorities? if (input.is(Token::Kind::Priority)) { - return IRUtils::getZombieConst(IR::Type_Bits::get(32), 0, std::string(inputStr)); + return Utils::getZombieConst(IR::Type_Bits::get(32), 0, std::string(inputStr)); } BUG_CHECK(result != nullptr, "Could not match restriction key label %s was not found in key list.", diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp index aee3f97ccc1..3a5a8d69c05 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -2,7 +2,9 @@ #include -#include "backends/p4tools/common/lib/ir.h" +#include "backends/p4tools/common/lib/util.h" +#include "ir/ir.h" +#include "ir/irutils.h" namespace P4Tools { @@ -24,7 +26,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c } else { tmp = currentName + currentKeyName; } - auto left = IRUtils::getZombieConst(type, 0, tmp); + auto left = Utils::getZombieConst(type, 0, tmp); std::string str = currentName.c_str(); std::vector elems; std::stringstream ss(str); @@ -37,7 +39,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c str += elems[i] + "."; } tmp = str + destTableName + "_key_" + destKeyName; - auto right = IRUtils::getZombieConst(type, 0, tmp); + auto right = Utils::getZombieConst(type, 0, tmp); auto* expr = new IR::Equ(left, right); std::vector constraint; constraint.push_back(expr); diff --git a/backends/p4tools/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/testgen/targets/bmv2/program_info.cpp index 536d535683a..6113631069b 100644 --- a/backends/p4tools/testgen/targets/bmv2/program_info.cpp +++ b/backends/p4tools/testgen/targets/bmv2/program_info.cpp @@ -57,7 +57,7 @@ BMv2_V1ModelProgramInfo::BMv2_V1ModelProgramInfo( /// larger than 32 bits const IR::Operation_Binary* constraint = new IR::Grt(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(), - IRUtils::getConstant(ExecutionState::getPacketSizeVarType(), 32)); + IR::getConstant(ExecutionState::getPacketSizeVarType(), 32)); /// Vector containing pairs of restrictions and nodes to which these restrictions apply. std::vector> restrictionsVec; /// Defines all "entry_restriction" and then converts restrictions from string to IR diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp index fbfef03c733..71c210149c8 100644 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -11,13 +11,14 @@ #include "backends/p4test/version.h" #include "backends/p4tools/common/compiler/midend.h" -#include "backends/p4tools/common/lib/ir.h" +#include "backends/p4tools/common/lib/util.h" #include "frontends/common/parseInput.h" #include "frontends/p4/frontend.h" #include "gtest/gtest-message.h" #include "gtest/gtest-test-part.h" #include "gtest/gtest.h" #include "ir/ir.h" +#include "ir/irutils.h" #include "ir/node.h" #include "lib/log.h" @@ -96,27 +97,27 @@ TEST_F(P4AssertsParserTest, Restrictions) { "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_1.p4", true); ASSERT_EQ(parsingResult.size(), (unsigned long)1); { - const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_mask_h.h.a1"); - const auto& expr2 = P4Tools::IRUtils::getZombieConst( + const auto& expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.ternary_table_mask_h.h.a1"); + const auto& expr2 = P4Tools::Utils::getZombieConst( IR::Type_Bits::get(8), 0, "ingress.ternary_table_lpm_prefix_h.h.a1"); - const auto* const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); - const auto* const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 64); + const auto* const1 = IR::getConstant(IR::Type_Bits::get(8), 0); + 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)); } { - const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_key_h.h.a1"); - const auto* const1 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 0); + const auto& expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, + "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)); } { - const auto& expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.ternary_table_key_h.h.a"); - const auto* const2 = P4Tools::IRUtils::getConstant(IR::Type_Bits::get(8), 255); + const auto& expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, + "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)); } @@ -127,9 +128,9 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), (unsigned long)2); const auto& expr1 = - P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); + P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); const auto& expr2 = - P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.a"); + P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.a"); const auto* operation = new IR::Equ(expr1, expr2); ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); } @@ -138,10 +139,10 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { Restrictions parsingResult = loadExample( "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), (unsigned long)2); - auto expr1 = P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.table_1_param_ingress.MyAction10"); + auto expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, + "ingress.table_1_param_ingress.MyAction10"); auto expr2 = - P4Tools::IRUtils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); + P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); auto operation = new IR::Equ(expr1, expr2); ASSERT_TRUE(parsingResult[1][0]->equiv(*operation)); } From c571ddf683e019b14fc5cd550590d111789c1e3d Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Mon, 7 Nov 2022 13:24:41 +0200 Subject: [PATCH 24/25] Add patch [no-jira] --- .../targets/bmv2/p4_asserts_parser.cpp | 4 +- .../targets/bmv2/p4_refers_to_parser.cpp | 50 +++++++++---------- .../targets/bmv2/p4_refers_to_parser.h | 6 +-- .../testgen/targets/bmv2/program_info.cpp | 4 +- .../test/p4-programs/bmv2_restrictions_2.p4 | 9 ++-- 5 files changed, 38 insertions(+), 35 deletions(-) diff --git a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp index 42720b472bc..3f5e79f586b 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.cpp @@ -168,7 +168,7 @@ const IR::Expression* makeConstant(Token input, const IR::Vector /// Returning the end index is necessary so that after moving from the end of the right side std::pair, size_t> findRightPart(std::vector tokens, size_t index) { size_t idx = index + 1; - int endIdx = 0; + size_t endIdx = 0; bool flag = true; while (flag) { if (idx == tokens.size() || @@ -181,7 +181,7 @@ std::pair, size_t> findRightPart(std::vector tokens, s } std::vector rightTokens; - for (int j = index + 1; j < endIdx; j++) { + for (size_t j = index + 1; j < endIdx; j++) { rightTokens.push_back(tokens[j]); } return std::make_pair(rightTokens, idx); diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp index 3a5a8d69c05..fd91ba82548 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp @@ -46,29 +46,31 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c restrictionsVec.push_back(constraint); } -const IR::Node* RefersToParser::postorder(IR::Annotation* annotation) { +void RefersToParser::postorder(const IR::Annotation* annotation) { const IR::P4Action* prevAction = nullptr; - if (annotation->name.name == "refers_to") { - if (const auto* action = findOrigCtxt()) { - if (prevAction != action) { - actionVector.push_back(action); - prevAction = action; - } - } else if (const auto* keys = findOrigCtxt()) { - const auto* table = findOrigCtxt(); - CHECK_NULL(table); - const auto* key = findOrigCtxt(); - CHECK_NULL(key); - auto it = find(keys->keyElements.begin(), keys->keyElements.end(), key); - if (it != keys->keyElements.end()) { - int id = it - keys->keyElements.begin(); - createRefersToConstraint(key->annotations->annotations, key->expression->type, - table->controlPlaneName(), id, false, - key->expression->toString()); - } + if (annotation->name.name != "refers_to") { + return; + } + if (const auto* action = findOrigCtxt()) { + if (prevAction != action) { + actionVector.push_back(action); + prevAction = action; } + } else if (const auto* keys = findOrigCtxt()) { + const auto* table = findOrigCtxt(); + CHECK_NULL(table); + const auto* key = findOrigCtxt(); + CHECK_NULL(key); + auto it = find(keys->keyElements.begin(), keys->keyElements.end(), key); + if (it != keys->keyElements.end()) { + int id = it - keys->keyElements.begin(); + createRefersToConstraint(key->annotations->annotations, key->expression->type, + table->controlPlaneName(), id, false, + key->expression->toString()); + } + } else { + BUG("refers_to annotation %1% is attached to unsupported element.", *annotation); } - return annotation; } // Finds a P4Action in the actionVector according @@ -114,7 +116,7 @@ void RefersToParser::createRefersToConstraint(const IR::Vector& BUG("Unexpected key type %s.", inputType->node_type_name()); } if (isParameter) { - currentKeyName = "_param_" + inputName + std::to_string(id); + currentKeyName = "_arg_" + inputName + std::to_string(id); createConstraint(false, controlPlaneName, currentKeyName, destKeyName, destTableName, type); } else { @@ -125,10 +127,10 @@ void RefersToParser::createRefersToConstraint(const IR::Vector& } } -const IR::Node* RefersToParser::postorder(IR::ActionListElement* action) { +void RefersToParser::postorder(const IR::ActionListElement* action) { const auto* actionCall = findAction(action); if (actionCall == nullptr) { - return action; + return; } if (const auto* table = findOrigCtxt()) { if (actionCall->parameters != nullptr) { @@ -143,8 +145,6 @@ const IR::Node* RefersToParser::postorder(IR::ActionListElement* action) { } } } - - return action; } } // namespace RefersToParser diff --git a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h index f852eb19c43..bde86d7c82e 100644 --- a/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h +++ b/backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h @@ -13,7 +13,7 @@ namespace P4Tools { namespace RefersToParser { -class RefersToParser : public Transform { +class RefersToParser : public Inspector { std::vector>& restrictionsVec; std::vector actionVector; @@ -32,9 +32,9 @@ class RefersToParser : public Transform { public: explicit RefersToParser(std::vector>& output); - const IR::Node* postorder(IR::ActionListElement* action) override; + void postorder(const IR::ActionListElement* action) override; - const IR::Node* postorder(IR::Annotation* annotation) override; + void postorder(const IR::Annotation* annotation) override; /// Builds names for the zombie constant and then creates a zombie constant and builds the /// refers_to constraints based on them diff --git a/backends/p4tools/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/testgen/targets/bmv2/program_info.cpp index 6113631069b..f746e7cd350 100644 --- a/backends/p4tools/testgen/targets/bmv2/program_info.cpp +++ b/backends/p4tools/testgen/targets/bmv2/program_info.cpp @@ -66,8 +66,8 @@ BMv2_V1ModelProgramInfo::BMv2_V1ModelProgramInfo( /// Defines all "refers_to" and then converts restrictions from string to IR expressions, /// and stores them in restrictionsVec to move targetConstraints further. program->apply(RefersToParser::RefersToParser(restrictionsVec)); - for (auto element : restrictionsVec) { - for (auto restriction : element) { + for (const auto& element : restrictionsVec) { + for (const auto* restriction : element) { constraint = new IR::LAnd(constraint, restriction); } } diff --git a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 index e4283a67bb5..8547e82b646 100755 --- a/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 +++ b/backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4 @@ -50,7 +50,7 @@ control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { } table table_1 { key = { - h.h.a : exact @refers_to(table_2 , h.h.a); + h.h.a : exact @refers_to(table_2 , h.h.b); } actions = { @@ -66,7 +66,7 @@ control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { table table_2 { key = { - h.h.a : exact; + h.h.b : exact; } actions = { @@ -81,8 +81,11 @@ control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) { } apply { - table_2.apply(); + table_1.apply(); + if (h.h.a == 2) { + table_2.apply(); + } } } From e8ebd3222f5e809d146ff3f16fb4163f0af2e7cb Mon Sep 17 00:00:00 2001 From: OleksandrLetychevskyiIntel Date: Wed, 9 Nov 2022 11:07:07 +0200 Subject: [PATCH 25/25] Fix gtests [no-jira] --- .../testgen/test/small-step/p4_asserts_parser_test.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp index 71c210149c8..78132226f98 100644 --- a/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp +++ b/backends/p4tools/testgen/test/small-step/p4_asserts_parser_test.cpp @@ -130,7 +130,7 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) { const auto& expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); const auto& expr2 = - P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.a"); + P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.b"); const auto* operation = new IR::Equ(expr1, expr2); ASSERT_TRUE(parsingResult[0][0]->equiv(*operation)); } @@ -140,7 +140,7 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) { "backends/p4tools/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4", false); ASSERT_EQ(parsingResult.size(), (unsigned long)2); auto expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, - "ingress.table_1_param_ingress.MyAction10"); + "ingress.table_1_arg_ingress.MyAction10"); auto expr2 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a"); auto operation = new IR::Equ(expr1, expr2);