[NetKAT] Add property checking functions to AnalysisEngine.

netkat/BUILD.bazel

@@ -335,10 +335,13 @@ cc_library(
     deps = [
         ":counter_example",
         ":frontend",
+        ":packet",
         ":packet_set",
         ":packet_transformer",
         "@com_google_absl//absl/log:check",
+        "@com_google_absl//absl/status",
         "@com_google_absl//absl/status:statusor",
+        "@com_google_gutil//gutil:status",
     ],
 )
 
@@ -350,6 +353,7 @@ cc_test(
         ":analysis_engine",
         ":frontend",
         ":gtest_utils",
+        "@com_google_absl//absl/status:status_matchers",
         "@com_google_fuzztest//fuzztest",
         "@com_google_googletest//:gtest_main",
         "@com_google_gutil//gutil:status_matchers",

netkat/analysis_engine.cc

@@ -14,14 +14,43 @@
 
 #include "netkat/analysis_engine.h"
 
+#include <vector>
+
 #include "absl/log/check.h"
+#include "absl/status/status.h"
 #include "absl/status/statusor.h"
+#include "gutil/status.h"
 #include "netkat/counter_example.h"
 #include "netkat/frontend.h"
+#include "netkat/packet.h"
 #include "netkat/packet_set.h"
 #include "netkat/packet_transformer.h"
 
 namespace netkat {
+namespace {
+absl::Status SatisfyProperty(PacketSetManager& set_manager,
+                             PacketSetHandle packets,
+                             PacketSetHandle property) {
+  PacketSetHandle violating_set =
+      set_manager.And(packets, set_manager.Not(property));
+
+  if (set_manager.IsEmptySet(violating_set)) {
+    return absl::OkStatus();
+  }
+
+  std::vector<Packet> concrete_packets =
+      set_manager.GetConcretePackets(violating_set);
+  if (concrete_packets.empty()) {
+    return absl::InternalError(
+        "Property violated, but could not get any concrete packet from the "
+        "violating set.");
+  }
+  return gutil::InvalidArgumentErrorBuilder()
+         << "Property violated by example packet:\n "
+         << PacketToString(concrete_packets[0]);
+}
+
+}  // namespace
 
 bool AnalysisEngine::CheckEquivalent(const Predicate& left,
                                      const Predicate& right) {
@@ -49,6 +78,30 @@ SuccessOrCounterExample AnalysisEngine::CheckEquivalent(const Policy& left,
   return SuccessOrCounterExample(*counter_example);
 }
 
+absl::Status AnalysisEngine::CheckPacketsSatisfyProperty(
+    const Predicate& packets, const Predicate& property) {
+  PacketSetManager& set_manager =
+      packet_transformer_manager_.GetPacketSetManager();
+  PacketSetHandle compiled_packets = set_manager.Compile(packets.ToProto());
+  PacketSetHandle compiled_property = set_manager.Compile(property.ToProto());
+  return SatisfyProperty(set_manager, compiled_packets, compiled_property);
+}
+
+absl::Status AnalysisEngine::CheckOutputSatisfiesProperty(
+    const Predicate& input_packets, const Policy& program,
+    const Predicate& property) {
+  PacketSetManager& set_manager =
+      packet_transformer_manager_.GetPacketSetManager();
+  PacketSetHandle compiled_input = set_manager.Compile(input_packets.ToProto());
+  PacketSetHandle compiled_property = set_manager.Compile(property.ToProto());
+
+  PacketTransformerHandle program_handle =
+      packet_transformer_manager_.Compile(program.ToProto());
+  PacketSetHandle program_output =
+      packet_transformer_manager_.Push(compiled_input, program_handle);
+  return SatisfyProperty(set_manager, program_output, compiled_property);
+}
+
 bool AnalysisEngine::ProgramForwardsAnyPacket(const Policy& program,
                                               const Predicate& packets) {
   PacketTransformerHandle user_packet_handle =
@@ -112,8 +165,7 @@ bool AnalysisEngine::CheckInputProducesAtMostGivenOutput(
   if (program_output == compiled_output) return true;
   if (program_output == set_manager.EmptySet()) return false;
 
-  // We can define less than or equal to as follows: a <= b === a + b == b
-  return set_manager.Or(program_output, compiled_output) == compiled_output;
+  return SatisfyProperty(set_manager, program_output, compiled_output).ok();
 }
 
 }  // namespace netkat

netkat/analysis_engine.h

@@ -21,8 +21,12 @@
 #ifndef GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_
 #define GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_
 
+#include <optional>
+
+#include "absl/status/status.h"
 #include "netkat/counter_example.h"
 #include "netkat/frontend.h"
+#include "netkat/packet.h"
 #include "netkat/packet_transformer.h"
 
 namespace netkat {
@@ -67,6 +71,27 @@ class AnalysisEngine {
   SuccessOrCounterExample CheckEquivalent(const Policy& left,
                                           const Policy& right);
 
+  // Returns whether the given `packets` satisfy the given `property`.
+  // This is true if all packets in `packets` are also in `property`.
+  // Equivalent to: packets <= property.
+  // WARNING: The empty set of packets vacuously satisfies all properties.
+  // If not satisfied, returns an InvalidArgument error with an example packet
+  // that violates the property.
+  absl::Status CheckPacketsSatisfyProperty(const Predicate& packets,
+                                           const Predicate& property);
+
+  // Returns whether the output of `program` for the given `input_packets`
+  // satisfies the given `property`.
+  // This is true if all packets produced by `program` from `input_packets`
+  // are in `property`.
+  // Equivalent to: push(input_packets, program) <= property.
+  // WARNING: The empty set of packets vacuously satisfies all properties.
+  // If not satisfied, returns an InvalidArgument error with an example packet
+  // that violates the property.
+  absl::Status CheckOutputSatisfiesProperty(const Predicate& input_packets,
+                                            const Policy& program,
+                                            const Predicate& property);
+
   // Returns whether any given packet, represented by the set of packets in
   // `packets`, is forwarded by `program`. A packet is considered "forwaded" if
   // it produces some non-zero output packet when the `program` is run on it.

netkat/analysis_engine_test.cc

@@ -16,6 +16,7 @@
 
 #include <utility>
 
+#include "absl/status/status_matchers.h"
 #include "fuzztest/fuzztest.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
@@ -26,6 +27,9 @@
 namespace netkat {
 namespace {
 
+using ::gutil::IsOk;
+using ::testing::Not;
+
 // We include only a single `CheckEquivalent` test as a smoke test since the
 // function is implemented in terms of `PacketSetManager`, which is tested
 // thoroughly in its own unit tests.
@@ -294,5 +298,59 @@ TEST(CheckInputProducesAtMostGivenOutputTest,
       Match("foo", 1) && Match("tag", 1)));
 }
 
+TEST(CheckPacketsSatisfyPropertyTest, EmptySetSatisfiesAllProperties) {
+  AnalysisEngine analyzer;
+  EXPECT_OK(analyzer.CheckPacketsSatisfyProperty(Predicate::False(),
+                                                 Predicate::True()));
+  EXPECT_OK(analyzer.CheckPacketsSatisfyProperty(Predicate::False(),
+                                                 Predicate::False()));
+  EXPECT_OK(analyzer.CheckPacketsSatisfyProperty(Predicate::False(),
+                                                 Match("foo", 1)));
+}
+
+TEST(CheckPacketsSatisfyPropertyTest, PacketsSatisfyPropertyReturnsOk) {
+  AnalysisEngine analyzer;
+  Predicate packets = Match("foo", 1);
+  Predicate property = Match("foo", 1) || Match("bar", 1);
+  EXPECT_OK(analyzer.CheckPacketsSatisfyProperty(packets, property));
+}
+
+TEST(CheckPacketsSatisfyPropertyTest,
+     PacketsDoNotSatisfyPropertyReturnsInvalidArgument) {
+  AnalysisEngine analyzer;
+  Predicate packets = Match("foo", 1) || Match("bar", 1);
+  Predicate property = Match("foo", 1);
+  EXPECT_THAT(analyzer.CheckPacketsSatisfyProperty(packets, property),
+              Not(IsOk()));
+}
+
+TEST(CheckOutputSatisfiesPropertyTest, EmptyOutputSatisfiesAllProperties) {
+  AnalysisEngine analyzer;
+  // Program that drops everything
+  Policy program = Filter(Predicate::False());
+  EXPECT_OK(analyzer.CheckOutputSatisfiesProperty(Predicate::True(), program,
+                                                  Predicate::True()));
+  EXPECT_OK(analyzer.CheckOutputSatisfiesProperty(Predicate::True(), program,
+                                                  Predicate::False()));
+}
+
+TEST(CheckOutputSatisfiesPropertyTest, OutputSatisfiesPropertyReturnsOk) {
+  AnalysisEngine analyzer;
+  Policy program = Modify("foo", 1);
+  Predicate property = Match("foo", 1);
+  EXPECT_OK(analyzer.CheckOutputSatisfiesProperty(Predicate::True(), program,
+                                                  property));
+}
+
+TEST(CheckOutputSatisfiesPropertyTest,
+     OutputDoesNotSatisfyPropertyReturnsInvalidArgument) {
+  AnalysisEngine analyzer;
+  Policy program = Modify("foo", 2);
+  Predicate property = Match("foo", 1);
+  EXPECT_THAT(analyzer.CheckOutputSatisfiesProperty(Predicate::True(), program,
+                                                    property),
+              Not(IsOk()));
+}
+
 }  // namespace
 }  // namespace netkat