[P4_Symbolic] Adding table_hit_entries_pb.txt files (sonic-net#695)

Co-authored-by: smolkaj <[email protected]>
Co-authored-by: kishanps <[email protected]>

p4_symbolic/symbolic/expected/table_hit_1.smt2

@@ -0,0 +1,167 @@
+; 
+(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 (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
+ (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+(assert
+ (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
+ (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (or $x49 $x93))))))))))))
+(assert
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
+ (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (and (and (not $x49) true) (= ?x38 (- 1)))))))))))))
+(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.ether_type () (_ BitVec 16))
+(declare-fun ethernet.src_addr () (_ BitVec 48))
+(assert
+ (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
+ (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+(assert
+ (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
+ (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (or $x49 $x93))))))))))))
+(assert
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
+ (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (let (($x207 (and (not $x49) true)))
+ (and $x207 (= ?x38 0)))))))))))))
+(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.ether_type () (_ BitVec 16))
+(declare-fun ethernet.src_addr () (_ BitVec 48))
+(assert
+ (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
+ (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+(assert
+ (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
+ (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (or $x49 $x93))))))))))))
+(assert
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x51 (ite $x48 0 (- 1))))
+ (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
+ (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (and (and (not $x49) $x44) (= ?x51 (- 1))))))))))))))
+(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.ether_type () (_ BitVec 16))
+(declare-fun ethernet.src_addr () (_ BitVec 48))
+(assert
+ (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
+ (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+(assert
+ (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
+ (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (or $x49 $x93))))))))))))
+(assert
+ (let (($x29 (= ethernet.ether_type (_ bv16 16))))
+ (let (($x30 (and true $x29)))
+ (let (($x31 (and true $x30)))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
+ (let ((?x51 (ite $x48 0 (- 1))))
+ (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
+ (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
+ (let (($x49 (= ?x54 (_ bv511 9))))
+ (and (and (not $x49) $x44) (= ?x51 0)))))))))))))
+(check-sat)
+

p4_symbolic/symbolic/expected/table_hit_1.txt

@@ -0,0 +1,18 @@
+Finding packet for table MyIngress.t_1 and row -1
+Cannot find solution!
+
+Finding packet for table MyIngress.t_1 and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000010
+
+Finding packet for table MyIngress.t_2 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000010
+
+Finding packet for table MyIngress.t_2 and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000011
+

p4_symbolic/testdata/conditional/table_hit_1_entries.pb.txt

@@ -0,0 +1,55 @@
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 41698643  # MyIngress.t_1
+      match {
+        field_id: 1  # hdr.ethernet.ether_type
+        exact {
+          value: "\x00\x10"
+        }
+      }
+      action {
+        action {
+          action_id: 29683729  # MyIngress.forward
+          params {
+            param_id: 1  # dst_addr
+            value: "\x00\x00\x00\x00\x00\x02"
+          }
+          params {
+            param_id: 2  # port
+            value: "\x02"
+          }
+        }
+      }
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 45015480  # MyIngress.t_2
+      match {
+        field_id: 1  # src_addr
+        exact {
+          value: "\x00\x00\x00\x00\x01\x00"
+        }
+      }
+      action {
+        action {
+          action_id: 29683729  # MyIngress.forward
+          params {
+            param_id: 1  # dst_addr
+            value: "\x00\x00\x00\x00\x00\x03"
+          }
+          params {
+            param_id: 2  # port
+            value: "\x03"
+          }
+        }
+      }
+    }
+  }
+}
+

p4_symbolic/testdata/conditional/table_hit_2_entries.pb.txt

@@ -0,0 +1,69 @@
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 44659798  # MyIngress.t1
+      match {
+        field_id: 1  # hdr.h1.f1
+        exact {
+          value: "\xff"
+        }
+      }
+      action {
+        action {
+          action_id: 29683729  # MyIngress.forward
+          params {
+            param_id: 1  # port
+            value: "\01"
+          }
+        }
+      }
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 40554969  # MyIngress.t2
+      match {
+        field_id: 1  # hdr.h1.f2
+        exact {
+          value: "\xff"
+        }
+      }
+      action {
+        action {
+          action_id: 29683729  # MyIngress.forward
+          params {
+            param_id: 1  # port
+            value: "\02"
+          }
+        }
+      }
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 36319071  # MyIngress.t3
+      match {
+        field_id: 1  # hdr.h1.f3
+        exact {
+          value: "\xff"
+        }
+      }
+      action {
+        action {
+          action_id: 29683729  # MyIngress.forward
+          params {
+            param_id: 1  # port
+            value: "\03"
+          }
+        }
+      }
+    }
+  }
+}