pping - Reduce verification complexity #47
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR tries to reduce the verification complexity (number of instructions it takes the verifier to verify the program) by breaking out parts of the program (specifically the packet parsing) into global functions that can be verified independently from the rest of the code.
The first commit just moves some struct members from the generic
parsing_contexstruct to thepacket_infostruct, partly because it semantically fits better, and partly to better separate the packet parsing functions from functions that operate on the information from the parsed packet. This will make it easier to break out the packet parsing into a global function later, as other functions will no longer require access to theparsing_contextanymore.The second commit removes some packet pointers in
packet_infoand instead adds a couple of fields (ip_lenandip_tos) that the FIB lookup needs. So instead of later retrieving relevant packet pointers and parse the necessary information to do a FIB lookup, parse the required information directly as part of the packet parsing stage and then simply get it frompacket_infowhen doing the FIB lookup.The third commit actually breaks out the packet parsing into global functions (one for tc and one for XDP), and this commit will require Toke's kernel fix to work if using the XDP ingress hook.
While this PR does sucessfully lower the verification complexity (and makes it possible to run it when compiled with LLVM-14 on kernels > 5.15 without hitting the 1m limit), it's a bit unclear how much of it can really be attributed to using global functions and how much of it is simply from restructuring the code. If one inlines the global functions, it takes ~302k insn to verify the program if compiled with LLVM-13 and ~301k if compiled with LLVM-14. But if called as global functions (as is done here), it takes ~231k (plus 228k for the global function) with LLVM-13 and ~221k (plus ~218k for the global function) with LLVM-14. So while the global functions do help reduce the maximum insn somewhat, total verification time will likely be a bit higher due to having to verify both the global function and the program (which added together takes more instructions).