Skip to content

Commit

Permalink
[P4_Symbolic] Add an $extracted$ field for each header in the symbo…
Browse files Browse the repository at this point in the history 
…lic guarded map. (#812)



Co-authored-by: kishanps <[email protected]>
Co-authored-by: smolkaj <[email protected]>
  • Loading branch information
@VSuryaprasad-HCL @kishanps @smolkaj
3 people authored Dec 11, 2024
1 parent 756827b commit 00398d4
Show file tree
Hide file tree
Showing 14 changed files with 2,195 additions and 2,182 deletions.
412 changes: 206 additions & 206 deletions p4_symbolic/symbolic/expected/basic.smt2
View file

Large diffs are not rendered by default.

186 changes: 93 additions & 93 deletions p4_symbolic/symbolic/expected/conditional.smt2
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,31 +4,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x39 (ite $x31 $x33 false)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) $x39) (= (- 1) (- 1))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x42 (ite $x34 $x36 false)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(and (and (not $x57) $x42) (= (- 1) (- 1))))))))))))))
(check-sat)

;
Expand All @@ -37,31 +37,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ 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 (($x40 (ite $x31 false $x34)))
(let ((?x38 (ite $x34 (_ bv511 9) (ite (and true $x31) (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x38)))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) $x40) (= (- 1) (- 1))))))))))))))
(let (($x37 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x43 (ite $x34 false $x37)))
(let ((?x41 (ite $x37 (_ bv511 9) (ite (and true $x34) (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x41)))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(and (and (not $x57) $x43) (= (- 1) (- 1))))))))))))))
(check-sat)

;
Expand All @@ -70,31 +70,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x49 (ite $x44 0 (- 1))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) true) (= ?x49 (- 1))))))))))))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x52 (ite $x47 0 (- 1))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not $x46)) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(and (and (not $x57) true) (= ?x52 (- 1))))))))))))))
(check-sat)

;
Expand All @@ -103,31 +103,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x49 (ite $x44 0 (- 1))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(let (($x97 (and (not $x54) true)))
(and $x97 (= ?x49 0))))))))))))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x52 (ite $x47 0 (- 1))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not $x46)) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(let (($x100 (and (not $x57) true)))
(and $x100 (= ?x52 0))))))))))))))
(check-sat)

Loading

0 comments on commit 00398d4

Please sign in to comment.