From c96bb21d4b92a1d75570fe9255d889b13d8ac006 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 27 Jul 2023 08:39:24 -0700 Subject: [PATCH 1/2] [P4-Symbolic] Assign egress_spec to egress_port only when the packet is not dropped in ingress. --- p4_symbolic/symbolic/expected/basic.smt2 | 10 ++-- .../symbolic/expected/conditional.smt2 | 10 ++-- .../expected/conditional_nonlattice.smt2 | 60 +++++++++---------- .../expected/conditional_sequence.smt2 | 12 ++-- p4_symbolic/symbolic/expected/hardcoded.smt2 | 11 ++-- p4_symbolic/symbolic/expected/reflector.smt2 | 13 ++-- .../symbolic/expected/string_optional.smt2 | 15 ++--- p4_symbolic/symbolic/expected/table.smt2 | 6 +- .../symbolic/expected/table_hit_1.smt2 | 39 ++++++------ .../symbolic/expected/table_hit_2.smt2 | 29 +++++---- p4_symbolic/symbolic/expected/vrf.smt2 | 10 ++-- p4_symbolic/symbolic/v1model.cc | 9 +-- 12 files changed, 114 insertions(+), 110 deletions(-) diff --git a/p4_symbolic/symbolic/expected/basic.smt2 b/p4_symbolic/symbolic/expected/basic.smt2 index f189a298..90b94d3e 100644 --- a/p4_symbolic/symbolic/expected/basic.smt2 +++ b/p4_symbolic/symbolic/expected/basic.smt2 @@ -241,7 +241,7 @@ (let ((a!10 (ite (and (and true a!1) (and true (= ipv4.dstAddr #x0a0a0000))) #b000000001 (ite a!2 #b000000000 (ite a!5 #b000000001 a!9))))) - (ite true a!10 standard_metadata.egress_port)))))) + (ite (not (= a!10 #b111111111)) a!10 standard_metadata.egress_port)))))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.etherType)) true false)) (a!3 (not (and true @@ -299,8 +299,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ethernet.etherType () (_ BitVec 16)) (assert - (let (($x136 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x136))) + (let (($x137 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x137))) (assert (let (($x56 (= ipv4.dstAddr (_ bv168427520 32)))) (let (($x57 (and true $x56))) @@ -321,7 +321,7 @@ (let (($x74 (and (and $x53 $x72) $x61))) (let (($x71 (and $x53 $x57))) (let ((?x124 (ite $x71 (_ bv1 9) (ite $x74 (_ bv0 9) (ite $x78 (_ bv1 9) ?x94))))) - (let (($x139 (or (or false (= ?x124 (_ bv0 9))) (= ?x124 (_ bv1 9))))) + (let (($x140 (or (or false (= ?x124 (_ bv0 9))) (= ?x124 (_ bv1 9))))) (let (($x45 (= ?x124 (_ bv511 9)))) - (or $x45 $x139))))))))))))))))))))))) + (or $x45 $x140))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional.smt2 b/p4_symbolic/symbolic/expected/conditional.smt2 index f44d8302..fbd2ecf9 100644 --- a/p4_symbolic/symbolic/expected/conditional.smt2 +++ b/p4_symbolic/symbolic/expected/conditional.smt2 @@ -79,7 +79,7 @@ (let ((a!4 (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!2 #b111111111 a!3))))) - (ite true a!4 standard_metadata.egress_port))) + (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) @@ -106,8 +106,8 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x63 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x63))) + (let (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64))) (assert (let (($x33 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) (let (($x35 (and true $x33))) @@ -117,7 +117,7 @@ (let (($x45 (and true $x44))) (let (($x46 (and true $x45))) (let ((?x54 (ite $x46 (_ bv1 9) ?x49))) - (let (($x66 (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))))) + (let (($x67 (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))))) (let (($x56 (= ?x54 (_ bv511 9)))) - (or $x56 $x66)))))))))))) + (or $x56 $x67)))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 index 2639b6b1..14bdd98e 100644 --- a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 @@ -93,7 +93,7 @@ (let ((a!7 (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!3 #b111111111 a!6))))) - (ite true a!7 standard_metadata.egress_port)))) + (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port)))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true @@ -134,29 +134,29 @@ (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x172 (= standard_metadata.ingress_port (_ bv19 9)))) - (let (($x167 (= standard_metadata.ingress_port (_ bv18 9)))) - (let (($x162 (= standard_metadata.ingress_port (_ bv17 9)))) - (let (($x157 (= standard_metadata.ingress_port (_ bv16 9)))) - (let (($x152 (= standard_metadata.ingress_port (_ bv15 9)))) - (let (($x147 (= standard_metadata.ingress_port (_ bv14 9)))) - (let (($x142 (= standard_metadata.ingress_port (_ bv13 9)))) - (let (($x137 (= standard_metadata.ingress_port (_ bv12 9)))) - (let (($x132 (= standard_metadata.ingress_port (_ bv11 9)))) - (let (($x127 (= standard_metadata.ingress_port (_ bv10 9)))) - (let (($x122 (= standard_metadata.ingress_port (_ bv9 9)))) - (let (($x117 (= standard_metadata.ingress_port (_ bv8 9)))) - (let (($x112 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x107 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x102 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x97 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x92 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x87 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x82 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x88 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x82) $x87))) - (let (($x123 (or (or (or (or (or (or (or $x88 $x92) $x97) $x102) $x107) $x112) $x117) $x122))) - (let (($x158 (or (or (or (or (or (or (or $x123 $x127) $x132) $x137) $x142) $x147) $x152) $x157))) - (or (or (or $x158 $x162) $x167) $x172)))))))))))))))))))))))) + (let (($x173 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x168 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x163 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x158 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x153 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x148 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x143 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x138 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x133 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x128 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x123 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x118 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x113 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x108 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x103 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x98 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x93 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x88 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x83 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x89 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x83) $x88))) + (let (($x124 (or (or (or (or (or (or (or $x89 $x93) $x98) $x103) $x108) $x113) $x118) $x123))) + (let (($x159 (or (or (or (or (or (or (or $x124 $x128) $x133) $x138) $x143) $x148) $x153) $x158))) + (or (or (or $x159 $x163) $x168) $x173)))))))))))))))))))))))) (assert (let (($x39 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) (let (($x33 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) @@ -173,11 +173,11 @@ (let (($x64 (and true $x63))) (let (($x65 (and true $x64))) (let ((?x73 (ite $x65 (_ bv1 9) ?x68))) - (let (($x95 (or (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))) (= ?x73 (_ bv3 9))))) - (let (($x115 (or (or (or (or $x95 (= ?x73 (_ bv4 9))) (= ?x73 (_ bv5 9))) (= ?x73 (_ bv6 9))) (= ?x73 (_ bv7 9))))) - (let (($x135 (or (or (or (or $x115 (= ?x73 (_ bv8 9))) (= ?x73 (_ bv9 9))) (= ?x73 (_ bv10 9))) (= ?x73 (_ bv11 9))))) - (let (($x155 (or (or (or (or $x135 (= ?x73 (_ bv12 9))) (= ?x73 (_ bv13 9))) (= ?x73 (_ bv14 9))) (= ?x73 (_ bv15 9))))) - (let (($x175 (or (or (or (or $x155 (= ?x73 (_ bv16 9))) (= ?x73 (_ bv17 9))) (= ?x73 (_ bv18 9))) (= ?x73 (_ bv19 9))))) + (let (($x96 (or (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))) (= ?x73 (_ bv3 9))))) + (let (($x116 (or (or (or (or $x96 (= ?x73 (_ bv4 9))) (= ?x73 (_ bv5 9))) (= ?x73 (_ bv6 9))) (= ?x73 (_ bv7 9))))) + (let (($x136 (or (or (or (or $x116 (= ?x73 (_ bv8 9))) (= ?x73 (_ bv9 9))) (= ?x73 (_ bv10 9))) (= ?x73 (_ bv11 9))))) + (let (($x156 (or (or (or (or $x136 (= ?x73 (_ bv12 9))) (= ?x73 (_ bv13 9))) (= ?x73 (_ bv14 9))) (= ?x73 (_ bv15 9))))) + (let (($x176 (or (or (or (or $x156 (= ?x73 (_ bv16 9))) (= ?x73 (_ bv17 9))) (= ?x73 (_ bv18 9))) (= ?x73 (_ bv19 9))))) (let (($x75 (= ?x73 (_ bv511 9)))) - (or $x75 $x175))))))))))))))))))))))) + (or $x75 $x176))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 index ed0b6044..fc3a5fe9 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 @@ -90,7 +90,7 @@ (egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth (egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta (egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (ite true +(egress) standard_metadata.egress_port: (ite (not (= standard_metadata.egress_spec #b111111111)) standard_metadata.egress_spec (ite (and true true (= h1.fr #xff)) #b000000001 @@ -113,11 +113,11 @@ (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x108 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x108))) + (let (($x109 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x109))) (assert - (let (($x110 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x111 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x110))) + (let (($x111 (= standard_metadata.egress_spec (_ bv1 9)))) + (let (($x112 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x111))) (let (($x94 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x94 $x111))))) + (or $x94 $x112))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/hardcoded.smt2 b/p4_symbolic/symbolic/expected/hardcoded.smt2 index 8e6253af..4b835ef2 100644 --- a/p4_symbolic/symbolic/expected/hardcoded.smt2 +++ b/p4_symbolic/symbolic/expected/hardcoded.smt2 @@ -58,7 +58,8 @@ (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) (concat #x00 #b1) standard_metadata.egress_spec))) - (ite true (ite a!1 (concat #x00 #b0) a!2) standard_metadata.egress_port)) +(let ((a!3 (not (= (ite a!1 (concat #x00 #b0) a!2) #b111111111)))) + (ite a!3 (ite a!1 (concat #x00 #b0) a!2) standard_metadata.egress_port))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) @@ -81,15 +82,15 @@ (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x49 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x49))) + (let (($x50 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x50))) (assert (let ((?x28 (concat (_ bv0 8) (_ bv0 1)))) (let (($x29 (= standard_metadata.ingress_port ?x28))) (let (($x31 (and true $x29))) (let (($x32 (and true (not $x29)))) (let ((?x37 (ite $x32 ?x28 (ite $x31 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x52 (or (or false (= ?x37 (_ bv0 9))) (= ?x37 (_ bv1 9))))) + (let (($x53 (or (or false (= ?x37 (_ bv0 9))) (= ?x37 (_ bv1 9))))) (let (($x41 (= ?x37 (_ bv511 9)))) - (or $x41 $x52))))))))) + (or $x41 $x53))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/reflector.smt2 b/p4_symbolic/symbolic/expected/reflector.smt2 index 5f125461..9c5ba037 100644 --- a/p4_symbolic/symbolic/expected/reflector.smt2 +++ b/p4_symbolic/symbolic/expected/reflector.smt2 @@ -54,7 +54,10 @@ (egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth (egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta (egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (ite true +(egress) standard_metadata.egress_port: (ite (not (= (ite true + standard_metadata.ingress_port + standard_metadata.egress_spec) + #b111111111)) (ite true standard_metadata.ingress_port standard_metadata.egress_spec) standard_metadata.egress_port) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid @@ -75,11 +78,11 @@ (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) (declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x37 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x37))) + (let (($x38 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x38))) (assert (let ((?x27 (ite true standard_metadata.ingress_port standard_metadata.egress_spec))) - (let (($x40 (or (or false (= ?x27 (_ bv0 9))) (= ?x27 (_ bv1 9))))) + (let (($x41 (or (or false (= ?x27 (_ bv0 9))) (= ?x27 (_ bv1 9))))) (let (($x29 (= ?x27 (_ bv511 9)))) - (or $x29 $x40))))) + (or $x29 $x41))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/string_optional.smt2 b/p4_symbolic/symbolic/expected/string_optional.smt2 index 9f134183..0210e513 100644 --- a/p4_symbolic/symbolic/expected/string_optional.smt2 +++ b/p4_symbolic/symbolic/expected/string_optional.smt2 @@ -94,11 +94,12 @@ a!3))) (let ((a!5 (and true (and true (= a!4 (concat #b0000000 #b10))))) (a!6 (not (and true (= a!4 (concat #b0000000 #b10)))))) - (ite true - (ite a!5 - #b000000000 - (ite (and true a!6 true) #b000000001 standard_metadata.egress_spec)) - standard_metadata.egress_port))))) +(let ((a!7 (ite a!5 + #b000000000 + (ite (and true a!6 true) + #b000000001 + standard_metadata.egress_spec)))) + (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port)))))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= standard_metadata.ingress_port #b000000000))) @@ -160,7 +161,7 @@ (let ((?x79 (ite (and (and true (not $x70)) true) (_ bv1 9) standard_metadata.egress_spec))) (let (($x71 (and true $x70))) (let ((?x81 (ite $x71 (_ bv0 9) ?x79))) - (let (($x88 (or (or (or false (= ?x81 (_ bv0 9))) (= ?x81 (_ bv1 9))) (= ?x81 (_ bv2 9))))) + (let (($x89 (or (or (or false (= ?x81 (_ bv0 9))) (= ?x81 (_ bv1 9))) (= ?x81 (_ bv2 9))))) (let (($x51 (= ?x81 (_ bv511 9)))) - (or $x51 $x88))))))))))))))))))))) + (or $x51 $x89))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table.smt2 b/p4_symbolic/symbolic/expected/table.smt2 index 786fa168..f6ae7815 100644 --- a/p4_symbolic/symbolic/expected/table.smt2 +++ b/p4_symbolic/symbolic/expected/table.smt2 @@ -62,7 +62,7 @@ (and true (= standard_metadata.ingress_port #b000000000))) #b000000001 (ite a!1 #b000000000 standard_metadata.egress_spec)))) - (ite true a!2 standard_metadata.egress_port))) + (ite (not (= a!2 #b111111111)) a!2 standard_metadata.egress_port))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= standard_metadata.ingress_port #b000000000))) @@ -97,7 +97,7 @@ (let (($x28 (and true $x27))) (let (($x32 (and true $x28))) (let ((?x46 (ite $x32 (_ bv1 9) (ite (and $x34 $x31) (_ bv0 9) standard_metadata.egress_spec)))) - (let (($x52 (or (or false (= ?x46 (_ bv0 9))) (= ?x46 (_ bv1 9))))) + (let (($x53 (or (or false (= ?x46 (_ bv0 9))) (= ?x46 (_ bv1 9))))) (let (($x37 (= ?x46 (_ bv511 9)))) - (or $x37 $x52))))))))))) + (or $x37 $x53))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_1.smt2 b/p4_symbolic/symbolic/expected/table_hit_1.smt2 index 31f6c69a..7ffdff09 100644 --- a/p4_symbolic/symbolic/expected/table_hit_1.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_1.smt2 @@ -82,14 +82,13 @@ (let ((a!3 (ite (and true (and true (= ethernet.ether_type #x0010))) #b000000010 (ite a!2 #b111111111 standard_metadata.egress_spec)))) - (ite true - (ite (and true - (distinct a!1 (- 1)) - true - (= ethernet.src_addr #x000000000100)) - #b000000011 - a!3) - standard_metadata.egress_port))) +(let ((a!4 (ite (and true + (distinct a!1 (- 1)) + true + (= ethernet.src_addr #x000000000100)) + #b000000011 + a!3))) + (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (and true (= ethernet.ether_type #x0010))) 0 (- 1))) (a!2 (and true (not (and true (= ethernet.ether_type #x0010)))))) @@ -117,15 +116,15 @@ (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (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 (($x95 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x75 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x71 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x67 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x72 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x67) $x71))) + (or (or (or (or (or $x72 $x75) $x80) $x85) $x90) $x95)))))))))) (assert (let ((?x38 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) (let (($x31 (= ethernet.ether_type (_ bv16 16)))) @@ -136,8 +135,8 @@ (let (($x46 (and true $x45))) (let (($x50 (and $x46 (and true (= ethernet.src_addr (_ bv256 48)))))) (let ((?x56 (ite $x50 (_ bv3 9) (ite $x33 (_ bv2 9) ?x38)))) - (let (($x77 (or (or (or (or false (= ?x56 (_ bv0 9))) (= ?x56 (_ bv1 9))) (= ?x56 (_ bv2 9))) (= ?x56 (_ bv3 9))))) - (let (($x97 (or (or (or (or $x77 (= ?x56 (_ bv4 9))) (= ?x56 (_ bv5 9))) (= ?x56 (_ bv6 9))) (= ?x56 (_ bv7 9))))) + (let (($x78 (or (or (or (or false (= ?x56 (_ bv0 9))) (= ?x56 (_ bv1 9))) (= ?x56 (_ bv2 9))) (= ?x56 (_ bv3 9))))) + (let (($x98 (or (or (or (or $x78 (= ?x56 (_ bv4 9))) (= ?x56 (_ bv5 9))) (= ?x56 (_ bv6 9))) (= ?x56 (_ bv7 9))))) (let (($x58 (= ?x56 (_ bv511 9)))) - (or $x58 $x97)))))))))))))) + (or $x58 $x98)))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_2.smt2 b/p4_symbolic/symbolic/expected/table_hit_2.smt2 index 0d0ea873..38eb57aa 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_2.smt2 @@ -79,9 +79,8 @@ (ite (and true true (= h1.f1 #xff)) #b000000001 (ite true (concat #x00 #b0) standard_metadata.egress_spec))))) - (ite true - (ite (and true a!1 true (= h1.f3 #xff)) #b000000011 a!3) - standard_metadata.egress_port))) +(let ((a!4 (ite (and true a!1 true (= h1.f3 #xff)) #b000000011 a!3))) + (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (= (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1))) (a!2 (distinct (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1)))) @@ -110,15 +109,15 @@ (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x102 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x97 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x92 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x87 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x82 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x78 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x74 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x79 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x74) $x78))) - (or (or (or (or (or $x79 $x82) $x87) $x92) $x97) $x102)))))))))) + (let (($x103 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x98 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x93 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x88 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x83 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x79 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x75 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x80 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x75) $x79))) + (or (or (or (or (or $x80 $x83) $x88) $x93) $x98) $x103)))))))))) (assert (let (($x37 (= h1.f1 (_ bv255 8)))) (let (($x38 (and true $x37))) @@ -132,8 +131,8 @@ (let (($x57 (and true $x56))) (let (($x60 (and $x57 (and true (= h1.f3 (_ bv255 8)))))) (let ((?x65 (ite $x60 (_ bv3 9) (ite $x50 (_ bv2 9) ?x45)))) - (let (($x85 (or (or (or (or false (= ?x65 (_ bv0 9))) (= ?x65 (_ bv1 9))) (= ?x65 (_ bv2 9))) (= ?x65 (_ bv3 9))))) - (let (($x105 (or (or (or (or $x85 (= ?x65 (_ bv4 9))) (= ?x65 (_ bv5 9))) (= ?x65 (_ bv6 9))) (= ?x65 (_ bv7 9))))) + (let (($x86 (or (or (or (or false (= ?x65 (_ bv0 9))) (= ?x65 (_ bv1 9))) (= ?x65 (_ bv2 9))) (= ?x65 (_ bv3 9))))) + (let (($x106 (or (or (or (or $x86 (= ?x65 (_ bv4 9))) (= ?x65 (_ bv5 9))) (= ?x65 (_ bv6 9))) (= ?x65 (_ bv7 9))))) (let (($x41 (= ?x65 (_ bv511 9)))) - (or $x41 $x105))))))))))))))))) + (or $x41 $x106))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2 index b20bd54b..0f876256 100644 --- a/p4_symbolic/symbolic/expected/vrf.smt2 +++ b/p4_symbolic/symbolic/expected/vrf.smt2 @@ -356,7 +356,7 @@ (let ((a!15 (ite (and (and (and true a!1) (bvuge a!5 #b1)) a!7) #b000000001 a!14))) - (ite true a!15 standard_metadata.egress_port))))))))) + (ite (not (= a!15 #b111111111)) a!15 standard_metadata.egress_port))))))))) (egress) standard_metadata.egress_rid: standard_metadata.egress_rid (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.eth_type)) true false)) (a!3 (not (and true (= (bvand ipv4.srcAddr #x09210909) #x00210100))))) @@ -437,8 +437,8 @@ (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x180 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x180))) + (let (($x181 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x181))) (assert (let ((?x61 (concat (_ bv0 9) (_ bv0 1)))) (let (($x75 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) @@ -470,7 +470,7 @@ (let (($x123 (and (and $x96 $x121) $x107))) (let (($x120 (and $x96 $x102))) (let ((?x169 (ite $x120 (_ bv1 9) (ite $x123 (_ bv0 9) (ite $x127 (_ bv1 9) (ite $x131 (_ bv1 9) ?x136)))))) - (let (($x183 (or (or false (= ?x169 (_ bv0 9))) (= ?x169 (_ bv1 9))))) + (let (($x184 (or (or false (= ?x169 (_ bv0 9))) (= ?x169 (_ bv1 9))))) (let (($x63 (= ?x169 (_ bv511 9)))) - (or $x63 $x183)))))))))))))))))))))))))))))))))) + (or $x63 $x184)))))))))))))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/v1model.cc b/p4_symbolic/symbolic/v1model.cc index 51f7bfb8..00f39a19 100644 --- a/p4_symbolic/symbolic/v1model.cc +++ b/p4_symbolic/symbolic/v1model.cc @@ -148,12 +148,13 @@ absl::Status EvaluateV1model(const ir::Dataplane &data_plane, /*guard=*/Z3Context().bool_val(true))); ASSIGN_OR_RETURN(z3::expr dropped, IsDropped(context.egress_headers)); - // Constrain egress_port to be equal to egress_spec. + // Assign egress_spec to egress_port if the packet is not dropped. + // https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md ASSIGN_OR_RETURN(z3::expr egress_spec, context.egress_headers.Get("standard_metadata.egress_spec")); - RETURN_IF_ERROR( - context.egress_headers.Set("standard_metadata.egress_port", egress_spec, - /*guard=*/Z3Context().bool_val(true))); + RETURN_IF_ERROR(context.egress_headers.Set("standard_metadata.egress_port", + egress_spec, + /*guard=*/!dropped)); // Evaluate the egress pipeline. ASSIGN_OR_RETURN( From b29775ccb1fd14f1dea5ff7fcaf5240a87a4a191 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 27 Jul 2023 09:29:38 -0700 Subject: [PATCH 2/2] [P4-Symbolic] Initialize standard metadata fields to 0. --- p4_symbolic/symbolic/BUILD.bazel | 9 +- p4_symbolic/symbolic/expected/basic.smt2 | 119 ++++++------- p4_symbolic/symbolic/expected/basic.txt | 32 ++-- .../symbolic/expected/conditional.smt2 | 101 ++++++----- .../expected/conditional_nonlattice.smt2 | 168 +++++++++--------- .../expected/conditional_nonlattice.txt | 16 +- .../expected/conditional_sequence.smt2 | 88 +++++---- p4_symbolic/symbolic/expected/hardcoded.smt2 | 95 +++++----- p4_symbolic/symbolic/expected/reflector.smt2 | 92 +++++----- .../symbolic/expected/string_optional.smt2 | 124 ++++++------- p4_symbolic/symbolic/expected/table.smt2 | 122 ++++++------- .../symbolic/expected/table_hit_1.smt2 | 119 ++++++------- .../symbolic/expected/table_hit_2.smt2 | 124 +++++++------ p4_symbolic/symbolic/expected/table_hit_2.txt | 20 +-- p4_symbolic/symbolic/expected/vrf.smt2 | 145 ++++++++------- p4_symbolic/symbolic/expected/vrf.txt | 36 ++-- p4_symbolic/symbolic/v1model_intrinsic.h | 33 ++++ 17 files changed, 717 insertions(+), 726 deletions(-) create mode 100644 p4_symbolic/symbolic/v1model_intrinsic.h diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 30ed2f47..77af8734 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -47,6 +47,7 @@ cc_library( "table.h", "util.h", "v1model.h", + "v1model_intrinsic.h", "values.h", ], deps = [ @@ -106,14 +107,6 @@ end_to_end_test( smt_golden_file = "expected/reflector.smt2", ) -end_to_end_test( - name = "ipv4_routing_test", - p4_program = "//p4_symbolic/testdata:ipv4-routing/basic.p4", - packets_golden_file = "expected/basic.txt", - smt_golden_file = "expected/basic.smt2", - table_entries = "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt", -) - # Checks the behavior of symbolic execution when there is a table application after a conditional. # Before go/optimized-symbolic-execution, p4-symbolic was executing t3 twice (once from the if # branch and once from the else branch). Now it executed each table exactly once, leading to diff --git a/p4_symbolic/symbolic/expected/basic.smt2 b/p4_symbolic/symbolic/expected/basic.smt2 index 90b94d3e..110c975b 100644 --- a/p4_symbolic/symbolic/expected/basic.smt2 +++ b/p4_symbolic/symbolic/expected/basic.smt2 @@ -23,22 +23,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -65,26 +65,26 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.etherType)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.etherType) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -203,10 +203,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.etherType)) true false)) (a!3 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) @@ -237,12 +237,12 @@ #b000000001 (ite (and (and true a!1) (and a!4 a!6) a!8) #b111111111 - standard_metadata.egress_spec)))) + #b000000000)))) (let ((a!10 (ite (and (and true a!1) (and true (= ipv4.dstAddr #x0a0a0000))) #b000000001 (ite a!2 #b000000000 (ite a!5 #b000000001 a!9))))) (ite (not (= a!10 #b111111111)) a!10 standard_metadata.egress_port)))))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.etherType)) true false)) (a!3 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) @@ -273,55 +273,54 @@ #b000000001 (ite (and (and true a!1) (and a!4 a!6) a!8) #b111111111 - standard_metadata.egress_spec)))) + #b000000000)))) (ite (and (and true a!1) (and true (= ipv4.dstAddr #x0a0a0000))) #b000000001 (ite a!2 #b000000000 (ite a!5 #b000000001 a!9))))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.etherType)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.etherType) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ethernet.etherType () (_ BitVec 16)) (assert - (let (($x137 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x137))) + (let (($x129 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x129))) (assert - (let (($x56 (= ipv4.dstAddr (_ bv168427520 32)))) - (let (($x57 (and true $x56))) - (let (($x72 (not $x57))) - (let (($x76 (and $x72 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) - (let (($x80 (and $x76 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) - (let (($x84 (and $x80 (not (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))))) + (let (($x50 (= ipv4.dstAddr (_ bv168427520 32)))) + (let (($x51 (and true $x50))) + (let (($x66 (not $x51))) + (let (($x70 (and $x66 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) + (let (($x74 (and $x70 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) + (let (($x78 (and $x74 (not (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))))) (let (($x11 (= (concat (_ bv0 4) (_ bv2048 12)) ethernet.etherType))) (let (($x10 (and true $x11))) - (let (($x48 (ite $x10 true false))) - (let (($x53 (and true $x48))) - (let (($x70 (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))) - (let (($x82 (and (and $x53 $x80) $x70))) - (let ((?x94 (ite $x82 (_ bv1 9) (ite (and $x53 $x84) (_ bv511 9) standard_metadata.egress_spec)))) - (let (($x65 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))) - (let (($x78 (and (and $x53 $x76) $x65))) - (let (($x61 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))) - (let (($x74 (and (and $x53 $x72) $x61))) - (let (($x71 (and $x53 $x57))) - (let ((?x124 (ite $x71 (_ bv1 9) (ite $x74 (_ bv0 9) (ite $x78 (_ bv1 9) ?x94))))) - (let (($x140 (or (or false (= ?x124 (_ bv0 9))) (= ?x124 (_ bv1 9))))) - (let (($x45 (= ?x124 (_ bv511 9)))) - (or $x45 $x140))))))))))))))))))))))) + (let (($x38 (ite $x10 true false))) + (let (($x47 (and true $x38))) + (let (($x64 (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))) + (let (($x76 (and (and $x47 $x74) $x64))) + (let (($x59 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))) + (let (($x72 (and (and $x47 $x70) $x59))) + (let (($x55 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))) + (let (($x68 (and (and $x47 $x66) $x55))) + (let ((?x108 (ite $x68 (_ bv0 9) (ite $x72 (_ bv1 9) (ite $x76 (_ bv1 9) (ite (and $x47 $x78) (_ bv511 9) (_ bv0 9))))))) + (let (($x65 (and $x47 $x51))) + (let ((?x116 (ite $x65 (_ bv1 9) ?x108))) + (let (($x132 (or (or false (= ?x116 (_ bv0 9))) (= ?x116 (_ bv1 9))))) + (let (($x44 (= ?x116 (_ bv511 9)))) + (or $x44 $x132))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/basic.txt b/p4_symbolic/symbolic/expected/basic.txt index d265e27e..27d6f6ba 100644 --- a/p4_symbolic/symbolic/expected/basic.txt +++ b/p4_symbolic/symbolic/expected/basic.txt @@ -7,7 +7,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 0 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000000 trace: dropped = 0 @@ -50,7 +50,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -93,7 +93,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -136,7 +136,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -147,7 +147,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 1 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000001 trace: dropped = 0 @@ -190,7 +190,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -233,7 +233,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -276,7 +276,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -287,7 +287,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 2 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000001 trace: dropped = 0 @@ -330,7 +330,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -373,7 +373,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -416,7 +416,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -427,7 +427,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 3 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000001 trace: dropped = 0 @@ -470,7 +470,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -513,7 +513,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -556,7 +556,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 diff --git a/p4_symbolic/symbolic/expected/conditional.smt2 b/p4_symbolic/symbolic/expected/conditional.smt2 index fbd2ecf9..91689af0 100644 --- a/p4_symbolic/symbolic/expected/conditional.smt2 +++ b/p4_symbolic/symbolic/expected/conditional.smt2 @@ -9,22 +9,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -37,22 +37,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -67,57 +67,56 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!3 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) #b111111111 - standard_metadata.egress_spec))) + #b000000000))) (let ((a!4 (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!2 #b111111111 a!3))))) (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!3 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) #b111111111 - standard_metadata.egress_spec))) + #b000000000))) (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!2 #b111111111 a!3)))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (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 (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64))) + (let (($x56 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x56))) (assert - (let (($x33 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) - (let (($x35 (and true $x33))) - (let (($x36 (and true (not $x33)))) - (let ((?x49 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x36 (_ bv511 9) (ite $x35 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x44 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x45 (and true $x44))) - (let (($x46 (and true $x45))) - (let ((?x54 (ite $x46 (_ bv1 9) ?x49))) - (let (($x67 (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))))) - (let (($x56 (= ?x54 (_ bv511 9)))) - (or $x56 $x67)))))))))))) + (let (($x12 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) + (let (($x24 (and true $x12))) + (let (($x17 (and true (not $x12)))) + (let ((?x42 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x17 (_ bv511 9) (ite $x24 (_ bv511 9) (_ bv0 9)))))) + (let (($x37 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x38 (and true $x37))) + (let (($x39 (and true $x38))) + (let ((?x47 (ite $x39 (_ bv1 9) ?x42))) + (let (($x59 (or (or false (= ?x47 (_ bv0 9))) (= ?x47 (_ bv1 9))))) + (let (($x49 (= ?x47 (_ bv511 9)))) + (or $x49 $x59)))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 index 14bdd98e..e2060054 100644 --- a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 @@ -9,22 +9,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -37,22 +37,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -67,10 +67,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (bvugt standard_metadata.ingress_port (concat #b00000 #xa))))) @@ -87,14 +87,12 @@ (bvugt standard_metadata.ingress_port (concat #b000000 #b101))) #b111111111 - (ite a!4 - #b111111111 - (ite a!5 #b111111111 standard_metadata.egress_spec))))) + (ite a!4 #b111111111 (ite a!5 #b111111111 #b000000000))))) (let ((a!7 (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!3 #b111111111 a!6))))) (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port)))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (bvugt standard_metadata.ingress_port (concat #b00000 #xa))))) @@ -111,73 +109,69 @@ (bvugt standard_metadata.ingress_port (concat #b000000 #b101))) #b111111111 - (ite a!4 - #b111111111 - (ite a!5 #b111111111 standard_metadata.egress_spec))))) + (ite a!4 #b111111111 (ite a!5 #b111111111 #b000000000))))) (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!3 #b111111111 a!6))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (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 (($x173 (= standard_metadata.ingress_port (_ bv19 9)))) - (let (($x168 (= standard_metadata.ingress_port (_ bv18 9)))) - (let (($x163 (= standard_metadata.ingress_port (_ bv17 9)))) - (let (($x158 (= standard_metadata.ingress_port (_ bv16 9)))) - (let (($x153 (= standard_metadata.ingress_port (_ bv15 9)))) - (let (($x148 (= standard_metadata.ingress_port (_ bv14 9)))) - (let (($x143 (= standard_metadata.ingress_port (_ bv13 9)))) - (let (($x138 (= standard_metadata.ingress_port (_ bv12 9)))) - (let (($x133 (= standard_metadata.ingress_port (_ bv11 9)))) - (let (($x128 (= standard_metadata.ingress_port (_ bv10 9)))) - (let (($x123 (= standard_metadata.ingress_port (_ bv9 9)))) - (let (($x118 (= standard_metadata.ingress_port (_ bv8 9)))) - (let (($x113 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x108 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x103 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x98 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x93 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x88 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x83 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x89 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x83) $x88))) - (let (($x124 (or (or (or (or (or (or (or $x89 $x93) $x98) $x103) $x108) $x113) $x118) $x123))) - (let (($x159 (or (or (or (or (or (or (or $x124 $x128) $x133) $x138) $x143) $x148) $x153) $x158))) - (or (or (or $x159 $x163) $x168) $x173)))))))))))))))))))))))) + (let (($x166 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x161 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x156 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x151 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x146 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x141 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x136 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x131 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x126 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x121 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x116 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x111 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x106 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x101 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x96 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x91 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x86 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x81 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x82 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x76) $x81))) + (let (($x117 (or (or (or (or (or (or (or $x82 $x86) $x91) $x96) $x101) $x106) $x111) $x116))) + (let (($x152 (or (or (or (or (or (or (or $x117 $x121) $x126) $x131) $x136) $x141) $x146) $x151))) + (or (or (or $x152 $x156) $x161) $x166)))))))))))))))))))))))) (assert - (let (($x39 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) - (let (($x33 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) - (let (($x35 (and true $x33))) - (let (($x41 (and $x35 $x39))) - (let (($x42 (and $x35 (not $x39)))) - (let (($x52 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) - (let (($x36 (and true (not $x33)))) - (let (($x54 (and $x36 $x52))) - (let ((?x56 (ite $x54 (_ bv511 9) (ite $x42 (_ bv511 9) (ite $x41 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x55 (and $x36 (not $x52)))) - (let ((?x68 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x55 (_ bv511 9) ?x56)))) - (let (($x63 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x64 (and true $x63))) - (let (($x65 (and true $x64))) - (let ((?x73 (ite $x65 (_ bv1 9) ?x68))) - (let (($x96 (or (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))) (= ?x73 (_ bv3 9))))) - (let (($x116 (or (or (or (or $x96 (= ?x73 (_ bv4 9))) (= ?x73 (_ bv5 9))) (= ?x73 (_ bv6 9))) (= ?x73 (_ bv7 9))))) - (let (($x136 (or (or (or (or $x116 (= ?x73 (_ bv8 9))) (= ?x73 (_ bv9 9))) (= ?x73 (_ bv10 9))) (= ?x73 (_ bv11 9))))) - (let (($x156 (or (or (or (or $x136 (= ?x73 (_ bv12 9))) (= ?x73 (_ bv13 9))) (= ?x73 (_ bv14 9))) (= ?x73 (_ bv15 9))))) - (let (($x176 (or (or (or (or $x156 (= ?x73 (_ bv16 9))) (= ?x73 (_ bv17 9))) (= ?x73 (_ bv18 9))) (= ?x73 (_ bv19 9))))) - (let (($x75 (= ?x73 (_ bv511 9)))) - (or $x75 $x176))))))))))))))))))))))) + (let (($x33 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x27 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x17 (and true $x27))) + (let (($x35 (and $x17 $x33))) + (let (($x36 (and $x17 (not $x33)))) + (let (($x46 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x22 (and true (not $x27)))) + (let (($x48 (and $x22 $x46))) + (let (($x49 (and $x22 (not $x46)))) + (let ((?x62 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x49 (_ bv511 9) (ite $x48 (_ bv511 9) (ite $x36 (_ bv511 9) (ite $x35 (_ bv511 9) (_ bv0 9)))))))) + (let (($x57 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x58 (and true $x57))) + (let (($x59 (and true $x58))) + (let ((?x67 (ite $x59 (_ bv1 9) ?x62))) + (let (($x89 (or (or (or (or false (= ?x67 (_ bv0 9))) (= ?x67 (_ bv1 9))) (= ?x67 (_ bv2 9))) (= ?x67 (_ bv3 9))))) + (let (($x109 (or (or (or (or $x89 (= ?x67 (_ bv4 9))) (= ?x67 (_ bv5 9))) (= ?x67 (_ bv6 9))) (= ?x67 (_ bv7 9))))) + (let (($x129 (or (or (or (or $x109 (= ?x67 (_ bv8 9))) (= ?x67 (_ bv9 9))) (= ?x67 (_ bv10 9))) (= ?x67 (_ bv11 9))))) + (let (($x149 (or (or (or (or $x129 (= ?x67 (_ bv12 9))) (= ?x67 (_ bv13 9))) (= ?x67 (_ bv14 9))) (= ?x67 (_ bv15 9))))) + (let (($x169 (or (or (or (or $x149 (= ?x67 (_ bv16 9))) (= ?x67 (_ bv17 9))) (= ?x67 (_ bv18 9))) (= ?x67 (_ bv19 9))))) + (let (($x69 (= ?x67 (_ bv511 9)))) + (or $x69 $x169)))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.txt b/p4_symbolic/symbolic/expected/conditional_nonlattice.txt index 39b32a5b..a1f18593 100644 --- a/p4_symbolic/symbolic/expected/conditional_nonlattice.txt +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.txt @@ -101,7 +101,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.t_2 and row -1 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000001100 egress_port = #b000000001 trace: dropped = 0 @@ -132,7 +132,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -161,7 +161,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -190,7 +190,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -207,7 +207,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.t_3 and row 0 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000001100 egress_port = #b000000001 trace: dropped = 0 @@ -238,7 +238,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -267,7 +267,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -296,7 +296,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 index fc3a5fe9..334097a3 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 @@ -16,22 +16,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) h1.$extracted$: (ite true true false) @@ -51,22 +51,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) h1.$extracted$: (ite true true false) @@ -86,38 +86,36 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (ite (not (= standard_metadata.egress_spec #b111111111)) - standard_metadata.egress_spec +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 +(egress) standard_metadata.egress_port: (ite (not (= #b000000000 #b111111111)) + #b000000000 (ite (and true true (= h1.fr #xff)) #b000000001 standard_metadata.egress_port)) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid -(egress) standard_metadata.egress_spec: standard_metadata.egress_spec -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.egress_rid: #x0000 +(egress) standard_metadata.egress_spec: #b000000000 +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x109 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x109))) + (let (($x101 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x101))) (assert - (let (($x111 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x112 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x111))) - (let (($x94 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x94 $x112))))) + (let (($x104 (or (or false (= (_ bv0 9) (_ bv0 9))) (= (_ bv0 9) (_ bv1 9))))) + (let (($x87 (= (_ bv0 9) (_ bv511 9)))) + (or $x87 $x104)))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/hardcoded.smt2 b/p4_symbolic/symbolic/expected/hardcoded.smt2 index 4b835ef2..1c4dee64 100644 --- a/p4_symbolic/symbolic/expected/hardcoded.smt2 +++ b/p4_symbolic/symbolic/expected/hardcoded.smt2 @@ -4,22 +4,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -27,22 +27,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -50,47 +50,46 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) (concat #x00 #b1) - standard_metadata.egress_spec))) + #b000000000))) (let ((a!3 (not (= (ite a!1 (concat #x00 #b0) a!2) #b111111111)))) (ite a!3 (ite a!1 (concat #x00 #b0) a!2) standard_metadata.egress_port))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) (concat #x00 #b1) - standard_metadata.egress_spec))) + #b000000000))) (ite a!1 (concat #x00 #b0) a!2)) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x50 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x50))) + (let (($x42 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x42))) (assert - (let ((?x28 (concat (_ bv0 8) (_ bv0 1)))) - (let (($x29 (= standard_metadata.ingress_port ?x28))) - (let (($x31 (and true $x29))) - (let (($x32 (and true (not $x29)))) - (let ((?x37 (ite $x32 ?x28 (ite $x31 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x53 (or (or false (= ?x37 (_ bv0 9))) (= ?x37 (_ bv1 9))))) - (let (($x41 (= ?x37 (_ bv511 9)))) - (or $x41 $x53))))))))) + (let ((?x22 (concat (_ bv0 8) (_ bv0 1)))) + (let (($x8 (= standard_metadata.ingress_port ?x22))) + (let (($x12 (and true $x8))) + (let (($x17 (and true (not $x8)))) + (let ((?x30 (ite $x17 ?x22 (ite $x12 (concat (_ bv0 8) (_ bv1 1)) (_ bv0 9))))) + (let (($x45 (or (or false (= ?x30 (_ bv0 9))) (= ?x30 (_ bv1 9))))) + (let (($x34 (= ?x30 (_ bv511 9)))) + (or $x34 $x45))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/reflector.smt2 b/p4_symbolic/symbolic/expected/reflector.smt2 index 9c5ba037..fc64a14a 100644 --- a/p4_symbolic/symbolic/expected/reflector.smt2 +++ b/p4_symbolic/symbolic/expected/reflector.smt2 @@ -4,22 +4,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -27,22 +27,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -50,39 +50,35 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (ite (not (= (ite true - standard_metadata.ingress_port - standard_metadata.egress_spec) - #b111111111)) - (ite true standard_metadata.ingress_port standard_metadata.egress_spec) +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 +(egress) standard_metadata.egress_port: (ite (not (= (ite true standard_metadata.ingress_port #b000000000) #b111111111)) + (ite true standard_metadata.ingress_port #b000000000) standard_metadata.egress_port) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid -(egress) standard_metadata.egress_spec: (ite true standard_metadata.ingress_port standard_metadata.egress_spec) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.egress_rid: #x0000 +(egress) standard_metadata.egress_spec: (ite true standard_metadata.ingress_port #b000000000) +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x38 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x38))) + (let (($x31 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x31))) (assert - (let ((?x27 (ite true standard_metadata.ingress_port standard_metadata.egress_spec))) - (let (($x41 (or (or false (= ?x27 (_ bv0 9))) (= ?x27 (_ bv1 9))))) - (let (($x29 (= ?x27 (_ bv511 9)))) - (or $x29 $x41))))) + (let (($x34 (or (or false (= (ite true standard_metadata.ingress_port (_ bv0 9)) (_ bv0 9))) (= (ite true standard_metadata.ingress_port (_ bv0 9)) (_ bv1 9))))) + (let ((?x10 (ite true standard_metadata.ingress_port (_ bv0 9)))) + (let (($x19 (= ?x10 (_ bv511 9)))) + (or $x19 $x34))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/string_optional.smt2 b/p4_symbolic/symbolic/expected/string_optional.smt2 index 0210e513..efaf665c 100644 --- a/p4_symbolic/symbolic/expected/string_optional.smt2 +++ b/p4_symbolic/symbolic/expected/string_optional.smt2 @@ -6,22 +6,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -31,22 +31,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -71,10 +71,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (and true (= standard_metadata.ingress_port #b000000000))) (and true (= standard_metadata.ingress_port #b000000001)))) @@ -96,11 +96,9 @@ (a!6 (not (and true (= a!4 (concat #b0000000 #b10)))))) (let ((a!7 (ite a!5 #b000000000 - (ite (and true a!6 true) - #b000000001 - standard_metadata.egress_spec)))) + (ite (and true a!6 true) #b000000001 #b000000000)))) (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port)))))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= standard_metadata.ingress_port #b000000000))) (and true (= standard_metadata.ingress_port #b000000001)))) @@ -120,48 +118,44 @@ a!3))) (let ((a!5 (and true (and true (= a!4 (concat #b0000000 #b10))))) (a!6 (not (and true (= a!4 (concat #b0000000 #b10)))))) - (ite a!5 - #b000000000 - (ite (and true a!6 true) #b000000001 standard_metadata.egress_spec)))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp + (ite a!5 #b000000000 (ite (and true a!6 true) #b000000001 #b000000000)))))) +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun scalars.metadata.string_field () (_ BitVec 9)) (assert - (let (($x40 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x37 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x37) $x40)))) + (let (($x32 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x29 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x29) $x32)))) (assert - (let ((?x67 (concat (_ bv0 7) (_ bv2 2)))) - (let ((?x31 (concat (_ bv0 8) (_ bv0 1)))) - (let (($x40 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x41 (and true $x40))) - (let (($x34 (= standard_metadata.ingress_port (_ bv0 9)))) - (let (($x35 (and true $x34))) - (let (($x43 (not $x35))) - (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port (_ bv1 9)))))))) - (let ((?x56 (ite (and $x48 $x41) ?x31 (ite true ?x31 scalars.metadata.string_field)))) - (let (($x37 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x38 (and true $x37))) - (let (($x42 (and true $x35))) - (let ((?x68 (ite $x42 ?x67 (ite (and (and true $x43) $x38) (concat (_ bv0 8) (_ bv1 1)) ?x56)))) - (let (($x70 (and true (= ?x68 ?x67)))) - (let ((?x79 (ite (and (and true (not $x70)) true) (_ bv1 9) standard_metadata.egress_spec))) - (let (($x71 (and true $x70))) - (let ((?x81 (ite $x71 (_ bv0 9) ?x79))) - (let (($x89 (or (or (or false (= ?x81 (_ bv0 9))) (= ?x81 (_ bv1 9))) (= ?x81 (_ bv2 9))))) - (let (($x51 (= ?x81 (_ bv511 9)))) - (or $x51 $x89))))))))))))))))))))) + (let ((?x59 (concat (_ bv0 7) (_ bv2 2)))) + (let ((?x24 (concat (_ bv0 8) (_ bv0 1)))) + (let (($x32 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x33 (and true $x32))) + (let (($x14 (= standard_metadata.ingress_port (_ bv0 9)))) + (let (($x19 (and true $x14))) + (let (($x35 (not $x19))) + (let (($x40 (and true (and $x35 (not (and true (= standard_metadata.ingress_port (_ bv1 9)))))))) + (let ((?x48 (ite (and $x40 $x33) ?x24 (ite true ?x24 scalars.metadata.string_field)))) + (let (($x29 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x30 (and true $x29))) + (let (($x34 (and true $x19))) + (let ((?x60 (ite $x34 ?x59 (ite (and (and true $x35) $x30) (concat (_ bv0 8) (_ bv1 1)) ?x48)))) + (let (($x62 (and true (= ?x60 ?x59)))) + (let (($x63 (and true $x62))) + (let ((?x73 (ite $x63 (_ bv0 9) (ite (and (and true (not $x62)) true) (_ bv1 9) (_ bv0 9))))) + (let (($x81 (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))))) + (let (($x43 (= ?x73 (_ bv511 9)))) + (or $x43 $x81)))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table.smt2 b/p4_symbolic/symbolic/expected/table.smt2 index f6ae7815..92278526 100644 --- a/p4_symbolic/symbolic/expected/table.smt2 +++ b/p4_symbolic/symbolic/expected/table.smt2 @@ -4,22 +4,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -27,22 +27,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -50,54 +50,48 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (let ((a!1 (and true - (not (and true (= standard_metadata.ingress_port #b000000000))) - true - (= standard_metadata.ingress_port #b000000001)))) -(let ((a!2 (ite (and true - (and true (= standard_metadata.ingress_port #b000000000))) - #b000000001 - (ite a!1 #b000000000 standard_metadata.egress_spec)))) - (ite (not (= a!2 #b111111111)) a!2 standard_metadata.egress_port))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid -(egress) standard_metadata.egress_spec: (let ((a!1 (and true - (not (and true (= standard_metadata.ingress_port #b000000000))) - true - (= standard_metadata.ingress_port #b000000001)))) - (ite (and true (and true (= standard_metadata.ingress_port #b000000000))) - #b000000001 - (ite a!1 #b000000000 standard_metadata.egress_spec))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 +(egress) standard_metadata.egress_port: (let ((a!1 (= (ite (and true + true + (= standard_metadata.ingress_port #b000000000)) + #b000000001 + #b000000000) + #b111111111))) + (ite (not a!1) + (ite (and true true (= standard_metadata.ingress_port #b000000000)) + #b000000001 + #b000000000) + standard_metadata.egress_port)) +(egress) standard_metadata.egress_rid: #x0000 +(egress) standard_metadata.egress_spec: (ite (and true true (= standard_metadata.ingress_port #b000000000)) + #b000000001 + #b000000000) +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x30 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x30))) + (let (($x19 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x19))) (assert - (let (($x30 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x31 (and true $x30))) - (let (($x34 (and true (not (and true (= standard_metadata.ingress_port (_ bv0 9))))))) - (let (($x27 (= standard_metadata.ingress_port (_ bv0 9)))) - (let (($x28 (and true $x27))) - (let (($x32 (and true $x28))) - (let ((?x46 (ite $x32 (_ bv1 9) (ite (and $x34 $x31) (_ bv0 9) standard_metadata.egress_spec)))) - (let (($x53 (or (or false (= ?x46 (_ bv0 9))) (= ?x46 (_ bv1 9))))) - (let (($x37 (= ?x46 (_ bv511 9)))) - (or $x37 $x53))))))))))) + (let (($x10 (= standard_metadata.ingress_port (_ bv0 9)))) + (let (($x22 (and true $x10))) + (let (($x17 (and true $x22))) + (let ((?x38 (ite $x17 (_ bv1 9) (_ bv0 9)))) + (let (($x42 (or (or false (= ?x38 (_ bv0 9))) (= ?x38 (_ bv1 9))))) + (let (($x29 (= ?x38 (_ bv511 9)))) + (or $x29 $x42)))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_1.smt2 b/p4_symbolic/symbolic/expected/table_hit_1.smt2 index 7ffdff09..aa8b2da1 100644 --- a/p4_symbolic/symbolic/expected/table_hit_1.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_1.smt2 @@ -9,22 +9,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -37,22 +37,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -73,15 +73,15 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (ite (and true (and true (= ethernet.ether_type #x0010))) 0 (- 1))) (a!2 (and true (not (and true (= ethernet.ether_type #x0010)))))) (let ((a!3 (ite (and true (and true (= ethernet.ether_type #x0010))) #b000000010 - (ite a!2 #b111111111 standard_metadata.egress_spec)))) + (ite a!2 #b111111111 #b000000000)))) (let ((a!4 (ite (and true (distinct a!1 (- 1)) true @@ -89,54 +89,53 @@ #b000000011 a!3))) (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (and true (= ethernet.ether_type #x0010))) 0 (- 1))) (a!2 (and true (not (and true (= ethernet.ether_type #x0010)))))) (let ((a!3 (ite (and true (and true (= ethernet.ether_type #x0010))) #b000000010 - (ite a!2 #b111111111 standard_metadata.egress_spec)))) + (ite a!2 #b111111111 #b000000000)))) (ite (and true (distinct a!1 (- 1)) true (= ethernet.src_addr #x000000000100)) #b000000011 a!3))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (assert - (let (($x95 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x90 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x85 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x80 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x71 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x67 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x72 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x67) $x71))) - (or (or (or (or (or $x72 $x75) $x80) $x85) $x90) $x95)))))))))) + (let (($x88 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x83 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x78 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x73 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x68 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x64 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x60 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x65 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x60) $x64))) + (or (or (or (or (or $x65 $x68) $x73) $x78) $x83) $x88)))))))))) (assert - (let ((?x38 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) - (let (($x31 (= ethernet.ether_type (_ bv16 16)))) - (let (($x32 (and true $x31))) - (let (($x33 (and true $x32))) - (let ((?x40 (ite $x33 0 (- 1)))) - (let (($x45 (and (distinct ?x40 (- 1)) true))) - (let (($x46 (and true $x45))) - (let (($x50 (and $x46 (and true (= ethernet.src_addr (_ bv256 48)))))) - (let ((?x56 (ite $x50 (_ bv3 9) (ite $x33 (_ bv2 9) ?x38)))) - (let (($x78 (or (or (or (or false (= ?x56 (_ bv0 9))) (= ?x56 (_ bv1 9))) (= ?x56 (_ bv2 9))) (= ?x56 (_ bv3 9))))) - (let (($x98 (or (or (or (or $x78 (= ?x56 (_ bv4 9))) (= ?x56 (_ bv5 9))) (= ?x56 (_ bv6 9))) (= ?x56 (_ bv7 9))))) - (let (($x58 (= ?x56 (_ bv511 9)))) - (or $x58 $x98)))))))))))))) + (let ((?x32 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) (_ bv0 9)))) + (let (($x30 (= ethernet.ether_type (_ bv16 16)))) + (let (($x15 (and true $x30))) + (let (($x27 (and true $x15))) + (let ((?x34 (ite $x27 0 (- 1)))) + (let (($x39 (and (distinct ?x34 (- 1)) true))) + (let (($x40 (and true $x39))) + (let (($x44 (and $x40 (and true (= ethernet.src_addr (_ bv256 48)))))) + (let ((?x50 (ite $x44 (_ bv3 9) (ite $x27 (_ bv2 9) ?x32)))) + (let (($x71 (or (or (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))) (= ?x50 (_ bv2 9))) (= ?x50 (_ bv3 9))))) + (let (($x91 (or (or (or (or $x71 (= ?x50 (_ bv4 9))) (= ?x50 (_ bv5 9))) (= ?x50 (_ bv6 9))) (= ?x50 (_ bv7 9))))) + (let (($x52 (= ?x50 (_ bv511 9)))) + (or $x52 $x91)))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_2.smt2 b/p4_symbolic/symbolic/expected/table_hit_2.smt2 index 38eb57aa..0ee87309 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_2.smt2 @@ -10,22 +10,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) h1.$extracted$: (ite true true false) @@ -39,22 +39,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) h1.$extracted$: (ite true true false) @@ -68,71 +68,69 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (= (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1))) (a!2 (distinct (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1)))) (let ((a!3 (ite (and true a!2 true (= h1.f2 #xff)) #b000000010 (ite (and true true (= h1.f1 #xff)) #b000000001 - (ite true (concat #x00 #b0) standard_metadata.egress_spec))))) + (ite true (concat #x00 #b0) #b000000000))))) (let ((a!4 (ite (and true a!1 true (= h1.f3 #xff)) #b000000011 a!3))) (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (= (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1))) (a!2 (distinct (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1)))) (let ((a!3 (ite (and true a!2 true (= h1.f2 #xff)) #b000000010 (ite (and true true (= h1.f1 #xff)) #b000000001 - (ite true (concat #x00 #b0) standard_metadata.egress_spec))))) + (ite true (concat #x00 #b0) #b000000000))))) (ite (and true a!1 true (= h1.f3 #xff)) #b000000011 a!3))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f1 () (_ BitVec 8)) (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x103 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x98 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x93 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x88 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x83 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x80 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x75) $x79))) - (or (or (or (or (or $x80 $x83) $x88) $x93) $x98) $x103)))))))))) + (let (($x95 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x75 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x71 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x67 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x72 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x67) $x71))) + (or (or (or (or (or $x72 $x75) $x80) $x85) $x90) $x95)))))))))) (assert - (let (($x37 (= h1.f1 (_ bv255 8)))) - (let (($x38 (and true $x37))) - (let (($x39 (and true $x38))) - (let ((?x45 (ite $x39 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let ((?x43 (ite $x39 0 (- 1)))) - (let (($x46 (and (distinct ?x43 (- 1)) true))) - (let (($x47 (and true $x46))) - (let (($x50 (and $x47 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x56 (= ?x43 (- 1)))) - (let (($x57 (and true $x56))) - (let (($x60 (and $x57 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x65 (ite $x60 (_ bv3 9) (ite $x50 (_ bv2 9) ?x45)))) - (let (($x86 (or (or (or (or false (= ?x65 (_ bv0 9))) (= ?x65 (_ bv1 9))) (= ?x65 (_ bv2 9))) (= ?x65 (_ bv3 9))))) - (let (($x106 (or (or (or (or $x86 (= ?x65 (_ bv4 9))) (= ?x65 (_ bv5 9))) (= ?x65 (_ bv6 9))) (= ?x65 (_ bv7 9))))) - (let (($x41 (= ?x65 (_ bv511 9)))) - (or $x41 $x106))))))))))))))))) + (let (($x18 (= h1.f1 (_ bv255 8)))) + (let (($x23 (and true $x18))) + (let (($x27 (and true $x23))) + (let ((?x36 (ite $x27 0 (- 1)))) + (let (($x39 (and (distinct ?x36 (- 1)) true))) + (let (($x40 (and true $x39))) + (let (($x43 (and $x40 (and true (= h1.f2 (_ bv255 8)))))) + (let (($x49 (= ?x36 (- 1)))) + (let (($x50 (and true $x49))) + (let (($x53 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x58 (ite $x53 (_ bv3 9) (ite $x43 (_ bv2 9) (ite $x27 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) (_ bv0 9))))))) + (let (($x78 (or (or (or (or false (= ?x58 (_ bv0 9))) (= ?x58 (_ bv1 9))) (= ?x58 (_ bv2 9))) (= ?x58 (_ bv3 9))))) + (let (($x98 (or (or (or (or $x78 (= ?x58 (_ bv4 9))) (= ?x58 (_ bv5 9))) (= ?x58 (_ bv6 9))) (= ?x58 (_ bv7 9))))) + (let (($x34 (= ?x58 (_ bv511 9)))) + (or $x34 $x98)))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_2.txt b/p4_symbolic/symbolic/expected/table_hit_2.txt index 859f6a36..399ab984 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.txt +++ b/p4_symbolic/symbolic/expected/table_hit_2.txt @@ -107,12 +107,12 @@ ________________________________________________________________________________ Finding packet for table MyIngress.t1 and row 0 ================================================================================ ingress_port = #b000000000 -egress_port = #b000000010 +egress_port = #b000000001 trace: dropped = 0 got cloned = 0 MyIngress.t1 => was matched on entry 0 -MyIngress.t2 => was matched on entry 0 +MyIngress.t2 => was matched on entry -1 MyIngress.t3 => was not matched! MyIngress.t4 => was matched on entry -1 tbl_table_hit_2l83 => was matched on entry -1 @@ -122,7 +122,7 @@ $got_cloned$ = false h1.$extracted$ = false h1.$valid$ = true h1.f1 = #xff -h1.f2 = #xff +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -152,7 +152,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #xff +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -182,7 +182,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #xff +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -194,9 +194,9 @@ standard_metadata.checksum_error = #b0 standard_metadata.deq_qdepth = #b0000000000000000000 standard_metadata.deq_timedelta = #x00000000 standard_metadata.egress_global_timestamp = #x000000000000 -standard_metadata.egress_port = #b000000010 +standard_metadata.egress_port = #b000000001 standard_metadata.egress_rid = #x0000 -standard_metadata.egress_spec = #b000000010 +standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 @@ -227,7 +227,7 @@ $got_cloned$ = false h1.$extracted$ = false h1.$valid$ = true h1.f1 = #xff -h1.f2 = #x7f +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -257,7 +257,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #x7f +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -287,7 +287,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #x7f +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2 index 0f876256..f77a53f4 100644 --- a/p4_symbolic/symbolic/expected/vrf.smt2 +++ b/p4_symbolic/symbolic/expected/vrf.smt2 @@ -26,22 +26,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -71,26 +71,26 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.eth_type)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.eth_type) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -296,10 +296,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.eth_type)) true false)) (a!3 (not (and true (= (bvand ipv4.srcAddr #x09210909) #x00210100))))) (let ((a!2 (and (and true a!1) @@ -347,9 +347,7 @@ (and (not a!7) (not a!8)) a!9) #b000000001 - (ite a!11 - #b000000001 - (ite a!12 #b111111111 standard_metadata.egress_spec))))) + (ite a!11 #b000000001 (ite a!12 #b111111111 #b000000000))))) (let ((a!14 (ite (and (and (and true a!1) (bvuge a!5 #b1)) (not a!7) a!8) #b000000000 a!13))) @@ -357,7 +355,7 @@ #b000000001 a!14))) (ite (not (= a!15 #b111111111)) a!15 standard_metadata.egress_port))))))))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.eth_type)) true false)) (a!3 (not (and true (= (bvand ipv4.srcAddr #x09210909) #x00210100))))) (let ((a!2 (and (and true a!1) @@ -405,72 +403,69 @@ (and (not a!7) (not a!8)) a!9) #b000000001 - (ite a!11 - #b000000001 - (ite a!12 #b111111111 standard_metadata.egress_spec))))) + (ite a!11 #b000000001 (ite a!12 #b111111111 #b000000000))))) (let ((a!14 (ite (and (and (and true a!1) (bvuge a!5 #b1)) (not a!7) a!8) #b000000000 a!13))) (ite (and (and (and true a!1) (bvuge a!5 #b1)) a!7) #b000000001 a!14)))))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.eth_type)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.eth_type) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun scalars.local_metadata_t.vrf () (_ BitVec 10)) (declare-fun ipv4.srcAddr () (_ BitVec 32)) (declare-fun ethernet.eth_type () (_ BitVec 16)) (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x181 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x181))) + (let (($x172 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x172))) (assert - (let ((?x61 (concat (_ bv0 9) (_ bv0 1)))) - (let (($x75 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) + (let ((?x53 (concat (_ bv0 9) (_ bv0 1)))) + (let (($x67 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) (let (($x11 (= (concat (_ bv0 4) (_ bv2048 12)) ethernet.eth_type))) (let (($x10 (and true $x11))) - (let (($x51 (ite $x10 true false))) - (let (($x64 (and true $x51))) - (let (($x79 (and (and $x64 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x75))) - (let ((?x91 (concat (_ bv0 9) (_ bv1 1)))) - (let (($x70 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) - (let (($x76 (and $x64 $x70))) - (let ((?x92 (ite $x76 ?x91 (ite $x79 ?x61 (ite true ?x61 scalars.local_metadata_t.vrf))))) - (let (($x101 (= ?x92 ?x61))) - (let (($x119 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x101))) - (let (($x113 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x92 ?x91)))) - (let (($x107 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x101))) - (let (($x102 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x101))) - (let (($x121 (not $x102))) - (let (($x125 (and $x121 (not $x107)))) - (let (($x129 (and $x125 (not $x113)))) - (let ((?x58 (ite false (_ bv1 1) (_ bv0 1)))) - (let ((?x87 (ite true (_ bv1 1) (_ bv0 1)))) - (let ((?x93 (ite $x76 ?x87 (ite $x79 ?x87 (ite true ?x58 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x94 (bvuge ?x93 (_ bv1 1)))) - (let (($x96 (and $x64 $x94))) - (let ((?x136 (ite (and $x96 (and $x129 (not $x119))) (_ bv511 9) standard_metadata.egress_spec))) - (let (($x131 (and (and $x96 $x129) $x119))) - (let (($x127 (and (and $x96 $x125) $x113))) - (let (($x123 (and (and $x96 $x121) $x107))) - (let (($x120 (and $x96 $x102))) - (let ((?x169 (ite $x120 (_ bv1 9) (ite $x123 (_ bv0 9) (ite $x127 (_ bv1 9) (ite $x131 (_ bv1 9) ?x136)))))) - (let (($x184 (or (or false (= ?x169 (_ bv0 9))) (= ?x169 (_ bv1 9))))) - (let (($x63 (= ?x169 (_ bv511 9)))) - (or $x63 $x184)))))))))))))))))))))))))))))))))) + (let (($x41 (ite $x10 true false))) + (let (($x56 (and true $x41))) + (let (($x71 (and (and $x56 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x67))) + (let ((?x83 (concat (_ bv0 9) (_ bv1 1)))) + (let (($x62 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) + (let (($x68 (and $x56 $x62))) + (let ((?x84 (ite $x68 ?x83 (ite $x71 ?x53 (ite true ?x53 scalars.local_metadata_t.vrf))))) + (let (($x93 (= ?x84 ?x53))) + (let (($x111 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x93))) + (let (($x105 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x84 ?x83)))) + (let (($x99 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x93))) + (let (($x94 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x93))) + (let (($x113 (not $x94))) + (let (($x117 (and $x113 (not $x99)))) + (let (($x121 (and $x117 (not $x105)))) + (let ((?x51 (ite false (_ bv1 1) (_ bv0 1)))) + (let ((?x79 (ite true (_ bv1 1) (_ bv0 1)))) + (let ((?x85 (ite $x68 ?x79 (ite $x71 ?x79 (ite true ?x51 scalars.local_metadata_t.vrf_is_valid))))) + (let (($x86 (bvuge ?x85 (_ bv1 1)))) + (let (($x88 (and $x56 $x86))) + (let (($x123 (and (and $x88 $x121) $x111))) + (let (($x119 (and (and $x88 $x117) $x105))) + (let ((?x145 (ite $x119 (_ bv1 9) (ite $x123 (_ bv1 9) (ite (and $x88 (and $x121 (not $x111))) (_ bv511 9) (_ bv0 9)))))) + (let (($x115 (and (and $x88 $x113) $x99))) + (let (($x112 (and $x88 $x94))) + (let ((?x160 (ite $x112 (_ bv1 9) (ite $x115 (_ bv0 9) ?x145)))) + (let (($x175 (or (or false (= ?x160 (_ bv0 9))) (= ?x160 (_ bv1 9))))) + (let (($x55 (= ?x160 (_ bv511 9)))) + (or $x55 $x175)))))))))))))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/vrf.txt b/p4_symbolic/symbolic/expected/vrf.txt index 1294c897..09ad9f68 100644 --- a/p4_symbolic/symbolic/expected/vrf.txt +++ b/p4_symbolic/symbolic/expected/vrf.txt @@ -26,7 +26,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0010 +ipv4.dstAddr = #x0a0a0004 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -72,7 +72,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0010 +ipv4.dstAddr = #x0a0a0004 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -118,7 +118,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0010 +ipv4.dstAddr = #x0a0a0004 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -630,7 +630,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x00000000 +ipv4.dstAddr = #x0a000000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -676,7 +676,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x00000000 +ipv4.dstAddr = #x0a000000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -722,7 +722,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x00000000 +ipv4.dstAddr = #x0a000000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -918,7 +918,7 @@ egress_port = #b000000001 trace: dropped = 0 got cloned = 0 -packet_ingress.ipv4_lpm_table => was matched on entry 1 +packet_ingress.ipv4_lpm_table => was matched on entry 2 packet_ingress.set_vrf_table => was matched on entry 1 tbl_vrf133 => was matched on entry -1 @@ -932,7 +932,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -978,7 +978,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1018,13 +1018,13 @@ egress_headers: $got_cloned$ = false ethernet.$extracted$ = true ethernet.$valid$ = true -ethernet.dstAddr = #x000000000000 +ethernet.dstAddr = #x00000000000a ethernet.eth_type = #x0800 ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1069,7 +1069,7 @@ egress_port = #b000000001 trace: dropped = 0 got cloned = 0 -packet_ingress.ipv4_lpm_table => was matched on entry 1 +packet_ingress.ipv4_lpm_table => was matched on entry 2 packet_ingress.set_vrf_table => was matched on entry 1 tbl_vrf133 => was matched on entry -1 @@ -1083,7 +1083,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1108,7 +1108,7 @@ standard_metadata.deq_timedelta = #x00000000 standard_metadata.egress_global_timestamp = #x000000000000 standard_metadata.egress_port = #b000000000 standard_metadata.egress_rid = #x0000 -standard_metadata.egress_spec = #b000100000 +standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 @@ -1129,7 +1129,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1154,7 +1154,7 @@ standard_metadata.deq_timedelta = #x00000000 standard_metadata.egress_global_timestamp = #x000000000000 standard_metadata.egress_port = #b000000000 standard_metadata.egress_rid = #x0000 -standard_metadata.egress_spec = #b000100000 +standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 @@ -1169,13 +1169,13 @@ egress_headers: $got_cloned$ = false ethernet.$extracted$ = true ethernet.$valid$ = true -ethernet.dstAddr = #x000000000000 +ethernet.dstAddr = #x00000000000a ethernet.eth_type = #x0800 ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 diff --git a/p4_symbolic/symbolic/v1model_intrinsic.h b/p4_symbolic/symbolic/v1model_intrinsic.h new file mode 100644 index 00000000..ee88c185 --- /dev/null +++ b/p4_symbolic/symbolic/v1model_intrinsic.h @@ -0,0 +1,33 @@ +// 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. + +#ifndef P4_SYMBOLIC_SYMBOLIC_V1MODEL_INTRINSIC_H_ +#define P4_SYMBOLIC_SYMBOLIC_V1MODEL_INTRINSIC_H_ + +namespace p4_symbolic::symbolic::v1model { + +// Possible values of the v1model `standard_metadata_t` field `instance_type` in +// BMv2. The semantics of these values is explained here: +// https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md +#define PKT_INSTANCE_TYPE_NORMAL 0 +#define PKT_INSTANCE_TYPE_INGRESS_CLONE 1 +#define PKT_INSTANCE_TYPE_EGRESS_CLONE 2 +#define PKT_INSTANCE_TYPE_COALESCED 3 +#define PKT_INSTANCE_TYPE_INGRESS_RECIRC 4 +#define PKT_INSTANCE_TYPE_REPLICATION 5 +#define PKT_INSTANCE_TYPE_RESUBMIT 6 + +} // namespace p4_symbolic::symbolic::v1model + +#endif // PINS_P4_SYMBOLIC_SYMBOLIC_V1MODEL_INTRINSIC_H_