From 3e0513f9ce9a96204ba381df944d3ece705836c6 Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 18 Jan 2023 23:10:30 -0800 Subject: [PATCH 1/2] [P4_Symbolic] Update to comply with z3 version 4.12.0.0 (December 12th 2022). --- p4_symbolic/symbolic/BUILD.bazel | 18 ------ p4_symbolic/symbolic/expected/basic.smt2 | 4 +- .../symbolic/expected/conditional.smt2 | 4 +- .../expected/conditional_sequence.smt2 | 64 +++++++++---------- .../symbolic/expected/string_optional.smt2 | 8 +-- .../symbolic/expected/string_optional.txt | 8 +-- p4_symbolic/symbolic/expected/table.smt2 | 4 +- .../symbolic/expected/table_hit_1.smt2 | 4 +- p4_symbolic/symbolic/expected/table_hit_1.txt | 2 +- p4_symbolic/symbolic/expected/table_hit_2.txt | 4 +- p4_symbolic/symbolic/expected/vrf.smt2 | 4 +- p4_symbolic/symbolic/expected/vrf.txt | 32 +++++----- tests/gnoi/BUILD.bazel | 1 - 13 files changed, 69 insertions(+), 88 deletions(-) diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 75e349c8..c729f154 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -124,24 +124,6 @@ end_to_end_test( table_entries = "//p4_symbolic/testdata:conditional/conditional_sequence_entries.pb.txt", ) -end_to_end_test( - name = "table_hit_1_test", - output_golden_file = "expected/table_hit_1.txt", - p4_program = "//p4_symbolic/testdata:conditional/table_hit_1.p4", - port_count = 8, - smt_golden_file = "expected/table_hit_1.smt2", - table_entries = "//p4_symbolic/testdata:conditional/table_hit_1_entries.pb.txt", -) - -end_to_end_test( - name = "table_hit_2_test", - output_golden_file = "expected/table_hit_2.txt", - p4_program = "//p4_symbolic/testdata:conditional/table_hit_2.p4", - port_count = 8, - smt_golden_file = "expected/table_hit_2.smt2", - table_entries = "//p4_symbolic/testdata:conditional/table_hit_2_entries.pb.txt", -) - cc_test( name = "values_test", srcs = ["values_test.cc"], diff --git a/p4_symbolic/symbolic/expected/basic.smt2 b/p4_symbolic/symbolic/expected/basic.smt2 index 6fc6090c..ea71f237 100644 --- a/p4_symbolic/symbolic/expected/basic.smt2 +++ b/p4_symbolic/symbolic/expected/basic.smt2 @@ -97,8 +97,8 @@ (let (($x63 (and (and $x42 $x61) $x50))) (let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77)))))) (let (($x41 (= ?x113 (_ bv511 9)))) - (let (($x233 (and (not $x41) $x42))) - (and $x233 (= ?x112 0))))))))))))))))))))))) + (let (($x244 (and (not $x41) $x42))) + (and $x244 (= ?x112 0))))))))))))))))))))))) (check-sat) ; diff --git a/p4_symbolic/symbolic/expected/conditional.smt2 b/p4_symbolic/symbolic/expected/conditional.smt2 index f4fd807a..194deea5 100644 --- a/p4_symbolic/symbolic/expected/conditional.smt2 +++ b/p4_symbolic/symbolic/expected/conditional.smt2 @@ -125,7 +125,7 @@ (let ((?x45 (ite (and true (not $x41)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) (let (($x52 (= ?x50 (_ bv511 9)))) - (let (($x147 (and (not $x52) true))) - (and $x147 (= ?x47 0)))))))))))))) + (let (($x95 (and (not $x52) true))) + (and $x95 (= ?x47 0)))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 index a2d50bc8..43922001 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 @@ -13,8 +13,8 @@ (assert (let (($x41 (and true (not (= h1.f1 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x41) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x41) (= (- 1) (- 1))))))) (check-sat) ; @@ -32,8 +32,8 @@ (assert (let (($x46 (and true (not (= h1.f2 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x46) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x46) (= (- 1) (- 1))))))) (check-sat) ; @@ -51,8 +51,8 @@ (assert (let (($x50 (and true (not (= h1.f3 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x50) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x50) (= (- 1) (- 1))))))) (check-sat) ; @@ -70,8 +70,8 @@ (assert (let (($x54 (and true (not (= h1.f4 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x54) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x54) (= (- 1) (- 1))))))) (check-sat) ; @@ -89,8 +89,8 @@ (assert (let (($x58 (and true (not (= h1.f5 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x58) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x58) (= (- 1) (- 1))))))) (check-sat) ; @@ -108,8 +108,8 @@ (assert (let (($x62 (and true (not (= h1.f6 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x62) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x62) (= (- 1) (- 1))))))) (check-sat) ; @@ -127,8 +127,8 @@ (assert (let (($x66 (and true (not (= h1.f7 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x66) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x66) (= (- 1) (- 1))))))) (check-sat) ; @@ -146,8 +146,8 @@ (assert (let (($x70 (and true (not (= h1.f8 (concat (_ bv0 7) (_ bv0 1))))))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x70) (= (- 1) (- 1))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x70) (= (- 1) (- 1))))))) (check-sat) ; @@ -167,8 +167,8 @@ (let (($x38 (= h1.f1 ?x37))) (let (($x40 (and true $x38))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x40) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x40) (= (- 1) (- 1))))))))) (check-sat) ; @@ -188,8 +188,8 @@ (let (($x43 (= h1.f2 ?x37))) (let (($x45 (and true $x43))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x45) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x45) (= (- 1) (- 1))))))))) (check-sat) ; @@ -209,8 +209,8 @@ (let (($x47 (= h1.f3 ?x37))) (let (($x49 (and true $x47))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x49) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x49) (= (- 1) (- 1))))))))) (check-sat) ; @@ -230,8 +230,8 @@ (let (($x51 (= h1.f4 ?x37))) (let (($x53 (and true $x51))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x53) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x53) (= (- 1) (- 1))))))))) (check-sat) ; @@ -251,8 +251,8 @@ (let (($x55 (= h1.f5 ?x37))) (let (($x57 (and true $x55))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x57) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x57) (= (- 1) (- 1))))))))) (check-sat) ; @@ -272,8 +272,8 @@ (let (($x59 (= h1.f6 ?x37))) (let (($x61 (and true $x59))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x61) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x61) (= (- 1) (- 1))))))))) (check-sat) ; @@ -293,8 +293,8 @@ (let (($x63 (= h1.f7 ?x37))) (let (($x65 (and true $x63))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x65) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x65) (= (- 1) (- 1))))))))) (check-sat) ; @@ -314,8 +314,8 @@ (let (($x67 (= h1.f8 ?x37))) (let (($x69 (and true $x67))) (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x131 (not $x76))) - (and (and $x131 $x69) (= (- 1) (- 1))))))))) + (let (($x134 (not $x76))) + (and (and $x134 $x69) (= (- 1) (- 1))))))))) (check-sat) ; diff --git a/p4_symbolic/symbolic/expected/string_optional.smt2 b/p4_symbolic/symbolic/expected/string_optional.smt2 index cc1de54a..be5e676a 100644 --- a/p4_symbolic/symbolic/expected/string_optional.smt2 +++ b/p4_symbolic/symbolic/expected/string_optional.smt2 @@ -99,8 +99,8 @@ (let ((?x78 (ite (and (and true (not $x68)) true) (_ bv1 9) standard_metadata.egress_spec))) (let ((?x80 (ite $x69 (_ bv0 9) ?x78))) (let (($x49 (= ?x80 (_ bv511 9)))) - (let (($x132 (and (not $x49) true))) - (and $x132 (= ?x79 0))))))))))))))))))))))) + (let (($x117 (and (not $x49) true))) + (and $x117 (= ?x79 0))))))))))))))))))))))) (check-sat) ; @@ -260,8 +260,8 @@ (let (($x69 (and true $x68))) (let ((?x80 (ite $x69 (_ bv0 9) ?x78))) (let (($x49 (= ?x80 (_ bv511 9)))) - (let (($x132 (and (not $x49) true))) - (and $x132 (= ?x62 0))))))))))))))))))))))))) + (let (($x117 (and (not $x49) true))) + (and $x117 (= ?x62 0))))))))))))))))))))))))) (check-sat) ; diff --git a/p4_symbolic/symbolic/expected/string_optional.txt b/p4_symbolic/symbolic/expected/string_optional.txt index 49dd2cf9..f7b8daec 100644 --- a/p4_symbolic/symbolic/expected/string_optional.txt +++ b/p4_symbolic/symbolic/expected/string_optional.txt @@ -9,9 +9,9 @@ Finding packet for table MyIngress.optional_match and row 0 Finding packet for table MyIngress.optional_match and row 1 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000010 standard_metadata.egress_spec = #b000000001 - scalars.metadata.string_field = VALUE-1 + scalars.metadata.string_field = VALUE-2 Finding packet for table MyIngress.set_field_table and row -1 Cannot find solution! @@ -36,7 +36,7 @@ Finding packet for table MyIngress.set_field_table and row 2 Finding packet for table tbl_program92 and row -1 Dropped = 0 - standard_metadata.ingress_port = #b000000010 + standard_metadata.ingress_port = #b000000001 standard_metadata.egress_spec = #b000000001 - scalars.metadata.string_field = VALUE-2 + scalars.metadata.string_field = VALUE-1 diff --git a/p4_symbolic/symbolic/expected/table.smt2 b/p4_symbolic/symbolic/expected/table.smt2 index 0374cc85..71f928db 100644 --- a/p4_symbolic/symbolic/expected/table.smt2 +++ b/p4_symbolic/symbolic/expected/table.smt2 @@ -57,8 +57,8 @@ (let ((?x41 (ite (and (and true (not $x26)) $x29) (_ bv0 9) standard_metadata.egress_spec))) (let ((?x44 (ite $x30 (_ bv1 9) ?x41))) (let (($x35 (= ?x44 (_ bv511 9)))) - (let (($x102 (and (not $x35) true))) - (and $x102 (= ?x43 0)))))))))))))) + (let (($x109 (and (not $x35) true))) + (and $x109 (= ?x43 0)))))))))))))) (check-sat) ; diff --git a/p4_symbolic/symbolic/expected/table_hit_1.smt2 b/p4_symbolic/symbolic/expected/table_hit_1.smt2 index 1d233810..8860c77c 100644 --- a/p4_symbolic/symbolic/expected/table_hit_1.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_1.smt2 @@ -77,8 +77,8 @@ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) ?x41))) (let (($x49 (= ?x54 (_ bv511 9)))) - (let (($x207 (and (not $x49) true))) - (and $x207 (= ?x38 0))))))))))))) + (let (($x206 (and (not $x49) true))) + (and $x206 (= ?x38 0))))))))))))) (check-sat) ; diff --git a/p4_symbolic/symbolic/expected/table_hit_1.txt b/p4_symbolic/symbolic/expected/table_hit_1.txt index 8b0d0026..5b9a7645 100644 --- a/p4_symbolic/symbolic/expected/table_hit_1.txt +++ b/p4_symbolic/symbolic/expected/table_hit_1.txt @@ -4,7 +4,7 @@ Cannot find solution! Finding packet for table MyIngress.t_1 and row 0 Dropped = 0 standard_metadata.ingress_port = #b000000000 - standard_metadata.egress_spec = #b000000011 + standard_metadata.egress_spec = #b000000010 Finding packet for table MyIngress.t_2 and row -1 Dropped = 0 diff --git a/p4_symbolic/symbolic/expected/table_hit_2.txt b/p4_symbolic/symbolic/expected/table_hit_2.txt index 963d47c4..bf736f78 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.txt +++ b/p4_symbolic/symbolic/expected/table_hit_2.txt @@ -1,12 +1,12 @@ Finding packet for table MyIngress.t1 and row -1 Dropped = 0 standard_metadata.ingress_port = #b000000000 - standard_metadata.egress_spec = #b000000011 + standard_metadata.egress_spec = #b000000000 Finding packet for table MyIngress.t1 and row 0 Dropped = 0 standard_metadata.ingress_port = #b000000000 - standard_metadata.egress_spec = #b000000001 + standard_metadata.egress_spec = #b000000010 Finding packet for table MyIngress.t2 and row -1 Dropped = 0 diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2 index 423eab16..2bf13d32 100644 --- a/p4_symbolic/symbolic/expected/vrf.smt2 +++ b/p4_symbolic/symbolic/expected/vrf.smt2 @@ -139,8 +139,8 @@ (let (($x112 (and (and $x85 (not $x91)) $x96))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142)))) (let (($x52 (= ?x158 (_ bv511 9)))) - (let (($x308 (and (not $x52) $x85))) - (and $x308 (= ?x157 0))))))))))))))))))))))))))))))) + (let (($x307 (and (not $x52) $x85))) + (and $x307 (= ?x157 0))))))))))))))))))))))))))))))) (check-sat) ; diff --git a/p4_symbolic/symbolic/expected/vrf.txt b/p4_symbolic/symbolic/expected/vrf.txt index 00de6e1b..c2573bf9 100644 --- a/p4_symbolic/symbolic/expected/vrf.txt +++ b/p4_symbolic/symbolic/expected/vrf.txt @@ -3,17 +3,17 @@ Cannot find solution! Finding packet for table packet_ingress.ipv4_lpm_table and row 0 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000000 ipv4.srcAddr = #x29210000 - ipv4.dstAddr = #x0a0a0002 + ipv4.dstAddr = #x0a0a0080 ethernet.dstAddr = #x000000000000 scalars.local_metadata_t.vrf = VRF1 scalars.local_metadata_t.vrf_is_valid = #b1 Finding packet for table packet_ingress.ipv4_lpm_table and row 1 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x29210000 ipv4.dstAddr = #x0a0a0000 @@ -23,17 +23,17 @@ Finding packet for table packet_ingress.ipv4_lpm_table and row 1 Finding packet for table packet_ingress.ipv4_lpm_table and row 2 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x29210000 - ipv4.dstAddr = #x0a0e0000 + ipv4.dstAddr = #x0a8a0000 ethernet.dstAddr = #x00000000000a scalars.local_metadata_t.vrf = VRF1 scalars.local_metadata_t.vrf_is_valid = #b1 Finding packet for table packet_ingress.ipv4_lpm_table and row 3 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x20210100 ipv4.dstAddr = #x14140000 @@ -43,17 +43,17 @@ Finding packet for table packet_ingress.ipv4_lpm_table and row 3 Finding packet for table packet_ingress.set_vrf_table and row -1 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 - ipv4.srcAddr = #x08000909 - ipv4.dstAddr = #x14140000 + ipv4.srcAddr = #x21000809 + ipv4.dstAddr = #x00000000 ethernet.dstAddr = #x000000000000 scalars.local_metadata_t.vrf = VRF1 scalars.local_metadata_t.vrf_is_valid = #b0 Finding packet for table packet_ingress.set_vrf_table and row 0 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x20210100 ipv4.dstAddr = #x14140000 @@ -63,20 +63,20 @@ Finding packet for table packet_ingress.set_vrf_table and row 0 Finding packet for table packet_ingress.set_vrf_table and row 1 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x21210000 - ipv4.dstAddr = #x0a140000 + ipv4.dstAddr = #x0a000000 ethernet.dstAddr = #x00000000000a scalars.local_metadata_t.vrf = VRF1 scalars.local_metadata_t.vrf_is_valid = #b1 Finding packet for table tbl_vrf133 and row -1 Dropped = 0 - standard_metadata.ingress_port = #b000000001 + standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x21210000 - ipv4.dstAddr = #x0a140000 - ethernet.dstAddr = #x00000000000a + ipv4.dstAddr = #x0a000000 + ethernet.dstAddr = #x000000000000 scalars.local_metadata_t.vrf = VRF1 - scalars.local_metadata_t.vrf_is_valid = #b1 + scalars.local_metadata_t.vrf_is_valid = #b0 diff --git a/tests/gnoi/BUILD.bazel b/tests/gnoi/BUILD.bazel index d86c11c4..fa89d2b2 100644 --- a/tests/gnoi/BUILD.bazel +++ b/tests/gnoi/BUILD.bazel @@ -39,7 +39,6 @@ cc_library( "@com_google_absl//absl/container:flat_hash_set", "@com_google_absl//absl/flags:flag", "@com_google_absl//absl/random", - "@com_github_grpc_grpc//:grpc++", "@com_google_absl//absl/strings", "@com_google_absl//absl/time", "@com_google_googletest//:gtest", From d49ec9dca6034a9841132d31492ff5b5dddbacde Mon Sep 17 00:00:00 2001 From: jonathan-dilorenzo Date: Fri, 17 Mar 2023 10:36:50 -0700 Subject: [PATCH 2/2] [P4 Symbolic] Make certain Z3 APIs more general. PiperOrigin-RevId: 517449221 --- p4_symbolic/packet_synthesizer/util.cc | 2 +- p4_symbolic/symbolic/action.cc | 10 +- p4_symbolic/symbolic/table.cc | 154 ++++++++++++------------- p4_symbolic/symbolic/table.h | 8 ++ p4_symbolic/symbolic/values.cc | 8 +- p4_symbolic/symbolic/values.h | 3 +- p4_symbolic/symbolic/values_test.cc | 37 +++--- p4_symbolic/z3_util.cc | 5 +- p4_symbolic/z3_util.h | 5 +- 9 files changed, 124 insertions(+), 108 deletions(-) diff --git a/p4_symbolic/packet_synthesizer/util.cc b/p4_symbolic/packet_synthesizer/util.cc index 0019ab22..98432909 100644 --- a/p4_symbolic/packet_synthesizer/util.cc +++ b/p4_symbolic/packet_synthesizer/util.cc @@ -185,7 +185,7 @@ absl::StatusOr IrValueToZ3Bitvector(const pdpi::IrValue& value, ASSIGN_OR_RETURN(const std::string bytes, pdpi::IrValueToNormalizedByteString(value, bitwidth)); const std::string hex_string = pdpi::ByteStringToHexString(bytes); - return HexStringToZ3Bitvector(hex_string, bitwidth); + return HexStringToZ3Bitvector(Z3Context(), hex_string, bitwidth); } // The following functions return Z3 constraints corresponding to `field` diff --git a/p4_symbolic/symbolic/action.cc b/p4_symbolic/symbolic/action.cc index 527133db..e5b55b4f 100644 --- a/p4_symbolic/symbolic/action.cc +++ b/p4_symbolic/symbolic/action.cc @@ -168,7 +168,7 @@ absl::StatusOr EvaluateHexStr(const ir::HexstrValue &hexstr) { ASSIGN_OR_RETURN(pdpi::IrValue parsed_value, values::ParseIrValue(hexstr.value())); - return HexStringToZ3Bitvector(hexstr.value()); + return HexStringToZ3Bitvector(Z3Context(), hexstr.value()); } absl::StatusOr EvaluateBool(const ir::BoolValue &bool_value) { @@ -336,10 +336,10 @@ absl::Status EvaluateAction(const ir::Action &action, const std::string ¶meter_type_name = parameter.param().type_name().name(); const int bitwidth = parameter.param().bitwidth(); - ASSIGN_OR_RETURN( - z3::expr parameter_value, - values::FormatP4RTValue(/*field_name=*/"", parameter_type_name, - args.at(i - 1).value(), bitwidth, translator)); + ASSIGN_OR_RETURN(z3::expr parameter_value, + values::FormatP4RTValue( + Z3Context(), /*field_name=*/"", parameter_type_name, + args.at(i - 1).value(), bitwidth, translator)); context.scope.insert({parameter_name, parameter_value}); } diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index 948ed37c..39d0ed24 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -154,81 +154,6 @@ std::vector> SortEntries( return sorted_entries; } -// Analyze a single match that is part of a table entry. -// Constructs a symbolic expression that semantically corresponds to this -// match. -absl::StatusOr EvaluateSingleMatch( - p4::config::v1::MatchField match_definition, const std::string &field_name, - const z3::expr &field_expression, const pdpi::IrMatch &match, - values::P4RuntimeTranslator *translator) { - if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) { - // Arch-specific match type. - return absl::InvalidArgumentError( - absl::StrCat("Found match with non-standard type")); - } - - absl::Status mismatch = - gutil::InvalidArgumentErrorBuilder() - << "match on field '" << field_name << "' must be of type " - << p4::config::v1::MatchField::MatchType_Name( - match_definition.match_type()) - << " according to the table definition, but got entry with match: " - << match_definition.ShortDebugString(); - - auto GetZ3Value = - [&](const pdpi::IrValue &value) -> absl::StatusOr { - return values::FormatP4RTValue(field_name, - match_definition.type_name().name(), value, - match_definition.bitwidth(), translator); - }; - - switch (match_definition.match_type()) { - case p4::config::v1::MatchField::EXACT: { - if (match.match_value_case() != pdpi::IrMatch::kExact) return mismatch; - ASSIGN_OR_RETURN(z3::expr value_expression, GetZ3Value(match.exact())); - return operators::Eq(field_expression, value_expression); - } - - case p4::config::v1::MatchField::LPM: { - if (match.match_value_case() != pdpi::IrMatch::kLpm) return mismatch; - - ASSIGN_OR_RETURN(z3::expr value_expression, - GetZ3Value(match.lpm().value())); - return operators::PrefixEq( - field_expression, value_expression, - static_cast(match.lpm().prefix_length())); - } - - case p4::config::v1::MatchField::TERNARY: { - if (match.match_value_case() != pdpi::IrMatch::kTernary) return mismatch; - - ASSIGN_OR_RETURN(z3::expr mask_expression, - GetZ3Value(match.ternary().mask())); - ASSIGN_OR_RETURN(z3::expr value_expression, - GetZ3Value(match.ternary().value())); - ASSIGN_OR_RETURN(z3::expr masked_field, - operators::BitAnd(field_expression, mask_expression)); - return operators::Eq(masked_field, value_expression); - } - - case p4::config::v1::MatchField::OPTIONAL: { - if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch; - // According to the P4Runtime spec, "for don't care matches, the P4Runtime - // client must omit the field's entire FieldMatch entry when building the - // match repeated field of the TableEntry message". Therefore, if the - // match value is present for an optional match type, it must be a - // concrete value. - ASSIGN_OR_RETURN(z3::expr value_expression, - GetZ3Value(match.optional().value())); - return operators::Eq(field_expression, value_expression); - } - - default: - return absl::UnimplementedError(absl::StrCat( - "Found unsupported match type ", match_definition.DebugString())); - } -} - // Constructs a symbolic expression that is true if and only if this entry // is matched on. absl::StatusOr EvaluateTableEntryCondition( @@ -279,9 +204,10 @@ absl::StatusOr EvaluateTableEntryCondition( ASSIGN_OR_RETURN( z3::expr match_field_expr, action::EvaluateFieldValue(match_field, state, fake_context)); - ASSIGN_OR_RETURN(z3::expr match_expression, - EvaluateSingleMatch(match_definition, field_name, - match_field_expr, match, translator)); + ASSIGN_OR_RETURN( + z3::expr match_expression, + EvaluateSingleMatch(Z3Context(), match_definition, field_name, + match_field_expr, match, translator)); ASSIGN_OR_RETURN(condition_expression, operators::And(condition_expression, match_expression)); } @@ -350,6 +276,78 @@ absl::Status EvaluateTableEntryAction( } // namespace +absl::StatusOr EvaluateSingleMatch( + z3::context &context, p4::config::v1::MatchField match_definition, + const std::string &field_name, const z3::expr &field_expression, + const pdpi::IrMatch &match, values::P4RuntimeTranslator *translator) { + if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) { + // Arch-specific match type. + return absl::InvalidArgumentError( + absl::StrCat("Found match with non-standard type")); + } + + absl::Status mismatch = + gutil::InvalidArgumentErrorBuilder() + << "match on field '" << field_name << "' must be of type " + << p4::config::v1::MatchField::MatchType_Name( + match_definition.match_type()) + << " according to the table definition, but got entry with match: " + << match_definition.ShortDebugString(); + + auto GetZ3Value = + [&](const pdpi::IrValue &value) -> absl::StatusOr { + return values::FormatP4RTValue(context, field_name, + match_definition.type_name().name(), value, + match_definition.bitwidth(), translator); + }; + + switch (match_definition.match_type()) { + case p4::config::v1::MatchField::EXACT: { + if (match.match_value_case() != pdpi::IrMatch::kExact) return mismatch; + ASSIGN_OR_RETURN(z3::expr value_expression, GetZ3Value(match.exact())); + return operators::Eq(field_expression, value_expression); + } + + case p4::config::v1::MatchField::LPM: { + if (match.match_value_case() != pdpi::IrMatch::kLpm) return mismatch; + + ASSIGN_OR_RETURN(z3::expr value_expression, + GetZ3Value(match.lpm().value())); + return operators::PrefixEq( + field_expression, value_expression, + static_cast(match.lpm().prefix_length())); + } + + case p4::config::v1::MatchField::TERNARY: { + if (match.match_value_case() != pdpi::IrMatch::kTernary) return mismatch; + + ASSIGN_OR_RETURN(z3::expr mask_expression, + GetZ3Value(match.ternary().mask())); + ASSIGN_OR_RETURN(z3::expr value_expression, + GetZ3Value(match.ternary().value())); + ASSIGN_OR_RETURN(z3::expr masked_field, + operators::BitAnd(field_expression, mask_expression)); + return operators::Eq(masked_field, value_expression); + } + + case p4::config::v1::MatchField::OPTIONAL: { + if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch; + // According to the P4Runtime spec, "for don't care matches, the P4Runtime + // client must omit the field's entire FieldMatch entry when building the + // match repeated field of the TableEntry message". Therefore, if the + // match value is present for an optional match type, it must be a + // concrete value. + ASSIGN_OR_RETURN(z3::expr value_expression, + GetZ3Value(match.optional().value())); + return operators::Eq(field_expression, value_expression); + } + + default: + return absl::UnimplementedError(absl::StrCat( + "Found unsupported match type ", match_definition.DebugString())); + } +} + absl::StatusOr EvaluateTable( const Dataplane &data_plane, const ir::Table &table, const std::vector &entries, diff --git a/p4_symbolic/symbolic/table.h b/p4_symbolic/symbolic/table.h index 09def04b..7a6ae699 100644 --- a/p4_symbolic/symbolic/table.h +++ b/p4_symbolic/symbolic/table.h @@ -45,6 +45,14 @@ absl::StatusOr EvaluateTable( SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard); +// Analyze a single match that is part of a table entry. +// Constructs a symbolic expression that semantically corresponds to this +// match. +absl::StatusOr EvaluateSingleMatch( + z3::context &context, p4::config::v1::MatchField match_definition, + const std::string &field_name, const z3::expr &field_expression, + const pdpi::IrMatch &match, values::P4RuntimeTranslator *translator); + } // namespace table } // namespace symbolic } // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc index bfdf6666..b41af2f9 100644 --- a/p4_symbolic/symbolic/values.cc +++ b/p4_symbolic/symbolic/values.cc @@ -75,7 +75,8 @@ absl::StatusOr ParseIrValue(const std::string &value) { } } -absl::StatusOr FormatP4RTValue(const std::string &field_name, +absl::StatusOr FormatP4RTValue(z3::context &context, + const std::string &field_name, const std::string &type_name, const pdpi::IrValue &value, int bitwidth, @@ -110,7 +111,7 @@ absl::StatusOr FormatP4RTValue(const std::string &field_name, type_name, bitwidth)); } - return Z3Context().bv_val(int_value, bitwidth); + return context.bv_val(int_value, bitwidth); } default: { if (translator->fields_p4runtime_type.count(field_name)) { @@ -128,7 +129,8 @@ absl::StatusOr FormatP4RTValue(const std::string &field_name, pdpi::ArbitraryByteStringToIrValue( pdpi::HEX_STRING, bitwidth, byte_string)); // Now convert the hex string internally. - return HexStringToZ3Bitvector(normalized_value.hex_str(), bitwidth); + return HexStringToZ3Bitvector(context, normalized_value.hex_str(), + bitwidth); } } } diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h index d064fdd9..2d9d0118 100644 --- a/p4_symbolic/symbolic/values.h +++ b/p4_symbolic/symbolic/values.h @@ -113,7 +113,8 @@ absl::StatusOr ParseIrValue(const std::string &value); // translated values (i.e. string IrValues) the bitwidth MUST be 0, in which // case we use the minimum number of bits to encode the resulting translated // value. -absl::StatusOr FormatP4RTValue(const std::string &field_name, +absl::StatusOr FormatP4RTValue(z3::context &context, + const std::string &field_name, const std::string &type_name, const pdpi::IrValue &value, int bitwidth, diff --git a/p4_symbolic/symbolic/values_test.cc b/p4_symbolic/symbolic/values_test.cc index e1ab49ac..b9346ddc 100644 --- a/p4_symbolic/symbolic/values_test.cc +++ b/p4_symbolic/symbolic/values_test.cc @@ -28,9 +28,10 @@ TEST(TranslateValueToP4RT, ReverseTranslatedValuesAreEqualToTheOriginalOnes) { const std::string id = absl::StrCat("id-", i); pdpi::IrValue ir_value; ir_value.set_str(id); - ASSERT_OK_AND_ASSIGN(z3::expr expr, - FormatP4RTValue(kFieldName, kFieldType, ir_value, - /*bitwidth=*/0, &translator)); + ASSERT_OK_AND_ASSIGN( + z3::expr expr, + FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, + /*bitwidth=*/0, &translator)); z3_value_to_id[expr.to_string()] = id; } @@ -49,9 +50,10 @@ TEST(FormatP4RTValue, WorksFor64BitIPv6) { ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(ipv6: "0000:ffff:ffff:ffff::")pb")); - ASSERT_OK_AND_ASSIGN(z3::expr z3_expr, - FormatP4RTValue(kFieldName, kFieldType, ir_value, - /*bitwidth=*/64, &trasnlator)); + ASSERT_OK_AND_ASSIGN( + z3::expr z3_expr, + FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, + /*bitwidth=*/64, &trasnlator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x0000'ffff'ffff'ffffULL); } @@ -59,9 +61,10 @@ TEST(FormatP4RTValue, WorksForIpv4) { P4RuntimeTranslator trasnlator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(ipv4: "127.0.0.1")pb")); - ASSERT_OK_AND_ASSIGN(z3::expr z3_expr, - FormatP4RTValue(kFieldName, kFieldType, ir_value, - /*bitwidth=*/32, &trasnlator)); + ASSERT_OK_AND_ASSIGN( + z3::expr z3_expr, + FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, + /*bitwidth=*/32, &trasnlator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x7f000001); } @@ -69,9 +72,10 @@ TEST(FormatP4RTValue, WorksForMac) { P4RuntimeTranslator trasnlator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(mac: "01:02:03:04:05:06")pb")); - ASSERT_OK_AND_ASSIGN(z3::expr z3_expr, - FormatP4RTValue(kFieldName, kFieldType, ir_value, - /*bitwidth=*/48, &trasnlator)); + ASSERT_OK_AND_ASSIGN( + z3::expr z3_expr, + FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, + /*bitwidth=*/48, &trasnlator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x01'02'03'04'05'06ULL); } @@ -79,9 +83,10 @@ TEST(FormatP4RTValue, WorksForHexString) { P4RuntimeTranslator trasnlator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(hex_str: "0xabcd")pb")); - ASSERT_OK_AND_ASSIGN(z3::expr z3_expr, - FormatP4RTValue(kFieldName, kFieldType, ir_value, - /*bitwidth=*/16, &trasnlator)); + ASSERT_OK_AND_ASSIGN( + z3::expr z3_expr, + FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, + /*bitwidth=*/16, &trasnlator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0xabcd); } @@ -89,7 +94,7 @@ TEST(FormatP4RTValue, FailsForStringWithNonZeroBitwidth) { P4RuntimeTranslator trasnlator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(str: "dummy_value")pb")); - ASSERT_THAT(FormatP4RTValue(kFieldName, kFieldType, ir_value, + ASSERT_THAT(FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, /*bitwidth=*/16, &trasnlator), StatusIs(absl::StatusCode::kInvalidArgument)); } diff --git a/p4_symbolic/z3_util.cc b/p4_symbolic/z3_util.cc index a09186ca..1471a578 100644 --- a/p4_symbolic/z3_util.cc +++ b/p4_symbolic/z3_util.cc @@ -55,7 +55,8 @@ absl::StatusOr EvalZ3Int(const z3::expr& int_expr, return model.eval(int_expr, true).get_numeral_int(); } -absl::StatusOr HexStringToZ3Bitvector(const std::string& hex_string, +absl::StatusOr HexStringToZ3Bitvector(z3::context& context, + const std::string& hex_string, absl::optional bitwidth) { // TODO: Insert check to ensure this won't throw an exception. mpz_class integer = mpz_class(hex_string, /*base=*/0); @@ -63,7 +64,7 @@ absl::StatusOr HexStringToZ3Bitvector(const std::string& hex_string, if (!bitwidth.has_value()) { bitwidth = integer.get_str(/*base=*/2).size(); } - return Z3Context().bv_val(decimal.c_str(), *bitwidth); + return context.bv_val(decimal.c_str(), *bitwidth); } uint64_t Z3ValueStringToInt(const std::string& value) { diff --git a/p4_symbolic/z3_util.h b/p4_symbolic/z3_util.h index f516f81f..7bb52e7a 100644 --- a/p4_symbolic/z3_util.h +++ b/p4_symbolic/z3_util.h @@ -44,9 +44,10 @@ absl::StatusOr> EvalZ3Bitvector(const z3::expr& bv_expr, // -- Constructing Z3 expressions ---------------------------------------------- // Returns Z3 bitvector of the given `hex_string` value. -// If no bitwidth is +// If no bitwidth is given, the size of the bitvector is derived from +// `hex_string`. absl::StatusOr HexStringToZ3Bitvector( - const std::string& hex_string, + z3::context& context, const std::string& hex_string, absl::optional bitwidth = absl::nullopt); // -- Misc. --------------------------------------------------------------------