Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins …
Browse files Browse the repository at this point in the history 
…into combined_1
  • Loading branch information
@VSuryaprasad-HCL
VSuryaprasad-HCL committed Oct 30, 2024
2 parents 4febf07 + 4e95a68 commit 86aabaa
Show file tree
Hide file tree
Showing 32 changed files with 4,084 additions and 82 deletions.
20 changes: 20 additions & 0 deletions p4_symbolic/symbolic/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,26 @@ end_to_end_test(
table_entries = "//p4_symbolic/testdata:string-optional/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
# smaller SMT formulas, hence better constraint solving performance.
end_to_end_test(
name = "condtional_test",
output_golden_file = "expected/conditional.txt",
p4_program = "//p4_symbolic/testdata:conditional/conditional.p4",
smt_golden_file = "expected/conditional.smt2",
table_entries = "//p4_symbolic/testdata:conditional/conditional_entries.pb.txt",
)

end_to_end_test(
name = "conditional_sequence_test",
output_golden_file = "expected/conditional_sequence.txt",
p4_program = "//p4_symbolic/testdata:conditional/conditional_sequence.p4",
smt_golden_file = "expected/conditional_sequence.smt2",
table_entries = "//p4_symbolic/testdata:conditional/conditional_sequence_entries.pb.txt",
)

cc_test(
name = "values_test",
srcs = ["values_test.cc"],
Expand Down
159 changes: 159 additions & 0 deletions p4_symbolic/symbolic/expected/conditional.smt2
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,159 @@
;
(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 (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let ((?x44 (ite (and $x33 (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x41 (and $x33 $x40)))
(let (($x34 (and true (not $x31))))
(let (($x56 (and $x34 (not (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))))
(let (($x53 (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))
(let (($x54 (and $x34 $x53)))
(let ((?x59 (ite $x54 (_ bv1 9) (ite $x56 (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(or $x65 (or (or false (= ?x59 (_ bv0 9))) (= ?x59 (_ bv1 9)))))))))))))))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x61 (ite $x31 $x33 false)))
(let ((?x44 (ite (and $x33 (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x41 (and $x33 $x40)))
(let (($x34 (and true (not $x31))))
(let (($x56 (and $x34 (not (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))))
(let (($x53 (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))
(let (($x54 (and $x34 $x53)))
(let ((?x59 (ite $x54 (_ bv1 9) (ite $x56 (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(and (and (not $x65) $x61) (= (- 1) (- 1)))))))))))))))))
(check-sat)

;
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let ((?x44 (ite (and $x33 (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x41 (and $x33 $x40)))
(let (($x34 (and true (not $x31))))
(let (($x56 (and $x34 (not (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))))
(let (($x53 (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))
(let (($x54 (and $x34 $x53)))
(let ((?x59 (ite $x54 (_ bv1 9) (ite $x56 (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(or $x65 (or (or false (= ?x59 (_ bv0 9))) (= ?x59 (_ bv1 9)))))))))))))))))
(assert
(let (($x34 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x64 (ite $x31 false $x34)))
(let (($x33 (and true $x31)))
(let ((?x44 (ite (and $x33 (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x41 (and $x33 $x40)))
(let (($x56 (and $x34 (not (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))))
(let (($x53 (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))
(let (($x54 (and $x34 $x53)))
(let ((?x59 (ite $x54 (_ bv1 9) (ite $x56 (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(and (and (not $x65) $x64) (= (- 1) (- 1)))))))))))))))))
(check-sat)

;
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let ((?x44 (ite (and $x33 (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x41 (and $x33 $x40)))
(let (($x34 (and true (not $x31))))
(let (($x56 (and $x34 (not (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))))
(let (($x53 (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))
(let (($x54 (and $x34 $x53)))
(let ((?x59 (ite $x54 (_ bv1 9) (ite $x56 (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(or $x65 (or (or false (= ?x59 (_ bv0 9))) (= ?x59 (_ bv1 9)))))))))))))))))
(assert
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x41 (and $x33 $x40)))
(let ((?x50 (ite $x41 (_ bv2 48) ethernet.dst_addr)))
(let (($x53 (and true (= ?x50 (_ bv1 48)))))
(let (($x34 (and true (not $x31))))
(let (($x54 (and $x34 $x53)))
(let ((?x63 (ite $x31 (ite $x41 0 (- 1)) (ite $x54 0 (- 1)))))
(let (($x62 (ite $x31 $x33 $x34)))
(let ((?x44 (ite (and $x33 (not $x40)) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x59 (ite $x54 (_ bv1 9) (ite (and $x34 (not $x53)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(and (and (not $x65) $x62) (= ?x63 (- 1))))))))))))))))))
(check-sat)

;
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let ((?x44 (ite (and $x33 (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x41 (and $x33 $x40)))
(let (($x34 (and true (not $x31))))
(let (($x56 (and $x34 (not (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))))
(let (($x53 (and true (= (ite $x41 (_ bv2 48) ethernet.dst_addr) (_ bv1 48)))))
(let (($x54 (and $x34 $x53)))
(let ((?x59 (ite $x54 (_ bv1 9) (ite $x56 (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(or $x65 (or (or false (= ?x59 (_ bv0 9))) (= ?x59 (_ bv1 9)))))))))))))))))
(assert
(let (($x39 (= ethernet.dst_addr (_ bv1 48))))
(let (($x40 (and true $x39)))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x41 (and $x33 $x40)))
(let ((?x50 (ite $x41 (_ bv2 48) ethernet.dst_addr)))
(let (($x53 (and true (= ?x50 (_ bv1 48)))))
(let (($x34 (and true (not $x31))))
(let (($x54 (and $x34 $x53)))
(let ((?x63 (ite $x31 (ite $x41 0 (- 1)) (ite $x54 0 (- 1)))))
(let (($x62 (ite $x31 $x33 $x34)))
(let ((?x44 (ite (and $x33 (not $x40)) (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x59 (ite $x54 (_ bv1 9) (ite (and $x34 (not $x53)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x41 (_ bv1 9) ?x44))))))
(let (($x65 (= ?x59 (_ bv511 9))))
(let (($x205 (and (not $x65) $x62)))
(and $x205 (= ?x63 0))))))))))))))))))
(check-sat)

18 changes: 18 additions & 0 deletions p4_symbolic/symbolic/expected/conditional.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
Finding packet for table MyIngress.t_1 and row -1
Dropped = 0
standard_metadata.ingress_port = #b000000000
standard_metadata.egress_spec = #b000000001

Finding packet for table MyIngress.t_2 and row -1
Dropped = 0
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000001

Finding packet for table MyIngress.t_3 and row -1
Cannot find solution!

Finding packet for table MyIngress.t_3 and row 0
Dropped = 0
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000001

Loading

0 comments on commit 86aabaa

Please sign in to comment.