Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[P4_Symbolic] Add function to create a fully symbolic entry. #941

Merged
merged 6 commits into from
Jan 22, 2025
Merged

[P4_Symbolic] Add function to create a fully symbolic entry. #941

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
d3b98dc
[P4_Symbolic] Remove and modify outdated comments. Make the order of …
kishanps Jul 27, 2023
5ef654f
[P4-Symbolic] Overload `GetFieldBitwidth` to accept separate header a…
kishanps Aug 7, 2023
cf3dbf4
[P4-Symbolic] Create a class for symbolic table entries.
kishanps Aug 8, 2023
2844165
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Jan 20, 2025
b829084
[P4-Symbolic] Add function to create a fully symbolic entry.
kishanps Aug 8, 2023
1a53dd6
Merge branch 'main' into symbolic_import_branch_177
kishanps Jan 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
64 changes: 64 additions & 0 deletions p4_symbolic/symbolic/table_entry.cc
View file
Open in desktop
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
Open in desktop
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_
122 changes: 52 additions & 70 deletions p4_symbolic/symbolic/table_entry_test.cc
View file
Open in desktop
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,16 @@ 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 +117,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 +150,18 @@ 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 +178,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 +211,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 +233,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 +257,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 +297,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
Loading