[P4_Symbolic] Add golden test for packet synthesis for conditional.p4…

… and conditional_sequence.p4 (sonic-net#672)



Co-authored-by: kishanps <kishanps@google.com>

p4_symbolic/symbolic/BUILD.bazel

@@ -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"],

p4_symbolic/symbolic/expected/conditional.txt

@@ -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
+

p4_symbolic/symbolic/expected/conditional_sequence.txt

@@ -0,0 +1,90 @@
+Finding packet for table MyIngress.e1 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e2 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e3 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e4 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e5 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e6 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e7 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.e8 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i1 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i2 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i3 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i4 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i5 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i6 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i7 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.i8 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.t and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+
+Finding packet for table MyIngress.t and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+