Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
…into symbolic_import_branch_101
  • Loading branch information
VSuryaprasad-HCL committed Nov 20, 2024
2 parents 3e0513f + a58579a commit d962523
Show file tree
Hide file tree
Showing 16 changed files with 380 additions and 12 deletions.
2 changes: 2 additions & 0 deletions p4_symbolic/sai/deparser.cc
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,8 @@ absl::StatusOr<std::string> SaiDeparser(const SaiFields& packet,
RETURN_IF_ERROR(Deparse(packet.headers.erspan_ipv4, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.erspan_gre, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.ethernet, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.tunnel_encap_ipv6, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.tunnel_encap_gre, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.ipv4, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.ipv6, model, result));
RETURN_IF_ERROR(Deparse(packet.headers.udp, model, result));
Expand Down
2 changes: 1 addition & 1 deletion p4_symbolic/sai/deparser_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ TEST_P(SaiDeparserTest, IcmpPacketParserIntegrationTest) {
}

INSTANTIATE_TEST_SUITE_P(Instantiation, SaiDeparserTest,
testing::ValuesIn(sai::AllInstantiations()));
testing::ValuesIn(sai::AllSaiInstantiations()));

} // namespace
} // namespace p4_symbolic
29 changes: 29 additions & 0 deletions p4_symbolic/sai/fields.cc
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,32 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
.src_addr = get_field("ethernet.src_addr"),
.ether_type = get_field("ethernet.ether_type"),
};
auto tunnel_encap_ipv6 = SaiIpv6{
.valid = get_field("tunnel_encap_ipv6.$valid$"),
.version = get_field("tunnel_encap_ipv6.version"),
.dscp = get_field("tunnel_encap_ipv6.dscp"),
.ecn = get_field("tunnel_encap_ipv6.ecn"),
.flow_label = get_field("tunnel_encap_ipv6.flow_label"),
.payload_length = get_field("tunnel_encap_ipv6.payload_length"),
.next_header = get_field("tunnel_encap_ipv6.next_header"),
.hop_limit = get_field("tunnel_encap_ipv6.hop_limit"),
.src_addr = get_field("tunnel_encap_ipv6.src_addr"),
.dst_addr = get_field("tunnel_encap_ipv6.dst_addr"),
};
auto tunnel_encap_gre = SaiGre{
.valid = get_field("tunnel_encap_gre.$valid$"),
.checksum_present = get_field("tunnel_encap_gre.checksum_present"),
.routing_present = get_field("tunnel_encap_gre.routing_present"),
.key_present = get_field("tunnel_encap_gre.key_present"),
.sequence_present = get_field("tunnel_encap_gre.sequence_present"),
.strict_source_route = get_field("tunnel_encap_gre.strict_source_route"),
.recursion_control = get_field("tunnel_encap_gre.recursion_control"),
.acknowledgement_present =
get_field("tunnel_encap_gre.acknowledgement_present"),
.flags = get_field("tunnel_encap_gre.flags"),
.version = get_field("tunnel_encap_gre.version"),
.protocol = get_field("tunnel_encap_gre.protocol"),
};
auto ipv4 = SaiIpv4{
.valid = get_field("ipv4.$valid$"),
.version = get_field("ipv4.version"),
Expand Down Expand Up @@ -229,6 +255,7 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
.l4_dst_port = get_metadata_field("l4_dst_port"),
.mirror_session_id_valid = get_metadata_field("mirror_session_id_valid"),
.ingress_port = get_metadata_field("ingress_port"),
.route_metadata = get_metadata_field("route_metadata"),
};
auto standard_metadata = V1ModelStandardMetadata{
.ingress_port = get_field("standard_metadata.ingress_port"),
Expand All @@ -249,6 +276,8 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
.erspan_ipv4 = erspan_ipv4,
.erspan_gre = erspan_gre,
.ethernet = ethernet,
.tunnel_encap_ipv6 = tunnel_encap_ipv6,
.tunnel_encap_gre = tunnel_encap_gre,
.ipv4 = ipv4,
.ipv6 = ipv6,
.udp = udp,
Expand Down
7 changes: 6 additions & 1 deletion p4_symbolic/sai/fields.h
Original file line number Diff line number Diff line change
Expand Up @@ -131,8 +131,12 @@ struct SaiHeaders {
SaiEthernet erspan_ethernet;
SaiIpv4 erspan_ipv4;
SaiGre erspan_gre;

SaiEthernet ethernet;

// Not extracted during parsing.
SaiIpv6 tunnel_encap_ipv6;
SaiGre tunnel_encap_gre;

SaiIpv4 ipv4;
SaiIpv6 ipv6;
SaiUdp udp;
Expand All @@ -150,6 +154,7 @@ struct SaiLocalMetadata {
z3::expr l4_dst_port;
z3::expr mirror_session_id_valid;
z3::expr ingress_port;
z3::expr route_metadata;
};

// Symbolic version of `struct standard_metadata_t` in v1model.p4
Expand Down
2 changes: 1 addition & 1 deletion p4_symbolic/sai/fields_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ namespace p4_symbolic {
namespace {

TEST(GetSaiFields, CanGetIngressAndEgressFieldsForAllInstantiations) {
for (auto instantiation : sai::AllInstantiations()) {
for (auto instantiation : sai::AllSaiInstantiations()) {
const auto config = sai::GetNonstandardForwardingPipelineConfig(
instantiation, sai::NonstandardPlatform::kP4Symbolic);
ASSERT_OK_AND_ASSIGN(
Expand Down
7 changes: 6 additions & 1 deletion p4_symbolic/sai/parser.cc
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,8 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
SaiIpv4& erspan_ipv4 = fields.headers.erspan_ipv4;
SaiGre& erspan_gre = fields.headers.erspan_gre;
SaiEthernet& ethernet = fields.headers.ethernet;
SaiIpv6& tunnel_encap_ipv6 = fields.headers.tunnel_encap_ipv6;
SaiGre& tunnel_encap_gre = fields.headers.tunnel_encap_gre;
SaiIpv4& ipv4 = fields.headers.ipv4;
SaiIpv6& ipv6 = fields.headers.ipv6;
SaiUdp& udp = fields.headers.udp;
Expand All @@ -49,11 +51,14 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
constraints.push_back(!erspan_ethernet.valid);
constraints.push_back(!erspan_ipv4.valid);
constraints.push_back(!erspan_gre.valid);
constraints.push_back(local_metadata.admit_to_l3 == bv_true);
constraints.push_back(!tunnel_encap_ipv6.valid);
constraints.push_back(!tunnel_encap_gre.valid);
constraints.push_back(local_metadata.admit_to_l3 == bv_false);
constraints.push_back(local_metadata.vrf_id == 0);
constraints.push_back(local_metadata.mirror_session_id_valid == bv_false);
constraints.push_back(local_metadata.ingress_port ==
standard_metadata.ingress_port);
constraints.push_back(local_metadata.route_metadata == 0);

// `parse_ethernet` state.
constraints.push_back(ethernet.valid == Z3Context().bool_val(true));
Expand Down
2 changes: 1 addition & 1 deletion p4_symbolic/sai/sai_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ namespace {

TEST(EvaluateSaiPipeline,
SatisfiableForAllInstantiationsWithEmptyEntriesAndPorts) {
for (auto instantiation : sai::AllInstantiations()) {
for (auto instantiation : sai::AllSaiInstantiations()) {
const auto config = sai::GetNonstandardForwardingPipelineConfig(
instantiation, sai::NonstandardPlatform::kP4Symbolic);
ASSERT_OK_AND_ASSIGN(
Expand Down
4 changes: 2 additions & 2 deletions p4_symbolic/symbolic/expected/table_hit_1.txt
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ Finding packet for table MyIngress.t_1 and row 0

Finding packet for table MyIngress.t_2 and row -1
Dropped = 0
standard_metadata.ingress_port = #b000000000
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000010

Finding packet for table MyIngress.t_2 and row 0
Dropped = 0
standard_metadata.ingress_port = #b000000000
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000011

6 changes: 5 additions & 1 deletion p4_symbolic/symbolic/test.bzl
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,11 @@ def end_to_end_test(
("--entries=$(location %s)" % table_entries if table_entries else ""),
("--debug=$(location %s)" % smt_output_file),
("--port_count=%d" % port_count),
("&> $(location %s)" % test_output_file),
# Redirect stderr to stdout, so we can capture both.
"2>&1",
# Use `tee` to simultaneously capture output in file yet still print it to stdout, to
# ease debugging.
("| tee $(location %s)" % test_output_file),
]),
)

Expand Down
1 change: 1 addition & 0 deletions p4_symbolic/tests/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ package(

cc_test(
name = "sai_p4_component_test",
timeout = "long",
srcs = ["sai_p4_component_test.cc"],
deps = [
"//gutil:status_matchers",
Expand Down
10 changes: 10 additions & 0 deletions p4_symbolic/tests/sai_p4_component_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,16 @@ constexpr absl::string_view kTableEntries = R"pb(
action { set_nexthop_id { nexthop_id: "nexthop-1" } }
}
}
entries {
l3_admit_table_entry {
match {
dst_mac { value: "66:55:44:33:22:10" mask: "ff:ff:ff:ff:ff:ff" }
in_port { value: "0x005" }
}
action { admit_to_l3 {} }
priority: 1
}
}
entries {
nexthop_table_entry {
match { nexthop_id: "nexthop-1" }
Expand Down
2 changes: 1 addition & 1 deletion p4rt_app/p4runtime/p4info_verification_schema_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -895,7 +895,7 @@ TEST_P(GoogleInstantiationTest, SchemaSupportsInstantiation) {

INSTANTIATE_TEST_SUITE_P(
IsSupportedBySchemaTest, GoogleInstantiationTest,
ValuesIn(sai::AllInstantiations()),
ValuesIn(sai::AllSaiInstantiations()),
[](const testing::TestParamInfo<sai::Instantiation>& info) {
return sai::InstantiationToString(info.param);
});
Expand Down
2 changes: 1 addition & 1 deletion p4rt_app/p4runtime/p4info_verification_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ TEST_P(InstantiationTest, SaiP4InfoIsOk) {
}

INSTANTIATE_TEST_SUITE_P(P4InfoVerificationTest, InstantiationTest,
testing::ValuesIn(sai::AllInstantiations()),
testing::ValuesIn(sai::AllSaiInstantiations()),
[](testing::TestParamInfo<sai::Instantiation> info) {
return sai::InstantiationToString(info.param);
});
Expand Down
2 changes: 1 addition & 1 deletion p4rt_app/tests/forwarding_pipeline_config_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -766,7 +766,7 @@ std::string PerConfigTestCaseName(

INSTANTIATE_TEST_SUITE_P(
ForwardingPipelineConfig, PerConfigTest,
testing::Combine(testing::ValuesIn(sai::AllInstantiations()),
testing::Combine(testing::ValuesIn(sai::AllSaiInstantiations()),
testing::ValuesIn(sai::AllStages())),
PerConfigTestCaseName);

Expand Down
2 changes: 1 addition & 1 deletion p4rt_app/tests/p4_programs_test.cc
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ TEST_P(P4ProgramsTest, CompositeUdfFieldsShouldAlwaysUseHexStrings) {

INSTANTIATE_TEST_SUITE_P(
P4ProgramsTestInstance, P4ProgramsTest,
testing::ValuesIn(sai::AllInstantiations()),
testing::ValuesIn(sai::AllSaiInstantiations()),
[](const testing::TestParamInfo<P4ProgramsTest::ParamType>& param) {
return sai::InstantiationToString(param.param);
});
Expand Down
Loading

0 comments on commit d962523

Please sign in to comment.