Skip to content

Commit

Permalink
[P4-Symbolic] Add function to create a fully symbolic entry.
Browse files Browse the repository at this point in the history 
PiperOrigin-RevId: 554836810
  • Loading branch information
@kishanps @VSuryaprasad-HCL
kishanps authored and VSuryaprasad-HCL committed Jan 9, 2025
1 parent fa49599 commit 8b1dd4d
Show file tree
Hide file tree
Showing 3 changed files with 129 additions and 70 deletions.
64 changes: 64 additions & 0 deletions p4_symbolic/symbolic/table_entry.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@
#include "p4_symbolic/symbolic/table_entry.h"

#include <algorithm>
#include <cstddef>
#include <optional>
#include <string>
#include <utility>

Expand All @@ -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"
Expand Down Expand Up @@ -309,4 +312,65 @@ absl::StatusOr<z3::expr> TableEntry::GetActionParameter(
action_param.bitwidth);
}

absl::StatusOr<ir::TableEntry> CreateSymbolicIrTableEntry(
const ir::Table &table, int priority, std::optional<size_t> 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
15 changes: 15 additions & 0 deletions p4_symbolic/symbolic/table_entry.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@
#ifndef PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_
#define PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_

#include <cstddef>
#include <optional>
#include <string>
#include <vector>

Expand Down Expand Up @@ -124,6 +126,19 @@ class TableEntry {

using TableEntries = absl::btree_map<std::string, std::vector<TableEntry>>;

// 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<ir::TableEntry> CreateSymbolicIrTableEntry(
const ir::Table &table, int priority = 0,
std::optional<size_t> prefix_length = std::nullopt);

} // namespace p4_symbolic::symbolic

#endif // PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_
120 changes: 50 additions & 70 deletions p4_symbolic/symbolic/table_entry_test.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,52 +72,15 @@ class IPv4RoutingTableEntriesTest : public testing::Test {
ir_entries_ = std::move(dataplane.entries);
}

absl::StatusOr<TableEntry> CreateSymbolicEntry(int entry_index,
int prefix_length) const {
absl::StatusOr<ir::Table> GetTable() const {
// The P4 program should have exactly one table.
if (state_->program.tables_size() != 1) {
return gutil::InternalErrorBuilder()
<< "The program must have exactly 1 table. Found "
<< 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:
Expand All @@ -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);
Expand All @@ -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()
Expand All @@ -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,
Expand All @@ -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));
Expand All @@ -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,
Expand All @@ -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,
Expand All @@ -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),
Expand Down Expand Up @@ -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();
Expand Down

0 comments on commit 8b1dd4d

Please sign in to comment.