Start symbolic packet implementation.

PiperOrigin-RevId: 698838599

netkat/BUILD.bazel

@@ -26,3 +26,23 @@ cc_test(
         "@com_google_googletest//:gtest_main",
     ],
 )
+
+cc_library(
+    name = "symbolic_packet",
+    hdrs = ["symbolic_packet.h"],
+    deps = [
+        ":netkat_cc_proto",
+        "@com_google_absl//absl/strings:str_format",
+    ],
+)
+
+cc_test(
+    name = "symbolic_packet_test",
+    srcs = ["symbolic_packet_test.cc"],
+    deps = [
+        ":netkat_cc_proto",
+        ":symbolic_packet",
+        "@com_google_fuzztest//fuzztest",
+        "@com_google_googletest//:gtest_main",
+    ],
+)

netkat/symbolic_packet.h

@@ -0,0 +1,113 @@
+// Copyright 2024 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_SYMBOLIC_PACKET_H_
+#define GOOGLE_NETKAT_NETKAT_SYMBOLIC_PACKET_H_
+
+#include <cstdint>
+#include <limits>
+#include <utility>
+
+#include "absl/strings/str_format.h"
+#include "netkat/netkat.pb.h"
+
+namespace netkat {
+
+// TODO(smolkaj): Implement this.
+class SymbolicPacketManager;
+
+// A "Symbolic Packet" is a data structure that represents a (possibly large or
+// infinite) set of concrete packets, typically compactly and efficiently.
+//
+// Compared to NetKAT predicates, which semantically also represent sets of
+// packets, symbolic packets have a few advantages:
+// * Cheap to store, copy, hash, and compare: O(1)
+// * Cheap to check set equality: O(1)
+// * Cheap to check set membership and set containment: O(# packet fields)
+//
+// NOTES ON THE API:
+// * The majoriy of operations on `SymbolicPacket`s are defined as methods on
+//   `SymbolicPacketManager`.
+// * Each `SymbolicPacket` is implicitly associated with the
+//  `SymbolicPacketManager` object that created it; using it with a different
+//  `SymbolicPacketManager` object is undefined behavior.
+// * `EmptySet()` and `FullSet()` are exceptions to the above rule in that they
+//   work with any `SymbolicPacketManager` object.
+//
+// CAUTION: This implementation has NOT yet been optimized for performance.
+// Performance can likely ne improved significantly, e.g. as follows:
+// * Profiling and benchmarking to identify inefficiencies.
+// * Using standard techniques described in the literature on Binary Decision
+//   Diagrams (BDDs) and other decision diagrams, e.g. in the paper
+//   "Efficient Implementation of a BDD Package".
+class SymbolicPacket {
+ public:
+  // Default constructor: the empty set of packets.
+  SymbolicPacket() = default;
+
+  // The symbolic packet representing the empty set of packets.
+  static SymbolicPacket EmptySet() { return SymbolicPacket(kEmptySetIndex); }
+
+  // The symbolic packet representing the full set of packets.
+  static SymbolicPacket FullSet() { return SymbolicPacket(kFullSetIndex); }
+
+  // Returns true iff this symbolic packet represents the empty set of packets.
+  bool IsEmptySet() const { return node_index_ == kEmptySetIndex; }
+
+  // Returns true iff this symbolic packet represents the full set of packets.
+  bool IsFullSet() const { return node_index_ == kFullSetIndex; }
+
+  // Two symbolic packets compare equal iff they represent the same set of
+  // concrete packets. Comparison is O(1), thanks to a canonical representation.
+  friend auto operator<=>(SymbolicPacket a, SymbolicPacket b) = default;
+
+  // Hashing, see https://abseil.io/docs/cpp/guides/hash.
+  template <typename H>
+  friend H AbslHashValue(H h, SymbolicPacket packet) {
+    return H::combine(std::move(h), packet.node_index_);
+  }
+
+  // Formatting, see https://abseil.io/docs/cpp/guides/abslstringify.
+  template <typename Sink>
+  friend void AbslStringify(Sink& sink, SymbolicPacket packet) {
+    if (packet.IsEmptySet()) {
+      absl::Format(&sink, "SymPkt<false>");
+    } else if (packet.IsFullSet()) {
+      absl::Format(&sink, "SymPkt<true>");
+    } else {
+      absl::Format(&sink, "SymPkt<%d>", packet.node_index_);
+    }
+  }
+
+ private:
+  // In memory, a `SymbolicPacket` is just a `uint32_t` that indexes into
+  // `SymbolicPacketManager`, making it cheap to store, copy, hash, and compare.
+  //
+  // The `node_index_` is either:
+  // * `kEmptySetIndex`: the empty set of packets.
+  // * `kFullSetIndex`: the full set of packets.
+  // * Otherwise, an index into the `nodes_` vector in `SymbolicPacketManager`.
+  uint32_t node_index_ = kEmptySetIndex;
+  static constexpr uint32_t kEmptySetIndex =
+      std::numeric_limits<uint32_t>::max();
+  static constexpr uint32_t kFullSetIndex =
+      std::numeric_limits<uint32_t>::max() - 1;
+  explicit SymbolicPacket(uint32_t node_index) : node_index_(node_index) {}
+  friend class SymbolicPacketManager;
+};
+
+}  // namespace netkat
+
+#endif  // GOOGLE_NETKAT_NETKAT_SYMBOLIC_PACKET_H_

netkat/symbolic_packet_test.cc

@@ -0,0 +1,40 @@
+// Copyright 2024 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/symbolic_packet.h"
+
+#include "gtest/gtest.h"
+
+namespace netkat {
+namespace {
+
+TEST(SymbolicPacketTest, DefaultConstructorYieldsEmptySet) {
+  EXPECT_TRUE(SymbolicPacket().IsEmptySet());
+}
+
+TEST(SymbolicPacketTest, EmptySetIsEmptySet) {
+  EXPECT_TRUE(SymbolicPacket::EmptySet().IsEmptySet());
+}
+
+TEST(SymbolicPacketTest, FullSetIsFullSet) {
+  EXPECT_TRUE(SymbolicPacket::FullSet().IsFullSet());
+}
+
+TEST(SymbolicPacketTest, EmptySetDoesNotEqualFullSet) {
+  EXPECT_NE(SymbolicPacket::EmptySet(), SymbolicPacket::FullSet());
+}
+
+}  // namespace
+}  // namespace netkat