From 3e0513f9ce9a96204ba381df944d3ece705836c6 Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 18 Jan 2023 23:10:30 -0800 Subject: [PATCH 1/6] [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/6] [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. -------------------------------------------------------------------- From c43f6b86959f90c041964ef49acb267362518660 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 25 May 2023 09:22:32 -0700 Subject: [PATCH 3/6] Extend BMv2 proto to support parsers. PiperOrigin-RevId: 535281220 --- p4_symbolic/bmv2/bmv2.proto | 100 ++++++++++++++++--- p4_symbolic/bmv2/expected/basic.pb.txt | 45 +++++++++ p4_symbolic/bmv2/expected/set_invalid.pb.txt | 17 ++++ p4_symbolic/bmv2/expected/table_hit_1.pb.txt | 17 ++++ p4_symbolic/bmv2/expected/table_hit_2.pb.txt | 17 ++++ p4_symbolic/bmv2/test.cc | 4 +- 6 files changed, 183 insertions(+), 17 deletions(-) diff --git a/p4_symbolic/bmv2/bmv2.proto b/p4_symbolic/bmv2/bmv2.proto index 7d0352c0..1062fc94 100644 --- a/p4_symbolic/bmv2/bmv2.proto +++ b/p4_symbolic/bmv2/bmv2.proto @@ -13,7 +13,9 @@ // limitations under the License. // This file contains protobuf definitions for parsing bmv2 json -// files (outputs of p4c). +// files (outputs of p4c). The JSON format reference can be found at +// https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md +// or third_party/p4lang_behavioral_model/docs/JSON_format.md // Some attributes here are intentionally un-constrained (e.g. // struct). This allows parsing of radically different possibilities // or types of constructs that may appear interchangably in that @@ -130,34 +132,104 @@ message Parser { int32 id = 2; // The name of the start state of the parser. string init_state = 3; - // A list of all parser states. - repeated ParserState parse_states = 4; + // A list of all parse states. + repeated ParseState parse_states = 4; } -// Defines a parser state. -message ParserState { - // The user defined name of the state (not qualified). +// Defines a parse state. +// The body of a parse state consists of a series of parser statements (which +// p4c compiles into a list of parser operations), such as assignments, +// variable/constant declarations, conditionals, etc., followed by a transition +// statement. +message ParseState { + // The user-defined name of the state (not qualified). // It does not include the name of the parser. string name = 1; - // Auto generated ID unique among all parser states including those + // Auto-generated ID unique among all parse states including those // belonging to a different parser. int32 id = 2; - // All the possible transitions from this state to different states. + // Ordered list of operations performed in the current parse state. + repeated ParserOperation parser_ops = 3; + // All the possible transitions from this state to other states. repeated ParserTransition transitions = 4; + // Optionally the transition statement contains a "select" expression which + // acts similarly to the switch-case expression in C. The condition of the + // select expression is a list of expressions, which usually contains only one + // element in typical cases. This transition_key represents exactly the + // condition of the select expression as a list of key fields. It will be an + // empty list if the parse state contains only one default transition. + // Reference: https://p4.org/p4-spec/docs/P4-16-v-1.2.3.html#sec-select + repeated ParserTransitionKeyField transition_key = 5; } -// Defines a transition between two parser states. +// Defines a parser operation corresponding to a single statement in a parse +// state. For instance, a parser operation can be a "set" operation +// (corresponding to an assignment statement), an "extract" operation +// (corresponding to an "extract" method call), or other primitives supported by +// the target implementation. Reference: +// https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md#parser-operations. +message ParserOperation { + // Parser operation types. + enum ParserOpType { + unspecified = 0; + // Performs extraction for a fixed-width header. + extract = 1; + // Performs extraction for a variable-width header. + extract_VL = 2; + // Sets a field with the given value. + set = 3; + // Verifies if the given condition holds true. If not, sets + // standard_metadata.parser_error with the specified error code. + verify = 4; + // Shifts the current read position by the given number of bytes. + // Deprecated in favor of advance. + shift = 5; + // Advances the current read position by the given number of bits. + // BMv2 currently requires the number of bits to be a multiple of 8. + advance = 6; + // An invocation of an extern method (must be supported by the target). + primitive = 7; + } + + // The type of parser operation. + ParserOpType op = 1; + // Parameters of the operation. + // The semantics of parameters depend on the type of operation. + // https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md#parser-operations + repeated google.protobuf.Struct parameters = 2; +} + +// One field of a transition key. +message ParserTransitionKeyField { + enum ParserTransKeyFieldType { + unspecified = 0; + // Specifies a normal header field. + field = 1; + // Specifies a header field of the last extracted instance in a stack. + stack_field = 2; + // Specifies a header field of the last extracted instance in a union stack. + union_stack_field = 3; + // Evaluates to a set of bits from the input packet without advancing the + // current read position. + lookahead = 4; + } + + ParserTransKeyFieldType type = 1; + google.protobuf.ListValue value = 2; +} + +// Defines a transition between two parse states. message ParserTransition { - // The value of the condition/match dictating whether - // this transition is applied or not. - // A hexstring or a parser value set depending on the type. + // The value of the condition/match dictating whether this transition is + // applied or not. It can be an empty string (a default transition), a + // hexstring, or a parser value set depending on the type. string value = 1; - // The type of the value above, usually a hex string. + // The type of the transition value, usually a hex string. ParserTransitionType type = 2; // Any mask applied by the transition, if no mask is applied, // protobuf will parse this as "". string mask = 3; - // The name of the state this transition points to. + // The name of the next parse state, or "" if this is the last state. string next_state = 4; } diff --git a/p4_symbolic/bmv2/expected/basic.pb.txt b/p4_symbolic/bmv2/expected/basic.pb.txt index a70f11ba..78bfd67d 100644 --- a/p4_symbolic/bmv2/expected/basic.pb.txt +++ b/p4_symbolic/bmv2/expected/basic.pb.txt @@ -391,6 +391,23 @@ parsers { init_state: "start" parse_states { name: "start" + parser_ops { + op: extract + parameters { + fields { + key: "type" + value { + string_value: "regular" + } + } + fields { + key: "value" + value { + string_value: "ethernet" + } + } + } + } transitions { value: "0x0800" type: hexstr @@ -398,10 +415,38 @@ parsers { } transitions { } + transition_key { + type: field + value { + values { + string_value: "ethernet" + } + values { + string_value: "etherType" + } + } + } } parse_states { name: "parse_ipv4" id: 1 + parser_ops { + op: extract + parameters { + fields { + key: "type" + value { + string_value: "regular" + } + } + fields { + key: "value" + value { + string_value: "ipv4" + } + } + } + } transitions { } } diff --git a/p4_symbolic/bmv2/expected/set_invalid.pb.txt b/p4_symbolic/bmv2/expected/set_invalid.pb.txt index 3c4a7ca8..36110f33 100644 --- a/p4_symbolic/bmv2/expected/set_invalid.pb.txt +++ b/p4_symbolic/bmv2/expected/set_invalid.pb.txt @@ -228,6 +228,23 @@ parsers { init_state: "start" parse_states { name: "start" + parser_ops { + op: extract + parameters { + fields { + key: "type" + value { + string_value: "regular" + } + } + fields { + key: "value" + value { + string_value: "h" + } + } + } + } transitions { } } diff --git a/p4_symbolic/bmv2/expected/table_hit_1.pb.txt b/p4_symbolic/bmv2/expected/table_hit_1.pb.txt index 508e64b5..13e64a2b 100644 --- a/p4_symbolic/bmv2/expected/table_hit_1.pb.txt +++ b/p4_symbolic/bmv2/expected/table_hit_1.pb.txt @@ -250,6 +250,23 @@ parsers { init_state: "start" parse_states { name: "start" + parser_ops { + op: extract + parameters { + fields { + key: "type" + value { + string_value: "regular" + } + } + fields { + key: "value" + value { + string_value: "ethernet" + } + } + } + } transitions { } } diff --git a/p4_symbolic/bmv2/expected/table_hit_2.pb.txt b/p4_symbolic/bmv2/expected/table_hit_2.pb.txt index ba3f44aa..e0b7a17b 100644 --- a/p4_symbolic/bmv2/expected/table_hit_2.pb.txt +++ b/p4_symbolic/bmv2/expected/table_hit_2.pb.txt @@ -261,6 +261,23 @@ parsers { init_state: "start" parse_states { name: "start" + parser_ops { + op: extract + parameters { + fields { + key: "type" + value { + string_value: "regular" + } + } + fields { + key: "value" + value { + string_value: "h1" + } + } + } + } transitions { } } diff --git a/p4_symbolic/bmv2/test.cc b/p4_symbolic/bmv2/test.cc index 2764747a..a2b70d89 100644 --- a/p4_symbolic/bmv2/test.cc +++ b/p4_symbolic/bmv2/test.cc @@ -19,7 +19,6 @@ // objects using protobuf text format and json format to two output files. // The output files paths are provided as command line flags. -#include #include #include @@ -28,7 +27,6 @@ #include "absl/flags/usage.h" #include "absl/status/status.h" #include "absl/strings/str_format.h" -#include "google/protobuf/text_format.h" #include "google/protobuf/util/json_util.h" #include "gutil/io.h" #include "gutil/proto.h" @@ -82,7 +80,7 @@ int main(int argc, char *argv[]) { // Verify link and compile versions are the same. // GOOGLE_PROTOBUF_VERIFY_VERSION; - // Command line arugments and help message. + // Command line arguments and help message. absl::SetProgramUsageMessage( absl::StrFormat("usage: %s %s", argv[0], "--bmv2=path/to/bmv2.json " From acf5a821cab9859716c88280f52bdbfaf0273e97 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 21 Nov 2024 14:46:44 +0530 Subject: [PATCH 4/6] [P4_Symbolic] Adding p4_symbolic/ir/expected/hex_string_transition.txt [Extend IR proto and translation to support parsers] --- .../ir/expected/hex_string_transition.txt | 349 ++++++++++++++++++ 1 file changed, 349 insertions(+) create mode 100644 p4_symbolic/ir/expected/hex_string_transition.txt diff --git a/p4_symbolic/ir/expected/hex_string_transition.txt b/p4_symbolic/ir/expected/hex_string_transition.txt new file mode 100644 index 00000000..ea9b2f3d --- /dev/null +++ b/p4_symbolic/ir/expected/hex_string_transition.txt @@ -0,0 +1,349 @@ +headers { + key: "ethernet" + value { + name: "ethernet_t" + id: 2 + fields { + key: "dst_addr" + value { + name: "dst_addr" + bitwidth: 48 + } + } + fields { + key: "ether_type" + value { + name: "ether_type" + bitwidth: 16 + } + } + fields { + key: "src_addr" + value { + name: "src_addr" + bitwidth: 48 + } + } + } +} +headers { + key: "ipv4" + value { + name: "ipv4_t" + id: 3 + fields { + key: "do_not_fragment" + value { + name: "do_not_fragment" + bitwidth: 1 + } + } + fields { + key: "dscp" + value { + name: "dscp" + bitwidth: 6 + } + } + fields { + key: "dst_addr" + value { + name: "dst_addr" + bitwidth: 32 + } + } + fields { + key: "ecn" + value { + name: "ecn" + bitwidth: 2 + } + } + fields { + key: "frag_offset" + value { + name: "frag_offset" + bitwidth: 13 + } + } + fields { + key: "header_checksum" + value { + name: "header_checksum" + bitwidth: 16 + } + } + fields { + key: "identification" + value { + name: "identification" + bitwidth: 16 + } + } + fields { + key: "ihl" + value { + name: "ihl" + bitwidth: 4 + } + } + fields { + key: "more_fragments" + value { + name: "more_fragments" + bitwidth: 1 + } + } + fields { + key: "protocol" + value { + name: "protocol" + bitwidth: 8 + } + } + fields { + key: "reserved" + value { + name: "reserved" + bitwidth: 1 + } + } + fields { + key: "src_addr" + value { + name: "src_addr" + bitwidth: 32 + } + } + fields { + key: "total_len" + value { + name: "total_len" + bitwidth: 16 + } + } + fields { + key: "ttl" + value { + name: "ttl" + bitwidth: 8 + } + } + fields { + key: "version" + value { + name: "version" + bitwidth: 4 + } + } + } +} +headers { + key: "scalars" + value { + name: "scalars_0" + } +} +headers { + key: "standard_metadata" + value { + name: "standard_metadata" + id: 1 + fields { + key: "_padding" + value { + name: "_padding" + bitwidth: 3 + } + } + fields { + key: "checksum_error" + value { + name: "checksum_error" + bitwidth: 1 + } + } + fields { + key: "deq_qdepth" + value { + name: "deq_qdepth" + bitwidth: 19 + } + } + fields { + key: "deq_timedelta" + value { + name: "deq_timedelta" + bitwidth: 32 + } + } + fields { + key: "egress_global_timestamp" + value { + name: "egress_global_timestamp" + bitwidth: 48 + } + } + fields { + key: "egress_port" + value { + name: "egress_port" + bitwidth: 9 + } + } + fields { + key: "egress_rid" + value { + name: "egress_rid" + bitwidth: 16 + } + } + fields { + key: "egress_spec" + value { + name: "egress_spec" + bitwidth: 9 + } + } + fields { + key: "enq_qdepth" + value { + name: "enq_qdepth" + bitwidth: 19 + } + } + fields { + key: "enq_timestamp" + value { + name: "enq_timestamp" + bitwidth: 32 + } + } + fields { + key: "ingress_global_timestamp" + value { + name: "ingress_global_timestamp" + bitwidth: 48 + } + } + fields { + key: "ingress_port" + value { + name: "ingress_port" + bitwidth: 9 + } + } + fields { + key: "instance_type" + value { + name: "instance_type" + bitwidth: 32 + } + } + fields { + key: "mcast_grp" + value { + name: "mcast_grp" + bitwidth: 16 + } + } + fields { + key: "packet_length" + value { + name: "packet_length" + bitwidth: 32 + } + } + fields { + key: "parser_error" + value { + name: "parser_error" + bitwidth: 32 + } + } + fields { + key: "priority" + value { + name: "priority" + bitwidth: 3 + } + } + } +} +pipeline { + key: "egress" + value { + name: "egress" + initial_control: "__END_OF_PIPELINE__" + } +} +pipeline { + key: "ingress" + value { + name: "ingress" + initial_control: "__END_OF_PIPELINE__" + } +} +parsers { + key: "parser" + value { + name: "parser" + initial_state: "start" + parse_states { + key: "parse_ipv4" + value { + name: "parse_ipv4" + parser_ops { + extract { + header { + header_name: "ipv4" + } + } + } + transitions { + default_transition { + next_state: "__END_OF_PARSER__" + } + } + } + } + parse_states { + key: "start" + value { + name: "start" + parser_ops { + extract { + header { + header_name: "ethernet" + } + } + } + transition_key_fields { + field { + header_name: "ethernet" + field_name: "ether_type" + } + } + transitions { + hex_string_transition { + value: "0x0000" + mask: "0xfe00" + next_state: "__END_OF_PARSER__" + } + } + transitions { + hex_string_transition { + value: "0x0800" + next_state: "parse_ipv4" + } + } + transitions { + default_transition { + next_state: "__END_OF_PARSER__" + } + } + } + } + } +} + From e2a4b6d422e2d46b8045208858c78489c2b7beaf Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 21 Nov 2024 18:28:52 +0530 Subject: [PATCH 5/6] [P4_Symbolic] Extend IR proto and translation to support parsers. --- p4_symbolic/ir/BUILD.bazel | 9 + .../ir/expected/hex_string_transition.txt | 62 ----- p4_symbolic/ir/ir.h | 6 +- p4_symbolic/testdata/common/headers.p4 | 215 ++++++++++++++++++ .../testdata/parser/hex_string_transition.p4 | 71 ++++++ 5 files changed, 300 insertions(+), 63 deletions(-) create mode 100644 p4_symbolic/testdata/common/headers.p4 create mode 100644 p4_symbolic/testdata/parser/hex_string_transition.p4 diff --git a/p4_symbolic/ir/BUILD.bazel b/p4_symbolic/ir/BUILD.bazel index 0bafd3ff..3e29443c 100644 --- a/p4_symbolic/ir/BUILD.bazel +++ b/p4_symbolic/ir/BUILD.bazel @@ -90,6 +90,7 @@ cc_library( "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", + "@com_google_absl//absl/strings:str_format", ], ) @@ -202,3 +203,11 @@ ir_parsing_test( golden_file = "expected/table_hit_2.txt", p4_program = "//p4_symbolic/testdata:conditional/table_hit_2.p4", ) + +ir_parsing_test( + name = "hex_string_transition_test", + golden_file = "expected/hex_string_transition.txt", + p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_program = "//p4_symbolic/testdata:parser/hex_string_transition.p4", +) + diff --git a/p4_symbolic/ir/expected/hex_string_transition.txt b/p4_symbolic/ir/expected/hex_string_transition.txt index ea9b2f3d..fb63ca77 100644 --- a/p4_symbolic/ir/expected/hex_string_transition.txt +++ b/p4_symbolic/ir/expected/hex_string_transition.txt @@ -284,66 +284,4 @@ pipeline { initial_control: "__END_OF_PIPELINE__" } } -parsers { - key: "parser" - value { - name: "parser" - initial_state: "start" - parse_states { - key: "parse_ipv4" - value { - name: "parse_ipv4" - parser_ops { - extract { - header { - header_name: "ipv4" - } - } - } - transitions { - default_transition { - next_state: "__END_OF_PARSER__" - } - } - } - } - parse_states { - key: "start" - value { - name: "start" - parser_ops { - extract { - header { - header_name: "ethernet" - } - } - } - transition_key_fields { - field { - header_name: "ethernet" - field_name: "ether_type" - } - } - transitions { - hex_string_transition { - value: "0x0000" - mask: "0xfe00" - next_state: "__END_OF_PARSER__" - } - } - transitions { - hex_string_transition { - value: "0x0800" - next_state: "parse_ipv4" - } - } - transitions { - default_transition { - next_state: "__END_OF_PARSER__" - } - } - } - } - } -} diff --git a/p4_symbolic/ir/ir.h b/p4_symbolic/ir/ir.h index bfab9c4b..b57ea6fe 100644 --- a/p4_symbolic/ir/ir.h +++ b/p4_symbolic/ir/ir.h @@ -20,7 +20,6 @@ #define P4_SYMBOLIC_IR_IR_H_ #include "absl/status/statusor.h" -#include "absl/strings/string_view.h" #include "p4_symbolic/bmv2/bmv2.pb.h" #include "p4_symbolic/ir/ir.pb.h" @@ -31,6 +30,11 @@ namespace ir { // in P4-Symbolic's IR. inline std::string EndOfPipeline() { return "__END_OF_PIPELINE__"; } +// A special parse state name indicating the end of execution in a parser in +// P4-Symbolic's IR. We decided to keep the parser CFG separated from the +// pipeline CFG for the symbolic evaluation. +inline std::string EndOfParser() { return "__END_OF_PARSER__"; } + // For any table application, BMv2 JSON (and P4-Symbolic IR) use a map from // actions that may be executed as a result of table application to the next // table/control that must be evaluated if the corresponding action is executed. diff --git a/p4_symbolic/testdata/common/headers.p4 b/p4_symbolic/testdata/common/headers.p4 new file mode 100644 index 00000000..8804687f --- /dev/null +++ b/p4_symbolic/testdata/common/headers.p4 @@ -0,0 +1,215 @@ +#ifndef P4_SYMBOLIC_TESTDATA_COMMON_HEADERS_P4_ +#define P4_SYMBOLIC_TESTDATA_COMMON_HEADERS_P4_ + +#define ETHERTYPE_IPV4 0x0800 +#define ETHERTYPE_IPV6 0x86dd +#define ETHERTYPE_ARP 0x0806 +#define ETHERTYPE_LLDP 0x88cc +#define ETHERTYPE_8021Q 0x8100 + +#define IP_PROTOCOL_TCP 0x06 +#define IP_PROTOCOL_UDP 0x11 +#define IP_PROTOCOL_ICMP 0x01 +#define IP_PROTOCOL_ICMPV6 0x3a +#define IP_PROTOCOLS_GRE 0x2f + +#define GRE_PROTOCOL_ERSPAN 0x88be + +#define ERSPAN_VERSION_TYPE_II 1 + +typedef bit<48> ethernet_addr_t; +typedef bit<32> ipv4_addr_t; +typedef bit<128> ipv6_addr_t; +typedef bit<12> vlan_id_t; +typedef bit<16> ether_type_t; + +// "The VID value 0xFFF is reserved for implementation use; it must not be +// configured or transmitted." (https://en.wikipedia.org/wiki/IEEE_802.1Q). +const vlan_id_t INTERNAL_VLAN_ID = 0xfff; +// "The reserved value 0x000 indicates that the frame does not carry a VLAN ID; +// in this case, the 802.1Q tag specifies only a priority" +// (https://en.wikipedia.org/wiki/IEEE_802.1Q). +const vlan_id_t NO_VLAN_ID = 0x000; + +// --- Intrinsic ports --------------------------------------------------------- + +// Port used for PacketIO. Packets sent to this port go to the CPU. +// Packets received on this port come from the CPU. +#define SAI_P4_CPU_PORT 510 + +// The port used by `mark_to_drop` from v1model.p4. For details, see the +// documentation of `mark_to_drop`. +#define SAI_P4_DROP_PORT 511 + +// -- Translated Types --------------------------------------------------------- + +// BMv2 does not support @p4runtime_translation. + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +@p4runtime_translation_mappings({ + // The "default VRF", 0, corresponds to the empty string, "", in P4Runtime. + {"", 0}, +}) +#endif +type bit<16> vrf_id_t; + +const vrf_id_t kDefaultVrf = 0; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit<16> port_id_t; + +// -- Protocol headers --------------------------------------------------------- + +#define ETHERNET_HEADER_BYTES 14 + +header ethernet_t { + ethernet_addr_t dst_addr; + ethernet_addr_t src_addr; + ether_type_t ether_type; +} + +header vlan_t { + // Note: Tag Protocol Identifier (TPID) will be parsed as the ether_type of + // the ethernet header. It is technically a part of the vlan header but is + // modeled like this to facilitate parsing and deparsing. + bit<3> priority_code_point; // PCP + bit<1> drop_eligible_indicator; // DEI + vlan_id_t vlan_id; // VID + // Note: The next ether_type will be parsed as part of the vlan + // header. It is technically a part of the ethernet header but is modeled like + // this to facilitate parsing and deparsing. + ether_type_t ether_type; +} + +#define IPV4_HEADER_BYTES 20 + +header ipv4_t { + bit<4> version; + bit<4> ihl; + bit<6> dscp; // The 6 most significant bits of the diff_serv field. + bit<2> ecn; // The 2 least significant bits of the diff_serv field. + bit<16> total_len; + bit<16> identification; + bit<1> reserved; + bit<1> do_not_fragment; + bit<1> more_fragments; + bit<13> frag_offset; + bit<8> ttl; + bit<8> protocol; + bit<16> header_checksum; + ipv4_addr_t src_addr; + ipv4_addr_t dst_addr; +} + +#define IPV6_HEADER_BYTES 40 + +header ipv6_t { + bit<4> version; + bit<6> dscp; // The 6 most significant bits of the traffic_class field. + bit<2> ecn; // The 2 least significant bits of the traffic_class field. + bit<20> flow_label; + bit<16> payload_length; + bit<8> next_header; + bit<8> hop_limit; + ipv6_addr_t src_addr; + ipv6_addr_t dst_addr; +} + +header udp_t { + bit<16> src_port; + bit<16> dst_port; + bit<16> hdr_length; + bit<16> checksum; +} + +header tcp_t { + bit<16> src_port; + bit<16> dst_port; + bit<32> seq_no; + bit<32> ack_no; + bit<4> data_offset; + bit<4> res; + bit<8> flags; + bit<16> window; + bit<16> checksum; + bit<16> urgent_ptr; +} + +header icmp_t { + bit<8> type; + bit<8> code; + bit<16> checksum; +} + +header arp_t { + bit<16> hw_type; + bit<16> proto_type; + bit<8> hw_addr_len; + bit<8> proto_addr_len; + bit<16> opcode; + bit<48> sender_hw_addr; + bit<32> sender_proto_addr; + bit<48> target_hw_addr; + bit<32> target_proto_addr; +} + +#define GRE_HEADER_BYTES 4 + +header gre_t { + bit<1> checksum_present; + bit<1> routing_present; + bit<1> key_present; + bit<1> sequence_present; + bit<1> strict_source_route; + bit<3> recursion_control; + bit<1> acknowledgement_present; + bit<4> flags; + bit<3> version; + bit<16> protocol; +} + +// -- Packet IO headers -------------------------------------------------------- + +@controller_header("packet_in") +header packet_in_header_t { + // The port the packet ingressed on. + port_id_t ingress_port; + // The initial intended egress port decided for the packet by the pipeline. + port_id_t target_egress_port; +} + +@controller_header("packet_out") +header packet_out_header_t { + // The port this packet should egress out of when `submit_to_ingress == 0`. + // Meaningless when `submit_to_ingress == 1`. + port_id_t egress_port; + // Indicates if the packet should go through the ingress pipeline like a + // dataplane packet, or be sent straight out of the given `egress_port`. + bit<1> submit_to_ingress; + // Padding field to align the header to 8-bit multiple, as required by BMv2. + // Carries no information. + @padding + bit<7> unused_pad; +} + +// -- Preserved Field Lists ---------------------------------------------------- + +// The field list numbers used in @field_list annotations to identify the fields +// that need to be preserved during clone/recirculation/etc. operations. +enum bit<8> PreservedFieldList { + CLONE_I2E_MIRRORING = 8w1, + // We implement packet-in in SAI P4 by using the replication engine to make a + // clone of the punted packet and then send the clone to the controller. But + // the standard metadata of the packet clone will be empty, that's a problem + // because the controller needs to know the ingress port and expected egress + // port of the punted packet. To solve this problem, we save the targeted + // egress port and ingress port of the punted packet in local metadata and use + // clone_preserving_field_list to preserve these local metadata fields when + // cloning the punted packet. + CLONE_I2E_PACKET_IN = 8w2 +}; + +#endif // P4_SYMBOLIC_TESTDATA_COMMON_HEADERS_P4_ diff --git a/p4_symbolic/testdata/parser/hex_string_transition.p4 b/p4_symbolic/testdata/parser/hex_string_transition.p4 new file mode 100644 index 00000000..5c28ea09 --- /dev/null +++ b/p4_symbolic/testdata/parser/hex_string_transition.p4 @@ -0,0 +1,71 @@ +#include +#include "../common/headers.p4" + +struct local_metadata_t { + /* empty */ +} + +struct headers_t { + ethernet_t ethernet; + ipv4_t ipv4; +} + +parser packet_parser(packet_in packet, out headers_t headers, + inout local_metadata_t local_metadata, + inout standard_metadata_t standard_metadata) { + state start { + transition parse_ethernet; + } + + state parse_ethernet { + packet.extract(headers.ethernet); + transition select(headers.ethernet.ether_type) { + 0 &&& 0xfe00: accept; + ETHERTYPE_IPV4: parse_ipv4; + default: accept; + } + } + + state parse_ipv4 { + packet.extract(headers.ipv4); + transition accept; + } +} + +control empty_verify_checksum(inout headers_t headers, + inout local_metadata_t local_metadata) { + apply {} +} // control empty_verify_checksum + +control ingress(inout headers_t headers, + inout local_metadata_t local_metadata, + inout standard_metadata_t standard_metadata) { + apply {} +} // control ingress + +control egress(inout headers_t headers, + inout local_metadata_t local_metadata, + inout standard_metadata_t standard_metadata) { + apply {} +} // control egress + +control empty_compute_checksum(inout headers_t headers, + inout local_metadata_t local_metadata) { + apply {} +} // control empty_compute_checksum + +control packet_deparser(packet_out packet, in headers_t headers) { + apply { + packet.emit(headers.ethernet); + } +} // control packet_deparser + +V1Switch( + packet_parser(), + empty_verify_checksum(), + ingress(), + egress(), + empty_compute_checksum(), + packet_deparser() +) main; + From 25d7f4e91b50f6f872d67c04cc76e4af0028df54 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 21 Nov 2024 20:42:43 +0530 Subject: [PATCH 6/6] [P4_Symbolic] Adding p4_symbolic/ir/expected/set_parser_operation.txt [Extend IR proto and translation to support parsers] --- .../ir/expected/set_parser_operation.txt | 449 ++++++++++++++++++ 1 file changed, 449 insertions(+) create mode 100644 p4_symbolic/ir/expected/set_parser_operation.txt diff --git a/p4_symbolic/ir/expected/set_parser_operation.txt b/p4_symbolic/ir/expected/set_parser_operation.txt new file mode 100644 index 00000000..834b535e --- /dev/null +++ b/p4_symbolic/ir/expected/set_parser_operation.txt @@ -0,0 +1,449 @@ +headers { + key: "ethernet" + value { + name: "ethernet_t" + id: 2 + fields { + key: "dst_addr" + value { + name: "dst_addr" + bitwidth: 48 + } + } + fields { + key: "ether_type" + value { + name: "ether_type" + bitwidth: 16 + } + } + fields { + key: "src_addr" + value { + name: "src_addr" + bitwidth: 48 + } + } + } +} +headers { + key: "ipv4" + value { + name: "ipv4_t" + id: 3 + fields { + key: "do_not_fragment" + value { + name: "do_not_fragment" + bitwidth: 1 + } + } + fields { + key: "dscp" + value { + name: "dscp" + bitwidth: 6 + } + } + fields { + key: "dst_addr" + value { + name: "dst_addr" + bitwidth: 32 + } + } + fields { + key: "ecn" + value { + name: "ecn" + bitwidth: 2 + } + } + fields { + key: "frag_offset" + value { + name: "frag_offset" + bitwidth: 13 + } + } + fields { + key: "header_checksum" + value { + name: "header_checksum" + bitwidth: 16 + } + } + fields { + key: "identification" + value { + name: "identification" + bitwidth: 16 + } + } + fields { + key: "ihl" + value { + name: "ihl" + bitwidth: 4 + } + } + fields { + key: "more_fragments" + value { + name: "more_fragments" + bitwidth: 1 + } + } + fields { + key: "protocol" + value { + name: "protocol" + bitwidth: 8 + } + } + fields { + key: "reserved" + value { + name: "reserved" + bitwidth: 1 + } + } + fields { + key: "src_addr" + value { + name: "src_addr" + bitwidth: 32 + } + } + fields { + key: "total_len" + value { + name: "total_len" + bitwidth: 16 + } + } + fields { + key: "ttl" + value { + name: "ttl" + bitwidth: 8 + } + } + fields { + key: "version" + value { + name: "version" + bitwidth: 4 + } + } + } +} +headers { + key: "scalars" + value { + name: "scalars_0" + fields { + key: "local_metadata_t.dst_mac" + value { + name: "local_metadata_t.dst_mac" + bitwidth: 48 + } + } + fields { + key: "local_metadata_t.ether_type" + value { + name: "local_metadata_t.ether_type" + bitwidth: 16 + } + } + fields { + key: "local_metadata_t.signed_integer1" + value { + name: "local_metadata_t.signed_integer1" + bitwidth: 16 + signed: true + } + } + fields { + key: "local_metadata_t.signed_integer2" + value { + name: "local_metadata_t.signed_integer2" + bitwidth: 16 + signed: true + } + } + fields { + key: "local_metadata_t.src_mac" + value { + name: "local_metadata_t.src_mac" + bitwidth: 48 + } + } + } +} +headers { + key: "standard_metadata" + value { + name: "standard_metadata" + id: 1 + fields { + key: "_padding" + value { + name: "_padding" + bitwidth: 3 + } + } + fields { + key: "checksum_error" + value { + name: "checksum_error" + bitwidth: 1 + } + } + fields { + key: "deq_qdepth" + value { + name: "deq_qdepth" + bitwidth: 19 + } + } + fields { + key: "deq_timedelta" + value { + name: "deq_timedelta" + bitwidth: 32 + } + } + fields { + key: "egress_global_timestamp" + value { + name: "egress_global_timestamp" + bitwidth: 48 + } + } + fields { + key: "egress_port" + value { + name: "egress_port" + bitwidth: 9 + } + } + fields { + key: "egress_rid" + value { + name: "egress_rid" + bitwidth: 16 + } + } + fields { + key: "egress_spec" + value { + name: "egress_spec" + bitwidth: 9 + } + } + fields { + key: "enq_qdepth" + value { + name: "enq_qdepth" + bitwidth: 19 + } + } + fields { + key: "enq_timestamp" + value { + name: "enq_timestamp" + bitwidth: 32 + } + } + fields { + key: "ingress_global_timestamp" + value { + name: "ingress_global_timestamp" + bitwidth: 48 + } + } + fields { + key: "ingress_port" + value { + name: "ingress_port" + bitwidth: 9 + } + } + fields { + key: "instance_type" + value { + name: "instance_type" + bitwidth: 32 + } + } + fields { + key: "mcast_grp" + value { + name: "mcast_grp" + bitwidth: 16 + } + } + fields { + key: "packet_length" + value { + name: "packet_length" + bitwidth: 32 + } + } + fields { + key: "parser_error" + value { + name: "parser_error" + bitwidth: 32 + } + } + fields { + key: "priority" + value { + name: "priority" + bitwidth: 3 + } + } + } +} +pipeline { + key: "egress" + value { + name: "egress" + initial_control: "__END_OF_PIPELINE__" + } +} +pipeline { + key: "ingress" + value { + name: "ingress" + initial_control: "__END_OF_PIPELINE__" + } +} +parsers { + key: "parser" + value { + name: "parser" + initial_state: "start" + parse_states { + key: "parse_ipv4" + value { + name: "parse_ipv4" + parser_ops { + extract { + header { + header_name: "ipv4" + } + } + } + transitions { + default_transition { + next_state: "__END_OF_PARSER__" + } + } + } + } + parse_states { + key: "start" + value { + name: "start" + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t.ether_type" + } + lookahead_rvalue { + bitwidth: 16 + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t.signed_integer1" + } + hexstr_rvalue { + value: "0x0001" + negative: true + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t.signed_integer2" + } + hexstr_rvalue { + value: "0x0002" + } + } + } + parser_ops { + extract { + header { + header_name: "ethernet" + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t.dst_mac" + } + field_rvalue { + header_name: "ethernet" + field_name: "dst_addr" + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t.src_mac" + } + expression_rvalue { + binary_expression { + operation: BIT_AND + left { + field_value { + header_name: "ethernet" + field_name: "src_addr" + } + } + right { + hexstr_value { + value: "0xffffffffff00" + } + } + } + } + } + } + transition_key_fields { + field { + header_name: "scalars" + field_name: "local_metadata_t.ether_type" + } + } + transitions { + hex_string_transition { + value: "0x0800" + next_state: "parse_ipv4" + } + } + transitions { + default_transition { + next_state: "__END_OF_PARSER__" + } + } + } + } + } +} +