Start to use a concrete key data structure.

Author: fruffy

Diff for: core/control_plane/control_plane_objects.cpp

@@ -6,6 +6,7 @@
 #include "backends/p4tools/common/control_plane/symbolic_variables.h"
 #include "backends/p4tools/common/lib/variables.h"
 #include "backends/p4tools/modules/flay/core/control_plane/substitute_variable.h"
+#include "backends/p4tools/modules/flay/core/lib/simplify_expression.h"
 #include "backends/p4tools/modules/flay/core/lib/z3_cache.h"
 #include "ir/irutils.h"
 #include "lib/timer.h"
@@ -290,6 +291,25 @@ Z3ControlPlaneAssignmentSet WildCardMatchEntry::computeZ3ControlPlaneAssignments
 TableConfiguration
 **************************************************************************************************/
 
+const IR::Expression *buildKeyMatches(const KeyMap &keyMap) {
+    if (keyMap.empty()) {
+        return IR::BoolLiteral::get(false);
+    }
+    const IR::Expression *hitCondition = nullptr;
+    for (const auto *key : keyMap) {
+        const auto *matchExpr = key->computeControlPlaneConstraint();
+        if (hitCondition == nullptr) {
+            hitCondition = matchExpr;
+        } else {
+            hitCondition = new IR::LAnd(hitCondition, matchExpr);
+        }
+    }
+    // The table can only "hit" when it is actually configured by the control-plane.
+    // Pay attention to how we use "toString" for the path name here.
+    // We need to match these choices correctly. TODO: Make this very explicit.
+    return hitCondition;
+}
+
 bool TableConfiguration::CompareTableMatch::operator()(const TableMatchEntry &left,
                                                        const TableMatchEntry &right) {
     return left.priority() > right.priority();
@@ -306,10 +326,10 @@ bool TableConfiguration::operator<(const ControlPlaneItem &other) const {
                                           : typeid(*this).hash_code() < typeid(other).hash_code();
 }
 
-void TableConfiguration::setTableKeyMatch(const IR::Expression *tableKeyMatch) {
-    _tableKeyMatch = tableKeyMatch;
+void TableConfiguration::setTableKeyMatch(const KeyMap &tableKeyMap) {
+    _tableKeyMatch = SimplifyExpression::simplify(buildKeyMatches(tableKeyMap));
     // When we set the table key match, we also need to recompute the match of all table entries.
-    auto z3TableKeyMatch = Z3Cache::set(tableKeyMatch);
+    auto z3TableKeyMatch = Z3Cache::set(_tableKeyMatch);
     for (const auto &tableMatchEntry : _tableEntries) {
         tableMatchEntry.get().setZ3Condition(z3TableKeyMatch);
     }
@@ -341,21 +361,21 @@ ControlPlaneAssignmentSet TableConfiguration::computeControlPlaneAssignments() c
         return defaultAssignments;
     }
 
-    // If we have more than kMaxEntriesPerTable entries we give up.
-    // Set the entries symbolic and assume they can be executed freely.
-    if (_tableEntries.size() > kMaxEntriesPerTable) {
-        for (const auto &[symbol, assignment] : defaultAssignments) {
-            const auto *symbolicVar =
-                ToolsVariables::getSymbolicVariable(symbol.get().type, symbol.get().label + "*");
-            auto it = defaultAssignments.find(symbol);
-            if (it == defaultAssignments.end()) {
-                defaultAssignments.emplace(symbol, *symbolicVar);
-            } else {
-                it->second = *symbolicVar;
-            }
-        }
-        return defaultAssignments;
-    }
+    // // If we have more than kMaxEntriesPerTable entries we give up.
+    // // Set the entries symbolic and assume they can be executed freely.
+    // if (_tableEntries.size() > kMaxEntriesPerTable) {
+    //     for (const auto &[symbol, assignment] : defaultAssignments) {
+    //         const auto *symbolicVar =
+    //             ToolsVariables::getSymbolicVariable(symbol.get().type, symbol.get().label + "*");
+    //         auto it = defaultAssignments.find(symbol);
+    //         if (it == defaultAssignments.end()) {
+    //             defaultAssignments.emplace(symbol, *symbolicVar);
+    //         } else {
+    //             it->second = *symbolicVar;
+    //         }
+    //     }
+    //     return defaultAssignments;
+    // }
 
     for (const auto &tableEntry : _tableEntries) {
         const auto &actionAssignments = tableEntry.get().actionAssignment();
@@ -384,10 +404,10 @@ Z3ControlPlaneAssignmentSet TableConfiguration::computeZ3ControlPlaneAssignments
 
     // If we have more than kMaxEntriesPerTable entries we give up.
     // Set the entries symbolic and assume they can be executed freely.
-    if (_tableEntries.size() > kMaxEntriesPerTable) {
-        defaultAssignments.setAllSymbolic();
-        return defaultAssignments;
-    }
+    // if (_tableEntries.size() > kMaxEntriesPerTable) {
+    //     defaultAssignments.setAllSymbolic();
+    //     return defaultAssignments;
+    // }
 
     Util::ScopedTimer timer("computeZ3ControlPlaneAssignments");
     auto z3TableKeyMatchOpt = Z3Cache::get(_tableKeyMatch);

Diff for: core/control_plane/control_plane_objects.h

@@ -337,6 +337,8 @@ TableConfiguration
 /// The active set of table entries. Sorted by type.
 using TableEntrySet = std::set<std::reference_wrapper<TableMatchEntry>, std::less<TableMatchEntry>>;
 
+using KeyMap = std::vector<const TableMatchKey *>;
+
 /// Concrete configuration of a control plane table. May contain arbitrary many table match
 /// entries.
 class TableConfiguration : public Z3ControlPlaneItem {
@@ -365,7 +367,7 @@ class TableConfiguration : public Z3ControlPlaneItem {
     bool operator<(const ControlPlaneItem &other) const override;
 
     /// Set the table key match expression.
-    void setTableKeyMatch(const IR::Expression *tableKeyMatch);
+    void setTableKeyMatch(const KeyMap &tableKeyMap);
 
     /// Adds a new table entry.
     int addTableEntry(TableMatchEntry &tableMatchEntry, bool replace);

Diff for: core/interpreter/table_executor.cpp

@@ -98,7 +98,7 @@ const IR::Key *TableExecutor::resolveKey(const IR::Key *key) const {
 KeyMap TableExecutor::computeHitCondition(const IR::Key &key) const {
     KeyMap keyMap;
     for (const auto *keyField : key.keyElements) {
-        keyMap.insert(computeTargetMatchType(keyField));
+        keyMap.push_back(computeTargetMatchType(keyField));
     }
     return keyMap;
 }
@@ -239,37 +239,16 @@ void TableExecutor::processTableActionOptions(
     }
 }
 
-const IR::Expression *TableExecutor::buildKeyMatches(const KeyMap &keyMap) {
-    if (keyMap.empty()) {
-        return IR::BoolLiteral::get(false);
-    }
-    const IR::Expression *hitCondition = nullptr;
-    for (const auto *key : keyMap) {
-        const auto *matchExpr = key->computeControlPlaneConstraint();
-        if (hitCondition == nullptr) {
-            hitCondition = matchExpr;
-        } else {
-            hitCondition = new IR::LAnd(hitCondition, matchExpr);
-        }
-    }
-    // The table can only "hit" when it is actually configured by the control-plane.
-    // Pay attention to how we use "toString" for the path name here.
-    // We need to match these choices correctly. TODO: Make this very explicit.
-    return hitCondition;
-}
-
 const IR::Expression *TableExecutor::processTable() {
     const auto &table = getP4Table();
     TableUtils::TableProperties properties;
     TableUtils::checkTableImmutability(table, properties);
 
     // Then, resolve the key.
     const auto *key = table.getKey();
-    const IR::Expression *tableKeyExpression = nullptr;
+    KeyMap tableKeyMap;
     if (key != nullptr) {
-        tableKeyExpression = buildKeyMatches(computeHitCondition(*resolveKey(key)));
-    } else {
-        tableKeyExpression = IR::BoolLiteral::get(false);
+        tableKeyMap = computeHitCondition(*resolveKey(key));
     }
 
     const auto *defaultActionPath = TableUtils::getDefaultActionName(table);
@@ -289,8 +268,7 @@ const IR::Expression *TableExecutor::processTable() {
     if (tableControlPlaneItem != controlPlaneConstraints().end()) {
         auto *tableControlPlaneConfiguration =
             tableControlPlaneItem->second.get().checkedTo<TableConfiguration>();
-        tableControlPlaneConfiguration->setTableKeyMatch(
-            SimplifyExpression::simplify(tableKeyExpression));
+        tableControlPlaneConfiguration->setTableKeyMatch(tableKeyMap);
     } else {
         ::P4::error("Table %s has no control plane configuration", table.controlPlaneName());
     }

Diff for: core/interpreter/table_executor.h

@@ -15,8 +15,6 @@ namespace P4::P4Tools::Flay {
 /// Forward declaration of the calling expression resolver.
 class ExpressionResolver;
 
-using KeyMap = std::set<const TableMatchKey *>;
-
 /// Executes a table and synthesizes control plane action parameters.
 class TableExecutor {
  private: