diff --git a/gutil/proto.cc b/gutil/proto.cc index 21b05575..dea72359 100644 --- a/gutil/proto.cc +++ b/gutil/proto.cc @@ -117,6 +117,15 @@ absl::StatusOr ProtoDiff( return diff; } +bool ProtoEqual(const google::protobuf::Message &message1, + const google::protobuf::Message &message2, + google::protobuf::util::MessageDifferencer &differ) { + if (message1.GetDescriptor() != message2.GetDescriptor()) { + return false; + } + return differ.Compare(message1, message2); +} + absl::StatusOr GetOneOfFieldName( const google::protobuf::Message &message, const std::string &oneof_name) { const auto *oneof_descriptor = diff --git a/gutil/proto.h b/gutil/proto.h index 896cb3d0..2a93f9a4 100644 --- a/gutil/proto.h +++ b/gutil/proto.h @@ -61,6 +61,11 @@ absl::StatusOr ProtoDiff( google::protobuf::util::MessageDifferencer differ = google::protobuf::util::MessageDifferencer()); +// Similar to `ProtoDiff`, execpt returns boolean result of equality comparison. +bool ProtoEqual(const google::protobuf::Message &message1, + const google::protobuf::Message &message2, + google::protobuf::util::MessageDifferencer &differ); + // Get the name of the oneof enum that is set. // Eg: // message IrValue { diff --git a/p4_fuzzer/BUILD.bazel b/p4_fuzzer/BUILD.bazel index 6af20f77..80b70684 100644 --- a/p4_fuzzer/BUILD.bazel +++ b/p4_fuzzer/BUILD.bazel @@ -1,4 +1,5 @@ load("@com_github_p4lang_p4c//:bazel/p4_library.bzl", "p4_library") +load("//p4_pdpi/testing:diff_test.bzl", "cmd_diff_test") package( licenses = ["notice"], @@ -25,7 +26,9 @@ cc_library( deps = [ "//p4_pdpi:entity_keys", "//gutil:collections", + "//gutil:proto", "//gutil:status", + "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", "//p4_pdpi/internal:ordered_map", "@com_github_google_glog//:glog", @@ -38,7 +41,9 @@ cc_library( "@com_google_absl//absl/strings", "@com_google_absl//absl/strings:str_format", "@com_google_absl//absl/types:optional", - ], + "@com_google_absl//absl/types:span", + "@com_google_protobuf//:protobuf", + ], ) cc_test( @@ -48,15 +53,18 @@ cc_test( ":switch_state", ":test_utils", "//gutil:collections", + "//gutil:proto", "//gutil:proto_matchers", "//gutil:status_matchers", "//p4_pdpi:ir", "//p4_pdpi/testing:main_p4_pd_cc_proto", "//p4_pdpi/testing:test_p4info_cc", + "//p4_pdpi:pd", "@com_github_google_glog//:glog", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", + "@com_google_absl//absl/types:optional", "@com_google_googletest//:gtest_main", ], ) @@ -92,7 +100,11 @@ cc_library( "fuzzer_config.h", ], deps = [ + ":table_entry_key", "//p4_pdpi:ir_cc_proto", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/container:btree", + "@com_google_absl//absl/container:flat_hash_set", ], ) @@ -113,15 +125,10 @@ cc_library( ":switch_state", "//gutil:collections", "//gutil:status", - "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", - "//p4_pdpi:pd", "//p4_pdpi/internal:ordered_map", "//p4_pdpi/netaddr:ipv6_address", "//p4_pdpi/utils:ir", - "//sai_p4/instantiations/google:instantiations", - "//sai_p4/instantiations/google:sai_p4info_cc", - "//sai_p4/fixed:p4_ids", "@com_github_google_glog//:glog", "@com_github_p4lang_p4runtime//:p4info_cc_proto", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", @@ -152,17 +159,12 @@ cc_test( ":mutation_and_fuzz_util", ":test_utils", "//gutil:collections", - "//gutil:proto", "//gutil:proto_matchers", "//gutil:status_matchers", - "//gutil:testing", - "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", - "//p4_pdpi:pd", - "//sai_p4/instantiations/google:instantiations", - "//sai_p4/instantiations/google:sai_p4info_cc", "@com_github_p4lang_p4runtime//:p4info_cc_proto", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/container:flat_hash_set", "@com_google_absl//absl/random", "@com_google_absl//absl/random:distributions", "@com_google_absl//absl/random:seed_sequences", @@ -276,6 +278,33 @@ cc_test( ], ) +cc_library( + name = "test_utils", + testonly = True, + srcs = ["test_utils.cc"], + hdrs = ["test_utils.h"], + deps = [ + ":fuzzer_config", + ":mutation_and_fuzz_util", + ":switch_state", + "//gutil:collections", + "//gutil:testing", + "//p4_pdpi:ir", + "//p4_pdpi:ir_cc_proto", + "//p4_pdpi/internal:ordered_map", + "//p4_pdpi/testing:test_p4info_cc", + "//sai_p4/instantiations/google:sai_p4info_cc", + "@com_github_p4lang_p4runtime//:p4info_cc_proto", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/random", + "@com_google_absl//absl/status", + "@com_google_absl//absl/status:statusor", + "@com_google_absl//absl/strings", + ], +) + +# -- P4 libraries for testing ------------------------------------------------- + p4_library( name = "single_table_single_entry", src = "p4_programs/single_table_single_entry.p4", @@ -308,40 +337,43 @@ p4_library( ], ) +p4_library( + name = "sai_main", + src = "p4_programs/sai-p4-google/sai_main.p4", + p4info_out = "sai_main_info.pb.txt", + deps = glob(["p4_programs/sai-p4-google/*"]), +) + cc_library( name = "acl_table_test_ids", hdrs = ["p4_programs/sai-p4-google/ids.h"], ) -cc_library( - name = "test_utils", - testonly = True, - srcs = ["test_utils.cc"], - hdrs = ["test_utils.h"], +# go/golden-test-with-coverage +cc_test( + name = "switch_state_assert_entry_equality_test_runner", + srcs = ["switch_state_assert_entry_equality_test_runner.cc"], + linkstatic = True, deps = [ - ":fuzzer_config", - ":mutation_and_fuzz_util", ":switch_state", "//gutil:collections", "//gutil:testing", "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", - "//p4_pdpi/internal:ordered_map", "//p4_pdpi/testing:test_p4info_cc", - "//sai_p4/instantiations/google:sai_p4info_cc", "@com_github_p4lang_p4runtime//:p4info_cc_proto", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", - "@com_google_absl//absl/random", "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", + "@com_google_absl//absl/types:span", + "@com_google_protobuf//:protobuf", ], ) -p4_library( - name = "sai_main", - src = "p4_programs/sai-p4-google/sai_main.p4", - p4info_out = "sai_main_info.pb.txt", - deps = glob(["p4_programs/sai-p4-google/*"]), +cmd_diff_test( + name = "switch_state_assert_entry_equality_test", + actual_cmd = "$(execpath :switch_state_assert_entry_equality_test_runner)", + expected = ":switch_state_assert_entry_equality_test.expected.output", + tools = [":switch_state_assert_entry_equality_test_runner"], ) - diff --git a/p4_fuzzer/fuzz_util.cc b/p4_fuzzer/fuzz_util.cc index 3f726838..f9cbf61c 100644 --- a/p4_fuzzer/fuzz_util.cc +++ b/p4_fuzzer/fuzz_util.cc @@ -25,9 +25,11 @@ #include "absl/base/internal/endian.h" #include "absl/container/btree_set.h" #include "absl/random/distributions.h" +#include "absl/status/status.h" #include "absl/status/statusor.h" #include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" +#include "absl/strings/substitute.h" #include "google/protobuf/repeated_field.h" #include "gutil/collections.h" #include "gutil/status.h" @@ -39,9 +41,7 @@ #include "p4_pdpi/internal/ordered_map.h" #include "p4_pdpi/ir.pb.h" #include "p4_pdpi/netaddr/ipv6_address.h" -#include "p4_pdpi/pd.h" #include "p4_pdpi/utils/ir.h" -#include "sai_p4/fixed/ids.h" namespace p4_fuzzer { @@ -98,6 +98,15 @@ bool IsReferring( namespace { +inline bool IsDisabledForFuzzing(const FuzzerConfig& config, + absl::string_view name) { + return config.disabled_fully_qualified_names.contains(name); +} + +std::string FuzzPort(absl::BitGen* gen, const FuzzerConfig& config) { + return UniformFromSpan(gen, config.ports); +} + inline int DivideRoundedUp(const unsigned int n, const unsigned int d) { if (n == 0 || d == 0) { return 0; @@ -106,10 +115,6 @@ inline int DivideRoundedUp(const unsigned int n, const unsigned int d) { return (n - 1) / d + 1; } -std::string FuzzPort(absl::BitGen* gen, const FuzzerConfig& config) { - return UniformFromSpan(gen, config.ports); -} - absl::StatusOr FuzzActionProfileAction( absl::BitGen* gen, const FuzzerConfig& config, const SwitchState& switch_state, @@ -118,9 +123,9 @@ absl::StatusOr FuzzActionProfileAction( ASSIGN_OR_RETURN( *action.mutable_action(), - FuzzAction( - gen, config, switch_state, - ChooseNonDefaultActionRef(gen, config, ir_table_info).action())); + FuzzAction(gen, config, switch_state, + UniformFromSpan(gen, AllValidActions(config, ir_table_info)) + .action())); action.set_weight(Uniform(*gen, 1, max_weight)); action.set_watch_port(FuzzPort(gen, config)); @@ -136,6 +141,8 @@ std::vector TablesUsedByFuzzer(const FuzzerConfig& config) { if (table.role() != config.role) continue; // Tables without actions cannot have valid table entries. if (table.entry_actions().empty()) continue; + // Tables on the disallow list should not be fuzzed. + if (IsDisabledForFuzzing(config, table.preamble().name())) continue; table_ids.push_back(key); } return table_ids; @@ -422,41 +429,57 @@ absl::StatusOr GetActionProfile( << "No action profile corresponds to table with id " << table_id; } -// Returns the list of all table IDs in the underlying P4 program. -const std::vector AllTableIds(const FuzzerConfig& config) { - std::vector table_ids; +/*const std::vector AllValidActions( + const FuzzerConfig& config, const pdpi::IrTableDefinition& table) { + std::vector actions; - for (auto& [table_id, table_def] : Ordered(config.info.tables_by_id())) { - table_ids.push_back(table_id); + for (const auto& action : table.entry_actions()) { + // Skip deprecated, unused, and disallowed actions. + if (pdpi::IsElementDeprecated(action.action().preamble().annotations()) || + pdpi::IsElementUnused(action.action().preamble().annotations()) || + IsDisabledForFuzzing(config, action.action().preamble().name())) + continue; + actions.push_back(action); } - return table_ids; -} + return actions; +}*/ -// Returns the list of all action IDs in the underlying P4 program. -const std::vector AllActionIds(const FuzzerConfig& config) { - std::vector action_ids; +const std::vector AllValidActions( + const FuzzerConfig& config, const pdpi::IrTableDefinition& table) { + std::vector actions; - for (auto& [action_id, action_def] : Ordered(config.info.actions_by_id())) { - action_ids.push_back(action_id); + for (const auto& action : table.entry_actions()) { + // Skip deprecated, unused, and disallowed actions. + if (pdpi::IsElementDeprecated(action.action().preamble().annotations()) || + action.action().is_unsupported() || + IsDisabledForFuzzing(config, action.action().preamble().name())) + continue; + actions.push_back(action); } - return action_ids; + return actions; } -// Returns the list of all match field IDs in the underlying P4 program for -// table with id table_id. -const std::vector AllMatchFieldIds(const FuzzerConfig& config, - const uint32_t table_id) { - std::vector match_ids; +const std::vector AllValidMatchFields( + const FuzzerConfig& config, const pdpi::IrTableDefinition& table) { + std::vector match_fields; + + for (const auto& [_, match_field_info] : + Ordered(table.match_fields_by_id())) { + // Skip deprecated, unused, and disallowed fields. + const std::string fully_qualified_match_field = absl::StrCat( + table.preamble().name(), ".", match_field_info.match_field().name()); + if (pdpi::IsElementDeprecated( + match_field_info.match_field().annotations()) || + //pdpi::IsElementUnused(match_field_info.match_field().annotations()) || + IsDisabledForFuzzing(config, fully_qualified_match_field)) + continue; - for (auto& [match_id, match_def] : - Ordered(gutil::FindOrDie(config.info.tables_by_id(), table_id) - .match_fields_by_id())) { - match_ids.push_back(match_id); + match_fields.push_back(match_field_info); } - return match_ids; + return match_fields; } std::string FuzzRandomId(absl::BitGen* gen, int min_chars, int max_chars) { @@ -491,18 +514,6 @@ Mutation FuzzMutation(absl::BitGen* gen, const FuzzerConfig& config) { return static_cast(UniformFromSpan(gen, valid_indexes)); } -pdpi::IrActionReference ChooseNonDefaultActionRef( - absl::BitGen* gen, const FuzzerConfig& config, - const pdpi::IrTableDefinition& ir_table_info) { - std::vector refs; - - for (const auto& action_ref : ir_table_info.entry_actions()) { - refs.push_back(action_ref); - } - - return UniformFromSpan(gen, refs); -} - std::string SetUnusedBitsToZero(int used_bits, std::string data) { const int bytes = data.size(); const int used_bytes = DivideRoundedUp(used_bits, kBitsInByte); @@ -760,7 +771,10 @@ absl::StatusOr FuzzAction( std::string value, FuzzValue(gen, config, switch_state, ir_param.param().type_name(), ir_param.param().bitwidth(), ir_param.references(), - /*non_zero=*/true)); + /*non_zero=*/true), + _.SetPrepend() << "while fuzzing parameter '" << ir_param.param().name() + << "' of action '" << ir_action_info.preamble().name() + << "': "); param->set_value(value); } @@ -776,6 +790,99 @@ absl::StatusOr FuzzAction( // However, uniform sampling gives us highly clustered weights almost all the // time and we prefer to generate skewed weights more often. Therefore, this // simpler approach, should serve us well. +/*absl::StatusOr FuzzActionProfileActionSet( + absl::BitGen* gen, const FuzzerConfig& config, + const SwitchState& switch_state, + const pdpi::IrTableDefinition& ir_table_info) { + p4::v1::ActionProfileActionSet action_set; + + ASSIGN_OR_RETURN( + auto action_profile, + GetActionProfile(config.info, ir_table_info.preamble().id())); + + switch (action_profile.selector_size_semantics()) { + case p4::config::v1::ActionProfile::SUM_OF_MEMBERS: { + int max_number_of_actions = action_profile.max_group_size() != 0 + ? action_profile.max_group_size() + : kActionProfileActionSetMaxCardinality; + int number_of_actions = Uniform(absl::IntervalClosedClosed, *gen, 0, + max_number_of_actions); + + for (int i = 0; i < number_of_actions; i++) { + ASSIGN_OR_RETURN( + auto action, + FuzzActionProfileAction(gen, config, switch_state, ir_table_info, + kActionProfileMaxMemberWeight)); + *action_set.add_action_profile_actions() = action; + } + + return action_set; + } + case p4::config::v1::ActionProfile::SUM_OF_WEIGHTS: { + // The max_group_size specifies the maximum total weight of a group of + // actions in an Action Selector (described by an ActionProfileActionSet). + // If max_group_size is 0, then any weights less than size are allowed by + // the server. + int unallocated_weight = action_profile.max_group_size() == 0 + ? action_profile.size() + : action_profile.max_group_size(); + + // Note that the semantics of `size` in an action selector is the maximum + // sum of all member weights across ALL selector groups. The + // `max_group_size` is the maximum sum of all member weights within a + // single group. Thus, the maximum total weight of a single group should + // be no larger than either the max_group_size or the size. + // TODO: When https://github.com/p4lang/p4runtime/issues/355 + // is fixed, `max_group_size` will never be greater than `size`, rendering + // this assignment unnecessary. + unallocated_weight = static_cast( + std::min(int64_t{unallocated_weight}, action_profile.size())); + + // It is entirely unclear what should happen if max_group_size or size is + // negative or if size is 0. Since these values are nonsensical, we will + // return an InvalidArgumentError until the specification changes. + // TODO: This if-statement can also disappear if + // https://github.com/p4lang/p4runtime/issues/355 is resolved, ruling out + // these cases. + if (unallocated_weight <= 0) { + return gutil::InvalidArgumentErrorBuilder() + << "non-positive size '" << action_profile.size() + << "' or negative max_group_size '" + << action_profile.max_group_size() << "' in action profile '" + << action_profile.preamble().alias() << "'"; + } + + // We want to randomly select some number of actions up to our max + // cardinality; however, we can't have more actions than the amount of + // weight we support since every action must have weight >= 1. + int number_of_actions = Uniform( + absl::IntervalClosedClosed, *gen, 0, + std::min(unallocated_weight, kActionProfileActionSetMaxCardinality)); + + for (int i = 0; i < number_of_actions; i++) { + // Since each action must have at least weight 1, we need to take the + // number of remaining actions into account to determine the acceptable + // max weight. + int remaining_actions = number_of_actions - i - 1; + int max_weight = unallocated_weight - remaining_actions; + + ASSIGN_OR_RETURN(auto action, + FuzzActionProfileAction(gen, config, switch_state, + ir_table_info, max_weight)); + *action_set.add_action_profile_actions() = action; + unallocated_weight -= action.weight(); + } + + return action_set; + } + default: + return absl::InvalidArgumentError(absl::Substitute( + "action profile '$0' uses invalid selector size semantics '$1'", + action_profile.preamble().alias(), + action_profile.selector_size_semantics())); + } +}*/ + absl::StatusOr FuzzActionProfileActionSet( absl::BitGen* gen, const FuzzerConfig& config, const SwitchState& switch_state, @@ -786,60 +893,89 @@ absl::StatusOr FuzzActionProfileActionSet( auto action_profile, GetActionProfile(config.info, ir_table_info.preamble().id())); - // The max_group_size specifies the maximum total weight of a group of actions - // in an Action Selector (described by an ActionProfileActionSet). - // If max_group_size is 0, then any weights less than size are allowed by the - // server. - int unallocated_weight = action_profile.max_group_size() == 0 - ? action_profile.size() - : action_profile.max_group_size(); - - // Note that the semantics of `size` in an action selector is the maximum - // sum of all member weights across ALL selector groups. The `max_group_size` - // is the maximum sum of all member weights within a single group. - // Thus, the maximum total weight of a single group should be - // no larger than either the max_group_size or the size. - // TODO: When https://github.com/p4lang/p4runtime/issues/355 is fixed, - // `max_group_size` will never be greater than `size`, rendering this - // assignment unnecessary. - unallocated_weight = static_cast( - std::min(int64_t{unallocated_weight}, action_profile.size())); - - // It is entirely unclear what should happen if max_group_size or size is - // negative or if size is 0. Since these values are nonsensical, we will - // return an InvalidArgumentError until the specification changes. - // TODO: This if-statement can also disappear if - // https://github.com/p4lang/p4runtime/issues/355 is resolved, ruling out - // these cases. - if (unallocated_weight <= 0) { - return gutil::InvalidArgumentErrorBuilder() - << "non-positive size '" << action_profile.size() - << "' or negative max_group_size '" - << action_profile.max_group_size() << "' in action profile '" - << action_profile.preamble().alias() << "'"; - } - - // We want to randomly select some number of actions up to our max - // cardinality; however, we can't have more actions than the amount of weight - // we support since every action must have weight >= 1. - int number_of_actions = Uniform( - absl::IntervalClosedClosed, *gen, 0, - std::min(unallocated_weight, kActionProfileActionSetMaxCardinality)); - - for (int i = 0; i < number_of_actions; i++) { - // Since each action must have at least weight 1, we need to take the number - // of remaining actions into account to determine the acceptable max weight. - int remaining_actions = number_of_actions - i - 1; - int max_weight = unallocated_weight - remaining_actions; - - ASSIGN_OR_RETURN(auto action, - FuzzActionProfileAction(gen, config, switch_state, - ir_table_info, max_weight)); - *action_set.add_action_profile_actions() = action; - unallocated_weight -= action.weight(); - } - - return action_set; + if (action_profile.has_sum_of_members()) { + int max_number_of_actions = action_profile.max_group_size() != 0 + ? action_profile.max_group_size() + : kActionProfileActionSetMaxCardinality; + int number_of_actions = Uniform( + absl::IntervalClosedClosed, *gen, + config.no_empty_action_profile_groups ? 1 : 0, max_number_of_actions); + + // Get the max member weight from the P4Info if it is set. + int max_member_weight = + action_profile.sum_of_members().max_member_weight() != 0 + ? action_profile.sum_of_members().max_member_weight() + : kActionProfileMaxMemberWeight; + + for (int i = 0; i < number_of_actions; i++) { + ASSIGN_OR_RETURN(auto action, FuzzActionProfileAction( + gen, config, switch_state, + ir_table_info, max_member_weight)); + *action_set.add_action_profile_actions() = action; + } + + return action_set; + } else { + // If the action profile does not use SumOfMembers semantics, then it must + // be SumOfWeights since that is both the default and the only other option. + + // The max_group_size specifies the maximum total weight of a group of + // actions in an Action Selector (described by an ActionProfileActionSet). + // If max_group_size is 0, then any weights less than size are allowed by + // the server. + int unallocated_weight = action_profile.max_group_size() == 0 + ? action_profile.size() + : action_profile.max_group_size(); + + // Note that the semantics of `size` in an action selector is the maximum + // sum of all member weights across ALL selector groups. The + // `max_group_size` is the maximum sum of all member weights within a + // single group. Thus, the maximum total weight of a single group should + // be no larger than either the max_group_size or the size. + // TODO: When https://github.com/p4lang/p4runtime/issues/355 + // is fixed, `max_group_size` will never be greater than `size`, rendering + // this assignment unnecessary. + unallocated_weight = static_cast( + std::min(int64_t{unallocated_weight}, action_profile.size())); + + // It is entirely unclear what should happen if max_group_size or size is + // negative or if size is 0. Since these values are nonsensical, we will + // return an InvalidArgumentError until the specification changes. + // TODO: This if-statement can also disappear if + // https://github.com/p4lang/p4runtime/issues/355 is resolved, ruling out + // these cases. + if (unallocated_weight <= 0) { + return gutil::InvalidArgumentErrorBuilder() + << "non-positive size '" << action_profile.size() + << "' or negative max_group_size '" + << action_profile.max_group_size() << "' in action profile '" + << action_profile.preamble().alias() << "'"; + } + + // We want to randomly select some number of actions up to our max + // cardinality; however, we can't have more actions than the amount of + // weight we support since every action must have weight >= 1. + int number_of_actions = Uniform( + absl::IntervalClosedClosed, *gen, + config.no_empty_action_profile_groups ? 1 : 0, + std::min(unallocated_weight, kActionProfileActionSetMaxCardinality)); + + for (int i = 0; i < number_of_actions; i++) { + // Since each action must have at least weight 1, we need to take the + // number of remaining actions into account to determine the acceptable + // max weight. + int remaining_actions = number_of_actions - i - 1; + int max_weight = unallocated_weight - remaining_actions; + + ASSIGN_OR_RETURN(auto action, + FuzzActionProfileAction(gen, config, switch_state, + ir_table_info, max_weight)); + *action_set.add_action_profile_actions() = action; + unallocated_weight -= action.weight(); + } + + return action_set; + } } void EnforceTableConstraints(absl::BitGen* gen, const FuzzerConfig& config, @@ -861,7 +997,8 @@ absl::StatusOr FuzzAction( *result.mutable_action(), FuzzAction( gen, config, switch_state, - ChooseNonDefaultActionRef(gen, config, table_definition).action())); + UniformFromSpan(gen, AllValidActions(config, table_definition)) + .action())); } else { ASSIGN_OR_RETURN(*result.mutable_action_profile_action_set(), FuzzActionProfileActionSet(gen, config, switch_state, @@ -878,15 +1015,8 @@ absl::StatusOr FuzzValidTableEntry( table_entry.set_table_id(ir_table_info.preamble().id()); // Generate the matches. - for (auto& [key, match_field_info] : ir_table_info.match_fields_by_id()) { - // Skip deprecated fields - bool deprecated = - absl::c_any_of(match_field_info.match_field().annotations(), - [](const std::string annotation) { - return absl::StartsWith(annotation, "@deprecated("); - }); - if (deprecated) continue; - + for (const pdpi::IrMatchFieldDefinition& match_field_info : + AllValidMatchFields(config, ir_table_info)) { // If the field can have wildcards, we generate a wildcard match with // probability `kFieldMatchWildcardProbability`. // In the P4RT spec, wildcards are represented as the absence of a match @@ -915,7 +1045,8 @@ absl::StatusOr FuzzValidTableEntry( // Generate the action. ASSIGN_OR_RETURN(*table_entry.mutable_action(), - FuzzAction(gen, config, switch_state, ir_table_info)); + FuzzAction(gen, config, switch_state, ir_table_info), + _.SetPrepend() << "while fuzzing action: "); // Set cookie and priority. table_entry.set_metadata( diff --git a/p4_fuzzer/fuzz_util.h b/p4_fuzzer/fuzz_util.h index 36582ae8..eb01aeaf 100644 --- a/p4_fuzzer/fuzz_util.h +++ b/p4_fuzzer/fuzz_util.h @@ -31,16 +31,13 @@ #include #include "absl/random/random.h" -#include "absl/strings/match.h" #include "absl/types/optional.h" #include "absl/types/span.h" #include "glog/logging.h" -#include "p4/config/v1/p4info.pb.h" -#include "p4/v1/p4runtime.pb.h" #include "p4_fuzzer/fuzzer.pb.h" #include "p4_fuzzer/fuzzer_config.h" #include "p4_fuzzer/switch_state.h" -#include "p4_pdpi/ir.h" +#include "p4_pdpi/ir.pb.h" namespace p4_fuzzer { @@ -48,6 +45,10 @@ namespace p4_fuzzer { // that support one-shot action selector programming. constexpr int kActionProfileActionSetMaxCardinality = 32; +// Max member weight for action profiles that use SumOfMembers size semantics. +// TODO: Get this information from the P4Info when possible. +constexpr int kActionProfileMaxMemberWeight = 4095; + // A predicate over P4 values (match field or action parameter). using P4ValuePredicate = std::function& vec) { absl::StatusOr GetActionProfile( const pdpi::IrP4Info& ir_info, int table_id); -// Returns the list of all table IDs in the underlying P4 program. -const std::vector AllTableIds(const FuzzerConfig& config); - -// Returns the list of all action IDs in the underlying P4 program. -const std::vector AllActionIds(const FuzzerConfig& config); +// Returns the list of all "valid" actions in the underlying P4 program for +// `table`. Valid actions are those that are legal for use in table entries and +// not @deprecated, @unused, or disabled. +const std::vector AllValidActions( + const FuzzerConfig& config, const pdpi::IrTableDefinition& table); -// Returns the list of all match field IDs in the underlying P4 program for -// table with id table_id. -const std::vector AllMatchFieldIds(const FuzzerConfig& config, - const uint32_t table_id); +// Returns the list of all "valid" match fields in the underlying P4 program for +// `table`. Valid match fields are those that are not @deprecated, @unused, or +// disabled. +const std::vector AllValidMatchFields( + const FuzzerConfig& config, const pdpi::IrTableDefinition& table); // Takes a string `data` that represents a number in network byte // order (big-endian), and masks off all but the least significant `used_bits` @@ -221,12 +223,6 @@ AnnotatedWriteRequest FuzzWriteRequest( const SwitchState& switch_state, absl::optional max_batch_size = absl::nullopt); -// Takes a P4 Runtime table and returns randomly chosen action ref from the -// action refs that are not in default only scope. -pdpi::IrActionReference ChooseNonDefaultActionRef( - absl::BitGen* gen, const FuzzerConfig& config, - const pdpi::IrTableDefinition& ir_table_info); - } // namespace p4_fuzzer #endif // P4_FUZZER_FUZZ_UTIL_H_ diff --git a/p4_fuzzer/fuzz_util_test.cc b/p4_fuzzer/fuzz_util_test.cc index 7e1f3b8a..a83dddcf 100644 --- a/p4_fuzzer/fuzz_util_test.cc +++ b/p4_fuzzer/fuzz_util_test.cc @@ -13,36 +13,36 @@ // limitations under the License. #include "p4_fuzzer/fuzz_util.h" +#include #include #include +#include +#include "absl/container/flat_hash_set.h" #include "absl/random/distributions.h" #include "absl/random/random.h" #include "absl/random/seed_sequences.h" #include "absl/status/status.h" #include "absl/status/statusor.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/str_split.h" #include "gmock/gmock.h" #include "gtest/gtest.h" #include "gutil/collections.h" -#include "gutil/proto.h" #include "gutil/proto_matchers.h" #include "gutil/status_matchers.h" -#include "gutil/testing.h" #include "p4/config/v1/p4info.pb.h" #include "p4/v1/p4runtime.pb.h" #include "p4_fuzzer/fuzzer.pb.h" -#include "p4_fuzzer/mutation.h" #include "p4_fuzzer/test_utils.h" -#include "p4_pdpi/ir.h" #include "p4_pdpi/ir.pb.h" -#include "p4_pdpi/pd.h" -#include "sai_p4/instantiations/google/instantiations.h" -#include "sai_p4/instantiations/google/sai_p4info.h" namespace p4_fuzzer { namespace { using ::gutil::EqualsProto; +using ::testing::AnyOfArray; +using ::testing::Not; TEST(FuzzUtilTest, SetUnusedBitsToZeroInThreeBytes) { std::string data("\xff\xff\xff", 3); @@ -279,6 +279,90 @@ TEST(FuzzUtilTest, FuzzWriteRequestRespectMaxBatchSize) { } } +TEST(FuzzUtilTest, FuzzWriteRequestRespectsDisallowList) { + FuzzerTestState fuzzer_state = ConstructStandardFuzzerTestState(); + fuzzer_state.config.disabled_fully_qualified_names = { + "ingress.id_test_table", "ingress.exact_table", "ingress.ternary_table"}; + + absl::flat_hash_set disallowed_ids; + for (const auto& path : fuzzer_state.config.disabled_fully_qualified_names) { + std::vector parts = absl::StrSplit(path, '.'); + ASSERT_OK_AND_ASSIGN( + const pdpi::IrTableDefinition& table, + gutil::FindOrStatus(fuzzer_state.config.info.tables_by_name(), + parts[parts.size() - 1])); + disallowed_ids.insert(table.preamble().id()); + } + + for (int i = 0; i < 1000; i++) { + AnnotatedWriteRequest request = + FuzzWriteRequest(&fuzzer_state.gen, fuzzer_state.config, + fuzzer_state.switch_state, /*max_batch_size=*/1); + if (request.updates_size() > 0) { + EXPECT_THAT(request.updates(0).pi().entity().table_entry().table_id(), + Not(AnyOfArray(disallowed_ids))); + } + } +} + +TEST(FuzzUtilTest, FuzzValidTableEntryRespectsDisallowList) { + FuzzerTestState fuzzer_state = ConstructStandardFuzzerTestState(); + fuzzer_state.config.disabled_fully_qualified_names = { + "ingress.ternary_table.ipv6_upper_64_bits", + "ingress.ternary_table.normal", + "ingress.ternary_table.mac", + "ingress.ternary_table.unsupported_field", + }; + + ASSERT_OK_AND_ASSIGN( + const pdpi::IrTableDefinition& ternary_table, + gutil::FindOrStatus(fuzzer_state.config.info.tables_by_name(), + "ternary_table")); + + absl::flat_hash_set disallowed_ids; + for (const auto& path : fuzzer_state.config.disabled_fully_qualified_names) { + std::vector parts = absl::StrSplit(path, '.'); + ASSERT_OK_AND_ASSIGN( + const pdpi::IrMatchFieldDefinition& match, + gutil::FindOrStatus(ternary_table.match_fields_by_name(), + parts[parts.size() - 1])); + disallowed_ids.insert(match.match_field().id()); + } + + for (int i = 0; i < 1000; i++) { + ASSERT_OK_AND_ASSIGN( + p4::v1::TableEntry entry, + FuzzValidTableEntry(&fuzzer_state.gen, fuzzer_state.config, + fuzzer_state.switch_state, + ternary_table.preamble().id())); + for (const auto& match : entry.match()) { + EXPECT_THAT(match.field_id(), Not(AnyOfArray(disallowed_ids))); + } + } +} + +TEST(FuzzUtilTest, FuzzActionRespectsDisallowList) { + FuzzerTestState fuzzer_state = ConstructStandardFuzzerTestState(); + ASSERT_OK_AND_ASSIGN( + pdpi::IrActionDefinition do_thing_action, + gutil::FindOrStatus(fuzzer_state.config.info.actions_by_name(), + "do_thing_1")); + fuzzer_state.config.disabled_fully_qualified_names = { + do_thing_action.preamble().name()}; + + ASSERT_OK_AND_ASSIGN( + const pdpi::IrTableDefinition& id_test_table, + gutil::FindOrStatus(fuzzer_state.config.info.tables_by_name(), + "id_test_table")); + + for (int i = 0; i < 1000; i++) { + ASSERT_OK_AND_ASSIGN(p4::v1::TableAction action, + FuzzAction(&fuzzer_state.gen, fuzzer_state.config, + fuzzer_state.switch_state, id_test_table)); + EXPECT_NE(action.action().action_id(), do_thing_action.preamble().id()); + } +} + // TODO: Add a direct test for FuzzValue that either sometimes // generates something for non-standard match fields, or, if that is never // correct, makes sure it still works with that possibility removed. diff --git a/p4_fuzzer/fuzzer_config.h b/p4_fuzzer/fuzzer_config.h index 1e799c87..a1159895 100644 --- a/p4_fuzzer/fuzzer_config.h +++ b/p4_fuzzer/fuzzer_config.h @@ -14,6 +14,12 @@ #ifndef GOOGLE_P4_FUZZER_FUZZER_CONFIG_H_ #define GOOGLE_P4_FUZZER_FUZZER_CONFIG_H_ +#include + +#include "absl/container/btree_set.h" +#include "absl/container/flat_hash_set.h" +#include "p4/v1/p4runtime.pb.h" +#include "p4_fuzzer/table_entry_key.h" #include "p4_pdpi/ir.pb.h" namespace p4_fuzzer { @@ -25,8 +31,34 @@ struct FuzzerConfig { std::vector ports; // The set of valid QOS queues. std::vector qos_queues; + // The set of tables where the fuzzer should treat their resource guarantees + // as hard limits rather than trying to go above them. If there are + // limitations or bugs on the switch causing it to behave incorrectly when the + // resource guarantees of particular tables are exceeded, this list can be + // used to allow the fuzzer to produce interesting results in spite of this + // shortcoming. + // This is a btree_set to ensure a deterministic ordering. + absl::btree_set + tables_for_which_to_not_exceed_resource_guarantees; + // Fully qualified names of tables, actions, or match fields to skip during + // fuzzing. Match field names should be prepended with the relevant table name + // to uniquely identify them. + // Users should ensure that any set that makes it impossible to generate a + // valid table entry for a particular table contains the table itself. + // TODO: Check the property above instead. + absl::flat_hash_set disabled_fully_qualified_names; // The P4RT role the fuzzer should use. std::string role; + // The probability of performing a mutation on a given table entry. + float mutate_update_probability; + // A function for masking inequalities (due to known bugs) between entries + // with the same TableEntryKey on the switch and in the fuzzer. + std::optional< + std::function> + TreatAsEqualDuringReadDueToKnownBug; + // Controls whether empty ActionProfile one-shots should be generated. + bool no_empty_action_profile_groups = false; + }; } // namespace p4_fuzzer diff --git a/p4_fuzzer/mutation.cc b/p4_fuzzer/mutation.cc index 7957b56b..165258c0 100644 --- a/p4_fuzzer/mutation.cc +++ b/p4_fuzzer/mutation.cc @@ -18,6 +18,7 @@ #include "gutil/collections.h" #include "p4/v1/p4runtime.pb.h" #include "p4_fuzzer/fuzz_util.h" +#include "p4_pdpi/internal/ordered_map.h" namespace p4_fuzzer { @@ -37,6 +38,44 @@ uint32_t UniformNotFromList(BitGen* gen, const std::vector& list) { return choice; } + +// Returns the list of all table IDs in the underlying P4 program. +const std::vector AllTableIds(const FuzzerConfig& config) { + std::vector table_ids; + + for (auto& [table_id, table_def] : Ordered(config.info.tables_by_id())) { + table_ids.push_back(table_id); + } + + return table_ids; +} + +// Returns the list of all action IDs in the underlying P4 program. +const std::vector AllActionIds(const FuzzerConfig& config) { + std::vector action_ids; + + for (auto& [action_id, action_def] : Ordered(config.info.actions_by_id())) { + action_ids.push_back(action_id); + } + + return action_ids; +} + +// Returns the list of all match field IDs in the underlying P4 program for +// table with id table_id. +const std::vector AllMatchFieldIds(const FuzzerConfig& config, + const uint32_t table_id) { + std::vector match_ids; + + for (auto& [match_id, match_def] : + Ordered(gutil::FindOrDie(config.info.tables_by_id(), table_id) + .match_fields_by_id())) { + match_ids.push_back(match_id); + } + + return match_ids; +} + } // namespace absl::Status MutateInvalidMatchFieldId(BitGen* gen, TableEntry* entry, @@ -147,7 +186,8 @@ absl::Status MutateInvalidTableImplementation(BitGen* gen, TableEntry* entry, *entry->mutable_action()->mutable_action(), FuzzAction( gen, config, switch_state, - ChooseNonDefaultActionRef(gen, config, ir_table_info).action())); + UniformFromSpan(gen, AllValidActions(config, ir_table_info)) + .action())); break; } diff --git a/p4_fuzzer/switch_state.cc b/p4_fuzzer/switch_state.cc index 9e857ff6..4597bb53 100644 --- a/p4_fuzzer/switch_state.cc +++ b/p4_fuzzer/switch_state.cc @@ -14,36 +14,76 @@ #include "p4_fuzzer/switch_state.h" #include +#include +#include #include +#include #include #include #include #include "absl/algorithm/container.h" #include "absl/container/btree_set.h" +#include "absl/container/flat_hash_map.h" #include "absl/status/status.h" #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "glog/logging.h" +#include "google/protobuf/util/message_differencer.h" #include "gutil/collections.h" +#include "gutil/proto.h" #include "gutil/status.h" #include "p4/config/v1/p4info.pb.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/internal/ordered_map.h" +#include "p4_pdpi/ir.h" #include "p4_pdpi/ir.pb.h" namespace p4_fuzzer { using ::gutil::FindOrDie; +using ::gutil::PrintTextProto; using ::p4::v1::TableEntry; using ::p4::v1::Update; using ::pdpi::IrP4Info; using ::pdpi::IrTableEntry; +/*absl::StatusOr CanonicalizeTableEntry(const IrP4Info& info, + const TableEntry& entry, + bool key_only) { + ASSIGN_OR_RETURN(IrTableEntry ir_entry, + pdpi::PiTableEntryToIr(info, entry, key_only), + _ << "Could not canonicalize: PiToIr Error\n" + << entry.DebugString()); + ASSIGN_OR_RETURN(TableEntry canonical_entry, + IrTableEntryToPi(info, ir_entry, key_only), + _ << "Could not canonicalize: IrToPi Error\n" + << entry.DebugString()); + return canonical_entry; +}*/ + +absl::StatusOr CanonicalizeTableEntry(const IrP4Info& info, + const TableEntry& entry, + bool key_only) { + auto pdpi_options = pdpi::TranslationOptions{ + .key_only = key_only, + }; + ASSIGN_OR_RETURN(IrTableEntry ir_entry, + pdpi::PiTableEntryToIr(info, entry, pdpi_options), + _ << "Could not canonicalize: PiToIr Error\n" + << entry.DebugString()); + ASSIGN_OR_RETURN(TableEntry canonical_entry, + IrTableEntryToPi(info, ir_entry, pdpi_options), + _ << "Could not canonicalize: IrToPi Error\n" + << entry.DebugString()); + return canonical_entry; +} + SwitchState::SwitchState(IrP4Info ir_p4info) : ir_p4info_(std::move(ir_p4info)) { for (auto& [table_id, table] : ir_p4info_.tables_by_id()) { tables_[table_id] = TableEntries(); + canonical_tables_[table_id] = TableEntries(); } } @@ -108,8 +148,33 @@ std::vector SwitchState::GetTableEntries( return result; } -absl::optional SwitchState::GetTableEntry(TableEntry entry) const { - auto table = FindOrDie(tables_, entry.table_id()); +std::vector SwitchState::GetCanonicalTableEntries( + const uint32_t table_id) const { + std::vector result; + + for (const auto& [key, entry] : FindOrDie(canonical_tables_, table_id)) { + result.push_back(entry); + } + + return result; +} + +std::optional SwitchState::GetTableEntry( + const TableEntry& entry) const { + const TableEntries& table = FindOrDie(tables_, entry.table_id()); + + if (auto table_iter = table.find(pdpi::TableEntryKey(entry)); + table_iter != table.end()) { + auto [table_key, table_entry] = *table_iter; + return table_entry; + } + + return absl::nullopt; +} + +std::optional SwitchState::GetCanonicalTableEntry( + const TableEntry& entry) const { + const TableEntries& table = FindOrDie(canonical_tables_, entry.table_id()); if (auto table_iter = table.find(pdpi::TableEntryKey(entry)); table_iter != table.end()) { @@ -124,40 +189,97 @@ absl::Status SwitchState::ApplyUpdate(const Update& update) { const int table_id = update.entity().table_entry().table_id(); auto& table = FindOrDie(tables_, table_id); + auto& canonical_table = FindOrDie(canonical_tables_, table_id); const TableEntry& table_entry = update.entity().table_entry(); + // TODO: PDPI IR Update translation currently does not properly + // ignore non-key fields on DELETE updates. Therefore, information to ignore + // non-key fields is explitcitly passed for canonicalization. + ASSIGN_OR_RETURN( + const TableEntry& canonical_table_entry, + CanonicalizeTableEntry(ir_p4info_, table_entry, + /*key_only=*/update.type() == Update::DELETE)); switch (update.type()) { case Update::INSERT: { auto [iter, not_present] = table.insert(/*value=*/{pdpi::TableEntryKey(table_entry), table_entry}); + auto [canonical_iter, canonical_not_present] = + canonical_table.insert(/*value=*/{ + pdpi::TableEntryKey(canonical_table_entry), canonical_table_entry}); + + if (not_present != canonical_not_present) { + return gutil::InternalErrorBuilder() + << "Standard Table and Canonical Table out of sync. Entry " + << (not_present ? "not present" : "present") + << " in Standard Table but " + << (canonical_not_present ? "not present" : "present") + << " in Canonical Table.\n" + << "Offending Entry Update\n" + << update.DebugString(); + } + if (!not_present) { return gutil::InvalidArgumentErrorBuilder() << "Cannot install the same table entry multiple times. Update: " << update.DebugString(); } + break; } case Update::DELETE: { - if (tables_[table_id].erase(pdpi::TableEntryKey(table_entry)) != 1) { + int entries_erased = tables_[table_id].erase(pdpi::TableEntryKey(table_entry)); + int canonical_entries_erased = canonical_tables_[table_id].erase( + pdpi::TableEntryKey(canonical_table_entry)); + + if (entries_erased != canonical_entries_erased) { + return gutil::InternalErrorBuilder() + << "Standard Table and Canonical Table out of sync. Entry " + << (entries_erased == 0 ? "not present" : "present") + << " in Standard Table but " + << (canonical_entries_erased == 0 ? "not present" : "present") + << " in Canonical Table.\n" + << "Offending Update\n" + << update.DebugString(); + } + + if (entries_erased != 1) { return gutil::InvalidArgumentErrorBuilder() << "Cannot erase non-existent table entries. Update: " << update.DebugString(); } + break; } case Update::MODIFY: { - auto [iter, not_present] = - table.insert(/*value=*/{pdpi::TableEntryKey(table_entry), table_entry}); + auto [iter, not_present] = table.insert_or_assign( + /*k=*/pdpi::TableEntryKey(table_entry), /*obj=*/table_entry); + + auto [canonical_iter, canonical_not_present] = + canonical_table.insert_or_assign(/*k=*/ + pdpi::TableEntryKey(canonical_table_entry), + /*obj=*/canonical_table_entry); + + if (not_present != canonical_not_present) { + return gutil::InternalErrorBuilder() + << "Standard Table and Canonical Table out of sync. Entry " + << (not_present ? "not present" : "present") + << " in Standard Table but " + << (canonical_not_present ? "not present" : "present") + << " in Canonical Table.\n" + << "Offending Update\n" + << update.DebugString(); + } if (not_present) { return gutil::InvalidArgumentErrorBuilder() << "Cannot modify a non-existing update. Update: " << update.DebugString(); } + break; } @@ -173,12 +295,22 @@ absl::Status SwitchState::SetTableEntries( for (const p4::v1::TableEntry& entry : table_entries) { auto table = tables_.find(entry.table_id()); + auto canonical_table = canonical_tables_.find(entry.table_id()); if (table == tables_.end()) { return gutil::InvalidArgumentErrorBuilder() << "table entry with unknown table ID '" << entry.table_id() << "'"; } + if (canonical_table == canonical_tables_.end()) { + return gutil::InvalidArgumentErrorBuilder() + << "canonical table entry with unknown table ID '" + << entry.table_id() << "'"; + } + ASSIGN_OR_RETURN(TableEntry canonical_entry, + CanonicalizeTableEntry(ir_p4info_, entry, false)); table->second.insert({pdpi::TableEntryKey(entry), entry}); + canonical_table->second.insert( + {pdpi::TableEntryKey(canonical_entry), canonical_entry}); } return absl::OkStatus(); @@ -276,5 +408,178 @@ absl::btree_set SwitchState::GetIdsForMatchField( return result; } +absl::Status SwitchState::CheckConsistency() const { + if (tables_.size() != canonical_tables_.size()) { + return absl::InternalError( + absl::StrFormat("Size of `tables_` and `canonical_tables_` is " + "different. `tables_`: '%d' `canonical_tables_`: '%d'", + tables_.size(), canonical_tables_.size())); + } + + // Ensure that every `table_id` in `tables_` is also present in + // `canonical_tables_` and that the corresponding tables are the same size. + for (const auto& [table_id, table] : tables_) { + if (!canonical_tables_.contains(table_id)) { + return absl::InternalError(absl::StrFormat( + "`canonical_tables_` is missing table with id '%d'", table_id)); + } + + const TableEntries& canonical_table = canonical_tables_.at(table_id); + + if (canonical_table.size() != table.size()) { + return absl::InternalError(absl::StrFormat( + "Number of standard entries differs from number of canonical entries " + "in table with id %d. Standard Entries: %d Canonical Entries: %d", + table_id, table.size(), canonical_tables_.at(table_id).size())); + } + + // Ensure that every `table_entry` in a standard table has a corresponding + // `canonical_table_entry` in a canonical table. + for (const auto& [table_key, table_entry] : table) { + ASSIGN_OR_RETURN(TableEntry canonical_table_entry, + CanonicalizeTableEntry(ir_p4info_, table_entry, false)); + + std::optional fetched_entry = + GetCanonicalTableEntry(canonical_table_entry); + if (!fetched_entry.has_value()) { + return absl::InternalError(absl::StrFormat( + "Table entry %s is missing corresponding canonical table entry", + table_entry.DebugString())); + } + + google::protobuf::util::MessageDifferencer differ; + differ.TreatAsSet(TableEntry::descriptor()->FindFieldByName("match")); + if (!gutil::ProtoEqual(canonical_table_entry, *fetched_entry, differ)) { + return absl::InternalError(absl::StrFormat( + "Stored canonical entry differs from expected canonical entry\n " + "Stored Entry: %s Expected Entry: %s", + fetched_entry->DebugString(), canonical_table_entry.DebugString())); + } + } + } + return absl::OkStatus(); +} + +absl::Status SwitchState::AssertEntriesAreEqualToState( + const std::vector& switch_entries, + std::optional> + TreatAsEqualDueToKnownBug) const { + std::string status_message = ""; + + // Condition that requires a search for unique entries in switchstate. + bool entry_unique_to_switch = false; + + if (switch_entries.size() != GetNumTableEntries()) { + absl::StrAppendFormat(&status_message, + "Number of entries on switch does not match number " + "of entries in Fuzzer\n" + "Entries on switch: %d\n" + "Entries in Fuzzer: %d\n", + switch_entries.size(), GetNumTableEntries()); + } + + // Message differencer for PI Table Entries. + google::protobuf::util::MessageDifferencer differ; + differ.TreatAsSet( + p4::v1::TableEntry().GetDescriptor()->FindFieldByName("match")); + + // Message differencer for IR Table Entries. + google::protobuf::util::MessageDifferencer ir_differ; + ir_differ.TreatAsSet( + IrTableEntry().GetDescriptor()->FindFieldByName("matches")); + + std::optional fuzzer_entry; + for (const auto& switch_entry : switch_entries) { + fuzzer_entry = GetCanonicalTableEntry(switch_entry); + + // Is there an entry on the switch that does not exist in the Fuzzer? + if (!fuzzer_entry.has_value()) { + entry_unique_to_switch = true; + ASSIGN_OR_RETURN(IrTableEntry ir_entry, + pdpi::PiTableEntryToIr(ir_p4info_, switch_entry)); + absl::StrAppend( + &status_message, + "The following entry exists on switch but not in Fuzzer:\n", + PrintTextProto(ir_entry)); + continue; + } + + std::string differences = ""; + differ.ReportDifferencesToString(&differences); + std::string ir_differences = ""; + ir_differ.ReportDifferencesToString(&ir_differences); + + // Is there an entry with the same key on both the switch and in the Fuzzer, + // but they differ in other ways? + if (!differ.Compare(*fuzzer_entry, switch_entry)) { + ASSIGN_OR_RETURN(IrTableEntry ir_switch_entry, + pdpi::PiTableEntryToIr(ir_p4info_, switch_entry)); + ASSIGN_OR_RETURN(IrTableEntry ir_fuzzer_entry, + pdpi::PiTableEntryToIr(ir_p4info_, *fuzzer_entry)); + + if (ir_differ.Compare(ir_fuzzer_entry, ir_switch_entry)) { + return absl::InternalError(absl::StrFormat( + "PI 'entries' were not equal but IR 'entries' were\n" + "IR Entry\n" + "%s" + "Differences in PI 'entries'\n" + "%s\n" + "Switch PI Entry\n" + "%s" + "Fuzzer PI Entry\n" + "%s", + PrintTextProto(ir_switch_entry), differences, + PrintTextProto(switch_entry), PrintTextProto(*fuzzer_entry))); + + // If there is a difference, are known bugs being masked and is the + // difference caused by a known bug? + } else if (!TreatAsEqualDueToKnownBug.has_value() || + !(*TreatAsEqualDueToKnownBug)(ir_fuzzer_entry, + ir_switch_entry)) { + absl::StrAppendFormat( + &status_message, + "Entry exists in both switch and Fuzzer, but is different:\n" + "%s\n" + "Entry on switch:\n" + "%s" + "Entry in Fuzzer:\n" + "%s", + ir_differences, PrintTextProto(ir_switch_entry), + PrintTextProto(ir_fuzzer_entry)); + } + } + } + + // Are there entries in the Fuzzer that do not exist on the switch? + if (switch_entries.size() != GetNumTableEntries() || entry_unique_to_switch) { + absl::flat_hash_map fuzzer_state_copy = + canonical_tables_; + + // Removes all entries from the `fuzzer_state_copy` that exist on the + // switch. + for (const auto& switch_entry : switch_entries) { + if (GetCanonicalTableEntry(switch_entry).has_value()) { + fuzzer_state_copy.at(switch_entry.table_id()) + .erase(pdpi::TableEntryKey(switch_entry)); + } + } + + // All remaining entries exist only in the fuzzer. + for (const auto& [table_id, table] : fuzzer_state_copy) { + for (const auto& [key, fuzzer_entry] : table) { + ASSIGN_OR_RETURN(IrTableEntry ir_entry, + pdpi::PiTableEntryToIr(ir_p4info_, fuzzer_entry)); + absl::StrAppend( + &status_message, + "The following entry exists in Fuzzer but not on switch:\n", + PrintTextProto(ir_entry)); + } + } + } + + if (status_message.empty()) return absl::OkStatus(); + + return absl::FailedPreconditionError(status_message); +} } // namespace p4_fuzzer diff --git a/p4_fuzzer/switch_state.h b/p4_fuzzer/switch_state.h index 582b1a19..c819c365 100644 --- a/p4_fuzzer/switch_state.h +++ b/p4_fuzzer/switch_state.h @@ -15,8 +15,11 @@ #define P4_FUZZER_SWITCH_STATE_H_ #include +#include +#include #include #include +#include #include "absl/container/btree_map.h" #include "absl/container/btree_set.h" @@ -40,6 +43,14 @@ namespace p4_fuzzer { // TableEntryKey() here is the constructor for the class TableEntryKey. using TableEntries = absl::btree_map; +// Returns the canonical form of `entry` according to the P4 Runtime Spec +// https://s3-us-west-2.amazonaws.com/p4runtime/ci/main/P4Runtime-Spec.html#sec-bytestrings. +// TODO: Canonical form is achieved by performing an IR roundtrip +// translation. This ties correctness to IR functionality. Local +// canonicalization would be preferred. +absl::StatusOr CanonicalizeTableEntry( + const pdpi::IrP4Info& info, const p4::v1::TableEntry& entry, bool key_only); + // Tracks the state of a switch, with methods to apply updates or query the // current state. The class assumes all calls are valid (e.g table_ids must all // exist). Crashes if that is not the case. @@ -68,6 +79,10 @@ class SwitchState { std::vector GetTableEntries( const uint32_t table_id) const; + // Returns all table entries in a given canonical table. + std::vector GetCanonicalTableEntries( + const uint32_t table_id) const; + // Returns the number of table entries in a given table. int64_t GetNumTableEntries(const uint32_t table_id) const; @@ -76,8 +91,13 @@ class SwitchState { // Returns the current state of a table entry (or nullopt if it is not // present). Only the uniquely identifying fields of entry are considered. - absl::optional GetTableEntry( - p4::v1::TableEntry entry) const; + std::optional GetTableEntry( + const p4::v1::TableEntry& entry) const; + + // Returns the current state of a canonical table entry (or nullopt if it is + // not present). Only the uniquely identifying fields of entry are considered. + std::optional GetCanonicalTableEntry( + const p4::v1::TableEntry& entry) const; // Returns the list of all non-const table IDs in the underlying P4 program. const std::vector AllTableIds() const; @@ -104,9 +124,33 @@ class SwitchState { pdpi::IrP4Info GetIrP4Info() const { return ir_p4info_; } + // Used in testing to check that SwitchState is always consistent by: + // - Ensuring that the standard and canonical table states are in sync. + absl::Status CheckConsistency() const; + + // Returns OK if the set of elements in `switch_entries` is equal to + // the set of all canonical entries in SwitchState. Returns + // FailedPreconditionError if there are differences. Status message records 3 + // types of differences: + // 1. Entry is in `switch_entries`, but not in fuzzer state. + // 2. Entry key is present in both, but value is different. + // 3. Entry is not in `switch_entries`, but in fuzzer state. + // Returns InvalidArgumentError if any difference cannot be translated to an + // IR representation. + // An optional functor `TreatAsEqualDueToKnownBug` can be used to mask known + // bugs when comparing entries with the same `TableEntryKey`. + absl::Status AssertEntriesAreEqualToState( + const std::vector& switch_entries, + std::optional> + TreatAsEqualDueToKnownBug = std::nullopt) const; + private: // A map from table ids to the entries they store. + // Invariant: An entry, `e`, is represented in `tables_` <=> canonical(e) is + // represented in `canonical_tables_`. absl::flat_hash_map tables_; + absl::flat_hash_map canonical_tables_; pdpi::IrP4Info ir_p4info_; }; diff --git a/p4_fuzzer/switch_state_assert_entry_equality_test.expected.output b/p4_fuzzer/switch_state_assert_entry_equality_test.expected.output new file mode 100644 index 00000000..73ec312a --- /dev/null +++ b/p4_fuzzer/switch_state_assert_entry_equality_test.expected.output @@ -0,0 +1,169 @@ +######################################################### +### Test Case: Switch Has Unique Entry +######################################################### + +=== Switch Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + +=== Fuzzer Entries === + +=== Mask Function === +No mask function was used + +=== Test Output === +FAILED_PRECONDITION: Number of entries on switch does not match number of entries in Fuzzer +Entries on switch: 1 +Entries in Fuzzer: 0 +The following entry exists on switch but not in Fuzzer: +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + + +######################################################### +### Test Case: Fuzzer Has Unique Entry +######################################################### + +=== Switch Entries === + +=== Fuzzer Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + +=== Mask Function === +No mask function was used + +=== Test Output === +FAILED_PRECONDITION: Number of entries on switch does not match number of entries in Fuzzer +Entries on switch: 0 +Entries in Fuzzer: 1 +The following entry exists in Fuzzer but not on switch: +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + + +######################################################### +### Test Case: Switch and Fuzzer entry have same key but different value +######################################################### + +=== Switch Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + +=== Fuzzer Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} +controller_metadata: "Am cookie, much wow" + +=== Mask Function === +No mask function was used + +=== Test Output === +FAILED_PRECONDITION: Entry exists in both switch and Fuzzer, but is different: +deleted: controller_metadata: "Am cookie, much wow" + +Entry on switch: +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} +Entry in Fuzzer: +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} +controller_metadata: "Am cookie, much wow" + + +######################################################### +### Test Case: Switch and Fuzzer have same entries +######################################################### + +=== Switch Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + +=== Fuzzer Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + +=== Mask Function === +No mask function was used + +=== Test Output === +OK: + +######################################################### +### Test Case: Missing metadata is ignored due to mask function +######################################################### + +=== Switch Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} + +=== Fuzzer Entries === +table_name: "golden_table" +matches { + name: "field1" + exact { + hex_str: "0xbe0a0bed" + } +} +controller_metadata: "Am cookie, much wow" + +=== Mask Function === +Mask ignores metadata field + +=== Test Output === +OK: diff --git a/p4_fuzzer/switch_state_assert_entry_equality_test_runner.cc b/p4_fuzzer/switch_state_assert_entry_equality_test_runner.cc new file mode 100644 index 00000000..8e9ce3b9 --- /dev/null +++ b/p4_fuzzer/switch_state_assert_entry_equality_test_runner.cc @@ -0,0 +1,233 @@ +#include +#include +#include +#include +#include + +#include "absl/status/status.h" +#include "absl/status/statusor.h" +#include "absl/strings/substitute.h" +#include "absl/types/span.h" +#include "google/protobuf/util/message_differencer.h" +#include "gutil/collections.h" +#include "gutil/testing.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4/v1/p4runtime.pb.h" +#include "p4_fuzzer/switch_state.h" +#include "p4_pdpi/ir.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_pdpi/testing/test_p4info.h" + +namespace p4_fuzzer { +namespace { + +using ::p4::config::v1::P4Info; +using ::p4::config::v1::Preamble; +using ::p4::config::v1::Table; +using ::p4::v1::TableEntry; +using ::pdpi::CreateIrP4Info; +using ::pdpi::IrP4Info; +using ::pdpi::IrTableEntry; + +constexpr char kGoldenName[] = "golden_table"; + +IrP4Info GetIrP4Info() { + P4Info info; + + Table* spam_table = info.add_tables(); + Preamble* preamble = spam_table->mutable_preamble(); + preamble->set_id(1); + preamble->set_alias(kGoldenName); + p4::config::v1::MatchField* match_field = + spam_table->mutable_match_fields()->Add(); + match_field->set_id(1); + match_field->set_name("field1"); + match_field->set_bitwidth(32); + match_field->set_match_type(p4::config::v1::MatchField::EXACT); + + return CreateIrP4Info(info).value(); +} + +struct TestCase { + std::string description; + std::vector switch_entries; + std::vector fuzzer_entries; + std::string mask_function_description; + std::optional> mask_function; +}; + +std::vector TestCases() { + std::vector test_cases; + + test_cases.emplace_back(TestCase{ + .description = "Switch Has Unique Entry", + .switch_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + )pb", + kGoldenName))}, + .fuzzer_entries = {}, + }); + + test_cases.emplace_back(TestCase{ + .description = "Fuzzer Has Unique Entry", + .switch_entries = {}, + .fuzzer_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + )pb", + kGoldenName))}, + }); + + test_cases.emplace_back(TestCase{ + .description = + "Switch and Fuzzer entry have same key but different value", + .switch_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + )pb", + kGoldenName))}, + .fuzzer_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + controller_metadata: "Am cookie, much wow" + )pb", + kGoldenName))}, + }); + + test_cases.emplace_back(TestCase{ + .description = "Switch and Fuzzer have same entries", + .switch_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + )pb", + kGoldenName))}, + .fuzzer_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + )pb", + kGoldenName))}, + }); + + test_cases.emplace_back(TestCase{ + .description = "Missing metadata is ignored due to mask function", + .switch_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + )pb", + kGoldenName))}, + .fuzzer_entries = {gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_name: "$0" + matches { + name: "field1" + exact { hex_str: "0xbe0a0bed" } + } + controller_metadata: "Am cookie, much wow" + )pb", + kGoldenName))}, + .mask_function_description = "Mask ignores metadata field", + .mask_function = + [](IrTableEntry a, IrTableEntry b) { + google::protobuf::util::MessageDifferencer differ; + differ.IgnoreField(IrTableEntry::descriptor()->FindFieldByName( + "controller_metadata")); + return differ.Compare(a, b); + }, + }); + + return test_cases; +} + +void PrintEntries(absl::Span entries) { + for (const auto& entry : entries) { + std::cout << gutil::PrintTextProto(entry); + } + std::cout << "\n"; +} + +absl::StatusOr> IrToPiVector( + absl::Span ir_entries, const IrP4Info& ir_info) { + std::vector pi_entries; + for (const auto& ir_entry : ir_entries) { + ASSIGN_OR_RETURN(p4::v1::TableEntry pi_entry, + pdpi::IrTableEntryToPi(ir_info, ir_entry)); + pi_entries.push_back(pi_entry); + } + return pi_entries; +} + +absl::Status main() { + IrP4Info ir_info = GetIrP4Info(); + SwitchState state(ir_info); + absl::Status status; + + for (const auto& test : TestCases()) { + state.ClearTableEntries(); + + ASSIGN_OR_RETURN(std::vector pi_fuzzer_entries, + IrToPiVector(test.fuzzer_entries, ir_info)); + ASSIGN_OR_RETURN(std::vector pi_switch_entries, + IrToPiVector(test.switch_entries, ir_info)); + + RETURN_IF_ERROR(state.SetTableEntries(pi_fuzzer_entries)); + RETURN_IF_ERROR(state.CheckConsistency()); + + std::cout << "#########################################################\n" + << "### Test Case: " << test.description << "\n" + << "#########################################################\n\n" + << "=== Switch Entries ===\n"; + PrintEntries(test.switch_entries); + std::cout << "=== Fuzzer Entries ===\n"; + PrintEntries(test.fuzzer_entries); + std::cout << "=== Mask Function ===\n"; + if (test.mask_function.has_value()) { + std::cout << test.mask_function_description << "\n\n"; + } else { + std::cout << "No mask function was used\n\n"; + } + std::cout << "=== Test Output ===\n" + << gutil::StableStatusToString(state.AssertEntriesAreEqualToState( + pi_switch_entries, test.mask_function)) + << "\n"; + } + return absl::OkStatus(); +} + +} // namespace +} // namespace p4_fuzzer + +int main() { + absl::Status status = p4_fuzzer::main(); + if (!status.ok()) { + std::cout << status; + } +} diff --git a/p4_fuzzer/switch_state_test.cc b/p4_fuzzer/switch_state_test.cc index 980ed15c..b9ddf1aa 100644 --- a/p4_fuzzer/switch_state_test.cc +++ b/p4_fuzzer/switch_state_test.cc @@ -18,9 +18,11 @@ #include "absl/status/status.h" #include "absl/strings/str_cat.h" #include "absl/strings/substitute.h" +#include "absl/types/optional.h" #include "glog/logging.h" #include "gtest/gtest.h" #include "gutil/collections.h" +#include "gutil/proto.h" #include "gutil/proto_matchers.h" #include "gutil/status_matchers.h" #include "gutil/testing.h" @@ -34,6 +36,7 @@ namespace p4_fuzzer { namespace { +using ::gutil::EqualsProto; using ::p4::config::v1::P4Info; using ::p4::config::v1::Preamble; using ::p4::config::v1::Table; @@ -41,11 +44,48 @@ using ::p4::v1::TableEntry; using ::p4::v1::Update; using ::pdpi::CreateIrP4Info; using ::pdpi::IrP4Info; -using ::testing::StrEq; +using ::testing::Not; +using ::testing::Optional; // All P4Runtime table IDs must have their most significant byte equal to this // value. constexpr uint32_t kTableIdMostSignificantByte = 0x02'00'00'00; +constexpr uint32_t kBareTable1 = 1; +constexpr uint32_t kBareTable2 = 2; +constexpr uint32_t kSpamTableId = 41; +constexpr uint32_t kEggTableId = 42; + +IrP4Info GetIrP4Info() { + P4Info info; + + Table* bare_table_1 = info.add_tables(); + Preamble* preamble = bare_table_1->mutable_preamble(); + preamble->set_id(kBareTable1); + preamble->set_alias("bare_table_1"); + + Table* bare_table_2 = info.add_tables(); + preamble = bare_table_2->mutable_preamble(); + preamble->set_id(kBareTable2); + preamble->set_alias("bare_table_2"); + + Table* spam_table = info.add_tables(); + preamble = spam_table->mutable_preamble(); + preamble->set_id(kSpamTableId); + preamble->set_alias("spam_table"); + p4::config::v1::MatchField* match_field = + spam_table->mutable_match_fields()->Add(); + match_field->set_id(1); + match_field->set_name("field1"); + match_field->set_bitwidth(32); + match_field->set_match_type(p4::config::v1::MatchField::EXACT); + + Table* egg_table = info.add_tables(); + preamble = egg_table->mutable_preamble(); + preamble->set_id(kEggTableId); + preamble->set_alias("egg_table"); + + return CreateIrP4Info(info).value(); +} TEST(SwitchStateTest, TableEmptyTrivial) { IrP4Info info; @@ -66,38 +106,30 @@ TEST(SwitchStateTest, TableEmptyFromP4Info) { } TEST(SwitchStateTest, RuleInsert) { - P4Info info; - Table* ptable = info.add_tables(); - Preamble* preamble = ptable->mutable_preamble(); - preamble->set_id(42); - preamble->set_alias("Spam"); - - ptable = info.add_tables(); - preamble = ptable->mutable_preamble(); - preamble->set_id(43); - preamble->set_alias("Eggs"); - - IrP4Info ir_info = CreateIrP4Info(info).value(); - - SwitchState state(ir_info); + SwitchState state(GetIrP4Info()); Update update; update.set_type(Update::INSERT); TableEntry* entry = update.mutable_entity()->mutable_table_entry(); - entry->set_table_id(42); + entry->set_table_id(kBareTable1); ASSERT_OK(state.ApplyUpdate(update)); EXPECT_FALSE(state.AllTablesEmpty()); - EXPECT_FALSE(state.IsTableEmpty(42)); - EXPECT_TRUE(state.IsTableEmpty(43)); + EXPECT_FALSE(state.IsTableEmpty(kBareTable1)); + EXPECT_TRUE(state.IsTableEmpty(kBareTable2)); + + EXPECT_EQ(state.GetNumTableEntries(kBareTable1), 1); + EXPECT_EQ(state.GetNumTableEntries(kBareTable2), 0); + + EXPECT_EQ(state.GetTableEntries(kBareTable1).size(), 1); + EXPECT_EQ(state.GetTableEntries(kBareTable2).size(), 0); - EXPECT_EQ(state.GetNumTableEntries(42), 1); - EXPECT_EQ(state.GetNumTableEntries(43), 0); + EXPECT_EQ(state.GetCanonicalTableEntries(kBareTable1).size(), 1); + EXPECT_EQ(state.GetCanonicalTableEntries(kBareTable2).size(), 0); - EXPECT_EQ(state.GetTableEntries(42).size(), 1); - EXPECT_EQ(state.GetTableEntries(43).size(), 0); + EXPECT_OK(state.CheckConsistency()); state.ClearTableEntries(); EXPECT_TRUE(state.AllTablesEmpty()); @@ -112,37 +144,120 @@ TEST(SwitchStateTest, ClearTableEntriesPreservesP4Info) { EXPECT_THAT(state.GetIrP4Info(), gutil::EqualsProto(p4info)); } -TEST(SwitchStateTest, RuleDelete) { - P4Info info; - Table* ptable = info.add_tables(); - Preamble* preamble = ptable->mutable_preamble(); - preamble->set_id(42); - preamble->set_alias("Spam"); +TEST(SwitchStateTest, RuleModify) { + SwitchState state(GetIrP4Info()); + + // Construct old_entry and new_entry. + TableEntry old_entry = gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_id: $0 + match { + field_id: 1 + exact { value: "\378\"" } + } + metadata: "cookie: 42" + )pb", + kSpamTableId)); + + TableEntry new_entry = old_entry; + new_entry.set_metadata("not_a_cookie"); + + // Set up SwitchState. + Update update; + update.set_type(Update::INSERT); + *update.mutable_entity()->mutable_table_entry() = old_entry; + + ASSERT_OK(state.ApplyUpdate(update)); - ptable = info.add_tables(); - preamble = ptable->mutable_preamble(); - preamble->set_id(43); - preamble->set_alias("Eggs"); + ASSERT_THAT(state.GetTableEntry(old_entry), + Optional(Not(EqualsProto(new_entry)))); - IrP4Info ir_info = CreateIrP4Info(info).value(); + // Modify SwitchState + update.set_type(Update::MODIFY); + update.mutable_entity()->mutable_table_entry()->set_metadata("not_a_cookie"); - SwitchState state(ir_info); + ASSERT_OK(state.ApplyUpdate(update)); + + ASSERT_THAT(state.GetTableEntry(new_entry), Optional(EqualsProto(new_entry))); + + ASSERT_OK(state.CheckConsistency()); +} + +TEST(SwitchStateTest, RuleDelete) { + SwitchState state(GetIrP4Info()); Update update; update.set_type(Update::INSERT); TableEntry* entry = update.mutable_entity()->mutable_table_entry(); - entry->set_table_id(42); + entry->set_table_id(kBareTable1); ASSERT_OK(state.ApplyUpdate(update)); + EXPECT_OK(state.CheckConsistency()); + update.set_type(Update::DELETE); ASSERT_OK(state.ApplyUpdate(update)); EXPECT_TRUE(state.AllTablesEmpty()); - EXPECT_EQ(state.GetNumTableEntries(42), 0); - EXPECT_EQ(state.GetTableEntries(42).size(), 0); + EXPECT_EQ(state.GetNumTableEntries(kBareTable1), 0); + EXPECT_EQ(state.GetTableEntries(kBareTable1).size(), 0); + EXPECT_EQ(state.GetCanonicalTableEntries(kBareTable1).size(), 0); + + EXPECT_OK(state.CheckConsistency()); +} + +TEST(SwitchStateTest, + NonCanonicalAndCanonicalEntriesAreProperlyStoredAndRetrieved) { + SwitchState state(GetIrP4Info()); + + // Construct non-canonical entry and its canonical counterpart. + TableEntry entry_in_update = gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_id: $0 + match { + field_id: 1 + exact { value: "\000\378\"" } + } + )pb", + kSpamTableId)); + + TableEntry canonicalized_entry = gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_id: $0 + match { + field_id: 1 + exact { value: "\378\"" } + } + )pb", + kSpamTableId)); + + // Check for correct canonicalization. + ASSERT_OK_AND_ASSIGN(TableEntry canonicalized_entry_in_update, + CanonicalizeTableEntry(GetIrP4Info(), entry_in_update, + /*key_only=*/false)); + ASSERT_THAT(canonicalized_entry_in_update, + gutil::EqualsProto(canonicalized_entry)); + + // Set up SwitchState. + Update update; + update.set_type(Update::INSERT); + *update.mutable_entity()->mutable_table_entry() = entry_in_update; + + ASSERT_OK(state.ApplyUpdate(update)); + + // Ensure that entry_in_update is stored in standard table. + ASSERT_FALSE(state.GetTableEntry(canonicalized_entry).has_value()); + ASSERT_THAT(state.GetTableEntry(entry_in_update), + Optional(EqualsProto(entry_in_update))); + + // Ensure that canonical entry is stored in canonical table. + ASSERT_FALSE(state.GetCanonicalTableEntry(entry_in_update).has_value()); + ASSERT_THAT(state.GetCanonicalTableEntry(canonicalized_entry), + testing::Optional(gutil::EqualsProto(canonicalized_entry))); + + ASSERT_OK(state.CheckConsistency()); } Update MakePiUpdate(const pdpi::IrP4Info& info, Update::Type type, @@ -155,5 +270,58 @@ Update MakePiUpdate(const pdpi::IrP4Info& info, Update::Type type, return *pi; } +TEST(SwitchStateTest, SetTableEntriesSetsTableEntries) { + SwitchState state(GetIrP4Info()); + + EXPECT_TRUE(state.AllTablesEmpty()); + + // Call SetTableEntries and ensure it indeed populates the correct tables. + std::vector entries; + entries.emplace_back() = // Entry #1 in table 1. + gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_id: $0 + match { + field_id: 1 + exact { value: "\378\"" } + } + )pb", + kSpamTableId)); + entries.emplace_back().set_table_id(kEggTableId); // Entry #1 in table 2. + entries.emplace_back() = // Entry #2 in table 1. + gutil::ParseProtoOrDie( + absl::Substitute(R"pb( + table_id: $0 + match { + field_id: 1 + exact { value: "\377\"" } + } + )pb", + kSpamTableId)); + ASSERT_OK(state.SetTableEntries(entries)) + << " with the following P4Info:\n " << state.GetIrP4Info().DebugString(); + EXPECT_EQ(state.GetNumTableEntries(kSpamTableId), 2); + EXPECT_EQ(state.GetNumTableEntries(kEggTableId), 1); + EXPECT_EQ(state.GetNumTableEntries(), 3); + + EXPECT_OK(state.CheckConsistency()); + + state.ClearTableEntries(); + EXPECT_EQ(state.GetNumTableEntries(kSpamTableId), 0); + EXPECT_EQ(state.GetNumTableEntries(kEggTableId), 0); + EXPECT_EQ(state.GetNumTableEntries(), 0); + EXPECT_TRUE(state.AllTablesEmpty()); + + EXPECT_OK(state.CheckConsistency()); +} + +TEST(SwitchStateTest, SetTableEntriesFailsForUnknownTableIds) { + SwitchState state(pdpi::GetTestIrP4Info()); + EXPECT_THAT( + state.SetTableEntries(std::vector{ + gutil::ParseProtoOrDie("table_id: 123456789")}), + gutil::StatusIs(absl::StatusCode::kInvalidArgument)); +} + } // namespace } // namespace p4_fuzzer diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index 407c073f..6b5da50f 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -35,6 +35,7 @@ cc_binary( ":parser", "//gutil:status", "//p4_symbolic/bmv2", + "//p4_symbolic/sai:parser", "//p4_symbolic/symbolic", "//p4_symbolic/util", "@com_google_absl//absl/flags:flag", diff --git a/p4_symbolic/ir/table_entries.cc b/p4_symbolic/ir/table_entries.cc index 38a64437..714b9266 100644 --- a/p4_symbolic/ir/table_entries.cc +++ b/p4_symbolic/ir/table_entries.cc @@ -18,13 +18,60 @@ #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "absl/strings/str_split.h" +#include "gutil/status.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/ir.h" +#include "p4_pdpi/ir.pb.h" #include "p4_symbolic/util/io.h" namespace p4_symbolic { namespace ir { +namespace { + +absl::Status UseFullyQualifiedTableName(const pdpi::IrP4Info &p4info, + pdpi::IrTableEntry &entry) { + auto &alias = entry.table_name(); + RET_CHECK(p4info.tables_by_name().count(alias) == 1) + << "where alias = '" << alias << "' and IR table entry =\n" + << entry.DebugString(); + auto &full_name = p4info.tables_by_name().at(alias).preamble().name(); + entry.set_table_name(full_name); + return absl::OkStatus(); +} + +absl::Status UseFullyQualifiedActionName(const pdpi::IrP4Info &p4info, + pdpi::IrActionInvocation &action) { + auto &alias = action.name(); + RET_CHECK(p4info.actions_by_name().count(alias) == 1) + << "where alias = '" << alias; + auto &full_name = p4info.actions_by_name().at(alias).preamble().name(); + action.set_name(full_name); + return absl::OkStatus(); +} + +absl::Status UseFullyQualifiedNamesInEntry(const pdpi::IrP4Info &info, + pdpi::IrTableEntry &entry) { + RETURN_IF_ERROR(UseFullyQualifiedTableName(info, entry)); + switch (entry.type_case()) { + case pdpi::IrTableEntry::kAction: + return UseFullyQualifiedActionName(info, *entry.mutable_action()); + case pdpi::IrTableEntry::kActionSet: + for (auto &action : *entry.mutable_action_set()->mutable_actions()) { + RETURN_IF_ERROR( + UseFullyQualifiedActionName(info, *action.mutable_action())); + } + return absl::OkStatus(); + default: + break; + } + return gutil::InvalidArgumentErrorBuilder() + << "unexpected or missing action in table entry: " + << entry.DebugString(); +} + +} // namespace + absl::StatusOr ParseTableEntries( const pdpi::IrP4Info &p4info, absl::Span entries) { @@ -34,22 +81,7 @@ absl::StatusOr ParseTableEntries( for (const p4::v1::TableEntry &pi_entry : entries) { ASSIGN_OR_RETURN(pdpi::IrTableEntry pdpi_entry, pdpi::PiTableEntryToIr(p4info, pi_entry)); - - // Replace table and action aliases with their respective full name. - const std::string &table_alias = pdpi_entry.table_name(); - const std::string &action_alias = pdpi_entry.action().name(); - - // Make sure both table and action referred to by entry exist. - RET_CHECK(p4info.tables_by_name().count(table_alias) == 1); - RET_CHECK(p4info.actions_by_name().count(action_alias) == 1); - - const std::string &table_name = - p4info.tables_by_name().at(table_alias).preamble().name(); - const std::string &action_name = - p4info.actions_by_name().at(action_alias).preamble().name(); - - pdpi_entry.mutable_action()->set_name(action_name); - pdpi_entry.set_table_name(table_name); + RETURN_IF_ERROR(UseFullyQualifiedNamesInEntry(p4info, pdpi_entry)); output[pdpi_entry.table_name()].push_back(pdpi_entry); } return output; diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc index 53cde49c..283afd1b 100644 --- a/p4_symbolic/main.cc +++ b/p4_symbolic/main.cc @@ -30,6 +30,7 @@ #include "gutil/status.h" #include "p4_symbolic/bmv2/bmv2.h" #include "p4_symbolic/parser.h" +#include "p4_symbolic/sai/parser.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/util/io.h" @@ -65,8 +66,17 @@ absl::Status ParseAndEvaluate() { // Evaluate program symbolically. ASSIGN_OR_RETURN( const std::unique_ptr &solver_state, - p4_symbolic::symbolic::EvaluateP4Pipeline( - dataplane, std::vector{0, 1}, hardcoded_parser)); + p4_symbolic::symbolic::EvaluateP4Pipeline(dataplane, + std::vector{0, 1})); + // Add constraints for parser. + if (hardcoded_parser) { + ASSIGN_OR_RETURN( + std::vector parser_constraints, + p4_symbolic::EvaluateSaiParser(solver_state->context.ingress_headers)); + for (auto &constraint : parser_constraints) { + solver_state->solver->add(constraint); + } + } // Find a packet matching every entry of every table. // Loop over tables in a deterministic order for output consistency (important diff --git a/p4_symbolic/sai/BUILD.bazel b/p4_symbolic/sai/BUILD.bazel new file mode 100644 index 00000000..ae881aff --- /dev/null +++ b/p4_symbolic/sai/BUILD.bazel @@ -0,0 +1,46 @@ +# 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. + +load("@bazel_skylib//rules:build_test.bzl", "build_test") +load("//p4_pdpi/testing:diff_test.bzl", "cmd_diff_test", "diff_test") +load("//p4_pdpi:pdgen.bzl", "p4_pd_proto") +load("@com_github_p4lang_p4c//:bazel/p4_library.bzl", "p4_library") + +package(licenses = ["notice"]) + +cc_library( + name = "fields", + srcs = ["fields.cc"], + hdrs = ["fields.h"], + deps = [ + "//gutil:status", + "//p4_symbolic/symbolic", + "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/strings", + ], +) + +cc_library( + name = "parser", + srcs = ["parser.cc"], + hdrs = ["parser.h"], + visibility = ["//p4_symbolic:__subpackages__"], + deps = [ + ":fields", + "//gutil:status", + "//p4_symbolic/symbolic", + "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/status", + ], +) diff --git a/p4_symbolic/sai/README.md b/p4_symbolic/sai/README.md new file mode 100644 index 00000000..7bf5929d --- /dev/null +++ b/p4_symbolic/sai/README.md @@ -0,0 +1,3 @@ +This directory contains all code that is specific to the SAI P4 program. + +TODO: - Move symbolic/packet.{h,cc} to this directory. diff --git a/p4_symbolic/sai/fields.cc b/p4_symbolic/sai/fields.cc new file mode 100644 index 00000000..b1255dd9 --- /dev/null +++ b/p4_symbolic/sai/fields.cc @@ -0,0 +1,119 @@ +// 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/sai/fields.h" + +#include "absl/strings/match.h" +#include "absl/strings/str_join.h" +#include "gutil/status.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "z3++.h" + +namespace p4_symbolic { + +namespace { + +using ::p4_symbolic::symbolic::SymbolicPerPacketState; +using ::p4_symbolic::symbolic::Z3Context; + +// The p4c compiler mangles field names from the local_metadata struct. +// As a workaround, we unmangle the names, best effort. +absl::StatusOr GetUserMetadata(const std::string& field, + const SymbolicPerPacketState& state) { + // Compute set of mangled field names that match the given field name. + std::vector mangled_candidates; + for (const auto& [key, _] : state) { + if (absl::StartsWith(key, "scalars.userMetadata.") && + absl::StrContains(key, field)) { + mangled_candidates.push_back(key); + } + } + + if (mangled_candidates.size() == 1) { + return state.Get(mangled_candidates[0]); + } + + auto error = gutil::InternalErrorBuilder() + << "unable to disambiguate metadata field '" << field << "': "; + if (mangled_candidates.empty()) + return error << "no matching fields found in config"; + return error << "several mangled fields in the config match:\n- " + << absl::StrJoin(mangled_candidates, "\n- "); +} + +} // namespace + +absl::StatusOr GetSaiFields(const SymbolicPerPacketState& state) { + // Helpers to extract fields. + std::vector errors; + auto get_field = [&](const std::string& field) -> z3::expr { + auto result = state.Get(field); + if (result.ok()) return *result; + errors.push_back(result.status()); + // Return dummy. + return z3::expr(Z3Context()); + }; + auto get_metadata_field = [&](const std::string& field) -> z3::expr { + auto result = GetUserMetadata(field, state); + if (result.ok()) return *result; + errors.push_back(result.status()); + // Return dummy. + return z3::expr(Z3Context()); + }; + + auto ethernet = SaiEthernet{ + .valid = get_field("ethernet.$valid$"), + .dst_addr = get_field("ethernet.dst_addr"), + .src_addr = get_field("ethernet.src_addr"), + .ether_type = get_field("ethernet.ether_type"), + }; + auto ipv4 = SaiIpv4{ + .valid = get_field("ipv4.$valid$"), + .version = get_field("ipv4.version"), + .ihl = get_field("ipv4.ihl"), + .dscp = get_field("ipv4.dscp"), + .ecn = get_field("ipv4.ecn"), + .total_len = get_field("ipv4.total_len"), + .identification = get_field("ipv4.identification"), + .reserved = get_field("ipv4.reserved"), + .do_not_fragment = get_field("ipv4.do_not_fragment"), + .more_fragments = get_field("ipv4.more_fragments"), + .frag_offset = get_field("ipv4.frag_offset"), + .ttl = get_field("ipv4.ttl"), + .protocol = get_field("ipv4.protocol"), + .header_checksum = get_field("ipv4.header_checksum"), + .src_addr = get_field("ipv4.src_addr"), + .dst_addr = get_field("ipv4.dst_addr"), + }; + auto local_metadata = SaiLocalMetadata{ + .admit_to_l3 = get_metadata_field("admit_to_l3"), + .vrf_id = get_metadata_field("vrf_id"), + .mirror_session_id_valid = get_metadata_field("mirror_session_id_valid"), + }; + + if (!errors.empty()) { + return gutil::InternalErrorBuilder() + << "Errors while trying to extract hard coded fields:\n- " + << absl::StrJoin(errors, "\n- ", + [](std::string* out, const absl::Status& error) { + absl::StrAppend(out, error.ToString()); + }); + } + return SaiFields{ + .headers = SaiHeaders{.ethernet = ethernet, .ipv4 = ipv4}, + .local_metadata = local_metadata, + }; +} + +} // namespace p4_symbolic diff --git a/p4_symbolic/sai/fields.h b/p4_symbolic/sai/fields.h new file mode 100644 index 00000000..103c2982 --- /dev/null +++ b/p4_symbolic/sai/fields.h @@ -0,0 +1,80 @@ +// 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. + +// This file exposes the SAI header/metadata fields as Z3 expressions, making it +// easy to formulate constraints on these fields. + +#ifndef PINS_P4_SYMBOLIC_SAI_FIELDS_H_ +#define PINS_P4_SYMBOLIC_SAI_FIELDS_H_ + +#include "p4_symbolic/symbolic/symbolic.h" +#include "z3++.h" + +namespace p4_symbolic { + +// Symbolic version of `struct ethernet_t` in headers.p4. +struct SaiEthernet { + z3::expr valid; + z3::expr dst_addr; + z3::expr src_addr; + z3::expr ether_type; +}; + +// Symbolic version of `struct ipv4_t` in headers.p4. +struct SaiIpv4 { + z3::expr valid; + z3::expr version; + z3::expr ihl; + z3::expr dscp; + z3::expr ecn; + z3::expr total_len; + z3::expr identification; + z3::expr reserved; + z3::expr do_not_fragment; + z3::expr more_fragments; + z3::expr frag_offset; + z3::expr ttl; + z3::expr protocol; + z3::expr header_checksum; + z3::expr src_addr; + z3::expr dst_addr; +}; + +// Symbolic version of `struct headers_t` in metadata.p4. +struct SaiHeaders { + SaiEthernet ethernet; + SaiIpv4 ipv4; +}; + +// Symbolic version of `struct local_metadata_t` in metadata.p4. +struct SaiLocalMetadata { + z3::expr admit_to_l3; + z3::expr vrf_id; + // TODO: add `packet_rewrites` fields. + z3::expr mirror_session_id_valid; + // TODO: add `mirror*` fields. + // TODO: Add `color` field. +}; + +struct SaiFields { + SaiHeaders headers; + SaiLocalMetadata local_metadata; +}; + +absl::StatusOr GetSaiFields( + const symbolic::SymbolicPerPacketState& state); + +} // namespace p4_symbolic + +#endif // PINS_P4_SYMBOLIC_SAI_FIELDS_H_ diff --git a/p4_symbolic/sai/parser.cc b/p4_symbolic/sai/parser.cc new file mode 100644 index 00000000..a46e3213 --- /dev/null +++ b/p4_symbolic/sai/parser.cc @@ -0,0 +1,145 @@ +// 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/sai/parser.h" + +#include "gutil/status.h" +#include "p4_symbolic/sai/fields.h" +#include "p4_symbolic/symbolic/operators.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "z3++.h" + +namespace p4_symbolic { + +using ::p4_symbolic::symbolic::SymbolicPerPacketState; +using ::p4_symbolic::symbolic::Z3Context; + +absl::StatusOr> EvaluateSaiParser( + const SymbolicPerPacketState& state) { + std::vector constraints; + + ASSIGN_OR_RETURN(SaiFields fields, GetSaiFields(state)); + SaiEthernet& ethernet = fields.headers.ethernet; + SaiIpv4& ipv4 = fields.headers.ipv4; + z3::expr bv_true = Z3Context().bv_val(1, 1); + z3::expr bv_false = Z3Context().bv_val(0, 1); + + // `start` state. + constraints.push_back(fields.local_metadata.admit_to_l3 == bv_true); + constraints.push_back(fields.local_metadata.mirror_session_id_valid == + bv_false); + + // `parse_ethernet` state. + constraints.push_back(ethernet.valid == Z3Context().bool_val(true)); + constraints.push_back(ipv4.valid == (ethernet.ether_type == 0x0800)); + + // TODO: clean up old code. + // // Set initial value for vrf. + // ASSIGN_OR_RETURN(z3::expr vrf_id, + // state.Get("scalars.userMetadata.vrf_id")); ASSIGN_OR_RETURN(z3::expr + // vrf_constraint, + // operators::Eq(vrf_id, Z3Context().bv_val(0, 1))); + // constraints.push_back(vrf_constraint); + + // // l4_src_port and l4_dst_port are extracted from the headers if tcp or + // udp + // // were used, and set to zero otherwise. + // // We must be careful that these values are guarded by the proper + // validity + // // guards, or we will impose contradictory constraints. + // ASSIGN_OR_RETURN(z3::expr l4_src_port, + // state.Get("scalars.userMetadata.l4_src_port")); + // ASSIGN_OR_RETURN(z3::expr l4_dst_port, + // state.Get("scalars.userMetadata.l4_dst_port")); + + // // Find out which headers the program supports. + // ASSIGN_OR_RETURN(z3::expr ipv4_valid, state.Get("ipv4.$valid$")); + // ASSIGN_OR_RETURN(z3::expr ipv6_valid, state.Get("ipv6.$valid$")); + // ASSIGN_OR_RETURN(z3::expr arp_valid, state.Get("arp.$valid$")); + + // // Put restrictions on what "eth_type" can be and how it affects validity + // of + // // certain headers. + // ASSIGN_OR_RETURN(z3::expr eth_type, state.Get("ethernet.ether_type")); + // constraints.push_back(ipv4_valid == (eth_type == ETHERTYPE_IPV4)); + // constraints.push_back(ipv6_valid == (eth_type == ETHERTYPE_IPV6)); + // constraints.push_back(arp_valid == (eth_type == ETHERTYPE_ARP)); + + // Put similar restrictions on the validity of protocol-specific headers. + // Which protocol used is specified by ipv4.protcol or ipv6.next_headers. + // ASSIGN_OR_RETURN(z3::expr protocol, state.Get("ipv4.protocol")); + // ASSIGN_OR_RETURN(z3::expr next_header, state.Get("ipv6.next_header")); + + // // ICMP. + // ASSIGN_OR_RETURN(z3::expr icmp_valid, state.Get("icmp.$valid$")); + // z3::expr icmp_valid_ipv4 = (protocol == IP_PROTOCOL_ICMP) && ipv4_valid; + // z3::expr icmp_valid_ipv6 = (next_header == IP_PROTOCOL_ICMPV6) && + // ipv6_valid; constraints.push_back(icmp_valid == (icmp_valid_ipv4 || + // icmp_valid_ipv6)); + + // // TCP. + // ASSIGN_OR_RETURN(z3::expr tcp_valid, state.Get("tcp.$valid$")); + // z3::expr tcp_valid_ipv4 = (protocol == IP_PROTOCOL_TCP) && ipv4_valid; + // z3::expr tcp_valid_ipv6 = (next_header == IP_PROTOCOL_TCP) && ipv6_valid; + // constraints.push_back(tcp_valid == (tcp_valid_ipv4 || tcp_valid_ipv6)); + + // // Set l4_src_port and l4_dst_port to those of tcp header, if tcp is + // used. ASSIGN_OR_RETURN(z3::expr tcp_src_port, state.Get("tcp.src_port")); + // ASSIGN_OR_RETURN(z3::expr tcp_dst_port, state.Get("tcp.dst_port")); + // ASSIGN_OR_RETURN(z3::expr l4_src_port_eq_tcp_src_port, + // operators::Eq(tcp_src_port, l4_src_port)); + // ASSIGN_OR_RETURN(z3::expr l4_dst_port_eq_tcp_dst_port, + // operators::Eq(tcp_dst_port, l4_dst_port)); + + // constraints.push_back(z3::implies(tcp_valid, + // l4_src_port_eq_tcp_src_port)); + // constraints.push_back(z3::implies(tcp_valid, + // l4_dst_port_eq_tcp_dst_port)); + + // // UDP. + // ASSIGN_OR_RETURN(z3::expr udp_valid, state.Get("udp.$valid$")); + // z3::expr udp_valid_ipv4 = (protocol == IP_PROTOCOL_UDP) && ipv4_valid; + // z3::expr udp_valid_ipv6 = (next_header == IP_PROTOCOL_UDP) && ipv6_valid; + // constraints.push_back(udp_valid == (udp_valid_ipv4 || udp_valid_ipv6)); + + // // Set l4_src_port and l4_dst_port to those of udp header, if udp is + // used. ASSIGN_OR_RETURN(z3::expr udp_src_port, state.Get("udp.src_port")); + // ASSIGN_OR_RETURN(z3::expr udp_dst_port, state.Get("udp.dst_port")); + // ASSIGN_OR_RETURN(z3::expr l4_src_port_eq_udp_src_port, + // operators::Eq(udp_src_port, l4_src_port)); + // ASSIGN_OR_RETURN(z3::expr l4_dst_port_eq_udp_dst_port, + // operators::Eq(udp_dst_port, l4_dst_port)); + + // constraints.push_back(z3::implies(udp_valid, + // l4_src_port_eq_udp_src_port)); + // constraints.push_back(z3::implies(udp_valid, + // l4_dst_port_eq_udp_dst_port)); + + // // Default values for l4_src_port and l4_dst_port. + // ASSIGN_OR_RETURN(z3::expr tcp_or_udp_valid, + // operators::Or(tcp_valid, udp_valid)); + // ASSIGN_OR_RETURN(z3::expr l4_src_port_constraint, + // operators::Eq(l4_src_port, Z3Context().bv_val(0, 1))); + // ASSIGN_OR_RETURN(z3::expr l4_dst_port_constraint, + // operators::Eq(l4_dst_port, Z3Context().bv_val(0, 1))); + // constraints.push_back(z3::implies(!tcp_or_udp_valid, + // l4_src_port_constraint)); + // constraints.push_back(z3::implies(!tcp_or_udp_valid, + // l4_dst_port_constraint)); + + // Done, return all constraints. + return constraints; +} + +} // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/parser.h b/p4_symbolic/sai/parser.h similarity index 60% rename from p4_symbolic/symbolic/parser.h rename to p4_symbolic/sai/parser.h index 0438a57a..4ec558dd 100644 --- a/p4_symbolic/symbolic/parser.h +++ b/p4_symbolic/sai/parser.h @@ -18,34 +18,22 @@ // based on the fields in the packet, and sets the default values // for local_metadata fields. -#ifndef P4_SYMBOLIC_SYMBOLIC_PARSER_H_ -#define P4_SYMBOLIC_SYMBOLIC_PARSER_H_ +#ifndef GOOGLE_P4_SYMBOLIC_SAI_PARSER_H_ +#define GOOGLE_P4_SYMBOLIC_SAI_PARSER_H_ #include #include "gutil/status.h" #include "p4_symbolic/symbolic/symbolic.h" -#define ETHERTYPE_IPV4 0x0800 -#define ETHERTYPE_IPV6 0x86dd -#define ETHERTYPE_ARP 0x0806 - -#define IP_PROTOCOL_TCP 0x06 -#define IP_PROTOCOL_UDP 0x11 -#define IP_PROTOCOL_ICMP 0x01 -#define IP_PROTOCOL_ICMPV6 0x3a - namespace p4_symbolic { -namespace symbolic { -namespace parser { -// Creates assertions/constraints that encode some of the interesting -// behavior of parsers in specific programs we want to analyze. -absl::StatusOr> EvaluateHardcodedParser( - const SymbolicPerPacketState &state); +// Generates constraints encoding the behavior of the SAI parser. +// NOTE: The parser logic is currently hard-coded and not parsed from the +// program. +absl::StatusOr> EvaluateSaiParser( + const symbolic::SymbolicPerPacketState &state); -} // namespace parser -} // namespace symbolic } // namespace p4_symbolic -#endif // P4_SYMBOLIC_SYMBOLIC_PARSER_H_ +#endif // GOOGLE_P4_SYMBOLIC_SAI_PARSER_H_ diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index db9f54cb..5e26e7ab 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -29,7 +29,6 @@ cc_library( "guarded_map.cc", "operators.cc", "packet.cc", - "parser.cc", "symbolic.cc", "table.cc", "util.cc", @@ -42,7 +41,6 @@ cc_library( "guarded_map.h", "operators.h", "packet.h", - "parser.h", "symbolic.h", "table.h", "util.h", @@ -59,11 +57,14 @@ cc_library( "//p4_symbolic/ir:ir_cc_proto", "//p4_symbolic/ir:table_entries", "@com_github_google_glog//:glog", - "@com_github_z3prover_z3//:api", - "@com_gnu_gmp//:gmp", + "@com_github_p4lang_p4runtime//:p4info_cc_proto", + "@com_github_z3prover_z3//:api", + "@com_gnu_gmp//:gmp", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", "@com_google_absl//absl/strings:str_format", + "@com_google_absl//absl/types:optional", + "@com_google_absl//absl/types:span", "@com_google_protobuf//:protobuf", ], ) diff --git a/p4_symbolic/symbolic/action.cc b/p4_symbolic/symbolic/action.cc index 80c7bc94..769bb3ba 100644 --- a/p4_symbolic/symbolic/action.cc +++ b/p4_symbolic/symbolic/action.cc @@ -32,9 +32,13 @@ absl::Status EvaluateStatement(const ir::Statement &statement, return EvaluateAssignmentStatement(statement.assignment(), state, context, guard); } + case ir::Statement::kClone: // TODO: Add support for cloning. case ir::Statement::kDrop: { // https://github.com/p4lang/p4c/blob/7ee76d16da63883c5092ab0c28321f04c2646759/p4include/v1model.p4#L435 - const std::string &header_name = statement.drop().header().header_name(); + const std::string &header_name = + // TODO: conditonal needed to interpret clone as drop. + statement.has_drop() ? statement.drop().header().header_name() + : "standard_metadata"; z3::expr dropped_value = Z3Context().bv_val(DROPPED_EGRESS_SPEC_VALUE, DROPPED_EGRESS_SPEC_LENGTH); RETURN_IF_ERROR(state->Set(absl::StrFormat("%s.egress_spec", header_name), @@ -43,10 +47,6 @@ absl::Status EvaluateStatement(const ir::Statement &statement, Z3Context().bv_val(0, 1), guard)); return absl::OkStatus(); } - case ir::Statement::kClone: { - // No-op. - return absl::OkStatus(); - } case ir::Statement::kHash: { const ir::FieldValue &field = statement.hash().field(); std::string field_name = diff --git a/p4_symbolic/symbolic/conditional.cc b/p4_symbolic/symbolic/conditional.cc index b5068e64..06969812 100644 --- a/p4_symbolic/symbolic/conditional.cc +++ b/p4_symbolic/symbolic/conditional.cc @@ -27,7 +27,7 @@ namespace symbolic { namespace conditional { absl::StatusOr EvaluateConditional( - const Dataplane data_plane, const ir::Conditional &conditional, + const Dataplane &data_plane, const ir::Conditional &conditional, SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard) { // Evaluate the condition. diff --git a/p4_symbolic/symbolic/conditional.h b/p4_symbolic/symbolic/conditional.h index a4fa8b87..afd46073 100644 --- a/p4_symbolic/symbolic/conditional.h +++ b/p4_symbolic/symbolic/conditional.h @@ -30,7 +30,7 @@ namespace symbolic { namespace conditional { absl::StatusOr EvaluateConditional( - const Dataplane data_plane, const ir::Conditional &conditional, + const Dataplane &data_plane, const ir::Conditional &conditional, SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard); diff --git a/p4_symbolic/symbolic/operators.cc b/p4_symbolic/symbolic/operators.cc index ce6044f5..d941ac22 100644 --- a/p4_symbolic/symbolic/operators.cc +++ b/p4_symbolic/symbolic/operators.cc @@ -60,6 +60,13 @@ z3::expr Suffix(const z3::expr &bitvector, unsigned int suffix_size) { // the longest. absl::StatusOr> SortCheckAndPad( const z3::expr &a, const z3::expr &b) { + // Coerce bit<1> to bool. + if (a.is_bool() && b.is_bv() && b.get_sort().bv_size() == 1) { + return std::make_pair(a, b == 1); + } + if (b.is_bool() && a.is_bv() && a.get_sort().bv_size() == 1) { + return std::make_pair(a == 1, b); + } // Totally incompatible sorts (e.g. int and bitvector). if (a.get_sort().sort_kind() != b.get_sort().sort_kind()) { return absl::InvalidArgumentError(absl::StrFormat( @@ -73,7 +80,7 @@ absl::StatusOr> SortCheckAndPad( int b_len = b.get_sort().bv_size(); return std::make_pair(Pad(a, b_len - a_len), Pad(b, a_len - b_len)); } - return std::make_pair(z3::expr(a), z3::expr(b)); + return std::make_pair(a, b); } // Check that the two expressions have compatible sorts, and return an diff --git a/p4_symbolic/symbolic/operators.h b/p4_symbolic/symbolic/operators.h index 933164cb..5bd3c2c3 100644 --- a/p4_symbolic/symbolic/operators.h +++ b/p4_symbolic/symbolic/operators.h @@ -13,7 +13,8 @@ // limitations under the License. // Defines a wrapper around z3 c++ API operators. -// The wrappers ensure sort compatibility, and pad bitvectors when needed. +// The wrappers ensure sort compatibility, and pad bitvectors when needed, and +// automatically convert between bool and bit<1>. // Additionally, they use absl::Status to convey sort compatibility failures // instead of runtime crashes. diff --git a/p4_symbolic/symbolic/parser.cc b/p4_symbolic/symbolic/parser.cc deleted file mode 100644 index dd77d82c..00000000 --- a/p4_symbolic/symbolic/parser.cc +++ /dev/null @@ -1,122 +0,0 @@ -// 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. - -// Hardcodes the behavior of an interesting p4 parser that is part -// of the p4 program we are interested in. -// The hardcoded behavior sets the validity of certain header fields -// based on the fields in the packet, and sets the default values -// for local_metadata fields. - -#include "p4_symbolic/symbolic/parser.h" - -#include "p4_symbolic/symbolic/operators.h" -#include "z3++.h" - -namespace p4_symbolic { -namespace symbolic { -namespace parser { - -absl::StatusOr> EvaluateHardcodedParser( - const SymbolicPerPacketState &state) { - std::vector constraints; - - // Set initial value for vrf. - ASSIGN_OR_RETURN(z3::expr vrf_id, state.Get("scalars.userMetadata.vrf_id")); - ASSIGN_OR_RETURN(z3::expr vrf_constraint, - operators::Eq(vrf_id, Z3Context().bv_val(0, 1))); - constraints.push_back(vrf_constraint); - - // l4_src_port and l4_dst_port are extracted from the headers if tcp or udp - // were used, and set to zero otherwise. - // We must be careful that these values are guarded by the proper validity - // guards, or we will impose contradictory constraints. - ASSIGN_OR_RETURN(z3::expr l4_src_port, - state.Get("scalars.userMetadata.l4_src_port")); - ASSIGN_OR_RETURN(z3::expr l4_dst_port, - state.Get("scalars.userMetadata.l4_dst_port")); - - // Find out which headers the program supports. - ASSIGN_OR_RETURN(z3::expr ipv4_valid, state.Get("ipv4.$valid$")); - ASSIGN_OR_RETURN(z3::expr ipv6_valid, state.Get("ipv6.$valid$")); - ASSIGN_OR_RETURN(z3::expr arp_valid, state.Get("arp.$valid$")); - - // Put restrictions on what "eth_type" can be and how it affects validity of - // certain headers. - ASSIGN_OR_RETURN(z3::expr eth_type, state.Get("ethernet.ether_type")); - constraints.push_back(ipv4_valid == (eth_type == ETHERTYPE_IPV4)); - constraints.push_back(ipv6_valid == (eth_type == ETHERTYPE_IPV6)); - constraints.push_back(arp_valid == (eth_type == ETHERTYPE_ARP)); - - // Put similar restrictions on the validity of protocol-specific headers. - // Which protocol used is specified by ipv4.protcol or ipv6.next_headers. - ASSIGN_OR_RETURN(z3::expr protocol, state.Get("ipv4.protocol")); - ASSIGN_OR_RETURN(z3::expr next_header, state.Get("ipv6.next_header")); - - // ICMP. - ASSIGN_OR_RETURN(z3::expr icmp_valid, state.Get("icmp.$valid$")); - z3::expr icmp_valid_ipv4 = (protocol == IP_PROTOCOL_ICMP) && ipv4_valid; - z3::expr icmp_valid_ipv6 = (next_header == IP_PROTOCOL_ICMPV6) && ipv6_valid; - constraints.push_back(icmp_valid == (icmp_valid_ipv4 || icmp_valid_ipv6)); - - // TCP. - ASSIGN_OR_RETURN(z3::expr tcp_valid, state.Get("tcp.$valid$")); - z3::expr tcp_valid_ipv4 = (protocol == IP_PROTOCOL_TCP) && ipv4_valid; - z3::expr tcp_valid_ipv6 = (next_header == IP_PROTOCOL_TCP) && ipv6_valid; - constraints.push_back(tcp_valid == (tcp_valid_ipv4 || tcp_valid_ipv6)); - - // Set l4_src_port and l4_dst_port to those of tcp header, if tcp is used. - ASSIGN_OR_RETURN(z3::expr tcp_src_port, state.Get("tcp.src_port")); - ASSIGN_OR_RETURN(z3::expr tcp_dst_port, state.Get("tcp.dst_port")); - ASSIGN_OR_RETURN(z3::expr l4_src_port_eq_tcp_src_port, - operators::Eq(tcp_src_port, l4_src_port)); - ASSIGN_OR_RETURN(z3::expr l4_dst_port_eq_tcp_dst_port, - operators::Eq(tcp_dst_port, l4_dst_port)); - - constraints.push_back(z3::implies(tcp_valid, l4_src_port_eq_tcp_src_port)); - constraints.push_back(z3::implies(tcp_valid, l4_dst_port_eq_tcp_dst_port)); - - // UDP. - ASSIGN_OR_RETURN(z3::expr udp_valid, state.Get("udp.$valid$")); - z3::expr udp_valid_ipv4 = (protocol == IP_PROTOCOL_UDP) && ipv4_valid; - z3::expr udp_valid_ipv6 = (next_header == IP_PROTOCOL_UDP) && ipv6_valid; - constraints.push_back(udp_valid == (udp_valid_ipv4 || udp_valid_ipv6)); - - // Set l4_src_port and l4_dst_port to those of udp header, if udp is used. - ASSIGN_OR_RETURN(z3::expr udp_src_port, state.Get("udp.src_port")); - ASSIGN_OR_RETURN(z3::expr udp_dst_port, state.Get("udp.dst_port")); - ASSIGN_OR_RETURN(z3::expr l4_src_port_eq_udp_src_port, - operators::Eq(udp_src_port, l4_src_port)); - ASSIGN_OR_RETURN(z3::expr l4_dst_port_eq_udp_dst_port, - operators::Eq(udp_dst_port, l4_dst_port)); - - constraints.push_back(z3::implies(udp_valid, l4_src_port_eq_udp_src_port)); - constraints.push_back(z3::implies(udp_valid, l4_dst_port_eq_udp_dst_port)); - - // Default values for l4_src_port and l4_dst_port. - ASSIGN_OR_RETURN(z3::expr tcp_or_udp_valid, - operators::Or(tcp_valid, udp_valid)); - ASSIGN_OR_RETURN(z3::expr l4_src_port_constraint, - operators::Eq(l4_src_port, Z3Context().bv_val(0, 1))); - ASSIGN_OR_RETURN(z3::expr l4_dst_port_constraint, - operators::Eq(l4_dst_port, Z3Context().bv_val(0, 1))); - constraints.push_back(z3::implies(!tcp_or_udp_valid, l4_src_port_constraint)); - constraints.push_back(z3::implies(!tcp_or_udp_valid, l4_dst_port_constraint)); - - // Done, return all constraints. - return constraints; -} - -} // namespace parser -} // namespace symbolic -} // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index 4da0463b..0f4e4151 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -16,10 +16,11 @@ #include +#include "absl/types/optional.h" +#include "glog/logging.h" #include "p4_symbolic/symbolic/control.h" #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/packet.h" -#include "p4_symbolic/symbolic/parser.h" #include "p4_symbolic/symbolic/util.h" namespace p4_symbolic { @@ -31,8 +32,7 @@ z3::context &Z3Context() { } absl::StatusOr> EvaluateP4Pipeline( - const Dataplane &data_plane, const std::vector &physical_ports, - bool hardcoded_parser) { + const Dataplane &data_plane, const std::vector &physical_ports) { // Use global context to define a solver. std::unique_ptr z3_solver = std::make_unique(Z3Context()); @@ -43,13 +43,6 @@ absl::StatusOr> EvaluateP4Pipeline( ASSIGN_OR_RETURN(SymbolicPerPacketState ingress_headers, SymbolicGuardedMap::CreateSymbolicGuardedMap( data_plane.program.headers())); - if (hardcoded_parser) { - ASSIGN_OR_RETURN(std::vector parser_constraints, - parser::EvaluateHardcodedParser(ingress_headers)); - for (const z3::expr &constraint : parser_constraints) { - z3_solver->add(constraint); - } - } // Initially, the p4runtime translator has empty state. values::P4RuntimeTranslator translator; @@ -123,25 +116,25 @@ absl::StatusOr> Solve( solver_state->solver->push(); solver_state->solver->add(constraint); - switch (solver_state->solver->check()) { + z3::check_result check_result = solver_state->solver->check(); + switch (check_result) { case z3::unsat: - solver_state->solver->pop(); - return std::optional(); - case z3::unknown: solver_state->solver->pop(); - return std::optional(); + return absl::nullopt; case z3::sat: - default: z3::model packet_model = solver_state->solver->get_model(); ASSIGN_OR_RETURN( ConcreteContext result, util::ExtractFromModel(solver_state->context, packet_model, solver_state->translator)); solver_state->solver->pop(); - return std::make_optional(result); + return result; } + LOG(DFATAL) << "invalid Z3 check() result: " + << static_cast(check_result); + return absl::nullopt; } std::string DebugSMT(const std::unique_ptr &solver_state, diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index a6675743..c11655b4 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -269,8 +269,7 @@ using Assertion = std::function; // entries for every table in that program, and the available physical ports // on the switch. absl::StatusOr> EvaluateP4Pipeline( - const Dataplane &data_plane, const std::vector &physical_ports, - bool hardcoded_parser); + const Dataplane &data_plane, const std::vector &physical_ports); // Finds a concrete packet and flow in the program that satisfies the given // assertion and meets the structure constrained by solver_state. diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index 85868b03..0398df51 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -26,8 +26,15 @@ #include "absl/status/status.h" #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" +#include "absl/types/optional.h" +#include "absl/types/span.h" +#include "gutil/status.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4_pdpi/ir.pb.h" #include "p4_symbolic/symbolic/action.h" #include "p4_symbolic/symbolic/operators.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/values.h" #include "z3++.h" namespace p4_symbolic { @@ -71,23 +78,21 @@ int FindMatchWithName(const pdpi::IrTableEntry &entry, // and not the sorted array. std::vector> SortEntries( const ir::Table &table, const std::vector &entries) { + if (entries.empty()) return {}; // Find which *definition* of priority we should use by looking at the // table's match types. const pdpi::IrTableDefinition &table_definition = table.table_definition(); bool has_ternary = false; - bool has_lpm = false; - int lpm_index = -1; - for (const auto &[id, match_field_definition] : - table_definition.match_fields_by_id()) { + absl::optional lpm_key; + for (const auto &[name, match_field_definition] : + table_definition.match_fields_by_name()) { switch (match_field_definition.match_field().match_type()) { case p4::config::v1::MatchField::TERNARY: { has_ternary = true; break; } case p4::config::v1::MatchField::LPM: { - has_lpm = true; - // The match id starts from 1 (instead of zero). - lpm_index = id - 1; + lpm_key = name; break; } default: { @@ -116,13 +121,23 @@ std::vector> SortEntries( const std::pair &entry2) { return entry1.second.priority() > entry2.second.priority(); }; - } else if (has_lpm) { + } else if (lpm_key.has_value()) { // Sort by prefix length. - comparator = [lpm_index]( + comparator = [lpm_key]( const std::pair &entry1, const std::pair &entry2) { - return entry1.second.matches(lpm_index).lpm().prefix_length() > - entry2.second.matches(lpm_index).lpm().prefix_length(); + auto is_lpm_match = [=](const pdpi::IrMatch &match) -> bool { + return match.name() == *lpm_key; + }; + auto matches1 = entry1.second.matches(); + auto matches2 = entry2.second.matches(); + auto it1 = std::find_if(matches1.begin(), matches1.end(), is_lpm_match); + auto it2 = std::find_if(matches2.begin(), matches2.end(), is_lpm_match); + int prefix_length1 = + it1 == matches1.end() ? 0 : it1->lpm().prefix_length(); + int prefix_length2 = + it2 == matches2.end() ? 0 : it2->lpm().prefix_length(); + return prefix_length1 > prefix_length2; }; } else { return sorted_entries; @@ -147,14 +162,17 @@ absl::StatusOr EvaluateSingleMatch( absl::StrCat("Found match with non-standard type")); } + absl::Status mismatch = + gutil::InvalidArgumentErrorBuilder() + << "match on field '" << field_name << "' must be of type " + << p4::config::v1::MatchField::MatchType_Name( + match_definition.match_type()) + << " according to the table definition, but got entry with match: " + << match_definition.ShortDebugString(); + switch (match_definition.match_type()) { case p4::config::v1::MatchField::EXACT: { - if (match.match_value_case() != pdpi::IrMatch::kExact) { - return absl::InvalidArgumentError( - absl::StrCat("Match definition in table has type \"Exact\" but its " - "invocation in TableEntry has a different type ", - match_definition.DebugString())); - } + if (match.match_value_case() != pdpi::IrMatch::kExact) return mismatch; ASSIGN_OR_RETURN(z3::expr value_expression, values::FormatP4RTValue( field_name, match_definition.type_name().name(), @@ -163,12 +181,7 @@ absl::StatusOr EvaluateSingleMatch( } case p4::config::v1::MatchField::LPM: { - if (match.match_value_case() != pdpi::IrMatch::kLpm) { - return absl::InvalidArgumentError( - absl::StrCat("Match definition in table has type \"LPM\" but its " - "invocation in TableEntry has a different type ", - match_definition.DebugString())); - } + if (match.match_value_case() != pdpi::IrMatch::kLpm) return mismatch; ASSIGN_OR_RETURN(z3::expr value_expression, values::FormatBmv2Value(match.lpm().value())); @@ -178,12 +191,7 @@ absl::StatusOr EvaluateSingleMatch( } case p4::config::v1::MatchField::TERNARY: { - if (match.match_value_case() != pdpi::IrMatch::kTernary) { - return absl::InvalidArgumentError( - absl::StrCat("Match definition in table has type \"TERNARY\" but " - "its invocation in TableEntry has a different type ", - match_definition.DebugString())); - } + if (match.match_value_case() != pdpi::IrMatch::kTernary) return mismatch; ASSIGN_OR_RETURN(z3::expr mask_expression, values::FormatBmv2Value(match.ternary().mask())); @@ -194,6 +202,13 @@ absl::StatusOr EvaluateSingleMatch( return operators::Eq(masked_field, value_expression); } + case p4::config::v1::MatchField::OPTIONAL: { + if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch; + ASSIGN_OR_RETURN(z3::expr value_expression, + values::FormatBmv2Value(match.optional().value())); + return operators::Eq(field_expression, value_expression); + } + default: return absl::UnimplementedError(absl::StrCat( "Found unsupported match type ", match_definition.DebugString())); @@ -255,6 +270,20 @@ absl::StatusOr EvaluateTableEntryCondition( return condition_expression; } +absl::Status EvaluateSingeTableEntryAction( + const pdpi::IrActionInvocation &action, + const google::protobuf::Map &actions, + SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, + const z3::expr &guard) { + // Check that the action invoked by entry exists. + if (actions.count(action.name()) != 1) { + return gutil::InvalidArgumentErrorBuilder() + << "unknown action '" << action.name() << "'"; + } + return action::EvaluateAction(actions.at(action.name()), action.params(), + state, translator, guard); +} + // Constructs a symbolic expressions that represents the action invocation // corresponding to this entry. absl::Status EvaluateTableEntryAction( @@ -262,25 +291,47 @@ absl::Status EvaluateTableEntryAction( const google::protobuf::Map &actions, SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard) { - // Check that the action invoked by entry exists. - const std::string &table_name = table.table_definition().preamble().name(); - const std::string &action_name = entry.action().name(); - if (actions.count(action_name) != 1) { - return absl::InvalidArgumentError( - absl::StrCat("Found a match entry ", entry.DebugString(), " in table", - table_name, " referring to unknown action ", action_name)); + switch (entry.type_case()) { + case pdpi::IrTableEntry::kAction: + RETURN_IF_ERROR(EvaluateSingeTableEntryAction(entry.action(), actions, + state, translator, guard)) + .SetPrepend() + << "In table entry '" << entry.ShortDebugString() << "':"; + return absl::OkStatus(); + case pdpi::IrTableEntry::kActionSet: { + auto &action_set = entry.action_set().actions(); + // For action sets, we introduce a new free integer variable "selector" + // whose value determines which action is executed: to a first + // approximation, action i is executed iff `selector == i`. + std::string selector_name = + absl::StrCat("action selector for ", entry.DebugString()); + z3::expr selector = Z3Context().int_const(selector_name.c_str()); + z3::expr unselected = Z3Context().bool_val(true); + for (int i = 0; i < action_set.size(); ++i) { + auto &action = action_set.at(i).action(); + bool is_last_action = i == action_set.size() - 1; + z3::expr selected = is_last_action ? unselected : (selector == i); + unselected = unselected && !selected; + RETURN_IF_ERROR(EvaluateSingeTableEntryAction(action, actions, state, + translator, + guard && selected)) + .SetPrepend() + << "In table entry '" << entry.ShortDebugString() << "':"; + } + return absl::OkStatus(); + } + default: + break; } - - // Instantiate the action's symbolic expression with the entry values. - const ir::Action &action = actions.at(action_name); - return action::EvaluateAction(action, entry.action().params(), state, - translator, guard); + return gutil::InvalidArgumentErrorBuilder() + << "unexpected or missing action in table entry: " + << entry.DebugString(); } } // namespace absl::StatusOr EvaluateTable( - const Dataplane data_plane, const ir::Table &table, + const Dataplane &data_plane, const ir::Table &table, const std::vector &entries, SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard) { diff --git a/p4_symbolic/symbolic/table.h b/p4_symbolic/symbolic/table.h index 03a4af3a..69676773 100644 --- a/p4_symbolic/symbolic/table.h +++ b/p4_symbolic/symbolic/table.h @@ -37,7 +37,7 @@ namespace symbolic { namespace table { absl::StatusOr EvaluateTable( - const Dataplane data_plane, const ir::Table &table, + const Dataplane &data_plane, const ir::Table &table, const std::vector &entries, SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard); diff --git a/p4_symbolic/testdata/ipv4-routing/basic.p4 b/p4_symbolic/testdata/ipv4-routing/basic.p4 index 170e3240..d700304f 100644 --- a/p4_symbolic/testdata/ipv4-routing/basic.p4 +++ b/p4_symbolic/testdata/ipv4-routing/basic.p4 @@ -103,14 +103,14 @@ control MyIngress(inout headers hdr, action drop() { mark_to_drop(standard_metadata); } - + action ipv4_forward(macAddr_t dstAddr, egressSpec_t port) { standard_metadata.egress_spec = port; hdr.ethernet.srcAddr = hdr.ethernet.dstAddr; hdr.ethernet.dstAddr = dstAddr; hdr.ipv4.ttl = hdr.ipv4.ttl - 1; } - + table ipv4_lpm { key = { hdr.ipv4.dstAddr: lpm @format(IPV4_ADDRESS); @@ -123,7 +123,7 @@ control MyIngress(inout headers hdr, size = 1024; default_action = drop(); } - + apply { if (hdr.ipv4.isValid()) { ipv4_lpm.apply(); diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index 63056f1a..87daf147 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -17,7 +17,8 @@ cc_test( "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", "//p4_pdpi:pd", - "//p4_symbolic:parser", + "//p4_symbolic:parser", + "//p4_symbolic/sai:parser", "//p4_symbolic/symbolic", "//sai_p4/instantiations/google:sai_nonstandard_platforms_cc", "//sai_p4/instantiations/google:sai_pd_cc_proto", diff --git a/p4_symbolic/tests/sai_p4_component_test.cc b/p4_symbolic/tests/sai_p4_component_test.cc index eaf7700c..e6cbe62f 100644 --- a/p4_symbolic/tests/sai_p4_component_test.cc +++ b/p4_symbolic/tests/sai_p4_component_test.cc @@ -13,6 +13,7 @@ #include "p4_pdpi/ir.pb.h" #include "p4_pdpi/pd.h" #include "p4_symbolic/parser.h" +#include "p4_symbolic/sai/parser.h" #include "p4_symbolic/symbolic/symbolic.h" #include "sai_p4/instantiations/google/sai_nonstandard_platforms.h" #include "sai_p4/instantiations/google/sai_pd.pb.h" @@ -30,17 +31,14 @@ using ::testing::Not; constexpr absl::string_view kTableEntries = R"PB( entries { acl_pre_ingress_table_entry { - match {} + match { + src_mac { value: "22:22:22:11:11:11" mask: "ff:ff:ff:ff:ff:ff" } + dst_ip { value: "10.0.10.0" mask: "255.255.255.255" } + } action { set_vrf { vrf_id: "vrf-80" } } priority: 1 } } - entries { - ipv6_table_entry { - match { vrf_id: "vrf-80" } - action { drop {} } - } - } entries { ipv4_table_entry { match { vrf_id: "vrf-80" } diff --git a/sai_p4/fixed/routing.p4 b/sai_p4/fixed/routing.p4 index 85fd4ee1..2c4600f4 100644 --- a/sai_p4/fixed/routing.p4 +++ b/sai_p4/fixed/routing.p4 @@ -439,6 +439,9 @@ control routing(in headers_t headers, // Calling this action will override unicast, and can itself be overriden by // `mark_to_drop`. // + // Using a `multicast_group_id` of 0 is not allowed. + // TODO: Enforce this requirement using p4-constraints. + // // TODO: Remove `@unsupported` annotation once the switch stack // supports multicast. @unsupported