Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[P4_Symbolic] Initialize standard metadata fields to 0. #934

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

[P4_Symbolic] Initialize standard metadata fields to 0. #934

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
c96bb21
[P4-Symbolic] Assign egress_spec to egress_port only when the packet …
kishanps Jul 27, 2023
b29775c
[P4-Symbolic] Initialize standard metadata fields to 0.
kishanps Jul 27, 2023
7ef9039
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Jan 8, 2025
061a67a
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Jan 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 1 addition & 8 deletions p4_symbolic/symbolic/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ cc_library(
"table.h",
"util.h",
"v1model.h",
"v1model_intrinsic.h",
"values.h",
],
deps = [
Expand Down Expand Up @@ -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
Expand Down
119 changes: 59 additions & 60 deletions p4_symbolic/symbolic/expected/basic.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
32 changes: 16 additions & 16 deletions p4_symbolic/symbolic/expected/basic.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading
Loading