Clean up the entry_restriction parser, make sure to print a warning w…

…hen constraints are not feasible.
p4lang · Jun 22, 2023 · 179b2e1 · 179b2e1
1 parent a5e9f50
commit 179b2e1
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 12 deletions.
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
@@ -512,17 +512,23 @@ const IR::Node *AssertsParser::postorder(IR::P4Table *node) {
         return node;
     }
 
+    Z3Solver solver;
     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;
+        // Using Z3Solver, we check the feasibility of restrictions, if they are not
+        // feasible, we delete keys and entries from the table to execute
+        // default_action
+        solver.push();
         if (solver.checkSat(restrictions) == true) {
             restrictionsVec.push_back(restrictions);
             continue;
         }
+        ::warning(
+            "Restriction %1% is not feasible. Not generating entries for table %2% and instead "
+            "using default action.",
+            restrStr, node);
+        solver.pop();
         auto *cloneTable = node->clone();
         auto *cloneProperties = node->properties->clone();
         IR::IndexedVector<IR::Property> properties;

diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp
@@ -1,7 +1,6 @@
 #include "backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h"
 
-#include <stddef.h>
-
+#include <cstddef>
 #include <cstdint>
 #include <iostream>
 #include <string>
@@ -13,7 +12,6 @@
 #include "ir/ir.h"
 #include "ir/vector.h"
 #include "lib/exceptions.h"
-#include "lib/log.h"
 #include "lib/null.h"
 
 namespace P4Tools::RefersToParser {
@@ -34,7 +32,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
     } else {
         tmp = currentName + currentKeyName;
     }
-    auto left = ToolsVariables::getSymbolicVariable(type, tmp);
+    const auto *left = ToolsVariables::getSymbolicVariable(type, tmp);
     std::string str = currentName.c_str();
     std::vector<std::string> elems;
     std::stringstream ss(str);
@@ -47,7 +45,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
         str += elems[i] + ".";
     }
     tmp = str + destTableName + "_key_" + destKeyName;
-    auto right = ToolsVariables::getSymbolicVariable(type, tmp);
+    const auto *right = ToolsVariables::getSymbolicVariable(type, tmp);
     auto *expr = new IR::Equ(left, right);
     std::vector<const IR::Expression *> constraint;
     constraint.push_back(expr);
@@ -64,9 +62,6 @@ cstring buildName(IR::Vector<IR::AnnotationToken> 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(const IR::Annotation *annotation,
                                               const IR::Type *inputType, cstring controlPlaneName,
                                               bool isParameter, cstring inputName) {