[P4_Symbolic] Implement support for synthesis criteria on ingress por…

…t.Fix comment for OutputCriteria.drop_expected

p4_symbolic/packet_synthesizer/packet_synthesis_criteria.cc

@@ -58,6 +58,12 @@ absl::StatusOr<CriteriaVariant> GetCriteriaVariant(
             criteria.payload_criteria();
       }
       break;
+    case CriteriaVariant::kIngressPortCriteria:
+      if (criteria.has_ingress_port_criteria()) {
+        *criteria_variant.mutable_ingress_port_criteria() =
+            criteria.ingress_port_criteria();
+      }
+      break;
     default:
       return gutil::InvalidArgumentErrorBuilder()
              << "Unexpected criteria case " << criteria_case;

p4_symbolic/packet_synthesizer/packet_synthesis_criteria.proto

@@ -36,7 +36,8 @@ message TableReachabilityCriteria {
 
 // Criteria for the output behavior for the synthesized packet.
 message OutputCriteria {
-  // Whether the packet must get dropped.
+  // If true, the packet must get dropped. If false, the packet must get
+  // forwarded.
   bool drop_expected = 1;
 }
 
@@ -61,6 +62,13 @@ message PayloadCriteria {
   string payload = 1;
 }
 
+// Criteria on the port on which a packet should appear.
+message PortCriteria {
+  // In P4-Symbolic, this is also referred to as "physical port".
+  int32 v1model_port = 1;
+  // TODO: Support P4RT port names.
+}
+
 // The coverage criteria for (single) packet synthesis. All fields are optional.
 // If a criterion is not provided, no constraints for that criterion will be
 // added.
@@ -70,15 +78,22 @@ message PacketSynthesisCriteria {
   TableReachabilityCriteria table_reachability_criteria = 3;
   TableEntryReachabilityCriteria table_entry_reachability_criteria = 4;
   PayloadCriteria payload_criteria = 5;
+  PortCriteria ingress_port_criteria = 6;
 }
 
 // Contains a single (type of) criteria.
+// This is mostly an implementation detail (not visible to the clients): a
+// handy struct enabling us to programmatically specify the order of
+// fields in PacketSynthesisCriteria (to define the order of their respective Z3
+// frames) and to project PacketSynthesisCriteria messages to each individual
+// variant. See PacketSynthesizer::PrepareZ3SolverStack for more details.
 message CriteriaVariant {
   oneof criteria {
     OutputCriteria output_criteria = 1;
     HeaderCriteria input_packet_header_criteria = 2;
     TableReachabilityCriteria table_reachability_criteria = 3;
     TableEntryReachabilityCriteria table_entry_reachability_criteria = 4;
     PayloadCriteria payload_criteria = 5;
+    PortCriteria ingress_port_criteria = 6;
   }
 }

p4_symbolic/packet_synthesizer/packet_synthesis_criteria_test.cc

@@ -113,5 +113,20 @@ TEST(GetCriteriaVariantTest, YieldsCorrectVariantForPayloadCriteria) {
               IsOkAndHolds(EqualsProto(expected_variant)));
 }
 
+TEST(GetCriteriaVariantTest, YieldsCorrectVariantForIngressPortCriteria) {
+  auto ingress_port_criteria =
+      gutil::ParseProtoOrDie<PortCriteria>(R"pb(v1model_port: 5)pb");
+
+  PacketSynthesisCriteria criteria;
+  *criteria.mutable_ingress_port_criteria() = ingress_port_criteria;
+
+  CriteriaVariant expected_variant;
+  *expected_variant.mutable_ingress_port_criteria() = ingress_port_criteria;
+
+  ASSERT_THAT(
+      GetCriteriaVariant(criteria, CriteriaVariant::kIngressPortCriteria),
+      IsOkAndHolds(EqualsProto(expected_variant)));
+}
+
 }  // namespace
 }  // namespace p4_symbolic::packet_synthesizer

p4_symbolic/packet_synthesizer/packet_synthesizer.cc

@@ -36,6 +36,7 @@
 #include "p4_symbolic/deparser.h"
 #include "p4_symbolic/ir/ir.pb.h"
 #include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h"
+#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.pb.h"
 #include "p4_symbolic/packet_synthesizer/util.h"
 #include "p4_symbolic/sai/sai.h"
 #include "p4_symbolic/symbolic/symbolic.h"
@@ -184,6 +185,15 @@ absl::Status AddConstraintsForInputPacketHeader(const HeaderCriteria& criteria,
   return absl::OkStatus();
 }
 
+// Adds logical assertions corresponding to the given `criteria` (for packet
+// ingress port) to `solver_state`.
+absl::Status AddConstraintsForIngressPort(const PortCriteria& criteria,
+                                          SolverState& solver_state) {
+  solver_state.solver->add(solver_state.context.ingress_port ==
+                           criteria.v1model_port());
+  return absl::OkStatus();
+}
+
 // The following functions add logical assertions to the current solver state
 // corresponding to the given `criteria`.
 absl::Status AddConstraints(const OutputCriteria& criteria,
@@ -332,9 +342,15 @@ absl::Status PacketSynthesizer::AddFrameForCriteria(
         return AddConstraints(criteria.table_entry_reachability_criteria(),
                               solver_state_);
       break;
+    case CriteriaVariant::kIngressPortCriteria:
+      if (criteria.has_ingress_port_criteria())
+        return AddConstraintsForIngressPort(criteria.ingress_port_criteria(),
+                                            solver_state_);
+      break;
     default:
       return gutil::InvalidArgumentErrorBuilder()
-             << "Unsupported criteria case " << criteria.ShortDebugString();
+              << "Unsupported criteria case " << criteria_case << " for "
+             << criteria.ShortDebugString();
   }
 
   return absl::OkStatus();

p4_symbolic/packet_synthesizer/packet_synthesizer.h

@@ -85,6 +85,7 @@ class PacketSynthesizer {
       CriteriaVariant::kInputPacketHeaderCriteria,
       CriteriaVariant::kTableReachabilityCriteria,
       CriteriaVariant::kTableEntryReachabilityCriteria,
+      CriteriaVariant::kIngressPortCriteria,
   };
 
 private: