From fab509a97a3249a84b7eac06f519ab9d3678f9e6 Mon Sep 17 00:00:00 2001 From: Anthony Roy Date: Fri, 18 Oct 2024 19:32:49 +0000 Subject: [PATCH] Add Github actions and some initial build files. PiperOrigin-RevId: 687389500 --- .bazelrc | 3 ++ .github/workflows/ci.yml | 48 ++++++++++++++++++++++ BUILD => BUILD.bazel | 7 +++- METADATA | 67 ------------------------------ MODULE.bazel | 28 +++++++++++++ README.md | 66 +++++++++++++++--------------- docs/CONTRIBUTING.md | 4 +- netkat/BUILD.bazel | 26 ++++++++++++ netkat/netkat.proto | 88 ++++++++++++++++++++++++++++++++++++++++ netkat/netkat_test.cc | 62 ++++++++++++++++++++++++++++ 10 files changed, 295 insertions(+), 104 deletions(-) create mode 100644 .bazelrc create mode 100644 .github/workflows/ci.yml rename BUILD => BUILD.bazel (66%) delete mode 100644 METADATA create mode 100644 MODULE.bazel create mode 100644 netkat/BUILD.bazel create mode 100644 netkat/netkat.proto create mode 100644 netkat/netkat_test.cc diff --git a/.bazelrc b/.bazelrc new file mode 100644 index 0000000..65541b1 --- /dev/null +++ b/.bazelrc @@ -0,0 +1,3 @@ +# Use C++ 20. +build --cxxopt=-std=c++20 +build --host_cxxopt=-std=c++20 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..f3fad80 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,48 @@ +name: build + +# Controls when the workflow will run +on: + # Triggers the workflow on push or pull request events but only for the "main" branch + push: + branches: [ "main" ] + pull_request: + branches: [ "main" ] + schedule: + # Run daily at midnight to ensure we catch regressions. + - cron: "0 0 * * *" + # Manual + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + + - name: Mount bazel cache + uses: actions/cache/restore@v4 + with: + path: "~/.cache/bazel" + key: bazel-${{ hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}-${{ github.ref_name }} + restore-keys: | + bazel-${{hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}-${{ github.ref_name }} + bazel-${{hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }} + bazel- + + + - name: Build + run: ./bazel build --test_output=errors //... + - name: Test + run: ./bazel test --test_output=errors //... + + - name: Compress cache + run: rm -rf $(./bazel info repository_cache) + + - name: Save bazel cache + uses: actions/cache/save@v4 + # Only create a new cache entry if we're on the main branch or the build takes >5mins. + if: github.ref_name == "main" || env.duration > 300 + with: + path: "~/.cache/bazel" + key: bazel-${{ hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}-${{ github.ref_name }}-${{ github.run_id }} diff --git a/BUILD b/BUILD.bazel similarity index 66% rename from BUILD rename to BUILD.bazel index 344b1be..0f8186f 100644 --- a/BUILD +++ b/BUILD.bazel @@ -1,8 +1,11 @@ # NetKAT, a framework for describing and reasoning about packet-switched networks. -load("//tools/build_defs/license:license.bzl", "license") +load("@rules_license//rules:license.bzl", "license") -package(default_applicable_licenses = [":license"]) +package( + default_applicable_licenses = [":license"], + default_visibility = [":__subpackages__"], +) # Define the license for this package, which is used as the default license # for all targets in this package based on default_applicable_licenses above. diff --git a/METADATA b/METADATA deleted file mode 100644 index 1fd70cb..0000000 --- a/METADATA +++ /dev/null @@ -1,67 +0,0 @@ -# go/google3metadata -# proto-file: devtools/metadata/metadata.proto -# proto-message: MetaData - -name: "NetKAT" -description: "Framework for describing and reasoning about packet-switched networks" - -third_party { - identifier { - type: "Piper" - value: "http://google3/third_party/netkat" - primary_source: true - } -} - -# Block submissions on SpongeMonitor findings. -presubmit: { - include_presubmit: "//depot/google3/testing/tools/sponge_monitor/blocking_presubmit.METADATA" - check_tests: { - project: "netkat" - } -} - -# Block submissions on Linter findings. -presubmit: { - check_lint { - base { - disable_tags: "ROLLBACK_OF" - disable_tags: "CLEANUP" - } - failure_status: ERROR - } -} - -presubmit: { - check_tricorder: { - action: SUBMIT - categories: "ClangTidy" - categories: "ErrorProne" - categories: "UnusedDeps" - categories: "TODONT" # go/todont - categories: "CppDefensiveCoding" # go/cpp-defensive-coding - } -} - -tricorder { - enable: TODONT # go/todont - enable: CppDefensiveCoding # go/cpp-defensive-coding - enable: TargetSizeLimits # go/targetsizelimits-presubmit - options { - cpp_defensive_coding: { - # Most critical CDC checks: - applicable_rules: POINTER_CHECKS - applicable_rules: MAYBE_NULL_CHECKS - - # Next most critical: - applicable_rules: OPTIONAL_CHECKS - applicable_rules: STATUS_OR_CHECKS - - # These checks have been shown to prevent crashes, but can be quite noisy - # on certain codebases. We recommend codebases enable them to gauge their - # effectiveness, and then disable them if they find them to be too noisy. - applicable_rules: VECTOR_CHECKS - applicable_rules: PROTO_CHECKS - } - } -} diff --git a/MODULE.bazel b/MODULE.bazel new file mode 100644 index 0000000..edb576a --- /dev/null +++ b/MODULE.bazel @@ -0,0 +1,28 @@ +# 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. + +# https://bazel.build/external/overview#bzlmod + +module( + name = "google-netkat", + version = "0.0.1", + bazel_compatibility = [">=7.3.2"], + compatibility_level = 1, +) + +bazel_dep(name = "rules_cc", version = "0.0.13") +bazel_dep(name = "rules_license", version = "1.0.0") +bazel_dep(name = "protobuf", version = "28.2", repo_name = "com_google_protobuf") +bazel_dep(name = "abseil-cpp", version = "20240116.2", repo_name = "com_google_absl") +bazel_dep(name = "googletest", version = "1.15.2", repo_name = "com_google_googletest") diff --git a/README.md b/README.md index 6cf5e5b..eba2b99 100644 --- a/README.md +++ b/README.md @@ -5,37 +5,37 @@ This is a C++ implementation of NetKAT. NetKAT is a domain specific language (DSL) and system for specifying, programming, and reasoning about packet-switched networks. Key features include: -* Automated reasoning and verification. -* Modular composition, supporting clean isolation and abstraction. -* Simple, yet very powerful syntax & semantics. -* Strong mathematical foundation. +* Automated reasoning and verification. +* Modular composition, supporting clean isolation and abstraction. +* Simple, yet very powerful syntax & semantics. +* Strong mathematical foundation. If you want to learn more, you may check out the list of -[publications on NetKAT](#academic-publications-on-netkat) below. In the future, +[pulbications on NetKAT](#academic-publications-on-netkat) below. In the future, we also hope to provide a gentler introduction to NetKAT in the form of a tutorial. -Note: We expect that this NetKAT implementation may diverge from NeKAT as -described [in the literature](#academic-publications-on-netkat) over time, -as we take liberty to optimize and adjust the language for industrial use. +Note: We expect that this NetKAT implementation may diverge from NetKAT as +described [in the literature](#academic-publications-on-netkat) over time, as we +take liberty to optimize and adjust the language for industrial use. ## Disclaimer -This is not an officially supported Google product. This project is not -eligible for the [Google Open Source Software Vulnerability Rewards -Program](https://bughunters.google.com/open-source-security). +This is not an officially supported Google product. This project is not eligible +for the +[Google Open Source Software Vulnerability Rewards Program](https://bughunters.google.com/open-source-security). ## Academic Publications on NetKAT -NetKAT was first conceived and studied in academia. -Here, we list a small selection of key publications related to NetKAT. +NetKAT was first conceived and studied in academia. Here, we list a small +selection of key publications related to NetKAT. -* **NetKAT: Semantic Foundations for Networks.** POPL 2014. - [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/frenetic-netkat.pdf) -* **A Fast Compiler for NetKAT.** ICFP 2015. - [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/netkat-compiler.pdf) -* **KATch: A Fast Symbolic Verifier for NetKAT.** PLDI 2024. - [[PDF]](https://research.google/pubs/katch-a-fast-symbolic-verifier-for-netkat/) +* **NetKAT: Semantic Foundations for Networks.** POPL 2014. + [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/frenetic-netkat.pdf) +* **A Fast Compiler for NetKAT.** ICFP 2015. + [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/netkat-compiler.pdf) +* **KATch: A Fast Symbolic Verifier for NetKAT.** PLDI 2024. + [[PDF]](https://research.google/pubs/katch-a-fast-symbolic-verifier-for-netkat/) ## Contributing @@ -49,22 +49,22 @@ information. Apache header: - Copyright 2024 Google LLC +``` +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 +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 + 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. +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 can be done automatically using -[addlicense](https://github.com/google/addlicense) as follows: -```sh -addlicense -c "The NetKAT Authors" -l apache ./netkat -``` +[addlicense](https://github.com/google/addlicense) as follows: `sh addlicense -c +"The NetKAT authors" -l apache .` diff --git a/docs/CONTRIBUTING.md b/docs/CONTRIBUTING.md index 8956a61..8b5b5a8 100644 --- a/docs/CONTRIBUTING.md +++ b/docs/CONTRIBUTING.md @@ -20,8 +20,8 @@ sign a new one. ### Review our Community Guidelines -This project follows [Google's Open Source Community -Guidelines](https://opensource.google/conduct/). +This project follows +[Google's Open Source Community Guidelines](https://opensource.google/conduct/). ## Contribution process diff --git a/netkat/BUILD.bazel b/netkat/BUILD.bazel new file mode 100644 index 0000000..5fe03cc --- /dev/null +++ b/netkat/BUILD.bazel @@ -0,0 +1,26 @@ + + +package( + default_applicable_licenses = ["//:license"], + default_visibility = [":__subpackages__"], +) + +proto_library( + name = "netkat_proto", + srcs = ["netkat.proto"], +) + +cc_proto_library( + name = "netkat_cc_proto", + deps = [":netkat_proto"], +) + +cc_test( + name = "netkat_test", + srcs = ["netkat_test.cc"], + deps = [ + ":netkat_cc_proto", + "@com_google_absl//absl/log", + "@com_google_googletest//:gtest_main", + ], +) diff --git a/netkat/netkat.proto b/netkat/netkat.proto new file mode 100644 index 0000000..3ebb737 --- /dev/null +++ b/netkat/netkat.proto @@ -0,0 +1,88 @@ +// 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. +// ----------------------------------------------------------------------------- + +// Proto representation of NetKAT programs (predicates and policies). +// +// This representation is NOT intended as a user-facing API. Instead, it serves +// as an intermdiate representation (IR) that is produced by user-facing +// NetKAT APIs (NetKAT frontend(s)) and consumed by NetKAT backends. +// +// This reprensentation is expected to lack the convenience and type safety of +// the user-facing API. +// +// Why have an IR? +// * Designing an ergonomic user-facing API is hard, and requires resolving many +// design questions without an obvious "best" answer. +// * By having an IR, we can immediately work on the backend without waiting for +// the user-facing API to be finalized. More generally, it decouples the +// frontend design from the backend design. +// * Given that there is likely not a single best user-facing API, we may want +// to explore multiple ones (but share the IR and backend). +// * It may make sense to have a specialized frontend API tailroed to Google's +// internal needs, but it will likely not be open-sourceable. +// +// Why use protobufs for the IR? +// * It provides many useful features out of the box: +// serialization/deserialization, pretty-printing, a text format, fuzzing +// (e.g. using https://github.com/google/fuzztest), diffing. +// * It makes it easy to implement frontends and backends in different +// programming languages. +// * It makes it easy to run backends as (gRPC) services. + +syntax = "proto3"; + +package netkat; + +// A NetKAT predicate (internal intermdiate representation). +message PredicateProto { + oneof predicate { + Bool bool_constant = 1; + Match match = 3; + And and_operation = 4; + Or or_operation = 5; + Not not_operation = 6; + } + + // A boolean constant (true or false). + message Bool { + bool value = 1; + } + + // Checks if a field has a specific value. + // + // NOTE: This message is expected to change in the future! E.g., the type of + // `value` will change to support things like 128-bit IPv6 addresses. + message Match { + string field = 1; + int32 value = 2; + } + + // Boolean conjunction (&&) of two predicates. + message And { + PredicateProto left = 1; + PredicateProto right = 2; + } + + // Boolean disjunction (||) of two predicates. + message Or { + PredicateProto left = 1; + PredicateProto right = 2; + } + + // Boolean negation (!) of a predicate. + message Not { + PredicateProto negand = 1; + } +} diff --git a/netkat/netkat_test.cc b/netkat/netkat_test.cc new file mode 100644 index 0000000..23f3860 --- /dev/null +++ b/netkat/netkat_test.cc @@ -0,0 +1,62 @@ +// 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 "absl/log/log.h" +#include "gtest/gtest.h" +#include "netkat/netkat.pb.h" + +namespace netkat { +namespace { + +// Ensures that the protobuf C++ compiler does not add underscores to the +// generated code for sub messages and oneof fields of `PredicateProto`. +// +// This test is needed because we uses key words such as "and", "or", "not", +// "bool", which are all reserved protobuf/C++ keywords. +TEST(NetkatProtoTest, PredicateOneOfFieldNamesDontRequireUnderscores) { + PredicateProto predicate; + switch (predicate.predicate_case()) { + case PredicateProto::kAndOperation: { + const PredicateProto::And& and_operation = predicate.and_operation(); + LOG(INFO) << "and_operation: " << and_operation; + break; + } + case PredicateProto::kOrOperation: { + const PredicateProto::Or& or_operation = predicate.or_operation(); + LOG(INFO) << "or_operation: " << or_operation; + break; + } + case PredicateProto::kNotOperation: { + const PredicateProto::Not& not_operation = predicate.not_operation(); + LOG(INFO) << "not_operation: " << not_operation; + break; + } + case PredicateProto::kMatch: { + const PredicateProto::Match& match = predicate.match(); + LOG(INFO) << "match: " << match; + break; + } + case PredicateProto::kBoolConstant: { + const PredicateProto::Bool& bool_constant = predicate.bool_constant(); + LOG(INFO) << "bool_constant: " << bool_constant; + break; + } + case PredicateProto::PREDICATE_NOT_SET: + break; + } +} + +} // namespace +} // namespace netkat