Add a p4-constraints and @refers_to parser to P4Tools.

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
@@ -56,6 +57,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

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

backends/p4tools/testgen/targets/bmv2/p4_asserts_parser.h

@@ -0,0 +1,116 @@
+#ifndef TESTGEN_TARGETS_BMV2_P4_ASSERTS_PARSER_H_
+#define TESTGEN_TARGETS_BMV2_P4_ASSERTS_PARSER_H_
+
+#include <iomanip>
+#include <iostream>
+#include <string>
+#include <string_view>
+#include <utility>
+#include <vector>
+
+#include "ir/ir.h"
+
+namespace P4Tools {
+namespace AssertsParser {
+
+class AssertsParser : public Transform {
+    std::vector<std::vector<const IR::Expression*>>& restrictionsVec;
+
+ public:
+    explicit AssertsParser(std::vector<std::vector<const IR::Expression*>>& output);
+    /// A function that calls the beginning of the transformation of restrictions from a string into
+    /// an IR::Expression. Internally calls all other necessary functions, for example
+    /// combineTokensToNames and the like, to eventually get an IR expression that meets the string
+    /// constraint
+    static std::vector<const IR::Expression*> genIRStructs(
+        cstring tableName, cstring restrictionString,
+        const IR::Vector<IR::KeyElement>& keyElements);
+    const IR::Node* postorder(IR::P4Table* node) override;
+};
+
+class Token {
+ public:
+    enum class Kind {
+        Priority,
+        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;
+
+    void kind(Kind kind) noexcept;
+
+    bool is(Kind kind) const noexcept;
+
+    bool is_not(Kind kind) const noexcept;
+
+    bool is_one_of(Kind k1, Kind k2) const noexcept;
+
+    template <typename... Ts>
+    bool is_one_of(Kind k1, Kind k2, Ts... ks) const noexcept;
+
+    std::string_view lexeme() const noexcept;
+
+    void lexeme(std::string_view lexeme) noexcept;
+};
+
+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;
+    char prev() noexcept;
+    char get() noexcept;
+};
+}  // namespace AssertsParser
+}  // namespace P4Tools
+
+#endif /* TESTGEN_TARGETS_BMV2_P4_ASSERTS_PARSER_H_ */

backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.cpp

@@ -0,0 +1,147 @@
+#include "backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h"
+
+#include <boost/optional/optional_io.hpp>
+
+#include "backends/p4tools/common/lib/ir.h"
+
+namespace P4Tools {
+
+namespace RefersToParser {
+
+RefersToParser::RefersToParser(std::vector<std::vector<const IR::Expression*>>& output)
+    : restrictionsVec(output) {
+    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) {
+    cstring tmp = "";
+    if (table)
+        tmp = currentName + "_key_" + currentKeyName;
+    else
+        tmp = currentName + currentKeyName;
+    auto left = IRUtils::getZombieConst(type, 0, tmp);
+    std::string str = static_cast<std::string>(currentName);
+    std::vector<std::string> elems;
+    std::stringstream ss(str);
+    std::string item;
+    while (std::getline(ss, item, '.')) {
+        elems.push_back(item);
+    }
+    str = "";
+    for (long unsigned int 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<const IR::Expression*> 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<IR::P4Action>()) {
+            if (prevAction != action) {
+                actionVector.push_back(action);
+                prevAction = action;
+            }
+        } else if (auto keys = findOrigCtxt<IR::Key>()) {
+            auto table = findOrigCtxt<IR::P4Table>();
+            CHECK_NULL(table);
+            auto key = findOrigCtxt<IR::KeyElement>();
+            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;
+}
+// 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) {
+            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<IR::AnnotationToken> input) {
+    cstring result = "";
+    for (long unsigned int i = 2; i < input.size(); i++) {
+        result += input[i]->text;
+    }
+    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<IR::Annotation> 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) {
+        if (annotation->name.name == "refers_to") {
+            cstring destTableName = annotation->body[0]->text;
+            cstring destKeyName = buildName(annotation->body);
+            if (auto bit = inputType->to<IR::Type_Bits>()) {
+                type = bit;
+            } else if (auto varbit = inputType->to<IR::Extracted_Varbits>()) {
+                type = varbit;
+            } else if (inputType->to<IR::Type_Unknown>()) {
+                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);
+            }
+        }
+    }
+}
+
+const IR::Node* RefersToParser::postorder(IR::ActionListElement* action) {
+    auto findedAction = findAction(action);
+    if (!findedAction) {
+        return action;
+    }
+    if (auto table = findOrigCtxt<IR::P4Table>()) {
+        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

backends/p4tools/testgen/targets/bmv2/p4_refers_to_parser.h

@@ -0,0 +1,42 @@
+#ifndef TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_
+#define TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_
+
+#include <iomanip>
+#include <iostream>
+#include <string>
+#include <string_view>
+#include <utility>
+#include <vector>
+
+#include "ir/ir.h"
+
+namespace P4Tools {
+namespace RefersToParser {
+
+class RefersToParser : public Transform {
+    std::vector<std::vector<const IR::Expression*>>& restrictionsVec;
+    std::vector<const IR::P4Action*> 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<IR::Annotation> annotations, const IR::Type* inputType,
+                                  cstring controlPlaneName, int id, bool isParameter,
+                                  cstring inputName);
+
+ public:
+    explicit RefersToParser(std::vector<std::vector<const IR::Expression*>>& 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);
+};
+
+}  // namespace RefersToParser
+}  // namespace P4Tools
+
+#endif /* TESTGEN_TARGETS_BMV2_P4_REFERS_TO_PARSER_H_ */

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 {
 
@@ -50,11 +52,25 @@ 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
-    targetConstraints =
+    /// 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<std::vector<const IR::Expression*>> 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) {
+            constraint = new IR::LAnd(constraint, restriction);
+        }
+    }
+    targetConstraints = constraint;
 }
 
 const ordered_map<cstring, const IR::Type_Declaration*>*