From f770f3063f4a37ad87dd16fb2b96af95dd0d403b Mon Sep 17 00:00:00 2001 From: VSuryaprasad-hcl <159443973+VSuryaprasad-HCL@users.noreply.github.com> Date: Mon, 20 Jan 2025 01:20:22 +0000 Subject: [PATCH] [P4_Symbolic] Overload `GetFieldBitwidth` to accept separate header and field names as parameters. (#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 --- p4_symbolic/symbolic/table_entry.cc | 312 ++++++++++++++++++++++++++++ p4_symbolic/symbolic/table_entry.h | 129 ++++++++++++ p4_symbolic/symbolic/util.cc | 65 +++--- p4_symbolic/symbolic/util.h | 12 +- 4 files changed, 490 insertions(+), 28 deletions(-) create mode 100644 p4_symbolic/symbolic/table_entry.cc create mode 100644 p4_symbolic/symbolic/table_entry.h diff --git a/p4_symbolic/symbolic/table_entry.cc b/p4_symbolic/symbolic/table_entry.cc new file mode 100644 index 00000000..7f662553 --- /dev/null +++ b/p4_symbolic/symbolic/table_entry.cc @@ -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 +#include +#include + +#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 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 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: + // "_entry____(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 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: + // "_entry___$chosen$" + return absl::StrCat(GetTableName(), "_entry_", GetIndex(), "_", action_name, + "_$chosen$"); +} + +absl::StatusOr +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: + // "_entry___" + std::string variable_name = absl::StrCat( + GetTableName(), "_entry_", GetIndex(), "_", action_name, "_", param_name); + return SymbolicActionParameterInfo{ + .variable_name = variable_name, + .bitwidth = bitwidth, + }; +} + +absl::StatusOr 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 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 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 diff --git a/p4_symbolic/symbolic/table_entry.h b/p4_symbolic/symbolic/table_entry.h new file mode 100644 index 00000000..8eb8a98c --- /dev/null +++ b/p4_symbolic/symbolic/table_entry.h @@ -0,0 +1,129 @@ +// 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. + +#ifndef PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ +#define PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ + +#include +#include + +#include "absl/container/btree_map.h" +#include "absl/status/statusor.h" +#include "absl/strings/string_view.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "z3++.h" + +namespace p4_symbolic::symbolic { + +// Contains the symbolic variables of a symbolic match of a table entry. +struct SymbolicMatchVariables { + p4::config::v1::MatchField::MatchType match_type; + z3::expr value; + z3::expr mask; +}; + +// Contains the symbolic variable names and bit-width of the symbolic match of a +// table entry. +struct SymbolicMatchInfo { + p4::config::v1::MatchField::MatchType match_type; + int bitwidth; + // Value variable name of the symbolic match. It looks like + // "_entry____value". + std::string value_variable_name; + // Value variable name of the symbolic match. It looks like + // "_entry____mask". + std::string mask_variable_name; +}; + +// Contains the symbolic variable name and bit-width of the symbolic action +// parameter of a table entry. +struct SymbolicActionParameterInfo { + // Variable name of the symbolic action parameter. It looks like + // "_entry___". + std::string variable_name; + int bitwidth; +}; + +class TableEntry { + public: + // Constructs a table entry object, where the `index` is the original index of + // the entry in the table and the `ir_entry` is the entry in P4-Symbolic IR. + TableEntry(int index, ir::TableEntry ir_entry); + + // Returns the original index of the entry as installed in the table. + int GetIndex() const; + // Returns true if the IR entry has a concrete entry. + bool IsConcrete() const; + // Returns true if the IR entry has a symbolic entry. + bool IsSymbolic() const; + // Returns the table name of the table to which the entry belongs. + const std::string &GetTableName() const; + // Returns the P4-Symbolic IR table entry. + const ir::TableEntry &GetP4SymbolicIrTableEntry() const; + // Returns the PDPI IR table entry, which may represent a concrete entry or + // the skeleton for a symbolic entry. + // Note: If symbolic, the returned entry may not be a well-formed PDPI IR + // entry. See p4_symbolic/ir/ir.proto for details. + const pdpi::IrTableEntry &GetPdpiIrTableEntry() const; + + // Returns the symbolic variables of the symbolic match with the given + // `match_name`. Returns an error if this is not a symbolic entry. + absl::StatusOr GetMatchValues( + absl::string_view match_name, const ir::Table &table, + const ir::P4Program &program, z3::context &z3_context) const; + // Returns the symbolic variable of the action invocation with the given + // `action_name`. Returns an error if this is not a symbolic entry. + absl::StatusOr GetActionInvocation(absl::string_view action_name, + const ir::Table &table, + z3::context &z3_context) const; + // Returns the symbolic variable of the action parameter with the given + // `param_name` in the `action`. Returns an error if this is not a symbolic + // entry. + absl::StatusOr GetActionParameter(absl::string_view param_name, + const ir::Action &action, + const ir::Table &table, + z3::context &z3_context) const; + + private: + int index_; // The original index of the entry in the table. + ir::TableEntry ir_entry_; // Entry in P4-Symbolic IR. + + // Returns the symbolic variable names, the bit-width, and the match type of + // the symbolic match with the given `match_name`. An error is returned if + // this is not a symbolic entry, or if the given `match_name` is not found in + // the table definition. + absl::StatusOr GetSymbolicMatchInfo( + absl::string_view match_name, const ir::Table &table, + const ir::P4Program &program) const; + // Returns the symbolic variable name of the action invocation with the given + // `action_name`. An error is returned if this is not a symbolic entry, or if + // the given `action_name` is not found in the table definition. + absl::StatusOr GetActionChoiceSymbolicVariableName( + absl::string_view action_name, const ir::Table &table) const; + // Returns the symbolic variable name and the bit-width of the action + // parameter with the given `action_name` and `param_name`. An error is + // returned if this is not a symbolic entry, or if the given `action_name` and + // `param_name` are not found in the table and action definition. + absl::StatusOr GetSymbolicActionParameterInfo( + absl::string_view param_name, const ir::Action &action, + const ir::Table &table) const; +}; + +using TableEntries = absl::btree_map>; + +} // namespace p4_symbolic::symbolic + +#endif // PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc index ddb7f665..63c5ca70 100644 --- a/p4_symbolic/symbolic/util.cc +++ b/p4_symbolic/symbolic/util.cc @@ -17,17 +17,25 @@ #include "p4_symbolic/symbolic/util.h" #include +#include +#include "absl/container/btree_map.h" #include "absl/status/status.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "absl/strings/str_split.h" #include "absl/strings/string_view.h" #include "absl/strings/substitute.h" #include "glog/logging.h" +#include "gutil/status.h" #include "p4_pdpi/internal/ordered_map.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/z3_util.h" +#include "z3++.h" namespace p4_symbolic { namespace symbolic { @@ -35,33 +43,27 @@ namespace util { namespace { -// Extract the header field definition of a `field_ref` from the given P4 -// `program`. +// Extracts the header field definition based on the given `header_name` and +// `field_name` from the given P4 `program`. absl::StatusOr GetFieldDefinition( - const ir::P4Program &program, absl::string_view field_ref) { - // Split the field reference into header and field names. - std::vector split = absl::StrSplit(field_ref, '.'); - if (split.size() != 2) { - return absl::InvalidArgumentError( - absl::Substitute("Expected
. got '$0'", field_ref)); - } - const std::string &header_name = split[0]; - const std::string &field_name = split[1]; - + const ir::P4Program &program, absl::string_view header_name, + absl::string_view field_name) { // Extract the header definition from the program. - if (!program.headers().contains(header_name)) { - return absl::InvalidArgumentError( - absl::Substitute("Unexpected header instance'$0'", header_name)); + auto header_it = program.headers().find(header_name); + if (header_it == program.headers().end()) { + return gutil::InvalidArgumentErrorBuilder() + << "Unexpected header instance '" << header_name << "'"; } - const p4_symbolic::ir::HeaderType &header_def = - program.headers().at(header_name); + const p4_symbolic::ir::HeaderType &header = header_it->second; // Extract the field definition from the header definition. - if (!header_def.fields().contains(field_name)) { - return absl::InvalidArgumentError(absl::Substitute( - "Unexpected field'$0' in header '$1'", field_name, header_name)); + auto field_it = header.fields().find(field_name); + if (field_it == header.fields().end()) { + return gutil::InvalidArgumentErrorBuilder() + << "Unexpected field '" << field_name << "' in header '" + << header_name << "'"; } - return header_def.fields().at(field_name); + return field_it->second; } } // namespace @@ -238,14 +240,27 @@ absl::StatusOr MergeDisjointTableMatches( return merged; } -absl::StatusOr GetFieldBitwidth(absl::string_view field_name, +absl::StatusOr GetFieldBitwidth(absl::string_view qualified_field_name, + const ir::P4Program &program) { + // Split the fully qualified field name into header and field names. + std::vector split = absl::StrSplit(qualified_field_name, '.'); + if (split.size() != 2) { + return absl::InvalidArgumentError(absl::Substitute( + "Expected
. got '$0'", qualified_field_name)); + } + return GetFieldBitwidth(/*header_name=*/split[0], /*field_name=*/split[1], + program); +} + +absl::StatusOr GetFieldBitwidth(absl::string_view header_name, + absl::string_view field_name, const ir::P4Program &program) { - if (absl::EndsWith(field_name, symbolic::kValidPseudoField) || - absl::EndsWith(field_name, symbolic::kExtractedPseudoField)) { + if (field_name == symbolic::kValidPseudoField || + field_name == symbolic::kExtractedPseudoField) { return 1; } else { ASSIGN_OR_RETURN(const ir::HeaderField field_definition, - GetFieldDefinition(program, field_name)); + GetFieldDefinition(program, header_name, field_name)); return field_definition.bitwidth(); } } diff --git a/p4_symbolic/symbolic/util.h b/p4_symbolic/symbolic/util.h index 2dd6b661..fdf42cbb 100644 --- a/p4_symbolic/symbolic/util.h +++ b/p4_symbolic/symbolic/util.h @@ -63,9 +63,15 @@ absl::StatusOr MergeDisjointTableMatches(const SymbolicTableMatches &lhs, const SymbolicTableMatches &rhs); -// Extracts the bit-width of the field with name `field_name` in the given -// `program`. -absl::StatusOr GetFieldBitwidth(absl::string_view field_name, +// Extracts the bit-width of the field with the `qualified_field_name` (i.e., +// `
.`) in the given `program`. +absl::StatusOr GetFieldBitwidth(absl::string_view qualified_field_name, + const ir::P4Program &program); + +// Extracts the bit-width of the field with the name `field_name` of header +// `header_name` in the given `program`. +absl::StatusOr GetFieldBitwidth(absl::string_view header_name, + absl::string_view field_name, const ir::P4Program &program); // Returns the full valid field name of the given header.