Skip to content

Commit

Permalink
[P4_Symbolic] Overload GetFieldBitwidth to accept separate header a…
Browse files Browse the repository at this point in the history 
…nd field names as parameters. (sonic-net#939)

* [P4_Symbolic] Remove and modify outdated comments. Make the order of creating symbolic header fields deterministic.Initialize standard metadata fields to 0.

* [P4-Symbolic] Overload `GetFieldBitwidth` to accept separate header and field names as parameters.

---------

Co-authored-by: kishanps <[email protected]>
  • Loading branch information
@VSuryaprasad-HCL @kishanps
VSuryaprasad-HCL and kishanps authored Jan 20, 2025
1 parent f871a54 commit f770f30
Show file tree
Hide file tree
Showing 4 changed files with 490 additions and 28 deletions.
312 changes: 312 additions & 0 deletions p4_symbolic/symbolic/table_entry.cc
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,312 @@
// Copyright 2024 Google LLC
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#include "p4_symbolic/symbolic/table_entry.h"

#include <algorithm>
#include <string>
#include <utility>

#include "absl/container/flat_hash_map.h"
#include "absl/status/statusor.h"
#include "absl/strings/str_cat.h"
#include "absl/strings/string_view.h"
#include "gutil/status.h"
#include "p4/config/v1/p4info.pb.h"
#include "p4_pdpi/ir.pb.h"
#include "p4_symbolic/ir/ir.pb.h"
#include "p4_symbolic/symbolic/util.h"
#include "z3++.h"

namespace p4_symbolic::symbolic {

using MatchType = p4::config::v1::MatchField::MatchType;

namespace {

// A static mapping between the PI match type to the type string.
const absl::flat_hash_map<MatchType, std::string> match_type_to_str = {
{MatchType::MatchField_MatchType_EXACT, "exact"},
{MatchType::MatchField_MatchType_LPM, "lpm"},
{MatchType::MatchField_MatchType_TERNARY, "ternary"},
{MatchType::MatchField_MatchType_OPTIONAL, "optional"},
};

} // namespace

TableEntry::TableEntry(int index, ir::TableEntry ir_entry)
: index_(index), ir_entry_(std::move(ir_entry)) {}

int TableEntry::GetIndex() const { return index_; }
bool TableEntry::IsConcrete() const { return ir_entry_.has_concrete_entry(); }
bool TableEntry::IsSymbolic() const { return ir_entry_.has_symbolic_entry(); }

const std::string &TableEntry::GetTableName() const {
return GetPdpiIrTableEntry().table_name();
}

const ir::TableEntry &TableEntry::GetP4SymbolicIrTableEntry() const {
return ir_entry_;
}

const pdpi::IrTableEntry &TableEntry::GetPdpiIrTableEntry() const {
if (IsConcrete()) return ir_entry_.concrete_entry();
return ir_entry_.symbolic_entry().sketch();
}

absl::StatusOr<SymbolicMatchInfo> TableEntry::GetSymbolicMatchInfo(
absl::string_view match_name, const ir::Table &table,
const ir::P4Program &program) const {
// Check if the match exists in the table definition.
if (!table.table_definition().match_fields_by_name().contains(match_name)) {
return gutil::NotFoundErrorBuilder()
<< "Match '" << match_name << "' not found in table '"
<< GetTableName() << "'";
}

const p4::config::v1::MatchField &pi_match_field = table.table_definition()
.match_fields_by_name()
.at(match_name)
.match_field();

// Check if the match type is specified and supported.
if (!pi_match_field.has_match_type() ||
!match_type_to_str.contains(pi_match_field.match_type())) {
return gutil::InvalidArgumentErrorBuilder()
<< "Match type must be one of [exact, lpm, ternary, optional]. "
"Found match: "
<< pi_match_field.DebugString();
}

// Return an error if this is a fully concrete entry.
if (IsConcrete()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Entry " << GetIndex() << " of table '" << GetTableName()
<< "' is not symbolic.";
}

// If the specified match of this entry is an explicit wildcard, return an
// error and no symbolic variable should be created.
const auto &entry_matches = GetPdpiIrTableEntry().matches();
auto ir_match_it =
std::find_if(entry_matches.begin(), entry_matches.end(),
[&match_name](const pdpi::IrMatch &match) -> bool {
return match.name() == match_name;
});
if (ir_match_it == entry_matches.end()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Match '" << match_name
<< "' is an explicit wildcard. The match is omitted in the IR table"
" entry. To specify a symbolic match, please set the match name"
" while leaving other fields unset.";
}

// Use the matched header field to get the match bit-width.
auto it = table.table_implementation().match_name_to_field().find(match_name);
if (it == table.table_implementation().match_name_to_field().end()) {
return gutil::NotFoundErrorBuilder()
<< "Match '" << match_name
<< "' not found in implementation of table '" << GetTableName()
<< "'. Found: " << table.DebugString();
}
ASSIGN_OR_RETURN(int bitwidth,
util::GetFieldBitwidth(it->second.header_name(),
it->second.field_name(), program));

// If the table definition has the match bit-width, make sure it is consistent
// with the one in the table implementation.
if (pi_match_field.bitwidth() != 0 && pi_match_field.bitwidth() != bitwidth) {
return gutil::InternalErrorBuilder()
<< "Bit-width of match '" << match_name << "' in table '"
<< GetTableName()
<< "' is inconsistent between the definition and implementation.";
}

// Construct and return the variable names with the following template:
// "<table_name>_entry_<index>_<match_name>_<match_type>_(value|mask)"
const auto &match_type = pi_match_field.match_type();
std::string name_prefix =
absl::StrCat(GetTableName(), "_entry_", GetIndex(), "_", match_name, "_",
match_type_to_str.at(match_type), "_");
return SymbolicMatchInfo{
.match_type = match_type,
.bitwidth = bitwidth,
.value_variable_name = absl::StrCat(name_prefix, "value"),
.mask_variable_name = absl::StrCat(name_prefix, "mask"),
};
}

absl::StatusOr<std::string> TableEntry::GetActionChoiceSymbolicVariableName(
absl::string_view action_name, const ir::Table &table) const {
// Check if the action exists in the table definition based on the given
// `action_name`.
auto action_ref_it = std::find_if(
table.table_definition().entry_actions().begin(),
table.table_definition().entry_actions().end(),
[&action_name](const pdpi::IrActionReference &action_ref) -> bool {
return action_ref.action().preamble().name() == action_name;
});

if (action_ref_it == table.table_definition().entry_actions().end()) {
return gutil::NotFoundErrorBuilder()
<< "Action '" << action_name << "' not found in table '"
<< GetTableName() << "'";
}

// Return an error if this is a fully concrete entry.
if (IsConcrete()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Entry " << GetIndex() << " of table '" << GetTableName()
<< "' is not symbolic.";
}

// Construct and return the variable name with the following template:
// "<table_name>_entry_<index>_<action_name>_$chosen$"
return absl::StrCat(GetTableName(), "_entry_", GetIndex(), "_", action_name,
"_$chosen$");
}

absl::StatusOr<SymbolicActionParameterInfo>
TableEntry::GetSymbolicActionParameterInfo(absl::string_view param_name,
const ir::Action &action,
const ir::Table &table) const {
const absl::string_view action_name =
action.action_definition().preamble().name();

// Check if the action with the given `action_name` exists in the table
// definition.
auto action_ref_it = std::find_if(
table.table_definition().entry_actions().begin(),
table.table_definition().entry_actions().end(),
[&action_name](const pdpi::IrActionReference &action_ref) -> bool {
return action_ref.action().preamble().name() == action_name;
});

if (action_ref_it == table.table_definition().entry_actions().end()) {
return gutil::NotFoundErrorBuilder()
<< "Action '" << action_name << "' not found in table '"
<< GetTableName() << "'";
}

// Return an error if this is a fully concrete entry.
if (IsConcrete()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Entry " << GetIndex() << " of table '" << GetTableName()
<< "' is not symbolic.";
}

// Check if the parameter with the given `param_name` exists in the action
// implementation.
auto param_bitwidth_it =
action.action_implementation().parameter_to_bitwidth().find(param_name);
if (param_bitwidth_it ==
action.action_implementation().parameter_to_bitwidth().end()) {
return gutil::NotFoundErrorBuilder()
<< "Action parameter '" << param_name
<< "' not found in implementation of action '" << action_name << "'";
}
int bitwidth = param_bitwidth_it->second;

// Check if the parameter with the given `param_name` exists in the action
// definition.
auto param_it = action.action_definition().params_by_name().find(param_name);
if (param_it == action.action_definition().params_by_name().end()) {
return gutil::NotFoundErrorBuilder()
<< "Action parameter '" << param_name
<< "' not found in definition of action '" << action_name << "'";
}

// If the action definition has the parameter bit-width, make sure it is
// consistent with the one in the action implementation.
if (param_it->second.param().bitwidth() != 0 &&
param_it->second.param().bitwidth() != bitwidth) {
return gutil::InternalErrorBuilder()
<< "Bit-width of parameter '" << param_name << "' in action '"
<< action_name
<< "' is inconsistent between the definition and implementation.";
}

// Construct and return the variable name and its bit-width with the following
// template:
// "<table_name>_entry_<index>_<action_name>_<param_name>"
std::string variable_name = absl::StrCat(
GetTableName(), "_entry_", GetIndex(), "_", action_name, "_", param_name);
return SymbolicActionParameterInfo{
.variable_name = variable_name,
.bitwidth = bitwidth,
};
}

absl::StatusOr<SymbolicMatchVariables> TableEntry::GetMatchValues(
absl::string_view match_name, const ir::Table &table,
const ir::P4Program &program, z3::context &z3_context) const {
// Return an error if this is a fully concrete entry.
if (IsConcrete()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Entry " << GetIndex() << " of table '" << GetTableName()
<< "' is not symbolic.";
}

// Get symbolic variable names.
ASSIGN_OR_RETURN(SymbolicMatchInfo match,
GetSymbolicMatchInfo(match_name, table, program));

// Construct and return the symbolic variables as Z3 expressions.
return SymbolicMatchVariables{
.match_type = match.match_type,
.value = z3_context.bv_const(match.value_variable_name.c_str(),
match.bitwidth),
.mask =
z3_context.bv_const(match.mask_variable_name.c_str(), match.bitwidth),
};
}

absl::StatusOr<z3::expr> TableEntry::GetActionInvocation(
absl::string_view action_name, const ir::Table &table,
z3::context &z3_context) const {
// Return an error if this is a fully concrete entry.
if (IsConcrete()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Entry " << GetIndex() << " of table '" << GetTableName()
<< "' is not symbolic.";
}

// Get symbolic variable names.
ASSIGN_OR_RETURN(std::string variable_name,
GetActionChoiceSymbolicVariableName(action_name, table));

// Construct and return the symbolic variable as a Z3 expression.
return z3_context.bool_const(variable_name.c_str());
}

absl::StatusOr<z3::expr> TableEntry::GetActionParameter(
absl::string_view param_name, const ir::Action &action,
const ir::Table &table, z3::context &z3_context) const {
// Return an error if this is a fully concrete entry.
if (IsConcrete()) {
return gutil::InvalidArgumentErrorBuilder()
<< "Entry " << GetIndex() << " of table '" << GetTableName()
<< "' is not symbolic.";
}

// Get symbolic variable names.
ASSIGN_OR_RETURN(auto action_param,
GetSymbolicActionParameterInfo(param_name, action, table));

// Construct and return the symbolic variable as a Z3 expression.
return z3_context.bv_const(action_param.variable_name.c_str(),
action_param.bitwidth);
}

} // namespace p4_symbolic::symbolic
Loading

0 comments on commit f770f30

Please sign in to comment.