search

guodong / tobdd

First-ever high-throughput BDD library for scalable data plane verification
Apache License 2.0
0 stars 1 forks source link

How do we handle NAT? #1

Open dhalperi opened 1 year ago

dhalperi commented 1 year ago

Came here after reading the poster at SIGCOMM. Thanks!

An important part of dataplane verification is NAT. A subpart of that is erasing some bits and replacing them. You can see this code here for Batfish: EraseAndSet is used in, for example, assigning IPs and ports after NAT.

How do we get the bdd#exist operation for existential quantification, as well as projection and swapping bits in BDDs, etc.?

guodong commented 1 year ago

Hi dhalperi, thanks for your attention. For erasing/replacing/adding bits for a predicate, e.g., ab -> \bar{b}c, you can simply construct a new predicate and just ignore/replace/add that variables by !getVar(1) & getVar(2) (assume that you create vars with order a/b/c). Or you can use !b & c if b and c are references to BDD node instances.

I didn't implement first order logic in this implementation, that should be added in future.