dslab-epfl / klint

Repository for the "Automated Verification of Network Function Binaries" paper (NSDI'22).
MIT License
8 stars 5 forks source link

`make verify-dns_aaa_records` raise `Exception: Cannot borrow from an ephemeral allocation` #6

Closed tharvik closed 1 year ago

tharvik commented 1 year ago

when trying to verify nf/dns_aaa_records, it raises this weird exception. looking at the readme, its status is "Not verified". shall I also remove it in the coming up PR deleting the paper related files? or is it indeed a bug that should be addressed?

SolalPirelli commented 1 year ago

This is not paper-related, it was an extra thing during a semester project from some students, and is indeed not done.

"Ephemeral" here means "allocation that is not supposed to survive an iteration of the packet-processing loop", such as the packet buffer.

"Borrow" means a data structure needs (partial or total) ownership to a chunk of memory, for instance the hash map needs to partially own its keys so that their hashes can't change while they're used by the hash map.

tharvik commented 1 year ago

This is not paper-related, it was an extra thing during a semester project from some students, and is indeed not done.

So, do we remove it?

SolalPirelli commented 1 year ago

Yes, like the BPF stuff, we can remove it + add an indication on the readme that it exists at commit xyz.