diff --git a/p4_symbolic/symbolic/table_entry.cc b/p4_symbolic/symbolic/table_entry.cc index 7f662553..f186a541 100644 --- a/p4_symbolic/symbolic/table_entry.cc +++ b/p4_symbolic/symbolic/table_entry.cc @@ -15,6 +15,8 @@ #include "p4_symbolic/symbolic/table_entry.h" #include +#include +#include #include #include @@ -24,6 +26,7 @@ #include "absl/strings/string_view.h" #include "gutil/status.h" #include "p4/config/v1/p4info.pb.h" +#include "p4_pdpi/internal/ordered_map.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/util.h" @@ -309,4 +312,65 @@ absl::StatusOr TableEntry::GetActionParameter( action_param.bitwidth); } +absl::StatusOr CreateSymbolicIrTableEntry( + const ir::Table &table, int priority, std::optional prefix_length) { + // Build a symbolic table entry in P4-Symbolic IR. + ir::TableEntry ir_entry; + pdpi::IrTableEntry &sketch = + *ir_entry.mutable_symbolic_entry()->mutable_sketch(); + + // Set table name. + const std::string &table_name = table.table_definition().preamble().name(); + sketch.set_table_name(table_name); + + bool has_ternary_or_optional = false; + pdpi::IrMatch *lpm_match = nullptr; + + for (const auto &[match_name, match_definition] : + Ordered(table.table_definition().match_fields_by_name())) { + // Set match name. + pdpi::IrMatch *ir_match = sketch.add_matches(); + ir_match->set_name(match_name); + + const auto &pi_match = match_definition.match_field(); + switch (pi_match.match_type()) { + case MatchType::MatchField_MatchType_TERNARY: + case MatchType::MatchField_MatchType_OPTIONAL: { + has_ternary_or_optional = true; + break; + } + case MatchType::MatchField_MatchType_LPM: { + lpm_match = ir_match; + break; + } + default: { + // Exact or some other unsupported type, no need to do anything here. + // An absl error will be returned during symbolic evaluation. + break; + } + } + } + + // Set prefix length for single-LPM tables. + if (!has_ternary_or_optional && lpm_match) { + if (!prefix_length.has_value()) { + return gutil::InvalidArgumentErrorBuilder() + << "Prefix length must be provided for tables with a single LPM " + "match."; + } + lpm_match->mutable_lpm()->set_prefix_length(*prefix_length); + } + + // Set priority. + if (has_ternary_or_optional && priority <= 0) { + return gutil::InvalidArgumentErrorBuilder() + << "Priority must be greater than 0 for tables with ternary or " + "optional matches. Found: " + << priority; + } + sketch.set_priority(has_ternary_or_optional ? priority : 0); + + return ir_entry; +} + } // namespace p4_symbolic::symbolic diff --git a/p4_symbolic/symbolic/table_entry.h b/p4_symbolic/symbolic/table_entry.h index 8eb8a98c..4f5dd9ec 100644 --- a/p4_symbolic/symbolic/table_entry.h +++ b/p4_symbolic/symbolic/table_entry.h @@ -15,6 +15,8 @@ #ifndef PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ #define PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ +#include +#include #include #include @@ -124,6 +126,19 @@ class TableEntry { using TableEntries = absl::btree_map>; +// Returns a fully symbolic IR table entry for the given `table`. +// All matches will be specified as a symbolic match. +// If the given `table` has ternary or optional matches, the `priority` must be +// provided with a positive value, and it is set concretely in the table entry +// for deterministic entry priority. Otherwise the `priority` must be 0. +// If the given `table` has no ternary or optional matches, and has exactly 1 +// LPM match with zero or more exact matches, the `prefix_length` must be +// provided with a non-negative value, and it is set concretely in the table +// entry for deterministic entry priority. +absl::StatusOr CreateSymbolicIrTableEntry( + const ir::Table &table, int priority = 0, + std::optional prefix_length = std::nullopt); + } // namespace p4_symbolic::symbolic #endif // PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ diff --git a/p4_symbolic/symbolic/table_entry_test.cc b/p4_symbolic/symbolic/table_entry_test.cc index 89614811..cf6ffa36 100644 --- a/p4_symbolic/symbolic/table_entry_test.cc +++ b/p4_symbolic/symbolic/table_entry_test.cc @@ -72,8 +72,7 @@ class IPv4RoutingTableEntriesTest : public testing::Test { ir_entries_ = std::move(dataplane.entries); } - absl::StatusOr CreateSymbolicEntry(int entry_index, - int prefix_length) const { + absl::StatusOr GetTable() const { // The P4 program should have exactly one table. if (state_->program.tables_size() != 1) { return gutil::InternalErrorBuilder() @@ -81,43 +80,7 @@ class IPv4RoutingTableEntriesTest : public testing::Test { << state_->program.tables_size() << " tables."; } - const std::string &table_name = state_->program.tables().begin()->first; - const ir::Table &table = state_->program.tables().begin()->second; - - // The table should have exactly one LPM match. - if (table.table_definition().match_fields_by_name_size() != 1) { - return gutil::InternalErrorBuilder() - << "The table '" << table_name - << "' must have exactly 1 match. Found: " - << table.table_definition().DebugString(); - } - - const std::string &match_name = - table.table_definition().match_fields_by_name().begin()->first; - const p4::config::v1::MatchField &pi_match = table.table_definition() - .match_fields_by_name() - .begin() - ->second.match_field(); - - // The match should be an LPM match. - if (pi_match.match_type() != MatchType::MatchField_MatchType_LPM) { - return gutil::InternalErrorBuilder() - << "The match '" << match_name - << "' must be an LPM match. Found: " << pi_match.DebugString(); - } - - // Construct the symbolic table entry in P4-Symbolic IR. - ir::TableEntry ir_entry; - pdpi::IrTableEntry &sketch = - *ir_entry.mutable_symbolic_entry()->mutable_sketch(); - sketch.set_table_name(table_name); - pdpi::IrMatch &ir_match = *sketch.add_matches(); - ir_match.set_name(match_name); - ir_match.mutable_lpm()->set_prefix_length(prefix_length); - sketch.set_priority(0); - - // Build and return the symbolic table entry object. - return TableEntry(entry_index, ir_entry); + return state_->program.tables().begin()->second; } protected: @@ -127,11 +90,15 @@ class IPv4RoutingTableEntriesTest : public testing::Test { TEST_F(IPv4RoutingTableEntriesTest, SymbolicEntryWithGetterFunctions) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test all basic getter functions. EXPECT_EQ(entry.GetIndex(), entry_index); @@ -149,15 +116,17 @@ TEST_F(IPv4RoutingTableEntriesTest, SymbolicEntryWithGetterFunctions) { TEST_F(IPv4RoutingTableEntriesTest, MatchVariablesOfSymbolicEntry) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test the symbolic variables of the symbolic LPM match. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; const std::string &match_name = entry.GetPdpiIrTableEntry().matches(0).name(); int bitwidth = table.table_definition() .match_fields_by_name() @@ -180,15 +149,17 @@ TEST_F(IPv4RoutingTableEntriesTest, MatchVariablesOfSymbolicEntry) { TEST_F(IPv4RoutingTableEntriesTest, ActionInvocationVariablesOfSymbolicEntry) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test the symbolic variables of the symbolic action invocations. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; for (const auto &action_ref : table.table_definition().entry_actions()) { const std::string &action_name = action_ref.action().preamble().name(); ASSERT_OK_AND_ASSIGN(z3::expr action_invocation, @@ -205,15 +176,17 @@ TEST_F(IPv4RoutingTableEntriesTest, ActionInvocationVariablesOfSymbolicEntry) { TEST_F(IPv4RoutingTableEntriesTest, ActionParameterVariablesOfSymbolicEntry) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test the symbolic variables of the symbolic action parameters. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; for (const auto &action_ref : table.table_definition().entry_actions()) { const std::string &action_name = action_ref.action().preamble().name(); ASSERT_TRUE(state_->program.actions().contains(action_name)); @@ -236,15 +209,17 @@ TEST_F(IPv4RoutingTableEntriesTest, ActionParameterVariablesOfSymbolicEntry) { TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentMatch) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test getting the symbolic variables of a non-existent match. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; constexpr absl::string_view non_existent_match_name = "non_existent_match"; EXPECT_THAT( entry.GetMatchValues(non_existent_match_name, table, state_->program, @@ -256,18 +231,19 @@ TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentMatch) { TEST_F(IPv4RoutingTableEntriesTest, ErrorWithWildcardMatch) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry with all wildcard matches. - ASSERT_OK_AND_ASSIGN(TableEntry non_wildcard_entry, - CreateSymbolicEntry(entry_index, prefix_length)); - ir::TableEntry ir_entry = non_wildcard_entry.GetP4SymbolicIrTableEntry(); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry non_wildcard_entry(entry_index, ir_entry); ir_entry.mutable_symbolic_entry()->mutable_sketch()->clear_matches(); TableEntry entry(entry_index, ir_entry); // Test getting the symbolic variables of an all-wildcard symbolic entry. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; constexpr absl::string_view match_name = "hdr.ipv4.dstAddr"; EXPECT_THAT( entry.GetMatchValues(match_name, table, state_->program, @@ -279,15 +255,17 @@ TEST_F(IPv4RoutingTableEntriesTest, ErrorWithWildcardMatch) { TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentAction) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test getting the symbolic variables of a non-existent action. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; constexpr absl::string_view non_existent_action_name = "non_existent_action"; EXPECT_THAT(entry.GetActionInvocation(non_existent_action_name, table, *state_->context.z3_context), @@ -317,15 +295,17 @@ TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentAction) { TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentActionParameter) { constexpr int entry_index = 0; + constexpr int priority = 0; constexpr int prefix_length = 16; // Construct a symbolic table entry. - ASSERT_OK_AND_ASSIGN(TableEntry entry, - CreateSymbolicEntry(entry_index, prefix_length)); + ASSERT_OK_AND_ASSIGN(ir::Table table, GetTable()); + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + CreateSymbolicIrTableEntry(table, priority, prefix_length)); + TableEntry entry(entry_index, std::move(ir_entry)); // Test getting the symbolic variables of a non-existent action parameter. - ASSERT_EQ(state_->program.tables_size(), 1); - const ir::Table &table = state_->program.tables().begin()->second; constexpr absl::string_view non_existent_param_name = "non_existent_param"; for (const auto &action_ref : table.table_definition().entry_actions()) { const std::string &action_name = action_ref.action().preamble().name();