-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[NetKAT] Add pretty printer for SymbolicPackets, for debugging only.
PiperOrigin-RevId: 703290191
- Loading branch information
1 parent
24ec2d0
commit fbb09c1
Showing
12 changed files
with
1,336 additions
and
115 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
// 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/interned_field.h" | ||
|
||
#include <string> | ||
|
||
#include "absl/log/check.h" | ||
#include "absl/status/status.h" | ||
#include "absl/strings/string_view.h" | ||
#include "gutil/status.h" | ||
|
||
namespace netkat { | ||
|
||
InternedField InternedFieldManager::InternField(absl::string_view field_name) { | ||
auto [it, inserted] = interned_field_by_name_.try_emplace( | ||
field_name, InternedField(field_names_.size())); | ||
if (inserted) field_names_.push_back(std::string(field_name)); | ||
return it->second; | ||
} | ||
|
||
std::string InternedFieldManager::GetFieldNameOrDie(InternedField field) const { | ||
CHECK_LT(field.index_, field_names_.size()); // Crash ok | ||
return field_names_[field.index_]; | ||
} | ||
|
||
absl::Status InternedFieldManager::CheckInternalInvariants() const { | ||
for (int i = 0; i < field_names_.size(); ++i) { | ||
auto it = interned_field_by_name_.find(field_names_[i]); | ||
RET_CHECK(it != interned_field_by_name_.end()); | ||
RET_CHECK(it->second.index_ == i); | ||
} | ||
|
||
for (const auto& [name, field] : interned_field_by_name_) { | ||
RET_CHECK(field.index_ < field_names_.size()); | ||
RET_CHECK(field_names_[field.index_] == name); | ||
} | ||
|
||
return absl::OkStatus(); | ||
} | ||
|
||
} // namespace netkat |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,117 @@ | ||
// 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. | ||
// | ||
// ----------------------------------------------------------------------------- | ||
// File: interned_field.h | ||
// ----------------------------------------------------------------------------- | ||
// | ||
// A module for "interning" (aka hash-consing) NetKAT packet fields, see | ||
// https://en.wikipedia.org/wiki/String_interning. This makes it cheap to | ||
// compare, hash, copy and store packet fields (small constant time/space). | ||
|
||
#ifndef GOOGLE_NETKAT_NETKAT_INTERNED_FIELD_H_ | ||
#define GOOGLE_NETKAT_NETKAT_INTERNED_FIELD_H_ | ||
|
||
#include <compare> | ||
#include <cstdint> | ||
#include <string> | ||
#include <utility> | ||
#include <vector> | ||
|
||
#include "absl/container/flat_hash_map.h" | ||
#include "absl/status/status.h" | ||
#include "absl/strings/str_format.h" | ||
#include "absl/strings/string_view.h" | ||
|
||
namespace netkat { | ||
|
||
// An "interned" (aka hash-consed) NetKAT packet field, e.g. "dst_ip". | ||
// | ||
// Technically, a lightweight handle (16 bits) that is very cheap (O(1)) to | ||
// copy, store, hash, and compare. Handles can only be created by an | ||
// `InternedFieldManager` object, which owns the field name (e.g. "dst_ip") | ||
// associated with the handle. | ||
// | ||
// CAUTION: Each `InternedField` is implicitly associated with the manager | ||
// object that created it; using it with a different manager object has | ||
// undefined behavior. | ||
class [[nodiscard]] InternedField { | ||
public: | ||
// `InternedField`s can only be created by `InternedFieldManager`. | ||
InternedField() = delete; | ||
friend class InternedFieldManager; | ||
|
||
// O(1) comparison, thanks to interning/hash-consing. | ||
friend auto operator<=>(InternedField a, InternedField b) = default; | ||
|
||
// Hashing, see https://abseil.io/docs/cpp/guides/hash. | ||
template <typename H> | ||
friend H AbslHashValue(H h, InternedField field) { | ||
return H::combine(std::move(h), field.index_); | ||
} | ||
|
||
// Formatting, see https://abseil.io/docs/cpp/guides/abslstringify. | ||
template <typename Sink> | ||
friend void AbslStringify(Sink& sink, InternedField field) { | ||
absl::Format(&sink, "InternedField<%d>", field.index_); | ||
} | ||
|
||
private: | ||
// An index into the `field_names_` vector of the `InternedFieldManager` | ||
// object associated with this `InternedField`: `field_names_[index_]` is the | ||
// name of the field. The index is otherwise arbitrary and meaningless. | ||
// | ||
// We use a 16-bit index as a tradeoff between minimizing memory usage while | ||
// supporting sufficiently many fields. We expect 100s, but not more than | ||
// 2^16 ~= 65k fields. | ||
uint16_t index_; | ||
explicit InternedField(uint16_t index) : index_(index) {} | ||
}; | ||
|
||
// Protect against regressions in the memory layout, as it affects performance. | ||
static_assert(sizeof(InternedField) <= 2); | ||
|
||
// An "arena" for interning NetKAT packet fields, owning the memory associated | ||
// with the interned fields. | ||
class InternedFieldManager { | ||
public: | ||
InternedFieldManager() = default; | ||
|
||
// Returns an interned representation of field with the given name. | ||
InternedField InternField(absl::string_view field_name); | ||
|
||
// Returns the name of the given interned field, or crashes if the interned | ||
// field was not created by this manager object. | ||
std::string GetFieldNameOrDie(InternedField field) const; | ||
|
||
// Dynamically checks all class invariants. Exposed for testing only. | ||
absl::Status CheckInternalInvariants() const; | ||
|
||
private: | ||
// All field names interned by this manager object. The name of an interned | ||
// field `f` created by this object is `field_names_[f.index_]`. | ||
std::vector<std::string> field_names_; | ||
|
||
// A so called "unique table" to ensure each field name is added to | ||
// `field_names_` at most once, and thus is represented by a unique index into | ||
// that vector. | ||
// | ||
// Invariant: | ||
// `interned_field_by_name_[n] == f` iff `field_names_[f.index_] == n`. | ||
absl::flat_hash_map<std::string, InternedField> interned_field_by_name_; | ||
}; | ||
|
||
} // namespace netkat | ||
|
||
#endif // GOOGLE_NETKAT_NETKAT_INTERNED_FIELD_H_ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,76 @@ | ||
// 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/interned_field.h" | ||
|
||
#include "absl/base/no_destructor.h" | ||
#include "absl/container/flat_hash_set.h" | ||
#include "absl/strings/str_cat.h" | ||
#include "gmock/gmock.h" | ||
#include "gtest/gtest.h" | ||
#include "gutil/status_matchers.h" | ||
|
||
namespace netkat { | ||
|
||
namespace { | ||
|
||
using testing::StartsWith; | ||
|
||
// We use a global manager object across all tests to exercise statefulness. | ||
InternedFieldManager& Manager() { | ||
static absl::NoDestructor<InternedFieldManager> manager; | ||
return *manager; | ||
} | ||
|
||
// After executing all tests, we check once that no invariants are violated. | ||
class CheckInternedFieldManagerInvariantsOnTearDown | ||
: public testing::Environment { | ||
public: | ||
~CheckInternedFieldManagerInvariantsOnTearDown() override {} | ||
void SetUp() override {} | ||
void TearDown() override { ASSERT_OK(Manager().CheckInternalInvariants()); } | ||
}; | ||
testing::Environment* const foo_env = testing::AddGlobalTestEnvironment( | ||
new CheckInternedFieldManagerInvariantsOnTearDown); | ||
|
||
TEST(InternedFieldManagerTest, AbslStringifyWorkst) { | ||
EXPECT_THAT(absl::StrCat(Manager().InternField("foo")), | ||
StartsWith("InternedField")); | ||
} | ||
|
||
TEST(InternedFieldManagerTest, AbslHashValueWorks) { | ||
absl::flat_hash_set<InternedField> set = { | ||
Manager().InternField("foo"), | ||
Manager().InternField("bar"), | ||
}; | ||
EXPECT_EQ(set.size(), 2); | ||
} | ||
|
||
TEST(InternedFieldManagerTest, InternFieldReturnsSameFieldForSameName) { | ||
EXPECT_EQ(Manager().InternField("foo"), Manager().InternField("foo")); | ||
} | ||
|
||
TEST(InternedFieldManagerTest, | ||
InternFieldReturnsDifferentFieldForDifferentNames) { | ||
EXPECT_NE(Manager().InternField("foo"), Manager().InternField("bar")); | ||
} | ||
|
||
TEST(InternedFieldManagerTest, GetFieldNameOrDieReturnsNameOfInternedField) { | ||
InternedField foo = Manager().InternField("foo"); | ||
InternedField bar = Manager().InternField("bar"); | ||
EXPECT_EQ(Manager().GetFieldNameOrDie(foo), "foo"); | ||
EXPECT_EQ(Manager().GetFieldNameOrDie(bar), "bar"); | ||
} | ||
} // namespace | ||
} // namespace netkat |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.