Skip to content

Commit

Permalink
[P4_Symbolic] Eliminate the use of a global Z3 context. (#928)
Browse files Browse the repository at this point in the history 
* [P4-Symbolic] Use generic deparser to extract input/output packets

* [P4-Symbolic] Use p4-symbolic's test data instead of SAI P4 for deparser tests.

* [P4-Symbolic] Move IR parser to `ir/`. Simplify IR parser API. Remove unused IR pdpi_driver. Remove hard-coded SAI parser. Remove EvaluateSaiPipeline. Refactor SAI-specific code.

* [P4-Symbolic] Remove dependencies on SAI fields.

* [P4-Symbolic] Add non-SAI tests for the generic deparser. Output concrete solutions to a file instead of standard output.

* [Comb] Rename PD->IR/PI to set up for deprecation.

* [P4-Symbolic] Move symbolic/concrete context to context.{cc,h} separated from symbolic.{cc,h}, and make the context-related objects constructed along with the solver state and then passed along the symbolic evaluation.

* [P4-Symbolic] Eliminate the use of a global Z3 context.

---------

Co-authored-by: kishanps <kishanps@google.com>
  • Loading branch information
@VSuryaprasad-HCL @kishanps
VSuryaprasad-HCL and kishanps authored Jan 7, 2025
1 parent 8615e2e commit 7cb0b4d
Show file tree
Hide file tree
Showing 30 changed files with 412 additions and 317 deletions.
1 change: 0 additions & 1 deletion p4_symbolic/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,6 @@ cc_test(
deps = [
":deparser",
":test_util",
":z3_util",
"//gutil:status_matchers",
"//p4_pdpi/packetlib",
"//p4_pdpi/packetlib:packetlib_cc_proto",
Expand Down
18 changes: 8 additions & 10 deletions p4_symbolic/deparser_test.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@
#include "p4_symbolic/symbolic/symbolic.h"
#include "p4_symbolic/symbolic/util.h"
#include "p4_symbolic/test_util.h"
#include "p4_symbolic/z3_util.h"
#include "z3++.h"

namespace p4_symbolic {
Expand All @@ -55,7 +54,6 @@ class IPv4RoutingBasicTest : public testing::Test {
ASSERT_OK_AND_ASSIGN(
std::vector<p4::v1::TableEntry> entries,
GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path));
Z3Context(/*renew=*/true);
ASSERT_OK_AND_ASSIGN(state_, symbolic::EvaluateP4Program(config, entries));
}

Expand All @@ -73,12 +71,12 @@ TEST_F(IPv4RoutingBasicTest, DeparseIngressAndEgressHeadersWithoutConstraints) {
TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders1) {
// Add constraints.
{
z3::context &z3_context = *state_->context.z3_context;
ASSERT_OK_AND_ASSIGN(
z3::expr eth_dst_addr,
state_->context.egress_headers.Get("ethernet.dstAddr"));
state_->solver->add(eth_dst_addr == Z3Context().bv_val(0, 48));
state_->solver->add(state_->context.egress_port ==
Z3Context().bv_val(1, 9));
state_->solver->add(eth_dst_addr == z3_context.bv_val(0, 48));
state_->solver->add(state_->context.egress_port == z3_context.bv_val(1, 9));

ASSERT_OK_AND_ASSIGN(
z3::expr ipv4_valid,
Expand All @@ -105,13 +103,13 @@ TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders1) {
TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders2) {
// Add constraints.
{
z3::context &z3_context = *state_->context.z3_context;
ASSERT_OK_AND_ASSIGN(
z3::expr eth_dst_addr,
state_->context.egress_headers.Get("ethernet.dstAddr"));
state_->solver->add(eth_dst_addr ==
Z3Context().bv_val((22UL << 40) + 22, 48));
state_->solver->add(state_->context.egress_port ==
Z3Context().bv_val(1, 9));
z3_context.bv_val((22UL << 40) + 22, 48));
state_->solver->add(state_->context.egress_port == z3_context.bv_val(1, 9));

ASSERT_OK_AND_ASSIGN(
z3::expr ipv4_valid,
Expand Down Expand Up @@ -139,10 +137,11 @@ TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders2) {
TEST_F(IPv4RoutingBasicTest, DeparseEgressHeaders) {
// Add constraints.
{
z3::context &z3_context = *state_->context.z3_context;
ASSERT_OK_AND_ASSIGN(z3::expr ipv4_dst_addr,
state_->context.ingress_headers.Get("ipv4.dstAddr"));
state_->solver->add(ipv4_dst_addr ==
Z3Context().bv_val((10UL << 24) + 1, 32));
z3_context.bv_val((10UL << 24) + 1, 32));

ASSERT_OK_AND_ASSIGN(
z3::expr ipv4_valid,
Expand Down Expand Up @@ -180,7 +179,6 @@ class SaiDeparserTest : public testing::Test {
ASSERT_OK_AND_ASSIGN(
p4::v1::ForwardingPipelineConfig config,
ParseToForwardingPipelineConfig(bmv2_json_path, p4info_path));
Z3Context(/*renew=*/true);
ASSERT_OK_AND_ASSIGN(state_,
symbolic::EvaluateP4Program(config, /*entries=*/{}));
}
Expand Down
90 changes: 52 additions & 38 deletions p4_symbolic/packet_synthesizer/util.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ namespace {
// The use of a template here is a hack to improve readability.
// TODO: Move to p4-symbolic utility library.
template <size_t num_bits>
inline z3::expr Bitvector(uint64_t value) {
return p4_symbolic::Z3Context().bv_val(value, num_bits);
inline z3::expr Bitvector(uint64_t value, z3::context& z3_context) {
return z3_context.bv_val(value, num_bits);
}

// TODO: Move to netaddr.
Expand Down Expand Up @@ -76,41 +76,57 @@ absl::StatusOr<std::vector<Ipv6Range>> GetUnicastIpv6Ranges() {
}

// TODO: Move to p4-symbolic utility library and add unit tests.
absl::StatusOr<z3::expr> Ipv6PrefixLengthToZ3Mask(int prefix_length) {
absl::StatusOr<z3::expr> Ipv6PrefixLengthToZ3Mask(int prefix_length,
z3::context& z3_context) {
if (prefix_length < 0 || prefix_length > 128) {
return gutil::InvalidArgumentErrorBuilder()
<< "invalid IPv6 prefix length: " << prefix_length;
}
if (prefix_length > 64) {
return Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu).rotate_left(64) |
Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu << (128 - prefix_length));
return Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu, z3_context).rotate_left(64) |
Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu << (128 - prefix_length),
z3_context);
} else {
return Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu << (64 - prefix_length))
return Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu << (64 - prefix_length),
z3_context)
.rotate_left(64);
}
}

// TODO: Move to p4-symbolic utility library.
absl::StatusOr<z3::expr> Ipv6AddressToZ3Bitvector(
const netaddr::Ipv6Address& ipv6) {
const netaddr::Ipv6Address& ipv6, z3::context& z3_context) {
std::bitset<128> bits = ipv6.ToBitset();
uint64_t upper = (bits >> 64).to_ullong();
uint64_t lower =
(bits & std::bitset<128>(0xFFFF'FFFF'FFFF'FFFFu)).to_ullong();
return Bitvector<128>(upper).rotate_left(64) | Bitvector<128>(lower);
return Bitvector<128>(upper, z3_context).rotate_left(64) |
Bitvector<128>(lower, z3_context);
}

absl::StatusOr<z3::expr> IsIpv6UnicastAddress(z3::expr ipv6_address) {
z3::expr result = p4_symbolic::Z3Context().bool_val(false);
z3::context& z3_context = ipv6_address.ctx();
z3::expr result = z3_context.bool_val(false);
ASSIGN_OR_RETURN(std::vector<Ipv6Range> ranges, GetUnicastIpv6Ranges());
for (auto& range : ranges) {
ASSIGN_OR_RETURN(z3::expr value, Ipv6AddressToZ3Bitvector(range.value));
ASSIGN_OR_RETURN(z3::expr value,
Ipv6AddressToZ3Bitvector(range.value, z3_context));
ASSIGN_OR_RETURN(z3::expr mask,
Ipv6PrefixLengthToZ3Mask(range.prefix_length));
Ipv6PrefixLengthToZ3Mask(range.prefix_length, z3_context));
result = result || ((ipv6_address & mask) == value);
}
return result;
}

absl::StatusOr<z3::expr> IrValueToZ3Bitvector(const pdpi::IrValue& value,
int bitwidth,
z3::context& z3_context) {
ASSIGN_OR_RETURN(const std::string bytes,
pdpi::IrValueToNormalizedByteString(value, bitwidth));
const std::string hex_string = pdpi::ByteStringToHexString(bytes);
return HexStringToZ3Bitvector(z3_context, hex_string, bitwidth);
}

} // namespace

// TODO: We need extra constraints to avoid generating packets
Expand All @@ -119,6 +135,8 @@ absl::StatusOr<z3::expr> IsIpv6UnicastAddress(z3::expr ipv6_address) {
// function would disappear.
absl::Status AddSanePacketConstraints(
p4_symbolic::symbolic::SolverState& state) {
z3::context& z3_context = *state.context.z3_context;

// ======Ethernet constraints======
ASSIGN_OR_RETURN(z3::expr ethernet_src_addr,
state.context.ingress_headers.Get("ethernet.src_addr"));
Expand All @@ -134,13 +152,14 @@ absl::Status AddSanePacketConstraints(
// such packets still continue to hit the acl_ingress table and some of the
// entries cause such packets to get punted. So we should not disallow the
// generation of such packets.
state.solver->add((ethernet_src_addr & Bitvector<48>(0x03'00'00'00'00'00)) ==
Bitvector<48>(0x02'00'00'00'00'00));
state.solver->add(
(ethernet_src_addr & Bitvector<48>(0x03'00'00'00'00'00, z3_context)) ==
Bitvector<48>(0x02'00'00'00'00'00, z3_context));

for (auto& mac_address : {ethernet_src_addr, ethernet_dst_addr}) {
// Require key parts of the address to be nonzero to avoid corner cases.
auto nonzero_masks = std::vector({
Bitvector<48>(0x00'FF'FF'00'00'00), // OUI
Bitvector<48>(0x00'FF'FF'00'00'00, z3_context), // OUI
});
for (auto& nonzero_mask : nonzero_masks) {
state.solver->add((mac_address & nonzero_mask) != 0);
Expand All @@ -156,15 +175,16 @@ absl::Status AddSanePacketConstraints(
state.context.ingress_headers.Get("ipv4.dst_addr"));
// Avoid martian IP addresses.
// https://tools.ietf.org/html/rfc1122#section-3.2.1.3
state.solver->add((ipv4_src_addr & Bitvector<32>(0xFF'00'00'00)) != 0);
state.solver->add(
(ipv4_src_addr & Bitvector<32>(0xFF'00'00'00, z3_context)) != 0);
// Src IP address cannot be 255.255.255.255 (broadcast).
state.solver->add(ipv4_src_addr != Bitvector<32>(0xFF'FF'FF'FF));
state.solver->add(ipv4_src_addr != Bitvector<32>(0xFF'FF'FF'FF, z3_context));
// Neither src nor dst IPv4 addresses can be 0.
state.solver->add(ipv4_src_addr != Bitvector<32>(0));
state.solver->add(ipv4_dst_addr != Bitvector<32>(0));
state.solver->add(ipv4_src_addr != Bitvector<32>(0, z3_context));
state.solver->add(ipv4_dst_addr != Bitvector<32>(0, z3_context));
// Neither src nor dst IPv4 addresses can be 127.0.0.1 (loopback).
state.solver->add(ipv4_src_addr != Bitvector<32>(0x7F'00'00'01));
state.solver->add(ipv4_dst_addr != Bitvector<32>(0x7F'00'00'01));
state.solver->add(ipv4_src_addr != Bitvector<32>(0x7F'00'00'01, z3_context));
state.solver->add(ipv4_dst_addr != Bitvector<32>(0x7F'00'00'01, z3_context));

// ======Ipv6 constraints======
ASSIGN_OR_RETURN(z3::expr ipv6_src_addr,
Expand All @@ -177,11 +197,11 @@ absl::Status AddSanePacketConstraints(
state.solver->add(constraint);
}
// Neither src nor dst IPv6 addresses can be 0.
state.solver->add(ipv6_src_addr != Bitvector<128>(0));
state.solver->add(ipv6_dst_addr != Bitvector<128>(0));
state.solver->add(ipv6_src_addr != Bitvector<128>(0, z3_context));
state.solver->add(ipv6_dst_addr != Bitvector<128>(0, z3_context));
// Neither src nor dst IPv6 addresses can be ::1 (loopback).
state.solver->add(ipv6_src_addr != Bitvector<128>(1));
state.solver->add(ipv6_dst_addr != Bitvector<128>(1));
state.solver->add(ipv6_src_addr != Bitvector<128>(1, z3_context));
state.solver->add(ipv6_dst_addr != Bitvector<128>(1, z3_context));

// ======VLAN constraints==========
// TODO: Make unconditional when we no longer need
Expand All @@ -193,40 +213,34 @@ absl::Status AddSanePacketConstraints(
state.context.ingress_headers.Get("vlan.vlan_id"));
// TODO: Consider testing the following VIDs when PacketIO is
// properly modeled.
state.solver->add(vlan_id != Bitvector<12>(0xFFF));
state.solver->add(vlan_id != Bitvector<12>(0x001));
state.solver->add(vlan_id != Bitvector<12>(0xFFF, z3_context));
state.solver->add(vlan_id != Bitvector<12>(0x001, z3_context));
}

return absl::OkStatus();
}

absl::StatusOr<z3::expr> IrValueToZ3Bitvector(const pdpi::IrValue& value,
int bitwidth) {
ASSIGN_OR_RETURN(const std::string bytes,
pdpi::IrValueToNormalizedByteString(value, bitwidth));
const std::string hex_string = pdpi::ByteStringToHexString(bytes);
return HexStringToZ3Bitvector(Z3Context(), hex_string, bitwidth);
}

// The following functions return Z3 constraints corresponding to `field`
// matching the given pdpi::IrMatch value.
absl::StatusOr<z3::expr> GetFieldMatchConstraints(z3::expr field, int bitwidth,
const pdpi::IrValue& match) {
ASSIGN_OR_RETURN(z3::expr value, IrValueToZ3Bitvector(match, bitwidth));
ASSIGN_OR_RETURN(z3::expr value,
IrValueToZ3Bitvector(match, bitwidth, field.ctx()));
return Eq(field, value);
}
absl::StatusOr<z3::expr> GetFieldMatchConstraints(
z3::expr field, int bitwidth, const pdpi::IrMatch::IrLpmMatch& match) {
ASSIGN_OR_RETURN(z3::expr value,
IrValueToZ3Bitvector(match.value(), bitwidth));
IrValueToZ3Bitvector(match.value(), bitwidth, field.ctx()));
return PrefixEq(field, value,
static_cast<unsigned int>(match.prefix_length()));
}
absl::StatusOr<z3::expr> GetFieldMatchConstraints(
z3::expr field, int bitwidth, const pdpi::IrMatch::IrTernaryMatch& match) {
ASSIGN_OR_RETURN(z3::expr value,
IrValueToZ3Bitvector(match.value(), bitwidth));
ASSIGN_OR_RETURN(z3::expr mask, IrValueToZ3Bitvector(match.mask(), bitwidth));
IrValueToZ3Bitvector(match.value(), bitwidth, field.ctx()));
ASSIGN_OR_RETURN(z3::expr mask,
IrValueToZ3Bitvector(match.mask(), bitwidth, field.ctx()));
ASSIGN_OR_RETURN(z3::expr masked_field, BitAnd(field, mask));
return Eq(masked_field, value);
}
Expand Down
2 changes: 1 addition & 1 deletion p4_symbolic/packet_synthesizer/util.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
#include "absl/status/status.h"
#include "p4_symbolic/symbolic/symbolic.h"

// This file contains varrious utility functions and classes used by packet
// This file contains various utility functions and classes used by packet
// synthesizer.

namespace p4_symbolic::packet_synthesizer {
Expand Down
2 changes: 1 addition & 1 deletion p4_symbolic/symbolic/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,7 @@ cc_test(
"//gutil:testing",
"//p4_pdpi:ir_cc_proto",
"//p4_symbolic:z3_util",
"@com_github_z3prover_z3//:api",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/strings",
"@com_google_googletest//:gtest_main",
Expand All @@ -156,7 +157,6 @@ cc_test(
":symbolic",
"//gutil:proto",
"//gutil:status_matchers",
"//p4_symbolic:z3_util",
"//p4_symbolic/ir",
"//p4_symbolic/ir:ir_cc_proto",
"@com_github_google_glog//:glog",
Expand Down
Loading

0 comments on commit 7cb0b4d

Please sign in to comment.