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

* [P4-Symbolic] Assign egress_spec to egress_port only when the packet is not dropped in ingress.

* [P4-Symbolic] Initialize standard metadata fields to 0.

---------

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

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

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)

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