From e83312e290673ae8c81205aca8d25fa9b0164bd4 Mon Sep 17 00:00:00 2001 From: kishanps Date: Fri, 2 Jun 2023 15:24:08 -0700 Subject: [PATCH 1/4] Extend BMv2 proto with error codes. PiperOrigin-RevId: 537422979 --- p4_symbolic/bmv2/bmv2.proto | 4 +- p4_symbolic/bmv2/expected/basic.pb.txt | 56 ++++++++++++++++++++ p4_symbolic/bmv2/expected/hardcoded.pb.txt | 56 ++++++++++++++++++++ p4_symbolic/bmv2/expected/reflector.pb.txt | 56 ++++++++++++++++++++ p4_symbolic/bmv2/expected/set_invalid.pb.txt | 56 ++++++++++++++++++++ p4_symbolic/bmv2/expected/table.pb.txt | 56 ++++++++++++++++++++ p4_symbolic/bmv2/expected/table_hit_1.pb.txt | 56 ++++++++++++++++++++ p4_symbolic/bmv2/expected/table_hit_2.pb.txt | 56 ++++++++++++++++++++ 8 files changed, 395 insertions(+), 1 deletion(-) diff --git a/p4_symbolic/bmv2/bmv2.proto b/p4_symbolic/bmv2/bmv2.proto index 1062fc946..1dbe270fa 100644 --- a/p4_symbolic/bmv2/bmv2.proto +++ b/p4_symbolic/bmv2/bmv2.proto @@ -78,7 +78,7 @@ message P4Program { repeated Deparser deparsers = 4; // All actions defined in the program, including their names // paramters, and bodies. - // Eventhough actions are typically attached to tables, + // Even though actions are typically attached to tables, // they are defined seperatly in the JSON format, // and the table definitions refer to them by their action id. repeated Action actions = 5; @@ -86,6 +86,8 @@ message P4Program { // including all their tables, and the mapping of tables // to actions via match keys. repeated Pipeline pipelines = 6; + // All errors defined in the program. + repeated google.protobuf.ListValue errors = 7; } // A P4 header type definition. diff --git a/p4_symbolic/bmv2/expected/basic.pb.txt b/p4_symbolic/bmv2/expected/basic.pb.txt index 78bfd67d0..f21b6e569 100644 --- a/p4_symbolic/bmv2/expected/basic.pb.txt +++ b/p4_symbolic/bmv2/expected/basic.pb.txt @@ -1109,3 +1109,59 @@ pipelines { source_fragment: "MyEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} diff --git a/p4_symbolic/bmv2/expected/hardcoded.pb.txt b/p4_symbolic/bmv2/expected/hardcoded.pb.txt index 2f005d75a..ae3760a32 100644 --- a/p4_symbolic/bmv2/expected/hardcoded.pb.txt +++ b/p4_symbolic/bmv2/expected/hardcoded.pb.txt @@ -522,3 +522,59 @@ pipelines { source_fragment: "UselessEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} diff --git a/p4_symbolic/bmv2/expected/reflector.pb.txt b/p4_symbolic/bmv2/expected/reflector.pb.txt index f85073d50..228170438 100644 --- a/p4_symbolic/bmv2/expected/reflector.pb.txt +++ b/p4_symbolic/bmv2/expected/reflector.pb.txt @@ -350,3 +350,59 @@ pipelines { source_fragment: "UselessEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} diff --git a/p4_symbolic/bmv2/expected/set_invalid.pb.txt b/p4_symbolic/bmv2/expected/set_invalid.pb.txt index 36110f339..9eb33bf57 100644 --- a/p4_symbolic/bmv2/expected/set_invalid.pb.txt +++ b/p4_symbolic/bmv2/expected/set_invalid.pb.txt @@ -644,3 +644,59 @@ pipelines { source_fragment: "UselessEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} diff --git a/p4_symbolic/bmv2/expected/table.pb.txt b/p4_symbolic/bmv2/expected/table.pb.txt index 65ddab30f..971d0f548 100644 --- a/p4_symbolic/bmv2/expected/table.pb.txt +++ b/p4_symbolic/bmv2/expected/table.pb.txt @@ -362,3 +362,59 @@ pipelines { source_fragment: "UselessEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} diff --git a/p4_symbolic/bmv2/expected/table_hit_1.pb.txt b/p4_symbolic/bmv2/expected/table_hit_1.pb.txt index 13e64a2b4..b5454af2c 100644 --- a/p4_symbolic/bmv2/expected/table_hit_1.pb.txt +++ b/p4_symbolic/bmv2/expected/table_hit_1.pb.txt @@ -860,3 +860,59 @@ pipelines { source_fragment: "MyEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} diff --git a/p4_symbolic/bmv2/expected/table_hit_2.pb.txt b/p4_symbolic/bmv2/expected/table_hit_2.pb.txt index e0b7a17ba..75e37a1ab 100644 --- a/p4_symbolic/bmv2/expected/table_hit_2.pb.txt +++ b/p4_symbolic/bmv2/expected/table_hit_2.pb.txt @@ -922,3 +922,59 @@ pipelines { source_fragment: "MyEgress" } } +errors { + values { + string_value: "NoError" + } + values { + number_value: 0 + } +} +errors { + values { + string_value: "PacketTooShort" + } + values { + number_value: 1 + } +} +errors { + values { + string_value: "NoMatch" + } + values { + number_value: 2 + } +} +errors { + values { + string_value: "StackOutOfBounds" + } + values { + number_value: 3 + } +} +errors { + values { + string_value: "HeaderTooShort" + } + values { + number_value: 4 + } +} +errors { + values { + string_value: "ParserTimeout" + } + values { + number_value: 5 + } +} +errors { + values { + string_value: "ParserInvalidArgument" + } + values { + number_value: 6 + } +} From e281ac413ad21cd8787335184bd196c3af7d3402 Mon Sep 17 00:00:00 2001 From: VSuryaprasad-HCL Date: Mon, 25 Nov 2024 20:09:29 +0530 Subject: [PATCH 2/4] [P4_Symbolic] Adding p4_symbolic/symbolic/expected/conditional_nonlattice. [Remove disjointness check on set of tables that get evaluate in each branch of a conditional.] --- .../expected/conditional_nonlattice.smt2 | 290 ++++++++++++++++++ .../expected/conditional_nonlattice.txt | 18 ++ 2 files changed, 308 insertions(+) create mode 100644 p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 create mode 100644 p4_symbolic/symbolic/expected/conditional_nonlattice.txt diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 new file mode 100644 index 000000000..cfba9e48c --- /dev/null +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 @@ -0,0 +1,290 @@ +; +(set-info :status unknown) +(declare-fun standard_metadata.ingress_port () (_ BitVec 9)) +(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) +(declare-fun ethernet.dst_addr () (_ BitVec 48)) +(assert + (let (($x170 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x165 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x160 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x155 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x150 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x145 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x140 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x135 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x130 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x125 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x120 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x115 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x110 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x105 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x100 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85))) + (let (($x121 (or (or (or (or (or (or (or $x86 $x90) $x95) $x100) $x105) $x110) $x115) $x120))) + (let (($x156 (or (or (or (or (or (or (or $x121 $x125) $x130) $x135) $x140) $x145) $x150) $x155))) + (or (or (or $x156 $x160) $x165) $x170)))))))))))))))))))))))) +(assert + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x40 (and $x33 (not $x37)))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not $x31)))) + (let (($x52 (and $x34 $x50))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x66 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54)))) + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x71 (ite $x63 (_ bv1 9) ?x66))) + (let (($x93 (or (or (or (or false (= ?x71 (_ bv0 9))) (= ?x71 (_ bv1 9))) (= ?x71 (_ bv2 9))) (= ?x71 (_ bv3 9))))) + (let (($x113 (or (or (or (or $x93 (= ?x71 (_ bv4 9))) (= ?x71 (_ bv5 9))) (= ?x71 (_ bv6 9))) (= ?x71 (_ bv7 9))))) + (let (($x133 (or (or (or (or $x113 (= ?x71 (_ bv8 9))) (= ?x71 (_ bv9 9))) (= ?x71 (_ bv10 9))) (= ?x71 (_ bv11 9))))) + (let (($x153 (or (or (or (or $x133 (= ?x71 (_ bv12 9))) (= ?x71 (_ bv13 9))) (= ?x71 (_ bv14 9))) (= ?x71 (_ bv15 9))))) + (let (($x173 (or (or (or (or $x153 (= ?x71 (_ bv16 9))) (= ?x71 (_ bv17 9))) (= ?x71 (_ bv18 9))) (= ?x71 (_ bv19 9))))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (or $x73 $x173))))))))))))))))))))))) +(assert + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))))) + (let (($x52 (and $x34 $x50))) + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x58 (ite $x31 (ite $x37 $x39 false) (ite $x50 $x52 false)))) + (let (($x40 (and $x33 (not $x37)))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x66 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54)))) + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x71 (ite $x63 (_ bv1 9) ?x66))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (and (and (not $x73) $x58) (= (- 1) (- 1))))))))))))))))))))) +(check-sat) + +; +(set-info :status unknown) +(declare-fun standard_metadata.ingress_port () (_ BitVec 9)) +(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) +(declare-fun ethernet.dst_addr () (_ BitVec 48)) +(assert + (let (($x170 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x165 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x160 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x155 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x150 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x145 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x140 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x135 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x130 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x125 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x120 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x115 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x110 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x105 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x100 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85))) + (let (($x121 (or (or (or (or (or (or (or $x86 $x90) $x95) $x100) $x105) $x110) $x115) $x120))) + (let (($x156 (or (or (or (or (or (or (or $x121 $x125) $x130) $x135) $x140) $x145) $x150) $x155))) + (or (or (or $x156 $x160) $x165) $x170)))))))))))))))))))))))) +(assert + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x40 (and $x33 (not $x37)))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not $x31)))) + (let (($x52 (and $x34 $x50))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x66 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54)))) + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x71 (ite $x63 (_ bv1 9) ?x66))) + (let (($x93 (or (or (or (or false (= ?x71 (_ bv0 9))) (= ?x71 (_ bv1 9))) (= ?x71 (_ bv2 9))) (= ?x71 (_ bv3 9))))) + (let (($x113 (or (or (or (or $x93 (= ?x71 (_ bv4 9))) (= ?x71 (_ bv5 9))) (= ?x71 (_ bv6 9))) (= ?x71 (_ bv7 9))))) + (let (($x133 (or (or (or (or $x113 (= ?x71 (_ bv8 9))) (= ?x71 (_ bv9 9))) (= ?x71 (_ bv10 9))) (= ?x71 (_ bv11 9))))) + (let (($x153 (or (or (or (or $x133 (= ?x71 (_ bv12 9))) (= ?x71 (_ bv13 9))) (= ?x71 (_ bv14 9))) (= ?x71 (_ bv15 9))))) + (let (($x173 (or (or (or (or $x153 (= ?x71 (_ bv16 9))) (= ?x71 (_ bv17 9))) (= ?x71 (_ bv18 9))) (= ?x71 (_ bv19 9))))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (or $x73 $x173))))))))))))))))))))))) +(assert + (let (($x34 (and true (not (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))))) + (let (($x53 (and $x34 (not (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x40 (and $x33 (not (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))))) + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x59 (ite $x31 (ite $x37 false $x40) (ite $x50 false $x53)))) + (let ((?x44 (ite $x40 (_ bv511 9) (ite (and $x33 $x37) (_ bv511 9) standard_metadata.egress_spec)))) + (let (($x52 (and $x34 $x50))) + (let ((?x66 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x53 (_ bv511 9) (ite $x52 (_ bv511 9) ?x44))))) + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x71 (ite $x63 (_ bv1 9) ?x66))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (and (and (not $x73) $x59) (= (- 1) (- 1)))))))))))))))))))) +(check-sat) + +; +(set-info :status unknown) +(declare-fun standard_metadata.ingress_port () (_ BitVec 9)) +(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) +(declare-fun ethernet.dst_addr () (_ BitVec 48)) +(assert + (let (($x170 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x165 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x160 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x155 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x150 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x145 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x140 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x135 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x130 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x125 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x120 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x115 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x110 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x105 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x100 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85))) + (let (($x121 (or (or (or (or (or (or (or $x86 $x90) $x95) $x100) $x105) $x110) $x115) $x120))) + (let (($x156 (or (or (or (or (or (or (or $x121 $x125) $x130) $x135) $x140) $x145) $x150) $x155))) + (or (or (or $x156 $x160) $x165) $x170)))))))))))))))))))))))) +(assert + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x40 (and $x33 (not $x37)))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not $x31)))) + (let (($x52 (and $x34 $x50))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x66 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54)))) + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x71 (ite $x63 (_ bv1 9) ?x66))) + (let (($x93 (or (or (or (or false (= ?x71 (_ bv0 9))) (= ?x71 (_ bv1 9))) (= ?x71 (_ bv2 9))) (= ?x71 (_ bv3 9))))) + (let (($x113 (or (or (or (or $x93 (= ?x71 (_ bv4 9))) (= ?x71 (_ bv5 9))) (= ?x71 (_ bv6 9))) (= ?x71 (_ bv7 9))))) + (let (($x133 (or (or (or (or $x113 (= ?x71 (_ bv8 9))) (= ?x71 (_ bv9 9))) (= ?x71 (_ bv10 9))) (= ?x71 (_ bv11 9))))) + (let (($x153 (or (or (or (or $x133 (= ?x71 (_ bv12 9))) (= ?x71 (_ bv13 9))) (= ?x71 (_ bv14 9))) (= ?x71 (_ bv15 9))))) + (let (($x173 (or (or (or (or $x153 (= ?x71 (_ bv16 9))) (= ?x71 (_ bv17 9))) (= ?x71 (_ bv18 9))) (= ?x71 (_ bv19 9))))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (or $x73 $x173))))))))))))))))))))))) +(assert + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x68 (ite $x63 0 (- 1)))) + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x40 (and $x33 (not $x37)))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not $x31)))) + (let (($x52 (and $x34 $x50))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x71 (ite $x63 (_ bv1 9) (ite (and true (not $x62)) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54))))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (and (and (not $x73) true) (= ?x68 (- 1)))))))))))))))))))) +(check-sat) + +; +(set-info :status unknown) +(declare-fun standard_metadata.ingress_port () (_ BitVec 9)) +(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) +(declare-fun ethernet.dst_addr () (_ BitVec 48)) +(assert + (let (($x170 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x165 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x160 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x155 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x150 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x145 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x140 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x135 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x130 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x125 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x120 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x115 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x110 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x105 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x100 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85))) + (let (($x121 (or (or (or (or (or (or (or $x86 $x90) $x95) $x100) $x105) $x110) $x115) $x120))) + (let (($x156 (or (or (or (or (or (or (or $x121 $x125) $x130) $x135) $x140) $x145) $x150) $x155))) + (or (or (or $x156 $x160) $x165) $x170)))))))))))))))))))))))) +(assert + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x40 (and $x33 (not $x37)))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not $x31)))) + (let (($x52 (and $x34 $x50))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x66 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54)))) + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x71 (ite $x63 (_ bv1 9) ?x66))) + (let (($x93 (or (or (or (or false (= ?x71 (_ bv0 9))) (= ?x71 (_ bv1 9))) (= ?x71 (_ bv2 9))) (= ?x71 (_ bv3 9))))) + (let (($x113 (or (or (or (or $x93 (= ?x71 (_ bv4 9))) (= ?x71 (_ bv5 9))) (= ?x71 (_ bv6 9))) (= ?x71 (_ bv7 9))))) + (let (($x133 (or (or (or (or $x113 (= ?x71 (_ bv8 9))) (= ?x71 (_ bv9 9))) (= ?x71 (_ bv10 9))) (= ?x71 (_ bv11 9))))) + (let (($x153 (or (or (or (or $x133 (= ?x71 (_ bv12 9))) (= ?x71 (_ bv13 9))) (= ?x71 (_ bv14 9))) (= ?x71 (_ bv15 9))))) + (let (($x173 (or (or (or (or $x153 (= ?x71 (_ bv16 9))) (= ?x71 (_ bv17 9))) (= ?x71 (_ bv18 9))) (= ?x71 (_ bv19 9))))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (or $x73 $x173))))))))))))))))))))))) +(assert + (let (($x61 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x62 (and true $x61))) + (let (($x63 (and true $x62))) + (let ((?x68 (ite $x63 0 (- 1)))) + (let (($x37 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x31 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x33 (and true $x31))) + (let (($x39 (and $x33 $x37))) + (let (($x40 (and $x33 (not $x37)))) + (let (($x50 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x34 (and true (not $x31)))) + (let (($x52 (and $x34 $x50))) + (let ((?x54 (ite $x52 (_ bv511 9) (ite $x40 (_ bv511 9) (ite $x39 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x53 (and $x34 (not $x50)))) + (let ((?x71 (ite $x63 (_ bv1 9) (ite (and true (not $x62)) (_ bv511 9) (ite $x53 (_ bv511 9) ?x54))))) + (let (($x73 (= ?x71 (_ bv511 9)))) + (let (($x269 (and (not $x73) true))) + (and $x269 (= ?x68 0)))))))))))))))))))) +(check-sat) + diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.txt b/p4_symbolic/symbolic/expected/conditional_nonlattice.txt new file mode 100644 index 000000000..625c5f304 --- /dev/null +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.txt @@ -0,0 +1,18 @@ +Finding packet for table MyIngress.t_1 and row -1 + Dropped = 0 + standard_metadata.ingress_port = #b000001000 + standard_metadata.egress_spec = #b000000001 + +Finding packet for table MyIngress.t_2 and row -1 + Dropped = 0 + standard_metadata.ingress_port = #b000000000 + standard_metadata.egress_spec = #b000000001 + +Finding packet for table MyIngress.t_3 and row -1 +Cannot find solution! + +Finding packet for table MyIngress.t_3 and row 0 + Dropped = 0 + standard_metadata.ingress_port = #b000000000 + standard_metadata.egress_spec = #b000000001 + From 788fcdd5585a7e0a6998bdaa13fffc4af8dfcde2 Mon Sep 17 00:00:00 2001 From: VSuryaprasad-HCL Date: Mon, 25 Nov 2024 20:34:28 +0530 Subject: [PATCH 3/4] [P4_Symbolic] Adding p4_symbolic/testdata/conditional/conditional_nonlattice files. [Remove disjointness check on set of tables that get evaluate in each branch of a conditional.] --- .../conditional/conditional_nonlattice.p4 | 145 ++++++++++++++++++ .../conditional_nonlattice_entries.pb.txt | 28 ++++ 2 files changed, 173 insertions(+) create mode 100644 p4_symbolic/testdata/conditional/conditional_nonlattice.p4 create mode 100644 p4_symbolic/testdata/conditional/conditional_nonlattice_entries.pb.txt diff --git a/p4_symbolic/testdata/conditional/conditional_nonlattice.p4 b/p4_symbolic/testdata/conditional/conditional_nonlattice.p4 new file mode 100644 index 000000000..b4f24b829 --- /dev/null +++ b/p4_symbolic/testdata/conditional/conditional_nonlattice.p4 @@ -0,0 +1,145 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +/* -*- P4_16 -*- */ +#include +#include + +typedef bit<9> egress_spec_t; +typedef bit<48> mac_addr_t; + +header ethernet_t { + mac_addr_t dst_addr; + mac_addr_t src_addr; + bit<16> ether_type; +} + +struct metadata { + /* empty */ +} + +struct headers { + ethernet_t ethernet; +} + +parser MyParser(packet_in packet, + out headers hdr, + inout metadata meta, + inout standard_metadata_t standard_metadata) { + + state start { + transition parse_ethernet; + } + + state parse_ethernet { + packet.extract(hdr.ethernet); + transition accept; + } +} + + +control MyIngress(inout headers hdr, + inout metadata meta, + inout standard_metadata_t standard_metadata) { + action drop() { + mark_to_drop(standard_metadata); + } + + action forward(mac_addr_t dst_addr, egress_spec_t port) { + standard_metadata.egress_spec = port; + hdr.ethernet.dst_addr = dst_addr; + } + + table t_1 { + key = { + hdr.ethernet.ether_type: exact; + } + actions = { + @proto_id(1) drop; + @proto_id(2) forward; + } + size = 1024; + default_action = drop(); + } + table t_2 { + key = { + hdr.ethernet.src_addr: exact; + } + actions = { + @proto_id(1) drop; + @proto_id(2) forward; + } + size = 1024; + default_action = drop(); + } + table t_3 { + key = { + hdr.ethernet.dst_addr: exact; + } + actions = { + @proto_id(1) drop; + @proto_id(2) forward; + } + size = 1024; + default_action = drop(); + } + + apply { + if (standard_metadata.ingress_port > 10) { + if (standard_metadata.ingress_port > 15) { + t_1.apply(); + } else { + t_2.apply(); + } + } else { + if (standard_metadata.ingress_port > 5) { + t_1.apply(); + } else { + t_2.apply(); + } + } + t_3.apply(); + } +} + +control MyEgress(inout headers hdr, + inout metadata meta, + inout standard_metadata_t standard_metadata) { + apply { } +} + + + +control MyDeparser(packet_out packet, in headers hdr) { + apply { + packet.emit(hdr.ethernet); + } +} + +control MyComputeChecksum(inout headers hdr, inout metadata meta) { + apply { } +} + +control MyVerifyChecksum(inout headers hdr, inout metadata meta) { + apply { } +} + +V1Switch( +MyParser(), +MyVerifyChecksum(), +MyIngress(), +MyEgress(), +MyComputeChecksum(), +MyDeparser() +) main; diff --git a/p4_symbolic/testdata/conditional/conditional_nonlattice_entries.pb.txt b/p4_symbolic/testdata/conditional/conditional_nonlattice_entries.pb.txt new file mode 100644 index 000000000..1fda5aa37 --- /dev/null +++ b/p4_symbolic/testdata/conditional/conditional_nonlattice_entries.pb.txt @@ -0,0 +1,28 @@ +updates { + type: INSERT + entity { + table_entry { + table_id: 44506558 # hdr.ethernet.dst_addr + match { + field_id: 1 # dst_addr + exact { + value: "\x00\x00\x00\x00\x00\x01" + } + } + action { + action { + action_id: 29683729 # MyIngress.forward + params { + param_id: 1 # dst_addr + value: "\x00\x00\x00\x00\x00\x02" + } + params { + param_id: 2 # port + value: "\01" + } + } + } + } + } +} + From b6b0d623327d5131bc20444de5c6037dc353c067 Mon Sep 17 00:00:00 2001 From: kheradmandG Date: Tue, 6 Jun 2023 12:07:09 -0700 Subject: [PATCH 4/4] [P4-Symbolic] Remove disjointness check on set of tables that get evaluate in each branch of a conditional. --- p4_symbolic/symbolic/conditional.cc | 8 +- p4_symbolic/symbolic/expected/basic.smt2 | 47 +- .../symbolic/expected/conditional.smt2 | 138 +++--- .../expected/conditional_sequence.smt2 | 350 ++++++++------- p4_symbolic/symbolic/expected/hardcoded.smt2 | 26 +- .../symbolic/expected/table_hit_1.smt2 | 156 ++++--- .../symbolic/expected/table_hit_2.smt2 | 425 ++++++++++-------- p4_symbolic/symbolic/expected/vrf.smt2 | 152 ++++--- p4_symbolic/symbolic/expected/vrf.txt | 14 +- p4_symbolic/symbolic/table.cc | 14 +- p4_symbolic/symbolic/test.bzl | 2 - p4_symbolic/symbolic/util.cc | 27 +- 12 files changed, 730 insertions(+), 629 deletions(-) diff --git a/p4_symbolic/symbolic/conditional.cc b/p4_symbolic/symbolic/conditional.cc index 945c18bb1..85815e512 100644 --- a/p4_symbolic/symbolic/conditional.cc +++ b/p4_symbolic/symbolic/conditional.cc @@ -66,10 +66,10 @@ absl::StatusOr EvaluateConditional( data_plane, get_next_control_for_branch(conditional.else_branch()), state, translator, else_guard)); - // Now we have two traces that need merging. The two traces are guaranteed to - // contain different table matches (see go/optimized-symbolic-execution). - ASSIGN_OR_RETURN(SymbolicTableMatches merged_matches, - util::MergeDisjointTableMatches(if_matches, else_matches)); + // Now we have two traces that need merging. + ASSIGN_OR_RETURN( + SymbolicTableMatches merged_matches, + util::MergeMatchesOnCondition(condition, if_matches, else_matches)); if (!conditional.optimized_symbolic_execution_info() .continue_to_merge_point()) { diff --git a/p4_symbolic/symbolic/expected/basic.smt2 b/p4_symbolic/symbolic/expected/basic.smt2 index ea71f2374..670ef6d17 100644 --- a/p4_symbolic/symbolic/expected/basic.smt2 +++ b/p4_symbolic/symbolic/expected/basic.smt2 @@ -5,8 +5,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ipv4.$valid$ () Bool) (assert - (let (($x123 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))) + (let (($x125 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125))) (assert (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) @@ -34,7 +34,8 @@ (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) (let (($x60 (and $x42 $x46))) - (let ((?x112 (ite $x60 1 ?x102))) + (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1)))) + (let (($x119 (ite ipv4.$valid$ $x42 false))) (let (($x61 (not $x46))) (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) @@ -46,7 +47,7 @@ (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)))) - (and (and (not $x41) $x42) (= ?x112 (- 1))))))))))))))))))))))) + (and (and (not $x41) $x119) (= ?x120 (- 1)))))))))))))))))))))))) (check-sat) ; @@ -56,8 +57,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ipv4.$valid$ () Bool) (assert - (let (($x123 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))) + (let (($x125 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125))) (assert (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) @@ -85,7 +86,8 @@ (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) (let (($x60 (and $x42 $x46))) - (let ((?x112 (ite $x60 1 ?x102))) + (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1)))) + (let (($x119 (ite ipv4.$valid$ $x42 false))) (let (($x61 (not $x46))) (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) @@ -97,8 +99,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 (($x244 (and (not $x41) $x42))) - (and $x244 (= ?x112 0))))))))))))))))))))))) + (let (($x246 (and (not $x41) $x119))) + (and $x246 (= ?x120 0)))))))))))))))))))))))) (check-sat) ; @@ -108,8 +110,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ipv4.$valid$ () Bool) (assert - (let (($x123 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))) + (let (($x125 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125))) (assert (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) @@ -137,7 +139,8 @@ (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) (let (($x60 (and $x42 $x46))) - (let ((?x112 (ite $x60 1 ?x102))) + (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1)))) + (let (($x119 (ite ipv4.$valid$ $x42 false))) (let (($x61 (not $x46))) (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) @@ -149,7 +152,7 @@ (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)))) - (and (and (not $x41) $x42) (= ?x112 1)))))))))))))))))))))) + (and (and (not $x41) $x119) (= ?x120 1))))))))))))))))))))))) (check-sat) ; @@ -159,8 +162,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ipv4.$valid$ () Bool) (assert - (let (($x123 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))) + (let (($x125 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125))) (assert (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) @@ -188,7 +191,8 @@ (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) (let (($x60 (and $x42 $x46))) - (let ((?x112 (ite $x60 1 ?x102))) + (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1)))) + (let (($x119 (ite ipv4.$valid$ $x42 false))) (let (($x61 (not $x46))) (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) @@ -200,7 +204,7 @@ (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)))) - (and (and (not $x41) $x42) (= ?x112 2)))))))))))))))))))))) + (and (and (not $x41) $x119) (= ?x120 2))))))))))))))))))))))) (check-sat) ; @@ -210,8 +214,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ipv4.$valid$ () Bool) (assert - (let (($x123 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))) + (let (($x125 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125))) (assert (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) @@ -239,7 +243,8 @@ (let (($x45 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x46 (and true $x45))) (let (($x60 (and $x42 $x46))) - (let ((?x112 (ite $x60 1 ?x102))) + (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1)))) + (let (($x119 (ite ipv4.$valid$ $x42 false))) (let (($x61 (not $x46))) (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) @@ -251,6 +256,6 @@ (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)))) - (and (and (not $x41) $x42) (= ?x112 3)))))))))))))))))))))) + (and (and (not $x41) $x119) (= ?x120 3))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional.smt2 b/p4_symbolic/symbolic/expected/conditional.smt2 index 194deea5c..29458bd67 100644 --- a/p4_symbolic/symbolic/expected/conditional.smt2 +++ b/p4_symbolic/symbolic/expected/conditional.smt2 @@ -4,30 +4,31 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x59 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))) + (let (($x61 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))) (assert (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) (let (($x34 (and true (not $x31)))) - (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) - (let (($x52 (= ?x50 (_ bv511 9)))) - (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9)))))))))))))) + (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9)))))))))))))) (assert (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) + (let (($x39 (ite $x31 $x33 false))) (let (($x34 (and true (not $x31)))) - (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) - (let (($x52 (= ?x50 (_ bv511 9)))) - (and (and (not $x52) $x33) (= (- 1) (- 1))))))))))))) + (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (and (and (not $x54) $x39) (= (- 1) (- 1)))))))))))))) (check-sat) ; @@ -36,30 +37,31 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x59 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))) + (let (($x61 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))) (assert (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) (let (($x34 (and true (not $x31)))) - (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) - (let (($x52 (= ?x50 (_ bv511 9)))) - (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9)))))))))))))) + (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9)))))))))))))) (assert (let (($x34 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))))) (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) - (let (($x33 (and true $x31))) - (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) - (let (($x52 (= ?x50 (_ bv511 9)))) - (and (and (not $x52) $x34) (= (- 1) (- 1))))))))))))) + (let (($x40 (ite $x31 false $x34))) + (let ((?x38 (ite $x34 (_ bv511 9) (ite (and true $x31) (_ bv511 9) standard_metadata.egress_spec)))) + (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x38))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (and (and (not $x54) $x40) (= (- 1) (- 1)))))))))))))) (check-sat) ; @@ -68,31 +70,31 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x59 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))) + (let (($x61 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))) (assert (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) (let (($x34 (and true (not $x31)))) - (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) - (let (($x52 (= ?x50 (_ bv511 9)))) - (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9)))))))))))))) + (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9)))))))))))))) (assert - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x47 (ite $x42 0 (- 1)))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x49 (ite $x44 0 (- 1)))) (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) (let (($x34 (and true (not $x31)))) - (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)))) - (and (and (not $x52) true) (= ?x47 (- 1)))))))))))))) + (let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (and (and (not $x54) true) (= ?x49 (- 1)))))))))))))) (check-sat) ; @@ -101,31 +103,31 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x59 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))) + (let (($x61 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))) (assert (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) (let (($x34 (and true (not $x31)))) - (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x50 (ite $x42 (_ bv1 9) ?x45))) - (let (($x52 (= ?x50 (_ bv511 9)))) - (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9)))))))))))))) + (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9)))))))))))))) (assert - (let (($x40 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x41 (and true $x40))) - (let (($x42 (and true $x41))) - (let ((?x47 (ite $x42 0 (- 1)))) + (let (($x42 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x43 (and true $x42))) + (let (($x44 (and true $x43))) + (let ((?x49 (ite $x44 0 (- 1)))) (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x33 (and true $x31))) (let (($x34 (and true (not $x31)))) - (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 (($x95 (and (not $x52) true))) - (and $x95 (= ?x47 0)))))))))))))) + (let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))) + (let ((?x52 (ite $x44 (_ bv1 9) ?x47))) + (let (($x54 (= ?x52 (_ bv511 9)))) + (let (($x97 (and (not $x54) true))) + (and $x97 (= ?x49 0)))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 index 439220010..521c97308 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 @@ -4,17 +4,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f1 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x41 (and true (not (= h1.f1 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x41) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x38 (= h1.f1 ?x37))) + (let (($x44 (ite $x38 false (and true (not $x38))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x44) (= (- 1) (- 1))))))))) (check-sat) ; @@ -23,17 +25,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f2 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x46 (and true (not (= h1.f2 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x46) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x45 (= h1.f2 ?x37))) + (let (($x50 (ite $x45 false (and true (not $x45))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x50) (= (- 1) (- 1))))))))) (check-sat) ; @@ -42,17 +46,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x50 (and true (not (= h1.f3 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x50) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x51 (= h1.f3 ?x37))) + (let (($x56 (ite $x51 false (and true (not $x51))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x56) (= (- 1) (- 1))))))))) (check-sat) ; @@ -61,17 +67,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f4 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x54 (and true (not (= h1.f4 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x54) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x57 (= h1.f4 ?x37))) + (let (($x62 (ite $x57 false (and true (not $x57))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x62) (= (- 1) (- 1))))))))) (check-sat) ; @@ -80,17 +88,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f5 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x58 (and true (not (= h1.f5 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x58) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x63 (= h1.f5 ?x37))) + (let (($x68 (ite $x63 false (and true (not $x63))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x68) (= (- 1) (- 1))))))))) (check-sat) ; @@ -99,17 +109,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f6 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x62 (and true (not (= h1.f6 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x62) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x69 (= h1.f6 ?x37))) + (let (($x74 (ite $x69 false (and true (not $x69))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x74) (= (- 1) (- 1))))))))) (check-sat) ; @@ -118,17 +130,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f7 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x66 (and true (not (= h1.f7 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x66) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x75 (= h1.f7 ?x37))) + (let (($x80 (ite $x75 false (and true (not $x75))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x80) (= (- 1) (- 1))))))))) (check-sat) ; @@ -137,17 +151,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f8 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x70 (and true (not (= h1.f8 (concat (_ bv0 7) (_ bv0 1))))))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x70) (= (- 1) (- 1))))))) + (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) + (let (($x81 (= h1.f8 ?x37))) + (let (($x86 (ite $x81 false (and true (not $x81))))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x86) (= (- 1) (- 1))))))))) (check-sat) ; @@ -156,19 +172,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f1 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) (let (($x38 (= h1.f1 ?x37))) - (let (($x40 (and true $x38))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x40) (= (- 1) (- 1))))))))) + (let (($x43 (ite $x38 (and true $x38) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x43) (= (- 1) (- 1))))))))) (check-sat) ; @@ -177,19 +193,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f2 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x43 (= h1.f2 ?x37))) - (let (($x45 (and true $x43))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x45) (= (- 1) (- 1))))))))) + (let (($x45 (= h1.f2 ?x37))) + (let (($x49 (ite $x45 (and true $x45) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x49) (= (- 1) (- 1))))))))) (check-sat) ; @@ -198,19 +214,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x47 (= h1.f3 ?x37))) - (let (($x49 (and true $x47))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x49) (= (- 1) (- 1))))))))) + (let (($x51 (= h1.f3 ?x37))) + (let (($x55 (ite $x51 (and true $x51) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x55) (= (- 1) (- 1))))))))) (check-sat) ; @@ -219,19 +235,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f4 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x51 (= h1.f4 ?x37))) - (let (($x53 (and true $x51))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x53) (= (- 1) (- 1))))))))) + (let (($x57 (= h1.f4 ?x37))) + (let (($x61 (ite $x57 (and true $x57) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x61) (= (- 1) (- 1))))))))) (check-sat) ; @@ -240,19 +256,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f5 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x55 (= h1.f5 ?x37))) - (let (($x57 (and true $x55))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x57) (= (- 1) (- 1))))))))) + (let (($x63 (= h1.f5 ?x37))) + (let (($x67 (ite $x63 (and true $x63) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x67) (= (- 1) (- 1))))))))) (check-sat) ; @@ -261,19 +277,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f6 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x59 (= h1.f6 ?x37))) - (let (($x61 (and true $x59))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x61) (= (- 1) (- 1))))))))) + (let (($x69 (= h1.f6 ?x37))) + (let (($x73 (ite $x69 (and true $x69) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x73) (= (- 1) (- 1))))))))) (check-sat) ; @@ -282,19 +298,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f7 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x63 (= h1.f7 ?x37))) - (let (($x65 (and true $x63))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x65) (= (- 1) (- 1))))))))) + (let (($x75 (= h1.f7 ?x37))) + (let (($x79 (ite $x75 (and true $x75) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x79) (= (- 1) (- 1))))))))) (check-sat) ; @@ -303,19 +319,19 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f8 () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert (let ((?x37 (concat (_ bv0 7) (_ bv0 1)))) - (let (($x67 (= h1.f8 ?x37))) - (let (($x69 (and true $x67))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (let (($x134 (not $x76))) - (and (and $x134 $x69) (= (- 1) (- 1))))))))) + (let (($x81 (= h1.f8 ?x37))) + (let (($x85 (ite $x81 (and true $x81) false))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (let (($x150 (not $x92))) + (and (and $x150 $x85) (= (- 1) (- 1))))))))) (check-sat) ; @@ -324,16 +340,16 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.fr () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x74 (and true (and true (= h1.fr (_ bv255 8)))))) - (let ((?x78 (ite $x74 0 (- 1)))) - (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x78 (- 1)))))) + (let (($x90 (and true (and true (= h1.fr (_ bv255 8)))))) + (let ((?x94 (ite $x90 0 (- 1)))) + (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x94 (- 1)))))) (check-sat) ; @@ -342,14 +358,14 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.fr () (_ BitVec 8)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90))) + (let (($x106 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106))) (assert - (let (($x92 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x76 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92))))) + (let (($x108 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x92 (= standard_metadata.egress_spec (_ bv511 9)))) + (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108))))) (assert - (let (($x74 (and true (and true (= h1.fr (_ bv255 8)))))) - (let ((?x78 (ite $x74 0 (- 1)))) - (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x78 0))))) + (let (($x90 (and true (and true (= h1.fr (_ bv255 8)))))) + (let ((?x94 (ite $x90 0 (- 1)))) + (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x94 0))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/hardcoded.smt2 b/p4_symbolic/symbolic/expected/hardcoded.smt2 index d91998907..76c947da0 100644 --- a/p4_symbolic/symbolic/expected/hardcoded.smt2 +++ b/p4_symbolic/symbolic/expected/hardcoded.smt2 @@ -3,24 +3,25 @@ (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x45 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x45))) + (let (($x47 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x47))) (assert (let ((?x26 (concat (_ bv0 8) (_ bv0 1)))) (let (($x27 (= standard_metadata.ingress_port ?x26))) (let (($x29 (and true $x27))) (let (($x30 (and true (not $x27)))) (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x37 (= ?x35 (_ bv511 9)))) - (or $x37 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9))))))))))) + (let (($x39 (= ?x35 (_ bv511 9)))) + (or $x39 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9))))))))))) (assert (let ((?x26 (concat (_ bv0 8) (_ bv0 1)))) (let (($x27 (= standard_metadata.ingress_port ?x26))) (let (($x29 (and true $x27))) + (let (($x36 (ite $x27 $x29 false))) (let (($x30 (and true (not $x27)))) (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x37 (= ?x35 (_ bv511 9)))) - (and (and (not $x37) $x29) (= (- 1) (- 1)))))))))) + (let (($x39 (= ?x35 (_ bv511 9)))) + (and (and (not $x39) $x36) (= (- 1) (- 1))))))))))) (check-sat) ; @@ -28,23 +29,24 @@ (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x45 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x45))) + (let (($x47 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x47))) (assert (let ((?x26 (concat (_ bv0 8) (_ bv0 1)))) (let (($x27 (= standard_metadata.ingress_port ?x26))) (let (($x29 (and true $x27))) (let (($x30 (and true (not $x27)))) (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x37 (= ?x35 (_ bv511 9)))) - (or $x37 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9))))))))))) + (let (($x39 (= ?x35 (_ bv511 9)))) + (or $x39 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9))))))))))) (assert (let (($x30 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))))) (let ((?x26 (concat (_ bv0 8) (_ bv0 1)))) (let (($x27 (= standard_metadata.ingress_port ?x26))) + (let (($x37 (ite $x27 false $x30))) (let (($x29 (and true $x27))) (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x37 (= ?x35 (_ bv511 9)))) - (and (and (not $x37) $x30) (= (- 1) (- 1)))))))))) + (let (($x39 (= ?x35 (_ bv511 9)))) + (and (and (not $x39) $x37) (= (- 1) (- 1))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_1.smt2 b/p4_symbolic/symbolic/expected/table_hit_1.smt2 index 8860c77ca..12f996338 100644 --- a/p4_symbolic/symbolic/expected/table_hit_1.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_1.smt2 @@ -5,38 +5,41 @@ (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x85 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x80 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x62 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66))) - (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90)))))))))) + (let (($x92 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x87 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x82 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x77 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x68 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68))) + (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92)))))))))) (assert (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) - (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true)))) + (let ((?x38 (ite $x31 0 (- 1)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36)))) - (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) - (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (or $x49 $x93)))))))))))) + (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) + (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (or $x56 $x95)))))))))))))) (assert (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) (let ((?x38 (ite $x31 0 (- 1)))) (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec)))) - (let (($x44 (and true (and (distinct ?x38 (- 1)) true)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) ?x41))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (and (and (not $x49) true) (= ?x38 (- 1))))))))))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (and (and (not $x56) true) (= ?x38 (- 1)))))))))))))) (check-sat) ; @@ -46,39 +49,42 @@ (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x85 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x80 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x62 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66))) - (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90)))))))))) + (let (($x92 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x87 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x82 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x77 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x68 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68))) + (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92)))))))))) (assert (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) - (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true)))) + (let ((?x38 (ite $x31 0 (- 1)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36)))) - (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) - (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (or $x49 $x93)))))))))))) + (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) + (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (or $x56 $x95)))))))))))))) (assert (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) (let ((?x38 (ite $x31 0 (- 1)))) (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec)))) - (let (($x44 (and true (and (distinct ?x38 (- 1)) true)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) ?x41))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (let (($x206 (and (not $x49) true))) - (and $x206 (= ?x38 0))))))))))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (let (($x208 (and (not $x56) true))) + (and $x208 (= ?x38 0)))))))))))))) (check-sat) ; @@ -88,39 +94,43 @@ (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x85 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x80 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x62 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66))) - (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90)))))))))) + (let (($x92 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x87 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x82 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x77 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x68 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68))) + (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92)))))))))) (assert (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) - (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true)))) + (let ((?x38 (ite $x31 0 (- 1)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36)))) - (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) - (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (or $x49 $x93)))))))))))) + (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) + (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (or $x56 $x95)))))))))))))) (assert (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) (let ((?x38 (ite $x31 0 (- 1)))) - (let (($x44 (and true (and (distinct ?x38 (- 1)) true)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) - (let ((?x51 (ite $x48 0 (- 1)))) + (let ((?x50 (ite $x43 (ite $x48 0 (- 1)) (- 1)))) + (let (($x49 (ite $x43 $x44 false))) (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec)))) (let ((?x54 (ite $x48 (_ bv3 9) ?x41))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (and (and (not $x49) $x44) (= ?x51 (- 1)))))))))))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (and (and (not $x56) $x49) (= ?x50 (- 1)))))))))))))))) (check-sat) ; @@ -130,38 +140,42 @@ (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (assert - (let (($x90 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x85 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x80 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x62 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66))) - (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90)))))))))) + (let (($x92 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x87 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x82 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x77 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x68 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68))) + (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92)))))))))) (assert (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) - (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true)))) + (let ((?x38 (ite $x31 0 (- 1)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36)))) - (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) - (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (or $x49 $x93)))))))))))) + (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9))))) + (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (or $x56 $x95)))))))))))))) (assert (let (($x29 (= ethernet.ether_type (_ bv16 16)))) (let (($x30 (and true $x29))) (let (($x31 (and true $x30))) (let ((?x38 (ite $x31 0 (- 1)))) - (let (($x44 (and true (and (distinct ?x38 (- 1)) true)))) + (let (($x43 (and (distinct ?x38 (- 1)) true))) + (let (($x44 (and true $x43))) (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48)))))) - (let ((?x51 (ite $x48 0 (- 1)))) + (let ((?x50 (ite $x43 (ite $x48 0 (- 1)) (- 1)))) + (let (($x49 (ite $x43 $x44 false))) (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec)))) (let ((?x54 (ite $x48 (_ bv3 9) ?x41))) - (let (($x49 (= ?x54 (_ bv511 9)))) - (and (and (not $x49) $x44) (= ?x51 0))))))))))))) + (let (($x56 (= ?x54 (_ bv511 9)))) + (and (and (not $x56) $x49) (= ?x50 0))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_2.smt2 b/p4_symbolic/symbolic/expected/table_hit_2.smt2 index 684383afe..68790db9e 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_2.smt2 @@ -6,41 +6,43 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) - (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) - (let (($x49 (= ?x41 (- 1)))) - (let (($x50 (and true $x49))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) + (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) - (let (($x49 (= ?x41 (- 1)))) + (let (($x54 (= ?x41 (- 1)))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct ?x41 (- 1)) true)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true $x49))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) true) $x49)))))))))))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) true) $x54))))))))))))) (check-sat) ; @@ -51,38 +53,43 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct ?x41 (- 1)) true)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= ?x41 (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) true) (= ?x41 0)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) true) (= ?x41 0)))))))))))))) (check-sat) ; @@ -93,39 +100,45 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) - (let (($x45 (and true (and (distinct ?x41 (- 1)) true)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let ((?x51 (ite $x48 0 (- 1)))) + (let (($x54 (= ?x41 (- 1)))) + (let ((?x65 (ite $x54 (- 1) (ite $x44 (ite $x48 0 (- 1)) (- 1))))) + (let (($x64 (ite $x54 false (ite $x44 $x45 false)))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x50 (and true (= ?x41 (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) $x45) (= ?x51 (- 1)))))))))))))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) $x64) (= ?x65 (- 1))))))))))))))))) (check-sat) ; @@ -136,39 +149,45 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) - (let (($x45 (and true (and (distinct ?x41 (- 1)) true)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let ((?x51 (ite $x48 0 (- 1)))) + (let (($x54 (= ?x41 (- 1)))) + (let ((?x65 (ite $x54 (- 1) (ite $x44 (ite $x48 0 (- 1)) (- 1))))) + (let (($x64 (ite $x54 false (ite $x44 $x45 false)))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x50 (and true (= ?x41 (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) $x45) (= ?x51 0))))))))))))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) $x64) (= ?x65 0)))))))))))))))) (check-sat) ; @@ -179,39 +198,45 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) - (let (($x50 (and true (= ?x41 (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x59 (ite $x56 0 (- 1)))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x60 (ite $x54 (ite $x58 0 (- 1)) (- 1)))) + (let (($x59 (ite $x54 $x55 false))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct ?x41 (- 1)) true)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) $x50) (= ?x59 (- 1)))))))))))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) $x59) (= ?x60 (- 1))))))))))))))))) (check-sat) ; @@ -222,39 +247,45 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x41 (ite $x37 0 (- 1)))) - (let (($x50 (and true (= ?x41 (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x59 (ite $x56 0 (- 1)))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x60 (ite $x54 (ite $x58 0 (- 1)) (- 1)))) + (let (($x59 (ite $x54 $x55 false))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct ?x41 (- 1)) true)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) $x50) (= ?x59 0))))))))))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) $x59) (= ?x60 0)))))))))))))))) (check-sat) ; @@ -265,37 +296,43 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) true) (= (- 1) (- 1)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) true) (= (- 1) (- 1))))))))))))))) (check-sat) ; @@ -306,36 +343,42 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x94 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x89 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x84 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x70 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x66 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70))) - (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94)))))))))) + (let (($x100 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x95 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x72 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76))) + (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100)))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9))))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (or $x39 $x97)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9))))) + (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9))))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (or $x39 $x103))))))))))))))) (assert (let (($x37 (and true (and true (= h1.f1 (_ bv255 8)))))) (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true)))) + (let ((?x41 (ite $x37 0 (- 1)))) + (let (($x44 (and (distinct ?x41 (- 1)) true))) + (let (($x45 (and true $x44))) (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1))))) - (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) - (let (($x39 (= ?x61 (_ bv511 9)))) - (and (and (not $x39) true) (= (- 1) (- 1)))))))))))) + (let (($x54 (= ?x41 (- 1)))) + (let (($x55 (and true $x54))) + (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43)))) + (let (($x39 (= ?x63 (_ bv511 9)))) + (and (and (not $x39) true) (= (- 1) (- 1))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2 index 2bf13d320..c60829860 100644 --- a/p4_symbolic/symbolic/expected/vrf.smt2 +++ b/p4_symbolic/symbolic/expected/vrf.smt2 @@ -8,8 +8,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -30,7 +30,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -38,7 +39,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -53,13 +54,15 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80)))) (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90))) (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1)))))) (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90))) (let (($x109 (and $x85 $x91))) - (let ((?x157 (ite $x109 1 ?x149))) + (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1)))) + (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false))) (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108))))) (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108))) (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102))) @@ -67,7 +70,7 @@ (let (($x112 (and (and $x85 (not $x91)) $x96))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142)))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x85) (= ?x157 (- 1))))))))))))))))))))))))))))))) + (and (and (not $x52) $x69) (= ?x70 (- 1))))))))))))))))))))))))))))))))) (check-sat) ; @@ -80,8 +83,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -102,7 +105,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -110,7 +114,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -125,13 +129,15 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80)))) (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90))) (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1)))))) (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90))) (let (($x109 (and $x85 $x91))) - (let ((?x157 (ite $x109 1 ?x149))) + (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1)))) + (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false))) (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108))))) (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108))) (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102))) @@ -139,8 +145,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 (($x307 (and (not $x52) $x85))) - (and $x307 (= ?x157 0))))))))))))))))))))))))))))))) + (let (($x309 (and (not $x52) $x69))) + (and $x309 (= ?x70 0))))))))))))))))))))))))))))))))) (check-sat) ; @@ -153,8 +159,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -175,7 +181,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -183,7 +190,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -198,13 +205,15 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80)))) (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90))) (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1)))))) (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90))) (let (($x109 (and $x85 $x91))) - (let ((?x157 (ite $x109 1 ?x149))) + (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1)))) + (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false))) (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108))))) (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108))) (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102))) @@ -212,7 +221,7 @@ (let (($x112 (and (and $x85 (not $x91)) $x96))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142)))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x85) (= ?x157 1)))))))))))))))))))))))))))))) + (and (and (not $x52) $x69) (= ?x70 1)))))))))))))))))))))))))))))))) (check-sat) ; @@ -225,8 +234,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -247,7 +256,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -255,7 +265,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -270,13 +280,15 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80)))) (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90))) (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1)))))) (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90))) (let (($x109 (and $x85 $x91))) - (let ((?x157 (ite $x109 1 ?x149))) + (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1)))) + (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false))) (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108))))) (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108))) (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102))) @@ -284,7 +296,7 @@ (let (($x112 (and (and $x85 (not $x91)) $x96))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142)))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x85) (= ?x157 2)))))))))))))))))))))))))))))) + (and (and (not $x52) $x69) (= ?x70 2)))))))))))))))))))))))))))))))) (check-sat) ; @@ -297,8 +309,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -319,7 +331,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -327,7 +340,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -342,13 +355,15 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80)))) (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90))) (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1)))))) (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90))) (let (($x109 (and $x85 $x91))) - (let ((?x157 (ite $x109 1 ?x149))) + (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1)))) + (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false))) (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108))))) (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108))) (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102))) @@ -356,7 +371,7 @@ (let (($x112 (and (and $x85 (not $x91)) $x96))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142)))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x85) (= ?x157 3)))))))))))))))))))))))))))))) + (and (and (not $x52) $x69) (= ?x70 3)))))))))))))))))))))))))))))))) (check-sat) ; @@ -369,8 +384,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -391,7 +406,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -399,13 +415,14 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) (let (($x53 (and true ipv4.$valid$))) (let (($x59 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) (let (($x65 (and $x53 $x59))) - (let ((?x79 (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))))) + (let ((?x84 (ite ipv4.$valid$ (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))) (- 1)))) + (let (($x71 (ite ipv4.$valid$ $x53 false))) (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x68 (and (and $x53 (not $x59)) $x64))) (let ((?x80 (concat (_ bv0 9) (_ bv1 1)))) @@ -421,7 +438,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -429,7 +447,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x53) (= ?x79 (- 1)))))))))))))))))))))))))))))))) + (and (and (not $x52) $x71) (= ?x84 (- 1)))))))))))))))))))))))))))))))))) (check-sat) ; @@ -442,8 +460,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -464,7 +482,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -472,13 +491,14 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) (let (($x53 (and true ipv4.$valid$))) (let (($x59 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) (let (($x65 (and $x53 $x59))) - (let ((?x79 (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))))) + (let ((?x84 (ite ipv4.$valid$ (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))) (- 1)))) + (let (($x71 (ite ipv4.$valid$ $x53 false))) (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x68 (and (and $x53 (not $x59)) $x64))) (let ((?x80 (concat (_ bv0 9) (_ bv1 1)))) @@ -494,7 +514,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -502,7 +523,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x53) (= ?x79 0))))))))))))))))))))))))))))))) + (and (and (not $x52) $x71) (= ?x84 0))))))))))))))))))))))))))))))))) (check-sat) ; @@ -515,8 +536,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -537,7 +558,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -545,13 +567,14 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) (let (($x53 (and true ipv4.$valid$))) (let (($x59 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) (let (($x65 (and $x53 $x59))) - (let ((?x79 (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))))) + (let ((?x84 (ite ipv4.$valid$ (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))) (- 1)))) + (let (($x71 (ite ipv4.$valid$ $x53 false))) (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x68 (and (and $x53 (not $x59)) $x64))) (let ((?x80 (concat (_ bv0 9) (_ bv1 1)))) @@ -567,7 +590,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -575,7 +599,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) $x53) (= ?x79 1))))))))))))))))))))))))))))))) + (and (and (not $x52) $x71) (= ?x84 1))))))))))))))))))))))))))))))))) (check-sat) ; @@ -588,8 +612,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x86 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86))) + (let (($x169 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -610,7 +634,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -618,7 +643,7 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))) + (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))) (assert (let ((?x50 (concat (_ bv0 9) (_ bv0 1)))) (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -639,7 +664,8 @@ (let ((?x47 (ite false (_ bv1 1) (_ bv0 1)))) (let ((?x76 (ite true (_ bv1 1) (_ bv0 1)))) (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1))))) + (let (($x83 (bvuge ?x82 (_ bv1 1)))) + (let (($x85 (and $x53 $x83))) (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x120 (and (and $x85 $x118) $x108))) (let (($x116 (and (and $x85 $x114) $x102))) @@ -647,5 +673,5 @@ (let (($x109 (and $x85 $x91))) (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125)))))) (let (($x52 (= ?x158 (_ bv511 9)))) - (and (and (not $x52) true) (= (- 1) (- 1))))))))))))))))))))))))))))))) + (and (and (not $x52) true) (= (- 1) (- 1)))))))))))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/vrf.txt b/p4_symbolic/symbolic/expected/vrf.txt index c2573bf90..297fffc02 100644 --- a/p4_symbolic/symbolic/expected/vrf.txt +++ b/p4_symbolic/symbolic/expected/vrf.txt @@ -6,7 +6,7 @@ Finding packet for table packet_ingress.ipv4_lpm_table and row 0 standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000000 ipv4.srcAddr = #x29210000 - ipv4.dstAddr = #x0a0a0080 + ipv4.dstAddr = #x0a0a0004 ethernet.dstAddr = #x000000000000 scalars.local_metadata_t.vrf = VRF1 scalars.local_metadata_t.vrf_is_valid = #b1 @@ -44,8 +44,8 @@ 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 = #b000000000 - standard_metadata.egress_spec = #b000000001 - ipv4.srcAddr = #x21000809 + standard_metadata.egress_spec = #b000000000 + ipv4.srcAddr = #x20000909 ipv4.dstAddr = #x00000000 ethernet.dstAddr = #x000000000000 scalars.local_metadata_t.vrf = VRF1 @@ -66,7 +66,7 @@ Finding packet for table packet_ingress.set_vrf_table and row 1 standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x21210000 - ipv4.dstAddr = #x0a000000 + ipv4.dstAddr = #x0a140000 ethernet.dstAddr = #x00000000000a scalars.local_metadata_t.vrf = VRF1 scalars.local_metadata_t.vrf_is_valid = #b1 @@ -76,7 +76,7 @@ Finding packet for table tbl_vrf133 and row -1 standard_metadata.ingress_port = #b000000000 standard_metadata.egress_spec = #b000000001 ipv4.srcAddr = #x21210000 - ipv4.dstAddr = #x0a000000 - ethernet.dstAddr = #x000000000000 + ipv4.dstAddr = #x0a140000 + ethernet.dstAddr = #x00000000000a scalars.local_metadata_t.vrf = VRF1 - scalars.local_metadata_t.vrf_is_valid = #b0 + scalars.local_metadata_t.vrf_is_valid = #b1 diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index 39d0ed24f..ab5add35a 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -484,15 +484,17 @@ absl::StatusOr EvaluateTable( for (const auto &[action, next_control] : sorted_action_to_next_control) { if (next_control != merge_point) { if (action == ir::TableHitAction() || action == ir::TableMissAction()) { - z3::expr branch_guard = action == ir::TableHitAction() - ? (match_index != kDefaultActionEntryIndex) - : (match_index == kDefaultActionEntryIndex); + z3::expr branch_condition = + action == ir::TableHitAction() + ? (match_index != kDefaultActionEntryIndex) + : (match_index == kDefaultActionEntryIndex); ASSIGN_OR_RETURN( SymbolicTableMatches branch_matches, control::EvaluateControl(data_plane, next_control, state, - translator, guard && branch_guard)); - ASSIGN_OR_RETURN(merged_matches, util::MergeDisjointTableMatches( - merged_matches, branch_matches)); + translator, guard && branch_condition)); + ASSIGN_OR_RETURN(merged_matches, + util::MergeMatchesOnCondition( + branch_condition, branch_matches, merged_matches)); } else { return absl::UnimplementedError( absl::Substitute("Conditional on executed table action is not " diff --git a/p4_symbolic/symbolic/test.bzl b/p4_symbolic/symbolic/test.bzl index b0b58d53c..ea6166a68 100644 --- a/p4_symbolic/symbolic/test.bzl +++ b/p4_symbolic/symbolic/test.bzl @@ -105,8 +105,6 @@ def end_to_end_test( ("--entries=$(location %s)" % table_entries if table_entries else ""), ("--debug=$(location %s)" % smt_output_file), ("--port_count=%d" % port_count), - # Redirect stderr to stdout, so we can capture both. - "2>&1", # Use `tee` to simultaneously capture output in file yet still print it to stdout, to # ease debugging. ("| tee $(location %s)" % test_output_file), diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc index 4e1e69033..e17ac707f 100644 --- a/p4_symbolic/symbolic/util.cc +++ b/p4_symbolic/symbolic/util.cc @@ -21,6 +21,7 @@ #include "absl/status/status.h" #include "absl/strings/str_format.h" #include "absl/strings/substitute.h" +#include "glog/logging.h" #include "p4_pdpi/utils/ir.h" #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/z3_util.h" @@ -139,18 +140,12 @@ absl::StatusOr MergeMatchesOnCondition( const SymbolicTableMatches &false_matches) { SymbolicTableMatches merged; - // Add all tables matches in true_trace. + // Merge all tables matches in true_trace (including ones in both traces). for (const auto &[name, true_match] : true_matches) { - // The table should not be applied in the other branch. - if (false_matches.contains(name)) { - return absl::InternalError( - absl::Substitute("Table '$0' was symbolically executed both in true " - "and false branches, this is not expected", - name)); - } - - // Get the default match for the false branch. - const SymbolicTableMatch false_match = DefaultTableMatch(); + // Find match in other trace (or use default). + const SymbolicTableMatch false_match = false_matches.contains(name) + ? false_matches.at(name) + : DefaultTableMatch(); // Merge this match. ASSIGN_OR_RETURN( @@ -165,14 +160,12 @@ absl::StatusOr MergeMatchesOnCondition( }}); } - // Add all tables matches in false_matches. + // Merge all tables matches in false_matches only. for (const auto &[name, false_match] : false_matches) { - // The table should not be applied in the other branch. if (true_matches.contains(name)) { - return absl::InternalError( - absl::Substitute("Table '$0' was symbolically executed both in true " - "and false branches, this is not expected", - name)); + // Already covered. + LOG(WARNING) << "Table '" << name << "' is evaluated more than once."; + continue; } // Get the default match for the true branch.