From e2fa992c4b54d95de7baeb2842c0df8c9dbf1417 Mon Sep 17 00:00:00 2001 From: Matthew Lam Date: Mon, 8 Dec 2025 11:27:15 -0800 Subject: [PATCH] [NetKAT] Support debugging/printing messages in CounterExamples for NetKAT. PiperOrigin-RevId: 841847140 --- netkat/BUILD.bazel | 40 +++ netkat/analysis_engine.cc | 21 +- netkat/analysis_engine.h | 20 +- ...lysis_engine_counter_example_test.expected | 312 ++++++++++++++++++ ...ysis_engine_counter_example_test_runner.cc | 115 +++++++ netkat/analysis_engine_test.cc | 55 +-- netkat/counter_example.cc | 268 +++++++++++++++ netkat/counter_example.h | 137 ++++++++ netkat/switch_test.cc | 19 +- netkat/table_test.cc | 23 +- 10 files changed, 969 insertions(+), 41 deletions(-) create mode 100644 netkat/analysis_engine_counter_example_test.expected create mode 100644 netkat/analysis_engine_counter_example_test_runner.cc create mode 100644 netkat/counter_example.cc create mode 100644 netkat/counter_example.h diff --git a/netkat/BUILD.bazel b/netkat/BUILD.bazel index ff33fa3..434dbc3 100644 --- a/netkat/BUILD.bazel +++ b/netkat/BUILD.bazel @@ -276,14 +276,34 @@ cc_library( hdrs = ["paged_stable_vector.h"], ) +cc_library( + name = "counter_example", + srcs = ["counter_example.cc"], + hdrs = ["counter_example.h"], + deps = [ + ":evaluator", + ":packet_set", + ":packet_transformer", + "@com_google_absl//absl/algorithm:container", + "@com_google_absl//absl/container:flat_hash_set", + "@com_google_absl//absl/log:check", + "@com_google_absl//absl/status", + "@com_google_absl//absl/status:statusor", + "@com_google_absl//absl/strings", + ], +) + cc_library( name = "analysis_engine", srcs = ["analysis_engine.cc"], hdrs = ["analysis_engine.h"], deps = [ + ":counter_example", ":frontend", ":packet_set", ":packet_transformer", + "@com_google_absl//absl/log:check", + "@com_google_absl//absl/status:statusor", ], ) @@ -301,6 +321,26 @@ cc_test( ], ) +# go/golden-test-with-coverage +cc_test( + name = "analysis_engine_counter_example_test_runner", + srcs = ["analysis_engine_counter_example_test_runner.cc"], + linkstatic = True, + deps = [ + ":analysis_engine", + ":counter_example", + ":frontend", + "@com_google_gutil//gutil:proto", + ], +) + +cmd_diff_test( + name = "analysis_engine_counter_example_diff_test", + actual_cmd = "$(execpath :analysis_engine_counter_example_test_runner)", + expected = ":analysis_engine_counter_example_test.expected", + tools = [":analysis_engine_counter_example_test_runner"], +) + cc_library( name = "packet_transformer", srcs = ["packet_transformer.cc"], diff --git a/netkat/analysis_engine.cc b/netkat/analysis_engine.cc index 0996018..c40e982 100644 --- a/netkat/analysis_engine.cc +++ b/netkat/analysis_engine.cc @@ -14,6 +14,9 @@ #include "netkat/analysis_engine.h" +#include "absl/log/check.h" +#include "absl/status/statusor.h" +#include "netkat/counter_example.h" #include "netkat/frontend.h" #include "netkat/packet_set.h" #include "netkat/packet_transformer.h" @@ -26,9 +29,21 @@ bool AnalysisEngine::CheckEquivalent(const Predicate& left, packet_transformer_manager_.Compile(Filter(right).ToProto()); } -bool AnalysisEngine::CheckEquivalent(const Policy& left, const Policy& right) { - return packet_transformer_manager_.Compile(left.ToProto()) == - packet_transformer_manager_.Compile(right.ToProto()); +SuccessOrCounterExample AnalysisEngine::CheckEquivalent(const Policy& left, + const Policy& right) { + PacketTransformerHandle left_packet_transformer = + packet_transformer_manager_.Compile(left.ToProto()); + PacketTransformerHandle right_packet_transformer = + packet_transformer_manager_.Compile(right.ToProto()); + if (left_packet_transformer == right_packet_transformer) { + return SuccessOrCounterExample(); + } + absl::StatusOr counter_example = + CounterExample::CreateEquivalenceCounterExample( + &packet_transformer_manager_, left_packet_transformer, + right_packet_transformer); + CHECK_OK(counter_example.status()); // Crash OK + return SuccessOrCounterExample(*counter_example); } bool AnalysisEngine::ProgramForwardsAnyPacket(const Policy& program, diff --git a/netkat/analysis_engine.h b/netkat/analysis_engine.h index 89ad63e..38f991c 100644 --- a/netkat/analysis_engine.h +++ b/netkat/analysis_engine.h @@ -21,6 +21,7 @@ #ifndef GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_ #define GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_ +#include "netkat/counter_example.h" #include "netkat/frontend.h" #include "netkat/packet_transformer.h" @@ -49,7 +50,24 @@ class AnalysisEngine { // Checks whether two policies are "equivalent", meaning they have the same // packets transformations, meaning Evaluate(left, packet) == Evaluate(right, // packet) for all packets. - bool CheckEquivalent(const Policy& left, const Policy& right); + // + // Returns a counter example for the given `left` and `right` policies if the + // policies are not equivalent, or `Success` if the policies are + // equivalent. The counter example is defined as: + // counter example := Pull(left - right, FullSet) or + // counter example := Pull(right - left, FullSet). + // + // Example: + // SuccessOrCounterExample result = CheckEquivalent(l,r); + // if(!result.IsSuccess()) { + // CounterExample counter_example = result->GetCounterExampleOrDie(); + // auto input_from_left_diff_right = + // counter_example.GetInputFromLeftDiffRightPolicies(); + // ... + // } + // + SuccessOrCounterExample CheckEquivalent(const Policy& left, + const Policy& right); // Returns whether any given packet, represented by the set of packets in // `packets`, is forwarded by `program`. A packet is considered "forwaded" if diff --git a/netkat/analysis_engine_counter_example_test.expected b/netkat/analysis_engine_counter_example_test.expected new file mode 100644 index 0000000..d30c356 --- /dev/null +++ b/netkat/analysis_engine_counter_example_test.expected @@ -0,0 +1,312 @@ +================================================================================ +Test case: left := Deny, right := Deny. No counter example found. +================================================================================ +-- Left Policy ----------------------------------------------------------------- +filter { + bool_constant { + } +} +-- Right Policy ---------------------------------------------------------------- +filter { + bool_constant { + } +} +-- Counter Example ------------------------------------------------------------- +No counter example found. +================================================================================ +Test case: left := Deny, right := Accept. Counter example found. +================================================================================ +-- Left Policy ----------------------------------------------------------------- +filter { + bool_constant { + } +} +-- Right Policy ---------------------------------------------------------------- +filter { + bool_constant { + value: true + } +} +-- Counter Example ------------------------------------------------------------- +Pull(Left - Right, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967295 [label="F" shape=box] +} + +Pull(Right - Left, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] +} + +Input/Output Packet Exists in Right, but not in Left: +- Input packet: {} +- Output packet: {} +================================================================================ +Test case: left := (a=2), right := (b=5). +================================================================================ +-- Left Policy ----------------------------------------------------------------- +filter { + match { + field: "a" + value: 2 + } +} +-- Right Policy ---------------------------------------------------------------- +filter { + match { + field: "b" + value: 5 + } +} +-- Counter Example ------------------------------------------------------------- +Pull(Left - Right, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 3 [label="a"] + 3 -> 2 [label="a==2; a:=2"] + 3 -> 4294967295 [style=dashed] + 2 [label="b"] + 2 -> 4294967295 [label="b==5"] + 2 -> 4294967294 [style=dashed] +} + +Pull(Right - Left, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 4 [label="a"] + 4 -> 4294967295 [label="a==2"] + 4 -> 1 [style=dashed] + 1 [label="b"] + 1 -> 4294967294 [label="b==5; b:=5"] + 1 -> 4294967295 [style=dashed] +} + +Input/Output Packet Exists in Left, but not in Right: +- Input packet: {a: 2} +- Output packet: {a: 2} +Input/Output Packet Exists in Right, but not in Left: +- Input packet: {b: 5} +- Output packet: {b: 5} +================================================================================ +Test case: left := (a=5), right := (a=5 && b=2). +================================================================================ +-- Left Policy ----------------------------------------------------------------- +filter { + match { + field: "a" + value: 5 + } +} +-- Right Policy ---------------------------------------------------------------- +filter { + and_op { + left { + match { + field: "a" + value: 5 + } + } + right { + match { + field: "b" + value: 2 + } + } + } +} +-- Counter Example ------------------------------------------------------------- +Pull(Left - Right, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 9 [label="a"] + 9 -> 8 [label="a==5; a:=5"] + 9 -> 4294967295 [style=dashed] + 8 [label="b"] + 8 -> 4294967295 [label="b==2"] + 8 -> 4294967294 [style=dashed] +} + +Pull(Right - Left, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967295 [label="F" shape=box] +} + +Input/Output Packet Exists in Left, but not in Right: +- Input packet: {a: 5} +- Output packet: {a: 5} +================================================================================ +Test case: left := (c=5), right := (c=5) || (d=2). +================================================================================ +-- Left Policy ----------------------------------------------------------------- +filter { + match { + field: "c" + value: 5 + } +} +-- Right Policy ---------------------------------------------------------------- +union_op { + left { + filter { + match { + field: "c" + value: 5 + } + } + } + right { + filter { + match { + field: "d" + value: 2 + } + } + } +} +-- Counter Example ------------------------------------------------------------- +Pull(Left - Right, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967295 [label="F" shape=box] +} + +Pull(Right - Left, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 13 [label="c"] + 13 -> 4294967295 [label="c==5"] + 13 -> 11 [style=dashed] + 11 [label="d"] + 11 -> 4294967294 [label="d==2; d:=2"] + 11 -> 4294967295 [style=dashed] +} + +Input/Output Packet Exists in Right, but not in Left: +- Input packet: {d: 2} +- Output packet: {d: 2} +================================================================================ +Test case: left := !(c=5), right := (c=5). +================================================================================ +-- Left Policy ----------------------------------------------------------------- +filter { + not_op { + negand { + match { + field: "c" + value: 5 + } + } + } +} +-- Right Policy ---------------------------------------------------------------- +filter { + match { + field: "c" + value: 5 + } +} +-- Counter Example ------------------------------------------------------------- +Pull(Left - Right, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 14 [label="c"] + 14 -> 4294967295 [label="c==5"] + 14 -> 4294967294 [style=dashed] +} + +Pull(Right - Left, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 10 [label="c"] + 10 -> 4294967294 [label="c==5; c:=5"] + 10 -> 4294967295 [style=dashed] +} + +Input/Output Packet Exists in Left, but not in Right: +- Input packet: {} +- Output packet: {} +Input/Output Packet Exists in Right, but not in Left: +- Input packet: {c: 5} +- Output packet: {c: 5} +================================================================================ +Test case: left := (f:=42), right := (g:=26). +================================================================================ +-- Left Policy ----------------------------------------------------------------- +modification { + field: "f" + value: 42 +} +-- Right Policy ---------------------------------------------------------------- +modification { + field: "g" + value: 26 +} +-- Counter Example ------------------------------------------------------------- +Pull(Left - Right, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 18 [label="f"] + 18 -> 17 [label="f==42; f:=42"] + 18 -> 4294967294 [label="f:=42" style=dashed] + 18 -> 4294967295 [style=dashed] + 17 [label="g"] + 17 -> 4294967295 [label="g==26"] + 17 -> 4294967294 [style=dashed] +} + +Pull(Right - Left, FullSet): +digraph { + node [fontsize = 14] + edge [fontsize = 12] + 4294967294 [label="T" shape=box] + 4294967295 [label="F" shape=box] + 20 [label="f"] + 20 -> 19 [label="f==42; f:=42"] + 20 -> 16 [style=dashed] + 19 [label="g"] + 19 -> 4294967295 [label="g==26"] + 19 -> 4294967294 [label="g:=26" style=dashed] + 19 -> 4294967295 [style=dashed] + 16 [label="g"] + 16 -> 4294967294 [label="g:=26" style=dashed] + 16 -> 4294967295 [style=dashed] +} + +Input/Output Packet Exists in Left, but not in Right: +- Input packet: {} +- Output packet: {f: 42} +- Input packet: {f: 42} +- Output packet: {f: 42} +Input/Output Packet Exists in Right, but not in Left: +- Input packet: {} +- Output packet: {g: 26} +- Input packet: {f: 42} +- Output packet: {g: 26,f: 42} diff --git a/netkat/analysis_engine_counter_example_test_runner.cc b/netkat/analysis_engine_counter_example_test_runner.cc new file mode 100644 index 0000000..afc285e --- /dev/null +++ b/netkat/analysis_engine_counter_example_test_runner.cc @@ -0,0 +1,115 @@ +// Copyright 2025 The NetKAT authors +// +// 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 +// +// https://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. +// ----------------------------------------------------------------------------- +// To generate the `analysis_engine_counter_example_test.expected` file, run: +// `bazel run +// //netkat:analysis_engine_counter_example_diff_test +// -- --update` + +#include +#include +#include + +#include "gutil/proto.h" +#include "netkat/analysis_engine.h" +#include "netkat/counter_example.h" +#include "netkat/frontend.h" + +namespace netkat { +namespace { + +constexpr char kBanner[] = + "==========================================================================" + "======\n"; +constexpr char kLeftPolicyHeader[] = + "-- Left Policy -----------------------------------------------------------" + "------\n"; +constexpr char kRightPolicyHeader[] = + "-- Right Policy ----------------------------------------------------------" + "------\n"; +constexpr char kCounterExampleHeader[] = + "-- Counter Example -------------------------------------------------------" + "------\n"; + +// A test case for the `ValidateTestRun` function. +struct TestCase { + // Human-readable description of this test case, for documentation. + std::string description; + Policy left_policy; + Policy right_policy; +}; + +std::vector TestCases() { + std::vector test_cases; + test_cases.push_back({ + .description = "left := Deny, right := Deny. No counter example found.", + .left_policy = Policy::Deny(), + .right_policy = Policy::Deny(), + }); + test_cases.push_back({ + .description = "left := Deny, right := Accept. Counter example found.", + .left_policy = Policy::Deny(), + .right_policy = Policy::Accept(), + }); + test_cases.push_back({ + .description = "left := (a=2), right := (b=5).", + .left_policy = Filter(Match("a", 2)), + .right_policy = Filter(Match("b", 5)), + }); + test_cases.push_back({ + .description = "left := (a=5), right := (a=5 && b=2).", + .left_policy = Filter(Match("a", 5)), + .right_policy = Filter(Match("a", 5) && Match("b", 2)), + }); + test_cases.push_back({ + .description = "left := (c=5), right := (c=5) || (d=2).", + .left_policy = Filter(Match("c", 5)), + .right_policy = Union(Filter(Match("c", 5)), Filter(Match("d", 2))), + }); + test_cases.push_back({ + .description = "left := !(c=5), right := (c=5).", + .left_policy = Filter(!Match("c", 5)), + .right_policy = Filter(Match("c", 5)), + }); + test_cases.push_back({ + .description = "left := (f:=42), right := (g:=26).", + .left_policy = Modify("f", 42), + .right_policy = Modify("g", 26), + }); + + return test_cases; +} + +void main() { + // This test needs a deterministic field interning order, and thus must start + // from a fresh manager. + AnalysisEngine analysis_engine; + for (const TestCase& test_case : TestCases()) { + SuccessOrCounterExample success_or_counter_example = + analysis_engine.CheckEquivalent(test_case.left_policy, + test_case.right_policy); + std::cout << kBanner << "Test case: " << test_case.description << "\n" + << kBanner; + std::cout << kLeftPolicyHeader + << gutil::PrintTextProto(test_case.left_policy.ToProto()); + std::cout << kRightPolicyHeader + << gutil::PrintTextProto(test_case.right_policy.ToProto()); + std::cout << kCounterExampleHeader << success_or_counter_example; + } +} + +} // namespace +} // namespace netkat + +int main() { netkat::main(); } diff --git a/netkat/analysis_engine_test.cc b/netkat/analysis_engine_test.cc index 462e2f0..a525308 100644 --- a/netkat/analysis_engine_test.cc +++ b/netkat/analysis_engine_test.cc @@ -60,45 +60,54 @@ TEST(AnalysisEngineTest, CheckEquivalentSmokeTests) { TEST(AnalysisEngineTest, CheckPolicyEquivalentSmokeTests) { AnalysisEngine analyzer; // Checks Deny and Accept are equivalent to themselves but not each other. - EXPECT_TRUE(analyzer.CheckEquivalent(Policy::Deny(), Policy::Deny())); - EXPECT_TRUE(analyzer.CheckEquivalent(Policy::Accept(), Policy::Accept())); - EXPECT_FALSE(analyzer.CheckEquivalent(Policy::Accept(), Policy::Deny())); - EXPECT_FALSE(analyzer.CheckEquivalent(Policy::Deny(), Policy::Accept())); + EXPECT_TRUE( + analyzer.CheckEquivalent(Policy::Deny(), Policy::Deny()).IsSuccess()); + EXPECT_TRUE( + analyzer.CheckEquivalent(Policy::Accept(), Policy::Accept()).IsSuccess()); + EXPECT_FALSE( + analyzer.CheckEquivalent(Policy::Accept(), Policy::Deny()).IsSuccess()); + EXPECT_FALSE( + analyzer.CheckEquivalent(Policy::Deny(), Policy::Accept()).IsSuccess()); // Checks different policies are equivalent to themselves but are not // equivalent to each other. const Policy p1 = Sequence(Filter(Match("port", 10)), Modify("port", 20)); const Policy p2 = Sequence(Filter(Match("switch", 42)), Modify("port", 21)); - EXPECT_TRUE(analyzer.CheckEquivalent(p1, p1)); - EXPECT_TRUE(analyzer.CheckEquivalent(p2, p2)); - EXPECT_FALSE(analyzer.CheckEquivalent(p1, p2)); - EXPECT_FALSE(analyzer.CheckEquivalent(p2, p1)); + EXPECT_TRUE(analyzer.CheckEquivalent(p1, p1).IsSuccess()); + EXPECT_TRUE(analyzer.CheckEquivalent(p2, p2).IsSuccess()); + EXPECT_FALSE(analyzer.CheckEquivalent(p1, p2).IsSuccess()); + EXPECT_FALSE(analyzer.CheckEquivalent(p2, p1).IsSuccess()); // Checks Union of Policies are commutative. - EXPECT_TRUE(analyzer.CheckEquivalent(Union(p1, p2), Union(p2, p1))); + EXPECT_TRUE( + analyzer.CheckEquivalent(Union(p1, p2), Union(p2, p1)).IsSuccess()); // Check Union of Policies are associative. const Policy p3 = Filter(Match("dst_mac", 30)); - EXPECT_TRUE(analyzer.CheckEquivalent(Union(p1, Union(p2, p3)), - Union(Union(p1, p2), p3))); + EXPECT_TRUE( + analyzer + .CheckEquivalent(Union(p1, Union(p2, p3)), Union(Union(p1, p2), p3)) + .IsSuccess()); // Some Sequence of Policies are not commutative: modifying the same field // with different values in different order would result in different // policies. const Policy modify_port_1 = Modify("port", 10); const Policy modify_port_2 = Modify("port", 20); - EXPECT_FALSE( - analyzer.CheckEquivalent(Sequence(modify_port_1, modify_port_2), - Sequence(modify_port_2, modify_port_1))); + EXPECT_FALSE(analyzer + .CheckEquivalent(Sequence(modify_port_1, modify_port_2), + Sequence(modify_port_2, modify_port_1)) + .IsSuccess()); // Sequence(p1, p2) can be equivalent to Sequence(p2, p1) depending // on what's p1 and p2: e.g., modifying different fields in different order // would result in equivalent policies. // This is the PA-MOD-MOD-COMM axiom in the NetKAT paper. const Policy modify_dst_mac = Modify("dst_mac", 1); - EXPECT_TRUE( - analyzer.CheckEquivalent(Sequence(modify_dst_mac, modify_port_1), - Sequence(modify_port_1, modify_dst_mac))); + EXPECT_TRUE(analyzer + .CheckEquivalent(Sequence(modify_dst_mac, modify_port_1), + Sequence(modify_port_1, modify_dst_mac)) + .IsSuccess()); } // A netkat::Policy representing the given topology @@ -115,17 +124,21 @@ TEST(AnalysisEngineTest, TopologyTraversalIsAccepted) { Policy traverse_topo_from_s1 = Sequence( Modify("switch", 1), Iterate(topology), Filter(Match("switch", 3))); EXPECT_TRUE( - analyzer.CheckEquivalent(traverse_topo_from_s1, Modify("switch", 3))); + analyzer.CheckEquivalent(traverse_topo_from_s1, Modify("switch", 3)) + .IsSuccess()); Policy traverse_topo_from_s2 = Sequence( Modify("switch", 2), Iterate(topology), Filter(Match("switch", 3))); EXPECT_TRUE( - analyzer.CheckEquivalent(traverse_topo_from_s2, Modify("switch", 3))); + analyzer.CheckEquivalent(traverse_topo_from_s2, Modify("switch", 3)) + .IsSuccess()); Policy traverse_from_non_existing_switch = Sequence( Modify("switch", 42), Iterate(topology), Filter(Match("switch", 3))); - EXPECT_TRUE(analyzer.CheckEquivalent(traverse_from_non_existing_switch, - Policy::Deny())); + EXPECT_TRUE( + analyzer + .CheckEquivalent(traverse_from_non_existing_switch, Policy::Deny()) + .IsSuccess()); } // TODO(anthonyroy): Consider fuzzing some of these tests. Doing so requires a diff --git a/netkat/counter_example.cc b/netkat/counter_example.cc new file mode 100644 index 0000000..885e70e --- /dev/null +++ b/netkat/counter_example.cc @@ -0,0 +1,268 @@ +// Copyright 2025 The NetKAT authors +// +// 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 +// +// https://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 "netkat/counter_example.h" + +#include +#include +#include +#include + +#include "absl/algorithm/container.h" +#include "absl/log/check.h" +#include "absl/status/status.h" +#include "absl/status/statusor.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/str_join.h" +#include "netkat/evaluator.h" +#include "netkat/packet_set.h" +#include "netkat/packet_transformer.h" + +namespace netkat { + +namespace { + +void StableSortOutputPacketsToInputPacket( + std::vector>& + output_packets_to_input_packet) { + absl::c_stable_sort( + output_packets_to_input_packet, + [](const std::pair& left, + const std::pair& right) { + // Create a canonical representation for the left and right Packet by + // sorting its key-value pairs. + std::vector> left_packet_vec( + left.first.begin(), left.first.end()); + absl::c_sort(left_packet_vec); + std::vector> right_packet_vec( + right.first.begin(), right.first.end()); + absl::c_sort(right_packet_vec); + + // Compare the canonical representations of the Packets. + if (left_packet_vec != right_packet_vec) { + return left_packet_vec < right_packet_vec; + } + + // If the Packets are identical, compare the OutputPackets. + // A canonical representation for a set of Packets is a sorted vector + // of their canonical representations. + auto create_canonical_rep = [](const OutputPackets& output_packets) { + std::vector>> vec_of_vecs; + vec_of_vecs.reserve(output_packets.size()); + for (const auto& packet : output_packets) { + std::vector> packet_vec(packet.begin(), + packet.end()); + absl::c_sort(packet_vec); + vec_of_vecs.push_back(std::move(packet_vec)); + } + absl::c_sort(vec_of_vecs); + return vec_of_vecs; + }; + + return create_canonical_rep(left.second) < + create_canonical_rep(right.second); + }); +} + +std::vector> GetInputPacketToOutputPackets( + PacketTransformerManager& packet_transformer_manager, + const PacketTransformerHandle& packet_transformer, + const PacketSetHandle& input_packet_set) { + std::vector> input_to_output_packets; + + // TODO: b/463710729 - Remove comment once GetConcretePackets returns a + // comprehensive set of packets. + // Currently, GetConcretePackets returns a set of packets that are not + // guaranteed to be exhaustive. + std::vector concrete_packets = + packet_transformer_manager.GetPacketSetManager().GetConcretePackets( + input_packet_set); + input_to_output_packets.reserve(concrete_packets.size()); + for (Packet& input_packet : concrete_packets) { + input_to_output_packets.push_back(std::make_pair( + input_packet, + packet_transformer_manager.Run(packet_transformer, input_packet))); + } + StableSortOutputPacketsToInputPacket(input_to_output_packets); + return input_to_output_packets; +} + +} // namespace + +absl::StatusOr CounterExample::CreateEquivalenceCounterExample( + PacketTransformerManager* packet_transformer_manager, + PacketTransformerHandle left_policy, PacketTransformerHandle right_policy) { + if (left_policy == right_policy) { + return absl::InvalidArgumentError( + "Left and right policies are the same, cannot create a counter " + "example."); + } + if (packet_transformer_manager == nullptr) { + return absl::InvalidArgumentError( + "Packet transformer manager is null, cannot create a counter example."); + } + return CounterExample(packet_transformer_manager, left_policy, right_policy); +} + +CounterExample::CounterExample( + PacketTransformerManager* packet_transformer_manager, + PacketTransformerHandle left_packet_transformer, + PacketTransformerHandle right_packet_transformer) + : packet_transformer_manager_(packet_transformer_manager), + left_packet_transformer_(left_packet_transformer), + right_packet_transformer_(right_packet_transformer) { + // Compute the set of packets that are in L but not R, and vice versa. + PacketTransformerHandle left_diff_right_transformer = + packet_transformer_manager_->Difference(left_packet_transformer, + right_packet_transformer); + PacketTransformerHandle right_diff_left_transformer = + packet_transformer_manager_->Difference(right_packet_transformer, + left_packet_transformer); + + // Compute the input packet sets to the difference of the left and right + // policies and vice versa. + PacketSetHandle fullset = + packet_transformer_manager_->GetPacketSetManager().FullSet(); + input_packets_in_left_but_not_right_ = + packet_transformer_manager_->Pull(left_diff_right_transformer, fullset); + input_packets_in_right_but_not_left_ = + packet_transformer_manager_->Pull(right_diff_left_transformer, fullset); +} + +PacketTransformerHandle CounterExample::GetLeftTransformer() const { + return left_packet_transformer_; +} +PacketTransformerHandle CounterExample::GetRightTransformer() const { + return right_packet_transformer_; +} + +PacketSetHandle CounterExample::GetInputPacketsInLeftButNotRight() const { + return input_packets_in_left_but_not_right_; +} +PacketSetHandle CounterExample::GetInputPacketsInRightButNotLeft() const { + return input_packets_in_right_but_not_left_; +} + +PacketSetHandle CounterExample::GetInputPacketsInBoth() const { + CHECK(packet_transformer_manager_ != nullptr); // Crash OK + return packet_transformer_manager_->GetPacketSetManager().Or( + input_packets_in_left_but_not_right_, + input_packets_in_right_but_not_left_); +} + +std::string CounterExample::GetInputFromLeftButNotRightAsDotOrDie() const { + CHECK(packet_transformer_manager_ != nullptr); // Crash OK + PacketTransformerHandle left_diff_right_transformer = + packet_transformer_manager_->Difference(left_packet_transformer_, + right_packet_transformer_); + return packet_transformer_manager_->ToDot(left_diff_right_transformer); +} + +std::string CounterExample::GetInputFromRightButNotLeftAsDotOrDie() const { + CHECK(packet_transformer_manager_ != nullptr); // Crash OK + PacketTransformerHandle right_diff_left_transformer = + packet_transformer_manager_->Difference(right_packet_transformer_, + left_packet_transformer_); + return packet_transformer_manager_->ToDot(right_diff_left_transformer); +} + +std::vector> +CounterExample::GetInputPacketToOutputPacketsForLeftDiffRightPoliciesOrDie() + const { + CHECK(packet_transformer_manager_ != nullptr); + PacketTransformerHandle left_diff_right_transformer = + packet_transformer_manager_->Difference(left_packet_transformer_, + right_packet_transformer_); + return GetInputPacketToOutputPackets(*packet_transformer_manager_, + left_diff_right_transformer, + input_packets_in_left_but_not_right_); +} + +std::vector> +CounterExample::GetInputPacketToOutputPacketsForRightDiffLeftPoliciesOrDie() + const { + CHECK(packet_transformer_manager_ != nullptr); + PacketTransformerHandle right_diff_left_transformer = + packet_transformer_manager_->Difference(right_packet_transformer_, + left_packet_transformer_); + return GetInputPacketToOutputPackets(*packet_transformer_manager_, + right_diff_left_transformer, + input_packets_in_right_but_not_left_); +} + +template +void AbslStringify(Sink& sink, const CounterExample& counter_example) { + absl::Format(&sink, "Pull(Left - Right, FullSet):\n%s\n", + counter_example.GetInputFromLeftButNotRightAsDotOrDie()); + absl::Format(&sink, "Pull(Right - Left, FullSet):\n%s\n", + counter_example.GetInputFromRightButNotLeftAsDotOrDie()); + if (!counter_example + .GetInputPacketToOutputPacketsForLeftDiffRightPoliciesOrDie() + .empty()) { + absl::Format(&sink, + "Input/Output Packet Exists in Left, but not in Right:\n"); + } + for (const auto& [input, output] : + counter_example + .GetInputPacketToOutputPacketsForLeftDiffRightPoliciesOrDie()) { + absl::Format(&sink, "- Input packet: {%s}\n", + absl::StrJoin(input, ",", absl::PairFormatter(": "))); + for (const auto& output_packet : output) { + absl::Format( + &sink, "- Output packet: {%s}\n", + absl::StrJoin(output_packet, ",", absl::PairFormatter(": "))); + } + } + if (!counter_example + .GetInputPacketToOutputPacketsForRightDiffLeftPoliciesOrDie() + .empty()) { + absl::Format(&sink, + "Input/Output Packet Exists in Right, but not in Left:\n"); + } + for (const auto& [input, output] : + counter_example + .GetInputPacketToOutputPacketsForRightDiffLeftPoliciesOrDie()) { + absl::Format(&sink, "- Input packet: {%s}\n", + absl::StrJoin(input, ",", absl::PairFormatter(": "))); + for (const auto& output_packet : output) { + absl::Format( + &sink, "- Output packet: {%s}\n", + absl::StrJoin(output_packet, ",", absl::PairFormatter(": "))); + } + } +} + +std::ostream& operator<<(std::ostream& os, + const CounterExample& counter_example) { + return os << absl::StrCat(counter_example); +} + +template +void AbslStringify(Sink& sink, + const SuccessOrCounterExample& success_or_counter_example) { + if (success_or_counter_example.IsSuccess()) { + absl::Format(&sink, "No counter example found.\n"); + } else { + absl::Format(&sink, "%v", + success_or_counter_example.GetCounterExampleOrDie()); + } +} + +std::ostream& operator<<( + std::ostream& os, + const SuccessOrCounterExample& success_or_counter_example) { + return os << absl::StrCat(success_or_counter_example); +} + +} // namespace netkat diff --git a/netkat/counter_example.h b/netkat/counter_example.h new file mode 100644 index 0000000..e7036c3 --- /dev/null +++ b/netkat/counter_example.h @@ -0,0 +1,137 @@ +// Copyright 2025 The NetKAT authors +// +// 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 +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef GOOGLE_NETKAT_NETKAT_COUNTER_EXAMPLE_H_ +#define GOOGLE_NETKAT_NETKAT_COUNTER_EXAMPLE_H_ + +#include +#include +#include +#include +#include + +#include "absl/container/flat_hash_set.h" +#include "absl/log/check.h" +#include "netkat/evaluator.h" +#include "netkat/packet_set.h" +#include "netkat/packet_transformer.h" + +namespace netkat { + +using OutputPackets = absl::flat_hash_set; + +// A counter example contains the difference between two policies and the +// corresponding input/output packets that belong to one policy, but not the +// other and vice versa. +// +// Note: The lifetime of `CounterExample` is dependent on the +// lifetime of the `PacketTransformerManager` that created it. +class CounterExample { + public: + static absl::StatusOr CreateEquivalenceCounterExample( + PacketTransformerManager* packet_transformer_manager, + PacketTransformerHandle left_policy, + PacketTransformerHandle right_policy); + + PacketTransformerHandle GetLeftTransformer() const; + PacketTransformerHandle GetRightTransformer() const; + + // Returns the input packet set that holds in the left transformer, but not + // the right transformer. The counterexample is represented by the following: + // PacketSetHandle := Pull(left policy - right policy, FullSet). + PacketSetHandle GetInputPacketsInLeftButNotRight() const; + + // Returns the input packet set that holds in the right transformer, but not + // the left transformer. The counterexample is represented by the following: + // PacketSetHandle := Pull(right policy - left policy, FullSet). + PacketSetHandle GetInputPacketsInRightButNotLeft() const; + + // Returns the set of input packets that are in both left and right policies. + PacketSetHandle GetInputPacketsInBoth() const; + + // Returns the packet set's dot representation for the counterexample or die. + // The counterexample is represented by the following: + // PacketSetHandle := Pull(left policy - right policy, FullSet). + std::string GetInputFromLeftButNotRightAsDotOrDie() const; + + // Returns the packet set's dot representation for the counterexample or die. + // The counterexample is represented by the following: + // PacketSetHandle := Pull(right policy - left policy, FullSet). + std::string GetInputFromRightButNotLeftAsDotOrDie() const; + + // Returns a map from input packets to output packets for the counterexample + // or die. The set of input packets is represented by the following: + // PacketSetHandle := Pull(left policy - right policy, FullSet). + // The set of outputs are generated by sending the input packets through + // corresponding transformer. + std::vector> + GetInputPacketToOutputPacketsForLeftDiffRightPoliciesOrDie() const; + + // Returns a map from input packets to output packets for the counterexample + // or die. The set of input packets is represented by the following: + // PacketSetHandle := Pull(right policy - left policy, FullSet). + // The set of outputs are generated by sending the input packets through + // corresponding transformer. + std::vector> + GetInputPacketToOutputPacketsForRightDiffLeftPoliciesOrDie() const; + + private: + CounterExample(PacketTransformerManager* packet_transformer_manager, + PacketTransformerHandle left_packet_transformer, + PacketTransformerHandle right_packet_transformer); + + PacketTransformerManager* packet_transformer_manager_; + PacketTransformerHandle left_packet_transformer_; + PacketTransformerHandle right_packet_transformer_; + PacketSetHandle input_packets_in_left_but_not_right_; + PacketSetHandle input_packets_in_right_but_not_left_; +}; + +template +void AbslStringify(Sink& sink, const CounterExample& counter_example); +std::ostream& operator<<(std::ostream& os, + const CounterExample& counter_example); + +// A success or counter example is a wrapper around a counter example. +// If the two policies compared in the analysis engine are the same, the +// SuccessOrCounterExample should have no counter example and return true when +// IsSuccess is called. Otherwise, if IsSuccess returns false, then the +// SuccessOrCounterExample will contain a counter example. +class SuccessOrCounterExample { + public: + SuccessOrCounterExample() = default; + explicit SuccessOrCounterExample(CounterExample counter_example) + : counter_example_(std::move(counter_example)) {} + + bool IsSuccess() const { return !counter_example_.has_value(); } + + const CounterExample& GetCounterExampleOrDie() const { + CHECK(counter_example_.has_value()); + return *counter_example_; + } + + private: + std::optional counter_example_; +}; + +template +void AbslStringify(Sink& sink, + const SuccessOrCounterExample& success_or_counter_example); +std::ostream& operator<<( + std::ostream& os, + const SuccessOrCounterExample& success_or_counter_example); + +} // namespace netkat + +#endif // GOOGLE_NETKAT_NETKAT_COUNTER_EXAMPLE_H_ diff --git a/netkat/switch_test.cc b/netkat/switch_test.cc index 73ffe91..99c4b84 100644 --- a/netkat/switch_test.cc +++ b/netkat/switch_test.cc @@ -81,9 +81,11 @@ TEST(NetkatSwitchTest, SingleStageSwitchReturnsCorrectPolicy) { EXPECT_CALL(*mock_stage, CleanUp()).WillOnce(Return(Modify("vrf", -1))); netkat::AnalysisEngine engine; - EXPECT_TRUE(engine.CheckEquivalent( - nk_switch.GetPolicy(), - Sequence(Filter(Match("vlan_id", 1)), Modify("vrf", -1)))); + EXPECT_TRUE(engine + .CheckEquivalent( + nk_switch.GetPolicy(), + Sequence(Filter(Match("vlan_id", 1)), Modify("vrf", -1))) + .IsSuccess()); } TEST(NetkatSwitchTest, MultiStageSwitchReturnsCorrectPolicy) { @@ -109,10 +111,13 @@ TEST(NetkatSwitchTest, MultiStageSwitchReturnsCorrectPolicy) { // The VLAN sets a VRF, the VRF remaps the VLAN. The resulting policy should // be as-if the VLAN is simply remapped... plus the metadata cleanup. netkat::AnalysisEngine engine; - EXPECT_TRUE(engine.CheckEquivalent( - nk_switch.GetPolicy(), - Sequence(Filter(Match("vlan_id", 1)), Modify("vlan_id", 2), - Modify("vrf", -1), Modify("rnd_tag", -1)))); + EXPECT_TRUE( + engine + .CheckEquivalent( + nk_switch.GetPolicy(), + Sequence(Filter(Match("vlan_id", 1)), Modify("vlan_id", 2), + Modify("vrf", -1), Modify("rnd_tag", -1))) + .IsSuccess()); } } // namespace diff --git a/netkat/table_test.cc b/netkat/table_test.cc index b69fa8a..f6fcb64 100644 --- a/netkat/table_test.cc +++ b/netkat/table_test.cc @@ -215,7 +215,8 @@ TEST(NetkatTable, MergeWithSameTableIsSemanticNoop) { AnalysisEngine engine; EXPECT_TRUE( - engine.CheckEquivalent(merged_table->GetPolicy(), table.GetPolicy())); + engine.CheckEquivalent(merged_table->GetPolicy(), table.GetPolicy()) + .IsSuccess()); } TEST(NetkatTable, MergeWithCopiedTableIsEquivalentToMergeWithSameTable) { @@ -235,10 +236,14 @@ TEST(NetkatTable, MergeWithCopiedTableIsEquivalentToMergeWithSameTable) { NetkatTable::Merge(copy_ctor_table, copy_ctor_table)); AnalysisEngine engine; - EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), - copy_assign_merged_table->GetPolicy())); - EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), - copy_ctor_merged_table->GetPolicy())); + EXPECT_TRUE(engine + .CheckEquivalent(merged_table->GetPolicy(), + copy_assign_merged_table->GetPolicy()) + .IsSuccess()); + EXPECT_TRUE(engine + .CheckEquivalent(merged_table->GetPolicy(), + copy_ctor_merged_table->GetPolicy()) + .IsSuccess()); } TEST(NetkatTable, MergeWithDifferentTablesIsCorrect) { @@ -263,12 +268,12 @@ TEST(NetkatTable, MergeWithDifferentTablesIsCorrect) { Sequence(Filter(Match("port", 2)), Modify("vrf", 3)), Sequence(Filter(Match("port", 3)), Modify("vrf", 4))); AnalysisEngine engine; - EXPECT_TRUE( - engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy)); + EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy) + .IsSuccess()); ASSERT_OK_AND_ASSIGN(merged_table, NetkatTable::Merge(table2, table1)); - EXPECT_TRUE( - engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy)); + EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy) + .IsSuccess()); } TEST(NetkatTable, MergeWithNonDeterminismIsError) {